From 32cee09a72c50e9f96d82072487a1db31545082d Mon Sep 17 00:00:00 2001
From: Joachim Klein <klein@tcs.inf.tu-dresden.de>
Date: Wed, 23 Mar 2016 13:57:46 +0000
Subject: [PATCH] HOAF2DA: Handle Buchi acceptance in HOA automata

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11271 bbc10eb1-c90d-0410-af57-cb519fbb1720
---
 prism/src/automata/HOAF2DA.java | 20 ++++++++++++++++++++
 1 file changed, 20 insertions(+)

diff --git a/prism/src/automata/HOAF2DA.java b/prism/src/automata/HOAF2DA.java
index 5101e80a..bdb11d35 100644
--- a/prism/src/automata/HOAF2DA.java
+++ b/prism/src/automata/HOAF2DA.java
@@ -50,6 +50,7 @@ import jltl2ba.APElement;
 import jltl2ba.APSet;
 import jltl2dstar.APMonom;
 import jltl2dstar.APMonom2APElements;
+import acceptance.AcceptanceBuchi;
 import acceptance.AcceptanceGenRabin;
 import acceptance.AcceptanceGenRabin.GenRabinPair;
 import acceptance.AcceptanceGeneric;
@@ -283,6 +284,8 @@ public class HOAF2DA implements HOAConsumer {
 				return prepareAcceptanceGenRabin();
 			} else if (accName.equals("Streett")) {
 				return prepareAcceptanceStreett();
+			} else if (accName.equals("Buchi")) {
+				return prepareAcceptanceBuchi();
 			}
 		}
 
@@ -341,6 +344,23 @@ public class HOAF2DA implements HOAConsumer {
 		throw new UnsupportedOperationException("Unknown operator in acceptance condition: "+expr);
 	}
 
+	/**
+	 * Prepare a Buchi acceptance condition from the acc-name header.
+	 */
+	private AcceptanceBuchi prepareAcceptanceBuchi() throws HOAConsumerException
+	{
+		if (extraInfo.size() != 0) {
+			throw new HOAConsumerException("Invalid acc-name: Buchi header");
+		}
+
+		acceptanceSets = new ArrayList<BitSet>(1);
+		BitSet acceptingStates = new BitSet();
+		AcceptanceBuchi acceptanceBuchi = new AcceptanceBuchi(acceptingStates);
+		acceptanceSets.add(acceptingStates);  // Inf(0)
+
+		return acceptanceBuchi;
+	}
+
 	/**
 	 * Prepare a Rabin acceptance condition from the acc-name header.
 	 */