From 17977dfbb758cb834b61589ab3fe7e99218640fb Mon Sep 17 00:00:00 2001
From: Joachim Klein <klein@tcs.inf.tu-dresden.de>
Date: Wed, 19 Jul 2017 12:36:30 +0000
Subject: [PATCH] LTL2DA: prepare for optionally using LTL2WDBA construction
 for the obligation fragment of LTL

Currently, the LTL2WDBA construction is not yet optimized for performance and
does not perform the minimization step that ensures that the WDBA are indeed minimal.
So, we don't activate it.


git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12070 bbc10eb1-c90d-0410-af57-cb519fbb1720
---
 prism/src/automata/LTL2DA.java | 28 ++++++++++++++++++++++++++--
 1 file changed, 26 insertions(+), 2 deletions(-)

diff --git a/prism/src/automata/LTL2DA.java b/prism/src/automata/LTL2DA.java
index 6069f4bb..92718f3e 100644
--- a/prism/src/automata/LTL2DA.java
+++ b/prism/src/automata/LTL2DA.java
@@ -43,6 +43,7 @@ import jhoafparser.parser.generated.ParseException;
 import jhoafparser.transformations.ToStateAcceptance;
 import jltl2ba.APSet;
 import jltl2ba.SimpleLTL;
+import jltl2ba.LTLFragments;
 import jltl2dstar.LTL2Rabin;
 import parser.Values;
 import parser.ast.Expression;
@@ -52,6 +53,7 @@ import prism.PrismNotSupportedException;
 import prism.PrismSettings;
 import acceptance.AcceptanceOmega;
 import acceptance.AcceptanceRabin;
+import acceptance.AcceptanceReach;
 import acceptance.AcceptanceType;
 
 /**
@@ -123,8 +125,30 @@ public class LTL2DA extends PrismComponent
 				if (useExternal) {
 					result = convertLTLFormulaToDAWithExternalTool(ltl, constants, allowedAcceptance);
 				} else {
-					// use jltl2dstar LTL2DA
-					result = LTL2Rabin.ltl2da(ltl.convertForJltl2ba(), allowedAcceptance);
+					SimpleLTL simpleLTL = ltl.convertForJltl2ba();
+
+					// don't use LTL2WDBA translation yet
+					boolean allowLTL2WDBA = false;
+					if (allowLTL2WDBA) {
+						LTLFragments fragments = LTLFragments.analyse(simpleLTL);
+						mainLog.println(fragments);
+
+						if (fragments.isSyntacticGuarantee() && AcceptanceType.contains(allowedAcceptance, AcceptanceType.REACH)) {
+							// a co-safety property
+							mainLog.println("Generating DFA for co-safety property...");
+							LTL2WDBA ltl2wdba = new LTL2WDBA(this);
+							result = ltl2wdba.cosafeltl2dfa(simpleLTL);
+						} else if (allowLTL2WDBA && fragments.isSyntacticObligation() && AcceptanceType.contains(allowedAcceptance, AcceptanceType.BUCHI)) {
+							// an obligation property
+							mainLog.println("Generating DBA for obligation property...");
+							LTL2WDBA ltl2wdba = new LTL2WDBA(this);
+							result = ltl2wdba.obligation2wdba(simpleLTL);
+						}
+					}
+					if (result == null) {
+						// use jltl2dstar LTL2DA
+						result = LTL2Rabin.ltl2da(simpleLTL, allowedAcceptance);
+					}
 				}
 			} else {
 				throw new PrismNotSupportedException("Could not convert LTL formula to deterministic automaton, formula had time-bounds");