From db18b203a9cd8040dbfa104c45bde4a560b250f4 Mon Sep 17 00:00:00 2001 From: ccremers Date: Thu, 16 Jun 2005 11:59:44 +0000 Subject: [PATCH] - Added "Empty" claim type, which is ignored. Syntax example: claim_x(I, Empty); --- src/arachne.c | 105 ++++++++++++++++++++++++--------------------- src/compiler.c | 6 +++ src/main.c | 96 +++++++++++++++++++++-------------------- src/modelchecker.c | 10 ++++- 4 files changed, 121 insertions(+), 96 deletions(-) diff --git a/src/arachne.c b/src/arachne.c index bca2c86..35e0f52 100644 --- a/src/arachne.c +++ b/src/arachne.c @@ -36,6 +36,8 @@ extern Term CLAIM_Secret; extern Term CLAIM_Nisynch; extern Term CLAIM_Niagree; +extern Term CLAIM_Empty; + extern Term TERM_Agent; extern Term TERM_Hidden; extern Term TERM_Function; @@ -3309,66 +3311,73 @@ arachne () /** * Check each claim */ - Protocol p; - Role r; - if (switches.filterClaim == NULL || switches.filterClaim == cl->type) + // Skip the dummy claims + if (!isTermEqual (cl->type, CLAIM_Empty)) { - int run; - - sys->current_claim = cl; - attack_length = INT_MAX; - cl->complete = 1; - p = (Protocol) cl->protocol; - r = (Role) cl->role; - - if (switches.output == PROOF) + // Any other claims might be filterered + if (switches.filterClaim == NULL + || switches.filterClaim == cl->type) { - indentPrint (); - eprintf ("Testing Claim "); - termPrint (cl->type); - eprintf (" from "); - termPrint (p->nameterm); - eprintf (", "); - termPrint (r->nameterm); - eprintf (" at index %i.\n", cl->ev); - } - indentDepth++; - run = semiRunCreate (p, r); - proof_suppose_run (run, 0, cl->ev + 1); - add_read_goals (run, 0, cl->ev + 1); + int run; + Protocol p; + Role r; + + sys->current_claim = cl; + attack_length = INT_MAX; + cl->complete = 1; + p = (Protocol) cl->protocol; + r = (Role) cl->role; + + if (switches.output == PROOF) + { + indentPrint (); + eprintf ("Testing Claim "); + termPrint (cl->type); + eprintf (" from "); + termPrint (p->nameterm); + eprintf (", "); + termPrint (r->nameterm); + eprintf (" at index %i.\n", cl->ev); + } + indentDepth++; + run = semiRunCreate (p, r); + proof_suppose_run (run, 0, cl->ev + 1); + add_read_goals (run, 0, cl->ev + 1); /** * Add specific goal info */ - add_claim_specifics (cl, - roledef_shift (sys->runs[run].start, cl->ev)); + add_claim_specifics (cl, + roledef_shift (sys->runs[run].start, + cl->ev)); #ifdef DEBUG - if (DEBUGL (5)) - { - printSemiState (); - } + if (DEBUGL (5)) + { + printSemiState (); + } #endif - // Iterate - iterate (); + // Iterate + iterate (); - //! Destroy - while (sys->bindings != NULL) - { - goal_remove_last (1); - } - while (sys->maxruns > 0) - { - semiRunDestroy (); - } + //! Destroy + while (sys->bindings != NULL) + { + goal_remove_last (1); + } + while (sys->maxruns > 0) + { + semiRunDestroy (); + } - //! Indent back - indentDepth--; + //! Indent back + indentDepth--; - if (switches.output == PROOF) - { - indentPrint (); - eprintf ("Proof complete for this claim.\n"); + if (switches.output == PROOF) + { + indentPrint (); + eprintf ("Proof complete for this claim.\n"); + } } } // next diff --git a/src/compiler.c b/src/compiler.c index 90474b3..2e4e420 100644 --- a/src/compiler.c +++ b/src/compiler.c @@ -64,6 +64,7 @@ Term TERM_Claim; Term CLAIM_Secret; Term CLAIM_Nisynch; Term CLAIM_Niagree; +Term CLAIM_Empty; /* * Global stuff @@ -108,6 +109,7 @@ compilerInit (const System mysys) langcons (CLAIM_Secret, "Secret", TERM_Claim); langcons (CLAIM_Nisynch, "Nisynch", TERM_Claim); langcons (CLAIM_Niagree, "Niagree", TERM_Claim); + langcons (CLAIM_Empty, "Empty", TERM_Claim); } //! Make a global constant @@ -593,6 +595,10 @@ commEvent (int event, Tac tc) } break; } + if (claim == CLAIM_Empty) + { + break; + } /* hmm, no handler yet */ diff --git a/src/main.c b/src/main.c index 0c938cf..c1039b3 100644 --- a/src/main.c +++ b/src/main.c @@ -65,6 +65,7 @@ System sys; extern struct tacnode *spdltac; extern Term TERM_Claim; +extern Term CLAIM_Empty; extern int mgu_match; void scanner_cleanup (void); @@ -366,66 +367,69 @@ timersPrint (const System sys) anyclaims = 0; while (cl_scan != NULL) { - anyclaims = 1; + if (!isTermEqual (cl_scan->type, CLAIM_Empty)) + { + anyclaims = 1; - eprintf ("claim\t"); + eprintf ("claim\t"); - /* claim label is tuple */ - if (realTermTuple (cl_scan->label)) - { - /* modern version: claim label is tuple (protocname, label) */ - /* first print protocol.role */ - termPrint (TermOp1 (cl_scan->label)); - eprintf ("\t"); - termPrint (cl_scan->rolename); - eprintf ("\t"); - /* second print event_label */ - termPrint (cl_scan->type); - eprintf ("_"); - termPrint (TermOp2 (cl_scan->label)); - eprintf ("\t"); - } - else - { - /* old-fashioned output */ - termPrint (cl_scan->type); - eprintf ("\t"); - termPrint (cl_scan->rolename); - eprintf (" ("); - termPrint (cl_scan->label); - eprintf (")\t"); - } - /* print counts etc. */ - eprintf ("found:\t"); - statesFormat (cl_scan->count); - if (cl_scan->count > 0) - { - if (cl_scan->failed > 0) + /* claim label is tuple */ + if (realTermTuple (cl_scan->label)) { + /* modern version: claim label is tuple (protocname, label) */ + /* first print protocol.role */ + termPrint (TermOp1 (cl_scan->label)); + eprintf ("\t"); + termPrint (cl_scan->rolename); + eprintf ("\t"); + /* second print event_label */ + termPrint (cl_scan->type); + eprintf ("_"); + termPrint (TermOp2 (cl_scan->label)); eprintf ("\t"); - eprintf ("failed:\t"); - statesFormat (cl_scan->failed); } else { - eprintf ("\tcorrect: "); - if (cl_scan->complete) + /* old-fashioned output */ + termPrint (cl_scan->type); + eprintf ("\t"); + termPrint (cl_scan->rolename); + eprintf (" ("); + termPrint (cl_scan->label); + eprintf (")\t"); + } + /* print counts etc. */ + eprintf ("found:\t"); + statesFormat (cl_scan->count); + if (cl_scan->count > 0) + { + if (cl_scan->failed > 0) { - eprintf ("complete_proof"); + eprintf ("\t"); + eprintf ("failed:\t"); + statesFormat (cl_scan->failed); } else { - eprintf ("bounded_proof"); - if (cl_scan->timebound) - eprintf ("\ttime=%i", get_time_limit ()); + eprintf ("\tcorrect: "); + if (cl_scan->complete) + { + eprintf ("complete_proof"); + } + else + { + eprintf ("bounded_proof"); + if (cl_scan->timebound) + eprintf ("\ttime=%i", get_time_limit ()); + } } } + else + { + eprintf ("\tcorrect: does_not_occur"); + } + eprintf ("\n"); } - else - { - eprintf ("\tcorrect: does_not_occur"); - } - eprintf ("\n"); cl_scan = cl_scan->next; } if (!anyclaims) diff --git a/src/modelchecker.c b/src/modelchecker.c index f674188..e50910b 100644 --- a/src/modelchecker.c +++ b/src/modelchecker.c @@ -30,6 +30,7 @@ extern Term CLAIM_Secret; extern Term CLAIM_Nisynch; extern Term CLAIM_Niagree; +extern Term CLAIM_Empty; /* Some forward declarations. @@ -1404,7 +1405,7 @@ executeTry (const System sys, int run) termlistDelete (sys->secrets); sys->secrets = oldsecrets; } - if (runPoint->to == CLAIM_Nisynch) + else if (runPoint->to == CLAIM_Nisynch) { /* * NISYNCH @@ -1422,7 +1423,7 @@ executeTry (const System sys, int run) flag = explorify (sys, run); } } - if (runPoint->to == CLAIM_Niagree) + else if (runPoint->to == CLAIM_Niagree) { /* * NIAGREE @@ -1440,6 +1441,11 @@ executeTry (const System sys, int run) flag = explorify (sys, run); } } + else // if (runPoint->to == CLAIM_Empty) + { + // Skip other claim types + flag = explorify (sys, run); + } } /* a claim always succeeds */ flag = 1;