Browse Source

Add "reach" option to -exportstrat (not actually used yet) [from Ganindu Prabhashana].

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11691 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Dave Parker 9 years ago
parent
commit
883fc69e23
  1. 18
      prism/src/prism/Prism.java
  2. 11
      prism/src/prism/PrismCL.java

18
prism/src/prism/Prism.java

@ -195,6 +195,8 @@ public class Prism extends PrismComponent implements PrismSettingsListener
protected boolean storeVector = false;
// Generate/store a strategy during model checking?
protected boolean genStrat = false;
// Should any generated strategies should be restricted to the states reachable under them?
protected boolean restrictStratToReach = false;
// Do bisimulation minimisation before model checking?
protected boolean doBisim = false;
@ -594,6 +596,14 @@ public class Prism extends PrismComponent implements PrismSettingsListener
this.genStrat = genStrat;
}
/**
* Specify whether or not any generated strategies should be restricted to the states reachable under them.
*/
public void setRestrictStratToReach(boolean restrictStratToReach)
{
this.restrictStratToReach = restrictStratToReach;
}
/**
* Specify whether or not to do bisimulation minimisation before model checking.
*/
@ -928,6 +938,14 @@ public class Prism extends PrismComponent implements PrismSettingsListener
return genStrat;
}
/**
* Whether or not any generated strategies should be restricted to the states reachable under them.
*/
public boolean getRestrictStratToReach()
{
return restrictStratToReach;
}
/**
* Whether or not to do bisimulation minimisation before model checking.
*/

11
prism/src/prism/PrismCL.java

@ -1985,6 +1985,17 @@ public class PrismCL implements PrismModelListener
else
throw new PrismException("Unknown value \"" + optVal + "\" provided for \"type\" option of -exportstrat");
}
else if (opt.startsWith("reach")) {
if (!opt.startsWith("reach="))
throw new PrismException("No value provided for \"reach\" option of -exportstrat");
String optVal = opt.substring(6);
if (optVal.equals("true"))
prism.setRestrictStratToReach(true);
else if (optVal.equals("false"))
prism.setRestrictStratToReach(false);
else
throw new PrismException("Unknown value \"" + optVal + "\" provided for \"reach\" option of -exportstrat");
}
// Unknown option
else {
throw new PrismException("Unknown option \"" + opt + "\" for -exportstrat switch");

Loading…
Cancel
Save