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

- Better handling of function from M0 collapse in dot output.

Browse Source
This commit is contained in:
ccremers 2006-07-02 12:51:19 +00:00
parent aeac3d6616
commit 0184b6277b
1 changed files with 52 additions and 45 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

75
src/dotout.c
View File

@ -587,17 +587,12 @@ isApplication (const System sys, const int run)
return false;
}
//! Check whether the event is an M_0 function application (special case of the previous)
//! Is an event enabled by M0 only?
int
isApplicationM0 (const System sys, const int run)
isEnabledM0 (const System sys, const int run, const int ev)
{
if (isApplication (sys, run))
{
int from_m0;
List bl;
from_m0 = false;
for (bl = sys->bindings; bl != NULL; bl = bl->next)
{
Binding b;
@ -609,14 +604,9 @@ isApplicationM0 (const System sys, const int run)
// still show it somewhere.
if (b->done)
{
// The '1' denotes that the key is in the second position
if (b->run_to == run && b->ev_to == 1)
if (b->run_to == run && b->ev_to == ev)
{
if (sys->runs[b->run_from].role == I_M)
{
from_m0 = true;
}
else
if (sys->runs[b->run_from].role != I_M)
{
return false;
}
@ -624,10 +614,21 @@ isApplicationM0 (const System sys, const int run)
}
}
}
if (from_m0)
{
// Source from M_0, and no others
return true;
}
//! Check whether the event is an M_0 function application (special case of the previous)
int
isApplicationM0 (const System sys, const int run)
{
if (sys->runs[run].length > 1)
{
if (isApplication (sys, run))
{
if (isEnabledM0 (sys, run, 1))
{
return true;
}
}
}
return false;
@ -963,10 +964,27 @@ regularModifiedLabel (Binding b)
void
drawBinding (const System sys, Binding b)
{
int intr_to, intr_from;
int intr_to, intr_from, m0_from;
void myarrow (const Binding b)
{
if (m0_from)
{
eprintf ("\t");
intruderNodeM0 ();
eprintf (" -> ");
node (sys, b->run_to, b->ev_to);
}
else
{
arrow (sys, b);
}
}
intr_from = (sys->runs[b->run_from].protocol == INTRUDER);
intr_to = (sys->runs[b->run_to].protocol == INTRUDER);
m0_from = false;
// Pruning: things going to M0 applications are pruned;
if (isApplicationM0 (sys, b->run_to))
@ -975,18 +993,7 @@ drawBinding (const System sys, Binding b)
}
if (isApplicationM0 (sys, b->run_from))
{
int run;
int ev;
eprintf ("\t");
intruderNodeM0 ();
eprintf (" -> ");
node (sys, b->run_to, b->ev_to);
eprintf (" [label=\"");
termPrintRemap (b->term);
eprintf ("\"]");
eprintf (";\n");
return;
m0_from = true;
}
// Normal drawing cases;
@ -1018,7 +1025,7 @@ drawBinding (const System sys, Binding b)
{
// intr->intr
eprintf ("\t");
arrow (sys, b);
myarrow (b);
eprintf (" [label=\"");
termPrintRemap (b->term);
eprintf ("\"]");
@ -1028,7 +1035,7 @@ drawBinding (const System sys, Binding b)
{
// intr->regular
eprintf ("\t");
arrow (sys, b);
myarrow (b);
eprintf (";\n");
}
}
@ -1039,7 +1046,7 @@ drawBinding (const System sys, Binding b)
{
// regular->intr
eprintf ("\t");
arrow (sys, b);
myarrow (b);
eprintf (";\n");
}
else
@ -1051,7 +1058,7 @@ drawBinding (const System sys, Binding b)
if (isCommunicationExact (sys, b))
{
eprintf ("\t");
arrow (sys, b);
myarrow (b);
eprintf (" [style=bold,color=\"%s\"]", GOODCOMMCOLOR);
eprintf (";\n");
}