From 3ddedb6f7f7bd9c932a12364041eb76b21061bc2 Mon Sep 17 00:00:00 2001 From: ccremers Date: Sun, 25 Jul 2004 18:24:50 +0000 Subject: [PATCH] - Totally untested. Otherwise, niagree should work ;) --- src/claim.c | 60 +++++++++++++++++++++++++++++++++++++ src/claim.h | 1 + src/compiler.c | 73 ++++++++++++++++++++++++++++++++++++++++++---- src/modelchecker.c | 21 +++++++++++-- src/termlist.c | 2 +- src/termlist.h | 2 +- 6 files changed, 149 insertions(+), 10 deletions(-) diff --git a/src/claim.c b/src/claim.c index 31bc01f..29fc5f9 100644 --- a/src/claim.c +++ b/src/claim.c @@ -367,3 +367,63 @@ check_claim_nisynch (const System sys, const int i) return result; } +//! Check validity of ni-agree claim at event i. +/** + *@returns 1 iff claim is true. + *@todo This is now just a copy of ni-synch, should be fixed asap. + */ +int +check_claim_niagree (const System sys, const int i) +{ + Roledef rd; + int result; + int rid; + Termmap f,g; + Term label; + Claimlist cl; + Termlist tl; + + rid = sys->traceRun[i]; + rd = sys->traceEvent[i]; + cl = rd->claiminfo; + cl->count = statesIncrease (cl->count); + f = termmapSet (NULL, sys->runs[rid].role->nameterm, rid); + + // map all labels in prec to LABEL_TODO + g = NULL; + label = rd->label; + + tl = cl->prec; + while (tl != NULL) + { + g = termmapSet (g, tl->term, LABEL_TODO); + tl = tl->next; + } + /* + * Check claim + */ + result = oki_nisynch(sys, i, f, g); + if (!result) + { + cl->failed = statesIncrease (cl->failed); + +//#ifdef DEBUG + warning ("Claim has failed!"); + printf ("To be exact, claim label "); + termPrint (cl->label); + printf (" with prec set "); + termlistPrint (cl->prec); + printf ("\n"); + printf ("i: %i\nf: ",i); + termmapPrint (f); + printf ("\ng: "); + termmapPrint (g); + printf ("\n"); +//#endif + + } + termmapDelete (f); + termmapDelete (g); + return result; +} + diff --git a/src/claim.h b/src/claim.h index 3fe7103..4234f12 100644 --- a/src/claim.h +++ b/src/claim.h @@ -2,5 +2,6 @@ #define CLAIMS int check_claim_nisynch (const System sys, const int i); +int check_claim_niagree (const System sys, const int i); #endif diff --git a/src/compiler.c b/src/compiler.c index 5098df7..f027a36 100644 --- a/src/compiler.c +++ b/src/compiler.c @@ -53,6 +53,7 @@ Term TERM_Agent; Term TERM_Claim; Term CLAIM_Secret; Term CLAIM_Nisynch; +Term CLAIM_Niagree; /* * Global stuff @@ -103,6 +104,7 @@ compile (const System mysys, Tac tc, int maxrunsset) langcons (CLAIM_Secret, "Secret", TERM_Claim); langcons (CLAIM_Nisynch, "Nisynch", TERM_Claim); + langcons (CLAIM_Niagree, "Niagree", TERM_Claim); /* process the tac */ tacProcess (tc); @@ -443,6 +445,14 @@ commEvent (int event, Tac tc) } break; } + if (claim == CLAIM_Niagree) + { + if (n != 0) + { + error ("NIAGREE claim requires no parameters at line %i.", trip->next->lineno); + } + break; + } /* hmm, no handler yet */ @@ -985,6 +995,7 @@ compute_prec_sets (const System sys) Term t; Roledef rd; Term label; + int claim_index; label = cl->label; // Locate r,lev from label, requires (TODO) unique labeling of claims! @@ -1017,7 +1028,7 @@ compute_prec_sets (const System sys) * Now we compute the preceding label set */ cl->prec = NULL; // clear first - i = index (r1,ev1); + claim_index = index (r1,ev1); r2 = 0; while (r2 < sys->rolecount) { @@ -1027,7 +1038,7 @@ compute_prec_sets (const System sys) rd = roledef_re (r2,ev2); while (rd != NULL) { - if (prec[index2 (index (r2,ev2),i)] == 1) + if (prec[index2 (index (r2,ev2),claim_index)] == 1) { // This event precedes the claim @@ -1042,6 +1053,12 @@ compute_prec_sets (const System sys) } r2++; } + /** + * --------------------------- + * Distinguish types of claims + * --------------------------- + */ + // For ni-synch, the preceding label sets are added to the synchronising_labels sets. if (cl->type == CLAIM_Nisynch) { @@ -1050,13 +1067,57 @@ compute_prec_sets (const System sys) tl_scan = cl->prec; while (tl_scan != NULL) { - if (!inTermlist (sys->synchronising_labels, tl_scan->term)) - { - sys->synchronising_labels = termlistAdd (sys->synchronising_labels, tl_scan->term); - } + sys->synchronising_labels = termlistAddNew (sys->synchronising_labels, tl_scan->term); tl_scan = tl_scan->next; } } + + // For ni-agree, the preceding set is also important, but we furthermore need a restricted + // synchronising_labels set + + //@todo Fix ni-agree synchronising label sets + if (cl->type == CLAIM_Niagree) + { + int r_scan; + + // Scan each role (except the current one) and pick out the last prec events. + r_scan = 0; + while (r_scan < sys->rolecount) + { + // Only other roles + if (r_scan != r1) + { + // Scan fully + int ev_scan; + Term t_buf; + + t_buf = NULL; + ev_scan = 0; + while (ev_scan < sys->roleeventmax) + { + // if this event preceds the claim, replace the label term + if (prec[index2 (index (r_scan, ev_scan), claim_index)] == 1) + { + Roledef rd; + + rd = roledef_re (r_scan,ev_scan); + if (rd->label != NULL) + { + t_buf = rd->label; + } + } + ev_scan++; + } + // Store only the last label + if (t_buf != NULL) + { + sys->synchronising_labels = termlistAddNew(sys->synchronising_labels, t_buf); + } + } + r_scan++; + } + } + #ifdef DEBUG // Porparam = 100 (weirdness) [x][cc][debug] can turn of the synchronising label sets (override). if (sys->porparam == 100) diff --git a/src/modelchecker.c b/src/modelchecker.c index a42f024..50ce232 100644 --- a/src/modelchecker.c +++ b/src/modelchecker.c @@ -28,6 +28,7 @@ extern Term CLAIM_Secret; extern Term CLAIM_Nisynch; +extern Term CLAIM_Niagree; /* Some forward declarations. @@ -1258,8 +1259,6 @@ executeTry (const System sys, int run) /* * NISYNCH */ - //!@todo TODO nisynch implementation - flag = check_claim_nisynch (sys, sys->step); if (!flag) { @@ -1273,6 +1272,24 @@ executeTry (const System sys, int run) flag = explorify (sys, run); } } + if (runPoint->to == CLAIM_Niagree) + { + /* + * NIAGREE + */ + flag = check_claim_niagree (sys, sys->step); + if (!flag) + { + /* violation */ + if (violateClaim (sys,sys->step+1, sys->step, NULL )) + flag = explorify (sys, run); + } + else + { + /* no violation */ + flag = explorify (sys, run); + } + } } /* a claim always succeeds */ flag = 1; diff --git a/src/termlist.c b/src/termlist.c index ed02bc3..f5da088 100644 --- a/src/termlist.c +++ b/src/termlist.c @@ -220,7 +220,7 @@ termlistAppend (const Termlist tl, const Term term) * Mimics a basic set type behaviour. */ Termlist -termlistAddNew (const Termlist tl, const term t) +termlistAddNew (const Termlist tl, const Term t) { if (inTermlist (tl, t)) return tl; diff --git a/src/termlist.h b/src/termlist.h index 6cde0e8..93e047b 100644 --- a/src/termlist.h +++ b/src/termlist.h @@ -32,7 +32,7 @@ __inline__ int inTermlist (Termlist tl, const Term term); int isTermlistEqual (Termlist tl1, Termlist tl2); Termlist termlistAdd (Termlist tl, Term term); Termlist termlistAppend (const Termlist tl, const Term term); -Termlist termlistAddNew (const Termlist tl, const term t); +Termlist termlistAddNew (const Termlist tl, const Term t); Termlist termlistConcat (Termlist tl1, Termlist tl2); Termlist termlistDelTerm (Termlist tl); Termlist termlistConjunct (Termlist tl1, Termlist tl2);