From dd87bdf86855bb8f790b7bc426ad9ccf451eccba Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Thu, 14 May 2015 17:25:36 +0200
Subject: [PATCH] =?UTF-8?q?wdba:=20adjust=20to=20work=20on=20any=20T=CF=89?=
 =?UTF-8?q?A?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

* src/twaalgos/minimize.cc, src/twaalgos/safety.cc,
src/twaalgos/safety.hh: Adjust.
* src/tests/wdba2.test: More tests.
---
 src/tests/wdba2.test     | 50 ++++++++++++++++++++++++++++++++++++++--
 src/twaalgos/minimize.cc |  5 +---
 src/twaalgos/safety.cc   | 11 ++-------
 src/twaalgos/safety.hh   |  6 ++---
 4 files changed, 54 insertions(+), 18 deletions(-)

diff --git a/src/tests/wdba2.test b/src/tests/wdba2.test
index 01e3dca41..fd35fb02f 100755
--- a/src/tests/wdba2.test
+++ b/src/tests/wdba2.test
@@ -1,7 +1,7 @@
 #!/bin/sh
 # -*- coding: utf-8 -*-
-# Copyright (C) 2012, 2014 Laboratoire de Recherche et Développement
-# de l'Epita (LRDE).
+# Copyright (C) 2012, 2014, 2015 Laboratoire de Recherche et
+# Développement de l'Epita (LRDE).
 #
 # This file is part of Spot, a model checking library.
 #
@@ -37,3 +37,49 @@ run 0 ../ltl2tgba -Rm -kt 'Fa | XGd' > out2
 cmp out expected
 cmp out2 expected
 
+cat >input <<EOF
+HOA: v1
+name: "XXFp1"
+States: 5
+Start: 4
+AP: 1 "p1"
+acc-name: Buchi
+Acceptance: 1 Inf(0)
+properties: implicit-labels state-acc complete deterministic
+--BODY--
+State: 0 {0}
+0 0
+State: 1 {0}
+3 0
+State: 2
+1 1
+State: 3
+3 0
+State: 4
+2 2
+--END--
+EOF
+
+cat >expected <<EOF
+HOA: v1
+States: 4
+Start: 2
+AP: 1 "p1"
+acc-name: Buchi
+Acceptance: 1 Inf(0)
+properties: implicit-labels state-acc complete deterministic
+properties: inherently-weak
+--BODY--
+State: 0 {0}
+0 0
+State: 1
+3 3
+State: 2
+1 1
+State: 3
+3 0
+--END--
+EOF
+
+../../bin/autfilt --small --high -C -Hi input > output
+diff output expected
diff --git a/src/twaalgos/minimize.cc b/src/twaalgos/minimize.cc
index 8c868010a..a53ae4a17 100644
--- a/src/twaalgos/minimize.cc
+++ b/src/twaalgos/minimize.cc
@@ -493,10 +493,6 @@ namespace spot
 
   twa_graph_ptr minimize_wdba(const const_twa_graph_ptr& a)
   {
-    if (a->acc().uses_fin_acceptance())
-      throw std::runtime_error
-	("minimize_wdba cannot work with Fin acceptance");
-
     hash_set* final = new hash_set;
     hash_set* non_final = new hash_set;
 
@@ -518,6 +514,7 @@ namespace spot
       // (i.e., it is not the start of any accepting word).
 
       scc_info sm(det_a);
+      sm.determine_unknown_acceptance();
       unsigned scc_count = sm.scc_count();
       // SCC that have been marked as useless.
       std::vector<bool> useless(scc_count);
diff --git a/src/twaalgos/safety.cc b/src/twaalgos/safety.cc
index 5bac45045..07a5d5e38 100644
--- a/src/twaalgos/safety.cc
+++ b/src/twaalgos/safety.cc
@@ -25,16 +25,13 @@ namespace spot
 {
   bool
   is_guarantee_automaton(const const_twa_graph_ptr& aut,
-			 const scc_info* si)
+			 scc_info* si)
   {
-    if (aut->acc().uses_fin_acceptance())
-      throw std::runtime_error
-	("is_guarantee_automaton() does not support Fin acceptance");
-
     // Create an scc_info if the user did not give one to us.
     bool need_si = !si;
     if (need_si)
       si = new scc_info(aut);
+    si->determine_unknown_acceptance();
 
     bool result = true;
 
@@ -42,10 +39,6 @@ namespace spot
       {
 	if (scc.is_rejecting())
 	  continue;
-	// Non-rejecting SCCs should necessarily be accepting, because
-	// with only one self loop, there should be no ambiguity.
-	if (!scc.is_accepting())
-	  return false;
 	// Accepting SCCs should have only one state.
 	auto& st = scc.states();
 	if (st.size() != 1)
diff --git a/src/twaalgos/safety.hh b/src/twaalgos/safety.hh
index 328006fe5..a28cffe9e 100644
--- a/src/twaalgos/safety.hh
+++ b/src/twaalgos/safety.hh
@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2010, 2011, 2013, 2014 Laboratoire de Recherche et
-// Développement de l'Epita (LRDE)
+// Copyright (C) 2010, 2011, 2013, 2014, 2015 Laboratoire de Recherche
+// et Développement de l'Epita (LRDE)
 //
 // This file is part of Spot, a model checking library.
 //
@@ -46,7 +46,7 @@ namespace spot
   /// will be built otherwise).
   SPOT_API bool
   is_guarantee_automaton(const const_twa_graph_ptr& aut,
-			 const scc_info* sm = 0);
+			 scc_info* sm = 0);
 
   /// \brief Whether a minimized WDBA represents a safety property.
   ///