diff --git a/src/roles.c b/src/roles.c new file mode 100644 index 0000000..b2a9ea4 --- /dev/null +++ b/src/roles.c @@ -0,0 +1,239 @@ +/** + * @file roles.c + * \brief role related logic. + */ +#include +#include +#include +#include "terms.h" +#include "termlists.h" +#include "knowledge.h" +#include "runs.h" +#include "memory.h" +#include "constraints.h" +#include "debug.h" +#include "output.h" +#include "tracebuf.h" +#include "roles.h" + +extern int globalLatex; // from runs.c + +//! Allocate memory the size of a roledef struct. +Roledef +makeRoledef () +{ + return (Roledef) memAlloc (sizeof (struct roledef)); +} + +//! Print a role event list. +void +roledefPrint (Roledef rd) +{ + if (rd == NULL) + { + printf ("[Empty roledef]\n"); + return; + } + if (rd->type == READ && rd->internal) + { + /* special case: internal read == choose ! */ + printf ("CHOOSE("); + termPrint (rd->message); + printf (")"); + return; + } + if (rd->type == READ) + printf ("READ"); + if (rd->type == SEND) + printf ("SEND"); + if (rd->type == CLAIM) + printf ("CLAIM"); + if (rd->label != NULL) + { + if (globalLatex) + { + printf ("$_{"); + termPrint (rd->label); + printf ("}$"); + } + else + { + printf ("_"); + termPrint (rd->label); + } + } + if (globalLatex) + printf ("$"); + printf ("("); + termPrint (rd->from); + printf (","); + if (rd->type == CLAIM) + printf (" "); + termPrint (rd->to); + printf (", "); + termPrint (rd->message); + printf (" )"); + if (globalLatex) + printf ("$"); +} + +//! Duplicate a single role event node. +/** + *\sa roledefDelete() + */ +Roledef +roledefDuplicate1 (const Roledef rd) +{ + Roledef newrd; + + if (rd == NULL) + return NULL; + newrd = makeRoledef (); + memcpy (newrd, rd, sizeof (struct roledef)); + newrd->next = NULL; + return newrd; +} + +//! Duplicate a role event list. +/** + *\sa roledefDelete() + */ +Roledef +roledefDuplicate (Roledef rd) +{ + Roledef newrd; + + if (rd == NULL) + return NULL; + newrd = roledefDuplicate1 (rd); + newrd->next = roledefDuplicate (rd->next); + return newrd; +} + +//! Delete a role event or event list. +/** + *\sa roledefDuplicate() + */ +void +roledefDelete (Roledef rd) +{ + if (rd == NULL) + return; + roledefDelete (rd->next); + memFree (rd, sizeof (struct roledef)); + return; +} + +//! Destroy a role event or event list. +void +roledefDestroy (Roledef rd) +{ + if (rd == NULL) + return; + roledefDestroy (rd->next); + termDelete (rd->from); + termDelete (rd->to); + termDelete (rd->message); + memFree (rd, sizeof (struct roledef)); + return; +} + +//! Make a new role event with the specified parameters. +/** + *@return A pointer to a new role event with the given parameters. + */ +Roledef +roledefInit (int type, Term label, Term from, Term to, Term msg, Claimlist cl) +{ + Roledef newEvent; + + newEvent = makeRoledef (); + newEvent->internal = 0; + newEvent->type = type; + newEvent->label = label; + newEvent->from = from; + newEvent->to = to; + newEvent->message = msg; + newEvent->forbidden = NULL; // no forbidden stuff + newEvent->knowPhase = -1; // we haven't explored any knowledge yet + newEvent->claiminfo = cl; // only for claims + newEvent->next = NULL; + return newEvent; +} + +//! Add a role event to an existing list, with the given parameters. +/** + *\sa roledefInit() + */ +Roledef +roledefAdd (Roledef rd, int type, Term label, Term from, Term to, Term msg, Claimlist cl) +{ + Roledef scan; + + if (rd == NULL) + return roledefInit (type, label, from, to, msg, cl); + + scan = rd; + while (scan->next != NULL) + scan = scan->next; + scan->next = roledefInit (type, label, from, to, msg, cl); + return rd; +} + +//! Create an empty role structure with a name. +Role +roleCreate (Term name) +{ + Role r; + + r = memAlloc (sizeof (struct role)); + r->nameterm = name; + r->next = NULL; + r->locals = NULL; + r->roledef = NULL; + return r; +} + +//! Print a role. +void +rolePrint (Role r) +{ + Roledef rd; + + if (r == NULL) + return; + + indent (); + printf ("[[Role : "); + termPrint (r->nameterm); + printf ("]]\n"); + locVarPrint (r->locals); + + rd = r->roledef; + while (rd != NULL) + { + roledefPrint (rd); + printf ("\n"); + rd = rd->next; + } +} + +//! Print a list of roles. +void +rolesPrint (Role r) +{ + if (r == NULL) + { + printf ("Empty role."); + } + else + { + while (r != NULL) + { + rolePrint (r); + r = r->next; + } + } +} + + diff --git a/src/roles.h b/src/roles.h new file mode 100644 index 0000000..4295296 --- /dev/null +++ b/src/roles.h @@ -0,0 +1,117 @@ +#ifndef ROLES +#define ROLES + +#include "terms.h" +#include "termmaps.h" +#include "termlists.h" +#include "knowledge.h" +#include "constraints.h" +#include "states.h" + +#define READ 1 +#define SEND 2 +#define CLAIM 3 + +//! The container for the claim info list +struct claimlist +{ + //! The term element for this node. + Term label; + //! The name of the role in which it occurs. + Term rolename; + //! Number of occurrences in system exploration. + states_t count; + //! Number of occurrences that failed. + states_t failed; + int r; //!< role number for mapping + int ev; //!< event index in role + //! Preceding label list + Termlist prec; + //! Next node pointer or NULL for the last element of the function. + struct claimlist *next; +}; + +//! Shorthand for claimlist pointers. +typedef struct claimlist *Claimlist; + +//! Structure for a role event node or list. +/** + *\sa role + */ +struct roledef +{ + //! flag for internal actions. + /** + * Typically, this is true to signify internal reads (e.g. variable choices) + * as opposed to a normal read. + */ + int internal; + //! Type of event. + /** + *\sa READ, SEND, CLAIM + */ + int type; + //! Event label. + Term label; + //! Event sender. + Term from; + //! Event target. + Term to; + //! Event message. + Term message; + //! Pointer to next roledef node. + struct roledef *next; + + /* + * Substructure for reads + */ + //! Illegal injections for this event. + Knowledge forbidden; + //! knowledge transitions counter. + int knowPhase; + + /* + * Substructure for claims + */ + //! Pointer to claim type info + Claimlist claiminfo; + + /* evt runid for synchronisation, but that is implied in the + base array */ +}; + +//! Shorthand for roledef pointer. +typedef struct roledef *Roledef; + +//! Role definition. +/** + *\sa roledef + */ +struct role +{ + //! Name of the role encoded in a term. + Term nameterm; + //! List of role events. + Roledef roledef; + //! Local constants for this role. + Termlist locals; + //! Pointer to next role definition. + struct role *next; +}; + +//! Shorthand for role pointer. +typedef struct role *Role; + +void roledefPrint (Roledef rd); +Roledef roledefDuplicate1 (const Roledef rd); +Roledef roledefDuplicate (Roledef rd); +void roledefDelete (Roledef rd); +void roledefDestroy (Roledef rd); +Roledef roledefInit (int type, Term label, Term from, Term to, Term msg, Claimlist cl); +Roledef roledefAdd (Roledef rd, int type, Term label, Term from, Term to, Term msg, Claimlist cl); +Role roleCreate (Term nameterm); +void rolePrint (Role r); +void rolesPrint (Role r); + +#endif + diff --git a/src/runs.c b/src/runs.c index e73e89f..2029e02 100644 --- a/src/runs.c +++ b/src/runs.c @@ -1,9 +1,6 @@ /** - * @file runs.c - * \brief run related logic. - * - * Originally contained only procedures related to runs, but has grown - * somewhat over time. + * @file system.c + * \brief system related logic. */ #include #include @@ -17,6 +14,7 @@ #include "debug.h" #include "output.h" #include "tracebuf.h" +#include "roles.h" /* from compiler.o */ extern Term TERM_Type; @@ -39,12 +37,7 @@ makeRun () return (Run) memAlloc (sizeof (struct run)); } -//! Allocate memory the size of a roledef struct. -Roledef -makeRoledef () -{ - return (Roledef) memAlloc (sizeof (struct roledef)); -} + //! Initialise a system structure. /** @@ -244,58 +237,6 @@ ensureValidRun (const System sys, int run) } } -//! Print a role event list. -void -roledefPrint (Roledef rd) -{ - if (rd == NULL) - { - printf ("[Empty roledef]\n"); - return; - } - if (rd->type == READ && rd->internal) - { - /* special case: internal read == choose ! */ - printf ("CHOOSE("); - termPrint (rd->message); - printf (")"); - return; - } - if (rd->type == READ) - printf ("READ"); - if (rd->type == SEND) - printf ("SEND"); - if (rd->type == CLAIM) - printf ("CLAIM"); - if (rd->label != NULL) - { - if (globalLatex) - { - printf ("$_{"); - termPrint (rd->label); - printf ("}$"); - } - else - { - printf ("_"); - termPrint (rd->label); - } - } - if (globalLatex) - printf ("$"); - printf ("("); - termPrint (rd->from); - printf (","); - if (rd->type == CLAIM) - printf (" "); - termPrint (rd->to); - printf (", "); - termPrint (rd->message); - printf (" )"); - if (globalLatex) - printf ("$"); -} - //! Print a run. void runPrint (Roledef rd) @@ -368,67 +309,6 @@ agentOfRun (const System sys, const int run) return agentOfRunRole(sys,run,sys->runs[run].role->nameterm); } -//! Duplicate a single role event node. -/** - *\sa roledefDelete() - */ -Roledef -roledefDuplicate1 (const Roledef rd) -{ - Roledef newrd; - - if (rd == NULL) - return NULL; - newrd = makeRoledef (); - memcpy (newrd, rd, sizeof (struct roledef)); - newrd->next = NULL; - return newrd; -} - -//! Duplicate a role event list. -/** - *\sa roledefDelete() - */ -Roledef -roledefDuplicate (Roledef rd) -{ - Roledef newrd; - - if (rd == NULL) - return NULL; - newrd = roledefDuplicate1 (rd); - newrd->next = roledefDuplicate (rd->next); - return newrd; -} - -//! Delete a role event or event list. -/** - *\sa roledefDuplicate() - */ -void -roledefDelete (Roledef rd) -{ - if (rd == NULL) - return; - roledefDelete (rd->next); - memFree (rd, sizeof (struct roledef)); - return; -} - -//! Destroy a role event or event list. -void -roledefDestroy (Roledef rd) -{ - if (rd == NULL) - return; - roledefDestroy (rd->next); - termDelete (rd->from); - termDelete (rd->to); - termDelete (rd->message); - memFree (rd, sizeof (struct roledef)); - return; -} - /** * A new run is created; now we want to know if it depends on any previous run. * This occurs when there is a smaller runid with an identical protocol role, with the @@ -679,48 +559,6 @@ roleInstance (const System sys, const Protocol protocol, const Role role, runs[rid].firstNonAgentRead = firstNonAgentRead (sys, rid); // symmetry reduction type II } -//! Make a new role event with the specified parameters. -/** - *@return A pointer to a new role event with the given parameters. - */ -Roledef -roledefInit (int type, Term label, Term from, Term to, Term msg, Claimlist cl) -{ - Roledef newEvent; - - newEvent = makeRoledef (); - newEvent->internal = 0; - newEvent->type = type; - newEvent->label = label; - newEvent->from = from; - newEvent->to = to; - newEvent->message = msg; - newEvent->forbidden = NULL; // no forbidden stuff - newEvent->knowPhase = -1; // we haven't explored any knowledge yet - newEvent->claiminfo = cl; // only for claims - newEvent->next = NULL; - return newEvent; -} - -//! Add a role event to an existing list, with the given parameters. -/** - *\sa roledefInit() - */ -Roledef -roledefAdd (Roledef rd, int type, Term label, Term from, Term to, Term msg, Claimlist cl) -{ - Roledef scan; - - if (rd == NULL) - return roledefInit (type, label, from, to, msg, cl); - - scan = rd; - while (scan->next != NULL) - scan = scan->next; - scan->next = roledefInit (type, label, from, to, msg, cl); - return rd; -} - //! Initialise the second system phase. /** @@ -813,21 +651,8 @@ protocolCreate (Term name) return p; } -//! Create an empty role structure with a name. -Role -roleCreate (Term name) -{ - Role r; - - r = memAlloc (sizeof (struct role)); - r->nameterm = name; - r->next = NULL; - r->locals = NULL; - r->roledef = NULL; - return r; -} - //! Print all local terms in a term list. +//@todo What is this doing here? This should be in termlists.c! void locVarPrint (Termlist tl) { @@ -884,48 +709,6 @@ protocolsPrint (Protocol p) } } -//! Print a role. -void -rolePrint (Role r) -{ - Roledef rd; - - if (r == NULL) - return; - - indent (); - printf ("[[Role : "); - termPrint (r->nameterm); - printf ("]]\n"); - locVarPrint (r->locals); - - rd = r->roledef; - while (rd != NULL) - { - roledefPrint (rd); - printf ("\n"); - rd = rd->next; - } -} - -//! Print a list of roles. -void -rolesPrint (Role r) -{ - if (r == NULL) - { - printf ("Empty role."); - } - else - { - while (r != NULL) - { - rolePrint (r); - r = r->next; - } - } -} - //! Determine whether there is an untrusted agent. /** *@param sys The system, containing system::untrusted. diff --git a/src/runs.h b/src/runs.h index 4fa3707..cc10b51 100644 --- a/src/runs.h +++ b/src/runs.h @@ -1,5 +1,5 @@ -#ifndef RUNS -#define RUNS +#ifndef SYSTEM +#define SYSTEM #include "terms.h" #include "termmaps.h" @@ -7,104 +7,11 @@ #include "knowledge.h" #include "constraints.h" #include "states.h" - -#define READ 1 -#define SEND 2 -#define CLAIM 3 +#include "roles.h" #define runPointerGet(sys,run) sys->runs[run].index #define runPointerSet(sys,run,newp) sys->runs[run].index = newp -//! The container for the claim info list -struct claimlist -{ - //! The term element for this node. - Term label; - //! The name of the role in which it occurs. - Term rolename; - //! Number of occurrences in system exploration. - states_t count; - //! Number of occurrences that failed. - states_t failed; - int r; //!< role number for mapping - int ev; //!< event index in role - //! Preceding label list - Termlist prec; - //! Next node pointer or NULL for the last element of the function. - struct claimlist *next; -}; - -//! Shorthand for claimlist pointers. -typedef struct claimlist *Claimlist; - -//! Structure for a role event node or list. -/** - *\sa role - */ -struct roledef -{ - //! flag for internal actions. - /** - * Typically, this is true to signify internal reads (e.g. variable choices) - * as opposed to a normal read. - */ - int internal; - //! Type of event. - /** - *\sa READ, SEND, CLAIM - */ - int type; - //! Event label. - Term label; - //! Event sender. - Term from; - //! Event target. - Term to; - //! Event message. - Term message; - //! Pointer to next roledef node. - struct roledef *next; - - /* - * Substructure for reads - */ - //! Illegal injections for this event. - Knowledge forbidden; - //! knowledge transitions counter. - int knowPhase; - - /* - * Substructure for claims - */ - //! Pointer to claim type info - Claimlist claiminfo; - - /* evt runid for synchronisation, but that is implied in the - base array */ -}; - -//! Shorthand for roledef pointer. -typedef struct roledef *Roledef; - -//! Role definition. -/** - *\sa roledef - */ -struct role -{ - //! Name of the role encoded in a term. - Term nameterm; - //! List of role events. - Roledef roledef; - //! Local constants for this role. - Termlist locals; - //! Pointer to next role definition. - struct role *next; -}; - -//! Shorthand for role pointer. -typedef struct role *Role; - //! Protocol definition. struct protocol { @@ -275,31 +182,21 @@ void statesPrintShort (const System sys); void systemDestroy (const System sys); void systemDone (const System sys); void ensureValidRun (const System sys, int run); -void roledefPrint (Roledef rd); void runPrint (Roledef rd); void runsPrint (const System sys); Term agentOfRunRole (const System sys, const int run, const Term role); Term agentOfRun (const System sys, const int run); -Roledef roledefDuplicate1 (const Roledef rd); -Roledef roledefDuplicate (Roledef rd); -void roledefDelete (Roledef rd); -void roledefDestroy (Roledef rd); void roleInstance (const System sys, const Protocol protocol, const Role role, const Termlist tolist); -Roledef roledefInit (int type, Term label, Term from, Term to, Term msg, Claimlist cl); -Roledef roledefAdd (Roledef rd, int type, Term label, Term from, Term to, Term msg, Claimlist cl); void systemStart (const System sys); void indentActivate (); void indentSet (int i); void indent (); Protocol protocolCreate (Term nameterm); -Role roleCreate (Term nameterm); void locVarPrint (Termlist tl); void protocolPrint (Protocol p); void protocolsPrint (Protocol p); -void rolePrint (Role r); -void rolesPrint (Role r); int untrustedAgent (const System sys, Termlist agents); int getMaxTraceLength (const System sys); void agentsOfRunPrint (const System sys, const int run);