diff --git a/prism/src/prism/PrismSettings.java b/prism/src/prism/PrismSettings.java index 725f5242..367b2b07 100644 --- a/prism/src/prism/PrismSettings.java +++ b/prism/src/prism/PrismSettings.java @@ -220,7 +220,7 @@ public class PrismSettings implements Observer // ENGINES/METHODS: { CHOICE_TYPE, PRISM_ENGINE, "Engine", "2.1", "Hybrid", "MTBDD,Sparse,Hybrid,Explicit", "Which engine (hybrid, sparse, MTBDD, explicit) should be used for model checking." }, - { CHOICE_TYPE, PRISM_PTA_METHOD, "PTA model checking method", "3.3", "Stochastic games", "Digital clocks,Stochastic games", + { CHOICE_TYPE, PRISM_PTA_METHOD, "PTA model checking method", "3.3", "Stochastic games", "Digital clocks,Stochastic games,Backwards reachability", "Which method to use for model checking of PTAs." }, { CHOICE_TYPE, PRISM_TRANSIENT_METHOD, "Transient probability computation method", "3.3", "Uniformisation", "Uniformisation,Fast adaptive uniformisation", "Which method to use for computing transient probabilities in CTMCs." }, @@ -889,8 +889,8 @@ public class PrismSettings implements Observer set(PRISM_PTA_METHOD, "Digital clocks"); else if (s.equals("games")) set(PRISM_PTA_METHOD, "Stochastic games"); - else if (s.equals("bisim")) - set(PRISM_PTA_METHOD, "Bisimulation minimisation"); + else if (s.equals("backwards") || s.equals("bw")) + set(PRISM_PTA_METHOD, "Backwards reachability"); else throw new PrismException("Unrecognised option for -" + sw + " switch (options are: digital, games)"); } else { diff --git a/prism/src/pta/BackwardsReach.java b/prism/src/pta/BackwardsReach.java new file mode 100644 index 00000000..0d498b5d --- /dev/null +++ b/prism/src/pta/BackwardsReach.java @@ -0,0 +1,244 @@ +//============================================================================== +// +// 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 BackwardsReach extends PrismComponent +{ + /** + * Create a new MDPModelChecker, inherit basic state from parent (unless null). + */ + public BackwardsReach(PrismComponent parent) throws PrismException + { + super(parent); + } + + /** + * Compute the min/max probability of reaching a target in a PTA, from the initial state, + * using the backwards reachability method. + * @param pta The PTA + * @param targetLocs Target locations + * @param targetConstraint Target timing contraint + * @param min Min or max probabilities (true=min, false=max) + */ + public double computeProbabilisticReachability(PTA pta, BitSet targetLocs, boolean min) throws PrismException + { + if (min) + throw new PrismException("Backwards reachability does not yet support minmum probabilities"); + + // Build backwards graph + BackwardsReachabilityGraph graph = buildBackwardsGraph(pta, targetLocs); + + // Build corresponding MDP + mainLog.print("Building MDP... "); + mainLog.flush(); + MDP mdp = graph.buildMDP(pta); + mainLog.println(mdp.infoString()); + //mdp.exportToDotFile("mdp.dot", target); + + // Compute reachability probs on MDP + MDPModelChecker mc = new MDPModelChecker(this); + mc.setExportAdv(true); + mc.setPrecomp(false); + ModelCheckerResult res = mc.computeReachProbs(mdp, graph.getTarget(), false); + + // Result is max prob over all initial states + return Math.max(0.0, Utils.minMaxOverArraySubset(res.soln, graph.getInitialStates(), false)); + } + + /** + * Build a backwards reachability graph, from a PTA object. + */ + public BackwardsReachabilityGraph buildBackwardsGraph(PTA pta, BitSet targetLocs) throws PrismException + { + LocZone lz; + LinkedList explore; // (Waiting) + IndexedSet found; // (Visited) + List states; + BackwardsReachabilityGraph graph; + int src, dest, count; + long timer; + + mainLog.print("\nBuilding backwards reachability graph..."); + mainLog.flush(); + ProgressDisplay progress = new ProgressDisplay(mainLog); + progress.start(); + timer = System.currentTimeMillis(); + + // Initialise data structures + graph = new BackwardsReachabilityGraph(); + found = new IndexedSet(); + explore = new LinkedList(); + graph.states = states = new ArrayList(); + + // Add target states + count = 0; + for (int loc = targetLocs.nextSetBit(0); loc >= 0; loc = targetLocs.nextSetBit(loc + 1)) { + Zone zTarget = DBM.createTrue(pta); + zTarget.addConstraints(pta.getInvariantConstraints(loc)); + LocZone lzTarget = new LocZone(loc, zTarget); + found.add(lzTarget); + explore.add(lzTarget); + states.add(lzTarget); + graph.addState(pta.getTransitions(loc)); + graph.addTargetState(count++); + } + + // Reachability loop + dest = -1; + // While there are unexplored symbolic states... + while (!explore.isEmpty()) { + // Pick next state to explore + // NB: States are added in order found so we know index of lz is dest+1 + lz = explore.removeFirst(); + dest++; + //mainLog.println("Exploring: " + dest + ":" + lz); + + // Time predecessor (same for all incoming edges) + lz = lz.deepCopy(); + lz.tPre(pta); + + // For each incoming transition... + // TODO: make more efficient + for (int ii = 0; ii < pta.getNumLocations(); ii++) { + if (targetLocs.get(ii)) + continue; + int iTrans = -1; + for (Transition tr : pta.getTransitions(ii)) { + iTrans++; + int numEdges = tr.getNumEdges(); + for (int iEdge = 0; iEdge < numEdges; iEdge++) { + Edge edge = tr.getEdges().get(iEdge); + //mainLog.println(edge); + if (edge.getDestination() != lz.loc) + continue; + LocZone lzSrc = lz.deepCopy(); + lzSrc.dPre(edge); + // If predecessor state is non-empty + if (!lzSrc.zone.isEmpty()) { + // add state + if (found.add(lzSrc)) { + //mainLog.println("Added " + Yset.getIndexOfLastAdd() + ":" + lzSrc); + explore.add(lzSrc); + states.add(lzSrc); + graph.addState(pta.getTransitions(lzSrc.loc)); + } + // end add state + src = found.getIndexOfLastAdd(); + //mainLog.println("D += " + src + ":" + lz2 + "->" + dest + ":..."); + graph.addTransition(src, iTrans, iEdge, dest); + //mainLog.println(src + ":" + graph.getList(src)); + + // For each state that lzTmp intersects lzSrc + int numStatesSoFar = states.size(); + for (int src2 = 0; src2 < numStatesSoFar; src2++) { + // TODO: if any edges in graph... + LocZone lzTmp = states.get(src2); + if (src2 != src && lzTmp.loc == lzSrc.loc) { + Zone zTmp = lzTmp.zone.deepCopy(); + zTmp.intersect(lzSrc.zone); + //mainLog.println("intersect with " + st + ":" + lzTmp + ": " + zTmp); + if (!zTmp.isEmpty()) { + // For all reachability graph edges from lzTmp... + int numTrans2 = graph.getList(src2).size(); + for (int iTrans2 = 0; iTrans2 < numTrans2; iTrans2++) { + List> edges2 = graph.getList(src2).get(iTrans2); + int numEdges2 = edges2.size(); + if (numEdges2 < 2) { + //mainLog.println("SKIP"); + continue; + } + for (int iEdge2 = 0; iEdge2 < numEdges2; iEdge2++) { + List dests2 = edges2.get(iEdge2); + int numDests2 = dests2.size(); + for (int iDest2 = 0; iDest2 < numDests2; iDest2++) { + int dest2 = dests2.get(iDest2); + // Edge (src2, iTrans2, iEdge2, dest2) + + // add state + + LocZone lz3 = new LocZone(lzSrc.loc, zTmp); + if (found.add(lz3)) { + //mainLog.println("Added2 " + Yset.getIndexOfLastAdd() + ":" + lz3); + explore.add(lz3); + states.add(lz3); + graph.addState(pta.getTransitions(lz3.loc)); + } else { + //mainLog.println("Reusing " + Yset.getIndexOfLastAdd() + ":" + lz3); + } + // end add state + int src3 = found.getIndexOfLastAdd(); + //mainLog.println("^D += " + src3 + ":" + lz3 + "->" + dest + ":..."); + graph.addTransition(src3, iTrans, iEdge, dest); + //mainLog.println(src3 + ":" + graph.getList(src3)); + //mainLog.println("^D += " + src3 + ":" + lz3 + "->" + dest2 + ":..."); + graph.addTransition(src3, iTrans2, iEdge2, dest2); + //mainLog.println(src3 + ":" + graph.getList(src3)); + } + } + } + } + } + } + } + } + } + } + // Print some progress info occasionally + if (progress.ready()) + progress.update(found.size()); + } + + // Tidy up progress display + progress.update(found.size()); + progress.end(" states"); + + // Determine which are initial states + // (NB: assume initial location = 0) + int numStates = states.size(); + for (int st = 0; st < numStates; st++) { + if (states.get(st).loc == 0) { + Zone z = states.get(st).zone.deepCopy(); + z.down(); + if (z.includes(DBM.createZero(pta))) + graph.addInitialState(st); + } + } + + // Reachability complete + timer = System.currentTimeMillis() - timer; + mainLog.println("Graph constructed in " + (timer / 1000.0) + " secs."); + mainLog.print("Graph: " + graph.states.size() + " symbolic states"); + mainLog.println(" (" + graph.getInitialStates().size() + " initial, " + graph.getTarget().cardinality() + " target)"); + + return graph; + } +} diff --git a/prism/src/pta/BackwardsReachabilityGraph.java b/prism/src/pta/BackwardsReachabilityGraph.java new file mode 100644 index 00000000..84e07ef9 --- /dev/null +++ b/prism/src/pta/BackwardsReachabilityGraph.java @@ -0,0 +1,252 @@ +//============================================================================== +// +// 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.ArrayList; +import java.util.BitSet; +import java.util.List; + +import prism.PrismException; +import explicit.Distribution; +import explicit.MDP; +import explicit.MDPSimple; + +public class BackwardsReachabilityGraph +{ + public List states; + private List initialStates; + private BitSet target; + private List>>> trans; + + public class Edge + { + int index; // Edge index in transition + int dest; // Destination location + + public Edge(int index, int dest) + { + this.index = index; + this.dest = dest; + } + + @Override + public String toString() + { + return index + "/" + dest; + } + + @Override + public boolean equals(Object o) + { + return o instanceof Edge && ((Edge) o).index == index && ((Edge) o).dest == dest; + } + } + + public BackwardsReachabilityGraph() + { + initialStates = new ArrayList(); + target = new BitSet(); + trans = new ArrayList>>>(); + } + + public void addState(List trs) + { + int numTransitions = trs.size(); + List>> list = new ArrayList>>(numTransitions); + for (int i = 0; i < numTransitions; i++) { + int numEdges = trs.get(i).getNumEdges(); + List> list2 = new ArrayList>(numEdges); + for (int j = 0; j < numEdges; j++) { + list2.add(new ArrayList()); + } + list.add(list2); + } + trans.add(list); + } + + public void addInitialState(int s) + { + initialStates.add(s); + } + + public void addTargetState(int s) + { + target.set(s); + } + + public List getInitialStates() + { + return initialStates; + } + + public BitSet getTarget() + { + return target; + } + + public void addTransition(int src, int tr, int i, int dest) + { + List list = trans.get(src).get(tr).get(i); + if (!list.contains(dest)) + list.add(dest); + } + + public List>> getList(int src) + { + return trans.get(src); + } + + public MDP buildMDP(PTA pta) + { + MDPSimple mdp = new MDPSimple(states.size() + 1); // + sink + int src = -1; + for (List>> list : trans) { + src++; + int tr = -1; + for (List> list2 : list) { + tr++; + Distribution distr = new Distribution(); + double prob, rest = 0; + int j = -1; + for (List dests : list2) { + j++; + prob = pta.getTransitions(states.get(src).loc).get(tr).getEdges().get(j).getProbability(); + if (dests.size() > 1) { + int sNew = mdp.addState(); + distr.add(sNew, prob); + for (int dest : dests) { + Distribution distr2 = new Distribution(); + distr2.add(dest, 1.0); + mdp.addChoice(sNew, distr2); + } + } else if (dests.size() == 1) { + distr.add(dests.get(0), prob); + } else { + rest += prob; + } + } + //if (rest > 0) + // distr.add(mdp.getNumStates() - 1, rest); + mdp.addChoice(src, distr); + } + } + // Add initial states + for (int is : initialStates) { + mdp.addInitialState(is); + } + // fix sink + try { + mdp.findDeadlocks(true); + } catch (PrismException e) { + // Never happens for MDPSimple + } + //log.println(mdp); + return mdp; + } + + public MDP buildMdpExpo(PTA pta) + { + MDPSimple mdp = new MDPSimple(states.size() + 1); // + sink + int src = -1; + for (List>> list : trans) { + src++; + int tr = -1; + for (List> list2 : list) { + tr++; + int dests[] = new int[list2.size()]; + int size = 1; + for (int i = 0; i < list2.size(); i++) { + if (list2.get(i).size() > 0) + size *= list2.get(i).size(); + } + if (size > 6) { + System.out.println(size + "!"); + System.out.println(list2); + for (List list3 : list2) { + for (int x : list3) { + System.out.println(x + ":" + states.get(x)); + } + } + + } + buildMdpExpo(mdp, pta, src, tr, list2, 0, dests); + } + } + // Add initial states + for (int is : initialStates) { + mdp.addInitialState(is); + } + // fix sink + try { + mdp.findDeadlocks(true); + } catch (PrismException e) { + // Never happens for MDPSimple + } + //log.println(mdp); + return mdp; + } + + public void buildMdpExpo(MDPSimple mdp, PTA pta, int src, int tr, List> list2, int i, int dests[]) + { + if (i == dests.length) { + //log.print(src + "/" + tr); + Distribution distr = new Distribution(); + double prob, rest = 0; + if (dests.length > 0) { + for (int j = 0; j < dests.length; j++) { + prob = pta.getTransitions(states.get(src).loc).get(tr).getEdges().get(j).getProbability(); + if (list2.get(j).size() > 0) { + //log.print(" " + prob + ":" + dests[j]); + distr.add(dests[j], prob); + } else { + rest += prob; + } + } + } + //if (rest > 0) + // distr.add(mdp.getNumStates() - 1, rest); + mdp.addChoice(src, distr); + //log.println(); + } else { + List list3 = list2.get(i); + if (list3.size() == 0) { + buildMdpExpo(mdp, pta, src, tr, list2, i + 1, dests); + } else { + for (int j = 0; j < list3.size(); j++) { + dests[i] = list3.get(j); + buildMdpExpo(mdp, pta, src, tr, list2, i + 1, dests); + } + } + } + } + + @Override + public String toString() + { + return trans.toString(); + } +} diff --git a/prism/src/pta/Constraint.java b/prism/src/pta/Constraint.java index d8f4388e..bf58ffdf 100644 --- a/prism/src/pta/Constraint.java +++ b/prism/src/pta/Constraint.java @@ -58,8 +58,7 @@ public class Constraint public int hashCode() { - // Simple hash code - return db; + return (((db * 7) + x) * 7) + y; } public boolean equals(Object o) diff --git a/prism/src/pta/DBM.java b/prism/src/pta/DBM.java index 62eee2c8..afd84e99 100644 --- a/prism/src/pta/DBM.java +++ b/prism/src/pta/DBM.java @@ -373,8 +373,14 @@ public class DBM extends Zone public int hashCode() { - // Simple hash code - return pta.numClocks; + int n = pta.numClocks + 1; + int hash = 0; + for (int i = 0; i < n; i++) { + for (int j = 0; j < n; j++) { + hash = (hash * 7) + d[i][j]; + } + } + return hash; } public boolean equals(Object o) diff --git a/prism/src/pta/DBMList.java b/prism/src/pta/DBMList.java index 026c5665..f9291b6c 100644 --- a/prism/src/pta/DBMList.java +++ b/prism/src/pta/DBMList.java @@ -467,8 +467,11 @@ public class DBMList extends NCZone @Override public int hashCode() { - // Simple hash code - return list.size(); + int hash = 0; + for (DBM dbm : list) { + hash = (hash * 7) + dbm.hashCode(); + } + return hash; } @Override diff --git a/prism/src/pta/LocZone.java b/prism/src/pta/LocZone.java index 35210ac7..c0ebe84c 100644 --- a/prism/src/pta/LocZone.java +++ b/prism/src/pta/LocZone.java @@ -79,6 +79,16 @@ public class LocZone zone.cClosure(pta.getMaxClockConstraint()); } + /** + * Do time part of predecessor operation (not including c-closure). + * Note: pta is passed in just for efficiency, could find it if we wanted. + */ + public void tPre(PTA pta) + { + // Time predecessor (down) + zone.down(pta.getInvariantConstraints(loc)); + } + /** * dPre: discrete predecessor */ @@ -111,8 +121,7 @@ public class LocZone public int hashCode() { - // Simple hash code - return loc; + return loc + zone.hashCode(); } public boolean equals(Object o) diff --git a/prism/src/pta/PTAModelChecker.java b/prism/src/pta/PTAModelChecker.java index 785bf8c8..faa799e6 100644 --- a/prism/src/pta/PTAModelChecker.java +++ b/prism/src/pta/PTAModelChecker.java @@ -313,10 +313,10 @@ public class PTAModelChecker extends PrismComponent return ptaAR.forwardsReachAbstractRefine(pta, targetLocs, null, min); } - // Do probability computation by first constructing a bisimulation - else if (ptaMethod.equals("Bisimulation minimisation")) { - // Not supported yet - throw new PrismException("Not yet supported"); + // Do probability computation through backwards reachability + else if (ptaMethod.equals("Backwards reachability")) { + BackwardsReach ptaBw = new BackwardsReach(this); + return ptaBw.computeProbabilisticReachability(pta, targetLocs, min); } else