Browse Source

acceptance: add / cleanup complementation to AcceptanceGeneric

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11113 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Joachim Klein 10 years ago
parent
commit
da3761dd5d
  1. 9
      prism/src/acceptance/AcceptanceRabin.java
  2. 8
      prism/src/acceptance/AcceptanceReach.java
  3. 11
      prism/src/acceptance/AcceptanceStreett.java

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

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

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

Loading…
Cancel
Save