diff --git a/src/latex.c b/src/latex.c index e3a0c44..52891f6 100644 --- a/src/latex.c +++ b/src/latex.c @@ -23,9 +23,10 @@ extern Term TERM_Function; /* struct for additional info */ -struct traceinfo { - int match; - int position; +struct traceinfo +{ + int match; + int position; }; /* global variables for this module */ @@ -37,109 +38,111 @@ int *runPerm; /* code */ -void latexInit(const System sys, int argc, char **argv) +void +latexInit (const System sys, int argc, char **argv) { - int i; + int i; - printf("\\documentclass{article}\n"); - printf("\\usepackage{msc}\n"); - printf("%%\n"); - printf("%% LaTeX output generated by %s\n", progname); - printf("%% Input:\n"); + printf ("\\documentclass{article}\n"); + printf ("\\usepackage{msc}\n"); + printf ("%%\n"); + printf ("%% LaTeX output generated by %s\n", progname); + printf ("%% Input:\n"); - /* print command line */ - printf("%% $"); - for (i = 0; i < argc; i++) - printf(" %s", argv[i]); - printf("\n"); + /* print command line */ + printf ("%% $"); + for (i = 0; i < argc; i++) + printf (" %s", argv[i]); + printf ("\n"); - printf("%%\n"); - printf("\\begin{document}\n\n"); + printf ("%%\n"); + printf ("\\begin{document}\n\n"); - /* comment macro (used for debugging) */ - printf("\\newcommand{\\comment}[1]{}\n"); + /* comment macro (used for debugging) */ + printf ("\\newcommand{\\comment}[1]{}\n"); - /* preamble */ - printf("\\input{preamble}\n"); + /* preamble */ + printf ("\\input{preamble}\n"); } -void latexDone(const System sys) +void +latexDone (const System sys) { - printf("\\input{postamble}\n"); - printf("\n\\end{document}\n\n"); + printf ("\\input{postamble}\n"); + printf ("\n\\end{document}\n\n"); } void latexTermPrint (Term term, Termlist highlight) { - if (term == NULL) - { - printf ("Empty term"); - return; - } + if (term == NULL) + { + printf ("Empty term"); + return; + } #ifdef DEBUG - if (!DEBUGL (1)) - { - term = deVar (term); - } + if (!DEBUGL (1)) + { + term = deVar (term); + } #else - term = deVar (term); + term = deVar (term); #endif - if (realTermLeaf (term)) + if (realTermLeaf (term)) + { + if (inTermlist (highlight, term)) + printf ("\\mathbf{"); + symbolPrint (term->symb); + if (realTermVariable (term)) + printf ("V"); + if (term->runid >= 0) { - if (inTermlist(highlight, term)) - printf("\\mathbf{"); - symbolPrint (term->symb); - if (realTermVariable (term)) - printf ("V"); - if (term->runid >= 0) - { - printf ("\\sharp%i", term->runid); - } - if (term->subst != NULL) - { - printf ("\\rightarrow"); - latexTermPrint (term->subst, highlight); - } - if (inTermlist(highlight, term)) - printf("}"); + printf ("\\sharp%i", term->runid); } - if (realTermTuple (term)) + if (term->subst != NULL) { - printf ("("); - while (realTermTuple (term)) - { - latexTermPrint (term->op1, highlight); - printf (","); - term = term->op2; - if (!realTermTuple (term)) - latexTermPrint (term, highlight); + printf ("\\rightarrow"); + latexTermPrint (term->subst, highlight); + } + if (inTermlist (highlight, term)) + printf ("}"); + } + if (realTermTuple (term)) + { + printf ("("); + while (realTermTuple (term)) + { + latexTermPrint (term->op1, highlight); + printf (","); + term = term->op2; + if (!realTermTuple (term)) + latexTermPrint (term, highlight); - } - printf (")"); - return; } - if (realTermEncrypt (term)) + printf (")"); + return; + } + if (realTermEncrypt (term)) + { + if (isTermLeaf (term->key) + && inTermlist (term->key->stype, TERM_Function)) { - if (isTermLeaf (term->key) - && inTermlist (term->key->stype, TERM_Function)) - { - /* function application */ - latexTermPrint (term->key, highlight); - printf ("("); - latexTermPrint (term->op, highlight); - printf (")"); - } - else - { - /* normal encryption */ - printf ("\\{"); - latexTermPrint (term->op, highlight); - printf ("\\}_{"); - latexTermPrint (term->key, highlight); - printf ("}"); - } + /* function application */ + latexTermPrint (term->key, highlight); + printf ("("); + latexTermPrint (term->op, highlight); + printf (")"); } + else + { + /* normal encryption */ + printf ("\\{"); + latexTermPrint (term->op, highlight); + printf ("\\}_{"); + latexTermPrint (term->key, highlight); + printf ("}"); + } + } } void @@ -156,309 +159,356 @@ latexTermlistPrint (Termlist tl, Termlist highlight) latexTermPrint (tl->term, highlight); tl = tl->next; if (tl != NULL) - printf(", "); + printf (", "); } printf ("]"); } -void latexTimers(const System sys) +void +latexTimers (const System sys) { - void endline(void) { - printf("\\\\ \\hline\n"); + void endline (void) + { + printf ("\\\\ \\hline\n"); + } + + printf ("\\begin{tabular}{|r|r|c|r|} \\hline\n"); + + /* display stats, header first */ + + printf ("Time & States & Attack & st/sec"); + endline (); + + /* print time */ + + double seconds; + seconds = (double) clock () / CLOCKS_PER_SEC; + printf ("$%.3e$ &", seconds); + + /* states traversed */ + + printf ("$"); + statesPrintShort (sys); + printf ("$ &"); + + /* flag + * + * L n Attack of length + * None failed claim + * NoClaim no claims + */ + + if (sys->claims == 0) + { + printf ("NoClaim & "); + } + else + { + if (sys->failed > 0) + printf ("L:%i & ", attackLength (sys->attack)); + else + printf ("None & "); } - printf("\\begin{tabular}{|r|r|c|r|} \\hline\n"); + /* + printf("%.3e (%li) claims encountered.\n",(double) + sys->claims, sys->claims); + printf("%.3e (%li) claims failed.\n",(double) + sys->failed, sys->failed); + */ - /* display stats, header first */ + /* states per second */ - printf("Time & States & Attack & st/sec"); - endline(); - - /* print time */ - - double seconds; - seconds = (double) clock() / CLOCKS_PER_SEC; - printf("$%.3e$ &", seconds); - - /* states traversed */ - - printf("$"); - statesPrintShort(sys); - printf("$ &"); - - /* flag - * - * L n Attack of length - * None failed claim - * NoClaim no claims - */ - - if (sys->claims == 0) { - printf("NoClaim & "); - } else { - if (sys->failed > 0) - printf("L:%i & ", attackLength(sys->attack)); - else - printf("None & "); + if (seconds > 0) + { + printf ("$%.3e$ ", + (double) (sys->statesLow + + (sys->statesHigh * ULONG_MAX)) / seconds); } - - /* - printf("%.3e (%li) claims encountered.\n",(double) - sys->claims, sys->claims); - printf("%.3e (%li) claims failed.\n",(double) - sys->failed, sys->failed); - */ - - /* states per second */ - - if (seconds > 0) { - printf("$%.3e$ ", - (double) (sys->statesLow + - (sys->statesHigh * ULONG_MAX)) / seconds); - } else { - printf("$\\infty$ "); + else + { + printf ("$\\infty$ "); } - endline(); + endline (); - printf("\\end{tabular}\n\n"); + printf ("\\end{tabular}\n\n"); } -void latexMSCStart() +void +latexMSCStart () { - if (landscape) - printf("\\begin{landscape}\n"); + if (landscape) + printf ("\\begin{landscape}\n"); - printf("\\begin{msc}{attack}\n"); + printf ("\\begin{msc}{attack}\n"); } -void latexMSCEnd() +void +latexMSCEnd () { - printf("\\end{msc}\n"); + printf ("\\end{msc}\n"); - if (landscape) - printf("\\end{landscape}\n"); + if (landscape) + printf ("\\end{landscape}\n"); } -void latexDeclInst(const System sys, int run) +void +latexDeclInst (const System sys, int run) { - Term bar = NULL; + Term bar = NULL; - bar = agentOfRun(sys, run); - printf("\\declinst{run%d}{$", run); - termPrint(bar); - printf("\\sharp%i$}{$", run); - agentsOfRunPrint(sys, run); - printf("$}\n"); + bar = agentOfRun (sys, run); + printf ("\\declinst{run%d}{$", run); + termPrint (bar); + printf ("\\sharp%i$}{$", run); + agentsOfRunPrint (sys, run); + printf ("$}\n"); } -void latexEventSpace(int amount) +void +latexEventSpace (int amount) { - int i; - //printf("%% number of newlines: %d\n",amount); - for (i = 0; i < EVENTSPACE * amount; i++) - printf("\\nextlevel\n"); + int i; + //printf("%% number of newlines: %d\n",amount); + for (i = 0; i < EVENTSPACE * amount; i++) + printf ("\\nextlevel\n"); } -void latexMessagePrint(struct tracebuf *tb, int from, int to) +void +latexMessagePrint (struct tracebuf *tb, int from, int to) { - Term sendTerm = NULL; - Term readTerm = NULL; + Term sendTerm = NULL; + Term readTerm = NULL; - if (from == -1 && to == -1) { - return; + if (from == -1 && to == -1) + { + return; + } + if (from != -1) + { + sendTerm = tb->event[from]->message; + } + if (to != -1) + { + readTerm = tb->event[to]->message; + } + if (from == -1 && to != -1) + { + printf ("\\found{$"); + termPrint (readTerm); + printf ("$}{}{run%d}\n", tb->run[to]); + } + else if (from != -1 && to == -1) + { + printf ("\\lost{$"); + termPrint (sendTerm); + printf ("$}{}{run%d}\n", tb->run[from]); + } + else if (from != -1 && to != -1) + { + + printf ("\\mess{$"); + + termPrint (sendTerm); + + if (!isTermEqual (sendTerm, readTerm)) + { + printf ("\\rightarrow"); + termPrint (readTerm); } - if (from != -1) { - sendTerm = tb->event[from]->message; - } - if (to != -1) { - readTerm = tb->event[to]->message; - } - if (from == -1 && to != -1) { - printf("\\found{$"); - termPrint(readTerm); - printf("$}{}{run%d}\n", tb->run[to]); - } else if (from != -1 && to == -1) { - printf("\\lost{$"); - termPrint(sendTerm); - printf("$}{}{run%d}\n", tb->run[from]); - } else if (from != -1 && to != -1) { - printf("\\mess{$"); + printf ("$}{run%d", tb->run[from]); + printf ("}{run%d}[%d]", tb->run[to], + EVENTSPACE * (tinfo[to].position - tinfo[from].position)); - termPrint(sendTerm); - - 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)); - - printf("\n"); - } + 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; + Term sendTerm = NULL; + Term readTerm = NULL; - if (from == -1 && to == -1) { - return; + if (from == -1 && to == -1) + { + return; + } + if (from != -1) + { + sendTerm = tb->event[from]->message; + } + if (to != -1) + { + readTerm = tb->event[to]->message; + } + if (from == -1 && to != -1) + { + printf ("\\found{$"); + latexTermPrint (readTerm, highlight); + printf ("$}{}{run%d}\n", tb->run[to]); + } + else if (from != -1 && to == -1) + { + printf ("\\lost{$"); + latexTermPrint (sendTerm, highlight); + printf ("$}{}{run%d}\n", tb->run[from]); + } + else if (from != -1 && to != -1) + { + + printf ("\\mess{$"); + + latexTermPrint (sendTerm, highlight); + + if (!isTermEqual (sendTerm, readTerm)) + { + printf ("\\rightarrow"); + latexTermPrint (readTerm, highlight); } - if (from != -1) { - sendTerm = tb->event[from]->message; - } - if (to != -1) { - readTerm = tb->event[to]->message; - } - if (from == -1 && to != -1) { - printf("\\found{$"); - latexTermPrint(readTerm, highlight); - printf("$}{}{run%d}\n", tb->run[to]); - } else if (from != -1 && to == -1) { - printf("\\lost{$"); - latexTermPrint(sendTerm, highlight); - printf("$}{}{run%d}\n", tb->run[from]); - } else if (from != -1 && to != -1) { - printf("\\mess{$"); + printf ("$}{run%d", tb->run[from]); + printf ("}{run%d}[%d]", tb->run[to], + EVENTSPACE * (tinfo[to].position - tinfo[from].position)); - latexTermPrint(sendTerm, highlight); - - 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)); - - printf("\n"); - } + 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); - termlistPrint(tl); - printf("$}{envright}\n"); + 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); - printf("$}{run%d}\n", tb->run[te]); - //printf("\\nextlevel\n"); + printf ("\\action{$"); + termPrint (tb->event[te]->message); + printf ("$}{run%d}\n", tb->run[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 "); - termlistPrint(tl); - printf("$}{run%d}\n", run); + printf ("\\condition{$"); + printf ("\\neg secret "); + termlistPrint (tl); + printf ("$}{run%d}\n", run); } -int latexCorrespondingSend(struct tracebuf *tb, int rd) +int +latexCorrespondingSend (struct tracebuf *tb, int rd) { - int labelMatch = 0; - int toMatch = 0; - int fromMatch = 0; - int tofromMatch = 0; - int messageMatch = 0; - int nMatches = 0; - int maxNMatches = 0; + int labelMatch = 0; + int toMatch = 0; + int fromMatch = 0; + int tofromMatch = 0; + int messageMatch = 0; + int nMatches = 0; + int maxNMatches = 0; - int readEvent = rd; - int sendEvent = -1; - int bestSendEvent = -1; + int readEvent = rd; + int sendEvent = -1; + int bestSendEvent = -1; - for (sendEvent = readEvent; sendEvent >= 0; sendEvent--) { - if (tb->event[sendEvent]->type == SEND) { - /* do all the different kind of matchings first */ + 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); - fromMatch = - isTermEqual(tb->event[sendEvent]->from, - tb->event[readEvent]->from); - tofromMatch = toMatch || fromMatch; - messageMatch = - isTermEqual(tb->event[sendEvent]->message, - tb->event[readEvent]->message); + labelMatch = + isTermEqual (tb->event[sendEvent]->label, + tb->event[readEvent]->label); + toMatch = + isTermEqual (tb->event[sendEvent]->to, tb->event[readEvent]->to); + fromMatch = + isTermEqual (tb->event[sendEvent]->from, + tb->event[readEvent]->from); + tofromMatch = toMatch || fromMatch; + messageMatch = + isTermEqual (tb->event[sendEvent]->message, + tb->event[readEvent]->message); - /* calculate the score */ + /* calculate the score */ - nMatches = labelMatch + tofromMatch + messageMatch; + nMatches = labelMatch + tofromMatch + messageMatch; - if (nMatches == 3) { - /* bingo! success on all matches */ + if (nMatches == 3) + { + /* bingo! success on all matches */ - //printf("Found perfect match: %d\n", s); - bestSendEvent = sendEvent; - break; + //printf("Found perfect match: %d\n", s); + bestSendEvent = sendEvent; + break; } - if (nMatches > maxNMatches) { - if (labelMatch && messageMatch) { - /* strongest restriction: message and label should match */ + if (nMatches > maxNMatches) + { + if (labelMatch && messageMatch) + { + /* strongest restriction: message and label should match */ - maxNMatches = nMatches; - bestSendEvent = sendEvent; + maxNMatches = nMatches; + bestSendEvent = sendEvent; - } else if (messageMatch) { - /* if label AND message don't match: */ - /* at least message should match */ + } + else if (messageMatch) + { + /* if label AND message don't match: */ + /* at least message should match */ - maxNMatches = nMatches; - bestSendEvent = sendEvent; - } else if (labelMatch) { - /* if message doesn't match */ - /* the label should matches */ + maxNMatches = nMatches; + bestSendEvent = sendEvent; + } + else if (labelMatch) + { + /* if message doesn't match */ + /* the label should matches */ - maxNMatches = nMatches; - bestSendEvent = sendEvent; + maxNMatches = nMatches; + bestSendEvent = sendEvent; } } } } - //bestSendEvent = NULL; - if (bestSendEvent == -1) { + //bestSendEvent = NULL; + if (bestSendEvent == -1) + { - int u; + int u; - 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)) { - bestSendEvent = u; - break; + 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)) + { + bestSendEvent = u; + break; } } } } - if (bestSendEvent == -1) { - printf("%% Could not find a matching SEND\n"); + if (bestSendEvent == -1) + { + printf ("%% Could not find a matching SEND\n"); } - return bestSendEvent; + return bestSendEvent; } @@ -487,33 +537,34 @@ newInKnowledge (const Knowledge know, Term term) if (term->type == TUPLE) { return (inTermlist (know->encrypt, term) || - (inKnowledge (know, term->op1) || + (inKnowledge (know, term->op1) || inKnowledge (know, term->op2))); } return 0; /* unrecognized term type, weird */ } -int latexCorrespondingSend2(struct tracebuf *tb, int readEvent) +int +latexCorrespondingSend2 (struct tracebuf *tb, int readEvent) { - int u; + int u; - for (u = tb->length - 1; u>=0 ; u--) - { - if (tb->event[u]->type == SEND) - { - if (!inKnowledge (tb->know[u], tb->event[readEvent]->message)) - { - /* - printf("%% term["); - printf("]#%d is introduced at traceEvent[%d] ",readEvent,u); - printf("\n"); - */ - return u; - } - } - } - - return -1; + for (u = tb->length - 1; u >= 0; u--) + { + if (tb->event[u]->type == SEND) + { + if (!inKnowledge (tb->know[u], tb->event[readEvent]->message)) + { + /* + printf("%% term["); + printf("]#%d is introduced at traceEvent[%d] ",readEvent,u); + printf("\n"); + */ + return u; + } + } + } + + return -1; } @@ -521,277 +572,305 @@ int latexCorrespondingSend2(struct tracebuf *tb, int readEvent) * Display knowledge in LaTeX format. */ -void knowledgePrintLatex(Knowledge know) +void +knowledgePrintLatex (Knowledge know) { - Termlist tl; + Termlist tl; - if (know == NULL) + if (know == NULL) { - printf("\\emptyset"); + printf ("\\emptyset"); } - else + else { - tl = knowledgeSet(know); - termlistPrint(tl); - termlistDelete(tl); + tl = knowledgeSet (know); + termlistPrint (tl); + termlistDelete (tl); } } -void attackDisplayLatex(System sys) +void +attackDisplayLatex (System sys) { - int i; - struct tracebuf *tb; - int *runPosition; - int currRun; - int position; - int eventSize; - Termlist tl; - Termlist newtl; - Termlist claimDetails; - Termlist highlights = NULL; - int cKnowledge; - int bestSend; + int i; + struct tracebuf *tb; + int *runPosition; + int currRun; + int position; + int eventSize; + Termlist tl; + Termlist newtl; + Termlist claimDetails; + Termlist highlights = NULL; + int cKnowledge; + int bestSend; - tb = sys->attack; - if (tb == NULL) { - printf("Attack pointer empty: nothing to display.\n"); - exit(1); - } - /* set variables */ - varbufSet (sys, tb->variables); - - /* Rebuild knowledge. Strange, this ought to be good. - * Maybe reconstruct dependencies as well. */ - tracebufRebuildKnow(tb); - - /* Make a comment in which the trace is displayed, for debugging etc. */ - printf("\n\\comment{ TRACE\n\n"); - printf("Length: %i\n",tb->length); - printf("Reallength: %i\n",tb->reallength); - printf("\n"); - i = 0; - while (i <= tb->length) + tb = sys->attack; + if (tb == NULL) { - printf("Knowledge %i:\n",i); - knowledgePrint(tb->know[i]); - printf(" [Inverses]: "); - knowledgeInversesPrint(tb->know[i]); - printf("\n\n"); - if (i < tb->length) + printf ("Attack pointer empty: nothing to display.\n"); + exit (1); + } + /* set variables */ + varbufSet (sys, tb->variables); + + /* Rebuild knowledge. Strange, this ought to be good. + * Maybe reconstruct dependencies as well. */ + tracebufRebuildKnow (tb); + + /* Make a comment in which the trace is displayed, for debugging etc. */ + printf ("\n\\comment{ TRACE\n\n"); + printf ("Length: %i\n", tb->length); + printf ("Reallength: %i\n", tb->reallength); + printf ("\n"); + i = 0; + while (i <= tb->length) + { + printf ("Knowledge %i:\n", i); + knowledgePrint (tb->know[i]); + printf (" [Inverses]: "); + knowledgeInversesPrint (tb->know[i]); + printf ("\n\n"); + if (i < tb->length) + { + printf ("Event %i\t[", i); + switch (tb->status[i]) + { + case S_UNK: + printf ("?"); + break; + case S_RED: + printf ("redundant"); + break; + case S_TOD: + printf ("to do"); + break; + case S_OKE: + printf ("okay"); + break; + default: + printf ("illegal status code"); + break; + } + printf ("]\t"); + termPrint (tb->event[i]->message); + printf ("\t#%i", tb->run[i]); + printf ("\n"); + roledefPrint (tb->event[i]); + printf ("\n\n"); + } + i++; + } + printf ("}\n\n"); + + /* display initial knowledge */ + printf ("$I_0 = \\emptyset \\oplus "); + knowledgePrintLatex (tb->know[0]); + printf ("$\n\n"); + + tinfo = + (struct traceinfo *) memAlloc ((tb->length + 1) * + sizeof (struct traceinfo)); + + width = 1; + for (i = 0; i < tb->length; i++) + { + if (tb->run[i] >= width) + width = tb->run[i] + 1; + } + + for (i = 0; i < tb->length; i++) + { + tb->link[i] = -1; + tinfo[i].match = -1; + tinfo[i].position = i; + } + tinfo[i].match = -1; + tinfo[i].position = i; + + runPosition = (int *) memAlloc (width * sizeof (int)); + for (i = 0; i < width; i++) + { + runPosition[i] = 0; + } + for (i = tb->length - 1; i >= 0; i--) + { + if (tb->status[i] != S_RED) + { + if (tb->event[i]->type == READ && !tb->event[i]->internal) + { + bestSend = latexCorrespondingSend2 (tb, i); + printf ("%% match: %d <-> %d\n", i, bestSend); + if (bestSend == -1) + continue; + + tb->link[i] = bestSend; + tb->link[bestSend] = i; + } + if (tb->event[i]->type == CLAIM) + { + claimDetails = + claimViolationDetails (sys, tb->run[i], tb->event[i], + tb->know[i]); + } + } + } + printf ("\\comment{ claimDetails :\n"); + termlistPrint (claimDetails); + printf ("\n}\n"); + + // landscape = (width > 4); // not for the time being + + position = 0; + currRun = 0; + eventSize = 0; + for (i = 0; i < tb->length; i++) + { + if (tb->status[i] != S_RED) + { + tinfo[i].position = position; + eventSize = 1; + currRun = tb->run[i]; + + switch (tb->event[i]->type) + { + case SEND: + position++; + tinfo[i].position++; + break; + case READ: + if (tb->link[i] != -1) { - printf("Event %i\t[",i); - switch (tb->status[i]) - { - case S_UNK: - printf("?"); - break; - case S_RED: - printf("redundant"); - break; - case S_TOD: - printf("to do"); - break; - case S_OKE: - printf("okay"); - break; - default: - printf("illegal status code"); - break; - } - printf("]\t"); - termPrint(tb->event[i]->message); - printf("\t#%i",tb->run[i]); - printf("\n"); - roledefPrint(tb->event[i]); - printf("\n\n"); + 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]]) + { + printf ("\\comment{\n"); + termPrint (tb->event[i]->message); + printf ("\n"); + termPrint (tb->event[tb->link[i]]->message); + printf ("\n"); + printf ("%% termDistance: %f\n", + termDistance (tb->event[i]->message, + tb->event[tb->link[i]]-> + message)); + printf ("}\n"); + tinfo[i].position = tinfo[tb->link[i]].position; + eventSize = 0; + } + } } - i++; - } - printf("}\n\n"); - - /* display initial knowledge */ - printf("$I_0 = \\emptyset \\oplus "); - knowledgePrintLatex(tb->know[0]); - printf("$\n\n"); - - tinfo = - (struct traceinfo *) memAlloc((tb->length+1) * - sizeof(struct traceinfo)); - - width = 1; - for (i = 0; i < tb->length; i++) { - if (tb->run[i] >= width) - width = tb->run[i] + 1; + if (tb->event[i]->internal) + { + eventSize = 0; + } + break; + case CLAIM: + if (claimDetails != NULL && claimDetails != (Termlist) - 1) + { + eventSize = 2; + } + else + { + eventSize = 0; + } + break; + default: + break; + } + if (!(tb->event[i]->type == READ && tb->event[i]->internal)) + runPosition[currRun] = tinfo[i].position + eventSize; + /* printf("%% Event %d at %d\n", i, position); */ + position += eventSize; + } } - for (i = 0; i < tb->length; i++) { - tb->link[i] = -1; - tinfo[i].match = -1; - tinfo[i].position = i; - } - tinfo[i].match = -1; - tinfo[i].position = i; - - runPosition = (int *) memAlloc(width * sizeof(int)); - for (i = 0; i < width; i++) { - runPosition[i] = 0; - } - for (i = tb->length - 1; i >= 0; i--) - { - if (tb->status[i] != S_RED) - { - if (tb->event[i]->type == READ && !tb->event[i]->internal) - { - bestSend = latexCorrespondingSend2(tb, i); - printf("%% match: %d <-> %d\n",i, bestSend); - if (bestSend == -1) - continue; - - tb->link[i] = bestSend; - tb->link[bestSend] = i; - } - if (tb->event[i]->type == CLAIM) - { - claimDetails = claimViolationDetails(sys, tb->run[i], tb->event[i], tb->know[i]); - } - } - } - printf("\\comment{ claimDetails :\n"); - termlistPrint(claimDetails); - printf("\n}\n"); - - // landscape = (width > 4); // not for the time being - - position = 0; - currRun = 0; - eventSize = 0; - for (i = 0; i < tb->length; i++) - { - if (tb->status[i] != S_RED) - { - tinfo[i].position = position; - eventSize = 1; - currRun = tb->run[i]; - - 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) - { - /* 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]]) - { - printf("\\comment{\n"); - termPrint(tb->event[i]->message); - printf("\n"); - termPrint(tb->event[tb->link[i]]->message); - printf("\n"); - printf("%% termDistance: %f\n", - termDistance(tb->event[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) { - eventSize = 0; - } - break; - case CLAIM: - if (claimDetails != NULL && claimDetails != (Termlist) -1) { - eventSize = 2; - } else { - eventSize = 0; - } - break; - default: - break; - } - if (!(tb->event[i]->type == READ && tb->event[i]->internal)) - runPosition[currRun] = tinfo[i].position + eventSize; - /* printf("%% Event %d at %d\n", i, position); */ - position += eventSize; - } - } - - latexMSCStart(); - for (i = 0; i < width; i++) { - if (runPosition[i] > 0) - latexDeclInst(sys, i); + latexMSCStart (); + for (i = 0; i < width; i++) + { + if (runPosition[i] > 0) + latexDeclInst (sys, i); } - //for (j=-1; j<=sys->step; j++) - position = 0; - cKnowledge = 0; - for (i = 0; i < tb->length; i++) - { - if (tb->status[i] != S_RED) - { - latexEventSpace(tinfo[i].position - position); - if (tinfo[i].position >= position) - { - position = tinfo[i].position; - } - switch (tb->event[i]->type) { - case SEND: - newtl = knowledgeNew(tb->know[i], tb->know[i + 1]); - highlights = NULL; - /* Build a Termlist of terms that from the claimViolationDetails, - that appear in the knowledge */ - if (newtl != NULL) - { - tl = claimDetails; - while (tl != NULL) - { - if (inTermlist(newtl, tl->term)) - { - highlights = termlistAdd(highlights, tl->term); - } - tl = tl->next; - } - printf("\\msccomment[4ex]{$I_%d=I_%d\\oplus ", cKnowledge + 1, - cKnowledge); - cKnowledge++; - latexTermlistPrint(newtl, highlights); - printf("$}{envright}\n"); - } + //for (j=-1; j<=sys->step; j++) + position = 0; + cKnowledge = 0; + for (i = 0; i < tb->length; i++) + { + if (tb->status[i] != S_RED) + { + latexEventSpace (tinfo[i].position - position); + if (tinfo[i].position >= position) + { + position = tinfo[i].position; + } + switch (tb->event[i]->type) + { + case SEND: + newtl = knowledgeNew (tb->know[i], tb->know[i + 1]); + highlights = NULL; + /* Build a Termlist of terms that from the claimViolationDetails, + that appear in the knowledge */ + if (newtl != NULL) + { + tl = claimDetails; + while (tl != NULL) + { + if (inTermlist (newtl, tl->term)) + { + highlights = termlistAdd (highlights, tl->term); + } + tl = tl->next; + } + 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) { - latexMessagePrintHighlight(tb, i, tb->link[i], highlights); - } else { - latexMessagePrintHighlight(tb, i, -1, highlights); //lost message - } - termlistDelete(highlights); + if (tb->link[i] != -1 && i < tb->length) + { + latexMessagePrintHighlight (tb, i, tb->link[i], highlights); + } + else + { + latexMessagePrintHighlight (tb, i, -1, highlights); //lost message + } + termlistDelete (highlights); - break; - case READ: - 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) { - latexClaim(tb, tb->run[i], claimDetails); - } - break; - default: - break; //kannie! - } - } + break; + case READ: + 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) + { + latexClaim (tb, tb->run[i], claimDetails); + } + break; + default: + break; //kannie! + } + } } - latexEventSpace(2); - latexMSCEnd(); - memFree(runPosition, width * sizeof(int)); - memFree(tinfo, (tb->length+1) * sizeof(struct traceinfo)); + latexEventSpace (2); + latexMSCEnd (); + memFree (runPosition, width * sizeof (int)); + memFree (tinfo, (tb->length + 1) * sizeof (struct traceinfo)); } diff --git a/src/output.c b/src/output.c index e6e1d8a..4c455ce 100644 --- a/src/output.c +++ b/src/output.c @@ -12,432 +12,481 @@ #include "latex.h" -void linePrint(int i) +void +linePrint (int i) { - indent(); - while (i > 0) { - printf("--------"); + indent (); + while (i > 0) + { + printf ("--------"); + i--; + } + printf ("\n"); +} + +int +correspondingSend (System sys, int rd) +{ + + int labelMatch = 0; + int toMatch = 0; + int fromMatch = 0; + int tofromMatch = 0; + int messageMatch = 0; + int nMatches = 0; + int maxNMatches = 0; + + int readEvent = rd; + int sendEvent = -1; + int bestSendEvent = -1; + + for (sendEvent = readEvent; sendEvent >= 0; sendEvent--) + { + if (sys->traceEvent[sendEvent]->type == SEND) + { + /* do all the different kind of matchings first */ + + labelMatch = + isTermEqualFn (sys->traceEvent[sendEvent]->label, + sys->traceEvent[readEvent]->label); + toMatch = + isTermEqualFn (sys->traceEvent[sendEvent]->to, + sys->traceEvent[readEvent]->to); + fromMatch = + isTermEqualFn (sys->traceEvent[sendEvent]->from, + sys->traceEvent[readEvent]->from); + tofromMatch = toMatch || fromMatch; + messageMatch = + isTermEqualFn (sys->traceEvent[sendEvent]->message, + sys->traceEvent[readEvent]->message); + + /* calculate the score */ + + nMatches = labelMatch + tofromMatch + messageMatch; + + if (nMatches == 3) + { + /* bingo! success on all matches */ + + //printf("Found perfect match: %d\n", s); + bestSendEvent = sendEvent; + break; + } + if (nMatches > maxNMatches) + { + /* if we found a better candidate than we already had, we'll update */ + + //printf("Comparing SEND #%d: ",s); + //if (labelMatch) printf("label "); + //if (toMatch) printf("to "); + //if (fromMatch) printf("from "); + //if (messageMatch) printf("message "); + //printf("\n"); + + /* however, we first want to be sure that at least some matches are successful */ + + if (labelMatch && messageMatch) + { + /* strongest restriction: message and label should match */ + + maxNMatches = nMatches; + bestSendEvent = sendEvent; + + } + else if (messageMatch) + { + /* if label AND message don't match: */ + /* at least message should match */ + + maxNMatches = nMatches; + bestSendEvent = sendEvent; + } + else if (labelMatch) + { + /* if message doesn't match */ + /* the label should matches */ + + maxNMatches = nMatches; + bestSendEvent = sendEvent; + } + //printf("Best match: %d maxNMatches: %d\n", s, maxNMatches); + } + } + } + + //bestSendEvent = NULL; + if (bestSendEvent == -1) + { + /*Termlist tl; + Term t; + + //newtl = knowledgeNew(sys->traceKnow[i],sys->traceKnow[i+1]); + + for (tl = sys->traceKnow[rd]->basic; tl != NULL; tl = tl->next) + { + t = tl->term; + termPrint(t); + printf(" - "); + } + printf("\n"); + for (tl = sys->traceKnow[rd]->encrypt; tl != NULL; tl = tl->next) + { + t = tl->term; + termPrint(t); + printf(" - "); + } + printf("\n"); + for (tl = sys->traceKnow[rd]->inverses; tl != NULL; tl = tl->next) + { + t = tl->term; + termPrint(t); + printf(" - "); + } + printf("\n"); */ + + int u; + + for (u = 0; u < rd; u++) + { + if (sys->traceEvent[u]->type == SEND) + { + + + //termPrint(readEvent->message); + //printf("\n"); + knowledgePrint (sys->traceKnow[u]); + //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)) + { + bestSendEvent = u; + break; + } + } + } + } + + if (bestSendEvent == -1) + { + printf ("!! Could not find a matching SEND\n"); + } + else + { + //latexMessagePrint(sys, bestSendEvent, readEvent); + //printf("Latex: "); + //termPrint(bestSendEvent->from); + //printf(" -> "); + if (!isTermEqualFn + (sys->traceEvent[bestSendEvent]->to, + sys->traceEvent[readEvent]->to)) + { + //termPrint(bestSendEvent->to); + //printf(" -> "); + } + if (!isTermEqualFn + (sys->traceEvent[bestSendEvent]->from, + sys->traceEvent[readEvent]->from)) + { + //termPrint(readEvent->from); + //printf(" -> "); + } + //termPrint(readEvent->to); + //printf("\n"); + } + return bestSendEvent; +} + +void +tracePrint (System sys) +{ + if (sys->latex) + { + //latexTracePrint(sys); + return; + } + + int i, j; + int lastrid; + int width; + Termlist newtl; + + /* fix the 'next' knowledge, this is required because sometimes + * when calling this function, the next knowledge is not stored + * yet, but required for the general form of the output . */ + + sys->traceKnow[sys->step + 1] = sys->know; + + + /* how wide is the trace? */ + width = 0; + for (i = 0; i <= sys->step; i++) + { + if (sys->traceRun[i] >= width) + width = sys->traceRun[i] + 1; + } + + linePrint (width); + indent (); + printf ("Dumping trace:\n"); + linePrint (width); + + /* first some parameter issues */ + + knowledgePrint (sys->traceKnow[0]); + /* also print inverses */ + indent (); + printf ("Inverses: "); + knowledgeInversesPrint (sys->traceKnow[0]); + printf ("\n"); + + /* Trace columns header. First the run identifier and role. On the + * second line we have the perceived agents for each partner role. + * These are printed in the same order as the role specification in the + * protocol. */ + + linePrint (width); + indent (); + + for (i = 0; i < width; i++) + { + termPrint (sys->runs[i].role->nameterm); + printf ("#%i\t", i); + } + printf ("\n"); + for (i = 0; i < width; i++) + { + termPrint (agentOfRun (sys, i)); + printf ("\t"); + } + printf ("\n"); + + for (i = 0; i < width; i++) + { + agentsOfRunPrint (sys, i); + printf ("\t"); + } + printf ("\n"); + + /* now we print the actual trace */ + + void sticks (int i) + { + while (i > 0) + { + printf ("|\t"); i--; - } - printf("\n"); -} + } + } -int correspondingSend(System sys, int rd) -{ - - int labelMatch = 0; - int toMatch = 0; - int fromMatch = 0; - int tofromMatch = 0; - int messageMatch = 0; - int nMatches = 0; - int maxNMatches = 0; - - int readEvent = rd; - int sendEvent = -1; - int bestSendEvent = -1; - - for (sendEvent = readEvent; sendEvent >= 0; sendEvent--) { - if (sys->traceEvent[sendEvent]->type == SEND) { - /* do all the different kind of matchings first */ - - labelMatch = - isTermEqualFn(sys->traceEvent[sendEvent]->label, - sys->traceEvent[readEvent]->label); - toMatch = - isTermEqualFn(sys->traceEvent[sendEvent]->to, - sys->traceEvent[readEvent]->to); - fromMatch = - isTermEqualFn(sys->traceEvent[sendEvent]->from, - sys->traceEvent[readEvent]->from); - tofromMatch = toMatch || fromMatch; - messageMatch = - isTermEqualFn(sys->traceEvent[sendEvent]->message, - sys->traceEvent[readEvent]->message); - - /* calculate the score */ - - nMatches = labelMatch + tofromMatch + messageMatch; - - if (nMatches == 3) { - /* bingo! success on all matches */ - - //printf("Found perfect match: %d\n", s); - bestSendEvent = sendEvent; - break; - } - if (nMatches > maxNMatches) { - /* if we found a better candidate than we already had, we'll update */ - - //printf("Comparing SEND #%d: ",s); - //if (labelMatch) printf("label "); - //if (toMatch) printf("to "); - //if (fromMatch) printf("from "); - //if (messageMatch) printf("message "); - //printf("\n"); - - /* however, we first want to be sure that at least some matches are successful */ - - if (labelMatch && messageMatch) { - /* strongest restriction: message and label should match */ - - maxNMatches = nMatches; - bestSendEvent = sendEvent; - - } else if (messageMatch) { - /* if label AND message don't match: */ - /* at least message should match */ - - maxNMatches = nMatches; - bestSendEvent = sendEvent; - } else if (labelMatch) { - /* if message doesn't match */ - /* the label should matches */ - - maxNMatches = nMatches; - bestSendEvent = sendEvent; - } - //printf("Best match: %d maxNMatches: %d\n", s, maxNMatches); - } - } - } - - //bestSendEvent = NULL; - if (bestSendEvent == -1) { - /*Termlist tl; - Term t; - - //newtl = knowledgeNew(sys->traceKnow[i],sys->traceKnow[i+1]); - - for (tl = sys->traceKnow[rd]->basic; tl != NULL; tl = tl->next) - { - t = tl->term; - termPrint(t); - printf(" - "); - } - printf("\n"); - for (tl = sys->traceKnow[rd]->encrypt; tl != NULL; tl = tl->next) - { - t = tl->term; - termPrint(t); - printf(" - "); - } - printf("\n"); - for (tl = sys->traceKnow[rd]->inverses; tl != NULL; tl = tl->next) - { - t = tl->term; - termPrint(t); - printf(" - "); - } - printf("\n"); */ - - int u; - - for (u = 0; u < rd; u++) { - if (sys->traceEvent[u]->type == SEND) { - - - //termPrint(readEvent->message); - //printf("\n"); - knowledgePrint(sys->traceKnow[u]); - //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)) { - bestSendEvent = u; - break; - } - } - } - } - - if (bestSendEvent == -1) { - printf("!! Could not find a matching SEND\n"); - } else { - //latexMessagePrint(sys, bestSendEvent, readEvent); - //printf("Latex: "); - //termPrint(bestSendEvent->from); - //printf(" -> "); - if (!isTermEqualFn - (sys->traceEvent[bestSendEvent]->to, - sys->traceEvent[readEvent]->to)) { - //termPrint(bestSendEvent->to); - //printf(" -> "); - } - if (!isTermEqualFn - (sys->traceEvent[bestSendEvent]->from, - sys->traceEvent[readEvent]->from)) { - //termPrint(readEvent->from); - //printf(" -> "); - } - //termPrint(readEvent->to); - //printf("\n"); - } - return bestSendEvent; -} - -void tracePrint(System sys) -{ - if (sys->latex) { - //latexTracePrint(sys); - return; - } - - int i, j; - int lastrid; - int width; - Termlist newtl; - - /* fix the 'next' knowledge, this is required because sometimes - * when calling this function, the next knowledge is not stored - * yet, but required for the general form of the output . */ - - sys->traceKnow[sys->step + 1] = sys->know; - - - /* how wide is the trace? */ - width = 0; - for (i = 0; i <= sys->step; i++) { - if (sys->traceRun[i] >= width) - width = sys->traceRun[i] + 1; - } - - linePrint(width); - indent(); - printf("Dumping trace:\n"); - linePrint(width); - - /* first some parameter issues */ - - knowledgePrint(sys->traceKnow[0]); - /* also print inverses */ - indent(); - printf("Inverses: "); - knowledgeInversesPrint(sys->traceKnow[0]); - printf("\n"); - - /* Trace columns header. First the run identifier and role. On the - * second line we have the perceived agents for each partner role. - * These are printed in the same order as the role specification in the - * protocol. */ - - linePrint(width); - indent(); - - for (i = 0; i < width; i++) { - termPrint(sys->runs[i].role->nameterm); - printf("#%i\t", i); - } - printf("\n"); - for (i = 0; i < width; i++) { - termPrint(agentOfRun(sys, i)); - printf("\t"); - } - printf("\n"); - - for (i = 0; i < width; i++) { - agentsOfRunPrint(sys, i); - printf("\t"); - } - printf("\n"); - - /* now we print the actual trace */ - - void sticks(int i) { - while (i > 0) { - printf("|\t"); - i--; - } - } - - void sticksLine(void) { - sticks(width); - printf("\n"); - } - - linePrint(width); - lastrid = -1; - for (i = 0; i <= sys->step; i++) { - /* yields extra newlines between switching of runs */ - - j = sys->traceRun[i]; - if (j != lastrid) { - sticksLine(); - lastrid = j; - } - - /* print the actual event */ - - indent(); - sticks(j); - roledefPrint(sys->traceEvent[i]); - - //if (sys->traceEvent[i]->type == READ && !sys->traceEvent[i]->internal) - //{ - /* calls routine to find the best SEND-candidate */ - /* the result is not yet being used */ - - // printf("\n"); - // correspondingSend(sys, i); - //} - - /* have we learnt anything new? */ - newtl = knowledgeNew(sys->traceKnow[i], sys->traceKnow[i + 1]); - if (newtl != NULL) { - printf("\n"); - sticksLine(); - sticks(width); - printf("/* Intruder learns "); - termlistPrint(newtl); - termlistDelete(newtl); - printf(" */"); - lastrid = -1; - } - - /* new line */ - printf("\n"); - } - - switch (sys->clp) { - case 1: - indent(); - printf("---[ constraints ]-----\n"); - constraintlistPrint(sys->constraints); - break; - default: - break; - } - linePrint(width); -} - - - -void attackDisplayAscii(System sys) -{ - int i, j; - int length; - int lastrid; - int width; - Termlist newtl; - struct tracebuf *tb; - - /* attack trace buffer */ - tb = sys->attack; - length = sys->attack->length; - - /* set variables */ - varbufSet (sys, tb->variables); - - /* how wide is the trace? */ - width = 0; - for (i = 0; i < length; i++) { - if (tb->run[i] >= width) - width = tb->run[i] + 1; - } - - linePrint(width); - indent(); - printf("Dumping trace:\n"); - linePrint(width); - - /* first some parameter issues */ - - knowledgePrint(tb->know[0]); - printf ("Variables: "); - termlistPrint (sys->variables); + void sticksLine (void) + { + sticks (width); printf ("\n"); + } - /* Trace columns header. First the run identifier and role. On the - * second line we have the perceived agents for each partner role. - * These are printed in the same order as the role specification in the - * protocol. */ + linePrint (width); + lastrid = -1; + for (i = 0; i <= sys->step; i++) + { + /* yields extra newlines between switching of runs */ - linePrint(width); - indent(); - - for (i = 0; i < width; i++) { - termPrint(sys->runs[i].role->nameterm); - printf("#%i\t", i); - } - printf("\n"); - for (i = 0; i < width; i++) { - termPrint(agentOfRun(sys, i)); - printf("\t"); - } - printf("\n"); - - for (i = 0; i < width; i++) { - agentsOfRunPrint(sys, i); - printf("\t"); - } - printf("\n"); - - /* now we print the actual trace */ - - void sticks(int i) { - while (i > 0) { - printf("|\t"); - i--; - } - } - - void sticksLine(void) { - sticks(width); - printf("\n"); - } - - linePrint(width); - lastrid = -1; - for (i = 0; i < length; i++) { - /* yields extra newlines between switching of runs */ - - j = tb->run[i]; - if (j != lastrid) { - sticksLine(); - lastrid = j; + j = sys->traceRun[i]; + if (j != lastrid) + { + sticksLine (); + lastrid = j; } - /* print the actual event */ + /* print the actual event */ - indent(); - sticks(j); - roledefPrint(tb->event[i]); + indent (); + sticks (j); + roledefPrint (sys->traceEvent[i]); - //if (sys->traceEvent[i]->type == READ && !sys->traceEvent[i]->internal) - //{ - /* calls routine to find the best SEND-candidate */ - /* the result is not yet being used */ + //if (sys->traceEvent[i]->type == READ && !sys->traceEvent[i]->internal) + //{ + /* calls routine to find the best SEND-candidate */ + /* the result is not yet being used */ - // printf("\n"); - // correspondingSend(sys, i); - //} + // printf("\n"); + // correspondingSend(sys, i); + //} - /* have we learnt anything new? */ - newtl = knowledgeNew(tb->know[i], tb->know[i + 1]); - if (newtl != NULL) { - printf("\n"); - sticksLine(); - sticks(width); - printf("/* Intruder learns "); - termlistPrint(newtl); - termlistDelete(newtl); - printf(" */"); - lastrid = -1; + /* have we learnt anything new? */ + newtl = knowledgeNew (sys->traceKnow[i], sys->traceKnow[i + 1]); + if (newtl != NULL) + { + printf ("\n"); + sticksLine (); + sticks (width); + printf ("/* Intruder learns "); + termlistPrint (newtl); + termlistDelete (newtl); + printf (" */"); + lastrid = -1; } - /* new line */ - printf("\n"); + /* new line */ + printf ("\n"); } - linePrint(width); + switch (sys->clp) + { + case 1: + indent (); + printf ("---[ constraints ]-----\n"); + constraintlistPrint (sys->constraints); + break; + default: + break; + } + linePrint (width); } -void attackDisplay(System sys) + +void +attackDisplayAscii (System sys) { - if (sys->latex) { - attackDisplayLatex(sys); - } else { - attackDisplayAscii(sys); + int i, j; + int length; + int lastrid; + int width; + Termlist newtl; + struct tracebuf *tb; + + /* attack trace buffer */ + tb = sys->attack; + length = sys->attack->length; + + /* set variables */ + varbufSet (sys, tb->variables); + + /* how wide is the trace? */ + width = 0; + for (i = 0; i < length; i++) + { + if (tb->run[i] >= width) + width = tb->run[i] + 1; + } + + linePrint (width); + indent (); + printf ("Dumping trace:\n"); + linePrint (width); + + /* first some parameter issues */ + + knowledgePrint (tb->know[0]); + printf ("Variables: "); + termlistPrint (sys->variables); + printf ("\n"); + + /* Trace columns header. First the run identifier and role. On the + * second line we have the perceived agents for each partner role. + * These are printed in the same order as the role specification in the + * protocol. */ + + linePrint (width); + indent (); + + for (i = 0; i < width; i++) + { + termPrint (sys->runs[i].role->nameterm); + printf ("#%i\t", i); + } + printf ("\n"); + for (i = 0; i < width; i++) + { + termPrint (agentOfRun (sys, i)); + printf ("\t"); + } + printf ("\n"); + + for (i = 0; i < width; i++) + { + agentsOfRunPrint (sys, i); + printf ("\t"); + } + printf ("\n"); + + /* now we print the actual trace */ + + void sticks (int i) + { + while (i > 0) + { + printf ("|\t"); + i--; + } + } + + void sticksLine (void) + { + sticks (width); + printf ("\n"); + } + + linePrint (width); + lastrid = -1; + for (i = 0; i < length; i++) + { + /* yields extra newlines between switching of runs */ + + j = tb->run[i]; + if (j != lastrid) + { + sticksLine (); + lastrid = j; + } + + /* print the actual event */ + + indent (); + sticks (j); + roledefPrint (tb->event[i]); + + //if (sys->traceEvent[i]->type == READ && !sys->traceEvent[i]->internal) + //{ + /* calls routine to find the best SEND-candidate */ + /* the result is not yet being used */ + + // printf("\n"); + // correspondingSend(sys, i); + //} + + /* have we learnt anything new? */ + newtl = knowledgeNew (tb->know[i], tb->know[i + 1]); + if (newtl != NULL) + { + printf ("\n"); + sticksLine (); + sticks (width); + printf ("/* Intruder learns "); + termlistPrint (newtl); + termlistDelete (newtl); + printf (" */"); + lastrid = -1; + } + + /* new line */ + printf ("\n"); + } + + linePrint (width); +} + + +void +attackDisplay (System sys) +{ + if (sys->latex) + { + attackDisplayLatex (sys); + } + else + { + attackDisplayAscii (sys); } }