From 994b6207d9f54874f92acf73657c921eeb758a2e Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Thu, 15 Sep 2016 05:53:17 +0000 Subject: [PATCH] AcceptanceGeneric: add toRabin() and toStreett() methods These methods work for the case where the generic acceptance condition has the required structure or can be easily padded to have the required structure for Rabin / Streett. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11827 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/acceptance/AcceptanceGeneric.java | 366 ++++++++++++++++++++ 1 file changed, 366 insertions(+) diff --git a/prism/src/acceptance/AcceptanceGeneric.java b/prism/src/acceptance/AcceptanceGeneric.java index 2ac902ea..febba209 100644 --- a/prism/src/acceptance/AcceptanceGeneric.java +++ b/prism/src/acceptance/AcceptanceGeneric.java @@ -32,7 +32,10 @@ import java.util.ArrayList; import java.util.BitSet; import java.util.Collections; import java.util.List; +import java.util.Stack; +import acceptance.AcceptanceRabin.RabinPair; +import acceptance.AcceptanceStreett.StreettPair; import prism.PrismException; import prism.PrismNotSupportedException; import jdd.JDDVars; @@ -366,6 +369,369 @@ public class AcceptanceGeneric implements AcceptanceOmega { return this.clone(); } + /** + * Attempt to convert this generic acceptance condition + * to a Rabin condition. If this condition does not have + * the required form (top-level disjunctions with conjunctive pairs), + * returns {@code null}. + *
+ * If the condition does not syntactically have the required + * from but can be easily converted to one (e.g., by converting + * a single Inf(S) to a Fin(emptyset) & Inf(S) etc) or by swapping + * Inf and Fin, this will be done. + *
+ * The BitSets for the state sets are cloned, i.e., modifications of + * the state sets of the returned acceptance condition will not affect + * the original generic acceptance condition. + * + * @param numStates the number of states in the underlying model/automaton (for generating state sets for true) + * @return the generated AcceptanceRabin condition, or false on failure + */ + public AcceptanceRabin toAcceptanceRabin(int numStates) + { + AcceptanceRabin result = new AcceptanceRabin(); + List disjuncts = extractDisjuncts(); + + for (AcceptanceGeneric term : disjuncts) { + RabinPair pair = term.toAcceptanceRabinPair(numStates); + if (pair == null) return null; + result.add(pair); + } + + return result; + } + + /** + * Attempt to convert this generic acceptance to a Rabin pair. + * + * @param numStates the number of states in the underlying model/automaton (for generating state sets for true) + * @return the generated RabinPair, or false on failure + */ + private RabinPair toAcceptanceRabinPair(int numStates) + { + BitSet L = null, K = null; + switch (getKind()) { + case TRUE: + L = new BitSet(); + K = new BitSet(); + K.set(0, numStates); + break; + case FALSE: + L = new BitSet(); + L.set(0, numStates); + K = new BitSet(); + break; + case AND: { + AcceptanceGeneric left = getLeft(); + AcceptanceGeneric right = getRight(); + + if (left.getKind() == ElementType.INF || left.getKind() == ElementType.INF_NOT) { + // swap + AcceptanceGeneric tmp = left; + left = right; + right = tmp; + } + + switch (left.getKind()) { + case AND: + case OR: + case FALSE: + case TRUE: + case INF: + case INF_NOT: + // not a Rabin condition + return null; + case FIN: + // Fin(A) <=> <>[]!A + // L = A + L = (BitSet) left.getStates().clone(); + break; + case FIN_NOT: + // Fin(!A) <=> <>[]A + // L = !A + L = (BitSet) left.getStates().clone(); + L.flip(0, numStates); + break; + } + + switch (right.getKind()) { + case AND: + case OR: + case FALSE: + case TRUE: + case FIN: + case FIN_NOT: + // not a Rabin condition + return null; + case INF: + // Inf(A) <=> []<>A + // K = A + K = (BitSet) right.getStates().clone(); + break; + case INF_NOT: + // Inf(!A) <=> []<>!A + // K = !A + K = (BitSet) right.getStates().clone(); + K.flip(0, numStates); + break; + } + + break; + } + case FIN: + // Fin(A) <=> <>[]!A & []<> true <=> RabinPair(A, true) + // L = A + L = (BitSet) getStates().clone(); + // K = true + K = new BitSet(); + K.set(0, numStates); + break; + case FIN_NOT: + // Fin(!A) <=> <>[]A & []<> true <=> RabinPair(!A, true) + // L = !A + L = (BitSet) getStates().clone(); + L.flip(0, numStates); + // K = true + K = new BitSet(); + K.set(0, numStates); + break; + case INF: + // Inf(A) <=> <>[]!false & []<> A <=> RabinPair(false, A) + // L = false + L = new BitSet(); + // K = A + K = (BitSet) getStates().clone(); + break; + case INF_NOT: + // Inf(!A) <=> <>[]!false & []<> !A <=> RabinPair(false, !A) + // L = false + L = new BitSet(); + // K = !A + K = (BitSet) getStates().clone(); + K.flip(0, numStates); + break; + case OR: + // not a Rabin pair + return null; + } + + return new AcceptanceRabin.RabinPair(L, K); + } + + /** + * Attempt to convert this generic acceptance condition + * to a Streett condition. If this condition does not have + * the required form (top-level conjunction with disjunctive pairs), + * returns {@code null}. + *
+ * If the condition does not syntactically have the required + * from but can be easily converted to one (e.g., by converting + * a single Inf(S) to a Fin(true) | Inf(S) etc) or by swapping + * Inf and Fin, this will be done. + *
+ * The BitSets for the state sets are cloned, i.e., modifications of + * the state sets of the returned acceptance condition will not affect + * the original generic acceptance condition. + * + * @param numStates the number of states in the underlying model/automaton (for generating state sets for true) + * @return the generated AcceptanceRabin condition, or false on failure + */ + public AcceptanceStreett toAcceptanceStreett(int numStates) + { + AcceptanceStreett result = new AcceptanceStreett(); + List conjuncts = extractConjuncts(); + + for (AcceptanceGeneric term : conjuncts) { + StreettPair pair = term.toAcceptanceStreettPair(numStates); + if (pair == null) return null; + result.add(pair); + } + + return result; + } + + /** + * Attempt to convert this generic acceptance to a Streett pair. + * + * @param numStates the number of states in the underlying model/automaton (for generating state sets for true) + * @return the generated RabinPair, or false on failure + */ + private StreettPair toAcceptanceStreettPair(int numStates) + { + BitSet R = null, G = null; + switch (getKind()) { + case TRUE: + // true = []<> false -> []<> false + R = new BitSet(); + G = new BitSet(); + break; + case FALSE: + // false = []<> true -> []<> false + R = new BitSet(); + R.set(0, numStates); + G = new BitSet(); + break; + case OR: { + AcceptanceGeneric left = getLeft(); + AcceptanceGeneric right = getRight(); + + if (left.getKind() == ElementType.INF || left.getKind() == ElementType.INF_NOT) { + // swap + AcceptanceGeneric tmp = left; + left = right; + right = tmp; + } + + switch (left.getKind()) { + case AND: + case OR: + case FALSE: + case TRUE: + case INF: + case INF_NOT: + // not a Streett condition + return null; + case FIN: + // Fin(A) -> R = A + R = (BitSet) left.getStates().clone(); + break; + case FIN_NOT: + // Fin(!A) -> R = !A + R = (BitSet) left.getStates().clone(); + R.flip(0, numStates); + break; + } + + switch (right.getKind()) { + case AND: + case OR: + case FALSE: + case TRUE: + case FIN: + case FIN_NOT: + // not a Streett condition + return null; + case INF: + // Inf(A) -> G = A + G = (BitSet) right.getStates().clone(); + break; + case INF_NOT: + // Inf(!A) -> G = !A + G = (BitSet) right.getStates().clone(); + G.flip(0, numStates); + break; + } + + break; + } + case FIN: + // Fin(A) <=> []<>A -> []<>false + // R = A + R = (BitSet) getStates().clone(); + // G = false + G = new BitSet(); + break; + case FIN_NOT: + // Fin(!A) <=> []<>!A -> []<>false + // R = !A + R = (BitSet) getStates().clone(); + R.flip(0, numStates); + // G = false + G = new BitSet(); + break; + case INF: + // Inf(A) <=> []<>true -> []<>A + // R = true + R = new BitSet(); + R.set(0, numStates); + // G = A + G = (BitSet) getStates().clone(); + break; + case INF_NOT: + // Inf(!A) <=> []<>true -> []<>!A + // R = true + R = new BitSet(); + R.set(0, numStates); + // G = !A + G = (BitSet) getStates().clone(); + G.flip(0, numStates); + break; + case AND: + // not a Streett pair + return null; + } + + return new AcceptanceStreett.StreettPair(R,G); + } + + /** + * Extract the operands of the top-level disjunctions, e.g., + * for (A & B) | (C | D)) would return the list [A&B,C,D]. + */ + public List extractDisjuncts() + { + ArrayList result = new ArrayList(); + Stack todo = new Stack(); + + todo.add(this); + while (!todo.isEmpty()) { + AcceptanceGeneric current = todo.pop(); + switch (current.getKind()) { + case AND: + case FALSE: + case TRUE: + case FIN: + case FIN_NOT: + case INF: + case INF_NOT: + // not a top level disjunction, add to list + result.add(current); + break; + case OR: + // still a top level disjunction, recurse + todo.push(current.getRight()); + todo.push(current.getLeft()); + break; + } + } + + return result; + } + + /** + * Extract the operands of the top-level conjunctions, e.g., + * for (A | B) & (C & D)) would return the list [A|B,C,D]. + */ + public List extractConjuncts() + { + ArrayList result = new ArrayList(); + Stack todo = new Stack(); + + todo.add(this); + while (!todo.isEmpty()) { + AcceptanceGeneric current = todo.pop(); + switch (current.getKind()) { + case OR: + case FALSE: + case TRUE: + case FIN: + case FIN_NOT: + case INF: + case INF_NOT: + // not a top level conjunction, add to list + result.add(current); + break; + case AND: + // still a top level conjunction, recurse + todo.push(current.getRight()); + todo.push(current.getLeft()); + break; + } + } + + return result; + } + @Override public String toString() { switch(kind) {