From d15b5f43a6d206fe863f203c11c60dc4f22c7075 Mon Sep 17 00:00:00 2001
From: Alexandre Lewkowicz <lewkow_a@epita.fr>
Date: Mon, 9 Nov 2015 17:45:21 +0100
Subject: [PATCH] safra: Fix properties and use new API

* src/tests/safra.cc, src/twaalgos/safra.cc: Here.
---
 src/tests/safra.cc    | 16 +++++++---------
 src/twaalgos/safra.cc |  4 ++--
 2 files changed, 9 insertions(+), 11 deletions(-)

diff --git a/src/tests/safra.cc b/src/tests/safra.cc
index d5fc49f6f..f38e278d9 100644
--- a/src/tests/safra.cc
+++ b/src/tests/safra.cc
@@ -20,7 +20,8 @@
 #include <iostream>
 #include <cstring>
 
-#include "ltlparse/public.hh" // ltl::parse
+#include "tl/parse.hh" // spot::parse_infix_psl
+#include "tl/formula.hh" // spot::formula
 #include "parseaut/public.hh"
 #include "twa/twagraph.hh"
 #include "twaalgos/degen.hh"
@@ -96,22 +97,19 @@ int main(int argc, char* argv[])
   spot::twa_graph_ptr res;
   if (in_ltl)
     {
-      spot::ltl::parse_error_list pel;
-      const spot::ltl::formula* f =
-      spot::ltl::parse_infix_psl(input, pel);
-      if (spot::ltl::format_parse_errors(std::cerr, input, pel))
+      spot::parse_error_list pel;
+      spot::formula f = spot::parse_infix_psl(input, pel);
+      if (spot::format_parse_errors(std::cerr, input, pel))
         return 2;
       spot::translator trans(dict);
       trans.set_pref(spot::postprocessor::Deterministic);
       auto tmp = trans.run(f);
       res = spot::tgba_determinisation(tmp, sim, pretty_print, scc_opt);
-      f->destroy();
     }
   else if (in_hoa)
     {
-      spot::parse_aut_error_list pel;
-      auto aut = spot::parse_aut(input, pel, dict);
-      if (spot::format_parse_aut_errors(std::cerr, input, pel))
+      auto aut = spot::parse_aut(input, dict);
+      if (aut->format_errors(std::cerr))
         return 2;
       res = tgba_determinisation(aut->aut, sim, pretty_print, scc_opt);
     }
diff --git a/src/twaalgos/safra.cc b/src/twaalgos/safra.cc
index 702c4052a..4e2a173cc 100644
--- a/src/twaalgos/safra.cc
+++ b/src/twaalgos/safra.cc
@@ -493,7 +493,7 @@ safra_state::compute_succs(const const_twa_graph_ptr& aut,
     res->copy_ap_of(aut);
     res->prop_copy(aut,
                    { false, // state based
-                   true, // inherently_weak
+                   false, // inherently_weak
                    false, // deterministic
                    true // stutter inv
                    });
@@ -550,7 +550,7 @@ safra_state::compute_succs(const const_twa_graph_ptr& aut,
     // Acceptance is now min(odd) since we con emit Red on paths 0 with new opti
     res->set_acceptance(sets, acc_cond::acc_code::parity(false, true, sets));
     res->prop_deterministic(true);
-    res->prop_state_based_acc(false);
+    res->prop_state_acc(false);
     if (bisimulation)
       res = simulation(res);
     if (pretty_print)