diff --git a/src/compiler.c b/src/compiler.c index 98d4296..f9ab936 100644 --- a/src/compiler.c +++ b/src/compiler.c @@ -939,12 +939,17 @@ claimAddAll (const System sys, const Protocol protocol, const Role role) } } - addSecrecyList (role->declaredconsts); - addSecrecyList (role->declaredvars); + if (!isHelperProtocol (protocol)) + { + addSecrecyList (role->declaredconsts); + addSecrecyList (role->declaredvars); - /* full non-injective agreement and ni-synch */ - claimCreate (sys, protocol, role, CLAIM_Niagree, NULL, NULL, -1); - claimCreate (sys, protocol, role, CLAIM_Nisynch, NULL, NULL, -1); + /* full non-injective agreement and ni-synch */ + claimCreate (sys, protocol, role, CLAIM_Alive, NULL, NULL, -1); + claimCreate (sys, protocol, role, CLAIM_Weakagree, NULL, NULL, -1); + claimCreate (sys, protocol, role, CLAIM_Niagree, NULL, NULL, -1); + claimCreate (sys, protocol, role, CLAIM_Nisynch, NULL, NULL, -1); + } } //! Compile a role @@ -1028,8 +1033,11 @@ roleCompile (Term nameterm, Tac tc) if (switches.addreachableclaim) { - claimCreate (sys, thisProtocol, thisRole, CLAIM_Reachable, NULL, NULL, - -1); + if (!isHelperProtocol (thisProtocol)) + { + claimCreate (sys, thisProtocol, thisRole, CLAIM_Reachable, NULL, + NULL, -1); + } } if (switches.addallclaims) { diff --git a/src/system.c b/src/system.c index c5624a3..e343a0e 100644 --- a/src/system.c +++ b/src/system.c @@ -1291,9 +1291,12 @@ selfSession (const System sys, const int run) int selfResponder (const System sys, const int run) { - if (sys->runs[run].role->initiator) + if (!isHelperProtocol (sys->runs[run].protocol)) { - return false; + if (sys->runs[run].role->initiator) + { + return false; + } } else { @@ -1328,9 +1331,12 @@ selfResponders (const System sys) int selfInitiator (const System sys, const int run) { - if (sys->runs[run].role->initiator) + if (!isHelperProtocol (sys->runs[run].protocol)) { - return selfSession (sys, run); + if (sys->runs[run].role->initiator) + { + return selfSession (sys, run); + } } else { @@ -1357,3 +1363,24 @@ selfInitiators (const System sys) } return count; } + +//! Check a protocol for being a helper protocol. +/** + * Special helper protocols start with an '@' conform the usage in Gijs + * Hollestelle's work. + */ +int +isHelperProtocol (Protocol p) +{ + if (p != NULL) + { + if (p->nameterm != NULL) + { + if (TermSymb (p->nameterm)->text[0] == '@') + { + return true; + } + } + } + return false; +} diff --git a/src/system.h b/src/system.h index 0914651..c57b2a4 100644 --- a/src/system.h +++ b/src/system.h @@ -208,6 +208,7 @@ int selfResponders (const System sys); int selfInitiator (const System sys, const int run); int selfInitiators (const System sys); int enoughAttacks (const System sys); +int isHelperProtocol (Protocol p); //! Equality for run structure naming