From f3d4e8c350ff304c7ad826c2ca5de925fe105c35 Mon Sep 17 00:00:00 2001 From: ccremers Date: Mon, 20 Mar 2006 09:40:45 +0000 Subject: [PATCH] - Some improvements to the intruder nodes. --- src/dotout.c | 245 +++++++++++++++++++-------------------------------- 1 file changed, 89 insertions(+), 156 deletions(-) diff --git a/src/dotout.c b/src/dotout.c index 69d2914..48cb917 100644 --- a/src/dotout.c +++ b/src/dotout.c @@ -83,6 +83,43 @@ termPrintRemap (const Term t) termPrintCustom (t, "", "", "(", ")", "\\{ ", " \\}", printVisualRun); } +//! Print a term; if it is a variable, show that +void +explainVariable (Term t) +{ + t = deVar (t); + if (realTermVariable (t)) + { + eprintf ("any "); + if (t->roleVar) + { + eprintf ("agent "); + } + termPrintRemap (t); + if (!t->roleVar) + { + if (switches.match == 0 && t->stype != NULL) + { + Termlist tl; + + eprintf (" of type "); + for (tl = t->stype; tl != NULL; tl = tl->next) + { + termPrintRemap (tl->term); + if (tl->next != NULL) + { + eprintf (","); + } + } + } + } + } + else + { + termPrintRemap (t); + } +} + //! Draw node void node (const System sys, const int run, const int index) @@ -598,8 +635,8 @@ drawClass (const System sys, Binding b) // not seen before: choose class eprintf ("\t"); chooseTermNode (varterm); - eprintf (" [label=\"Any "); - termPrintRemap (varterm); + eprintf (" [label=\""); + explainVariable (varterm); eprintf ("\"];\n"); eprintf ("\t"); chooseTermNode (varterm); @@ -608,6 +645,52 @@ drawClass (const System sys, Binding b) eprintf (" [weight=\"2.0\",arrowhead=\"none\",style=\"dotted\"];\n"); } +//! Print label of a regular->regular transition node (when comm. is not exact) +/** + * Note that we ignore any label differences, these are left implicit + */ +void +regularModifiedLabel (Binding b) +{ + Roledef rdfrom; + Roledef rdto; + + rdfrom = eventRoledef (sys, b->run_from, b->ev_from); + rdto = eventRoledef (sys, b->run_to, b->ev_to); + + // First up: compare messages contents' + if (!isTermEqual (rdfrom->message, b->term)) + { + // What is sent is not equal to what is bound + if (termInTerm (rdfrom->message, b->term)) + { + // Interm: simple select + eprintf ("select "); + termPrint (b->term); + eprintf ("\\n"); + } + else + { + // I'm not quite sure + eprintf ("modify\\n"); + } + } + + // Second: agent things + if (!isTermEqual (rdfrom->from, rdto->from)) + { + eprintf ("fake sender "); + termPrint (rdto->from); + eprintf ("\\n"); + } + if (!isTermEqual (rdfrom->to, rdto->to)) + { + eprintf ("redirect to "); + termPrint (rdto->to); + eprintf ("\\n"); + } +} + //! Draw a single binding void drawBinding (const System sys, Binding b) @@ -697,15 +780,8 @@ drawBinding (const System sys, Binding b) redirNode (sys, b); eprintf (" [style=filled,fillcolor=\""); printColor (INTRUDERCOLORH, INTRUDERCOLORL, INTRUDERCOLORS); - eprintf ("\",label=\"redirect"); - if (!isTermEqual - (eventRoledef (sys, b->run_from, b->ev_from)->message, - b->term)) - { - // Only explicitly mention redirect term when it differs from the sent term - eprintf ("\\n"); - termPrintRemap (b->term); - } + eprintf ("\",label=\""); + regularModifiedLabel (b); eprintf ("\"]"); eprintf (";\n"); @@ -753,34 +829,6 @@ drawAllBindings (const System sys) return fromintr; } -//! Nicely format the role and agents we think we're talking to. -void -agentsOfRunPrintOthers (const System sys, const int run) -{ - Term role = sys->runs[run].role->nameterm; - Termlist roles = sys->runs[run].protocol->rolenames; - - while (roles != NULL) - { - if (!isTermEqual (role, roles->term)) - { - Term agent; - - termPrintRemap (roles->term); - eprintf (" is "); - agent = agentOfRunRole (sys, run, roles->term); - if (isTermVariable (agent)) - { - eprintf ("any "); - } - termPrintRemap (agent); - eprintf ("\\l"); - } - roles = roles->next; - } -} - - //! Draw regular runs void @@ -931,11 +979,7 @@ drawRegularRuns (const System sys) rolename = sys->runs[run].role->nameterm; agentname = agentOfRunRole (sys, run, rolename); - if (isTermVariable (agentname)) - { - eprintf ("Any agent "); - } - termPrintRemap (agentname); + explainVariable (agentname); eprintf (" in role "); termPrintRemap (rolename); eprintf ("\\l"); @@ -1018,39 +1062,10 @@ drawRegularRuns (const System sys) { if (termOccursInRun (tnew, run)) { - Term t; - // Variables are mapped, maybe. But then we wonder whether they occur in reads. termPrintRemap (told); - t = deVar (tnew); eprintf (" : "); - if (realTermVariable (t)) - { - eprintf ("any "); - termPrintRemap (t); - if ((!t->roleVar) - && switches.match == 0 - && t->stype != NULL) - { - Termlist tl; - - eprintf (" of type "); - for (tl = t->stype; - tl != NULL; - tl = tl->next) - { - termPrintRemap (tl->term); - if (tl->next != NULL) - { - eprintf (","); - } - } - } - } - else - { - termPrintRemap (t); - } + explainVariable (tnew); } else { @@ -1191,85 +1206,6 @@ drawIntruderRuns (const System sys) //eprintf ("\t}\n\n"); } -//! Show intruder choices -void -drawIntruderChoices (const System sys) -{ - Termlist shown; - List bl; - - shown = NULL; - for (bl = sys->bindings; bl != NULL; bl = bl->next) - { - Binding b; - - b = (Binding) bl->data; - if ((!b->blocked) && (!b->done) && isTermVariable (b->term)) - { - /* - * If the binding is not blocked, but also not done, - * the intruder can apparently satisfy it at will. - */ - - if (!inTermlist (shown, b->term)) - { - int firsthere (int run, int ev) - { - /** - * @todo This is not very efficient, - * but maybe that is not really - * needed here. - */ - int notearlier (int run2, int ev2) - { - if (sys->runs[run2].protocol != INTRUDER) - { - return (!roledefSubTerm - (eventRoledef (sys, run2, ev2), b->term)); - } - else - { - return true; - } - } - - if (iteratePrecedingEvents (sys, notearlier, run, ev)) - { - eprintf ("\t"); - chooseTermNode (b->term); - eprintf (" -> "); - node (sys, run, ev); - eprintf (" [color=\"darkgreen\"];\n"); - } - return true; - } - - // If the first then we add a header - if (shown == NULL) - { - eprintf ("// Showing intruder choices.\n"); - } - // Not in the list, show new node - shown = termlistAdd (shown, b->term); - eprintf ("\t"); - chooseTermNode (b->term); - eprintf (" [label=\"Class: any "); - termPrintRemap (b->term); - eprintf ("\",color=\"darkgreen\"];\n"); - - iterate_first_regular_occurrences (sys, firsthere, b->term); - } - } - - } - - if (shown != NULL) - { - eprintf ("\n"); - } - termlistDelete (shown); -} - //! Display the current semistate using dot output format. /** @@ -1422,9 +1358,6 @@ dotSemiState (const System mysys) } #endif - // Intruder choices - //drawIntruderChoices (sys); - // Ranks //showRanks (sys, maxrank, ranks);