From c77bd235df8fc33afb91858ca84eb5ea99367fbf Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Sat, 31 Jan 2015 14:53:51 +0000 Subject: [PATCH] Add AcceptanceReach, AcceptanceReachDD (for DFA style acceptance). [Joachim Klein] git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@9608 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/acceptance/AcceptanceReach.java | 122 +++++++++++++++++++ prism/src/acceptance/AcceptanceReachDD.java | 125 ++++++++++++++++++++ prism/src/acceptance/AcceptanceType.java | 3 +- 3 files changed, 249 insertions(+), 1 deletion(-) create mode 100644 prism/src/acceptance/AcceptanceReach.java create mode 100644 prism/src/acceptance/AcceptanceReachDD.java diff --git a/prism/src/acceptance/AcceptanceReach.java b/prism/src/acceptance/AcceptanceReach.java new file mode 100644 index 00000000..77209416 --- /dev/null +++ b/prism/src/acceptance/AcceptanceReach.java @@ -0,0 +1,122 @@ +//============================================================================== +// +// 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 acceptance; + +import java.util.BitSet; + +import jdd.JDDVars; + +/** + * A reachability acceptance condition (based on BitSet state sets). + * The acceptance is defined via a set of goal states and + * has to be "upward-closed", i.e., once a goal state has been reached, + * all successor states are goal states as well. + */ +public class AcceptanceReach implements AcceptanceOmega +{ + /** The set of goal states */ + private BitSet goalStates = new BitSet(); + + /** Constructor (no goal states) */ + public AcceptanceReach() + { + } + + /** Constructor (set goal states) */ + public AcceptanceReach(BitSet goalStates) + { + this.goalStates = goalStates; + } + + /** Get the goal state set */ + public BitSet getGoalStates() + { + return goalStates; + } + + /** Set the goal state set */ + public void setGoalStates(BitSet goalStates) + { + this.goalStates = goalStates; + } + + /** Make a copy of the acceptance condition. */ + public AcceptanceReach clone() + { + return new AcceptanceReach((BitSet)goalStates.clone()); + } + + @Override + public boolean isBSCCAccepting(BitSet bscc_states) + { + return bscc_states.intersects(goalStates); + } + + + @Override + public void lift(LiftBitSet lifter) + { + goalStates=lifter.lift(goalStates); + } + + @Override + public AcceptanceReachDD toAcceptanceDD(JDDVars ddRowVars) + { + return new AcceptanceReachDD(this, ddRowVars); + } + + @Override + public String getSignatureForState(int i) + { + return goalStates.get(i) ? "!" : " "; + } + + @Override + public String getSizeStatistics() + { + return goalStates.cardinality()+" goal states"; + } + + @Override + public AcceptanceType getType() + { + return AcceptanceType.REACH; + } + + @Override + public String getTypeAbbreviated() + { + return "F"; + } + + @Override + public String getTypeName() + { + return "Finite"; + } + +} diff --git a/prism/src/acceptance/AcceptanceReachDD.java b/prism/src/acceptance/AcceptanceReachDD.java new file mode 100644 index 00000000..18c85c85 --- /dev/null +++ b/prism/src/acceptance/AcceptanceReachDD.java @@ -0,0 +1,125 @@ +package acceptance; +//============================================================================== +// +//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 +// +//============================================================================== + +import common.IterableBitSet; +import jdd.JDD; +import jdd.JDDNode; +import jdd.JDDVars; + +/** + * A reachability acceptance condition (based on JDD state sets). + * The acceptance is defined via a set of goal states and + * has to be "upward-closed", i.e., once a goal state has been reached, + * all successor states are goal states as well. + */ +public class AcceptanceReachDD implements AcceptanceOmegaDD +{ + /** The goal states */ + private JDDNode goalStates; + + /** + * Constructor, set goalStates. + * Becomes owner of the references of goalStates. + */ + public AcceptanceReachDD(JDDNode goalStates) + { + this.goalStates = goalStates; + } + + /** + * Constructor, from a BitSet-based AcceptanceReach. + * + * @param acceptance the BitSet-based acceptance condition + * @param ddRowVars JDDVars of the row variables corresponding to the bits in the bit set + */ + public AcceptanceReachDD(AcceptanceReach acceptance, JDDVars ddRowVars) + { + goalStates = JDD.Constant(0); + // get BDD based on the goalState bit set + for (int i : IterableBitSet.getSetBits(acceptance.getGoalStates())) { + goalStates = JDD.SetVectorElement(goalStates, ddRowVars, i, 1.0); + } + } + + /** Get a referenced copy of the state set of the goal states. + *
[ REFS: result, DEREFS: none ] + */ + public JDDNode getGoalStates() + { + JDD.Ref(goalStates); + return goalStates; + } + + /** + * Set the goal states. + * Becomes owner of the reference to goalStates. + */ + public void setGoalStates(JDDNode goalStates) + { + clear(); + this.goalStates = goalStates; + } + + @Override + public boolean isBSCCAccepting(JDDNode bscc_states) + { + return JDD.AreInterecting(goalStates, bscc_states); + } + + @Override + public String getSizeStatistics() + { + return "one set of goal states"; + } + + @Override + public AcceptanceType getType() + { + return AcceptanceType.REACH; + } + + @Override + public String getTypeAbbreviated() + { + return "F"; + } + + @Override + public String getTypeName() + { + return "Finite"; + } + + @Override + public void clear() + { + if (goalStates != null) { + JDD.Deref(goalStates); + } + } + +} diff --git a/prism/src/acceptance/AcceptanceType.java b/prism/src/acceptance/AcceptanceType.java index 6cebe7c2..a3d53730 100644 --- a/prism/src/acceptance/AcceptanceType.java +++ b/prism/src/acceptance/AcceptanceType.java @@ -31,7 +31,8 @@ package acceptance; */ public enum AcceptanceType { RABIN, - STREETT; + STREETT, + REACH; /** * Check whether an array of AcceptanceTypes contains a specific element.