From 7400c243f6ba7d67f1ddaeb2b5ff5b4a030e6538 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Sun, 21 Feb 2010 15:45:24 +0000 Subject: [PATCH] Some code for doing full model checking to test A-R loop. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@1761 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- .../src/explicit/PrismSTPGAbstractRefine.java | 22 +++++++++++++++++++ 1 file changed, 22 insertions(+) diff --git a/prism/src/explicit/PrismSTPGAbstractRefine.java b/prism/src/explicit/PrismSTPGAbstractRefine.java index 5b054b5a..98fc70e4 100644 --- a/prism/src/explicit/PrismSTPGAbstractRefine.java +++ b/prism/src/explicit/PrismSTPGAbstractRefine.java @@ -342,8 +342,21 @@ public class PrismSTPGAbstractRefine extends STPGAbstractRefine */ public void doExactModelChecking() throws PrismException { + ModelCheckerResult res = null; switch (modelType) { case DTMC: + switch (propertyType) { + case PROB_REACH: + break; + case PROB_REACH_BOUNDED: + res = ((MDPModelChecker) mc).probReachBounded(new MDP((DTMC)modelConcrete), targetConcrete, reachBound, false); +// res = ((MDPModelChecker) mc).probReach((MDP) abstraction, target, true); + break; + case EXP_REACH: + break; + default: + throw new PrismException("Property type " + propertyType + " not supported"); + } break; case CTMC: break; @@ -354,6 +367,13 @@ public class PrismSTPGAbstractRefine extends STPGAbstractRefine s += " model type " + modelType + " and property type " + propertyType; throw new PrismException(s); } + + // Display results for all initial states + mainLog.print("Results for initial state(s):"); + for (int j : modelConcrete.getInitialStates()) { + mainLog.print(" " + res.soln[j]); + } + mainLog.println(); } public static void main(String args[]) @@ -412,6 +432,8 @@ public class PrismSTPGAbstractRefine extends STPGAbstractRefine if (sOpt != null) { abstractRefine.setReachBound(Integer.parseInt(sOpt)); } + } else if (sw.equals("exact")) { + abstractRefine.exact = true; } // Otherwise, try passing to abstraction-refinement engine