- Added the names of the involved protocols to the attack output.
This commit is contained in:
parent
4cefc16543
commit
ec459dcbde
29
src/latex.c
29
src/latex.c
@ -228,12 +228,14 @@ latexTimers (const System sys)
|
|||||||
}
|
}
|
||||||
|
|
||||||
void
|
void
|
||||||
latexMSCStart ()
|
latexMSCStart (Termlist protocolnames)
|
||||||
{
|
{
|
||||||
if (landscape)
|
if (landscape)
|
||||||
printf ("\\begin{landscape}\n");
|
printf ("\\begin{landscape}\n");
|
||||||
|
|
||||||
printf ("\\begin{msc}{attack}\n");
|
printf ("\\begin{msc}{attack on $");
|
||||||
|
termlistPrint(protocolnames);
|
||||||
|
printf ("$}\n");
|
||||||
}
|
}
|
||||||
|
|
||||||
void
|
void
|
||||||
@ -787,13 +789,34 @@ attackDisplayLatex (System sys)
|
|||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
latexMSCStart ();
|
/* create title */
|
||||||
|
|
||||||
|
Termlist protocolnames = NULL;
|
||||||
|
Term pname;
|
||||||
|
for (i = 0; i < width; i++)
|
||||||
|
{
|
||||||
|
if (runPosition[i] > 0)
|
||||||
|
{
|
||||||
|
pname = sys->runs[i].protocol->nameterm;
|
||||||
|
if (!inTermlist(protocolnames, pname))
|
||||||
|
{
|
||||||
|
protocolnames = termlistAppend(protocolnames, pname);
|
||||||
|
}
|
||||||
|
}
|
||||||
|
}
|
||||||
|
latexMSCStart (protocolnames);
|
||||||
|
termlistDelete (protocolnames);
|
||||||
|
|
||||||
|
/* declare instances */
|
||||||
|
|
||||||
for (i = 0; i < width; i++)
|
for (i = 0; i < width; i++)
|
||||||
{
|
{
|
||||||
if (runPosition[i] > 0)
|
if (runPosition[i] > 0)
|
||||||
latexDeclInst (sys, i);
|
latexDeclInst (sys, i);
|
||||||
}
|
}
|
||||||
|
|
||||||
|
/* print the events in the attack */
|
||||||
|
|
||||||
//for (j=-1; j<=sys->step; j++)
|
//for (j=-1; j<=sys->step; j++)
|
||||||
position = 0;
|
position = 0;
|
||||||
cKnowledge = 0;
|
cKnowledge = 0;
|
||||||
|
Loading…
Reference in New Issue
Block a user