andr3/scyther
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

- Revised Arachne dot output significantly. It is now based on explicit

Browse Source 
ranking instead of the subgraphs. This will make it easier to layout
  e.g. LaTeX MSCs using the same algorithm.
This commit is contained in:
ccremers 2004-10-27 16:10:58 +00:00
parent 2680a2ca7a
commit 461a040d29
1 changed files with 73 additions and 28 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

73
src/arachne.c
View File

@ -738,10 +738,11 @@ dotSemiState ()
index = 0;
rd = sys->runs[run].start;
if (sys->runs[run].protocol != INTRUDER)
if (sys->runs[run].protocol != INTRUDER && sys->runs[run].length > 0)
{
// Regular run
/* DISABLED subgraphs
eprintf ("\tsubgraph cluster_run%i {\n", run);
eprintf ("\t\tlabel = \"");
eprintf ("#%i: ", run);
@ -757,6 +758,10 @@ dotSemiState ()
{
eprintf ("\t\tcolor = blue;\n");
}
*/
// Display the respective events
while (index < sys->runs[run].length)
{
// Print node itself
@ -785,7 +790,7 @@ dotSemiState ()
node (run, index - 1);
eprintf (" -> ");
node (run, index);
eprintf (" [style=\"bold\", weight=\"2.0\"]");
eprintf (" [style=\"bold\", weight=\"10.0\"]");
eprintf (";\n");
}
else
@ -820,14 +825,9 @@ dotSemiState ()
}
rd = rd->next;
}
if (done)
{
// Activity other than claims...
if (send_before_read)
{
// Sends first.
// Show this explicitly in the graph by adding a prefix start node
eprintf ("\t\ts%i [label=\"Start ", run);
// Draw the first box
// This used to be drawn only if done && send_before_read, now we always draw it.
eprintf ("\t\ts%i [label=\"Run %i ", run,run);
agentsOfRunPrint (sys, run);
eprintf ("\", shape=diamond];\n");
eprintf ("\t\ts%i -> ", run);
@ -835,12 +835,12 @@ dotSemiState ()
eprintf (";\n");
}
}
}
}
index++;
rd = rd->next;
}
/* DISABLED subgraphs
eprintf ("\t}\n");
*/
}
run++;
}
@ -931,10 +931,53 @@ dotSemiState ()
}
if (other_route == 0)
{
Roledef rd,rd2;
/*
* We have decided to draw this binding,
* from run2,ev2 to run,ev
* However, me might need to decide some colouring for this node.
*/
eprintf ("\t");
node (run2, ev2);
eprintf (" -> ");
node (run, ev);
eprintf (" ");
// decide color
rd = roledef_shift (sys->runs[run].start,ev);
rd2 = roledef_shift (sys->runs[run2].start,ev2);
if (rd->type == CLAIM)
{
// Towards a claim, so only indirect dependency
eprintf ("[color=cornflowerblue]");
}
else
{
// Not towards claim should imply towards read,
// but we check it to comply with future stuff.
if (rd->type == READ && rd2->type == SEND)
{
// We want to distinguish where it is from a 'broken' send
if (isTermEqual (rd->message, rd2->message))
{
if (isTermEqual (rd->from, rd2->from) && isTermEqual (rd->to, rd2->to))
{
// Wow, a perfect match. Leave the arrow as-is :)
eprintf ("[color=forestgreen]");
}
else
{
// Same message, different people
eprintf ("[label=\"redirect\",color=darkorange2]");
}
}
else
{
// Not even the same message, intruder construction
eprintf ("[label=\"construct\",color=red]");
}
}
}
// close up
eprintf (";\n");
}
}
@ -976,6 +1019,8 @@ dotSemiState ()
count = 0;
run = 0;
while (run < sys->maxruns)
{
if (sys->runs[run].protocol != INTRUDER)
{
int ev;
@ -985,13 +1030,13 @@ dotSemiState ()
if (myrank == ranks[node_number (run,ev)])
{
if (count == 0)
// For now, disabled
eprintf ("//\t{ rank = same; ");
eprintf ("\t{ rank = same; ");
count++;
eprintf ("r%ii%i; ",run,ev);
}
ev++;
}
}
run++;
}
if (count > 0)