- Fixed typo in --help (noted by Sjouke)
- State-space should generate classes.
This commit is contained in:
parent
6f670d7ab6
commit
d2ac518234
@ -505,22 +505,6 @@ switcher (const int process, int index, int commandline)
|
|||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
if (detect ('s', "state-space", 0))
|
|
||||||
{
|
|
||||||
if (!process)
|
|
||||||
{
|
|
||||||
helptext ("-s, --state-space",
|
|
||||||
"ignore any existing claims and add 'reachable' claims to generate the full state space");
|
|
||||||
}
|
|
||||||
else
|
|
||||||
{
|
|
||||||
switches.removeclaims = true; // remove parsed claims
|
|
||||||
switches.addreachableclaim = true; // add reachability claims
|
|
||||||
switches.prune = 0; // do not prune anything
|
|
||||||
return index;
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
if (detect ('C', "class", 0))
|
if (detect ('C', "class", 0))
|
||||||
{
|
{
|
||||||
if (!process)
|
if (!process)
|
||||||
@ -535,6 +519,23 @@ switcher (const int process, int index, int commandline)
|
|||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
if (detect ('s', "state-space", 0))
|
||||||
|
{
|
||||||
|
if (!process)
|
||||||
|
{
|
||||||
|
helptext ("-s, --state-space",
|
||||||
|
"ignore any existing claims and add 'reachable' claims. Generate full state space classes.");
|
||||||
|
}
|
||||||
|
else
|
||||||
|
{
|
||||||
|
switches.removeclaims = true; // remove parsed claims
|
||||||
|
switches.addreachableclaim = true; // add reachability claims
|
||||||
|
switches.prune = 0; // do not prune anything
|
||||||
|
switches.concrete = false; // show classes
|
||||||
|
return index;
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
if (detect (' ', "concrete", 0))
|
if (detect (' ', "concrete", 0))
|
||||||
{
|
{
|
||||||
if (!process)
|
if (!process)
|
||||||
@ -627,7 +628,7 @@ switcher (const int process, int index, int commandline)
|
|||||||
{
|
{
|
||||||
if (!process)
|
if (!process)
|
||||||
{
|
{
|
||||||
helptext ("-A,- -all-attacks",
|
helptext ("-A, --all-attacks",
|
||||||
"generate all attacks within the state space instead of just one");
|
"generate all attacks within the state space instead of just one");
|
||||||
}
|
}
|
||||||
else
|
else
|
||||||
|
@ -1,3 +1,5 @@
|
|||||||
|
- Scyther binary in www-ccremers hangen voor Sjouke, want daar update
|
||||||
|
hij de boel van.
|
||||||
- Maybe add warning for type of matching in the output, maybe stderr.
|
- Maybe add warning for type of matching in the output, maybe stderr.
|
||||||
- SConstruct file should check whether ctags actually exists (avoiding
|
- SConstruct file should check whether ctags actually exists (avoiding
|
||||||
errors)
|
errors)
|
||||||
|
Loading…
Reference in New Issue
Block a user