- Rewrote all main traversal logics to use inline functions.
- Added -t12. This is much faster than -t10, but yields equal states, and made it the default choice.
This commit is contained in:
ccremers
parent
03ccf10960
commit
4d60acf431
@ -79,7 +79,7 @@ main (int argc, char **argv)
|
||||
struct arg_file *infile = arg_file0(NULL,NULL,"FILE", "input file ('-' for stdin)");
|
||||
struct arg_file *outfile = arg_file0("o","output","FILE", "output file (default is stdout)");
|
||||
struct arg_int *traversal = arg_int0 ("t", "traverse", NULL,
|
||||
"set traversal method, partial order reduction (default is 10)");
|
||||
"set traversal method, partial order reduction (default is 12)");
|
||||
struct arg_int *match =
|
||||
arg_int0 ("m", "match", NULL, "matching method (default is 0)");
|
||||
struct arg_lit *clp =
|
||||
@ -161,7 +161,7 @@ main (int argc, char **argv)
|
||||
debugl->ival[0] = 0;
|
||||
porparam->ival[0] = 0;
|
||||
#endif
|
||||
traversal->ival[0] = 10;
|
||||
traversal->ival[0] = 12;
|
||||
match->ival[0] = 0;
|
||||
maxlength->ival[0] = -1;
|
||||
maxruns->ival[0] = INT_MAX;
|
||||
|
||||
@ -33,14 +33,17 @@ extern Term CLAIM_Nisynch;
|
||||
Some forward declarations.
|
||||
*/
|
||||
|
||||
int traverseSimple (const System oldsys);
|
||||
int traverseNonReads (const System oldsys);
|
||||
int traversePOR (const System oldsys);
|
||||
int traversePOR2 (const System oldsys);
|
||||
int traversePOR2b (const System oldsys);
|
||||
int traversePOR3 (const System oldsys);
|
||||
int traversePOR4 (const System oldsys);
|
||||
int traversePOR5 (const System oldsys);
|
||||
__inline__ int traverseSimple (const System oldsys);
|
||||
__inline__ int traverseNonReads (const System oldsys);
|
||||
__inline__ int traversePOR (const System oldsys);
|
||||
__inline__ int traversePOR2 (const System oldsys);
|
||||
__inline__ int traversePOR2b (const System oldsys);
|
||||
__inline__ int traversePOR3 (const System oldsys);
|
||||
__inline__ int traversePOR4 (const System oldsys);
|
||||
__inline__ int traversePOR5 (const System oldsys);
|
||||
__inline__ int traversePOR6 (const System oldsys);
|
||||
__inline__ int traversePOR7 (const System oldsys);
|
||||
__inline__ int traversePOR8 (const System oldsys);
|
||||
int propertyCheck (const System sys);
|
||||
int executeTry (const System sys, int run);
|
||||
int claimSecrecy (const System sys, const Term t);
|
||||
@ -101,6 +104,8 @@ traverse (const System sys)
|
||||
return traversePOR6 (sys);
|
||||
case 11:
|
||||
return traversePOR7 (sys);
|
||||
case 12:
|
||||
return traversePOR8 (sys);
|
||||
default:
|
||||
debug (2, "This is NOT an existing traversal method !");
|
||||
exit (1);
|
||||
@ -495,7 +500,7 @@ explorify (const System sys, const int run)
|
||||
return 1; // The event was indeed enabled (irrespective of traverse!)
|
||||
}
|
||||
|
||||
int
|
||||
__inline__ int
|
||||
traverseSimple (const System sys)
|
||||
{
|
||||
/* simple nondeterministic traversal */
|
||||
@ -530,7 +535,7 @@ traverseSimple (const System sys)
|
||||
#define isRead(sys,rd) ( rd != NULL && predRead(sys,rd) )
|
||||
#define nonRead(sys,rd) ( rd != NULL && !predRead(sys,rd) )
|
||||
|
||||
int
|
||||
__inline__ int
|
||||
nonReads (const System sys)
|
||||
{
|
||||
/* all sends first, then simple nondeterministic traversal */
|
||||
@ -550,7 +555,7 @@ nonReads (const System sys)
|
||||
return 0;
|
||||
}
|
||||
|
||||
int
|
||||
__inline__ int
|
||||
traverseNonReads (const System sys)
|
||||
{
|
||||
if (nonReads (sys))
|
||||
@ -678,7 +683,7 @@ traversePOR (const System sys)
|
||||
* New partial order reduction, which ought to be much more intuitive.
|
||||
*/
|
||||
|
||||
int
|
||||
__inline__ int
|
||||
traversePOR2b (const System sys)
|
||||
{
|
||||
Roledef runPoint;
|
||||
@ -829,7 +834,7 @@ traversePOR2b (const System sys)
|
||||
}
|
||||
}
|
||||
|
||||
int
|
||||
__inline__ int
|
||||
traversePOR2 (const System sys)
|
||||
{
|
||||
Roledef runPoint;
|
||||
@ -962,7 +967,7 @@ traversePOR2 (const System sys)
|
||||
}
|
||||
}
|
||||
|
||||
int
|
||||
__inline__ int
|
||||
traversePOR3 (const System sys)
|
||||
{
|
||||
Roledef rd;
|
||||
@ -1017,6 +1022,112 @@ traversePOR3 (const System sys)
|
||||
return 0;
|
||||
}
|
||||
|
||||
//! Execute a read in the knowledge postponing way, on which the partial order reduction for secrecy depends.
|
||||
|
||||
__inline__ int
|
||||
tryChoiceRead (const System sys, const int run, const Roledef rd)
|
||||
{
|
||||
int flag;
|
||||
|
||||
flag = 0;
|
||||
|
||||
/* the sendsdone check only prevent
|
||||
* some unneccessary inKnowledge tests,
|
||||
* and branch tests, still improves
|
||||
* about 15% */
|
||||
if (sys->knowPhase > rd->knowPhase)
|
||||
{
|
||||
/* apparently there has been a new knowledge item since the
|
||||
* previous check */
|
||||
|
||||
/* implicit check for enabledness */
|
||||
flag = executeTry (sys, run);
|
||||
|
||||
/* if it was enabled (flag) we postpone it if it makes sense
|
||||
* to do so (hasVariable, non internal) */
|
||||
if (flag && hasTermVariable (rd->message) && !rd->internal)
|
||||
{
|
||||
int stackKnowPhase = rd->knowPhase;
|
||||
|
||||
rd->knowPhase = sys->knowPhase;
|
||||
if (sys->clp)
|
||||
{
|
||||
block_clp (sys, run);
|
||||
}
|
||||
else
|
||||
{
|
||||
block_basic (sys, run);
|
||||
}
|
||||
rd->knowPhase = stackKnowPhase;
|
||||
}
|
||||
}
|
||||
return flag;
|
||||
}
|
||||
|
||||
//! Try to execute the event at the roledef. Returns true iff it was enabled, and thus explored.
|
||||
/**
|
||||
* Note that rd should not be NULL
|
||||
*/
|
||||
__inline__ int
|
||||
tryChoiceRoledef (const System sys, const int run, const Roledef rd)
|
||||
{
|
||||
int flag;
|
||||
|
||||
#ifdef DEBUG
|
||||
if (rd == NULL)
|
||||
error ("tryChoiceRoledef should not be called with a NULL rd pointer");
|
||||
#endif
|
||||
|
||||
flag = 0;
|
||||
switch (rd->type)
|
||||
{
|
||||
case CLAIM:
|
||||
case SEND:
|
||||
flag = executeTry (sys, run);
|
||||
break;
|
||||
|
||||
case READ:
|
||||
flag = tryChoiceRead (sys, run, rd);
|
||||
break;
|
||||
|
||||
default:
|
||||
fprintf (stderr, "Encountered unknown event type %i.\n", rd->type);
|
||||
exit (1);
|
||||
}
|
||||
return flag;
|
||||
}
|
||||
|
||||
//! Try to execute the event in a given run
|
||||
__inline__ int
|
||||
tryChoiceRun (const System sys, const int run)
|
||||
{
|
||||
Roledef rd;
|
||||
|
||||
rd = runPointerGet (sys, run);
|
||||
if (rd != NULL)
|
||||
return tryChoiceRoledef (sys, run, rd);
|
||||
else
|
||||
return 0;
|
||||
}
|
||||
|
||||
//! Yield the last active run in the partial trace, or 0 if there is none.
|
||||
|
||||
__inline__ int
|
||||
lastActiveRun (const System sys)
|
||||
{
|
||||
if (sys->step == 0)
|
||||
{
|
||||
/* first step, start at 0 */
|
||||
return 0;
|
||||
}
|
||||
else
|
||||
{
|
||||
/* there was a previous action, start scan from there */
|
||||
return sys->traceRun[sys->step - 1] + sys->porparam;
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
/*
|
||||
* POR4
|
||||
*
|
||||
@ -1026,7 +1137,7 @@ traversePOR3 (const System sys)
|
||||
* Based on some new considerations.
|
||||
*/
|
||||
|
||||
int
|
||||
__inline__ int
|
||||
traversePOR4 (const System sys)
|
||||
{
|
||||
Roledef rd;
|
||||
@ -1049,71 +1160,14 @@ traversePOR4 (const System sys)
|
||||
* and where lastrun is the runid of the previous event
|
||||
* in the trace, or 0 if there was none.
|
||||
*/
|
||||
if (sys->step == 0)
|
||||
{
|
||||
/* first step, start at 0 */
|
||||
offset = 0;
|
||||
}
|
||||
else
|
||||
{
|
||||
/* there was a previous action, start scan from there */
|
||||
offset = sys->traceRun[sys->step - 1] + sys->porparam;
|
||||
}
|
||||
offset = lastActiveRun (sys);
|
||||
|
||||
/* Try all events (implicitly we only handle enabled ones) starting with our
|
||||
* first choice. If one was chosen, flag is set, and the loop aborts. */
|
||||
for (i = 0; i < sys->maxruns && !flag; i++)
|
||||
{
|
||||
run = (i + offset) % sys->maxruns;
|
||||
rd = runPointerGet (sys, run);
|
||||
|
||||
if (rd != NULL)
|
||||
{
|
||||
switch (rd->type)
|
||||
{
|
||||
case CLAIM:
|
||||
case SEND:
|
||||
flag = executeTry (sys, run);
|
||||
break;
|
||||
|
||||
case READ:
|
||||
/* the sendsdone check only prevent
|
||||
* some unneccessary inKnowledge tests,
|
||||
* and branch tests, still improves
|
||||
* about 15% */
|
||||
if (sys->knowPhase > rd->knowPhase)
|
||||
{
|
||||
/* apparently there has been a new knowledge item since the
|
||||
* previous check */
|
||||
|
||||
/* implicit check for enabledness */
|
||||
flag = executeTry (sys, run);
|
||||
|
||||
/* if it was enabled (flag) we postpone it if it makes sense
|
||||
* to do so (hasVariable, non internal) */
|
||||
if (flag && hasTermVariable (rd->message) && !rd->internal)
|
||||
{
|
||||
int stackKnowPhase = rd->knowPhase;
|
||||
|
||||
rd->knowPhase = sys->knowPhase;
|
||||
if (sys->clp)
|
||||
{
|
||||
block_clp (sys, run);
|
||||
}
|
||||
else
|
||||
{
|
||||
block_basic (sys, run);
|
||||
}
|
||||
rd->knowPhase = stackKnowPhase;
|
||||
}
|
||||
}
|
||||
break;
|
||||
|
||||
default:
|
||||
fprintf (stderr, "Encountered unknown event type %i.\n", rd->type);
|
||||
exit (1);
|
||||
}
|
||||
}
|
||||
flag = tryChoiceRun (sys, run);
|
||||
}
|
||||
return flag;
|
||||
}
|
||||
@ -1124,7 +1178,7 @@ traversePOR4 (const System sys)
|
||||
* POR4 but does chooses first.
|
||||
*/
|
||||
|
||||
int
|
||||
__inline__ int
|
||||
traversePOR5 (const System sys)
|
||||
{
|
||||
Roledef rd;
|
||||
@ -1147,18 +1201,9 @@ traversePOR5 (const System sys)
|
||||
* and where lastrun is the runid of the previous event
|
||||
* in the trace, or 0 if there was none.
|
||||
*/
|
||||
if (sys->step == 0)
|
||||
{
|
||||
/* first step, start at 0 */
|
||||
offset = 0;
|
||||
}
|
||||
else
|
||||
{
|
||||
/* there was a previous action, start scan from there */
|
||||
offset = sys->traceRun[sys->step - 1] + sys->porparam;
|
||||
}
|
||||
offset = lastActiveRun (sys);
|
||||
|
||||
/* First pick out any choose events */
|
||||
/* First pick out any choose events */
|
||||
for (i = 0; i < sys->maxruns && !flag; i++)
|
||||
{
|
||||
run = (i + offset) % sys->maxruns;
|
||||
@ -1174,9 +1219,7 @@ traversePOR5 (const System sys)
|
||||
|
||||
case READ:
|
||||
if (rd->internal)
|
||||
{
|
||||
flag = executeTry (sys, run);
|
||||
}
|
||||
break;
|
||||
|
||||
default:
|
||||
@ -1191,55 +1234,7 @@ traversePOR5 (const System sys)
|
||||
for (i = 0; i < sys->maxruns && !flag; i++)
|
||||
{
|
||||
run = (i + offset) % sys->maxruns;
|
||||
rd = runPointerGet (sys, run);
|
||||
|
||||
if (rd != NULL)
|
||||
{
|
||||
switch (rd->type)
|
||||
{
|
||||
case CLAIM:
|
||||
case SEND:
|
||||
flag = executeTry (sys, run);
|
||||
break;
|
||||
|
||||
case READ:
|
||||
/* the sendsdone check only prevent
|
||||
* some unneccessary inKnowledge tests,
|
||||
* and branch tests, still improves
|
||||
* about 15% */
|
||||
if (sys->knowPhase > rd->knowPhase)
|
||||
{
|
||||
/* apparently there has been a new knowledge item since the
|
||||
* previous check */
|
||||
|
||||
/* implicit check for enabledness */
|
||||
flag = executeTry (sys, run);
|
||||
|
||||
/* if it was enabled (flag) we postpone it if it makes sense
|
||||
* to do so (hasVariable, non internal) */
|
||||
if (flag && hasTermVariable (rd->message) && !rd->internal)
|
||||
{
|
||||
int stackKnowPhase = rd->knowPhase;
|
||||
|
||||
rd->knowPhase = sys->knowPhase;
|
||||
if (sys->clp)
|
||||
{
|
||||
block_clp (sys, run);
|
||||
}
|
||||
else
|
||||
{
|
||||
block_basic (sys, run);
|
||||
}
|
||||
rd->knowPhase = stackKnowPhase;
|
||||
}
|
||||
}
|
||||
break;
|
||||
|
||||
default:
|
||||
fprintf (stderr, "Encountered unknown event type %i.\n", rd->type);
|
||||
exit (1);
|
||||
}
|
||||
}
|
||||
flag = tryChoiceRun (sys, run);
|
||||
}
|
||||
return flag;
|
||||
}
|
||||
@ -1250,7 +1245,7 @@ traversePOR5 (const System sys)
|
||||
* POR5 but has a left-oriented scan instead of working from the current run.
|
||||
*/
|
||||
|
||||
int
|
||||
__inline__ int
|
||||
traversePOR6 (const System sys)
|
||||
{
|
||||
Roledef rd;
|
||||
@ -1259,13 +1254,6 @@ traversePOR6 (const System sys)
|
||||
int i;
|
||||
int offset;
|
||||
|
||||
/* Previously we did the sends first. This does not always improve things,
|
||||
* depending on the protocol.
|
||||
*/
|
||||
// if (nonReads (sys)) return 1;
|
||||
|
||||
/* a choice for choose */
|
||||
|
||||
/* The 'choose' implemented here is the following:
|
||||
*
|
||||
* choose ev#rid
|
||||
@ -1274,57 +1262,10 @@ traversePOR6 (const System sys)
|
||||
|
||||
/* Try all events (implicitly we only handle enabled ones) left-to-right.
|
||||
* If one was chosen, flag is set, and the loop aborts. */
|
||||
|
||||
for (run = 0; run < sys->maxruns && !flag; run++)
|
||||
{
|
||||
rd = runPointerGet (sys, run);
|
||||
|
||||
if (rd != NULL)
|
||||
{
|
||||
switch (rd->type)
|
||||
{
|
||||
case CLAIM:
|
||||
case SEND:
|
||||
flag = executeTry (sys, run);
|
||||
break;
|
||||
|
||||
case READ:
|
||||
/* the sendsdone check only prevent
|
||||
* some unneccessary inKnowledge tests,
|
||||
* and branch tests, still improves
|
||||
* about 15% */
|
||||
if (sys->knowPhase > rd->knowPhase)
|
||||
{
|
||||
/* apparently there has been a new knowledge item since the
|
||||
* previous check */
|
||||
|
||||
/* implicit check for enabledness */
|
||||
flag = executeTry (sys, run);
|
||||
|
||||
/* if it was enabled (flag) we postpone it if it makes sense
|
||||
* to do so (hasVariable, non internal) */
|
||||
if (flag && hasTermVariable (rd->message) && !rd->internal)
|
||||
{
|
||||
int stackKnowPhase = rd->knowPhase;
|
||||
|
||||
rd->knowPhase = sys->knowPhase;
|
||||
if (sys->clp)
|
||||
{
|
||||
block_clp (sys, run);
|
||||
}
|
||||
else
|
||||
{
|
||||
block_basic (sys, run);
|
||||
}
|
||||
rd->knowPhase = stackKnowPhase;
|
||||
}
|
||||
}
|
||||
break;
|
||||
|
||||
default:
|
||||
fprintf (stderr, "Encountered unknown event type %i.\n", rd->type);
|
||||
exit (1);
|
||||
}
|
||||
}
|
||||
flag = tryChoiceRun (sys, run);
|
||||
}
|
||||
return flag;
|
||||
}
|
||||
@ -1335,7 +1276,7 @@ traversePOR6 (const System sys)
|
||||
* Left-oriented scan, to ensure reductions. However, first does all initial actions.
|
||||
*/
|
||||
|
||||
int
|
||||
__inline__ int
|
||||
traversePOR7 (const System sys)
|
||||
{
|
||||
Roledef rd;
|
||||
@ -1364,109 +1305,52 @@ traversePOR7 (const System sys)
|
||||
rd = runPointerGet (sys, run);
|
||||
if (rd == sys->runs[run].start)
|
||||
{
|
||||
switch (rd->type)
|
||||
{
|
||||
case CLAIM:
|
||||
case SEND:
|
||||
flag = executeTry (sys, run);
|
||||
break;
|
||||
|
||||
case READ:
|
||||
/* the sendsdone check only prevent
|
||||
* some unneccessary inKnowledge tests,
|
||||
* and branch tests, still improves
|
||||
* about 15% */
|
||||
if (sys->knowPhase > rd->knowPhase)
|
||||
{
|
||||
/* apparently there has been a new knowledge item since the
|
||||
* previous check */
|
||||
|
||||
/* implicit check for enabledness */
|
||||
flag = executeTry (sys, run);
|
||||
|
||||
/* if it was enabled (flag) we postpone it if it makes sense
|
||||
* to do so (hasVariable, non internal) */
|
||||
if (flag && hasTermVariable (rd->message) && !rd->internal)
|
||||
{
|
||||
int stackKnowPhase = rd->knowPhase;
|
||||
|
||||
rd->knowPhase = sys->knowPhase;
|
||||
if (sys->clp)
|
||||
{
|
||||
block_clp (sys, run);
|
||||
}
|
||||
else
|
||||
{
|
||||
block_basic (sys, run);
|
||||
}
|
||||
rd->knowPhase = stackKnowPhase;
|
||||
}
|
||||
}
|
||||
break;
|
||||
|
||||
default:
|
||||
fprintf (stderr, "Encountered unknown event type %i.\n", rd->type);
|
||||
exit (1);
|
||||
}
|
||||
flag = tryChoiceRoledef (sys, run, rd);
|
||||
}
|
||||
}
|
||||
/* Try all other events (implicitly we only handle enabled ones) left-to-right.
|
||||
* If one was chosen, flag is set, and the loop aborts. */
|
||||
for (run = 0; run < sys->maxruns && !flag; run++)
|
||||
{
|
||||
rd = runPointerGet (sys, run);
|
||||
|
||||
if (rd != NULL)
|
||||
{
|
||||
switch (rd->type)
|
||||
{
|
||||
case CLAIM:
|
||||
case SEND:
|
||||
flag = executeTry (sys, run);
|
||||
break;
|
||||
|
||||
case READ:
|
||||
/* the sendsdone check only prevent
|
||||
* some unneccessary inKnowledge tests,
|
||||
* and branch tests, still improves
|
||||
* about 15% */
|
||||
if (sys->knowPhase > rd->knowPhase)
|
||||
{
|
||||
/* apparently there has been a new knowledge item since the
|
||||
* previous check */
|
||||
|
||||
/* implicit check for enabledness */
|
||||
flag = executeTry (sys, run);
|
||||
|
||||
/* if it was enabled (flag) we postpone it if it makes sense
|
||||
* to do so (hasVariable, non internal) */
|
||||
if (flag && hasTermVariable (rd->message) && !rd->internal)
|
||||
{
|
||||
int stackKnowPhase = rd->knowPhase;
|
||||
|
||||
rd->knowPhase = sys->knowPhase;
|
||||
if (sys->clp)
|
||||
{
|
||||
block_clp (sys, run);
|
||||
}
|
||||
else
|
||||
{
|
||||
block_basic (sys, run);
|
||||
}
|
||||
rd->knowPhase = stackKnowPhase;
|
||||
}
|
||||
}
|
||||
break;
|
||||
|
||||
default:
|
||||
fprintf (stderr, "Encountered unknown event type %i.\n", rd->type);
|
||||
exit (1);
|
||||
}
|
||||
}
|
||||
flag = tryChoiceRun (sys, run);
|
||||
}
|
||||
return flag;
|
||||
}
|
||||
|
||||
/*
|
||||
* POR8
|
||||
*
|
||||
* POR6, but tries to continue on the current run.
|
||||
*/
|
||||
|
||||
__inline__ int
|
||||
traversePOR8 (const System sys)
|
||||
{
|
||||
Roledef rd;
|
||||
int flag = 0;
|
||||
int run;
|
||||
int i;
|
||||
int last;
|
||||
|
||||
/* Try all events (implicitly we only handle enabled ones) left-to-right.
|
||||
* If one was chosen, flag is set, and the loop aborts. */
|
||||
/* However, try to continue on the last chosen run first */
|
||||
|
||||
last = lastActiveRun (sys);
|
||||
flag = tryChoiceRun (sys, last);
|
||||
for (run = 0; run < sys->maxruns && !flag; run++)
|
||||
{
|
||||
if (run != last)
|
||||
flag = tryChoiceRun (sys, run);
|
||||
}
|
||||
return flag;
|
||||
}
|
||||
|
||||
|
||||
//! Check for the properties that have lasting effects throughout the trace.
|
||||
/**
|
||||
* Currently, only functions for secrecy.
|
||||
*/
|
||||
|
||||
int
|
||||
propertyCheck (const System sys)
|
||||
|
||||
Loading…
Reference in New Issue
Block a user