- Template cleanup for latex.

- Timers output now to stderr. Previously this was stdout/latex.
This commit is contained in:
ccremers 2004-05-21 12:32:57 +00:00
parent 8b41f5806d
commit 10f95a55a6
4 changed files with 17 additions and 83 deletions

View File

@ -51,6 +51,9 @@
\setlength{\maxmscaction}{\mscspacer} \setlength{\maxmscaction}{\mscspacer}
\setlength{\maxmsccondition}{\mscspacer} \setlength{\maxmsccondition}{\mscspacer}
% pagestyle without numbering
\pagestyle{empty}
\begin{document} \begin{document}
\input{attack} \input{attack}

View File

@ -214,75 +214,13 @@ latexTermlistPrint (Termlist tl, Termlist highlight)
} }
//! Display the timers and states traversed using LaTeX. //! Display the timers and states traversed using LaTeX.
/**
* Obsolete: we will now only print timers on stderr.
*/
void void
latexTimers (const System sys) 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");
} }
//! Start drawing MSC environment. //! Start drawing MSC environment.

View File

@ -409,18 +409,18 @@ timersPrint (const System sys)
{ {
/* display stats, header first */ /* 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 */ /* print time */
double seconds; double seconds;
seconds = (double) clock () / CLOCKS_PER_SEC; seconds = (double) clock () / CLOCKS_PER_SEC;
printf ("%.3e\t", seconds); fprintf (stderr, "%.3e\t", seconds);
/* states traversed */ /* states traversed */
statesPrintShort (sys); statesPrintShort (sys);
printf ("\t"); fprintf (stderr, "\t");
/* flag /* flag
* *
@ -431,14 +431,14 @@ timersPrint (const System sys)
if (sys->claims == 0) if (sys->claims == 0)
{ {
printf ("NoClaim\t\t"); fprintf (stderr, "NoClaim\t\t");
} }
else else
{ {
if (sys->failed > 0) if (sys->failed > 0)
printf ("L:%i\t\t", attackLength(sys->attack)); fprintf (stderr, "L:%i\t\t", attackLength(sys->attack));
else else
printf ("None\t\t"); fprintf (stderr, "None\t\t");
} }
/* /*
@ -452,16 +452,16 @@ timersPrint (const System sys)
if (seconds > 0) if (seconds > 0)
{ {
printf ("%.3e\t", fprintf (stderr, "%.3e\t",
(double) (sys->statesLow + (double) (sys->statesLow +
(sys->statesHigh * ULONG_MAX)) / seconds); (sys->statesHigh * ULONG_MAX)) / seconds);
} }
else else
{ {
printf ("<inf>\t\t"); fprintf (stderr, "<inf>\t\t");
} }
printf ("\n"); fprintf (stderr, "\n");
} }
//! Analyse the model by incremental runs. //! Analyse the model by incremental runs.
@ -585,13 +585,6 @@ int
modelCheck (const System sys) modelCheck (const System sys)
{ {
traverse (sys); // start model checking traverse (sys); // start model checking
if (sys->latex)
{
latexTimers (sys);
}
else
{
timersPrint (sys); timersPrint (sys);
}
return (sys->failed); return (sys->failed);
} }

View File

@ -166,7 +166,7 @@ statesApproximation (System sys)
void void
statesPrintShort (System sys) statesPrintShort (System sys)
{ {
printf ("%.3e", statesApproximation (sys)); fprintf (stderr,"%.3e", statesApproximation (sys));
} }
//! Print the number of states. //! Print the number of states.