From 7e0706e43e19ce07c70ecbe925691d0cf086af8c Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Tue, 20 Mar 2012 20:58:02 +0000 Subject: [PATCH] Ongoing improvements to CTL cex generation. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@4913 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/cex/CexPathAsBDDs.java | 5 +- prism/src/cex/CexPathStates.java | 195 +++++++++++++++++++++++ prism/src/prism/NonProbModelChecker.java | 75 +++++---- prism/src/prism/PrismCL.java | 10 ++ 4 files changed, 250 insertions(+), 35 deletions(-) create mode 100644 prism/src/cex/CexPathStates.java diff --git a/prism/src/cex/CexPathAsBDDs.java b/prism/src/cex/CexPathAsBDDs.java index b653aee7..e4cc3139 100644 --- a/prism/src/cex/CexPathAsBDDs.java +++ b/prism/src/cex/CexPathAsBDDs.java @@ -34,8 +34,9 @@ import parser.State; import simulator.PathFullInfo;; /** - * Class to store a single-path, non-probabilistic counterexample, as a list of BDDs. - * This is just a sequence of states, no more. + * Class to store a counterexample/witness comprising a single path, as a list of BDDs. + * The basic contents of the path is is a sequence of states (BDDs). + * Optionally, action labels can also be included. */ public class CexPathAsBDDs implements PathFullInfo { diff --git a/prism/src/cex/CexPathStates.java b/prism/src/cex/CexPathStates.java new file mode 100644 index 00000000..b2be15e9 --- /dev/null +++ b/prism/src/cex/CexPathStates.java @@ -0,0 +1,195 @@ +//============================================================================== +// +// Copyright (c) 2002- +// Authors: +// * Dave Parker (University of Oxford) +// +//------------------------------------------------------------------------------ +// +// This file is part of PRISM. +// +// PRISM is free software; you can redistribute it and/or modify +// it under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 2 of the License, or +// (at your option) any later version. +// +// PRISM is distributed in the hope that it will be useful, +// but WITHOUT ANY WARRANTY; without even the implied warranty of +// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +// GNU General Public License for more details. +// +// You should have received a copy of the GNU General Public License +// along with PRISM; if not, write to the Free Software Foundation, +// Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA +// +//============================================================================== + +package cex; + +import java.util.ArrayList; + +import parser.State; +import simulator.PathFullInfo;; + +/** + * Class to store a counterexample/witness comprising a single path, + * represented as a list of states, stored as State objects. + */ +public class CexPathStates implements PathFullInfo +{ + protected prism.Model model; + protected ArrayList states; + + /** + * Construct empty path. + */ + public CexPathStates(prism.Model model) + { + this.model = model; + states = new ArrayList(); + } + + /** + * Add a state to the path (will be stored, not copied). + */ + public void addState(State state) + { + states.add(state); + } + + /** + * Clear the counterexample. + */ + public void clear() + { + states = null; + } + + // ACCESSORS (for PathFullInfo) + + @Override + public int size() + { + return states.size() - 1; + } + + @Override + public State getState(int step) + { + return states.get(step); + } + + @Override + public double getStateReward(int step, int rsi) + { + return 0.0; + } + + @Override + public double getCumulativeTime(int step) + { + return 0.0; + } + + @Override + public double getCumulativeReward(int step, int rsi) + { + return 0.0; + } + + @Override + public double getTime(int step) + { + return 0.0; + } + + @Override + public int getChoice(int step) + { + return 0; + } + + @Override + public int getModuleOrActionIndex(int step) + { + return 0; + } + + @Override + public String getModuleOrAction(int step) + { + return ""; + } + + @Override + public double getTransitionReward(int step, int rsi) + { + return 0.0; + } + + @Override + public boolean isLooping() + { + return false; + } + + @Override + public int loopStart() + { + return 0; + } + + @Override + public int loopEnd() + { + return 0; + } + + @Override + public boolean hasRewardInfo() + { + return false; + } + + @Override + public boolean hasChoiceInfo() + { + return false; + } + + @Override + public boolean hasActionInfo() + { + return false; + } + + @Override + public boolean hasTimeInfo() + { + return false; + } + + @Override + public boolean hasLoopInfo() + { + return false; + } + + // Standard method + + @Override + public String toString() + { + State state; + int i, n; + String s = ""; + n = states.size(); + for (i = 0; i < n; i++) { + state = states.get(i); + s += state.toString(); + if (i < n - 1) + s += "\n"; + } + return s; + } +} diff --git a/prism/src/prism/NonProbModelChecker.java b/prism/src/prism/NonProbModelChecker.java index 1bc0adf0..8c1a9ec1 100644 --- a/prism/src/prism/NonProbModelChecker.java +++ b/prism/src/prism/NonProbModelChecker.java @@ -31,6 +31,7 @@ import java.util.*; import jdd.*; import parser.ast.*; import cex.CexPathAsBDDs; +import cex.CexPathStates; /* * Non probabilistic model checker, initially for CTL. @@ -269,6 +270,10 @@ public class NonProbModelChecker extends StateModelChecker tmp = tmp2; } + // Print iterations/timing info + l = System.currentTimeMillis() - l; + mainLog.println("\nCTL EU fixpoint: " + iters + " iterations in " + (l / 1000.0) + " seconds"); + // Process the counterexample info to produce a trace if (doGenCex) { if (!cexDone) { @@ -276,7 +281,7 @@ public class NonProbModelChecker extends StateModelChecker JDD.Deref(cexDDs.get(i)); } } else { - mainLog.println("\nProcessing counterexample trace (length " + (cexDDs.size() - 1) + ")..."); + mainLog.println("Processing counterexample trace (" + cexDDs.size() + " states long)..."); // First state of counterexample (at end of array) is initial state JDD.Deref(cexDDs.get(cexDDs.size() - 1)); cexDDs.set(cexDDs.size() - 1, cexInit); @@ -297,49 +302,53 @@ public class NonProbModelChecker extends StateModelChecker JDD.Deref(cexDDs.get(i)); cexDDs.set(i, tmp3); } - // For an MDP model, build a list of actions from counterexample - if (model.getModelType() == ModelType.MDP) { - cexActions = new Vector(); - for (i = cexDDs.size() - 1; i >= 1; i--) { - JDD.Ref(trans01); - JDD.Ref(cexDDs.get(i)); - tmp3 = JDD.And(trans01, cexDDs.get(i)); - JDD.Ref(cexDDs.get(i - 1)); - tmp3 = JDD.And(tmp3, JDD.PermuteVariables(cexDDs.get(i - 1), allDDRowVars, allDDColVars)); - tmp3 = JDD.ThereExists(tmp3, allDDColVars); - JDD.Ref(transActions); - tmp3 = JDD.Apply(JDD.TIMES, tmp3, transActions); - int action = (int) JDD.FindMax(tmp3); - cexActions.add(action > 0 ? model.getSynchs().get(action - 1) : ""); - JDD.Deref(tmp3); - JDD.Deref(cexDDs.get(i)); - } - JDD.Deref(cexDDs.get(0)); - mainLog.println("Counterexample (action sequence): " + cexActions); - result.setCounterexample(cexActions); + // Construct counterexample object + CexPathStates cex = new CexPathStates(model); + for (i = cexDDs.size() - 1; i >= 0; i--) { + cex.addState(model.convertBddToState(cexDDs.get(i))); + JDD.Deref(cexDDs.get(i)); } - // Otherwise, convert list of BDDs to list of states - else { - CexPathAsBDDs cex = new CexPathAsBDDs(model); - for (i = cexDDs.size() - 1; i >= 0; i--) { - cex.addState(cexDDs.get(i)); - JDD.Deref(cexDDs.get(i)); + result.setCounterexample(cex); + if (1 == 2) { + // For an MDP model, build a list of actions from counterexample + if (model.getModelType() == ModelType.MDP) { + cexActions = new Vector(); + for (i = cexDDs.size() - 1; i >= 1; i--) { + JDD.Ref(trans01); + JDD.Ref(cexDDs.get(i)); + tmp3 = JDD.And(trans01, cexDDs.get(i)); + JDD.Ref(cexDDs.get(i - 1)); + tmp3 = JDD.And(tmp3, JDD.PermuteVariables(cexDDs.get(i - 1), allDDRowVars, allDDColVars)); + tmp3 = JDD.ThereExists(tmp3, allDDColVars); + JDD.Ref(transActions); + tmp3 = JDD.Apply(JDD.TIMES, tmp3, transActions); + int action = (int) JDD.FindMax(tmp3); + cexActions.add(action > 0 ? model.getSynchs().get(action - 1) : ""); + JDD.Deref(tmp3); + JDD.Deref(cexDDs.get(i)); + } + JDD.Deref(cexDDs.get(0)); + mainLog.println("Counterexample (action sequence): " + cexActions); + result.setCounterexample(cexActions); + } + // Otherwise, convert list of BDDs to list of states + else { + CexPathAsBDDs cexBDDs = new CexPathAsBDDs(model); + for (i = cexDDs.size() - 1; i >= 0; i--) { + cexBDDs.addState(cexDDs.get(i)); + JDD.Deref(cexDDs.get(i)); + } + result.setCounterexample(cexBDDs); } - result.setCounterexample(cex); } } } - l = System.currentTimeMillis() - l; - // Derefs JDD.Deref(b1); JDD.Deref(b2); JDD.Deref(transRel); - // Print iterations/timing info - mainLog.println("\nCTL EU fixpoint: " + iters + " iterations in " + (l / 1000.0) + " seconds"); - return new StateValuesMTBDD(tmp, model); } } diff --git a/prism/src/prism/PrismCL.java b/prism/src/prism/PrismCL.java index 3ba24c0e..e4b1136b 100644 --- a/prism/src/prism/PrismCL.java +++ b/prism/src/prism/PrismCL.java @@ -29,8 +29,11 @@ package prism; import java.io.*; import java.util.*; +import cex.CexPathStates; + import parser.*; import parser.ast.*; +import simulator.SimulatorEngine; import simulator.method.*; // prism - command line version @@ -309,6 +312,13 @@ public class PrismCL implements PrismModelListener if (cex != null) { mainLog.println("\nCounterexample/witness:"); mainLog.println(cex); + /*SimulatorEngine engine = prism.getSimulator(); + try { + engine.loadPath(modulesFile, (CexPathStates) cex); + engine.exportPath(null, true, ",", null); + } catch (PrismException e) { + error(e.getMessage()); + }*/ if (cex instanceof cex.CexPathAsBDDs) { ((cex.CexPathAsBDDs) cex).clear(); }