From ae4b8c929e070ceb42451586d7a868a4b280a72d Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Wed, 23 Mar 2016 14:27:41 +0000 Subject: [PATCH] =?UTF-8?q?MDP=20model=20checking:=20allow=20B=C3=BCchi=20?= =?UTF-8?q?acceptance?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Büchi automata can currently be input via the external ltl2da translators. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11273 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/explicit/MDPModelChecker.java | 1 + prism/src/prism/NondetModelChecker.java | 1 + 2 files changed, 2 insertions(+) diff --git a/prism/src/explicit/MDPModelChecker.java b/prism/src/explicit/MDPModelChecker.java index 7c5b50be..194f27dd 100644 --- a/prism/src/explicit/MDPModelChecker.java +++ b/prism/src/explicit/MDPModelChecker.java @@ -86,6 +86,7 @@ public class MDPModelChecker extends ProbModelChecker // Build product of MDP and automaton AcceptanceType[] allowedAcceptance = { + AcceptanceType.BUCHI, AcceptanceType.RABIN, AcceptanceType.GENERALIZED_RABIN, AcceptanceType.REACH diff --git a/prism/src/prism/NondetModelChecker.java b/prism/src/prism/NondetModelChecker.java index 71605807..6d9f6026 100644 --- a/prism/src/prism/NondetModelChecker.java +++ b/prism/src/prism/NondetModelChecker.java @@ -1169,6 +1169,7 @@ public class NondetModelChecker extends NonProbModelChecker // Convert LTL formula to deterministic automaton (DA) AcceptanceType[] allowedAcceptance = { + AcceptanceType.BUCHI, AcceptanceType.RABIN, AcceptanceType.GENERALIZED_RABIN, AcceptanceType.REACH