Acceptance: add getSignatureForStateHOA()

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10531 bbc10eb1-c90d-0410-af57-cb519fbb1720

prism/src/acceptance/AcceptanceGenRabin.java

@@ -274,6 +274,31 @@ public class AcceptanceGenRabin
 		return result;
 	}
 
+	@Override
+	public String getSignatureForStateHOA(int stateIndex)
+	{
+		String result = "";
+
+		int set_index = 0;
+		for (GenRabinPair pair : this) {
+			if (pair.getL().get(stateIndex)) {
+				result += (result.isEmpty() ? "" : " ") + set_index;
+			}
+			set_index++;
+			for (int i=0; i < pair.getNumK(); i++) {
+				if (pair.getK(i).get(stateIndex)) {
+					result += (result.isEmpty() ? "" : " ") + set_index;
+				}
+				set_index++;
+			}
+		}
+
+		if (!result.isEmpty())
+			result = "{"+result+"}";
+
+		return result;
+	}
+
 	/** Returns a textual representation of this acceptance condition. */
 	@Override
 	public String toString()

prism/src/acceptance/AcceptanceGeneric.java

@@ -197,6 +197,22 @@ public class AcceptanceGeneric implements AcceptanceOmega {
 		return result;
 	}
 
+	@Override
+	public String getSignatureForStateHOA(int stateIndex) {
+		List<AcceptanceGeneric> leafNodes = getLeafNodes();
+
+		String result = "";
+		for (int i=0; i < leafNodes.size(); i++) {
+			if (leafNodes.get(i).getStates().get(stateIndex)) {
+				result += (result.isEmpty() ? "" : " ")+i;
+			}
+		}
+
+		if (!result.isEmpty())
+			result = "{" + result + "}";
+		return result;
+	}
+
 	@Override
 	public String getSizeStatistics() {
 		return "generic acceptance with " + countAcceptanceSets() + " acceptance sets";

prism/src/acceptance/AcceptanceOmega.java

@@ -41,9 +41,13 @@ public interface AcceptanceOmega extends Cloneable
 	 **/
 	public boolean isBSCCAccepting(BitSet bscc_states);
 
-	/** Get the acceptance signature for state i.
+	/** Get the acceptance signature for state {@code stateIndex}.
 	 **/
-	public String getSignatureForState(int i);
+	public String getSignatureForState(int stateIndex);
+
+	/** Get the acceptance signature for state {@code stateIndex} (HOA format).
+	 */
+	public String getSignatureForStateHOA(int stateIndex);
 
 	/**
 	 * Get a string describing the acceptance condition's size,

prism/src/acceptance/AcceptanceRabin.java

@@ -261,6 +261,28 @@ public class AcceptanceRabin
 		return result;
 	}
 
+	@Override
+	public String getSignatureForStateHOA(int stateIndex)
+	{
+		String result = "";
+
+		for (int pairIndex=0; pairIndex<size(); pairIndex++) {
+			RabinPair pair = get(pairIndex);
+			if (pair.getL().get(stateIndex)) {
+				result += (result.isEmpty() ? "" : " ") + pairIndex*2;
+			}
+			if (pair.getK().get(stateIndex)) {
+				result += (result.isEmpty() ? "" : " ") + (pairIndex*2+1);
+			}
+		}
+
+		if (!result.isEmpty())
+			result = "{"+result+"}";
+
+		return result;
+	}
+
+	
 	/** Returns a textual representation of this acceptance condition. */
 	@Override
 	public String toString()

prism/src/acceptance/AcceptanceReach.java

@@ -151,6 +151,16 @@ public class AcceptanceReach implements AcceptanceOmega
 		return goalStates.get(i) ? "!" : " ";
 	}
 	
+	@Override
+	public String getSignatureForStateHOA(int stateIndex)
+	{
+		if (goalStates.get(stateIndex)) {
+			return "{0}";
+		} else {
+			return "";
+		}
+	}
+
 	/** Returns a textual representation of this acceptance condition. */
 	@Override
 	public String toString()

prism/src/acceptance/AcceptanceStreett.java

@@ -265,6 +265,27 @@ public class AcceptanceStreett
 		return result;
 	}
 
+	@Override
+	public String getSignatureForStateHOA(int stateIndex)
+	{
+		String result = "";
+
+		for (int pairIndex=0; pairIndex<size(); pairIndex++) {
+			StreettPair pair = get(pairIndex);
+			if (pair.getR().get(stateIndex)) {
+				result += (result.isEmpty() ? "" : " ") + pairIndex*2;
+			}
+			if (pair.getG().get(stateIndex)) {
+				result += (result.isEmpty() ? "" : " ") + (pairIndex*2+1);
+			}
+		}
+
+		if (!result.isEmpty())
+			result = "{"+result+"}";
+
+		return result;
+	}
+
 	@Override
 	public String toString()
 	{