From 49b9846c5b9ac42bba76949f2b70ede12ee00d81 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Wed, 20 Jul 2011 20:24:42 +0000 Subject: [PATCH] Fix CTL counterexample generation for case where there are multiple initial states. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3307 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/prism/NonProbModelChecker.java | 14 ++++++++++---- 1 file changed, 10 insertions(+), 4 deletions(-) diff --git a/prism/src/prism/NonProbModelChecker.java b/prism/src/prism/NonProbModelChecker.java index 43d67112..c1704224 100644 --- a/prism/src/prism/NonProbModelChecker.java +++ b/prism/src/prism/NonProbModelChecker.java @@ -196,8 +196,9 @@ public class NonProbModelChecker extends StateModelChecker */ protected StateValues checkExistsUntil(ExpressionTemporal expr) throws PrismException { - JDDNode b1, b2, transRel, tmp, tmp2, tmp3, tmp4, init = null; + JDDNode b1, b2, transRel, tmp, tmp2, tmp3, init = null; ArrayList cexDDs = null; + JDDNode cexInit = null; boolean done, cexDone = false; Vector cexActions; int iters, i; @@ -255,8 +256,14 @@ public class NonProbModelChecker extends StateModelChecker JDD.Ref(tmp2); cexDDs.add(JDD.And(tmp2, JDD.Not(tmp))); // See if we have found the initial state yet, and if so, don't store any more info - if (JDD.AreInterecting(tmp2, init)) + if (JDD.AreInterecting(tmp2, init)) { cexDone = true; + // Choose an initial state (in case there are several) which intersects + JDD.Ref(tmp2); + JDD.Ref(init); + cexInit = JDD.And(tmp2, init); + cexInit = JDD.RestrictToFirst(cexInit, allDDRowVars); + } } JDD.Deref(tmp); tmp = tmp2; @@ -272,8 +279,7 @@ public class NonProbModelChecker extends StateModelChecker mainLog.println("\nProcessing counterexample trace (length " + (cexDDs.size() - 1) + ")..."); // First state of counterexample (at end of array) is initial state JDD.Deref(cexDDs.get(cexDDs.size() - 1)); - JDD.Ref(init); - cexDDs.set(cexDDs.size() - 1, init); + cexDDs.set(cexDDs.size() - 1, cexInit); // Go through remaining steps of counterexample for (i = cexDDs.size() - 2; i >= 0; i--) { // Get states that are a successor of the previous state of the counterexample