From e7759bfe37374e92a3a031c8f9236d3e0a1a7188 Mon Sep 17 00:00:00 2001
From: Joachim Klein <klein@tcs.inf.tu-dresden.de>
Date: Fri, 12 Oct 2018 14:25:05 +0200
Subject: [PATCH] (HOA path) explicit MDP checker: allow Streett acceptance for
 LTL model checking

---
 prism/src/explicit/MDPModelChecker.java | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/prism/src/explicit/MDPModelChecker.java b/prism/src/explicit/MDPModelChecker.java
index 8810b07a..ac95bca0 100644
--- a/prism/src/explicit/MDPModelChecker.java
+++ b/prism/src/explicit/MDPModelChecker.java
@@ -102,10 +102,11 @@ public class MDPModelChecker extends ProbModelChecker
 
 		// Build product of MDP and automaton
 		AcceptanceType[] allowedAcceptance = {
+				AcceptanceType.REACH,
 				AcceptanceType.BUCHI,
 				AcceptanceType.RABIN,
 				AcceptanceType.GENERALIZED_RABIN,
-				AcceptanceType.REACH
+				AcceptanceType.STREETT
 		};
 		product = mcLtl.constructProductMDP(this, (MDP)model, expr, statesOfInterest, allowedAcceptance);