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

- Made explicit chooses the default behaviour.

Browse Source
This commit is contained in:
ccremers 2004-07-20 21:31:28 +00:00
parent 81e715d612
commit 1ecdd1eb5a
2 changed files with 21 additions and 21 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

40
src/main.c
View File

@ -83,32 +83,32 @@ main (int argc, char **argv)
struct arg_int *match = struct arg_int *match =
arg_int0 ("m", "match", NULL, "matching method (default is 0)"); arg_int0 ("m", "match", NULL, "matching method (default is 0)");
struct arg_lit *clp = struct arg_lit *clp =
arg_lit0 ("c", "cl", "use constraint logic, non-associative."); arg_lit0 ("c", "cl", "use constraint logic, non-associative");
struct arg_int *prune = arg_int0 ("p", "prune", NULL, struct arg_int *prune = arg_int0 ("p", "prune", NULL,
"pruning method (default is 2)"); "pruning method (default is 2)");
struct arg_int *maxlength = arg_int0 ("l", "max-length", NULL, struct arg_int *maxlength = arg_int0 ("l", "max-length", NULL,
"prune traces longer than <int> events."); "prune traces longer than <int> events");
struct arg_lit *incTraces = arg_lit0 (NULL, "increment-traces", struct arg_lit *incTraces = arg_lit0 (NULL, "increment-traces",
"incremental search using the length of the traces."); "incremental search using the length of the traces.");
struct arg_int *maxruns = struct arg_int *maxruns =
arg_int0 ("r", "max-runs", NULL, "create at most <int> runs."); arg_int0 ("r", "max-runs", NULL, "create at most <int> runs");
struct arg_lit *incRuns = arg_lit0 (NULL, "increment-runs", struct arg_lit *incRuns = arg_lit0 (NULL, "increment-runs",
"incremental search using the number of runs."); "incremental search using the number of runs");
struct arg_lit *latex = arg_lit0 (NULL, "latex", "output in LaTeX format."); struct arg_lit *latex = arg_lit0 (NULL, "latex", "output in LaTeX format");
struct arg_lit *noreport = struct arg_lit *noreport =
arg_lit0 ("d", "disable-report", "don't report violations."); arg_lit0 ("d", "disable-report", "don't report violations");
struct arg_lit *switchS = arg_lit0 (NULL, "no-progress", "suppress progress bar."); struct arg_lit *switchS = arg_lit0 (NULL, "no-progress", "suppress progress bar");
struct arg_lit *switchSS = arg_lit0 (NULL, "state-space", "output state space graph."); struct arg_lit *switchSS = arg_lit0 (NULL, "state-space", "output state space graph");
struct arg_lit *switchFC = arg_lit0 (NULL, "force-choose", "force only explicit choose events."); struct arg_lit *switchIC = arg_lit0 (NULL, "implicit-choose", "allow implicit choose events (useful for few runs)");
struct arg_lit *switchRS = arg_lit0 (NULL, "read-symm", "enable read symmetry reductions."); struct arg_lit *switchRS = arg_lit0 (NULL, "read-symm", "enable read symmetry reductions");
struct arg_lit *switchAS = arg_lit0 (NULL, "no-agent-symm", "disable agent symmetry reductions."); struct arg_lit *switchAS = arg_lit0 (NULL, "no-agent-symm", "disable agent symmetry reductions");
struct arg_lit *switchSO = arg_lit0 (NULL, "symm-order", "enable ordering symmetry reductions."); struct arg_lit *switchSO = arg_lit0 (NULL, "symm-order", "enable ordering symmetry reductions");
struct arg_lit *switchNC = arg_lit0 (NULL, "no-noclaims-red", "disable no more claims reductions."); struct arg_lit *switchNC = arg_lit0 (NULL, "no-noclaims-red", "disable no more claims reductions");
struct arg_lit *switchRE = arg_lit0 (NULL, "no-endgame-red", "disable endgame reductions."); struct arg_lit *switchRE = arg_lit0 (NULL, "no-endgame-red", "disable endgame reductions");
#ifdef DEBUG #ifdef DEBUG
struct arg_int *porparam = arg_int0 (NULL, "pp", NULL, "POR parameter."); struct arg_int *porparam = arg_int0 (NULL, "pp", NULL, "POR parameter");
struct arg_lit *switchI = arg_lit0 ("I", "debug-indent", struct arg_lit *switchI = arg_lit0 ("I", "debug-indent",
"indent the debug output using trace length."); "indent the debug output using trace length");
struct arg_int *debugl = struct arg_int *debugl =
arg_int0 ("D", "debug", NULL, "set debug level (default is 0)"); arg_int0 ("D", "debug", NULL, "set debug level (default is 0)");
#endif #endif
@ -129,7 +129,7 @@ main (int argc, char **argv)
noreport, noreport,
switchS, switchS,
switchSS, switchSS,
switchFC, switchIC,
switchRS, switchRS,
switchAS, switchAS,
switchSO, switchSO,
@ -283,9 +283,9 @@ main (int argc, char **argv)
/* generate system */ /* generate system */
sys = systemInit (); sys = systemInit ();
if (switchFC->count > 0) if (switchIC->count > 0)
/* force explicit chooses */ /* allow implicit chooses */
sys->switchForceChoose = 1; sys->switchForceChoose = 0;
if (switchRS->count > 0) if (switchRS->count > 0)
{ {
if (switchSO->count > 0) if (switchSO->count > 0)

2
src/runs.c
View File

@ -64,7 +64,7 @@ systemInit ()
sys->porparam = 0; // multi-purpose parameter sys->porparam = 0; // multi-purpose parameter
sys->latex = 0; // latex output? sys->latex = 0; // latex output?
sys->switchStatespace = 0; sys->switchStatespace = 0;
sys->switchForceChoose = 0; // don't force explicit chooses by default sys->switchForceChoose = 1; // force explicit chooses by default
sys->switchReadSymm = 0; // don't force read symmetries by default sys->switchReadSymm = 0; // don't force read symmetries by default
sys->switchAgentSymm = 1; // default enable agent symmetry sys->switchAgentSymm = 1; // default enable agent symmetry
sys->switchSymmOrder = 0; // don't force symmetry order reduction by default sys->switchSymmOrder = 0; // don't force symmetry order reduction by default