diff --git a/src/attacktemplate.tex b/src/attacktemplate.tex index f068ad0..623c282 100644 --- a/src/attacktemplate.tex +++ b/src/attacktemplate.tex @@ -51,6 +51,9 @@ \setlength{\maxmscaction}{\mscspacer} \setlength{\maxmsccondition}{\mscspacer} +% pagestyle without numbering +\pagestyle{empty} + \begin{document} \input{attack} diff --git a/src/latex.c b/src/latex.c index 5f362d9..9dde12e 100644 --- a/src/latex.c +++ b/src/latex.c @@ -214,75 +214,13 @@ latexTermlistPrint (Termlist tl, Termlist highlight) } //! Display the timers and states traversed using LaTeX. +/** + * Obsolete: we will now only print timers on stderr. + */ 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 - * 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"); } //! Start drawing MSC environment. diff --git a/src/main.c b/src/main.c index ae2e6e4..c352ed4 100644 --- a/src/main.c +++ b/src/main.c @@ -409,18 +409,18 @@ timersPrint (const System sys) { /* display stats, header first */ - printf ("Time\t\tStates\t\tAttack\t\tst/sec\n"); + fprintf (stderr, "Time\t\tStates\t\tAttack\t\tst/sec\n"); /* print time */ double seconds; seconds = (double) clock () / CLOCKS_PER_SEC; - printf ("%.3e\t", seconds); + fprintf (stderr, "%.3e\t", seconds); /* states traversed */ statesPrintShort (sys); - printf ("\t"); + fprintf (stderr, "\t"); /* flag * @@ -431,14 +431,14 @@ timersPrint (const System sys) if (sys->claims == 0) { - printf ("NoClaim\t\t"); + fprintf (stderr, "NoClaim\t\t"); } else { if (sys->failed > 0) - printf ("L:%i\t\t", attackLength(sys->attack)); + fprintf (stderr, "L:%i\t\t", attackLength(sys->attack)); else - printf ("None\t\t"); + fprintf (stderr, "None\t\t"); } /* @@ -452,16 +452,16 @@ timersPrint (const System sys) if (seconds > 0) { - printf ("%.3e\t", + fprintf (stderr, "%.3e\t", (double) (sys->statesLow + (sys->statesHigh * ULONG_MAX)) / seconds); } else { - printf ("\t\t"); + fprintf (stderr, "\t\t"); } - printf ("\n"); + fprintf (stderr, "\n"); } //! Analyse the model by incremental runs. @@ -585,13 +585,6 @@ int modelCheck (const System sys) { traverse (sys); // start model checking - if (sys->latex) - { - latexTimers (sys); - } - else - { - timersPrint (sys); - } + timersPrint (sys); return (sys->failed); } diff --git a/src/runs.c b/src/runs.c index 2c103d0..61a04e6 100644 --- a/src/runs.c +++ b/src/runs.c @@ -166,7 +166,7 @@ statesApproximation (System sys) void statesPrintShort (System sys) { - printf ("%.3e", statesApproximation (sys)); + fprintf (stderr,"%.3e", statesApproximation (sys)); } //! Print the number of states.