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"); }