From 3f5a7490b6fa0d0c05a76da2c078bdccbef7ef6d Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Fri, 12 Feb 2016 14:16:58 +0000 Subject: [PATCH] acceptance: Refactor AcceptanceType (names for the acceptance types) git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11192 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/acceptance/AcceptanceBuchi.java | 8 ++-- prism/src/acceptance/AcceptanceBuchiDD.java | 6 ++- prism/src/acceptance/AcceptanceGenRabin.java | 14 +++--- .../src/acceptance/AcceptanceGenRabinDD.java | 12 ++--- prism/src/acceptance/AcceptanceGeneric.java | 8 ++-- prism/src/acceptance/AcceptanceGenericDD.java | 6 ++- prism/src/acceptance/AcceptanceOmega.java | 11 ++++- prism/src/acceptance/AcceptanceOmegaDD.java | 2 + prism/src/acceptance/AcceptanceRabin.java | 14 +++--- prism/src/acceptance/AcceptanceRabinDD.java | 13 +++-- prism/src/acceptance/AcceptanceReach.java | 14 +++--- prism/src/acceptance/AcceptanceReachDD.java | 12 ++--- prism/src/acceptance/AcceptanceStreett.java | 14 +++--- prism/src/acceptance/AcceptanceStreettDD.java | 12 ++--- prism/src/acceptance/AcceptanceType.java | 48 ++++++++++++++++--- 15 files changed, 123 insertions(+), 71 deletions(-) diff --git a/prism/src/acceptance/AcceptanceBuchi.java b/prism/src/acceptance/AcceptanceBuchi.java index 9a8df797..0b0374e1 100644 --- a/prism/src/acceptance/AcceptanceBuchi.java +++ b/prism/src/acceptance/AcceptanceBuchi.java @@ -150,7 +150,7 @@ public class AcceptanceBuchi implements AcceptanceOmega } else if (AcceptanceType.contains(allowedAcceptance, AcceptanceType.GENERIC)) { return complementToGeneric(); } - throw new PrismNotSupportedException("Can not complement " + getTypeName() + " acceptance to a supported acceptance type"); + throw new PrismNotSupportedException("Can not complement " + getType() + " acceptance to a supported acceptance type"); } @Override @@ -207,15 +207,17 @@ public class AcceptanceBuchi implements AcceptanceOmega } @Override + @Deprecated public String getTypeAbbreviated() { - return "B"; + return getType().getNameAbbreviated(); } @Override + @Deprecated public String getTypeName() { - return "Buchi"; + return getType().getName(); } @Override diff --git a/prism/src/acceptance/AcceptanceBuchiDD.java b/prism/src/acceptance/AcceptanceBuchiDD.java index 177520ee..ebcb163c 100644 --- a/prism/src/acceptance/AcceptanceBuchiDD.java +++ b/prism/src/acceptance/AcceptanceBuchiDD.java @@ -105,15 +105,17 @@ public class AcceptanceBuchiDD implements AcceptanceOmegaDD } @Override + @Deprecated public String getTypeAbbreviated() { - return "B"; + return getType().getNameAbbreviated(); } @Override + @Deprecated public String getTypeName() { - return "Buchi"; + return getType().getName(); } @Override diff --git a/prism/src/acceptance/AcceptanceGenRabin.java b/prism/src/acceptance/AcceptanceGenRabin.java index 17ba5d9b..8a5e5e93 100644 --- a/prism/src/acceptance/AcceptanceGenRabin.java +++ b/prism/src/acceptance/AcceptanceGenRabin.java @@ -204,7 +204,7 @@ public class AcceptanceGenRabin if (AcceptanceType.contains(allowedAcceptance, AcceptanceType.GENERIC)) { return complementToGeneric(); } - throw new PrismNotSupportedException("Can not complement " + getTypeName() + " acceptance to a supported acceptance type"); + throw new PrismNotSupportedException("Can not complement " + getType() + " acceptance to a supported acceptance type"); } @Override @@ -324,15 +324,15 @@ public class AcceptanceGenRabin } @Override - public String getTypeAbbreviated() - { - return "GR"; + @Deprecated + public String getTypeAbbreviated() { + return getType().getNameAbbreviated(); } @Override - public String getTypeName() - { - return "Generalized Rabin"; + @Deprecated + public String getTypeName() { + return getType().getName(); } @Override diff --git a/prism/src/acceptance/AcceptanceGenRabinDD.java b/prism/src/acceptance/AcceptanceGenRabinDD.java index 7c8e51d5..0a889e1b 100644 --- a/prism/src/acceptance/AcceptanceGenRabinDD.java +++ b/prism/src/acceptance/AcceptanceGenRabinDD.java @@ -213,14 +213,14 @@ public class AcceptanceGenRabinDD } @Override - public String getTypeAbbreviated() - { - return "GR"; + @Deprecated + public String getTypeAbbreviated() { + return getType().getNameAbbreviated(); } @Override - public String getTypeName() - { - return "Generalized Rabin"; + @Deprecated + public String getTypeName() { + return getType().getName(); } } diff --git a/prism/src/acceptance/AcceptanceGeneric.java b/prism/src/acceptance/AcceptanceGeneric.java index 10cd934f..5aa8a7d6 100644 --- a/prism/src/acceptance/AcceptanceGeneric.java +++ b/prism/src/acceptance/AcceptanceGeneric.java @@ -225,13 +225,15 @@ public class AcceptanceGeneric implements AcceptanceOmega { } @Override + @Deprecated public String getTypeAbbreviated() { - return ""; + return getType().getNameAbbreviated(); } @Override + @Deprecated public String getTypeName() { - return "generic"; + return getType().getName(); } @Override @@ -287,7 +289,7 @@ public class AcceptanceGeneric implements AcceptanceOmega { if (AcceptanceType.contains(allowedAcceptance, AcceptanceType.GENERIC)) { return this.complementToGeneric(); } - throw new PrismNotSupportedException("Can not complement " + getTypeName() + " acceptance to required acceptance type"); + throw new PrismNotSupportedException("Can not complement " + getType() + " acceptance to required acceptance type"); } @Override diff --git a/prism/src/acceptance/AcceptanceGenericDD.java b/prism/src/acceptance/AcceptanceGenericDD.java index 89797ddd..f82f6c26 100644 --- a/prism/src/acceptance/AcceptanceGenericDD.java +++ b/prism/src/acceptance/AcceptanceGenericDD.java @@ -154,13 +154,15 @@ public class AcceptanceGenericDD implements AcceptanceOmegaDD { } @Override + @Deprecated public String getTypeAbbreviated() { - return ""; + return getType().getNameAbbreviated(); } @Override + @Deprecated public String getTypeName() { - return "generic"; + return getType().getName(); } @Override diff --git a/prism/src/acceptance/AcceptanceOmega.java b/prism/src/acceptance/AcceptanceOmega.java index 2d7fea54..ea1cc399 100644 --- a/prism/src/acceptance/AcceptanceOmega.java +++ b/prism/src/acceptance/AcceptanceOmega.java @@ -60,11 +60,18 @@ public interface AcceptanceOmega extends Cloneable public AcceptanceType getType(); /** Returns the type of this acceptance condition as a String, - * i.e., "R" for Rabin + * i.e., "R" for Rabin. + *
+ * Deprecated, use {@code getType().getNameAbbreviated()} */ + @Deprecated public String getTypeAbbreviated(); - /** Returns a full name for this acceptance condition */ + /** Returns a full name for this acceptance condition + *
+ * Deprecated, use {@code getType()} in String context or {@code getType().getName()} + */ + @Deprecated public String getTypeName(); /** Print the appropriate Acceptance (and potentially acc-name) header */ diff --git a/prism/src/acceptance/AcceptanceOmegaDD.java b/prism/src/acceptance/AcceptanceOmegaDD.java index f4d6cb8f..ba67a888 100644 --- a/prism/src/acceptance/AcceptanceOmegaDD.java +++ b/prism/src/acceptance/AcceptanceOmegaDD.java @@ -51,6 +51,7 @@ public interface AcceptanceOmegaDD /** Returns the type of this acceptance condition as a String, * i.e., "R" for Rabin */ + @Deprecated public String getTypeAbbreviated(); /** @@ -61,5 +62,6 @@ public interface AcceptanceOmegaDD void clear(); /** Returns a full name for this acceptance condition */ + @Deprecated public String getTypeName(); } diff --git a/prism/src/acceptance/AcceptanceRabin.java b/prism/src/acceptance/AcceptanceRabin.java index a76a35d3..20e9ef09 100644 --- a/prism/src/acceptance/AcceptanceRabin.java +++ b/prism/src/acceptance/AcceptanceRabin.java @@ -210,7 +210,7 @@ public class AcceptanceRabin if (AcceptanceType.contains(allowedAcceptance, AcceptanceType.GENERIC)) { return complementToGeneric(); } - throw new PrismNotSupportedException("Can not complement " + getTypeName() + " acceptance to a supported acceptance type"); + throw new PrismNotSupportedException("Can not complement " + getType() + " acceptance to a supported acceptance type"); } /** @@ -317,15 +317,15 @@ public class AcceptanceRabin } @Override - public String getTypeAbbreviated() - { - return "R"; + @Deprecated + public String getTypeAbbreviated() { + return getType().getNameAbbreviated(); } @Override - public String getTypeName() - { - return "Rabin"; + @Deprecated + public String getTypeName() { + return getType().getName(); } @Override diff --git a/prism/src/acceptance/AcceptanceRabinDD.java b/prism/src/acceptance/AcceptanceRabinDD.java index d707a02c..5982b0b6 100644 --- a/prism/src/acceptance/AcceptanceRabinDD.java +++ b/prism/src/acceptance/AcceptanceRabinDD.java @@ -29,7 +29,6 @@ package acceptance; import java.util.ArrayList; import common.IterableBitSet; - import jdd.JDD; import jdd.JDDNode; import jdd.JDDVars; @@ -241,14 +240,14 @@ public class AcceptanceRabinDD } @Override - public String getTypeAbbreviated() - { - return "R"; + @Deprecated + public String getTypeAbbreviated() { + return getType().getNameAbbreviated(); } @Override - public String getTypeName() - { - return "Rabin"; + @Deprecated + public String getTypeName() { + return getType().getName(); } } diff --git a/prism/src/acceptance/AcceptanceReach.java b/prism/src/acceptance/AcceptanceReach.java index b5546824..5b7c235b 100644 --- a/prism/src/acceptance/AcceptanceReach.java +++ b/prism/src/acceptance/AcceptanceReach.java @@ -131,7 +131,7 @@ public class AcceptanceReach implements AcceptanceOmega } else if (AcceptanceType.contains(allowedAcceptance, AcceptanceType.GENERIC)) { return complementToGeneric(); } - throw new PrismNotSupportedException("Can not complement " + getTypeName() + " acceptance to a supported acceptance type"); + throw new PrismNotSupportedException("Can not complement " + getType() + " acceptance to a supported acceptance type"); } @Override @@ -188,15 +188,15 @@ public class AcceptanceReach implements AcceptanceOmega } @Override - public String getTypeAbbreviated() - { - return "F"; + @Deprecated + public String getTypeAbbreviated() { + return getType().getNameAbbreviated(); } @Override - public String getTypeName() - { - return "Finite"; + @Deprecated + public String getTypeName() { + return getType().getName(); } @Override diff --git a/prism/src/acceptance/AcceptanceReachDD.java b/prism/src/acceptance/AcceptanceReachDD.java index 9463fb22..cfe65d54 100644 --- a/prism/src/acceptance/AcceptanceReachDD.java +++ b/prism/src/acceptance/AcceptanceReachDD.java @@ -105,15 +105,15 @@ public class AcceptanceReachDD implements AcceptanceOmegaDD } @Override - public String getTypeAbbreviated() - { - return "F"; + @Deprecated + public String getTypeAbbreviated() { + return getType().getNameAbbreviated(); } @Override - public String getTypeName() - { - return "Finite"; + @Deprecated + public String getTypeName() { + return getType().getName(); } @Override diff --git a/prism/src/acceptance/AcceptanceStreett.java b/prism/src/acceptance/AcceptanceStreett.java index 3172ade4..1d761f88 100644 --- a/prism/src/acceptance/AcceptanceStreett.java +++ b/prism/src/acceptance/AcceptanceStreett.java @@ -213,7 +213,7 @@ public class AcceptanceStreett if (AcceptanceType.contains(allowedAcceptance, AcceptanceType.GENERIC)) { return complementToGeneric(); } - throw new PrismNotSupportedException("Can not complement " + getTypeName() + " acceptance to a supported acceptance type"); + throw new PrismNotSupportedException("Can not complement " + getType() + " acceptance to a supported acceptance type"); } @@ -319,15 +319,15 @@ public class AcceptanceStreett } @Override - public String getTypeAbbreviated() - { - return "S"; + @Deprecated + public String getTypeAbbreviated() { + return getType().getNameAbbreviated(); } @Override - public String getTypeName() - { - return "Streett"; + @Deprecated + public String getTypeName() { + return getType().getName(); } @Override diff --git a/prism/src/acceptance/AcceptanceStreettDD.java b/prism/src/acceptance/AcceptanceStreettDD.java index 09ef942f..b5b2b90b 100644 --- a/prism/src/acceptance/AcceptanceStreettDD.java +++ b/prism/src/acceptance/AcceptanceStreettDD.java @@ -239,14 +239,14 @@ public class AcceptanceStreettDD } @Override - public String getTypeAbbreviated() - { - return "S"; + @Deprecated + public String getTypeAbbreviated() { + return getType().getNameAbbreviated(); } @Override - public String getTypeName() - { - return "Streett"; + @Deprecated + public String getTypeName() { + return getType().getName(); } } diff --git a/prism/src/acceptance/AcceptanceType.java b/prism/src/acceptance/AcceptanceType.java index 03bb2bde..e40edce9 100644 --- a/prism/src/acceptance/AcceptanceType.java +++ b/prism/src/acceptance/AcceptanceType.java @@ -31,12 +31,48 @@ package acceptance; * An omega-regular acceptance type. */ public enum AcceptanceType { - BUCHI, - RABIN, - STREETT, - REACH, - GENERALIZED_RABIN, - GENERIC; + /** Büchi acceptance */ + BUCHI("Buchi", "B"), + /** Rabin acceptance */ + RABIN("Rabin", "R"), + /** Streett acceptance */ + STREETT("Streett", "S"), + /** Finite acceptance (goal states) */ + REACH("Finite", "F"), + /** Generalized Rabin acceptance */ + GENERALIZED_RABIN("generalized-Rabin", "GR"), + /** Generic acceptance, i.e., a boolean formula over Inf and Fin as in HOA format */ + GENERIC("generic", ""); // abbreviation for generic is empty, results in DA + + /** The long form name */ + private final String typeName; + /** The abbreviated name */ + private final String typeNameAbbreviated; + + private AcceptanceType(String typeName, String typeNameAbbreviated) + { + this.typeName = typeName; + this.typeNameAbbreviated = typeNameAbbreviated; + } + + /** Returns the long form name for this acceptance type */ + public String getName() + { + return typeName; + } + + /** Returns the abbreviated form of the name for this acceptance type */ + public String getNameAbbreviated() + { + return typeNameAbbreviated; + } + + @Override + public String toString() + { + // the long form name + return getName(); + } /** * Check whether an array of AcceptanceTypes contains a specific element.