From dbeba66e9a588a8a67f24a0bfd0caf75c0bb906c 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 1cee5bd7..d76fe5e0 100644
--- a/prism/src/explicit/MDPModelChecker.java
+++ b/prism/src/explicit/MDPModelChecker.java
@@ -99,10 +99,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);