- Claim iteration works nicely now.
This commit is contained in:
parent
68b2aa16e7
commit
53cb869426
@ -14,6 +14,8 @@
|
|||||||
#include "states.h"
|
#include "states.h"
|
||||||
#include "mgu.h"
|
#include "mgu.h"
|
||||||
#include "arachne.h"
|
#include "arachne.h"
|
||||||
|
#include "error.h"
|
||||||
|
#include "claim.h"
|
||||||
|
|
||||||
static System sys;
|
static System sys;
|
||||||
Protocol INTRUDER; // Pointers, to be set by the Init
|
Protocol INTRUDER; // Pointers, to be set by the Init
|
||||||
@ -777,16 +779,16 @@ iterate ()
|
|||||||
int
|
int
|
||||||
arachne ()
|
arachne ()
|
||||||
{
|
{
|
||||||
|
Claimlist cl;
|
||||||
/*
|
/*
|
||||||
* set up claim role(s)
|
* set up claim role(s)
|
||||||
*/
|
*/
|
||||||
|
|
||||||
if (sys->maxruns > 0)
|
if (sys->maxruns > 0)
|
||||||
{
|
{
|
||||||
sys->runs[0].length = roledef_length (sys->runs[0].start);
|
error ("Something is wrong, number of runs >0.");
|
||||||
}
|
}
|
||||||
|
|
||||||
#ifdef DEBUG
|
|
||||||
int print_send (Protocol p, Role r, Roledef rd, int index)
|
int print_send (Protocol p, Role r, Roledef rd, int index)
|
||||||
{
|
{
|
||||||
eprintf ("IRS: ");
|
eprintf ("IRS: ");
|
||||||
@ -800,17 +802,48 @@ arachne ()
|
|||||||
|
|
||||||
iterate_role_sends (print_send);
|
iterate_role_sends (print_send);
|
||||||
|
|
||||||
|
indentDepth = 0;
|
||||||
|
cl = sys->claimlist;
|
||||||
|
while (cl != NULL)
|
||||||
|
{
|
||||||
|
Protocol p;
|
||||||
|
Role r;
|
||||||
|
|
||||||
explanation = NULL;
|
explanation = NULL;
|
||||||
e_run = INVALID;
|
e_run = INVALID;
|
||||||
e_term1 = NULL;
|
e_term1 = NULL;
|
||||||
e_term2 = NULL;
|
e_term2 = NULL;
|
||||||
e_term3 = NULL;
|
e_term3 = NULL;
|
||||||
#endif
|
|
||||||
indentDepth = 0;
|
p = (Protocol) cl->protocol;
|
||||||
|
r = (Role) cl->role;
|
||||||
|
indentPrint ();
|
||||||
|
eprintf ("Testing Claim ");
|
||||||
|
termPrint (cl->type);
|
||||||
|
eprintf (" in protocol ");
|
||||||
|
termPrint (p->nameterm);
|
||||||
|
eprintf (", role ");
|
||||||
|
termPrint (r->nameterm);
|
||||||
|
eprintf (" at index %i.\n", cl->ev);
|
||||||
|
|
||||||
|
indentDepth++;
|
||||||
|
|
||||||
|
roleInstance (sys, p, r, NULL);
|
||||||
|
sys->runs[0].length = cl->ev+1;
|
||||||
|
#ifdef DEBUG
|
||||||
printSemiState ();
|
printSemiState ();
|
||||||
|
#endif
|
||||||
|
|
||||||
/*
|
/*
|
||||||
* iterate
|
* iterate
|
||||||
*/
|
*/
|
||||||
iterate ();
|
iterate ();
|
||||||
|
|
||||||
|
//! Destroy
|
||||||
|
roleInstanceDestroy (sys);
|
||||||
|
|
||||||
|
// next
|
||||||
|
indentDepth--;
|
||||||
|
cl = cl->next;
|
||||||
|
}
|
||||||
}
|
}
|
||||||
|
@ -464,7 +464,9 @@ commEvent (int event, Tac tc)
|
|||||||
cl = memAlloc (sizeof (struct claimlist));
|
cl = memAlloc (sizeof (struct claimlist));
|
||||||
cl->type = claim;
|
cl->type = claim;
|
||||||
cl->label = label;
|
cl->label = label;
|
||||||
|
cl->protocol = thisProtocol;
|
||||||
cl->rolename = fromrole;
|
cl->rolename = fromrole;
|
||||||
|
cl->role = thisRole;
|
||||||
cl->count = 0;
|
cl->count = 0;
|
||||||
cl->failed = 0;
|
cl->failed = 0;
|
||||||
cl->prec = NULL;
|
cl->prec = NULL;
|
||||||
|
@ -18,8 +18,12 @@ struct claimlist
|
|||||||
Term type;
|
Term type;
|
||||||
//! The term element for this node.
|
//! The term element for this node.
|
||||||
Term label;
|
Term label;
|
||||||
|
//! The pointer to the protocol (not defined yet?)
|
||||||
|
void *protocol;
|
||||||
//! The name of the role in which it occurs.
|
//! The name of the role in which it occurs.
|
||||||
Term rolename;
|
Term rolename;
|
||||||
|
//! The pointer to the role structure
|
||||||
|
void *role;
|
||||||
//! Number of occurrences in system exploration.
|
//! Number of occurrences in system exploration.
|
||||||
states_t count;
|
states_t count;
|
||||||
//! Number of occurrences that failed.
|
//! Number of occurrences that failed.
|
||||||
|
Loading…
Reference in New Issue
Block a user