From 4c527de9d04c16f2a2311c20d5ad4a69a09d8e1e Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Fri, 12 Feb 2016 14:10:55 +0000 Subject: [PATCH] add AcceptanceBuchi as acceptance type git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11191 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/acceptance/AcceptanceBuchi.java | 227 ++++++++++++++++++++ prism/src/acceptance/AcceptanceBuchiDD.java | 127 +++++++++++ prism/src/acceptance/AcceptanceType.java | 1 + 3 files changed, 355 insertions(+) create mode 100644 prism/src/acceptance/AcceptanceBuchi.java create mode 100644 prism/src/acceptance/AcceptanceBuchiDD.java diff --git a/prism/src/acceptance/AcceptanceBuchi.java b/prism/src/acceptance/AcceptanceBuchi.java new file mode 100644 index 00000000..9a8df797 --- /dev/null +++ b/prism/src/acceptance/AcceptanceBuchi.java @@ -0,0 +1,227 @@ +//============================================================================== +// +// Copyright (c) 2016- +// 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.io.PrintStream; +import java.util.BitSet; + +import prism.PrismException; +import prism.PrismNotSupportedException; +import jdd.JDDVars; + +/** + * A Büchi acceptance condition (based on BitSet state sets). + * The acceptance is defined via a set of "accepting" states + * (sometimes also called final states) and is accepting if + * "infinitely often an accepting state is visited" + */ +public class AcceptanceBuchi implements AcceptanceOmega +{ + /** The set of goal states */ + private BitSet acceptingStates = new BitSet(); + + /** Constructor (no accepting states) */ + public AcceptanceBuchi() + { + } + + /** Constructor (set accepting states) */ + public AcceptanceBuchi(BitSet acceptingStates) + { + this.acceptingStates = acceptingStates; + } + + /** Get the accepting state set */ + public BitSet getAcceptingStates() + { + return acceptingStates; + } + + /** Set the accepting state set */ + public void setAcceptingStates(BitSet acceptingStates) + { + this.acceptingStates = acceptingStates; + } + + /** Make a copy of the acceptance condition. */ + public AcceptanceBuchi clone() + { + return new AcceptanceBuchi((BitSet)acceptingStates.clone()); + } + + @Override + public boolean isBSCCAccepting(BitSet bscc_states) + { + return bscc_states.intersects(acceptingStates); + } + + /** + * Get the Rabin acceptance condition that is the equivalent of this Buchi condition. + */ + public AcceptanceRabin toRabin(int numStates) + { + AcceptanceRabin rabin = new AcceptanceRabin(); + rabin.add(new AcceptanceRabin.RabinPair(new BitSet(), (BitSet) acceptingStates.clone())); + return rabin; + } + + /** + * Get the Streett acceptance condition that is the equivalent of this Buchi condition. + */ + public AcceptanceStreett toStreett(int numStates) + { + AcceptanceStreett streett = new AcceptanceStreett(); + BitSet allStates = new BitSet(); + allStates.set(0, numStates); + streett.add(new AcceptanceStreett.StreettPair(allStates, (BitSet) acceptingStates.clone())); + return streett; + } + + /** + * Get a Rabin acceptance condition that is the complement of this condition, i.e., + * any word that is accepted by this condition is rejected by the returned Rabin condition. + * + * @param numStates the number of states in the underlying model / automaton (needed for complementing BitSets) + * @return the complement Rabin acceptance condition + */ + public AcceptanceRabin complementToRabin(int numStates) + { + AcceptanceRabin rabin = new AcceptanceRabin(); + BitSet allStates = new BitSet(); + allStates.set(0, numStates); + rabin.add(new AcceptanceRabin.RabinPair((BitSet) acceptingStates.clone(), allStates)); + return rabin; + } + + /** + * Get a Streett acceptance condition that is the complement of this condition, i.e., + * any word that is accepted by this condition is rejected by the returned Streett condition. + *
+ * Relies on the fact that once the goal states have been reached, all subsequent states + * are goal states. + * + * @param numStates the number of states in the underlying model / automaton (needed for complementing BitSets) + * @return the complement Streett acceptance condition + */ + public AcceptanceStreett complementToStreett(int numStates) + { + AcceptanceStreett streett = new AcceptanceStreett(); + streett.add(new AcceptanceStreett.StreettPair((BitSet) acceptingStates.clone(), new BitSet())); + return streett; + } + + /** Complement this acceptance condition, return as AcceptanceGeneric. */ + public AcceptanceGeneric complementToGeneric() + { + return toAcceptanceGeneric().complementToGeneric(); + } + + @Override + public AcceptanceOmega complement(int numStates, AcceptanceType... allowedAcceptance) throws PrismException + { + if (AcceptanceType.contains(allowedAcceptance, AcceptanceType.RABIN)) { + return complementToRabin(numStates); + } else if (AcceptanceType.contains(allowedAcceptance, AcceptanceType.STREETT)) { + return complementToStreett(numStates); + } else if (AcceptanceType.contains(allowedAcceptance, AcceptanceType.GENERIC)) { + return complementToGeneric(); + } + throw new PrismNotSupportedException("Can not complement " + getTypeName() + " acceptance to a supported acceptance type"); + } + + @Override + public void lift(LiftBitSet lifter) + { + acceptingStates=lifter.lift(acceptingStates); + } + + @Override + public AcceptanceBuchiDD toAcceptanceDD(JDDVars ddRowVars) + { + return new AcceptanceBuchiDD(this, ddRowVars); + } + + @Override + public AcceptanceGeneric toAcceptanceGeneric() + { + return new AcceptanceGeneric(AcceptanceGeneric.ElementType.INF, (BitSet) acceptingStates.clone()); + } + + @Override + public String getSignatureForState(int i) + { + return acceptingStates.get(i) ? "!" : " "; + } + + @Override + public String getSignatureForStateHOA(int stateIndex) + { + if (acceptingStates.get(stateIndex)) { + return "{0}"; + } else { + return ""; + } + } + + /** Returns a textual representation of this acceptance condition. */ + @Override + public String toString() + { + return acceptingStates.toString(); + } + + @Override + public String getSizeStatistics() + { + return acceptingStates.cardinality()+" accepting states"; + } + + @Override + public AcceptanceType getType() + { + return AcceptanceType.BUCHI; + } + + @Override + public String getTypeAbbreviated() + { + return "B"; + } + + @Override + public String getTypeName() + { + return "Buchi"; + } + + @Override + public void outputHOAHeader(PrintStream out) + { + out.println("acc-name: Buchi"); + out.println("Acceptance: 1 Inf(0)"); + } +} diff --git a/prism/src/acceptance/AcceptanceBuchiDD.java b/prism/src/acceptance/AcceptanceBuchiDD.java new file mode 100644 index 00000000..177520ee --- /dev/null +++ b/prism/src/acceptance/AcceptanceBuchiDD.java @@ -0,0 +1,127 @@ +//============================================================================== +// +//Copyright (c) 2016- +//Authors: +// * Joachim Klein (TU Dresden) +// * Dave Parker (University of Birmingham/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 acceptance; + +import common.IterableBitSet; +import jdd.JDD; +import jdd.JDDNode; +import jdd.JDDVars; + +/** + * A Büchi acceptance condition (based on JDD state sets). + * The acceptance is defined via a set of "accepting" states + * (sometimes also called final states) and is accepting if + * "infinitely often an accepting state is visited" + */ +public class AcceptanceBuchiDD implements AcceptanceOmegaDD +{ + /** The accepting states */ + private JDDNode acceptingStates; + + /** + * Constructor, set acceptingStates. + * Becomes owner of the references of acceptingStates. + */ + public AcceptanceBuchiDD(JDDNode acceptingStates) + { + this.acceptingStates = acceptingStates; + } + + /** + * Constructor, from a BitSet-based AcceptanceBuchi. + * + * @param acceptance the BitSet-based acceptance condition + * @param ddRowVars JDDVars of the row variables corresponding to the bits in the bit set + */ + public AcceptanceBuchiDD(AcceptanceBuchi acceptance, JDDVars ddRowVars) + { + acceptingStates = JDD.Constant(0); + // get BDD based on the acceptingState bit set + for (int i : IterableBitSet.getSetBits(acceptance.getAcceptingStates())) { + acceptingStates = JDD.SetVectorElement(acceptingStates, ddRowVars, i, 1.0); + } + } + + /** Get a referenced copy of the state set of the accepting states. + *
[ REFS: result, DEREFS: none ] + */ + public JDDNode getAcceptingStates() + { + JDD.Ref(acceptingStates); + return acceptingStates; + } + + /** + * Set the accepting states. + * Becomes owner of the reference to acceptingStates. + */ + public void setAcceptingStates(JDDNode acceptingStates) + { + clear(); + this.acceptingStates = acceptingStates; + } + + @Override + public boolean isBSCCAccepting(JDDNode bscc_states) + { + return JDD.AreIntersecting(acceptingStates, bscc_states); + } + + @Override + public String getSizeStatistics() + { + return "one set of accepting states"; + } + + @Override + public AcceptanceType getType() + { + return AcceptanceType.BUCHI; + } + + @Override + public String getTypeAbbreviated() + { + return "B"; + } + + @Override + public String getTypeName() + { + return "Buchi"; + } + + @Override + public void clear() + { + if (acceptingStates != null) { + JDD.Deref(acceptingStates); + } + } + +} diff --git a/prism/src/acceptance/AcceptanceType.java b/prism/src/acceptance/AcceptanceType.java index 2901f1dd..03bb2bde 100644 --- a/prism/src/acceptance/AcceptanceType.java +++ b/prism/src/acceptance/AcceptanceType.java @@ -31,6 +31,7 @@ package acceptance; * An omega-regular acceptance type. */ public enum AcceptanceType { + BUCHI, RABIN, STREETT, REACH,