From da3761dd5d6bace00a023b363344b988eee697e7 Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Wed, 6 Jan 2016 09:26:53 +0000 Subject: [PATCH] acceptance: add / cleanup complementation to AcceptanceGeneric git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11113 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/acceptance/AcceptanceRabin.java | 9 +++++++++ prism/src/acceptance/AcceptanceReach.java | 8 +++++++- prism/src/acceptance/AcceptanceStreett.java | 11 ++++++++++- 3 files changed, 26 insertions(+), 2 deletions(-) diff --git a/prism/src/acceptance/AcceptanceRabin.java b/prism/src/acceptance/AcceptanceRabin.java index b4759e29..a76a35d3 100644 --- a/prism/src/acceptance/AcceptanceRabin.java +++ b/prism/src/acceptance/AcceptanceRabin.java @@ -195,12 +195,21 @@ public class AcceptanceRabin return accStreett; } + /** 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.STREETT)) { return complementToStreett(); } + if (AcceptanceType.contains(allowedAcceptance, AcceptanceType.GENERIC)) { + return complementToGeneric(); + } throw new PrismNotSupportedException("Can not complement " + getTypeName() + " acceptance to a supported acceptance type"); } diff --git a/prism/src/acceptance/AcceptanceReach.java b/prism/src/acceptance/AcceptanceReach.java index 906f8d92..b5546824 100644 --- a/prism/src/acceptance/AcceptanceReach.java +++ b/prism/src/acceptance/AcceptanceReach.java @@ -115,6 +115,12 @@ public class AcceptanceReach implements AcceptanceOmega 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 { @@ -123,7 +129,7 @@ public class AcceptanceReach implements AcceptanceOmega } else if (AcceptanceType.contains(allowedAcceptance, AcceptanceType.STREETT)) { return complementToStreett(numStates); } else if (AcceptanceType.contains(allowedAcceptance, AcceptanceType.GENERIC)) { - return new AcceptanceGeneric(AcceptanceGeneric.ElementType.FIN, (BitSet) goalStates.clone()); + return complementToGeneric(); } throw new PrismNotSupportedException("Can not complement " + getTypeName() + " acceptance to a supported acceptance type"); } diff --git a/prism/src/acceptance/AcceptanceStreett.java b/prism/src/acceptance/AcceptanceStreett.java index 28cd9d32..3172ade4 100644 --- a/prism/src/acceptance/AcceptanceStreett.java +++ b/prism/src/acceptance/AcceptanceStreett.java @@ -197,13 +197,22 @@ public class AcceptanceStreett } return accRabin; } - + + /** 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(); } + if (AcceptanceType.contains(allowedAcceptance, AcceptanceType.GENERIC)) { + return complementToGeneric(); + } throw new PrismNotSupportedException("Can not complement " + getTypeName() + " acceptance to a supported acceptance type"); }