"Name of file for MDP adversary export (if enabled)"},
//PARAMETRICMODELCHECKING
{BOOLEAN_TYPE,PRISM_PARAM_ENABLED,"Do parametric model checking","4.1",newBoolean(false),"",
"Perform parametric model checking."},
{STRING_TYPE,PRISM_PARAM_PRECISION,"Parametric model checking precision","4.1","5/100","",
"Maximal volume of area to remain undecided in each step when performing parametric model checking."},
{CHOICE_TYPE,PRISM_PARAM_SPLIT,"Parametric model checking split method","4.1","Longest","Longest,All",
"Strategy to use when splitting a region during parametric model checking. Either split on longest side, or split on all sides."},
{CHOICE_TYPE,PRISM_PARAM_BISIM,"Parametric model checking bisimulation method","4.1","Weak","Weak,Strong,None",
"Type of bisimulation used to reduce model size during paramteric model checking. For reward-based properties, weak bisimulation cannot be used."},
{CHOICE_TYPE,PRISM_PARAM_FUNCTION,"Parametric model checking function representation","4.1","JAS-cached","JAS-cached,JAS,DAG",
"Type of representation for functions used during parametric model checking."},
{CHOICE_TYPE,PRISM_PARAM_ELIM_ORDER,"Parametric model checking state elimination order","4.1","Backward","Arbitrary,Forward,Forward-reversed,Backward,Backward-reversed,Random",
"Order in which states are eliminated during unbounded parametric model checking analysis."},
{INTEGER_TYPE,PRISM_PARAM_RANDOM_POINTS,"Parametric model checking random evaluations","4.1",newInteger(5),"",
"Number of random points to evaluate per region to increase chance of correctness during parametric model checking."},
{BOOLEAN_TYPE,PRISM_PARAM_SUBSUME_REGIONS,"Parametric model checking region subsumption","4.1",newBoolean(true),"",
"Subsume adjacent regions during parametric model checking."},
{DOUBLE_TYPE,PRISM_PARAM_DAG_MAX_ERROR,"Parametric model checking max. DAG error","4.1",newDouble(1E-100),"",
"Maximal error probability (i.e. maximum probability of of a wrong result) in DAG function representation used for parametric model checking."},
//FASTADAPTIVEUNIFORMISATION
{DOUBLE_TYPE,PRISM_FAU_DELTA,"Cut off delta","4.1",newDouble(10E-12),"",
"States which get a probability below this number during the fast adaptive analysis will be removed."},
{INTEGER_TYPE,PRISM_FAU_ARRAYTHRESHOLD,"Threshold to swap to array mode","4.1",newInteger(100),"",
"If this number of iterations happened during fast adaptive uniformisation without changes to the state space, assume that further changes are unlikely."},
{INTEGER_TYPE,PRISM_FAU_INTERVALS,"Number of time intervals","4.1",newInteger(1),"",
"Splits the time of a time-bounded property into the specified number of intervals."},
{DOUBLE_TYPE,PRISM_FAU_INITIVAL,"Length of initial time interval","4.1",newDouble(1.0),"",
"Length of initial time interval in addition to regular time intervals."},
},
{
{INTEGER_TYPE,SIMULATOR_DEFAULT_NUM_SAMPLES,"Default number of samples","4.0",newInteger(1000),"1,",
@ -354,23 +377,6 @@ public class PrismSettings implements Observer
{FONT_COLOUR_TYPE,LOG_FONT,"Display font","2.1",newFontColorPair(newFont("monospaced",Font.PLAIN,12),Color.black),"","Font used for the log display."},
{COLOUR_TYPE,LOG_BG_COLOUR,"Background colour","2.1",newColor(255,255,255),"","Background colour for the log display."},
{INTEGER_TYPE,LOG_BUFFER_LENGTH,"Buffer length","2.1",newInteger(10000),"1,","Length of the buffer for the log display."}
},
{
{BOOLEAN_TYPE,PARAM,"Do parametric model checking","4.0.4",newBoolean(false),"","Perform parametric model checking."},
{STRING_TYPE,PARAM_PRECISION,"Precision","4.0.4","5/100","","Maximal volume of area to remain undecided in each model checking step."},
{CHOICE_TYPE,PARAM_SPLIT,"Split method","4.0.4","longest","longest,all","Strategy to use when a region has to be split. Either split on longest side, or split on all sides."},
{CHOICE_TYPE,PARAM_BISIM,"Bisimulation method","4.0.4","weak","weak,strong,none","Bisimulation type to use to reduce model size. For reward-based properties, weak bisimulation cannot be used."},
{CHOICE_TYPE,PARAM_FUNCTION,"Function representation","4.0.4","jas-cached","jas-cached,jas,dag","Type of representation of functions used during parametric analysis."},
{CHOICE_TYPE,PARAM_ELIM_ORDER,"Order of state elimination","4.0.4","backward","arbitrary,forward,forward-reversed,backward,backward-reversed,random","Order in which states are eliminated during parametric unbounded analysis."},
{INTEGER_TYPE,PARAM_RANDOM_POINTS,"Random evaluations per region","4.0.4",newInteger(5),"","Number of random points to evaluate per region to increase chance of correctness."},
{BOOLEAN_TYPE,PARAM_SUBSUME_REGIONS,"Subsume adjacent regions","4.0.4",newBoolean(true),"","Subsume regions during parameter synthesis."},
{DOUBLE_TYPE,PARAM_DAG_MAX_ERROR,"Maximal error prob for dag functions","4.0.4",newDouble(1E-100),"","Maximal probability of a wrong result in DAG function representation."},
},
{
{DOUBLE_TYPE,PRISM_FAU_DELTA,"Cut off delta","4.0.1",newDouble(10E-12),"","States which get a probability below this number during the fast adaptive analysis will be removed."},
{INTEGER_TYPE,PRISM_FAU_ARRAYTHRESHOLD,"Threshold to swap to array mode","4.0.1",newInteger(100),"","If this number of iterations happened during fast adaptive uniformisation without changes to the state space, assume that further changes are unlikely."},
{INTEGER_TYPE,PRISM_FAU_INTERVALS,"Number of time intervals","4.0.1",newInteger(1),"","Splits the time of a time-bounded property into the specified number of intervals."},
{DOUBLE_TYPE,PRISM_FAU_INITIVAL,"Length of initial time interval","4.0.1",newDouble(1.0),"","Length of initial time interval in addition to regular time intervals."},
}
};
@ -1176,71 +1182,108 @@ public class PrismSettings implements Observer
}
}
//parametricextension
//PARAMETRICMODELCHECKING:
elseif(sw.equals("param")){
set(PARAM,true);
set(PRISM_PARAM_ENABLED,true);
}
elseif(sw.equals("param-precision")){
if(i<args.length-1){
set(PARAM_PRECISION,args[++i]);
set(PRISM_PARAM_PRECISION,args[++i]);
}else{
thrownewPrismException("No value specified for -"+sw+" switch");
}
}
elseif(sw.equals("param-split")){
elseif(sw.equals("paramsplit")){
if(i<args.length-1){
set(PARAM_SPLIT,args[++i]);
s=args[++i];
if(s.equals("longest"))
set(PRISM_PARAM_SPLIT,"Longest");
elseif(s.equals("all"))
set(PRISM_PARAM_SPLIT,"All");
else
thrownewPrismException("Unrecognised option for -"+sw+" switch (options are: longest, all)");
}else{
thrownewPrismException("No value specified for -"+sw+" switch");
}
}
elseif(sw.equals("param-bisim")){
elseif(sw.equals("parambisim")){
if(i<args.length-1){
set(PARAM_BISIM,args[++i]);
s=args[++i];
if(s.equals("strong"))
set(PRISM_PARAM_BISIM,"Strong");
elseif(s.equals("weak"))
set(PRISM_PARAM_BISIM,"Weak");
elseif(s.equals("none"))
set(PRISM_PARAM_BISIM,"None");
else
thrownewPrismException("Unrecognised option for -"+sw+" switch (options are: strong, weak, none)");
}else{
thrownewPrismException("No value specified for -"+sw+" switch");
}
}
elseif(sw.equals("param-function")){
elseif(sw.equals("paramfunction")){
if(i<args.length-1){
set(PARAM_FUNCTION,args[++i]);
s=args[++i];
if(s.equals("jascached"))
set(PRISM_PARAM_FUNCTION,"JAS-cached");
elseif(s.equals("jas"))
set(PRISM_PARAM_FUNCTION,"JAS");
elseif(s.equals("dag"))
set(PRISM_PARAM_FUNCTION,"DAG");
else
thrownewPrismException("Unrecognised option for -"+sw+" switch (options are: jascached, jas, dag)");
}else{
thrownewPrismException("No value specified for -"+sw+" switch");
}
}
elseif(sw.equals("param-elim-order")){
elseif(sw.equals("paramelimorder")){
if(i<args.length-1){
set(PARAM_ELIM_ORDER,args[++i]);
s=args[++i];
if(s.equals("arb"))
set(PRISM_PARAM_ELIM_ORDER,"Arbitrary");
elseif(s.equals("fw"))
set(PRISM_PARAM_ELIM_ORDER,"Forward");
elseif(s.equals("fwrev"))
set(PRISM_PARAM_ELIM_ORDER,"Forward-reversed");
elseif(s.equals("bw"))
set(PRISM_PARAM_ELIM_ORDER,"Backward");
elseif(s.equals("bwrev"))
set(PRISM_PARAM_ELIM_ORDER,"Backward-reversed");
elseif(s.equals("rand"))
set(PRISM_PARAM_ELIM_ORDER,"Random");
else
thrownewPrismException("Unrecognised option for -"+sw+" switch (options are: arb,fw,fwrev,bw,bwrev,rand)");
}else{
thrownewPrismException("No value specified for -"+sw+" switch");
}
}
elseif(sw.equals("param-random-points")){
elseif(sw.equals("paramrandompoints")){
try{
j=Integer.parseInt(args[++i]);
if(j<0)
thrownewNumberFormatException();
set(PARAM_RANDOM_POINTS,j);
set(PRISM_PARAM_RANDOM_POINTS,j);
}catch(NumberFormatExceptione){
thrownewPrismException("Invalid value for -"+sw+" switch");
}
}
elseif(sw.equals("param-subsume-regions")){
elseif(sw.equals("paramsubsumeregions")){
booleanb=Boolean.parseBoolean(args[++i]);
set(PARAM_SUBSUME_REGIONS,b);
set(PRISM_PARAM_SUBSUME_REGIONS,b);
}
elseif(sw.equals("param-dag-max-error")){
elseif(sw.equals("paramdagmaxerror")){
try{
d=Double.parseDouble(args[++i]);
if(d<0)
thrownewNumberFormatException();
set(PARAM_DAG_MAX_ERROR,d);
set(PRISM_PARAM_DAG_MAX_ERROR,d);
}catch(NumberFormatExceptione){
thrownewPrismException("Invalid value for -"+sw+" switch");
}
}
//FastAdaptiveUniformisation
//FASTADAPTIVEUNIFORMISATION
//Deltaforfastadaptiveuniformisation
elseif(sw.equals("faudelta")){
@ -1271,8 +1314,7 @@ public class PrismSettings implements Observer
thrownewPrismException("No value specified for -"+sw+" switch");
}
}
//numberofintervalsforfastadaptiveuniformisation
//Numberofintervalsforfastadaptiveuniformisation
elseif(sw.equals("fauintervals")){
if(i<args.length-1){
try{
@ -1389,21 +1431,21 @@ public class PrismSettings implements Observer
mainLog.println("-cuddepsilon <x> ............... Set epsilon value for CUDD package [default: 1e-15]");
mainLog.println();
mainLog.println("PARAMETRIC MODEL CHECKING OPTIONS:");
mainLog.println("-param <vals> .................. Define parameters and their ranges <vals>");
mainLog.println("-param-precision <x> ........... Set max undecided region for parameter synthesis [default: 5/100]");
mainLog.println("-param-split <name> ............ Set method to split parameter regions (longest,all) [default: longest]");
mainLog.println("-param-bisim <name> ............ Set bisimulation minimisation for parameter synthesis (weak,strong,none) [default: weak]");
mainLog.println("-param-function <name> ......... Set function representation for parameter synthesis (jas-cached,jas) [default: jas-cached]");
mainLog.println("-param-elim-order <name> ....... Set elimination order for parameter synthesis (arbitrary,forward,forward-reversed,backward,backward-reversed,random) [default: backward]");
mainLog.println("-param-random-points <n> ....... Set number of random points to evaluate per region [default: 5]");
mainLog.println("-param-subsume-regions <b> ..... Subsume adjacent regions during analysis [default: true]");
mainLog.println("-param-dag-max-error <b> ....... Maximal error probability allowed for DAG function representation [default: 1E-100]");
mainLog.println("-param <vals> .................. Do parametric model checking with parameters (and ranges) <vals>");
mainLog.println("-paramprecision <x> ............ Set max undecided region for parameter synthesis [default: 5/100]");
mainLog.println("-paramsplit <name> ............. Set method to split parameter regions (longest,all) [default: longest]");
mainLog.println("-parambisim <name> ............. Set bisimulation minimisation for parameter synthesis (weak,strong,none) [default: weak]");
mainLog.println("-paramfunction <name> .......... Set function representation for parameter synthesis (jascached,jas) [default: jascached]");
mainLog.println("-paramelimorder <name> ......... Set elimination order for parameter synthesis (arb,fw,fwrev,bw,bwrev,rand) [default: bw]");
mainLog.println("-paramrandompoints <n> ......... Set number of random points to evaluate per region [default: 5]");
mainLog.println("-paramsubsumeregions <b> ....... Subsume adjacent regions during analysis [default: true]");
mainLog.println("-paramdagmaxerror <b> .......... Maximal error probability allowed for DAG function representation [default: 1E-100]");
Dave Parker
13 years ago