From 9babbf4bf18b89a6d822e40424595bcae4335959 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Mon, 6 Jul 2015 10:55:36 +0000 Subject: [PATCH] Add explicit.PredecessorRelation class for computing / storing predecessor relation of models. [from Joachim Klein] git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10191 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/explicit/PredecessorRelation.java | 195 ++++++++++++++++++++ 1 file changed, 195 insertions(+) create mode 100644 prism/src/explicit/PredecessorRelation.java diff --git a/prism/src/explicit/PredecessorRelation.java b/prism/src/explicit/PredecessorRelation.java new file mode 100644 index 00000000..7e83560e --- /dev/null +++ b/prism/src/explicit/PredecessorRelation.java @@ -0,0 +1,195 @@ +//============================================================================== +// +// Copyright (c) 2014- +// Authors: +// * Joachim Klein (TU Dresden) +// +//------------------------------------------------------------------------------ +// +// 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 explicit; + +import java.util.ArrayList; +import java.util.BitSet; +import java.util.Iterator; +import java.util.List; +import java.util.Stack; + +import prism.PrismComponent; +import common.IterableBitSet; + +/** + * A class for storing and accessing the predecessor relation of an explicit Model. + *

+ * As Model only provide easy access to successors of states, + * the predecessor relation is computed and stored for subsequent efficient access. + *

+ * Note: Naturally, if the model changes, the predecessor relation + * has to be recomputed to remain accurate. + */ +public class PredecessorRelation +{ + /** + * pre[i] provides the list of predecessors of state with index i. + */ + List> pre; + + /** + * Constructor. Computes the predecessor relation for the given model + * by considering the successors of each state. + * + * @param model the Model + */ + public PredecessorRelation(Model model) + { + pre = new ArrayList>(model.getNumStates()); + // construct the (empty) array list for all states + for (int s = 0; s < model.getNumStates(); s++) { + pre.add(s, new ArrayList()); + } + + compute(model); + } + + /** Compute the predecessor relation using getSuccessorsIterator. */ + private void compute(Model model) + { + int n = model.getNumStates(); + + for (int s = 0; s < n; s++) { + Iterator it = model.getSuccessorsIterator(s); + while (it.hasNext()) { + Integer successor = it.next(); + + // Add the current state s to pre[successor]. + // + // As getSuccessorsIterator guarantees that + // there are no duplicates in the successors, + // s will be added to successor exactly once. + pre.get(successor).add(s); + } + } + } + + /** + * Get an Iterable over the predecessor states of {@code s}. + */ + public Iterable getPre(int s) + { + return pre.get(s); + } + + /** + * Get an Iterator over the predecessor states of {@code s}. + */ + public Iterator getPredecessorsIterator(int s) + { + return pre.get(s).iterator(); + } + + /** + * Static constructor to compute the predecessor relation for the given model. + * Logs diagnostic information to the log of the given PrismComponent. + * + * @param parent a PrismComponent (for obtaining the log and settings) + * @param model the model for which the predecessor relation should be computed + * @returns the predecessor relation + **/ + public static PredecessorRelation forModel(PrismComponent parent, Model model) + { + long timer = System.currentTimeMillis(); + + parent.getLog().print("Calculating predecessor relation for "+model.getModelType().fullName()+"... "); + parent.getLog().flush(); + + PredecessorRelation pre = new PredecessorRelation(model); + + timer = System.currentTimeMillis() - timer; + parent.getLog().println("done (" + timer / 1000.0 + " seconds)"); + + return pre; + } + + + /** + * Computes the set Pre*(target) via a DFS, i.e., all states that + * are in {@code target} or can reach {@code target} via one or more transitions + * from states contained in {@code remain}. + *
+ * If the parameter {@code remain} is {@code null}, then + * {@code remain} is considered to include all states in the model. + *
+ * If the parameter {@code absorbing} is not {@code null}, + * then the states in {@code absorbing} are considered to be absorbing, + * i.e., to have a single self-loop, disregarding other outgoing edges. + + * @param remain restriction on the states that may occur + * on the path to target, {@code null} = all states + * @param target The set of target states + * @param absorbing (optional) set of states that should be considered to be absorbing, + * i.e., their outgoing edges are ignored, {@code null} = no states + * @return the set of states Pre*(target) + */ + public BitSet calculatePreStar(BitSet remain, BitSet target, BitSet absorbing) + { + BitSet result; + + // all target states are in Pre* + result = (BitSet)target.clone(); + + // the stack of states whose predecessors have to be considered + Stack todo = new Stack(); + + // initial todo: all the target states + for (Integer s : IterableBitSet.getSetBits(target)) { + todo.add(s); + }; + + // the set of states that are finished + BitSet done = new BitSet(); + + while (!todo.isEmpty()) { + int s = todo.pop(); + // already considered? + if (done.get(s)) continue; + + done.set(s); + + // for each predecessor in the graph + for (int p : getPre(s)) { + if (absorbing != null && absorbing.get(p)) { + // predecessor is absorbing, thus the edge is considered to not exist + continue; + } + if (remain == null || remain.get(p)) { + // can reach result (and is in remain) + result.set(p); + if (!done.get(p)) { + // add to stack + todo.add(p); + } + } + } + } + + return result; + } + +}