- Added --no-intruder switch, but it is currently broken.
This commit is contained in:
parent
00e49601eb
commit
e82ce8b962
@ -3203,10 +3203,10 @@ prune_bounds ()
|
||||
return 1;
|
||||
|
||||
// Limit on intruder events count
|
||||
if (switches.maxIntruderActions < INT_MAX)
|
||||
if (switches.maxIntruderActions < INT_MAX || !(switches.intruder))
|
||||
{
|
||||
// Only check if actually used
|
||||
if (countIntruderActions () > switches.maxIntruderActions)
|
||||
if (!(switches.intruder) || countIntruderActions () > switches.maxIntruderActions)
|
||||
{
|
||||
if (switches.output == PROOF)
|
||||
{
|
||||
|
@ -69,6 +69,7 @@ switchesInit (int argc, char **argv)
|
||||
switches.agentTypecheck = 1; // default do check agent types
|
||||
switches.concrete = true; // default removes symbols, and makes traces concrete
|
||||
switches.extravert = false; // default allows also initiator Alice to talk to Alice
|
||||
switches.intruder = true; // default allows an intruder
|
||||
|
||||
// Misc
|
||||
switches.switchP = 0; // multi-purpose parameter
|
||||
@ -561,6 +562,22 @@ switcher (const int process, int index)
|
||||
}
|
||||
}
|
||||
|
||||
if (detect (' ', "no-intruder", 0))
|
||||
{
|
||||
if (!process)
|
||||
{
|
||||
/* for testing purposes: hide
|
||||
*
|
||||
* Disables the intruder
|
||||
*/
|
||||
}
|
||||
else
|
||||
{
|
||||
switches.intruder = false;
|
||||
return index;
|
||||
}
|
||||
}
|
||||
|
||||
if (detect (' ', "extravert", 0))
|
||||
{
|
||||
if (!process)
|
||||
|
@ -48,6 +48,7 @@ struct switchdata
|
||||
int agentTypecheck; //!< Check type of agent variables in all matching modes
|
||||
int concrete; //!< Swap out variables at the end.
|
||||
int extravert; //!< Disallow Alice talking to Alice
|
||||
int intruder; //!< Enable intruder actions (default)
|
||||
|
||||
// Misc
|
||||
int switchP; //!< A multi-purpose integer parameter, passed to the partial order reduction method selected.
|
||||
|
Loading…
Reference in New Issue
Block a user