From 7fbd43986ff93960cc6d4464ef5c18f2b5f4ce4f Mon Sep 17 00:00:00 2001 From: ccremers Date: Tue, 10 Aug 2004 15:02:37 +0000 Subject: [PATCH] Preparations for Arachne. - roleInstanceDestroy is very much needed. - fixed bug in maxruns maintenance for incRuns. - Arachne does not use run knowledge. --- src/main.c | 3 +++ src/system.c | 64 +++++++++++++++++++++++++++++++++++++++++++++++++--- src/system.h | 6 +++++ 3 files changed, 70 insertions(+), 3 deletions(-) diff --git a/src/main.c b/src/main.c index 303c38f..d40d702 100644 --- a/src/main.c +++ b/src/main.c @@ -329,6 +329,8 @@ main (int argc, char **argv) */ sys = systemInit (); + /* select default engine */ + sys->engine = POR_ENGINE; /* init compiler for this system */ compilerInit (sys); @@ -791,6 +793,7 @@ MC_incRuns (const System sys) runs++; } while (flag && runs <= maxruns); + sys->maxruns = maxruns; } //! Analyse the model by incremental trace lengths. diff --git a/src/system.c b/src/system.c index 4a2078c..0d84373 100644 --- a/src/system.c +++ b/src/system.c @@ -191,8 +191,10 @@ systemDone (const System sys) memFree (sys->traceNode, s * sizeof (states_t)); /* clear roledefs */ - for (run = 0; run < sys->maxruns; run++) - roledefDestroy (runPointerGet (sys, run)); + while (sys->maxruns > 0) + { + roleInstanceDestroy (sys); + } /* clear substructures */ termlistDestroy (sys->secrets); @@ -479,6 +481,7 @@ roleInstance (const System sys, const Protocol protocol, const Role role, Termlist scanfrom, scanto; Termlist fromlist = NULL; Termlist tolist = NULL; + Termlist artefacts = NULL; Term extterm = NULL; Term newvar; @@ -503,6 +506,7 @@ roleInstance (const System sys, const Protocol protocol, const Role role, /* There is a TYPE constant in the parameter list. * Generate a new local variable for this run, with this type */ newvar = makeTermType (VARIABLE, scanfrom->term->left.symb, rid); + artefacts = termlistAdd (artefacts, newvar); sys->variables = termlistAdd (sys->variables, newvar); newvar->stype = termlistAdd (NULL, scanto->term); tolist = termlistAdd (tolist, newvar); @@ -518,6 +522,7 @@ roleInstance (const System sys, const Protocol protocol, const Role role, * this will do for now. I.e. occurring * first in a read will do */ extterm = makeTermTuple (newvar, extterm); + artefacts = termlistAdd (artefacts, extterm); } } else @@ -565,6 +570,7 @@ roleInstance (const System sys, const Protocol protocol, const Role role, if (realTermLeaf (t)) { Term newt = makeTermType (t->type, t->left.symb, rid); + artefacts = termlistAdd (artefacts, newt); if (realTermVariable (newt)) { sys->variables = termlistAdd (sys->variables, newt); @@ -579,7 +585,14 @@ roleInstance (const System sys, const Protocol protocol, const Role role, /* TODO this is not what we want yet, also local knowledge. The local * knowledge (list?) also needs to be substituted on invocation. */ - runs[rid].know = knowledgeDuplicate (sys->know); + if (sys->engine == ARACHNE_ENGINE) + { + runs[rid].know = NULL; + } + else + { + runs[rid].know = knowledgeDuplicate (sys->know); + } /* now adjust the local run copy */ @@ -594,6 +607,7 @@ roleInstance (const System sys, const Protocol protocol, const Role role, } termlistDelete (fromlist); runs[rid].locals = tolist; + runs[rid].artefacts = artefacts; /* Determine symmetric run */ runs[rid].prevSymmRun = staticRunSymmetry (sys, rid); // symmetry reduction static analysis @@ -603,6 +617,50 @@ roleInstance (const System sys, const Protocol protocol, const Role role, } +//! Destroy roleInstance +/** + * Destroys the run with the highest index number + */ +void +roleInstanceDestroy (const System sys) +{ + int runid; + + runid = sys->maxruns - 1; + if (runid >= 0) + { + struct run myrun; + Termlist artefacts; + + myrun = sys->runs[runid]; + + // Destroy roledef + roledefDestroy (myrun.start); + // Destroy artefacts + termlistDelete (myrun.artefacts); + termlistDelete (myrun.locals); + termlistDelete (myrun.agents); + /* + * Arachne does real-time reduction of memory, POR does not + * Artefact removal can only be done if knowledge sets are empty, as with Arachne + */ + if (sys->engine == ARACHNE_ENGINE) + { + // Remove artefacts + artefacts = myrun.artefacts; + while (artefacts != NULL) + { + memFree(artefacts->term, sizeof (struct term)); + artefacts = artefacts->next; + } + } + // Destroy run struct allocation in array using realloc + sys->runs = (Run) memRealloc (sys->runs, sizeof (struct run) * (runid)); + // Reduce run count + sys->maxruns = runid; + } +} + //! Initialise the second system phase. /** * Allocates memory for traces. diff --git a/src/system.h b/src/system.h index 97a3935..791b5cb 100644 --- a/src/system.h +++ b/src/system.h @@ -15,6 +15,9 @@ enum outputs { EMPTY, ATTACK, STATESPACE, SCENARIOS, SUMMARY }; +enum engines +{ POR_ENGINE, ARACHNE_ENGINE }; + //! Protocol definition. struct protocol { @@ -44,6 +47,7 @@ struct run Roledef start; //!< Head of the run definition. Knowledge know; //!< Current knowledge of the run. Termlist locals; //!< Locals of the run. + Termlist artefacts; //!< Stuff created especially for this run. int prevSymmRun; //!< Used for symmetry reduction. Either -1, or the previous run with the same role def and at least a single parameter. int firstNonAgentRead; //!< Used for symmetry reductions for equal agents runs; -1 if there is no candidate. int firstReal; //!< 1 if a choose was inserted, otherwise 0 @@ -97,6 +101,7 @@ struct tracebuf //! The main state structure. struct system { + int engine; //!< Engine type (POR_ENGINE,ARACHNE_ENGINE) int step; //!< Step in trace during exploration. Can be managed globally Knowledge know; //!< Knowledge in currect step of system. struct parameters *parameters; // misc @@ -205,6 +210,7 @@ Term agentOfRunRole (const System sys, const int run, const Term role); Term agentOfRun (const System sys, const int run); void roleInstance (const System sys, const Protocol protocol, const Role role, const Termlist tolist); +void roleInstanceDestroy (const System sys); void systemStart (const System sys); void indentActivate (); void indentSet (int i);