andr3/scyther
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Weakagree and Alive claims now also allow for a role parameter + BUGFIX.

Browse Source 
Previously, weak agreement and aliveness claims would enforce a requirement for all agents in the range
of the rho of the claim run.

For some three-party protocols this was stronger than needed. We now allow an
optional role name parameter for these claims; if such a parameter is used, the claim
is only evaluated for the agents performing that role.

En passant fixed a potential bug: aliveness and weak agreement require a run for each
agent, but previously we didn't check if these were helper protocols. Clearly they
should not be.
This commit is contained in:
Cas Cremers 2013-05-23 16:38:44 +02:00
parent 9e13d07b6e
commit 5c2eded8f9
2 changed files with 75 additions and 43 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

104
src/claim.c
View File

@ -727,6 +727,29 @@ arachne_claim_nisynch (const System sys, const int claim_run,
return arachne_claim_authentications (sys, claim_run, claim_index, 1);
}
//! Test weak agreement with a single agent
int
has_weakagree_agent (const System sys, const int claim_run, const Term agent)
{
int run;
for (run = 0; run < sys->maxruns; run++)
{
if (!isHelperProtocol (sys->runs[run].protocol))
{
if (isTermEqual (agent, agentOfRun (sys, run)))
{
if (isTermlistSetEqual
(sys->runs[run].rho, sys->runs[claim_run].rho))
{
return true;
}
}
}
}
return false;
}
//! Test weak agreement
int
arachne_claim_weakagree (const System sys, const int claim_run,
@ -736,6 +759,9 @@ arachne_claim_weakagree (const System sys, const int claim_run,
* Runs for each supposed agent, with matching *sets* for rho.
* (so we can skip the actor)
*/
if (sys->current_claim->parameter == NULL)
{
// No parameter: need agents for all roles
Termlist tl;
for (tl = sys->runs[claim_run].rho; tl != NULL; tl = tl->next)
@ -743,35 +769,22 @@ arachne_claim_weakagree (const System sys, const int claim_run,
Term agent;
agent = tl->term;
if (!isTermEqual (agent, agentOfRun (sys, claim_run)))
{
int run;
int agentokay;
agentokay = false;
for (run = 0; run < sys->maxruns; run++)
{
if (run != claim_run)
{
if (isTermEqual (agent, agentOfRun (sys, run)))
{
if (isTermlistSetEqual
(sys->runs[run].rho, sys->runs[claim_run].rho))
{
agentokay = true;
break;
}
}
}
}
if (!agentokay)
if (!has_weakagree_agent (sys, claim_run, agent))
{
return false;
}
}
}
return true;
}
else
{
// Parameter for role
Term agent;
agent = agentOfRunRole (sys, claim_run, sys->current_claim->parameter);
return has_weakagree_agent (sys, claim_run, agent);
}
}
//! Test commit(X) => running(X)
/**
@ -861,6 +874,25 @@ arachne_claim_commit (const System sys, const int claim_run,
return false;
}
//! Test aliveness of agent
int
is_agent_alive (const System sys, const Term agent)
{
int run;
for (run = 0; run < sys->maxruns; run++)
{
if (!isHelperProtocol (sys->runs[run].protocol))
{
if (isTermEqual (agent, agentOfRun (sys, run)))
{
return true;
}
}
}
return false;
}
//! Test aliveness
int
arachne_claim_alive (const System sys, const int claim_run,
@ -870,29 +902,29 @@ arachne_claim_alive (const System sys, const int claim_run,
* Fairly simple claim: there must exist runs for each agent involved.
* We don't even consider the roles.
*/
if (sys->current_claim->parameter == NULL)
{
// No parameter: check for all roles
Termlist tl;
for (tl = sys->runs[claim_run].rho; tl != NULL; tl = tl->next)
{
int run;
int principalLives;
principalLives = false;
for (run = 0; run < sys->maxruns; run++)
{
if (isTermEqual (tl->term, agentOfRun (sys, run)))
{
principalLives = true;
break;
}
}
if (!principalLives)
if (!is_agent_alive (sys, tl->term))
{
return false;
}
}
return true;
}
else
{
// Parameter: check for agent in that role
Term agent;
agent = agentOfRunRole (sys, claim_run, sys->current_claim->parameter);
return is_agent_alive (sys, agent);
}
}
//! Determine good height for full session
/**

4
src/compiler.c
View File

@ -754,8 +754,8 @@ claimCreate (const System sys, const Protocol protocol, const Role role,
}
checkParameterRange (cl, CLAIM_Secret, 1, -1);
checkParameterRange (cl, CLAIM_SKR, 1, -1);
checkParameterRange (cl, CLAIM_Alive, 0, 0);
checkParameterRange (cl, CLAIM_Weakagree, 0, 0);
checkParameterRange (cl, CLAIM_Alive, 0, 1);
checkParameterRange (cl, CLAIM_Weakagree, 0, 1);
checkParameterRange (cl, CLAIM_Nisynch, 0, 0);
checkParameterRange (cl, CLAIM_Niagree, 0, 0);
checkParameterRange (cl, CLAIM_Reachable, 0, 0);