diff --git a/prism/src/acceptance/AcceptanceOmega.java b/prism/src/acceptance/AcceptanceOmega.java new file mode 100644 index 00000000..d5bf48ca --- /dev/null +++ b/prism/src/acceptance/AcceptanceOmega.java @@ -0,0 +1,85 @@ +//============================================================================== +// +// 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; + +/** + * Generic interface for an omega-regular acceptance condition (BitSet-based). + */ +public interface AcceptanceOmega extends Cloneable +{ + /** Returns true if the bottom strongly connected component (BSSC) + * given by bscc_states is accepting for this acceptance condition. + **/ + public boolean isBSCCAccepting(BitSet bscc_states); + + /** Get the acceptance signature for state i. + **/ + public String getSignatureForState(int i); + + /** + * Get a string describing the acceptance condition's size, + * i.e. "x Rabin pairs", etc. + */ + public String getSizeStatistics(); + + /** Returns the AcceptanceType of this acceptance condition */ + public AcceptanceType getType(); + + /** Returns the type of this acceptance condition as a String, + * i.e., "R" for Rabin + */ + public String getTypeAbbreviated(); + + /** Returns a full name for this acceptance condition */ + public String getTypeName(); + + /** Make a copy of the acceptance condition. */ + public AcceptanceOmega clone(); + + /** Abstract functor for use with the lift function. */ + public static abstract class LiftBitSet { + public abstract BitSet lift(BitSet states); + }; + + /** + * Lift the state sets in the acceptance condition. + * For each state set {@code states} in the condition, + * {@code lifter.lift(states)} is called and the state set is + * replaced by the result. + **/ + public void lift(LiftBitSet lifter); + + /** + * Convert this BitSet based acceptance condition to the corresponding BDD based acceptance condition. + * @param ddRowVars JDDVars of the row variables corresponding to the bits in the bitset + */ + public AcceptanceOmegaDD toAcceptanceDD(JDDVars ddRowVars); +} diff --git a/prism/src/acceptance/AcceptanceOmegaDD.java b/prism/src/acceptance/AcceptanceOmegaDD.java new file mode 100644 index 00000000..f4d6cb8f --- /dev/null +++ b/prism/src/acceptance/AcceptanceOmegaDD.java @@ -0,0 +1,65 @@ +//============================================================================== +// +// 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 jdd.JDDNode; + +/** + * Generic interface for an omega-regular acceptance condition (BDD-based). + */ +public interface AcceptanceOmegaDD +{ + /** Returns true if the bottom strongly connected component (BSSC) + * given by bscc_states is accepting for this acceptance condition. + *
[ REFS: none, DEREFS: none ] + **/ + public boolean isBSCCAccepting(JDDNode bscc_states); + + /** + * Get a string describing the acceptance condition's size, + * i.e. "x Rabin pairs", etc. + */ + public String getSizeStatistics(); + + /** Returns the AcceptanceType of this acceptance condition */ + public AcceptanceType getType(); + + /** Returns the type of this acceptance condition as a String, + * i.e., "R" for Rabin + */ + public String getTypeAbbreviated(); + + /** + * Clear the resources used by this acceptance condition. + * Call to ensure that the JDD based state sets actually get + * dereferenced. + */ + void clear(); + + /** Returns a full name for this acceptance condition */ + public String getTypeName(); +} diff --git a/prism/src/acceptance/AcceptanceRabin.java b/prism/src/acceptance/AcceptanceRabin.java new file mode 100644 index 00000000..7c855c41 --- /dev/null +++ b/prism/src/acceptance/AcceptanceRabin.java @@ -0,0 +1,256 @@ +//============================================================================== +// +// 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.ArrayList; +import java.util.BitSet; + +import jdd.JDDVars; + +/** + * A Rabin acceptance condition (based on BitSet state sets). + * This is a list of RabinPairs, which can be manipulated with the usual List interface. + *
+ * Semantics: Each Rabin pair has a state set L and K and is accepting iff + * L is not visited infinitely often and K is visited infinitely often: + * (F G !"L") & (G F "K"). + * + * The Rabin condition is accepting if at least one of the pairs is accepting. + */ +@SuppressWarnings("serial") +public class AcceptanceRabin + extends ArrayList + implements AcceptanceOmega +{ + + /** + * A pair in a Rabin acceptance condition, i.e., with + * (F G !"L") & (G F "K") + **/ + public static class RabinPair { + /** State set L (should be visited only finitely often) */ + private BitSet L; + + /** State set K (should be visited infinitely often) */ + private BitSet K; + + /** Constructor with L and K state sets */ + public RabinPair(BitSet L, BitSet K) { + this.L = L; + this.K = K; + } + + /** Get the state set L */ + public BitSet getL() + { + return L; + } + + /** Get the state set K */ + public BitSet getK() + { + return K; + } + + /** Returns true if the bottom strongly connected component + * given by bscc_states is accepting for this pair. + */ + public boolean isBSCCAccepting(BitSet bscc_states) + { + if (L.intersects(bscc_states)) { + // there is some state in bscc_states that is + // forbidden by L + return false; + } + + if (K.intersects(bscc_states)) { + // there is some state in bscc_states that is + // contained in K -> infinitely often visits to K + return true; + } + + return false; + } + + /** Generate signature for this Rabin pair and the given state. + * If the state is a member of L, returns "-pairIndex". + * If the state is a member of K, returns "+pairIndex". + * @param stateIndex the state index + * @param pairIndex the index of this Rabin pair + **/ + public String getSignatureForState(int stateIndex, int pairIndex) + { + if (L.get(stateIndex)) { + return "-"+pairIndex; + } else if (K.get(stateIndex)) { + return "+"+pairIndex; + } else { + return ""; + } + } + + @Override + public RabinPair clone() + { + return new RabinPair((BitSet)L.clone(), (BitSet)K.clone()); + } + + /** Returns a textual representation of this Rabin pair. */ + @Override + public String toString() { + return "(" + L + "," + K + ")"; + } + } + + /** Make a copy of the acceptance condition. */ + public AcceptanceRabin clone() + { + AcceptanceRabin result = new AcceptanceRabin(); + for (RabinPair pair : this) { + result.add(pair.clone()); + } + + return result; + } + + /** Returns true if the bottom strongly connected component + * given by bscc_states is accepting for this Rabin condition, + * i.e., there is a pair that accepts for bscc_states. + */ + public boolean isBSCCAccepting(BitSet bscc_states) + { + for (RabinPair pair : this) { + if (pair.isBSCCAccepting(bscc_states)) { + return true; + } + } + + return false; + } + + @Override + public void lift(LiftBitSet lifter) { + for (RabinPair pair : this) { + pair.L = lifter.lift(pair.L); + pair.K = lifter.lift(pair.K); + } + } + + /** + * Get the Streett acceptance condition that is the dual of this Rabin acceptance condition, i.e., + * any word that is accepted by this condition is rejected by the returned Streett condition. + * @return the complement Streett acceptance condition + */ + public AcceptanceStreett complement() + { + AcceptanceStreett accRabin = new AcceptanceStreett(); + + for (RabinPair accPairRabin : this) { + BitSet R = (BitSet) accPairRabin.getK().clone(); + BitSet G = (BitSet) accPairRabin.getL().clone(); + AcceptanceStreett.StreettPair accPairStreett = new AcceptanceStreett.StreettPair(R, G); + accRabin.add(accPairStreett); + } + + return accRabin; + } + + /** + * Returns a new Rabin acceptance condition that corresponds to the disjunction + * of this and the other Rabin acceptance condition. The RabinPairs are cloned, i.e., + * not shared with the argument acceptance condition. + * @param other the other Rabin acceptance condition + * @return new AcceptanceRabin, disjunction of this and other + */ + public AcceptanceRabin or(AcceptanceRabin other) + { + AcceptanceRabin result = new AcceptanceRabin(); + for (RabinPair pair : this) { + result.add((RabinPair) pair.clone()); + } + for (RabinPair pair : other) { + result.add((RabinPair) pair.clone()); + } + return result; + } + + @Override + public AcceptanceRabinDD toAcceptanceDD(JDDVars ddRowVars) + { + return new AcceptanceRabinDD(this, ddRowVars); + } + + /** + * Get the acceptance signature for state stateIndex. + **/ + public String getSignatureForState(int stateIndex) + { + String result = ""; + + for (int pairIndex=0; pairIndex (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.ArrayList; + +import common.IterableBitSet; + +import jdd.JDD; +import jdd.JDDNode; +import jdd.JDDVars; + +/** + * A Rabin acceptance condition (based on JDD state sets) + * This is a list of RabinPairs, which can be manipulated with the usual List interface. + *
+ * Semantics: Each Rabin pair has a state set L and K and is accepting iff + * L is not visited infinitely often and K is visited infinitely often: + * (F G !"L") & (G F "K"). + * + * The Rabin condition is accepting if at least one of the pairs is accepting. + */ +@SuppressWarnings("serial") +public class AcceptanceRabinDD + extends ArrayList + implements AcceptanceOmegaDD +{ + + /** + * A pair in a Rabin acceptance condition, i.e., with + * (F G !"L") & (G F "K") + **/ + public static class RabinPairDD { + /** State set L (should be visited only finitely often) */ + private JDDNode L; + + /** State set K (should be visited infinitely often) */ + private JDDNode K; + + /** + * Constructor with L and K state sets. + * Becomes owner of the references of L and K. + */ + public RabinPairDD(JDDNode L, JDDNode K) + { + this.L = L; + this.K = K; + } + + /** Clear resources of the state sets */ + public void clear() + { + if (L!=null) JDD.Deref(L); + if (K!=null) JDD.Deref(K); + } + + /** Get a referenced copy of the state set L. + *
[ REFS: result, DEREFS: none ] + */ + public JDDNode getL() + { + JDD.Ref(L); + return L; + } + + /** Get a referenced copy of the state set K. + *
[ REFS: result, DEREFS: none ] + */ + public JDDNode getK() + { + JDD.Ref(K); + return K; + } + + /** Returns true if the bottom strongly connected component + * given by bscc_states is accepting for this pair. + */ + public boolean isBSCCAccepting(JDDNode bscc_states) + { + if (JDD.AreInterecting(L, bscc_states)) { + // there is some state in bscc_states that is + // forbidden by L + return false; + } + + if (JDD.AreInterecting(K, bscc_states)) { + // there is some state in bscc_states that is + // contained in K -> infinitely often visits to K + return true; + } + + return false; + } + + /** Returns a textual representation of this Rabin pair. */ + @Override + public String toString() + { + return "(" + L + "," + K + ")"; + } + } + + /** + * Constructor, from a BitSet-based AcceptanceRabin. + * + * @param acceptance the BitSet-based acceptance condition + * @param ddRowVars JDDVars of the row variables corresponding to the bits in the bit set + */ + public AcceptanceRabinDD(AcceptanceRabin acceptance, JDDVars ddRowVars) + { + for (AcceptanceRabin.RabinPair pair : acceptance) { + // get BDD based newL and newK from the bit sets + JDDNode newL = JDD.Constant(0); + for (int i : IterableBitSet.getSetBits(pair.getL())) { + newL = JDD.SetVectorElement(newL, ddRowVars, i, 1.0); + } + + JDDNode newK = JDD.Constant(0); + for (int i : IterableBitSet.getSetBits(pair.getK())) { + newK = JDD.SetVectorElement(newK, ddRowVars, i, 1.0); + } + + RabinPairDD newPair = new RabinPairDD(newL, newK); + this.add(newPair); + } + } + + /** Returns true if the bottom strongly connected component + * given by bscc_states is accepting for this Rabin condition, + * i.e., there is a pair that accepts for bscc_states. + */ + public boolean isBSCCAccepting(JDDNode bscc_states) + { + for (RabinPairDD pair : this) { + if (pair.isBSCCAccepting(bscc_states)) { + return true; + } + } + return false; + } + + @Override + public void clear() + { + for (RabinPairDD pair : this) { + pair.clear(); + } + super.clear(); + } + + /** Returns a textual representation of this acceptance condition. */ + @Override + public String toString() + { + String result = ""; + for (RabinPairDD pair : this) { + result += pair.toString(); + } + return result; + } + + @Override + public String getSizeStatistics() + { + return size() + " Rabin pairs"; + } + + @Override + public AcceptanceType getType() + { + return AcceptanceType.RABIN; + } + + @Override + public String getTypeAbbreviated() + { + return "R"; + } + + @Override + public String getTypeName() + { + return "Rabin"; + } +} diff --git a/prism/src/acceptance/AcceptanceStreett.java b/prism/src/acceptance/AcceptanceStreett.java new file mode 100644 index 00000000..51dae747 --- /dev/null +++ b/prism/src/acceptance/AcceptanceStreett.java @@ -0,0 +1,257 @@ +//============================================================================== +// +// 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.ArrayList; +import java.util.BitSet; + +import jdd.JDDVars; + +/** + * A Streett acceptance condition (based on BitSet state sets). + * This is a list of StreettPairs, which can be manipulated with the usual List interface. + *
+ * Semantics: Each Streett pair has a state set R and G and is accepting iff + * visiting R infinitely often implies visiting G infinitely often: + * (G F "R") -> (G F "G"). + * + * The Streett condition is accepting if all pairs are accepting. + */ +@SuppressWarnings("serial") +public class AcceptanceStreett + extends ArrayList + implements AcceptanceOmega +{ + + /** + * A pair in a Streett acceptance condition, i.e., with + * (G F "R") -> (G F "G") + **/ + public static class StreettPair { + /** State set R */ + private BitSet R; + + /** State set G */ + private BitSet G; + + /** Constructor with R and G state sets */ + public StreettPair(BitSet R, BitSet G) + { + this.R = R; + this.G = G; + } + + /** Get the state set R */ + public BitSet getR() + { + return R; + } + + /** Get the state set G */ + public BitSet getG() + { + return G; + } + + /** Returns true if the bottom strongly connected component + * given by bscc_states is accepting for this pair. + */ + public boolean isBSCCAccepting(BitSet bscc_states) + { + if (R.intersects(bscc_states)) { + // there is some state in bscc_states + // that is in R, requiring that G is visited + // as well: + if (!G.intersects(bscc_states)) { + return false; + } else { + // G is visited as well + return true; + } + } else { + // no R visited, no need to check for G + return true; + } + } + + /** Generate signature for this Streett pair and the given state. + * If the state is a member of R, returns "-pairIndex". + * If the state is a member of G, returns "+pairIndex". + * @param stateIndex the state index + * @param pairIndex the index of this Streeet pair + **/ + public String getSignatureForState(int stateIndex, int pairIndex) + { + if (G.get(stateIndex)) { + return "+"+pairIndex; + } else if (R.get(stateIndex)) { + return "-"+pairIndex; + } else { + return ""; + } + } + + @Override + public StreettPair clone() + { + return new StreettPair((BitSet)R.clone(), (BitSet)G.clone()); + } + + /** Returns a textual representation of this Streett pair. */ + @Override + public String toString() { + return "(" + R + "->" + G + ")"; + } + } + + /** Make a copy of the acceptance condition. */ + public AcceptanceStreett clone() + { + AcceptanceStreett result = new AcceptanceStreett(); + for (StreettPair pair : this) { + result.add(pair.clone()); + } + + return result; + } + + /** Returns true if the bottom strongly connected component + * given by bscc_states is accepting for this Streett condition, + * i.e., all pairs accept for bscc_states. + */ + @Override + public boolean isBSCCAccepting(BitSet bscc_states) + { + for (StreettPair pair : this) { + if (!pair.isBSCCAccepting(bscc_states)) { + return false; + } + } + return true; + } + + + @Override + public void lift(LiftBitSet lifter) { + for (StreettPair pair : this) { + pair.R = lifter.lift(pair.R); + pair.G = lifter.lift(pair.G); + } + } + + /** + * Get the Rabin acceptance condition that is the dual of this Streett acceptance condition, i.e., + * any word that is accepted by this condition is rejected by the returned Rabin condition. + * @return the complement Rabin acceptance condition + */ + public AcceptanceRabin complement() + { + AcceptanceRabin accRabin = new AcceptanceRabin(); + + for (StreettPair accPairStreett : this) { + BitSet L = (BitSet) accPairStreett.getG().clone(); + BitSet K = (BitSet) accPairStreett.getR().clone(); + AcceptanceRabin.RabinPair accPairRabin = new AcceptanceRabin.RabinPair(L, K); + accRabin.add(accPairRabin); + } + return accRabin; + } + + /** + * Returns a new Streett acceptance condition that corresponds to the conjunction + * of this and the other Streett acceptance condition. The StreettPairs are cloned, i.e., + * not shared with the argument acceptance condition. + * @param other the other Streett acceptance condition + * @return new AcceptanceStreett, conjunction of this and other + */ + public AcceptanceStreett and(AcceptanceStreett other) + { + AcceptanceStreett result = new AcceptanceStreett(); + for (StreettPair pair : this) { + result.add((StreettPair) pair.clone()); + } + for (StreettPair pair : other) { + result.add((StreettPair) pair.clone()); + } + return result; + } + + @Override + public AcceptanceStreettDD toAcceptanceDD(JDDVars ddRowVars) + { + return new AcceptanceStreettDD(this, ddRowVars); + } + + /** + * Get the acceptance signature for state stateIndex. + **/ + public String getSignatureForState(int stateIndex) + { + String result = ""; + + for (int pairIndex=0; pairIndex (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.ArrayList; + +import common.IterableBitSet; + +import jdd.JDD; +import jdd.JDDNode; +import jdd.JDDVars; + +/** + * A Streett acceptance condition (based on JDD state sets). + * This is a list of StreettPairs, which can be manipulated with the usual List interface. + *
+ * Semantics: Each Streett pair has a state set R and G and is accepting iff + * visiting R infinitely often implies visiting G infinitely often: + * (G F "R") -> (G F "G"). + * + * The Streett condition is accepting if all pairs are accepting. + */ +@SuppressWarnings("serial") +public class AcceptanceStreettDD + extends ArrayList + implements AcceptanceOmegaDD +{ + + /** + * A pair in a Streett acceptance condition, i.e., with + * (G F "R") -> (G F "G") + **/ + public static class StreettPair { + /** State set R */ + private JDDNode R; + + /** State set G */ + private JDDNode G; + + /** + * Constructor with R and G state sets. + * Becomes owner of the references of R and G. + */ + public StreettPair(JDDNode R, JDDNode G) + { + this.R = R; + this.G = G; + } + + /** Clear resources of the state sets */ + public void clear() + { + if (R != null) JDD.Deref(R); + if (G != null) JDD.Deref(G); + } + + /** Get a referenced copy of the state set R. + *
[ REFS: result, DEREFS: none ] + */ + public JDDNode getR() + { + JDD.Ref(R); + return R; + } + + /** Get a referenced copy of the state set G. + *
[ REFS: result, DEREFS: none ] + */ + public JDDNode getG() + { + JDD.Ref(G); + return G; + } + + /** Returns true if the bottom strongly connected component + * given by bscc_states is accepting for this pair. + */ + public boolean isBSCCAccepting(JDDNode bscc_states) + { + if (JDD.AreInterecting(R, bscc_states)) { + // there is some state in bscc_states + // that is in R, requiring that G is visited + // as well: + if (!JDD.AreInterecting(G, bscc_states)) { + return false; + } else { + // G is visited as well + return true; + } + } else { + // no R visited, no need to check for G + return true; + } + } + + @Override + public String toString() + { + return "(" + R + "->" + G + ")"; + } + } + + /** + * Constructor, from a BitSet-based AcceptanceStreett. + * + * @param acceptance the BitSet-based acceptance condition + * @param ddRowVars JDDVars of the row variables corresponding to the bits in the bit set + */ + public AcceptanceStreettDD(AcceptanceStreett acceptance, JDDVars ddRowVars) + { + for (AcceptanceStreett.StreettPair pair : acceptance) { + // get BDD based newR and newG from the bit sets + JDDNode newR = JDD.Constant(0); + for (int i : IterableBitSet.getSetBits(pair.getR())) { + newR = JDD.SetVectorElement(newR, ddRowVars, i, 1.0); + } + + JDDNode newG = JDD.Constant(0); + for (int i : IterableBitSet.getSetBits(pair.getG())) { + newG = JDD.SetVectorElement(newG, ddRowVars, i, 1.0); + } + + StreettPair newPair = new StreettPair(newR, newG); + this.add(newPair); + } + } + + @Override + public boolean isBSCCAccepting(JDDNode bscc_states) + { + for (StreettPair pair : this) { + if (!pair.isBSCCAccepting(bscc_states)) { + return false; + } + } + return true; + } + + @Override + public void clear() + { + for (StreettPair pair : this) { + pair.clear(); + } + super.clear(); + } + + @Override + public String toString() { + String result = ""; + for (StreettPair pair : this) { + result += pair.toString(); + } + return result; + } + + @Override + public String getSizeStatistics() + { + return size() + " Streett pairs"; + } + + @Override + public AcceptanceType getType() + { + return AcceptanceType.STREETT; + } + + @Override + public String getTypeAbbreviated() + { + return "S"; + } + + @Override + public String getTypeName() + { + return "Streett"; + } +} diff --git a/prism/src/acceptance/AcceptanceType.java b/prism/src/acceptance/AcceptanceType.java new file mode 100644 index 00000000..6cebe7c2 --- /dev/null +++ b/prism/src/acceptance/AcceptanceType.java @@ -0,0 +1,49 @@ +//============================================================================== +// +// 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; + +/** + * An omega-regular acceptance type. + */ +public enum AcceptanceType { + RABIN, + STREETT; + + /** + * Check whether an array of AcceptanceTypes contains a specific element. + * @param types the array of AcceptanceTypes + * @param type the AcceptanceType that is tested for + */ + public static boolean contains(AcceptanceType[] types, AcceptanceType type) + { + for (AcceptanceType t: types) { + if (t.equals(type)) + return true; + } + return false; + } +}