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

@@ -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
 {

prism/src/cex/CexPathStates.java

@@ -0,0 +1,195 @@
+//==============================================================================
+//	
+//	Copyright (c) 2002-
+//	Authors:
+//	* Dave Parker <david.parker@comlab.ox.ac.uk> (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<State> states;
+
+	/**
+	 * Construct empty path.
+	 */
+	public CexPathStates(prism.Model model)
+	{
+		this.model = model;
+		states = new ArrayList<State>();
+	}
+
+	/**
+	 * 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;
+	}
+}

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<String>();
-					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<String>();
+						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);
 	}
 }

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();
 							}