diff --git a/src/dotout.c b/src/dotout.c index 28dfc32..b44d2ba 100644 --- a/src/dotout.c +++ b/src/dotout.c @@ -17,7 +17,6 @@ extern Role I_RRSD; #define isBound(rd) (rd->bound) #define length step - #define CLAIMTEXTCOLOR "#ffffff" #define CLAIMCOLOR "#000000" #define GOODCOMMCOLOR "forestgreen" @@ -36,6 +35,9 @@ extern Role I_RRSD; #define UNTRUSTEDCOLORS 0.4 #define MONOCHROMEFACTOR 0.7 // Monochrome settings. 0.0: all colors become white. 1.0: all colors remain the same lightness as the color versions. +#define CHOOSEWEIGHT "2.0" +#define RUNWEIGHT "10.0" + /* * Dot output * @@ -576,6 +578,54 @@ graph_ranks (int *ranks, int nodes) return rank; } +//! Display the ranks +/** + * Reinstated after it had been gone for a while + */ +void +showRanks (const System sys, const int maxrank, const int *ranks, + const int nodes) +{ + int rank; + + return; + + for (rank = 0; rank <= maxrank; rank++) + { + int found; + int run; + + found = 0; + for (run = 0; run < sys->maxruns; run++) + { + if (sys->runs[run].protocol != INTRUDER) + { + int ev; + + for (ev = 0; ev < sys->runs[run].step; ev++) + { + int n; + + n = eventNode (run, ev); + if (ranks[n] == rank) + { + if (found == 0) + { + eprintf ("\t{ rank = same; "); + } + node (sys, run, n); + eprintf ("; "); + found++; + } + } + } + } + if (found > 0) + { + eprintf ("}\n"); + } + } +} //! Iterate over events (in non-intruder runs) in which some value term occurs first. // Function should return true for iteration to continue. @@ -690,7 +740,8 @@ drawClass (const System sys, Binding b) chooseTermNode (varterm); eprintf (" -> "); node (sys, b->run_to, b->ev_to); - eprintf (" [weight=\"2.0\",arrowhead=\"none\",style=\"dotted\"];\n"); + eprintf (" [weight=\"%s\",arrowhead=\"none\",style=\"dotted\"];\n", + CHOOSEWEIGHT); } //! Print label of a regular->regular transition node (when comm. is not exact) @@ -880,6 +931,212 @@ drawAllBindings (const System sys) return fromintr; } +//! Print "Alice in role R" of a run +void +printAgentInRole (const System sys, const int run) +{ + Term rolename; + Term agentname; + + rolename = sys->runs[run].role->nameterm; + agentname = agentOfRunRole (sys, run, rolename); + explainVariable (agentname); + eprintf (" in role "); + termPrintRemap (rolename); +} + +//! rho, sigma, const +/* + * true if it has printed + */ +int +showLocal (const int run, Term told, Term tnew) +{ + if (realTermVariable (tnew)) + { + if (termOccursInRun (tnew, run)) + { + // Variables are mapped, maybe. But then we wonder whether they occur in reads. + termPrintRemap (told); + eprintf (" : "); + explainVariable (tnew); + } + else + { + return false; + } + } + else + { + termPrintRemap (tnew); + } + return true; +} + + +//! show a list of locals +/** + * always ends with a seperator if something was printed + */ +int +showLocals (const int run, Termlist tlold, Termlist tlnew, Term tavoid, + char *sep) +{ + int printsep; + int anything; + + printsep = false; + anything = false; + while (tlold != NULL && tlnew != NULL) + { + if (!isTermEqual (tlold->term, tavoid)) + { + if (printsep) + { + eprintf (sep); + printsep = false; + } + printsep = showLocal (run, tlold->term, tlnew->term); + if (printsep) + { + anything = true; + } + } + tlold = tlold->next; + tlnew = tlnew->next; + } + if (printsep) + { + eprintf (sep); + } + return anything; +} + +//! Explain the local constants +/** + * Return true iff something was printed + */ +int +printRunConstants (const System sys, const int run) +{ + if (sys->runs[run].constants != NULL) + { + eprintf ("Create "); + showLocals (run, sys->runs[run].role-> + declaredconsts, sys->runs[run].constants, NULL, ", "); + eprintf ("\\l"); + return true; + } + else + { + return false; + } +} + + +//! Explain a run in two lines +void +printRunExplanation (const System sys, const int run, const char *runrolesep, + const char *newline) +{ + int hadcontent; + + eprintf ("Run "); + printVisualRun (run); + + eprintf (runrolesep); + // Print first line + printAgentInRole (sys, run); + eprintf ("\\l"); + + // Second line + // Possible protocol (if more than one) + { + int showprotocol; + Protocol p; + int morethanone; + + // Simple case: don't show + showprotocol = false; + + // Check whether the protocol spec has more than one + morethanone = false; + for (p = sys->protocols; p != NULL; p = p->next) + { + if (p != INTRUDER) + { + if (p != sys->runs[run].protocol) + { + morethanone = true; + break; + } + } + } + + // More than one? + if (morethanone) + { + if (run == 0) + { + // If this is run 0 we report the protocol anyway, even is there is only a single one in the attack + showprotocol = true; + } + else + { + int r; + // For other runs we only report when there are multiple protocols + showprotocol = false; + for (r = 0; r < sys->maxruns; r++) + { + if (sys->runs[r].protocol != INTRUDER) + { + if (sys->runs[r].protocol != sys->runs[run].protocol) + { + showprotocol = true; + break; + } + } + } + } + } + + // Use the result + if (showprotocol) + { + eprintf ("Protocol "); + termPrintRemap (sys->runs[run].protocol->nameterm); + eprintf ("\\l"); + } + } + + eprintf (newline); + hadcontent = false; + + if (termlistLength (sys->runs[run].rho) > 1) + { + hadcontent = showLocals (run, sys->runs[run].protocol-> + rolenames, sys->runs[run].rho, + sys->runs[run].role->nameterm, "\\l"); + } + + if (hadcontent) + { + eprintf (newline); + hadcontent = false; + } + hadcontent = printRunConstants (sys, run); + + if (sys->runs[run].sigma != NULL) + { + if (hadcontent) + { + eprintf (newline); + hadcontent = false; + } + showLocals (run, sys->runs[run].role-> + declaredvars, sys->runs[run].sigma, NULL, "\\l"); + } +} //! Draw regular runs void @@ -908,23 +1165,17 @@ drawRegularRuns (const System sys) rd = sys->runs[run].start; // Regular run - /* - eprintf ("\tsubgraph cluster_run%i {\n", run); - eprintf ("\t\tlabel = \""); - eprintf ("#%i: ", run); - termPrintRemap (sys->runs[run].protocol->nameterm); - eprintf (", "); - agentsOfRunPrint (sys, run); - eprintf ("\\nTesting the second line\";\n", run); - if (run == 0) - { - eprintf ("\t\tcolor = red;\n"); - } - else - { - eprintf ("\t\tcolor = blue;\n"); - } - */ + if (switches.clusters) + { + eprintf ("\tsubgraph cluster_run%i {\n", run); + + eprintf ("\t\tstyle=filled;\n"); + eprintf ("\t\tcolor=lightgrey;\n"); + + eprintf ("\t\tlabel=\""); + printRunExplanation (sys, run, " : ", ""); + eprintf ("\";\n\n"); + } // set color setRunColorBuf (sys, run, colorbuf); @@ -982,7 +1233,8 @@ drawRegularRuns (const System sys) node (sys, run, prevnode); eprintf (" -> "); node (sys, run, index); - eprintf (" [style=\"bold\", weight=\"10.0\"]"); + eprintf (" [style=\"bold\", weight=\"%s\"]", + RUNWEIGHT); eprintf (";\n"); prevnode = index; } @@ -1018,187 +1270,38 @@ drawRegularRuns (const System sys) } rd = rd->next; } - // Draw the first box (HEADER) - // This used to be drawn only if done && send_before_read, now we always draw it. - eprintf ("\t\ts%i [label=\"{ ", run); - // Print first line - { - Term rolename; - Term agentname; - - rolename = sys->runs[run].role->nameterm; - agentname = - agentOfRunRole (sys, run, rolename); - explainVariable (agentname); - eprintf (" in role "); - termPrintRemap (rolename); - eprintf ("\\l"); - } - - // Second line - // Possible protocol (if more than one) - { - int showprotocol; - Protocol p; - int morethanone; - - // Simple case: don't show - showprotocol = false; - - // Check whether the protocol spec has more than one - morethanone = false; - for (p = sys->protocols; p != NULL; - p = p->next) - { - if (p != INTRUDER) - { - if (p != sys->runs[run].protocol) - { - morethanone = true; - break; - } - } - } - - // More than one? - if (morethanone) - { - if (run == 0) - { - // If this is run 0 we report the protocol anyway, even is there is only a single one in the attack - showprotocol = true; - } - else - { - int r; - // For other runs we only report when there are multiple protocols - showprotocol = false; - for (r = 0; r < sys->maxruns; r++) - { - if (sys->runs[r].protocol != - INTRUDER) - { - if (sys->runs[r].protocol != - sys->runs[run].protocol) - { - showprotocol = true; - break; - } - } - } - } - } - - // Use the result - if (showprotocol) - { - eprintf ("Protocol "); - termPrintRemap (sys->runs[run].protocol-> - nameterm); - eprintf ("\\l"); - } - } - eprintf ("Run "); - printVisualRun (run); - eprintf ("\\l"); - - - // rho, sigma, const - /* true if it has printed - */ - int showLocal (Term told, Term tnew) - { - if (realTermVariable (tnew)) - { - if (termOccursInRun (tnew, run)) - { - // Variables are mapped, maybe. But then we wonder whether they occur in reads. - termPrintRemap (told); - eprintf (" : "); - explainVariable (tnew); - } - else - { - return false; - } - } - else - { - termPrintRemap (tnew); - } - return true; - } - - void showLocals (Termlist tlold, Termlist tlnew, - Term tavoid, char *sep) - { - int printsep; - - printsep = false; - while (tlold != NULL && tlnew != NULL) - { - if (!isTermEqual (tlold->term, tavoid)) - { - if (printsep) - { - eprintf (sep); - printsep = false; - } - printsep = - showLocal (tlold->term, - tlnew->term); - } - tlold = tlold->next; - tlnew = tlnew->next; - } - } - - if (termlistLength (sys->runs[run].rho) > 1) + if (!switches.clusters) { - eprintf ("|"); - showLocals (sys->runs[run].protocol-> - rolenames, sys->runs[run].rho, - sys->runs[run].role->nameterm, - "\\l"); - eprintf ("\\l"); + // Draw the first box (HEADER) + // This used to be drawn only if done && send_before_read, now we always draw it. + eprintf ("\t\ts%i [label=\"{ ", run); + + printRunExplanation (sys, run, "\\l", "|"); + // close up + eprintf ("}\", shape=record"); + eprintf (",style=filled,fillcolor=\"%s\"", + colorbuf + 8); + eprintf ("];\n"); + eprintf ("\t\ts%i -> ", run); + node (sys, run, index); + eprintf (" [style=bold, weight=\"%s\"];\n", + RUNWEIGHT); + prevnode = index; } - if (sys->runs[run].constants != NULL) - { - eprintf ("|Create "); - showLocals (sys->runs[run].role-> - declaredconsts, - sys->runs[run].constants, NULL, - ", "); - eprintf ("\\l"); - } - if (sys->runs[run].sigma != NULL) - { - eprintf ("|"); - showLocals (sys->runs[run].role-> - declaredvars, - sys->runs[run].sigma, NULL, - "\\l"); - eprintf ("\\l"); - } - // close up - eprintf ("}\", shape=record"); - eprintf (",style=filled,fillcolor=\"%s\"", - colorbuf + 8); - eprintf ("];\n"); - eprintf ("\t\ts%i -> ", run); - node (sys, run, index); - eprintf (" [style=bold, weight=\"10.0\"];\n"); - prevnode = index; } } } index++; rd = rd->next; } - //eprintf ("\t}\n"); + + if (switches.clusters) + { + eprintf ("\t}\n"); + } } } @@ -1257,7 +1360,6 @@ drawIntruderRuns (const System sys) //eprintf ("\t}\n\n"); } - //! Display the current semistate using dot output format. /** * This is not as nice as we would like it. Furthermore, the function is too big. @@ -1410,7 +1512,7 @@ dotSemiState (const System mysys) #endif // Ranks - //showRanks (sys, maxrank, ranks); + showRanks (sys, maxrank, ranks, nodes); #ifdef DEBUG // Debug: print dependencies diff --git a/src/switches.c b/src/switches.c index f2c20c1..acdc766 100644 --- a/src/switches.c +++ b/src/switches.c @@ -78,6 +78,7 @@ switchesInit (int argc, char **argv) switches.extendTrivial = 0; // default off switches.plain = false; // default colors for terminal switches.monochrome = false; // default colors for dot + switches.clusters = false; // default is no clusters for now // Process the environment variable SCYTHERFLAGS process_environment (); @@ -907,6 +908,20 @@ switcher (const int process, int index, int commandline) } } + if (detect (' ', "clusters", 0)) + { + if (!process) + { + /* discourage: hide + */ + } + else + { + switches.clusters = true; + return index; + } + } + if (detect (' ', "intruder-actions", 1)) { if (!process) diff --git a/src/switches.h b/src/switches.h index cf670d8..441eb15 100644 --- a/src/switches.h +++ b/src/switches.h @@ -58,6 +58,7 @@ struct switchdata int extendTrivial; //!< Show further events in arachne xml output, based on knowledge underapproximation. (Includes at least the events of the nonreads extension) int plain; //!< Disable color output on terminal int monochrome; //!< Disable colors in dot output + int clusters; //!> Enable clusters in output }; extern struct switchdata switches; //!< pointer to switchdata structure