|
|
@ -293,6 +293,10 @@ public abstract class STPGAbstractRefine |
|
|
getModelChecker().setProb0(false); |
|
|
getModelChecker().setProb0(false); |
|
|
} else if (opt.equals("noprob1")) { |
|
|
} else if (opt.equals("noprob1")) { |
|
|
getModelChecker().setProb1(false); |
|
|
getModelChecker().setProb1(false); |
|
|
|
|
|
} else if (opt.equals("epsilon")) { |
|
|
|
|
|
if (optVal != null) { |
|
|
|
|
|
getModelChecker().setTermCritParam(Double.parseDouble(optVal)); |
|
|
|
|
|
} |
|
|
} else if (opt.equals("maxrefs")) { |
|
|
} else if (opt.equals("maxrefs")) { |
|
|
if (optVal != null) { |
|
|
if (optVal != null) { |
|
|
setMaxRefinements(Integer.parseInt(optVal)); |
|
|
setMaxRefinements(Integer.parseInt(optVal)); |
|
|
@ -598,10 +602,6 @@ public abstract class STPGAbstractRefine |
|
|
ModelCheckerResult res = null; |
|
|
ModelCheckerResult res = null; |
|
|
int i, n; |
|
|
int i, n; |
|
|
|
|
|
|
|
|
// Pass settings to model checker |
|
|
|
|
|
mc.setTermCrit(TermCrit.RELATIVE); |
|
|
|
|
|
mc.setTermCritParam(1e-8); |
|
|
|
|
|
|
|
|
|
|
|
// Compute lower bounds |
|
|
// Compute lower bounds |
|
|
switch (abstractionType) { |
|
|
switch (abstractionType) { |
|
|
case MDP: |
|
|
case MDP: |
|
|
|