From dda2907492a059e3a750f414a1750952824b939d Mon Sep 17 00:00:00 2001 From: ccremers Date: Thu, 29 Jul 2004 10:13:13 +0000 Subject: [PATCH] - Implemented output method selector, sys->output. - Changed disable-report switch into --empty. - --scenario=-1 now displays a list of scenarios. Use wc -l to count them. --- src/main.c | 80 +++++++++++++++++++++++++++++++--------------- src/modelchecker.c | 14 ++++---- src/output.c | 3 -- src/report.c | 2 +- src/system.c | 3 +- src/system.h | 4 ++- 6 files changed, 66 insertions(+), 40 deletions(-) diff --git a/src/main.c b/src/main.c index df36682..b59be9f 100644 --- a/src/main.c +++ b/src/main.c @@ -102,8 +102,8 @@ main (int argc, char **argv) struct arg_lit *switch_incremental_runs = arg_lit0 (NULL, "increment-runs", "incremental search using the number of runs"); struct arg_lit *switch_latex_output = arg_lit0 (NULL, "latex", "output in LaTeX format"); - struct arg_lit *switch_disable_violations_report = - arg_lit0 ("d", "disable-report", "don't report violations"); + struct arg_lit *switch_empty = + arg_lit0 ("e", "empty", "do not generate output"); struct arg_lit *switch_no_progress_bar = arg_lit0 (NULL, "no-progress", "suppress progress bar"); struct arg_lit *switch_state_space_graph = arg_lit0 (NULL, "state-space", "output state space graph"); struct arg_lit *switch_implicit_choose = arg_lit0 (NULL, "implicit-choose", "allow implicit choose events (useful for few runs)"); @@ -135,7 +135,7 @@ main (int argc, char **argv) switch_prune_trace_length, switch_incremental_trace_length, switch_maximum_runs, switch_incremental_runs, switch_latex_output, - switch_disable_violations_report, + switch_empty, switch_no_progress_bar, switch_state_space_graph, switch_implicit_choose, @@ -327,6 +327,10 @@ main (int argc, char **argv) * any scenario traversing selects chooses first. */ sys->switchScenario = switch_scenario->ival[0]; /* scenario selector */ + if (sys->switchScenario < 0) + { + sys->output = SCENARIOS; + } if (sys->switchScenario != 0) { #ifdef DEBUG @@ -396,15 +400,12 @@ main (int argc, char **argv) if (switch_state_space_graph->count > 0) { /* enable state space graph output */ - sys->switchStatespace = 1; - } - - /* TODO for now, warning for -m2 and non-clp */ - if (sys->match == 2 && !sys->clp) - { - printf - ("Warning: -m2 is only supported for constraint logic programming.\n"); + sys->output = STATESPACE; //!< New method } + if (switch_empty->count > 0) + sys->output = EMPTY; + if (switch_prune_trace_length->ival[0] >= 0) + sys->switch_maxtracelength = switch_prune_trace_length->ival[0]; #ifdef DEBUG /* in debugging mode, some extra switches */ if (switch_debug_indent->count > 0) @@ -415,10 +416,42 @@ main (int argc, char **argv) /* non-debug defaults */ sys->switchM = 0; #endif - if (switch_disable_violations_report->count > 0) - sys->report = 0; - if (switch_prune_trace_length->ival[0] >= 0) - sys->switch_maxtracelength = switch_prune_trace_length->ival[0]; + + /* + * --------------------------------------- + * Switches consistency checking. + * --------------------------------------- + */ + + /* Latex only makes sense for attacks */ + if (sys->latex && sys->output != ATTACK) + { + error ("Scyther can only generate LaTeX output for attacks."); + } + /* Incremental stuff only works for attack locating */ + if (switch_incremental_runs->count > 0 || + switch_incremental_trace_length->count > 0) + { + if (sys->output != ATTACK && + sys->output != EMPTY) + { + error ("Incremental traversal only for empty or attack output."); + } + } + /* TODO for now, warning for -m2 and non-clp */ + if (sys->match == 2 && !sys->clp) + { + warning ("-m2 is only supported for constraint logic programming."); + } + +#ifdef DEBUG + warning ("Selected output method is %i", sys->output); +#endif + /* + * --------------------------------------- + * Start real stuff + * --------------------------------------- + */ /* latex header? */ if (sys->latex) @@ -427,7 +460,7 @@ main (int argc, char **argv) /* model check system */ #ifdef DEBUG if (DEBUGL (1)) - printf ("Start modelchecking system.\n"); + warning ("Start modelchecking system."); #endif if (switch_incremental_runs->count > 0) { @@ -449,7 +482,10 @@ main (int argc, char **argv) if (sys->attack != NULL && sys->attack->length != 0) { - attackDisplay(sys); + if (sys->output == ATTACK) + { + attackDisplay(sys); + } /* mark exit code */ exitcode = 3; } @@ -563,12 +599,6 @@ timersPrint (const System sys) fprintf (stderr, "\n"); #endif - - /* if scenario counting, display */ - if (sys->switchScenario < 0) - { - fprintf (stderr, "Number of scenarios found: %i\n", sys->countScenario); - } } //! Analyse the model by incremental runs. @@ -697,7 +727,7 @@ MC_single (const System sys) int modelCheck (const System sys) { - if (sys->switchStatespace) + if (sys->output == STATESPACE) { graphInit (sys); } @@ -713,7 +743,7 @@ modelCheck (const System sys) } timersPrint (sys); - if (sys->switchStatespace) + if (sys->output == STATESPACE) { graphDone (sys); } diff --git a/src/modelchecker.c b/src/modelchecker.c index 72b2918..f43b44f 100644 --- a/src/modelchecker.c +++ b/src/modelchecker.c @@ -218,7 +218,7 @@ executeStep (const System sys, const int run) /* store new node numbder */ sys->traceNode[sys->step] = sys->states; /* the construction below always assumes MAX_GRAPH_STATES to be smaller than the unsigned long it, which seems realistic. */ - if (sys->switchStatespace && statesSmallerThan (sys->states, MAX_GRAPH_STATES)) + if (sys->output == STATESPACE && statesSmallerThan (sys->states, MAX_GRAPH_STATES)) { /* display graph */ graphNode (sys); @@ -566,21 +566,19 @@ explorify (const System sys, const int run) { sys->countScenario++; } -#ifdef DEBUG - /* If we are counting and debug, print it */ - if (sys->switchScenario < 0) + /* If we are displaying scenarios, print it */ + if (sys->output == SCENARIOS) { - printf ("// Scenario %i: ", sys->countScenario); + printf ("%i\t", sys->countScenario); scenarioPrint (sys); printf ("\n"); } -#endif /* If it is not the selected one, abort */ if (sys->switchScenario != sys->countScenario) { /* this branch is not interesting */ /* unfortunately, it is also not drawn in the state graph because of this */ - if (sys->switchStatespace) + if (sys->output == STATESPACE) { graphScenario (sys, run, rd); } @@ -1188,7 +1186,7 @@ violateClaim (const System sys, int length, int claimev, Termlist reqt) sys->failed = statesIncrease (sys->failed); /* mark the path in the state graph? */ - if (sys->switchStatespace) + if (sys->output == STATESPACE) { graphPath (sys, length); } diff --git a/src/output.c b/src/output.c index 1a98ee8..dd3dd94 100644 --- a/src/output.c +++ b/src/output.c @@ -481,9 +481,6 @@ attackDisplayAscii (const System sys) void attackDisplay (const System sys) { - if (!sys->report || sys->switchStatespace) - return; - if (sys->latex) { attackDisplayLatex (sys); diff --git a/src/report.c b/src/report.c index 2085db4..d0cf969 100644 --- a/src/report.c +++ b/src/report.c @@ -58,7 +58,7 @@ reportEnd (const System sys) void reportSecrecy (const System sys, Term t) { - if (!sys->report) + if (sys->output != ATTACK) { reportQuit (sys); return; diff --git a/src/system.c b/src/system.c index f8f08cc..00c9b47 100644 --- a/src/system.c +++ b/src/system.c @@ -54,10 +54,10 @@ systemInit () sys->attack = tracebufInit(); /* switches */ + sys->output = ATTACK; // default is to show the attacks sys->porparam = 0; // multi-purpose parameter sys->latex = 0; // latex output? sys->switchScenario = 0; - sys->switchStatespace = 0; sys->switchForceChoose = 1; // force explicit chooses by default sys->switchChooseFirst = 0; // no priority to chooses by default sys->switchReadSymm = 0; // don't force read symmetries by default @@ -69,7 +69,6 @@ systemInit () /* set illegal traversal by default, to make sure it is set later */ sys->traverse = 0; - sys->report = 1; sys->switch_maxtracelength = INT_MAX; sys->maxtracelength = INT_MAX; diff --git a/src/system.h b/src/system.h index 37aff30..f831879 100644 --- a/src/system.h +++ b/src/system.h @@ -91,6 +91,8 @@ struct tracebuf Varbuf variables; }; +enum outputs { EMPTY, ATTACK, STATESPACE, SCENARIOS }; + //! The main state structure. struct system { @@ -109,6 +111,7 @@ struct system int shortestattack; //!< Length of shortest attack trace. /* switches */ + int output; //!< From enum outputs: what should be produced. Default ATTACK. int report; int prune; //!< Type of pruning. int switch_maxtracelength; //!< Helps to remember the length of the last trace. @@ -118,7 +121,6 @@ struct system int switchS; //!< Progress display switch. (traversed states) int porparam; //!< A multi-purpose integer parameter, passed to the partial order reduction method selected. int switchScenario; //!< -1 to count, 0 for disable, 1-n to select the choose scenario - int switchStatespace; //!< Output statespace for dot package int switchForceChoose; //!< Force chooses for each run, even if involved in first read int switchChooseFirst; //!< Priority to chooses, implicit and explicit int switchReadSymm; //!< Enable read symmetry reduction