From 33780e8b8020e2f63813ef42e9e814edabc64c8a Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Sat, 6 Mar 2010 22:16:25 +0000 Subject: [PATCH] Small changes to PTA A-R to match A-R API. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@1792 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/pta/PTAAbstractRefine.java | 9 ++++----- 1 file changed, 4 insertions(+), 5 deletions(-) diff --git a/prism/src/pta/PTAAbstractRefine.java b/prism/src/pta/PTAAbstractRefine.java index 07bc196d..d152a440 100644 --- a/prism/src/pta/PTAAbstractRefine.java +++ b/prism/src/pta/PTAAbstractRefine.java @@ -80,7 +80,7 @@ public class PTAAbstractRefine extends STPGAbstractRefine // Store the set of target/initial states from forwards reachability target = forwardsReach.getTarget(); initialStates = forwardsReach.getInitialStates(); - + // Compute validities for all symbolic transitions in the graph graph.computeAllValidities(); @@ -272,8 +272,8 @@ public class PTAAbstractRefine extends STPGAbstractRefine // - abstraction (new states, initial states and transitions) // - target set - protected int splitState(int splitState, List> choiceLists, Set rebuildStates) - throws PrismException + protected int splitState(int splitState, List> choiceLists, Set rebuiltStates, + Set rebuildStates) throws PrismException { LocZone lzSplit; DBMList z, valid1; @@ -444,14 +444,13 @@ public class PTAAbstractRefine extends STPGAbstractRefine // Rebuild this state of the abstraction abstraction.clearState(i); buildSTPGState(i); - rebuildStates.add(i); + rebuiltStates.add(i); } if (verbosity >= 5) { mainLog.println("New graph: " + graph); } - // TODO: need to return this? return numNewStates; }