andr3/scyther
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

- Improved handling of pruning in explorify. Now, when pruning is done

Browse Source 
in explorify, the signal is passed back, and match_basic etc. will
  signal that the event was not enabled.
This commit is contained in:
ccremers 2004-07-19 12:03:29 +00:00
parent b412e56c7b
commit 03c19a4774
2 changed files with 48 additions and 36 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

44
src/match_basic.c
View File

@ -30,13 +30,11 @@ struct fvpass
int (*proceed) (System, int);
};
/*
* fix variables in a message, and check whether it can be accepted.
*
//! Fix variables in a message, and check whether it can be accepted.
/**
* fp.sys is only accessed for the matching type.
*@returns 1 (true) if there exists a message that can be accepted, fvpass returns 1 on it.
*/
int
fixVariablelist (const struct fvpass fp, const Knowledge know,
Termlist varlist, const Term message)
@ -89,11 +87,15 @@ fixVariablelist (const struct fvpass fp, const Knowledge know,
}
else
{
/* signal that it was enabled, now we omit the pruning */
flag = 1;
}
}
else
flag = 0;
{
/* not enabled */
flag = 0;
}
/* restore state */
if (copied)
@ -163,16 +165,15 @@ fixVariablelist (const struct fvpass fp, const Knowledge know,
#define enabled_basic(sys,know,newterm) !inKnowledge(know,newterm)
/*
* matchRead
*
* try to execute a read event. It must be able to be construct it from the
//! Try to execute a read event.
/**
* Try to execute a read event. It must be able to be construct it from the
* current intruder knowledge (Inject), but not from the forbidden knowledge
* set, which we tried earlier.
*
* returns 0 if it is not enabled, 1 if it was enabled (and routes explored)
*@returns 0 if it is not enabled, 1 if it was enabled (and routes explored)
*\sa explorify()
*/
int
matchRead_basic (const System sys, const int run,
int (*proceed) (System, int))
@ -194,7 +195,9 @@ matchRead_basic (const System sys, const int run,
fp.roledef->forbidden == NULL ||
enabled_basic (fp.sys, fp.roledef->forbidden, newterm))
{
/* it is enabled, i.e. not forbidden */
/* it is possibly enabled, i.e. not forbidden */
int enabled;
oldknow = fp.sys->know;
fp.sys->know = know;
#ifdef DEBUG
@ -203,10 +206,10 @@ matchRead_basic (const System sys, const int run,
printf ("+");
}
#endif
fp.proceed (fp.sys, fp.run);
enabled = fp.proceed (fp.sys, fp.run); // flag determines the enabled status now
fp.sys->know = oldknow;
termDelete (newterm);
return 1;
return enabled;
}
else
{
@ -252,13 +255,12 @@ matchRead_basic (const System sys, const int run,
return flag;
}
/*
* block
*
//! Skip an event
/**
* Skips over an event. Because the intruder knowledge is incremental, we can
* just overwrite the old value of forbidden.
*@returns 1
*/
int
block_basic (const System sys, const int run)
{
@ -273,6 +275,10 @@ block_basic (const System sys, const int run)
return 1;
}
//! Execute a send
/**
*@returns 1
*/
int
send_basic (const System sys, const int run)
{

40
src/modelchecker.c
View File

@ -237,8 +237,16 @@ Roledef removeIrrelevant (const System sys, const int run, Roledef rd)
}
//! Explores the system state given by the next step of a run.
/**
* grandiose naming scheme (c) sjors dubya.
/** Grandiose naming scheme (c) sjors dubya.
*
* After an event was instantiated, this function is called to explore the
* remainder of the system.
*
* Note that some additional pruning is done, so this function
* also determines the enabledness of the event that was just instantiated.
*
*@returns 1 (true) if the event was enabled.
*\sa match_basic(),executeTry()
*/
int
@ -255,8 +263,7 @@ explorify (const System sys, const int run)
if (rd == NULL)
{
fprintf (stderr, "ERROR: trying to progress completed run!\n");
exit (1);
error ("Trying to progress completed run!\n");
}
flag = 0;
@ -479,7 +486,7 @@ explorify (const System sys, const int run)
{
roleCap->next = roleCapPart;
}
return flag;
return 1; // The event was indeed enabled (irrespective of traverse!)
}
int
@ -531,8 +538,7 @@ nonReads (const System sys)
rd = runPointerGet (sys, run);
if (nonRead (sys, rd))
{
executeTry (sys, run);
return 1;
return executeTry (sys, run);
}
}
return 0;
@ -1061,8 +1067,7 @@ traversePOR4 (const System sys)
{
case CLAIM:
case SEND:
executeTry (sys, run);
flag = 1;
flag = executeTry (sys, run);
break;
case READ:
@ -1188,8 +1193,7 @@ traversePOR5 (const System sys)
{
case CLAIM:
case SEND:
executeTry (sys, run);
flag = 1;
flag = executeTry (sys, run);
break;
case READ:
@ -1274,8 +1278,7 @@ traversePOR6 (const System sys)
{
case CLAIM:
case SEND:
executeTry (sys, run);
flag = 1;
flag = executeTry (sys, run);
break;
case READ:
@ -1359,8 +1362,7 @@ traversePOR7 (const System sys)
{
case CLAIM:
case SEND:
executeTry (sys, run);
flag = 1;
flag = executeTry (sys, run);
break;
case READ:
@ -1414,8 +1416,7 @@ traversePOR7 (const System sys)
{
case CLAIM:
case SEND:
executeTry (sys, run);
flag = 1;
flag = executeTry (sys, run);
break;
case READ:
@ -1683,6 +1684,11 @@ violateClaim (const System sys, int length, int claimev, Termlist reqt)
return flag;
}
//! Try to execute the next event in a run.
/**
* One of the core functions of the system.
*@returns 0 (false) if the event was not enabled. 1 (true) if there was an enabled instantiation of this event.
*/
int
executeTry (const System sys, int run)
{