From c714d88e6e5db30d969b3225da40651d99ff4e6f Mon Sep 17 00:00:00 2001
From: Joachim Klein <klein@tcs.inf.tu-dresden.de>
Date: Thu, 9 Jul 2015 09:08:35 +0000
Subject: [PATCH] HOAF2DA: Limit atomic propositions to at most 30.

For more APs, the number of edges surpass what can
be stored in an int and we will get into trouble
with memory anyways.


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

diff --git a/prism/src/automata/HOAF2DA.java b/prism/src/automata/HOAF2DA.java
index 64262e39..29779c14 100644
--- a/prism/src/automata/HOAF2DA.java
+++ b/prism/src/automata/HOAF2DA.java
@@ -64,6 +64,7 @@ import acceptance.AcceptanceRabin.RabinPair;
  * <ul>
  * <li>The Start and States headers have to be present</li>
  * <li>All explicit edge labels have to be in disjunctive normal form (disjunction of conjunctive clauses)</li>
+ * <li>At most 30 atomic propositions</li>
  * </ul>
  */
 public class HOAF2DA implements HOAConsumer {
@@ -167,6 +168,10 @@ public class HOAF2DA implements HOAConsumer {
 
 	@Override
 	public void setAPs(List<String> aps) throws HOAConsumerException {
+		if (aps.size() > 30) {
+			throw new HOAConsumerException("Automaton has "+aps.size()+" atomic propositions, at most 30 are supported");
+		}
+
 		apList = aps;
 
 		for (String ap : aps) {