From cbeefa64656af8eb83474ebd480c5e4cd6c93cff Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Fri, 14 Jul 2017 16:06:14 +0000 Subject: [PATCH] symbolic acceptance: provide intersect() method to allow restriction of the state sets E.g., to restrict to the reachable states. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12040 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/acceptance/AcceptanceBuchiDD.java | 6 +++++ .../src/acceptance/AcceptanceGenRabinDD.java | 22 +++++++++++++++++++ prism/src/acceptance/AcceptanceGenericDD.java | 22 +++++++++++++++++++ prism/src/acceptance/AcceptanceOmegaDD.java | 8 +++++++ prism/src/acceptance/AcceptanceRabinDD.java | 20 +++++++++++++++++ prism/src/acceptance/AcceptanceReachDD.java | 6 +++++ prism/src/acceptance/AcceptanceStreettDD.java | 20 +++++++++++++++++ 7 files changed, 104 insertions(+) diff --git a/prism/src/acceptance/AcceptanceBuchiDD.java b/prism/src/acceptance/AcceptanceBuchiDD.java index d94be344..ad45f52a 100644 --- a/prism/src/acceptance/AcceptanceBuchiDD.java +++ b/prism/src/acceptance/AcceptanceBuchiDD.java @@ -99,6 +99,12 @@ public class AcceptanceBuchiDD implements AcceptanceOmegaDD return new AcceptanceBuchiDD(acceptingStates.copy()); } + @Override + public void intersect(JDDNode restrict) + { + acceptingStates = JDD.And(acceptingStates, restrict.copy()); + } + @Override public String getSizeStatistics() { diff --git a/prism/src/acceptance/AcceptanceGenRabinDD.java b/prism/src/acceptance/AcceptanceGenRabinDD.java index 194d241d..aa8f6564 100644 --- a/prism/src/acceptance/AcceptanceGenRabinDD.java +++ b/prism/src/acceptance/AcceptanceGenRabinDD.java @@ -153,6 +153,20 @@ public class AcceptanceGenRabinDD return new AcceptanceGenericDD(AcceptanceGeneric.ElementType.AND, genericL, genericKs); } + /** + * Replaces the BDD functions for the acceptance sets + * of this generalized Rabin pair with the intersection + * of the current acceptance sets and the function {@code restrict}. + *
[ REFS: none, DEREFS: none ] + */ + public void intersect(JDDNode restrict) + { + L = JDD.And(L, restrict.copy()); + for (int i = 0; i < K_list.size(); i++) { + K_list.set(i, JDD.And(K_list.get(i), restrict.copy())); + } + } + /** Returns a textual representation of this Rabin pair. */ @Override public String toString() @@ -221,6 +235,14 @@ public class AcceptanceGenRabinDD return result; } + @Override + public void intersect(JDDNode restrict) + { + for (GenRabinPairDD pair : this) { + pair.intersect(restrict); + } + } + @Override public void clear() { diff --git a/prism/src/acceptance/AcceptanceGenericDD.java b/prism/src/acceptance/AcceptanceGenericDD.java index 418208c5..525c68b2 100644 --- a/prism/src/acceptance/AcceptanceGenericDD.java +++ b/prism/src/acceptance/AcceptanceGenericDD.java @@ -176,6 +176,28 @@ public class AcceptanceGenericDD implements AcceptanceOmegaDD { throw new UnsupportedOperationException("Unsupported operator in generic acceptance expression"); } + @Override + public void intersect(JDDNode restrict) + { + switch(kind) { + case TRUE: + case FALSE: + return; + case AND: + case OR: + left.intersect(restrict); + right.intersect(restrict); + return; + case INF: + case INF_NOT: + case FIN: + case FIN_NOT: + states = JDD.And(states, restrict.copy()); + } + throw new UnsupportedOperationException("Unsupported operator in generic acceptance expression"); + } + + @Override public AcceptanceGenericDD clone() { diff --git a/prism/src/acceptance/AcceptanceOmegaDD.java b/prism/src/acceptance/AcceptanceOmegaDD.java index 0005a4e3..b8b830a6 100644 --- a/prism/src/acceptance/AcceptanceOmegaDD.java +++ b/prism/src/acceptance/AcceptanceOmegaDD.java @@ -47,6 +47,14 @@ public interface AcceptanceOmegaDD extends Cloneable */ public AcceptanceOmegaDD clone(); + /** + * Replaces the BDD functions for all the acceptance sets + * of this acceptance condition with the intersection + * of the current acceptance sets and the function {@code restrict}. + *
[ REFS: none, DEREFS: none ] + */ + public void intersect(JDDNode restrict); + /** * Get a string describing the acceptance condition's size, * i.e. "x Rabin pairs", etc. diff --git a/prism/src/acceptance/AcceptanceRabinDD.java b/prism/src/acceptance/AcceptanceRabinDD.java index 8fb51204..b59ff6d2 100644 --- a/prism/src/acceptance/AcceptanceRabinDD.java +++ b/prism/src/acceptance/AcceptanceRabinDD.java @@ -130,6 +130,18 @@ public class AcceptanceRabinDD return new AcceptanceGenericDD(AcceptanceGeneric.ElementType.AND, genericL, genericK); } + /** + * Replaces the BDD functions for the acceptance sets + * of this Rabin pair with the intersection + * of the current acceptance sets and the function {@code restrict}. + *
[ REFS: none, DEREFS: none ] + */ + public void intersect(JDDNode restrict) + { + L = JDD.And(L, restrict.copy()); + K = JDD.And(K, restrict.copy()); + } + /** Returns a textual representation of this Rabin pair. */ @Override public String toString() @@ -189,6 +201,14 @@ public class AcceptanceRabinDD return result; } + @Override + public void intersect(JDDNode restrict) + { + for (RabinPairDD pair : this) { + pair.intersect(restrict); + } + } + /** * 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. diff --git a/prism/src/acceptance/AcceptanceReachDD.java b/prism/src/acceptance/AcceptanceReachDD.java index e80b2333..36fc034f 100644 --- a/prism/src/acceptance/AcceptanceReachDD.java +++ b/prism/src/acceptance/AcceptanceReachDD.java @@ -99,6 +99,12 @@ public class AcceptanceReachDD implements AcceptanceOmegaDD return new AcceptanceReachDD(goalStates.copy()); } + @Override + public void intersect(JDDNode restrict) + { + goalStates = JDD.And(goalStates, restrict.copy()); + } + @Override public String getSizeStatistics() { diff --git a/prism/src/acceptance/AcceptanceStreettDD.java b/prism/src/acceptance/AcceptanceStreettDD.java index 8c2f9cc2..4d25d32b 100644 --- a/prism/src/acceptance/AcceptanceStreettDD.java +++ b/prism/src/acceptance/AcceptanceStreettDD.java @@ -132,6 +132,18 @@ public class AcceptanceStreettDD return new AcceptanceGenericDD(AcceptanceGeneric.ElementType.OR, genericR, genericG); } + /** + * Replaces the BDD functions for the acceptance sets + * of this Streett pair with the intersection + * of the current acceptance sets and the function {@code restrict}. + *
[ REFS: none, DEREFS: none ] + */ + public void intersect(JDDNode restrict) + { + R = JDD.And(R, restrict.copy()); + G = JDD.And(G, restrict.copy()); + } + @Override public String toString() { @@ -191,6 +203,14 @@ public class AcceptanceStreettDD } + @Override + public void intersect(JDDNode restrict) + { + for (StreettPairDD pair : this) { + pair.intersect(restrict); + } + } + @Override public void clear() {