- Re-indented the output and latex files.
This commit is contained in:
ccremers
parent
0f4e6a5aba
commit
6efcbdea62
239
src/latex.c
239
src/latex.c
@ -23,7 +23,8 @@ extern Term TERM_Function;
|
||||
|
||||
/* struct for additional info */
|
||||
|
||||
struct traceinfo {
|
||||
struct traceinfo
|
||||
{
|
||||
int match;
|
||||
int position;
|
||||
};
|
||||
@ -37,7 +38,8 @@ int *runPerm;
|
||||
|
||||
/* code */
|
||||
|
||||
void latexInit(const System sys, int argc, char **argv)
|
||||
void
|
||||
latexInit (const System sys, int argc, char **argv)
|
||||
{
|
||||
int i;
|
||||
|
||||
@ -63,7 +65,8 @@ void latexInit(const System sys, int argc, char **argv)
|
||||
printf ("\\input{preamble}\n");
|
||||
}
|
||||
|
||||
void latexDone(const System sys)
|
||||
void
|
||||
latexDone (const System sys)
|
||||
{
|
||||
printf ("\\input{postamble}\n");
|
||||
printf ("\n\\end{document}\n\n");
|
||||
@ -161,9 +164,11 @@ latexTermlistPrint (Termlist tl, Termlist highlight)
|
||||
printf ("]");
|
||||
}
|
||||
|
||||
void latexTimers(const System sys)
|
||||
void
|
||||
latexTimers (const System sys)
|
||||
{
|
||||
void endline (void)
|
||||
{
|
||||
void endline(void) {
|
||||
printf ("\\\\ \\hline\n");
|
||||
}
|
||||
|
||||
@ -193,9 +198,12 @@ void latexTimers(const System sys)
|
||||
* NoClaim no claims
|
||||
*/
|
||||
|
||||
if (sys->claims == 0) {
|
||||
if (sys->claims == 0)
|
||||
{
|
||||
printf ("NoClaim & ");
|
||||
} else {
|
||||
}
|
||||
else
|
||||
{
|
||||
if (sys->failed > 0)
|
||||
printf ("L:%i & ", attackLength (sys->attack));
|
||||
else
|
||||
@ -211,11 +219,14 @@ void latexTimers(const System sys)
|
||||
|
||||
/* states per second */
|
||||
|
||||
if (seconds > 0) {
|
||||
if (seconds > 0)
|
||||
{
|
||||
printf ("$%.3e$ ",
|
||||
(double) (sys->statesLow +
|
||||
(sys->statesHigh * ULONG_MAX)) / seconds);
|
||||
} else {
|
||||
}
|
||||
else
|
||||
{
|
||||
printf ("$\\infty$ ");
|
||||
}
|
||||
endline ();
|
||||
@ -223,7 +234,8 @@ void latexTimers(const System sys)
|
||||
printf ("\\end{tabular}\n\n");
|
||||
}
|
||||
|
||||
void latexMSCStart()
|
||||
void
|
||||
latexMSCStart ()
|
||||
{
|
||||
if (landscape)
|
||||
printf ("\\begin{landscape}\n");
|
||||
@ -231,7 +243,8 @@ void latexMSCStart()
|
||||
printf ("\\begin{msc}{attack}\n");
|
||||
}
|
||||
|
||||
void latexMSCEnd()
|
||||
void
|
||||
latexMSCEnd ()
|
||||
{
|
||||
printf ("\\end{msc}\n");
|
||||
|
||||
@ -240,7 +253,8 @@ void latexMSCEnd()
|
||||
|
||||
}
|
||||
|
||||
void latexDeclInst(const System sys, int run)
|
||||
void
|
||||
latexDeclInst (const System sys, int run)
|
||||
{
|
||||
Term bar = NULL;
|
||||
|
||||
@ -252,7 +266,8 @@ void latexDeclInst(const System sys, int run)
|
||||
printf ("$}\n");
|
||||
}
|
||||
|
||||
void latexEventSpace(int amount)
|
||||
void
|
||||
latexEventSpace (int amount)
|
||||
{
|
||||
int i;
|
||||
//printf("%% number of newlines: %d\n",amount);
|
||||
@ -261,100 +276,120 @@ void latexEventSpace(int amount)
|
||||
}
|
||||
|
||||
|
||||
void latexMessagePrint(struct tracebuf *tb, int from, int to)
|
||||
void
|
||||
latexMessagePrint (struct tracebuf *tb, int from, int to)
|
||||
{
|
||||
|
||||
Term sendTerm = NULL;
|
||||
Term readTerm = NULL;
|
||||
|
||||
if (from == -1 && to == -1) {
|
||||
if (from == -1 && to == -1)
|
||||
{
|
||||
return;
|
||||
}
|
||||
if (from != -1) {
|
||||
if (from != -1)
|
||||
{
|
||||
sendTerm = tb->event[from]->message;
|
||||
}
|
||||
if (to != -1) {
|
||||
if (to != -1)
|
||||
{
|
||||
readTerm = tb->event[to]->message;
|
||||
}
|
||||
if (from == -1 && to != -1) {
|
||||
if (from == -1 && to != -1)
|
||||
{
|
||||
printf ("\\found{$");
|
||||
termPrint (readTerm);
|
||||
printf ("$}{}{run%d}\n", tb->run[to]);
|
||||
} else if (from != -1 && to == -1) {
|
||||
}
|
||||
else if (from != -1 && to == -1)
|
||||
{
|
||||
printf ("\\lost{$");
|
||||
termPrint (sendTerm);
|
||||
printf ("$}{}{run%d}\n", tb->run[from]);
|
||||
} else if (from != -1 && to != -1) {
|
||||
}
|
||||
else if (from != -1 && to != -1)
|
||||
{
|
||||
|
||||
printf ("\\mess{$");
|
||||
|
||||
termPrint (sendTerm);
|
||||
|
||||
if (!isTermEqual(sendTerm, readTerm)) {
|
||||
if (!isTermEqual (sendTerm, readTerm))
|
||||
{
|
||||
printf ("\\rightarrow");
|
||||
termPrint (readTerm);
|
||||
}
|
||||
|
||||
printf ("$}{run%d", tb->run[from]);
|
||||
printf ("}{run%d}[%d]", tb->run[to],
|
||||
EVENTSPACE * (tinfo[to].position -
|
||||
tinfo[from].position));
|
||||
EVENTSPACE * (tinfo[to].position - tinfo[from].position));
|
||||
|
||||
printf ("\n");
|
||||
}
|
||||
}
|
||||
void latexMessagePrintHighlight(struct tracebuf *tb, int from, int to, Termlist highlight)
|
||||
void
|
||||
latexMessagePrintHighlight (struct tracebuf *tb, int from, int to,
|
||||
Termlist highlight)
|
||||
{
|
||||
|
||||
Term sendTerm = NULL;
|
||||
Term readTerm = NULL;
|
||||
|
||||
if (from == -1 && to == -1) {
|
||||
if (from == -1 && to == -1)
|
||||
{
|
||||
return;
|
||||
}
|
||||
if (from != -1) {
|
||||
if (from != -1)
|
||||
{
|
||||
sendTerm = tb->event[from]->message;
|
||||
}
|
||||
if (to != -1) {
|
||||
if (to != -1)
|
||||
{
|
||||
readTerm = tb->event[to]->message;
|
||||
}
|
||||
if (from == -1 && to != -1) {
|
||||
if (from == -1 && to != -1)
|
||||
{
|
||||
printf ("\\found{$");
|
||||
latexTermPrint (readTerm, highlight);
|
||||
printf ("$}{}{run%d}\n", tb->run[to]);
|
||||
} else if (from != -1 && to == -1) {
|
||||
}
|
||||
else if (from != -1 && to == -1)
|
||||
{
|
||||
printf ("\\lost{$");
|
||||
latexTermPrint (sendTerm, highlight);
|
||||
printf ("$}{}{run%d}\n", tb->run[from]);
|
||||
} else if (from != -1 && to != -1) {
|
||||
}
|
||||
else if (from != -1 && to != -1)
|
||||
{
|
||||
|
||||
printf ("\\mess{$");
|
||||
|
||||
latexTermPrint (sendTerm, highlight);
|
||||
|
||||
if (!isTermEqual(sendTerm, readTerm)) {
|
||||
if (!isTermEqual (sendTerm, readTerm))
|
||||
{
|
||||
printf ("\\rightarrow");
|
||||
latexTermPrint (readTerm, highlight);
|
||||
}
|
||||
|
||||
printf ("$}{run%d", tb->run[from]);
|
||||
printf ("}{run%d}[%d]", tb->run[to],
|
||||
EVENTSPACE * (tinfo[to].position -
|
||||
tinfo[from].position));
|
||||
EVENTSPACE * (tinfo[to].position - tinfo[from].position));
|
||||
|
||||
printf ("\n");
|
||||
}
|
||||
}
|
||||
void latexLearnComment(struct tracebuf *tb, int index, Termlist tl)
|
||||
void
|
||||
latexLearnComment (struct tracebuf *tb, int index, Termlist tl)
|
||||
{
|
||||
|
||||
printf("\\msccomment[4ex]{$I_%d=I_%d\\oplus ", index + 1,
|
||||
index);
|
||||
printf ("\\msccomment[4ex]{$I_%d=I_%d\\oplus ", index + 1, index);
|
||||
termlistPrint (tl);
|
||||
printf ("$}{envright}\n");
|
||||
}
|
||||
|
||||
void latexAction(struct tracebuf *tb, int te)
|
||||
void
|
||||
latexAction (struct tracebuf *tb, int te)
|
||||
{
|
||||
printf ("\\action{$");
|
||||
termPrint (tb->event[te]->message);
|
||||
@ -362,7 +397,8 @@ void latexAction(struct tracebuf *tb, int te)
|
||||
//printf("\\nextlevel\n");
|
||||
}
|
||||
|
||||
void latexClaim(struct tracebuf *tb, int run, Termlist tl)
|
||||
void
|
||||
latexClaim (struct tracebuf *tb, int run, Termlist tl)
|
||||
{
|
||||
printf ("\\condition{$");
|
||||
printf ("\\neg secret ");
|
||||
@ -370,7 +406,8 @@ void latexClaim(struct tracebuf *tb, int run, Termlist tl)
|
||||
printf ("$}{run%d}\n", run);
|
||||
}
|
||||
|
||||
int latexCorrespondingSend(struct tracebuf *tb, int rd)
|
||||
int
|
||||
latexCorrespondingSend (struct tracebuf *tb, int rd)
|
||||
{
|
||||
|
||||
int labelMatch = 0;
|
||||
@ -385,16 +422,17 @@ int latexCorrespondingSend(struct tracebuf *tb, int rd)
|
||||
int sendEvent = -1;
|
||||
int bestSendEvent = -1;
|
||||
|
||||
for (sendEvent = readEvent; sendEvent >= 0; sendEvent--) {
|
||||
if (tb->event[sendEvent]->type == SEND) {
|
||||
for (sendEvent = readEvent; sendEvent >= 0; sendEvent--)
|
||||
{
|
||||
if (tb->event[sendEvent]->type == SEND)
|
||||
{
|
||||
/* do all the different kind of matchings first */
|
||||
|
||||
labelMatch =
|
||||
isTermEqual (tb->event[sendEvent]->label,
|
||||
tb->event[readEvent]->label);
|
||||
toMatch =
|
||||
isTermEqual(tb->event[sendEvent]->to,
|
||||
tb->event[readEvent]->to);
|
||||
isTermEqual (tb->event[sendEvent]->to, tb->event[readEvent]->to);
|
||||
fromMatch =
|
||||
isTermEqual (tb->event[sendEvent]->from,
|
||||
tb->event[readEvent]->from);
|
||||
@ -407,27 +445,34 @@ int latexCorrespondingSend(struct tracebuf *tb, int rd)
|
||||
|
||||
nMatches = labelMatch + tofromMatch + messageMatch;
|
||||
|
||||
if (nMatches == 3) {
|
||||
if (nMatches == 3)
|
||||
{
|
||||
/* bingo! success on all matches */
|
||||
|
||||
//printf("Found perfect match: %d\n", s);
|
||||
bestSendEvent = sendEvent;
|
||||
break;
|
||||
}
|
||||
if (nMatches > maxNMatches) {
|
||||
if (labelMatch && messageMatch) {
|
||||
if (nMatches > maxNMatches)
|
||||
{
|
||||
if (labelMatch && messageMatch)
|
||||
{
|
||||
/* strongest restriction: message and label should match */
|
||||
|
||||
maxNMatches = nMatches;
|
||||
bestSendEvent = sendEvent;
|
||||
|
||||
} else if (messageMatch) {
|
||||
}
|
||||
else if (messageMatch)
|
||||
{
|
||||
/* if label AND message don't match: */
|
||||
/* at least message should match */
|
||||
|
||||
maxNMatches = nMatches;
|
||||
bestSendEvent = sendEvent;
|
||||
} else if (labelMatch) {
|
||||
}
|
||||
else if (labelMatch)
|
||||
{
|
||||
/* if message doesn't match */
|
||||
/* the label should matches */
|
||||
|
||||
@ -439,15 +484,19 @@ int latexCorrespondingSend(struct tracebuf *tb, int rd)
|
||||
}
|
||||
|
||||
//bestSendEvent = NULL;
|
||||
if (bestSendEvent == -1) {
|
||||
if (bestSendEvent == -1)
|
||||
{
|
||||
|
||||
int u;
|
||||
|
||||
for (u = 0; u < rd; u++) {
|
||||
if (tb->event[u]->type == SEND) {
|
||||
for (u = 0; u < rd; u++)
|
||||
{
|
||||
if (tb->event[u]->type == SEND)
|
||||
{
|
||||
//knowledgePrint(sys->traceKnow[u]);
|
||||
if (inKnowledge
|
||||
(tb->know[u + 1], tb->event[readEvent]->message)) {
|
||||
(tb->know[u + 1], tb->event[readEvent]->message))
|
||||
{
|
||||
bestSendEvent = u;
|
||||
break;
|
||||
}
|
||||
@ -455,7 +504,8 @@ int latexCorrespondingSend(struct tracebuf *tb, int rd)
|
||||
}
|
||||
}
|
||||
|
||||
if (bestSendEvent == -1) {
|
||||
if (bestSendEvent == -1)
|
||||
{
|
||||
printf ("%% Could not find a matching SEND\n");
|
||||
}
|
||||
return bestSendEvent;
|
||||
@ -493,7 +543,8 @@ newInKnowledge (const Knowledge know, Term term)
|
||||
return 0; /* unrecognized term type, weird */
|
||||
}
|
||||
|
||||
int latexCorrespondingSend2(struct tracebuf *tb, int readEvent)
|
||||
int
|
||||
latexCorrespondingSend2 (struct tracebuf *tb, int readEvent)
|
||||
{
|
||||
int u;
|
||||
|
||||
@ -521,7 +572,8 @@ int latexCorrespondingSend2(struct tracebuf *tb, int readEvent)
|
||||
* Display knowledge in LaTeX format.
|
||||
*/
|
||||
|
||||
void knowledgePrintLatex(Knowledge know)
|
||||
void
|
||||
knowledgePrintLatex (Knowledge know)
|
||||
{
|
||||
Termlist tl;
|
||||
|
||||
@ -537,7 +589,8 @@ void knowledgePrintLatex(Knowledge know)
|
||||
}
|
||||
}
|
||||
|
||||
void attackDisplayLatex(System sys)
|
||||
void
|
||||
attackDisplayLatex (System sys)
|
||||
{
|
||||
int i;
|
||||
struct tracebuf *tb;
|
||||
@ -553,7 +606,8 @@ void attackDisplayLatex(System sys)
|
||||
int bestSend;
|
||||
|
||||
tb = sys->attack;
|
||||
if (tb == NULL) {
|
||||
if (tb == NULL)
|
||||
{
|
||||
printf ("Attack pointer empty: nothing to display.\n");
|
||||
exit (1);
|
||||
}
|
||||
@ -619,12 +673,14 @@ void attackDisplayLatex(System sys)
|
||||
sizeof (struct traceinfo));
|
||||
|
||||
width = 1;
|
||||
for (i = 0; i < tb->length; i++) {
|
||||
for (i = 0; i < tb->length; i++)
|
||||
{
|
||||
if (tb->run[i] >= width)
|
||||
width = tb->run[i] + 1;
|
||||
}
|
||||
|
||||
for (i = 0; i < tb->length; i++) {
|
||||
for (i = 0; i < tb->length; i++)
|
||||
{
|
||||
tb->link[i] = -1;
|
||||
tinfo[i].match = -1;
|
||||
tinfo[i].position = i;
|
||||
@ -633,7 +689,8 @@ void attackDisplayLatex(System sys)
|
||||
tinfo[i].position = i;
|
||||
|
||||
runPosition = (int *) memAlloc (width * sizeof (int));
|
||||
for (i = 0; i < width; i++) {
|
||||
for (i = 0; i < width; i++)
|
||||
{
|
||||
runPosition[i] = 0;
|
||||
}
|
||||
for (i = tb->length - 1; i >= 0; i--)
|
||||
@ -652,7 +709,9 @@ void attackDisplayLatex(System sys)
|
||||
}
|
||||
if (tb->event[i]->type == CLAIM)
|
||||
{
|
||||
claimDetails = claimViolationDetails(sys, tb->run[i], tb->event[i], tb->know[i]);
|
||||
claimDetails =
|
||||
claimViolationDetails (sys, tb->run[i], tb->event[i],
|
||||
tb->know[i]);
|
||||
}
|
||||
}
|
||||
}
|
||||
@ -673,21 +732,27 @@ void attackDisplayLatex(System sys)
|
||||
eventSize = 1;
|
||||
currRun = tb->run[i];
|
||||
|
||||
switch (tb->event[i]->type) {
|
||||
switch (tb->event[i]->type)
|
||||
{
|
||||
case SEND:
|
||||
position++;
|
||||
tinfo[i].position++;
|
||||
break;
|
||||
case READ:
|
||||
if (tb->link[i] != -1) {
|
||||
if (termDistance(tb->event[i]->message,tb->event[tb->link[i]]->message) < LINKTHRESHOLD)
|
||||
if (tb->link[i] != -1)
|
||||
{
|
||||
if (termDistance
|
||||
(tb->event[i]->message,
|
||||
tb->event[tb->link[i]]->message) < LINKTHRESHOLD)
|
||||
{
|
||||
/* disconnect read-send */
|
||||
tb->link[tb->link[i]] = -1;
|
||||
tb->link[i] = -1;
|
||||
} else {
|
||||
if (runPosition[currRun] <= tinfo[tb->link[i]].position &&
|
||||
currRun != tb->run[tb->link[i]])
|
||||
}
|
||||
else
|
||||
{
|
||||
if (runPosition[currRun] <= tinfo[tb->link[i]].position
|
||||
&& currRun != tb->run[tb->link[i]])
|
||||
{
|
||||
printf ("\\comment{\n");
|
||||
termPrint (tb->event[i]->message);
|
||||
@ -696,21 +761,26 @@ void attackDisplayLatex(System sys)
|
||||
printf ("\n");
|
||||
printf ("%% termDistance: %f\n",
|
||||
termDistance (tb->event[i]->message,
|
||||
tb->event[tb->link[i]]->message));
|
||||
tb->event[tb->link[i]]->
|
||||
message));
|
||||
printf ("}\n");
|
||||
tinfo[i].position = tinfo[tb->link[i]].position;
|
||||
eventSize = 0;
|
||||
}
|
||||
}
|
||||
}
|
||||
if (tb->event[i]->internal) {
|
||||
if (tb->event[i]->internal)
|
||||
{
|
||||
eventSize = 0;
|
||||
}
|
||||
break;
|
||||
case CLAIM:
|
||||
if (claimDetails != NULL && claimDetails != (Termlist) -1) {
|
||||
if (claimDetails != NULL && claimDetails != (Termlist) - 1)
|
||||
{
|
||||
eventSize = 2;
|
||||
} else {
|
||||
}
|
||||
else
|
||||
{
|
||||
eventSize = 0;
|
||||
}
|
||||
break;
|
||||
@ -725,7 +795,8 @@ void attackDisplayLatex(System sys)
|
||||
}
|
||||
|
||||
latexMSCStart ();
|
||||
for (i = 0; i < width; i++) {
|
||||
for (i = 0; i < width; i++)
|
||||
{
|
||||
if (runPosition[i] > 0)
|
||||
latexDeclInst (sys, i);
|
||||
}
|
||||
@ -742,7 +813,8 @@ void attackDisplayLatex(System sys)
|
||||
{
|
||||
position = tinfo[i].position;
|
||||
}
|
||||
switch (tb->event[i]->type) {
|
||||
switch (tb->event[i]->type)
|
||||
{
|
||||
case SEND:
|
||||
newtl = knowledgeNew (tb->know[i], tb->know[i + 1]);
|
||||
highlights = NULL;
|
||||
@ -759,29 +831,36 @@ void attackDisplayLatex(System sys)
|
||||
}
|
||||
tl = tl->next;
|
||||
}
|
||||
printf("\\msccomment[4ex]{$I_%d=I_%d\\oplus ", cKnowledge + 1,
|
||||
cKnowledge);
|
||||
printf ("\\msccomment[4ex]{$I_%d=I_%d\\oplus ",
|
||||
cKnowledge + 1, cKnowledge);
|
||||
cKnowledge++;
|
||||
latexTermlistPrint (newtl, highlights);
|
||||
printf ("$}{envright}\n");
|
||||
}
|
||||
|
||||
if (tb->link[i] != -1 && i < tb->length) {
|
||||
if (tb->link[i] != -1 && i < tb->length)
|
||||
{
|
||||
latexMessagePrintHighlight (tb, i, tb->link[i], highlights);
|
||||
} else {
|
||||
}
|
||||
else
|
||||
{
|
||||
latexMessagePrintHighlight (tb, i, -1, highlights); //lost message
|
||||
}
|
||||
termlistDelete (highlights);
|
||||
|
||||
break;
|
||||
case READ:
|
||||
if (tb->event[i]->internal) {
|
||||
} else if (tb->link[i] == -1) {
|
||||
if (tb->event[i]->internal)
|
||||
{
|
||||
}
|
||||
else if (tb->link[i] == -1)
|
||||
{
|
||||
latexMessagePrint (tb, -1, i); //found message
|
||||
}
|
||||
break;
|
||||
case CLAIM:
|
||||
if (claimDetails != NULL && claimDetails != (Termlist) -1) {
|
||||
if (claimDetails != NULL && claimDetails != (Termlist) - 1)
|
||||
{
|
||||
latexClaim (tb, tb->run[i], claimDetails);
|
||||
}
|
||||
break;
|
||||
|
||||
139
src/output.c
139
src/output.c
@ -12,17 +12,20 @@
|
||||
#include "latex.h"
|
||||
|
||||
|
||||
void linePrint(int i)
|
||||
void
|
||||
linePrint (int i)
|
||||
{
|
||||
indent ();
|
||||
while (i > 0) {
|
||||
while (i > 0)
|
||||
{
|
||||
printf ("--------");
|
||||
i--;
|
||||
}
|
||||
printf ("\n");
|
||||
}
|
||||
|
||||
int correspondingSend(System sys, int rd)
|
||||
int
|
||||
correspondingSend (System sys, int rd)
|
||||
{
|
||||
|
||||
int labelMatch = 0;
|
||||
@ -37,8 +40,10 @@ int correspondingSend(System sys, int rd)
|
||||
int sendEvent = -1;
|
||||
int bestSendEvent = -1;
|
||||
|
||||
for (sendEvent = readEvent; sendEvent >= 0; sendEvent--) {
|
||||
if (sys->traceEvent[sendEvent]->type == SEND) {
|
||||
for (sendEvent = readEvent; sendEvent >= 0; sendEvent--)
|
||||
{
|
||||
if (sys->traceEvent[sendEvent]->type == SEND)
|
||||
{
|
||||
/* do all the different kind of matchings first */
|
||||
|
||||
labelMatch =
|
||||
@ -59,14 +64,16 @@ int correspondingSend(System sys, int rd)
|
||||
|
||||
nMatches = labelMatch + tofromMatch + messageMatch;
|
||||
|
||||
if (nMatches == 3) {
|
||||
if (nMatches == 3)
|
||||
{
|
||||
/* bingo! success on all matches */
|
||||
|
||||
//printf("Found perfect match: %d\n", s);
|
||||
bestSendEvent = sendEvent;
|
||||
break;
|
||||
}
|
||||
if (nMatches > maxNMatches) {
|
||||
if (nMatches > maxNMatches)
|
||||
{
|
||||
/* if we found a better candidate than we already had, we'll update */
|
||||
|
||||
//printf("Comparing SEND #%d: ",s);
|
||||
@ -78,19 +85,24 @@ int correspondingSend(System sys, int rd)
|
||||
|
||||
/* however, we first want to be sure that at least some matches are successful */
|
||||
|
||||
if (labelMatch && messageMatch) {
|
||||
if (labelMatch && messageMatch)
|
||||
{
|
||||
/* strongest restriction: message and label should match */
|
||||
|
||||
maxNMatches = nMatches;
|
||||
bestSendEvent = sendEvent;
|
||||
|
||||
} else if (messageMatch) {
|
||||
}
|
||||
else if (messageMatch)
|
||||
{
|
||||
/* if label AND message don't match: */
|
||||
/* at least message should match */
|
||||
|
||||
maxNMatches = nMatches;
|
||||
bestSendEvent = sendEvent;
|
||||
} else if (labelMatch) {
|
||||
}
|
||||
else if (labelMatch)
|
||||
{
|
||||
/* if message doesn't match */
|
||||
/* the label should matches */
|
||||
|
||||
@ -103,7 +115,8 @@ int correspondingSend(System sys, int rd)
|
||||
}
|
||||
|
||||
//bestSendEvent = NULL;
|
||||
if (bestSendEvent == -1) {
|
||||
if (bestSendEvent == -1)
|
||||
{
|
||||
/*Termlist tl;
|
||||
Term t;
|
||||
|
||||
@ -133,8 +146,10 @@ int correspondingSend(System sys, int rd)
|
||||
|
||||
int u;
|
||||
|
||||
for (u = 0; u < rd; u++) {
|
||||
if (sys->traceEvent[u]->type == SEND) {
|
||||
for (u = 0; u < rd; u++)
|
||||
{
|
||||
if (sys->traceEvent[u]->type == SEND)
|
||||
{
|
||||
|
||||
|
||||
//termPrint(readEvent->message);
|
||||
@ -143,7 +158,8 @@ int correspondingSend(System sys, int rd)
|
||||
//printf("Is received message in knowledge after SEND %d? %d\n", u, inKnowledge(sys->traceKnow[u+1],readEvent->message));
|
||||
if (inKnowledge
|
||||
(sys->traceKnow[u + 1],
|
||||
sys->traceEvent[readEvent]->message)) {
|
||||
sys->traceEvent[readEvent]->message))
|
||||
{
|
||||
bestSendEvent = u;
|
||||
break;
|
||||
}
|
||||
@ -151,22 +167,27 @@ int correspondingSend(System sys, int rd)
|
||||
}
|
||||
}
|
||||
|
||||
if (bestSendEvent == -1) {
|
||||
if (bestSendEvent == -1)
|
||||
{
|
||||
printf ("!! Could not find a matching SEND\n");
|
||||
} else {
|
||||
}
|
||||
else
|
||||
{
|
||||
//latexMessagePrint(sys, bestSendEvent, readEvent);
|
||||
//printf("Latex: ");
|
||||
//termPrint(bestSendEvent->from);
|
||||
//printf(" -> ");
|
||||
if (!isTermEqualFn
|
||||
(sys->traceEvent[bestSendEvent]->to,
|
||||
sys->traceEvent[readEvent]->to)) {
|
||||
sys->traceEvent[readEvent]->to))
|
||||
{
|
||||
//termPrint(bestSendEvent->to);
|
||||
//printf(" -> ");
|
||||
}
|
||||
if (!isTermEqualFn
|
||||
(sys->traceEvent[bestSendEvent]->from,
|
||||
sys->traceEvent[readEvent]->from)) {
|
||||
sys->traceEvent[readEvent]->from))
|
||||
{
|
||||
//termPrint(readEvent->from);
|
||||
//printf(" -> ");
|
||||
}
|
||||
@ -176,9 +197,11 @@ int correspondingSend(System sys, int rd)
|
||||
return bestSendEvent;
|
||||
}
|
||||
|
||||
void tracePrint(System sys)
|
||||
void
|
||||
tracePrint (System sys)
|
||||
{
|
||||
if (sys->latex)
|
||||
{
|
||||
if (sys->latex) {
|
||||
//latexTracePrint(sys);
|
||||
return;
|
||||
}
|
||||
@ -197,7 +220,8 @@ void tracePrint(System sys)
|
||||
|
||||
/* how wide is the trace? */
|
||||
width = 0;
|
||||
for (i = 0; i <= sys->step; i++) {
|
||||
for (i = 0; i <= sys->step; i++)
|
||||
{
|
||||
if (sys->traceRun[i] >= width)
|
||||
width = sys->traceRun[i] + 1;
|
||||
}
|
||||
@ -224,18 +248,21 @@ void tracePrint(System sys)
|
||||
linePrint (width);
|
||||
indent ();
|
||||
|
||||
for (i = 0; i < width; i++) {
|
||||
for (i = 0; i < width; i++)
|
||||
{
|
||||
termPrint (sys->runs[i].role->nameterm);
|
||||
printf ("#%i\t", i);
|
||||
}
|
||||
printf ("\n");
|
||||
for (i = 0; i < width; i++) {
|
||||
for (i = 0; i < width; i++)
|
||||
{
|
||||
termPrint (agentOfRun (sys, i));
|
||||
printf ("\t");
|
||||
}
|
||||
printf ("\n");
|
||||
|
||||
for (i = 0; i < width; i++) {
|
||||
for (i = 0; i < width; i++)
|
||||
{
|
||||
agentsOfRunPrint (sys, i);
|
||||
printf ("\t");
|
||||
}
|
||||
@ -243,25 +270,30 @@ void tracePrint(System sys)
|
||||
|
||||
/* now we print the actual trace */
|
||||
|
||||
void sticks(int i) {
|
||||
while (i > 0) {
|
||||
void sticks (int i)
|
||||
{
|
||||
while (i > 0)
|
||||
{
|
||||
printf ("|\t");
|
||||
i--;
|
||||
}
|
||||
}
|
||||
|
||||
void sticksLine(void) {
|
||||
void sticksLine (void)
|
||||
{
|
||||
sticks (width);
|
||||
printf ("\n");
|
||||
}
|
||||
|
||||
linePrint (width);
|
||||
lastrid = -1;
|
||||
for (i = 0; i <= sys->step; i++) {
|
||||
for (i = 0; i <= sys->step; i++)
|
||||
{
|
||||
/* yields extra newlines between switching of runs */
|
||||
|
||||
j = sys->traceRun[i];
|
||||
if (j != lastrid) {
|
||||
if (j != lastrid)
|
||||
{
|
||||
sticksLine ();
|
||||
lastrid = j;
|
||||
}
|
||||
@ -283,7 +315,8 @@ void tracePrint(System sys)
|
||||
|
||||
/* have we learnt anything new? */
|
||||
newtl = knowledgeNew (sys->traceKnow[i], sys->traceKnow[i + 1]);
|
||||
if (newtl != NULL) {
|
||||
if (newtl != NULL)
|
||||
{
|
||||
printf ("\n");
|
||||
sticksLine ();
|
||||
sticks (width);
|
||||
@ -298,7 +331,8 @@ void tracePrint(System sys)
|
||||
printf ("\n");
|
||||
}
|
||||
|
||||
switch (sys->clp) {
|
||||
switch (sys->clp)
|
||||
{
|
||||
case 1:
|
||||
indent ();
|
||||
printf ("---[ constraints ]-----\n");
|
||||
@ -312,7 +346,8 @@ void tracePrint(System sys)
|
||||
|
||||
|
||||
|
||||
void attackDisplayAscii(System sys)
|
||||
void
|
||||
attackDisplayAscii (System sys)
|
||||
{
|
||||
int i, j;
|
||||
int length;
|
||||
@ -330,7 +365,8 @@ void attackDisplayAscii(System sys)
|
||||
|
||||
/* how wide is the trace? */
|
||||
width = 0;
|
||||
for (i = 0; i < length; i++) {
|
||||
for (i = 0; i < length; i++)
|
||||
{
|
||||
if (tb->run[i] >= width)
|
||||
width = tb->run[i] + 1;
|
||||
}
|
||||
@ -355,18 +391,21 @@ void attackDisplayAscii(System sys)
|
||||
linePrint (width);
|
||||
indent ();
|
||||
|
||||
for (i = 0; i < width; i++) {
|
||||
for (i = 0; i < width; i++)
|
||||
{
|
||||
termPrint (sys->runs[i].role->nameterm);
|
||||
printf ("#%i\t", i);
|
||||
}
|
||||
printf ("\n");
|
||||
for (i = 0; i < width; i++) {
|
||||
for (i = 0; i < width; i++)
|
||||
{
|
||||
termPrint (agentOfRun (sys, i));
|
||||
printf ("\t");
|
||||
}
|
||||
printf ("\n");
|
||||
|
||||
for (i = 0; i < width; i++) {
|
||||
for (i = 0; i < width; i++)
|
||||
{
|
||||
agentsOfRunPrint (sys, i);
|
||||
printf ("\t");
|
||||
}
|
||||
@ -374,25 +413,30 @@ void attackDisplayAscii(System sys)
|
||||
|
||||
/* now we print the actual trace */
|
||||
|
||||
void sticks(int i) {
|
||||
while (i > 0) {
|
||||
void sticks (int i)
|
||||
{
|
||||
while (i > 0)
|
||||
{
|
||||
printf ("|\t");
|
||||
i--;
|
||||
}
|
||||
}
|
||||
|
||||
void sticksLine(void) {
|
||||
void sticksLine (void)
|
||||
{
|
||||
sticks (width);
|
||||
printf ("\n");
|
||||
}
|
||||
|
||||
linePrint (width);
|
||||
lastrid = -1;
|
||||
for (i = 0; i < length; i++) {
|
||||
for (i = 0; i < length; i++)
|
||||
{
|
||||
/* yields extra newlines between switching of runs */
|
||||
|
||||
j = tb->run[i];
|
||||
if (j != lastrid) {
|
||||
if (j != lastrid)
|
||||
{
|
||||
sticksLine ();
|
||||
lastrid = j;
|
||||
}
|
||||
@ -414,7 +458,8 @@ void attackDisplayAscii(System sys)
|
||||
|
||||
/* have we learnt anything new? */
|
||||
newtl = knowledgeNew (tb->know[i], tb->know[i + 1]);
|
||||
if (newtl != NULL) {
|
||||
if (newtl != NULL)
|
||||
{
|
||||
printf ("\n");
|
||||
sticksLine ();
|
||||
sticks (width);
|
||||
@ -433,11 +478,15 @@ void attackDisplayAscii(System sys)
|
||||
}
|
||||
|
||||
|
||||
void attackDisplay(System sys)
|
||||
void
|
||||
attackDisplay (System sys)
|
||||
{
|
||||
if (sys->latex)
|
||||
{
|
||||
if (sys->latex) {
|
||||
attackDisplayLatex (sys);
|
||||
} else {
|
||||
}
|
||||
else
|
||||
{
|
||||
attackDisplayAscii (sys);
|
||||
}
|
||||
}
|
||||
|
||||
Loading…
Reference in New Issue
Block a user