798 lines
17 KiB
C
798 lines
17 KiB
C
|
/*
|
||
|
|
* LaTeX output component
|
||
|
|
*/
|
||
|
|
|
||
|
|
#include <stdio.h>
|
||
|
|
#include <stdlib.h>
|
||
|
|
#include <time.h>
|
||
|
|
#include <limits.h>
|
||
|
|
#include "runs.h"
|
||
|
|
#include "memory.h"
|
||
|
|
#include "modelchecker.h"
|
||
|
|
#include "tracebuf.h"
|
||
|
|
#include "varbuf.h"
|
||
|
|
#include "output.h"
|
||
|
|
|
||
|
|
#define EVENTSPACE 1
|
||
|
|
#define LINKTHRESHOLD 0.95
|
||
|
|
|
||
|
|
extern const char *progname;
|
||
|
|
extern const char *releasetag;
|
||
|
|
extern int globalLatex;
|
||
|
|
extern Term TERM_Function;
|
||
|
|
|
||
|
|
/* struct for additional info */
|
||
|
|
|
||
|
|
struct traceinfo {
|
||
|
|
int match;
|
||
|
|
int position;
|
||
|
|
};
|
||
|
|
|
||
|
|
/* global variables for this module */
|
||
|
|
|
||
|
|
struct traceinfo *tinfo;
|
||
|
|
int width;
|
||
|
|
int landscape = 0;
|
||
|
|
int *runPerm;
|
||
|
|
|
||
|
|
/* code */
|
||
|
|
|
||
|
|
void latexInit(const System sys, int argc, char **argv)
|
||
|
|
{
|
||
|
|
int i;
|
||
|
|
|
||
|
|
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");
|
||
|
|
|
||
|
|
printf("%%\n");
|
||
|
|
printf("\\begin{document}\n\n");
|
||
|
|
|
||
|
|
/* comment macro (used for debugging) */
|
||
|
|
printf("\\newcommand{\\comment}[1]{}\n");
|
||
|
|
|
||
|
|
/* preamble */
|
||
|
|
printf("\\input{preamble}\n");
|
||
|
|
}
|
||
|
|
|
||
|
|
void latexDone(const System sys)
|
||
|
|
{
|
||
|
|
printf("\\input{postamble}\n");
|
||
|
|
printf("\n\\end{document}\n\n");
|
||
|
|
}
|
||
|
|
|
||
|
|
void
|
||
|
|
latexTermPrint (Term term, Termlist highlight)
|
||
|
|
{
|
||
|
|
if (term == NULL)
|
||
|
|
{
|
||
|
|
printf ("Empty term");
|
||
|
|
return;
|
||
|
|
}
|
||
|
|
#ifdef DEBUG
|
||
|
|
if (!DEBUGL (1))
|
||
|
|
{
|
||
|
|
term = deVar (term);
|
||
|
|
}
|
||
|
|
#else
|
||
|
|
term = deVar (term);
|
||
|
|
#endif
|
||
|
|
if (realTermLeaf (term))
|
||
|
|
{
|
||
|
|
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("}");
|
||
|
|
}
|
||
|
|
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))
|
||
|
|
{
|
||
|
|
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 ("}");
|
||
|
|
}
|
||
|
|
}
|
||
|
|
}
|
||
|
|
|
||
|
|
void
|
||
|
|
latexTermlistPrint (Termlist tl, Termlist highlight)
|
||
|
|
{
|
||
|
|
if (tl == NULL)
|
||
|
|
{
|
||
|
|
printf ("[Empty]");
|
||
|
|
return;
|
||
|
|
}
|
||
|
|
printf ("[");
|
||
|
|
while (tl != NULL)
|
||
|
|
{
|
||
|
|
latexTermPrint (tl->term, highlight);
|
||
|
|
tl = tl->next;
|
||
|
|
if (tl != NULL)
|
||
|
|
printf(", ");
|
||
|
|
}
|
||
|
|
printf ("]");
|
||
|
|
}
|
||
|
|
|
||
|
|
void latexTimers(const System sys)
|
||
|
|
{
|
||
|
|
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 <n>
|
||
|
|
* 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("%.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$ ");
|
||
|
|
}
|
||
|
|
endline();
|
||
|
|
|
||
|
|
printf("\\end{tabular}\n\n");
|
||
|
|
}
|
||
|
|
|
||
|
|
void latexMSCStart()
|
||
|
|
{
|
||
|
|
if (landscape)
|
||
|
|
printf("\\begin{landscape}\n");
|
||
|
|
|
||
|
|
printf("\\begin{msc}{attack}\n");
|
||
|
|
}
|
||
|
|
|
||
|
|
void latexMSCEnd()
|
||
|
|
{
|
||
|
|
printf("\\end{msc}\n");
|
||
|
|
|
||
|
|
if (landscape)
|
||
|
|
printf("\\end{landscape}\n");
|
||
|
|
|
||
|
|
}
|
||
|
|
|
||
|
|
void latexDeclInst(const System sys, int run)
|
||
|
|
{
|
||
|
|
Term bar = NULL;
|
||
|
|
|
||
|
|
bar = agentOfRun(sys, run);
|
||
|
|
printf("\\declinst{run%d}{$", run);
|
||
|
|
termPrint(bar);
|
||
|
|
printf("\\sharp%i$}{$", run);
|
||
|
|
agentsOfRunPrint(sys, run);
|
||
|
|
printf("$}\n");
|
||
|
|
}
|
||
|
|
|
||
|
|
void latexEventSpace(int amount)
|
||
|
|
{
|
||
|
|
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)
|
||
|
|
{
|
||
|
|
|
||
|
|
Term sendTerm = NULL;
|
||
|
|
Term readTerm = NULL;
|
||
|
|
|
||
|
|
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);
|
||
|
|
}
|
||
|
|
|
||
|
|
printf("$}{run%d", tb->run[from]);
|
||
|
|
printf("}{run%d}[%d]", tb->run[to],
|
||
|
|
EVENTSPACE * (tinfo[to].position -
|
||
|
|
tinfo[from].position));
|
||
|
|
|
||
|
|
printf("\n");
|
||
|
|
}
|
||
|
|
}
|
||
|
|
void latexMessagePrintHighlight(struct tracebuf *tb, int from, int to, Termlist highlight)
|
||
|
|
{
|
||
|
|
|
||
|
|
Term sendTerm = NULL;
|
||
|
|
Term readTerm = NULL;
|
||
|
|
|
||
|
|
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);
|
||
|
|
}
|
||
|
|
|
||
|
|
printf("$}{run%d", tb->run[from]);
|
||
|
|
printf("}{run%d}[%d]", tb->run[to],
|
||
|
|
EVENTSPACE * (tinfo[to].position -
|
||
|
|
tinfo[from].position));
|
||
|
|
|
||
|
|
printf("\n");
|
||
|
|
}
|
||
|
|
}
|
||
|
|
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");
|
||
|
|
}
|
||
|
|
|
||
|
|
void latexAction(struct tracebuf *tb, int te)
|
||
|
|
{
|
||
|
|
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)
|
||
|
|
{
|
||
|
|
printf("\\condition{$");
|
||
|
|
printf("\\neg secret ");
|
||
|
|
termlistPrint(tl);
|
||
|
|
printf("$}{run%d}\n", run);
|
||
|
|
}
|
||
|
|
|
||
|
|
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 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 */
|
||
|
|
|
||
|
|
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 */
|
||
|
|
|
||
|
|
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 (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;
|
||
|
|
}
|
||
|
|
}
|
||
|
|
}
|
||
|
|
}
|
||
|
|
|
||
|
|
//bestSendEvent = NULL;
|
||
|
|
if (bestSendEvent == -1) {
|
||
|
|
|
||
|
|
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;
|
||
|
|
}
|
||
|
|
}
|
||
|
|
}
|
||
|
|
}
|
||
|
|
|
||
|
|
if (bestSendEvent == -1) {
|
||
|
|
printf("%% Could not find a matching SEND\n");
|
||
|
|
}
|
||
|
|
return bestSendEvent;
|
||
|
|
}
|
||
|
|
|
||
|
|
|
||
|
|
int
|
||
|
|
newInKnowledge (const Knowledge know, Term term)
|
||
|
|
{
|
||
|
|
/* if there is no term, then it's okay 'fur sure' */
|
||
|
|
if (term == NULL)
|
||
|
|
return 1;
|
||
|
|
/* if there is a term, but no knowledge, we're in trouble */
|
||
|
|
if (know == NULL)
|
||
|
|
return 0;
|
||
|
|
|
||
|
|
mindwipe (know, inKnowledge (know, term));
|
||
|
|
|
||
|
|
term = deVar (term);
|
||
|
|
if (isTermLeaf (term))
|
||
|
|
{
|
||
|
|
return inTermlist (know->basic, term);
|
||
|
|
}
|
||
|
|
if (term->type == ENCRYPT)
|
||
|
|
{
|
||
|
|
return inTermlist (know->encrypt, term) ||
|
||
|
|
(inKnowledge (know, term->key) || inKnowledge (know, term->op));
|
||
|
|
}
|
||
|
|
if (term->type == TUPLE)
|
||
|
|
{
|
||
|
|
return (inTermlist (know->encrypt, term) ||
|
||
|
|
(inKnowledge (know, term->op1) ||
|
||
|
|
inKnowledge (know, term->op2)));
|
||
|
|
}
|
||
|
|
return 0; /* unrecognized term type, weird */
|
||
|
|
}
|
||
|
|
|
||
|
|
int latexCorrespondingSend2(struct tracebuf *tb, int readEvent)
|
||
|
|
{
|
||
|
|
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;
|
||
|
|
|
||
|
|
}
|
||
|
|
|
||
|
|
/*
|
||
|
|
* Display knowledge in LaTeX format.
|
||
|
|
*/
|
||
|
|
|
||
|
|
void knowledgePrintLatex(Knowledge know)
|
||
|
|
{
|
||
|
|
Termlist tl;
|
||
|
|
|
||
|
|
if (know == NULL)
|
||
|
|
{
|
||
|
|
printf("\\emptyset");
|
||
|
|
}
|
||
|
|
else
|
||
|
|
{
|
||
|
|
tl = knowledgeSet(know);
|
||
|
|
termlistPrint(tl);
|
||
|
|
termlistDelete(tl);
|
||
|
|
}
|
||
|
|
}
|
||
|
|
|
||
|
|
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;
|
||
|
|
|
||
|
|
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)
|
||
|
|
{
|
||
|
|
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) {
|
||
|
|
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);
|
||
|
|
}
|
||
|
|
|
||
|
|
//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);
|
||
|
|
|
||
|
|
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));
|
||
|
|
}
|