From 5d8ce238cfbab1caa09d4c833f81f48d6dda1041 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Fri, 15 Oct 2010 17:33:18 +0000 Subject: [PATCH] Moving bisim/expected parts of PTA MC to prism-pta. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@2156 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/pta/PTABisimulation.java | 365 ------------------------- prism/src/pta/PTAExpected.java | 422 ----------------------------- prism/src/pta/PTAModelChecker.java | 49 +--- 3 files changed, 3 insertions(+), 833 deletions(-) delete mode 100644 prism/src/pta/PTABisimulation.java delete mode 100644 prism/src/pta/PTAExpected.java diff --git a/prism/src/pta/PTABisimulation.java b/prism/src/pta/PTABisimulation.java deleted file mode 100644 index 8ca35e80..00000000 --- a/prism/src/pta/PTABisimulation.java +++ /dev/null @@ -1,365 +0,0 @@ -//============================================================================== -// -// 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 pta; - -import java.util.*; - -import prism.*; -import explicit.*; - -public class PTABisimulation -{ - // Log - private PrismLog mainLog; - // Forwards reachability graph - protected ReachabilityGraph graph; - // Initial state(s) - public List initialStates; - // Actual target (symbolic states) - public BitSet target; - - protected int verbosity; - - // Constructors - - public PTABisimulation(PrismLog mainLog, int verbosity) - { - this.mainLog = mainLog; - this.verbosity = verbosity; - } - - // Set methods for flags/settings, etc. - - public void setLog(PrismLog mainLog) - { - this.mainLog = mainLog; - } - - // Accessors for other info generated during bisimulation - - public BitSet getTarget() - { - return target; - } - - public List getInitialStates() - { - return initialStates; - } - - /** - * Compute a probabilistic time-abstracting bisimulation from a PTA and target set. - * @param pta: The PTA - * @param targetLoc: The set of target locations - */ - public MDP computeBisimulation(PTA pta, BitSet targetLocs) throws PrismException - { - ForwardsReach forwardsReach; - MDP mdp; - - // Build forwards reachability graph - forwardsReach = new ForwardsReach(mainLog); - graph = forwardsReach.buildForwardsGraph(pta, targetLocs, null); - - // Extract initial/target states - initialStates = forwardsReach.getInitialStates(); - target = forwardsReach.getTarget(); - - // Display states, graph, etc. - if (verbosity >= 5) { - mainLog.println("\nStates: "); - graph.printStates(mainLog); - mainLog.println("\nGraph: " + graph); - mainLog.println("Target states: " + target); - } - - // Do minimisation - computeBisimulation(graph, initialStates, target); - - mainLog.println("New graph: " + graph.states.size() + " symbolic states, " + target.cardinality() - + " target states"); - HashSet uniq = new HashSet(); - uniq.addAll(graph.states); - mainLog.println(uniq.size() + " unique"); - - // Display states, graph, etc. - if (verbosity >= 5) { - mainLog.println("\nNew states: "); - graph.printStates(mainLog); - mainLog.println("\nNew graph: " + graph); - } - - mainLog.println("\nBuilding MDP..."); - mdp = graph.buildMDP(initialStates); - mainLog.println("MDP: " + mdp.infoString()); - - return mdp; - } - - /** - * Compute a probabilistic time-abstracting bisimulation from a reachability graph. - * TODO: modifies graph, but not others ??? - * @param graph - * @param initialStates - * @param target - */ - public void computeBisimulation(ReachabilityGraph graph, List initialStates, BitSet target) throws PrismException - { - int i; - long timer, timerProgress; - boolean progressDisplayed; - - // Store pointer to graph (used in other methods below) - this.graph = graph; - - // Take copies of initial/target states (will be modified) - this.initialStates = new ArrayList(); - this.initialStates.addAll(initialStates); - this.target = (BitSet) target.clone(); - - // Starting bisimulation... - mainLog.println("\nComputing time-abstracting bisimulation..."); - timer = timerProgress = System.currentTimeMillis(); - progressDisplayed = false; - - // Compute validities for all symbolic transitions in the graph - graph.computeAllValidities(); - - // Go through symbolic transitions - boolean changed = true; - while (changed) { - changed = false; - for (i = 0; i < graph.states.size(); i++) { - if (splitState(i) > 1) { - changed = true; - } - // Print some progress info occasionally - if (System.currentTimeMillis() - timerProgress > 3000) { - if (!progressDisplayed) { - mainLog.print("Number of states so far:"); - progressDisplayed = true; - } - mainLog.print(" " + graph.states.size()); - mainLog.flush(); - timerProgress = System.currentTimeMillis(); - } - } - } - - // Tidy up progress display - if (progressDisplayed) - mainLog.println(" " + graph.states.size()); - - // Bisimulation complete - timer = System.currentTimeMillis() - timer; - mainLog.println("Bisimulation completed in " + (timer / 1000.0) + " secs."); - } - - protected int splitState(int splitState) throws PrismException - { - LocZone lzSplit; - int[] newStateMap, map; - int i, numTransitions, numStates, numNewStates; - ArrayList partition; - ArrayList sts, stsNew; - boolean rebuild; - DBM dbm; - - // Get abstract state to split - lzSplit = graph.states.get(splitState); - if (verbosity >= 1) - mainLog.println("Splitting: #" + splitState + "=" + lzSplit); - - // Get symbolic transition list for this state - sts = graph.trans.get(splitState); - - // Get validity of each outgoing transition from this state. - // In fact, since guards for multiple transitions are often identical, - // we only do this for distinct ones, and build a 'map' between them. - partition = new ArrayList(); - numTransitions = sts.size(); - map = new int[numTransitions]; - for (i = 0; i < numTransitions; i++) { - dbm = (DBM)((DBMList) sts.get(i).valid).list.get(0); - // See if we already have a copy of this zone z - map[i] = partition.indexOf(dbm); - // If not, add to list and store index in map - if (map[i] == -1) { - map[i] = partition.size(); - partition.add(dbm); - } - } - - // Check we actually got a strict split of the partition - if (partition.size() <= 1) { - //mainLog.println("Warning: failed to split state #" + splitState + "=" + lzSplit); - return 1; - } - - // Update symbolic state set info (graph.states) and store info about indices of new states - numNewStates = partition.size(); - newStateMap = new int[numNewStates]; - for (i = 0; i < numNewStates; i++) { - // First new state overwrites one that is being split - if (i == 0) { - graph.states.set(splitState, new LocZone(lzSplit.loc, partition.get(i))); - newStateMap[i] = splitState; - graph.trans.set(splitState, stsNew = new ArrayList()); - } - // Other new states are appended to end of list - else { - graph.states.add(new LocZone(lzSplit.loc, partition.get(i))); - newStateMap[i] = graph.states.size() - 1; - graph.trans.add(stsNew = new ArrayList()); - } - } - for (i = 0; i < numTransitions; i++) { - stsNew = graph.trans.get(newStateMap[map[i]]); - stsNew.add(sts.get(i)); - } - - // Display info - if (verbosity >= 1) { - mainLog.println("Splitting: #" + splitState + "=" + lzSplit); - mainLog.println("into " + numNewStates + ":"); - for (i = 0; i < numNewStates; i++) - mainLog.println("#" + newStateMap[i] + "=" + partition.get(i)); - } - if (verbosity >= 5) - mainLog.println("New states: " + graph.states); - - // Add new states to initial state set if needed - // Note: we assume any abstract state contains either all/no initial states - if (initialStates.contains(splitState)) { - for (i = 1; i < numNewStates; i++) { - initialStates.add(newStateMap[i]); - } - } - - // Rebuild target states - if (target.get(splitState)) { - for (i = 1; i < numNewStates; i++) { - target.set(newStateMap[i]); - } - } - - - // Update symbolic transitions and abstraction - Set oldSTs = new LinkedHashSet(); - Set newSTs = new LinkedHashSet(); - // Go through all abstract states - numStates = graph.states.size(); - for (i = 0; i < numStates; i++) { - oldSTs.clear(); - newSTs.clear(); - // Do we need to rebuild this state? - // (i.e. is it a new state or a successor of the split state?) - rebuild = false; - // For a new state... - if (i == splitState || i > numStates - numNewStates) { - // Split all symbolic transitions from this state - for (SymbolicTransition st : graph.trans.get(i)) { - oldSTs.add(st); - splitSymbolicTransition(i, st, splitState, newStateMap, newSTs); - } - rebuild = true; - } - // For a successor state - else { - // Split symbolic transitions that go to the split state - for (SymbolicTransition st : graph.trans.get(i)) { - if (st.hasSuccessor(splitState)) { - oldSTs.add(st); - splitSymbolicTransition(i, st, splitState, newStateMap, newSTs); - rebuild = true; - } - } - } - // Bail out, if we didn't need to rebuild for this state - if (!rebuild) - continue; - // Now, actually modify the graph - // (didn't do this on the fly because don't went to change - // the list that we are iterating over) - for (SymbolicTransition st : oldSTs) - graph.trans.get(i).remove(st); - for (SymbolicTransition st : newSTs) - graph.trans.get(i).add(st); - if ((verbosity >= 1) && !oldSTs.isEmpty()) { - mainLog.print("Replacing symbolic transitions: " + i + ":" + oldSTs); - mainLog.println(" with: " + i + ":" + newSTs); - } - } - - if (verbosity >= 5) { - mainLog.println("New graph: " + graph); - } - - return numNewStates; - } - - /** - * Split a symbolic transition, based on the division of a symbolic state into several parts. - * @param src: The source of the symbolic transition to be split - * @param st: The symbolic transition to be split - * @param splitState: The index of the symbolic state that is being split - * @param newStateMap: The indices of the new states - * @param newSTs: Where to put the new symbolic transitions - */ - private void splitSymbolicTransition(int src, SymbolicTransition st, int splitState, int newStateMap[], - Set newSTs) - { - // Take a copy of the transition, because we will modify it when analysing it - SymbolicTransition stNew = new SymbolicTransition(st); - // Recursively... - splitSymbolicTransition(src, stNew, splitState, newStateMap, newSTs, 0, st.dests.length); - } - - private void splitSymbolicTransition(int src, SymbolicTransition st, int splitState, int newStateMap[], - Set newSTs, int level, int n) - { - if (level == n) { - Zone valid = graph.computeValidity(src, st.tr, st.dests); - if (!valid.isEmpty()) { - SymbolicTransition stNew = new SymbolicTransition(st); - stNew.valid = valid; - newSTs.add(stNew); - } - } else { - if (st.dests[level] == splitState) { - int m = newStateMap.length; - for (int i = 0; i < m; i++) { - st.dests[level] = newStateMap[i]; - splitSymbolicTransition(src, st, splitState, newStateMap, newSTs, level + 1, n); - } - st.dests[level] = splitState; - } else { - splitSymbolicTransition(src, st, splitState, newStateMap, newSTs, level + 1, n); - } - } - } -} diff --git a/prism/src/pta/PTAExpected.java b/prism/src/pta/PTAExpected.java deleted file mode 100644 index 6e1e50b4..00000000 --- a/prism/src/pta/PTAExpected.java +++ /dev/null @@ -1,422 +0,0 @@ -//============================================================================== -// -// 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 pta; - -import java.util.*; - -import prism.*; -import explicit.*; - -public class PTAExpected -{ - // Prism object - private Prism prism; - // Log - private PrismLog mainLog; - // PTA and associated info - protected PTA pta = null; - protected BitSet targetLocs; - protected int numClocks; - // Forwards reachability graph - protected ReachabilityGraph graph; - // Initial state(s) - protected List initialStates; - // Actual target (symbolic states) - protected BitSet target; - - protected int verbosity = 1; - - /** - * Constructor. - */ - public PTAExpected(Prism prism) - { - this.prism = prism; - mainLog = prism.getMainLog(); - } - - // Set methods for flags/settings, etc. - - public void setLog(PrismLog mainLog) - { - this.mainLog = mainLog; - } - - /** - * Main method: do model checking. - */ - public double check(PTA pta, BitSet targetLocs, boolean min) throws PrismException - { - // Store PTA/target info - this.pta = pta; - this.targetLocs = targetLocs; - - ForwardsReach forwardsReach; - int src, numStates, i, j; - long timer; - int d1, d2; - Zone z, z1, z2; - LocZone lz1, lz2; - - numClocks = pta.getNumClocks(); - // Build forwards reachability graph - forwardsReach = new ForwardsReach(mainLog); - graph = forwardsReach.buildForwardsGraph(pta, targetLocs, null); - mainLog.println(pta); - mainLog.println(graph.states); - mainLog.println(graph); - // Extract initial/target states - initialStates = forwardsReach.getInitialStates(); - target = forwardsReach.getTarget(); - - // Compute validities for all symbolic transitions in the graph - graph.computeAllValidities(); - - PTABisimulation ptaBisim = new PTABisimulation(mainLog, verbosity); - ptaBisim.computeBisimulation(graph, initialStates, target); - initialStates = ptaBisim.getInitialStates(); - target = ptaBisim.getTarget(); - - /*PTAAbstractRefine ptaAR; - ptaAR = new PTAAbstractRefine(); - String arOptions = prism.getSettings().getString(PrismSettings.PRISM_AR_OPTIONS); - ptaAR.setLog(mainLog); - ptaAR.parseOptions(arOptions.split(",")); - ptaAR.forwardsReachAbstractRefine(pta, targetLocs, null, !min); - graph = ptaAR.graph; - mainLog.println(graph); - mainLog.println(graph.states); - for (LocZone lz : graph.states) { - mainLog.println(lz + ": "+lz.zone.storageInfo()); - }*/ - - if (false) { - // Go through symbolic transitions - boolean changed = true; - SymbolicTransition removeMe = null; - while (changed) { - changed = false; - numStates = graph.states.size(); - for (i = 0; i < numStates; i++) { - for (SymbolicTransition st : graph.trans.get(i)) { - //mainLog.println(i + ": " + st); - lz1 = graph.states.get(i); - z1 = lz1.zone; - z2 = st.valid; - //boolean same = equalMinMaxForZone(z1, z2, min); - boolean same = z1.equals(z2); - if (!same) { - //mainLog.println(st.tr); - mainLog.println("Diff for:" + i + ": " + lz1); - mainLog.println("Valid: " + z2); - mainLog.println(z1.storageInfo()); - mainLog.println(z2.storageInfo()); - printMinMaxForZone(z1, min); - printMinMaxForZone(z2, min); - mainLog.println("Splitting " + i + "(st=" + st + ")"); - graph.states.add(new LocZone(lz1.loc, st.valid.deepCopy())); - int newState = graph.states.size() - 1; - graph.copyState(i); - //throw new PrismException("Clock min/max different"); - splitSymbolicTransitionBackwards(i, newState); - removeMe = st; - changed = true; - break; - } - } - if (changed) { - graph.trans.get(i).remove(removeMe); - mainLog.println(graph.states); - mainLog.println(graph); - break; - } - } - } - } - - // Build MDP - MDP mdp = buildMDPWithRewards(graph, initialStates, min); - mainLog.println(mdp); - mainLog.println(mdp.getInitialStates()); - MDPModelChecker mdpMc = new MDPModelChecker(); - mdpMc.setLog(mainLog); - ModelCheckerResult res = mdpMc.expReach(mdp, target, min); - mainLog.println(res.soln); - mainLog.println(explicit.Utils.minOverArraySubset(res.soln, mdp.getInitialStates())); - mainLog.println(explicit.Utils.maxOverArraySubset(res.soln, mdp.getInitialStates())); - - throw new PrismException("Not implemented yet"); - } - - private void splitSymbolicTransitionBackwards(int splitState, int newState) - { - int i, numStates; - - // Update symbolic transitions and abstraction - Set oldSTs = new LinkedHashSet(); - Set newSTs = new LinkedHashSet(); - // Go through all abstract states - numStates = graph.states.size(); - for (i = 0; i < numStates; i++) { - oldSTs.clear(); - newSTs.clear(); - // For a new state... - if (i == splitState || i == newState) { - // Split all symbolic transitions from this state - for (SymbolicTransition st : graph.trans.get(i)) { - oldSTs.add(st); - splitSymbolicTransitionBackwards(i, st, splitState, newState, newSTs); - } - } - // For a successor state - else { - // Refine symbolic transitions that go to the split state - for (SymbolicTransition st : graph.trans.get(i)) { - if (st.hasSuccessor(splitState)) { - oldSTs.add(st); - splitSymbolicTransitionBackwards(i, st, splitState, newState, newSTs); - } - } - } - // Now, actually modify the graph - // (didn't do this on the fly because don't went to change - // the list that we are iterating over) - for (SymbolicTransition st : oldSTs) - graph.trans.get(i).remove(st); - for (SymbolicTransition st : newSTs) - graph.trans.get(i).add(st); - if ((verbosity >= 1) && !oldSTs.isEmpty()) { - mainLog.print("Replacing symbolic transitions: " + i + ":" + oldSTs); - mainLog.println(" with: " + i + ":" + newSTs); - } - } - } - - private void splitSymbolicTransitionBackwards(int src, SymbolicTransition st, int splitState, int newState, - Set newSTs) - { - // Take a copy of the transition, because we will modify it when analysing it - SymbolicTransition stNew = new SymbolicTransition(st); - // Recursively... - splitSymbolicTransitionBackwards(src, stNew, splitState, newState, newSTs, 0, st.dests.length); - } - - private void splitSymbolicTransitionBackwards(int src, SymbolicTransition st, int refineState, int newState, - Set newSTs, int level, int n) - { - if (level == n) { - Zone valid = graph.computeValidity(src, st.tr, st.dests); - if (!valid.isEmpty()) { - SymbolicTransition stNew = new SymbolicTransition(st); - stNew.valid = valid; - newSTs.add(stNew); - } - } else { - if (st.dests[level] == refineState) { - splitSymbolicTransitionBackwards(src, st, refineState, newState, newSTs, level + 1, n); - st.dests[level] = newState; - splitSymbolicTransitionBackwards(src, st, refineState, newState, newSTs, level + 1, n); - st.dests[level] = refineState; - } else { - splitSymbolicTransitionBackwards(src, st, refineState, newState, newSTs, level + 1, n); - } - } - } - - /** - * Check that minimum (or maximum) value for a clock in a zone. - * Note: clocks are indexed from 1. - */ - protected int getMinMaxForZone(Zone z, int x, boolean min) throws PrismException - { - if (z instanceof DBMList) { - if (((DBMList) z).list.size() > 1) - throw new PrismException("Can't compute min/max of non-convex zone"); - z = ((DBMList) z).list.get(0); - } - return min ? ((DBM) z).getMin(x) : ((DBM) z).getMax(x); - } - - /** - * Check that minimum (or maximum) clock values are all the same for two zones. - */ - protected boolean equalMinMaxForZone(Zone z1, Zone z2, boolean min) throws PrismException - { - for (int i = 1; i < numClocks + 1; i++) { - if (getMinMaxForZone(z1, i, min) != getMinMaxForZone(z2, i, min)) - return false; - } - return true; - } - - protected void printMinMaxForZone(Zone z, boolean min) throws PrismException - { - if (z instanceof DBMList) { - if (((DBMList) z).list.size() > 1) - throw new PrismException("Can't compute min/max of non-convex zone"); - z = ((DBMList) z).list.get(0); - } - for (int j = 1; j < numClocks + 1; j++) { - if (j > 1) - mainLog.print(","); - mainLog.print(min ? ((DBM) z).getMin(j) : ((DBM) z).getMax(j)); - } - mainLog.println(); - } - - /** - * Build an MDP from a forwards reachability graph, with rewards encoded. - */ - protected MDP buildMDPWithRewards(ReachabilityGraph graph, List initialStates, boolean min) - throws PrismException - { - Distribution distr; - int src, count, dest, choice, lzRew, rew, i, j; - double rewSum; - long timer; - MDPSimple mdp; - int someClock = 1; - - // Building MDP... - mainLog.println("\nBuilding MDP..."); - timer = System.currentTimeMillis(); - mdp = new MDPSimple(); - - // Add all states, including a new initial state - mdp.addStates(graph.states.size() + 1); - - // For each symbolic state... - src = 0; - for (LocZone lz : graph.states) { - mainLog.println("lz: " + lz); - // Check there is at least one enabled transition - // (don't want deadlocks in non-target states) - if (graph.trans.get(src).size() == 0 && !target.get(src)) { - throw new PrismException("MDP has deadlock in symbolic state " + lz); - } - // And for each outgoing transition in PTA... - for (SymbolicTransition st : graph.trans.get(src)) { - // Build distribution - distr = new Distribution(); - count = -1; - for (Edge edge : st.tr.getEdges()) { - count++; - dest = st.dests[count]; - distr.add(dest, edge.getProbability()); - } - // Skip if distribution is empty - if (distr.isEmpty()) - continue; - // Add distribution - choice = mdp.addChoice(src, distr); - // Compute reward - if (min) { - rewSum = 0.0; - rew = -1; - DBM dbm = DBM.createFromConstraints(pta, st.tr.getGuardConstraints()); - mainLog.println(dbm); - for (i = 1; i < numClocks + 1; i++) { - j = getMinMaxForZone(dbm, i, true); - j -= getMinMaxForZone(lz.zone, i, true); - mainLog.println(j); - if (i == 1 || j > rew) - rew = j; - mainLog.println(" " + rew); - } - rewSum = rew; - mainLog.println("# " + rew); - } else { - rewSum = 0.0; - count = -1; - for (Edge edge : st.tr.getEdges()) { - count++; - dest = st.dests[count]; - distr.add(dest, edge.getProbability()); - mainLog.println("lz" + count + ": " + graph.states.get(dest)); - - lzRew = -1; - rew = -1; - int last = -1; - - for (someClock = 1; someClock < numClocks + 1; someClock++) { - - lzRew = getMinMaxForZone(graph.states.get(dest).zone, someClock, min); - mainLog.println(lzRew); - if (lzRew > 10000) - throw new PrismException("stop"); - LocZone lz2 = lz.deepCopy(); - lz2.dPost(edge); - mainLog.println("post: " + lz2); - rew = getMinMaxForZone(lz2.zone, someClock, min); - mainLog.println(rew); - - mainLog.println(edge.getProbability() + " * (" + lzRew + "-" + rew + ")"); - mainLog.println("# " + (lzRew - rew)); - - if (someClock > 1) { - if (lzRew - rew != last) - throw new PrismException("stop"); - } - last = lzRew - rew; - - } - - rewSum += edge.getProbability() * (lzRew - rew); - mainLog.println("= " + (edge.getProbability() * (lzRew - rew))); - mainLog.println("resSum = " + rewSum); - } - count++; - - } - // Set reward - mdp.setTransitionReward(src, choice, rewSum); - } - src++; - } - - // Create a new initial state to encode incoming reward - src = mdp.getNumStates() - 1; - // PTAs only have one initial state but better check... - if (initialStates.size() != 1) - throw new PrismException("PTA cannot have multiple initial states"); - // Add transition + reward - distr = new Distribution(); - distr.add(initialStates.get(0), 1.0); - mdp.addChoice(src, distr); - if (!min) - mdp.setTransitionReward(src, 0, getMinMaxForZone(graph.states.get(initialStates.get(0)).zone, someClock, - min)); - mdp.addInitialState(src); - - // MDP construction done - timer = System.currentTimeMillis() - timer; - mainLog.println("MDP constructed in " + (timer / 1000.0) + " secs."); - mainLog.println("MDP: " + mdp.infoString()); - - return mdp; - } -} diff --git a/prism/src/pta/PTAModelChecker.java b/prism/src/pta/PTAModelChecker.java index 3d340f45..e704f099 100644 --- a/prism/src/pta/PTAModelChecker.java +++ b/prism/src/pta/PTAModelChecker.java @@ -295,13 +295,8 @@ public class PTAModelChecker // Do probability computation by first constructing a bisimulation else if (ptaMethod.equals("Bisimulation minimisation")) { - PTABisimulation ptaBisim = new PTABisimulation(mainLog, prism.getVerbose() ? 5 : 0); - MDP mdp = ptaBisim.computeBisimulation(pta, targetLocs); - MDPModelChecker mc = new MDPModelChecker(); - mc.setLog(mainLog); - mc.setVerbosity(prism.getVerbose() ? 5 : 0); - ModelCheckerResult res = mc.probReach(mdp, ptaBisim.getTarget(), min); - return res.soln[mdp.getFirstInitialState()]; + // Not supported yet + throw new PrismException("Not yet supported"); } else @@ -313,45 +308,7 @@ public class PTAModelChecker */ private Result checkExpressionReward(ExpressionReward expr) throws PrismException { - boolean min; - ExpressionTemporal exprTemp; - Expression exprTarget; - BitSet targetLocs; - double prob, reward; - - // Check whether Rmin=? or Rmax=? (only two cases allowed) - if (expr.getReward() != null) { - throw new PrismException("PTA model checking currently only supports Rmin=? and Rmax=? properties"); - } - min = expr.getRelOp().equals("min="); - - // Check this is a reachability property (only case allowed at the moment) - if (!(expr.getExpression() instanceof ExpressionTemporal)) - throw new PrismException("PTA model checking for rewards currently only supports the F operator"); - exprTemp = (ExpressionTemporal) expr.getExpression(); - if (exprTemp.getOperator() != ExpressionTemporal.R_F) - throw new PrismException("PTA model checking for rewards currently only supports the F operator"); - - // Determine locations satisfying target - exprTarget = exprTemp.getOperand2(); - targetLocs = checkLocationExpression(exprTarget); - mainLog.println("Target (" + exprTarget + ") satisfied by " + targetLocs.cardinality() + " locations."); - //mainLog.println(targetLocs); - - // Check that probability of reaching target is 1.0 - prob = computeProbabilisticReachability(targetLocs, !min); - // TODO: fix (do a qualitative version) - if (prob < 0.9999) { - throw new PrismException((min ? "Max" : "Min") + " probability of reaching target is less than 1"); - } - - // Do model checking... - /*PTAExpected ptaExp; - ptaExp = new PTAExpected(prism); - reward = ptaExp.check(pta, targetLocs, min);*/ - throw new PrismException("Reward properties not yet supported for PTAs"); - - //return new Result(new Double(reward)); + throw new PrismException("Not yet supported"); } /**