andr3/scyther
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

- Implemented output method selector, sys->output.

Browse Source 
- Changed disable-report switch into --empty.
- --scenario=-1 now displays a list of scenarios. Use wc -l to count
  them.
This commit is contained in:
ccremers 2004-07-29 10:13:13 +00:00
parent d5db3ca0e2
commit dda2907492
6 changed files with 66 additions and 40 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

78
src/main.c
View File

@ -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)
{
@ -448,8 +481,11 @@ main (int argc, char **argv)
/* Display shortest attack, if any */
if (sys->attack != NULL && sys->attack->length != 0)
{
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);
}

14
src/modelchecker.c
View File

@ -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);
}

3
src/output.c
View File

@ -481,9 +481,6 @@ attackDisplayAscii (const System sys)
void
attackDisplay (const System sys)
{
if (!sys->report || sys->switchStatespace)
return;
if (sys->latex)
{
attackDisplayLatex (sys);

2
src/report.c
View File

@ -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;

3
src/system.c
View File

@ -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;

4
src/system.h
View File

@ -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