From 2e94dd065eeee72efba24534a3d87a3bdc43cf85 Mon Sep 17 00:00:00 2001 From: ccremers Date: Fri, 26 May 2006 11:27:05 +0000 Subject: [PATCH] - "--clusters" output is quite advanced, but still dot makes a bit of a mess out of it. One of the reasons is that the intruder events cannot be used along with the normal ranking, because they no longer correspond to real events. --- src/depend.c | 1 - src/dotout.c | 221 ++++++++++++++++++++++++++++++++++----------------- src/system.c | 27 ++++++- src/system.h | 2 + 4 files changed, 174 insertions(+), 77 deletions(-) diff --git a/src/depend.c b/src/depend.c index f0cc106..6b9978f 100644 --- a/src/depend.c +++ b/src/depend.c @@ -562,7 +562,6 @@ iteratePrecedingEvents (const System sys, int (*func) (int run, int ev), { return false; } - break; } } } diff --git a/src/dotout.c b/src/dotout.c index b44d2ba..c7c123c 100644 --- a/src/dotout.c +++ b/src/dotout.c @@ -37,6 +37,8 @@ extern Role I_RRSD; #define CHOOSEWEIGHT "2.0" #define RUNWEIGHT "10.0" +//#define CHOOSEWEIGHT "1.0" +//#define RUNWEIGHT "1.0" /* * Dot output @@ -517,6 +519,30 @@ isCommunicationExact (const System sys, Binding b) return true; } +//! Ignore some events +int +isEventIgnored (const System sys, int run, int ev) +{ + Roledef rd; + + rd = eventRoledef (sys, run, ev); + if (rd->type == CLAIM) + { + if (run != 0) + { + return true; + } + else + { + if (ev != sys->current_claim->ev) + { + return true; + } + } + } + return false; +} + //! Determine ranks for all nodes /** * Some crude algorithm I sketched on the blackboard. @@ -524,9 +550,19 @@ isCommunicationExact (const System sys, Binding b) int graph_ranks (int *ranks, int nodes) { - int i; - int todo; + int done; int rank; + int changes; + + int getrank (int run, int ev) + { + return ranks[eventNode (run, ev)]; + } + + void setrank (int run, int ev, int rank) + { + ranks[eventNode (run, ev)] = rank; + } #ifdef DEBUG if (hasCycle ()) @@ -535,45 +571,82 @@ graph_ranks (int *ranks, int nodes) } #endif - i = 0; - while (i < nodes) - { - ranks[i] = INT_MAX; - i++; - } + { + int i; + + for (i = 0; i < nodes; i++) + { + ranks[i] = INT_MAX; + } + } - todo = nodes; rank = 0; - while (todo > 0) + done = false; + changes = true; + while (!done) { - // There are still unassigned nodes - int n; - - n = 0; - while (n < nodes) + int checkCanEventHappenNow (int run, Roledef rd, int ev) + { + //if (sys->runs[run].protocol != INTRUDER) { - if (ranks[n] == INT_MAX) + if (getrank (run, ev) == INT_MAX) { - // Does this node have incoming stuff from stuff with equal rank or higher? - int refn; + // Allright, this regular event is not assigned yet + int precevent (int run2, int ev2) + { + //if (sys->runs[run2].protocol != INTRUDER) + { + // regular preceding event + int rank2; - refn = 0; - while (refn < nodes) - { - if (ranks[refn] >= rank && getNode (refn, n)) - refn = nodes + 1; - else - refn++; + rank2 = getrank (run2, ev2); + if (rank2 > rank) + { + // higher rank, this cannot be done + return false; + } + if (rank2 == rank) + { + // equal rank: only if different run + if ((sys->runs[run].protocol != INTRUDER) + && (run2 == run)) + { + return false; + } + } } - if (refn == nodes) + return true; + } + + if (iteratePrecedingEvents (sys, precevent, run, ev)) { - ranks[n] = rank; - todo--; + // we can do it! + changes = true; + setrank (run, ev, rank); + } + else + { + done = false; } } - n++; } - rank++; + return true; + } + + + if (!changes) + { + rank++; + if (rank >= nodes) + { + warning ("Rank %i increased to the number of nodes %i.", rank, + nodes); + return rank; + } + } + done = true; + changes = false; + iterateAllEvents (sys, checkCanEventHappenNow); } return rank; } @@ -588,7 +661,7 @@ showRanks (const System sys, const int maxrank, const int *ranks, { int rank; - return; + //return; for (rank = 0; rank <= maxrank; rank++) { @@ -604,18 +677,22 @@ showRanks (const System sys, const int maxrank, const int *ranks, for (ev = 0; ev < sys->runs[run].step; ev++) { - int n; - - n = eventNode (run, ev); - if (ranks[n] == rank) + if (!isEventIgnored (sys, run, ev)) { - if (found == 0) + + int n; + + n = eventNode (run, ev); + if (ranks[n] == rank) { - eprintf ("\t{ rank = same; "); + if (found == 0) + { + eprintf ("\t{ rank = same; "); + } + node (sys, run, ev); + eprintf ("; "); + found++; } - node (sys, run, n); - eprintf ("; "); - found++; } } } @@ -979,8 +1056,8 @@ showLocal (const int run, Term told, Term tnew) * always ends with a seperator if something was printed */ int -showLocals (const int run, Termlist tlold, Termlist tlnew, Term tavoid, - char *sep) +showLocals (const int run, Termlist tlold, Termlist tlnew, + Term tavoid, char *sep) { int printsep; int anything; @@ -1036,8 +1113,8 @@ printRunConstants (const System sys, const int run) //! Explain a run in two lines void -printRunExplanation (const System sys, const int run, const char *runrolesep, - const char *newline) +printRunExplanation (const System sys, const int run, + const char *runrolesep, const char *newline) { int hadcontent; @@ -1183,24 +1260,7 @@ drawRegularRuns (const System sys) // Display the respective events while (index < sys->runs[run].length) { - int showthis; - - showthis = true; - if (rd->type == CLAIM) - { - if (run != 0) - { - showthis = false; - } - else - { - if (index != sys->current_claim->ev) - { - showthis = false; - } - } - } - if (showthis) + if (!isEventIgnored (sys, run, index)) { // Print node itself eprintf ("\t\t"); @@ -1280,13 +1340,15 @@ drawRegularRuns (const System sys) printRunExplanation (sys, run, "\\l", "|"); // close up eprintf ("}\", shape=record"); - eprintf (",style=filled,fillcolor=\"%s\"", - colorbuf + 8); + 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); + eprintf + (" [style=bold, weight=\"%s\"];\n", + RUNWEIGHT); prevnode = index; } @@ -1315,11 +1377,14 @@ drawIntruderRuns (const System sys) { int run; - /* - eprintf ("\tsubgraph intruder {\n"); - eprintf ("\t\tlabel = \"Intruder\\nTesting the seconds.\";\n"); - eprintf ("\t\tcolor = red;\n"); - */ + if (switches.clusters) + { + //eprintf ("\tsubgraph cluster_intruder {\n"); + eprintf ("\tsubgraph intr {\n"); + eprintf ("\t\tlabel = \"Intruder\";\n"); + eprintf ("\t\tcolor = red;\n"); + } + for (run = 0; run < sys->maxruns; run++) { if (sys->runs[run].length > 0) @@ -1357,7 +1422,10 @@ drawIntruderRuns (const System sys) } } } - //eprintf ("\t}\n\n"); + if (switches.clusters) + { + eprintf ("\t}\n\n"); + } } //! Display the current semistate using dot output format. @@ -1499,8 +1567,8 @@ dotSemiState (const System mysys) if (isDependEvent (r1, e1, r2, e2)) { eprintf - ("\tr%ii%i -> r%ii%i [color=grey];\n", r1, - e1, r2, e2); + ("\tr%ii%i -> r%ii%i [color=grey];\n", + r1, e1, r2, e2); } } } @@ -1512,7 +1580,10 @@ dotSemiState (const System mysys) #endif // Ranks - showRanks (sys, maxrank, ranks, nodes); + if (switches.clusters) + { + showRanks (sys, maxrank, ranks, nodes); + } #ifdef DEBUG // Debug: print dependencies diff --git a/src/system.c b/src/system.c index b8c8897..8c13b2a 100644 --- a/src/system.c +++ b/src/system.c @@ -1295,7 +1295,32 @@ iterateEvents (const System sys, const int run, return true; } -// Iterate over event type in a certain run (increasing through role) +//! Iterate over all events in all runs +/** + * This includes intruder as well as regular events + */ +int +iterateAllEvents (const System sys, + int (*callback) (int run, Roledef rd, int ev)) +{ + int run; + + int callwrapper (Roledef rd, int ev) + { + return callback (run, rd, ev); + } + + for (run = 0; run < sys->maxruns; run++) + { + if (!iterateEvents (sys, run, callwrapper)) + { + return false; + } + } + return true; +} + +//! Iterate over event type in a certain run (increasing through role) /** * If evtype == ANYEVENT then it does not matter. */ diff --git a/src/system.h b/src/system.h index 0a0e1c6..5ab319a 100644 --- a/src/system.h +++ b/src/system.h @@ -197,6 +197,8 @@ int iterateRuns (const System sys, int (*callback) (int r)); int iterateRegularRuns (const System sys, int (*callback) (int r)); int iterateEvents (const System sys, const int run, int (*callback) (Roledef rd, int ev)); +int iterateAllEvents (const System sys, + int (*callback) (int run, Roledef rd, int ev)); int iterateEventsType (const System sys, const int run, const int evtype, int (*callback) (Roledef rd, int ev)); int iterateLocalToOther (const System sys, const int myrun,