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

Reindenting code.

Browse Source
This commit is contained in:
Cas Cremers 2011-01-25 17:33:12 +01:00
parent 68409e14ad
commit fea2bcf477
4 changed files with 22 additions and 17 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

23
src/claim.c
View File

@ -793,10 +793,10 @@ arachne_claim_commit (const System sys, const int claim_run,
Termlist params_a;
rd_claim = roledef_shift (sys->runs[claim_run].start, claim_index);
params_a = tuple_to_termlist(rd_claim->message);
params_a = tuple_to_termlist (rd_claim->message);
actor_a = rd_claim->from;
actor_b = params_a->term;
partner_role = termLeft(rd_claim->claiminfo->parameter);
partner_role = termLeft (rd_claim->claiminfo->parameter);
/*
* Iterate over all preceding events (include claim run for consistency with formal definition)
@ -826,24 +826,27 @@ arachne_claim_commit (const System sys, const int claim_run,
{
Termlist params_b;
params_b = tuple_to_termlist(rd->message);
params_b = tuple_to_termlist (rd->message);
// check agent requirements
if (isTermEqual(rd->from,actor_b) && isTermEqual(params_b->term,actor_a))
if (isTermEqual (rd->from, actor_b)
&& isTermEqual (params_b->term, actor_a))
{
// check role (also same protocol)
if (isTermEqual(partner_role,rd->claiminfo->rolename))
if (isTermEqual
(partner_role, rd->claiminfo->rolename))
{
// check parameters
if (isTermlistEqual (params_a->next,params_b->next))
if (isTermlistEqual
(params_a->next, params_b->next))
{
// Claim holds
termlistDelete(params_b);
termlistDelete(params_a);
termlistDelete (params_b);
termlistDelete (params_a);
return true;
}
}
}
termlistDelete(params_b);
termlistDelete (params_b);
}
}
}
@ -851,7 +854,7 @@ arachne_claim_commit (const System sys, const int claim_run,
rd = rd->next;
}
}
termlistDelete(params_a);
termlistDelete (params_a);
return false;
}

7
src/dotout.c
View File

@ -621,14 +621,15 @@ isEventIgnored (const System sys, int run, int ev)
if (rd->type == CLAIM)
{
// If we are doing a reachability analysis, show all
if (isTermEqual(sys->current_claim->type, CLAIM_Reachable))
if (isTermEqual (sys->current_claim->type, CLAIM_Reachable))
{
return false;
}
// If the claim type is commit, we also show running claims
if (isTermEqual(sys->current_claim->type, CLAIM_Commit) || isTermEqual(sys->current_claim->type, CLAIM_Reachable))
if (isTermEqual (sys->current_claim->type, CLAIM_Commit)
|| isTermEqual (sys->current_claim->type, CLAIM_Reachable))
{
if (isTermEqual(rd->claiminfo->type, CLAIM_Running))
if (isTermEqual (rd->claiminfo->type, CLAIM_Running))
{
return false;
}

7
src/termlist.c
View File

@ -926,12 +926,13 @@ tuple_to_termlist (Term t)
}
//! Get the leftmost term of a tuple (e.g. a non-tuple)
Term termLeft(Term t)
Term
termLeft (Term t)
{
t = deVar(t);
t = deVar (t);
if (realTermTuple (t))
{
return termLeft(TermOp1 (t));
return termLeft (TermOp1 (t));
}
return t;
}

2
src/termlist.h
View File

@ -77,7 +77,7 @@ int termlistOrder (Termlist tl1, Termlist tl2);
int termlist_iterate (Termlist tl, int (*func) ());
Term termlist_to_tuple (Termlist tl);
Termlist tuple_to_termlist (Term t);
Term termLeft(Term t);
Term termLeft (Term t);
Termlist termlistMinusTermlist (const Termlist tlbig, const Termlist tlsmall);
#define TERMLISTADD(l,t) l = termlistAdd (l,t)