From 03c19a4774fe2f1fbb9ed3ca4d8f999c90ac7ecc Mon Sep 17 00:00:00 2001 From: ccremers Date: Mon, 19 Jul 2004 12:03:29 +0000 Subject: [PATCH] - Improved handling of pruning in explorify. Now, when pruning is done in explorify, the signal is passed back, and match_basic etc. will signal that the event was not enabled. --- src/match_basic.c | 44 +++++++++++++++++++++++++------------------- src/modelchecker.c | 40 +++++++++++++++++++++++----------------- 2 files changed, 48 insertions(+), 36 deletions(-) diff --git a/src/match_basic.c b/src/match_basic.c index bcb3c70..e72d5bb 100644 --- a/src/match_basic.c +++ b/src/match_basic.c @@ -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) { diff --git a/src/modelchecker.c b/src/modelchecker.c index 6c7102e..f5e8c07 100644 --- a/src/modelchecker.c +++ b/src/modelchecker.c @@ -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) {