MDP model checking: allow Büchi acceptance

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
10 years ago · ae4b8c929e
2 changed files with 2 additions and 0 deletions
--- 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
--- 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