From 4bd03ef8540b7b06921648a0090b93cd462230d3 Mon Sep 17 00:00:00 2001
From: Joachim Klein <klein@tcs.inf.tu-dresden.de>
Date: Thu, 20 Aug 2015 06:27:02 +0000
Subject: [PATCH] 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 | 25 ++++++++++++++++++++
 prism/src/acceptance/AcceptanceGeneric.java  | 16 +++++++++++++
 prism/src/acceptance/AcceptanceOmega.java    |  8 +++++--
 prism/src/acceptance/AcceptanceRabin.java    | 22 +++++++++++++++++
 prism/src/acceptance/AcceptanceReach.java    | 10 ++++++++
 prism/src/acceptance/AcceptanceStreett.java  | 21 ++++++++++++++++
 6 files changed, 100 insertions(+), 2 deletions(-)

diff --git a/prism/src/acceptance/AcceptanceGenRabin.java b/prism/src/acceptance/AcceptanceGenRabin.java
index ca2a7063..b578f44c 100644
--- a/prism/src/acceptance/AcceptanceGenRabin.java
+++ b/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()
diff --git a/prism/src/acceptance/AcceptanceGeneric.java b/prism/src/acceptance/AcceptanceGeneric.java
index 676840dc..56a78e77 100644
--- a/prism/src/acceptance/AcceptanceGeneric.java
+++ b/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";
diff --git a/prism/src/acceptance/AcceptanceOmega.java b/prism/src/acceptance/AcceptanceOmega.java
index 0e36d841..2ed9700b 100644
--- a/prism/src/acceptance/AcceptanceOmega.java
+++ b/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,
diff --git a/prism/src/acceptance/AcceptanceRabin.java b/prism/src/acceptance/AcceptanceRabin.java
index 298ef3c6..f9ea6acf 100644
--- a/prism/src/acceptance/AcceptanceRabin.java
+++ b/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()
diff --git a/prism/src/acceptance/AcceptanceReach.java b/prism/src/acceptance/AcceptanceReach.java
index 99d0034e..19993c60 100644
--- a/prism/src/acceptance/AcceptanceReach.java
+++ b/prism/src/acceptance/AcceptanceReach.java
@@ -150,6 +150,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
diff --git a/prism/src/acceptance/AcceptanceStreett.java b/prism/src/acceptance/AcceptanceStreett.java
index 5577d018..9376f75c 100644
--- a/prism/src/acceptance/AcceptanceStreett.java
+++ b/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()
 	{