- Added preliminary labellist support to the system.
This commit is contained in:
parent
275743c1a3
commit
542044e36f
14
src/claim.c
14
src/claim.c
@ -15,8 +15,11 @@
|
|||||||
|
|
||||||
/*
|
/*
|
||||||
* Validity checks for claims
|
* Validity checks for claims
|
||||||
|
*
|
||||||
|
* Note that the first few operate on claims, and that the tests for e.g. the Arachne engine are seperate.
|
||||||
*/
|
*/
|
||||||
|
|
||||||
|
|
||||||
#ifdef OKIDEBUG
|
#ifdef OKIDEBUG
|
||||||
int indac = 0;
|
int indac = 0;
|
||||||
|
|
||||||
@ -440,3 +443,14 @@ check_claim_niagree (const System sys, const int i)
|
|||||||
termmapDelete (g);
|
termmapDelete (g);
|
||||||
return result;
|
return result;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
||||||
|
//! Check arachne agreement claim
|
||||||
|
/**
|
||||||
|
* Per default, occurs in run 0, but for generality we have left the run parameter in.
|
||||||
|
*@returns 1 if the claim is true, 0 if it is not.
|
||||||
|
*/
|
||||||
|
int arachne_claim_agree (const System sys, const int claim_run, const int claim_index)
|
||||||
|
{
|
||||||
|
}
|
||||||
|
|
||||||
|
@ -20,6 +20,19 @@
|
|||||||
static System sys;
|
static System sys;
|
||||||
static Tac tac_root;
|
static Tac tac_root;
|
||||||
|
|
||||||
|
/*
|
||||||
|
* Structure to store label information
|
||||||
|
*/
|
||||||
|
struct labelinfo
|
||||||
|
{
|
||||||
|
Term label;
|
||||||
|
Term protocol;
|
||||||
|
Term sendrole;
|
||||||
|
Term readrole;
|
||||||
|
};
|
||||||
|
|
||||||
|
typedef struct labelinfo Labelinfo;
|
||||||
|
|
||||||
/*
|
/*
|
||||||
* Declaration from system.c
|
* Declaration from system.c
|
||||||
*/
|
*/
|
||||||
@ -898,6 +911,8 @@ compute_role_variables (const System sys, Protocol p, Role r)
|
|||||||
* a mapping from all events to event/claim labels.
|
* a mapping from all events to event/claim labels.
|
||||||
* A second table is used to compute the precedence order, and
|
* A second table is used to compute the precedence order, and
|
||||||
* Warshall's algorithm is used to compute the transitive closure.
|
* Warshall's algorithm is used to compute the transitive closure.
|
||||||
|
* Then, for each claim, the in the preceding labels occurring roles are stored,
|
||||||
|
* which is useful later.
|
||||||
*@returns For each claim in the claim list, a preceding label set is defined.
|
*@returns For each claim in the claim list, a preceding label set is defined.
|
||||||
*/
|
*/
|
||||||
void
|
void
|
||||||
|
25
src/label.c
Normal file
25
src/label.c
Normal file
@ -0,0 +1,25 @@
|
|||||||
|
/**
|
||||||
|
* Label info
|
||||||
|
*/
|
||||||
|
|
||||||
|
#include "memory.h"
|
||||||
|
#include "term.h"
|
||||||
|
#include "label.h"
|
||||||
|
|
||||||
|
Labelinfo label_create (const Term label, const Term protocol)
|
||||||
|
{
|
||||||
|
Labelinfo li;
|
||||||
|
|
||||||
|
li = (Labelinfo) memAlloc (sizeof (struct labelinfo));
|
||||||
|
li->label = label;
|
||||||
|
li->protocol = protocol;
|
||||||
|
li->sendrole = NULL;
|
||||||
|
li->readrole = NULL;
|
||||||
|
return li;
|
||||||
|
}
|
||||||
|
|
||||||
|
void label_destroy (Labelinfo linfo)
|
||||||
|
{
|
||||||
|
memFree (linfo, sizeof (struct labelinfo));
|
||||||
|
}
|
||||||
|
|
22
src/label.h
Normal file
22
src/label.h
Normal file
@ -0,0 +1,22 @@
|
|||||||
|
#ifndef LABEL
|
||||||
|
#define LABEL
|
||||||
|
|
||||||
|
#include "term.h"
|
||||||
|
|
||||||
|
/*
|
||||||
|
* Structure to store label information
|
||||||
|
*/
|
||||||
|
struct labelinfo
|
||||||
|
{
|
||||||
|
Term label;
|
||||||
|
Term protocol;
|
||||||
|
Term sendrole;
|
||||||
|
Term readrole;
|
||||||
|
};
|
||||||
|
|
||||||
|
typedef struct labelinfo* Labelinfo;
|
||||||
|
|
||||||
|
Labelinfo label_create (const Term label, const Term protocol);
|
||||||
|
void label_destroy (Labelinfo linfo);
|
||||||
|
|
||||||
|
#endif
|
@ -97,6 +97,7 @@ systemInit ()
|
|||||||
sys->rolecount = 0;
|
sys->rolecount = 0;
|
||||||
sys->roleeventmax = 0;
|
sys->roleeventmax = 0;
|
||||||
sys->claimlist = NULL;
|
sys->claimlist = NULL;
|
||||||
|
sys->labellist = NULL;
|
||||||
|
|
||||||
/* matching CLP */
|
/* matching CLP */
|
||||||
sys->constraints = NULL; // no initial constraints
|
sys->constraints = NULL; // no initial constraints
|
||||||
|
@ -176,6 +176,7 @@ struct system
|
|||||||
int roleeventmax; //!< Maximum number of events in a single role
|
int roleeventmax; //!< Maximum number of events in a single role
|
||||||
int lastChooseRun; //!< Last run with a choose event
|
int lastChooseRun; //!< Last run with a choose event
|
||||||
Claimlist claimlist; //!< List of claims in the system, with occurrence counts
|
Claimlist claimlist; //!< List of claims in the system, with occurrence counts
|
||||||
|
List labellist; //!< List of labelinfo stuff
|
||||||
|
|
||||||
/* constructed trace pointers, static */
|
/* constructed trace pointers, static */
|
||||||
Roledef *traceEvent; //!< Trace roledefs: MaxRuns * maxRoledef
|
Roledef *traceEvent; //!< Trace roledefs: MaxRuns * maxRoledef
|
||||||
|
Loading…
Reference in New Issue
Block a user