From 10c4a92ddb736e50b71254380f2f401c5c0dbdb0 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Thu, 27 Nov 2014 19:09:06 +0100
Subject: [PATCH] python: fix spot.py script for new acceptance interface

* wrap/python/ajax/spot.in: Adjust to the new interface.
* wrap/python/spot.i: Work around missing support for nested classes.
* wrap/python/tests/ltl2tgba.py, wrap/python/tests/ltl2tgba.test: More
test.
---
 wrap/python/ajax/spot.in        | 10 +++++-----
 wrap/python/spot.i              | 12 ++++++++++++
 wrap/python/tests/ltl2tgba.py   | 11 ++++++++++-
 wrap/python/tests/ltl2tgba.test |  3 +++
 4 files changed, 30 insertions(+), 6 deletions(-)

diff --git a/wrap/python/ajax/spot.in b/wrap/python/ajax/spot.in
index 6877b47c6..642e80b57 100755
--- a/wrap/python/ajax/spot.in
+++ b/wrap/python/ajax/spot.in
@@ -325,14 +325,14 @@ def print_stats(automaton, detinfo = False, ta = False):
                       's' if stats.transitions > 1 else '',
                       stats.sub_transitions,
                       's' if stats.sub_transitions > 1 else ''))
-    if hasattr(automaton, 'number_of_acceptance_conditions'):
-        count = automaton.number_of_acceptance_conditions()
+    if hasattr(automaton, 'acc'):
+        count = automaton.acc().num_sets()
         if count > 0:
             unbufprint(", %d acceptance condition" % count)
             if count > 1:
                 unbufprint("s")
-            acc = automaton.all_acceptance_conditions()
-            unbufprint(": " + spot.bdd_format_accset(automaton.get_dict(), acc))
+            unbufprint(": " +
+                       automaton.acc().format(automaton.acc().all_sets()))
         else:
             unbufprint(", no acceptance condition (all cycles are accepting)")
     unbufprint("</p>\n")
@@ -780,7 +780,7 @@ if output_type == 'r':
         ec = 0
     else:
         ec_a = 0
-        n_acc = degen.number_of_acceptance_conditions()
+        n_acc = degen.acc().num_sets()
         n_max = eci.max_acceptance_conditions()
         n_min = eci.min_acceptance_conditions()
         if (n_acc <= n_max):
diff --git a/wrap/python/spot.i b/wrap/python/spot.i
index 5d14a7a91..4e0b19c33 100644
--- a/wrap/python/spot.i
+++ b/wrap/python/spot.i
@@ -105,6 +105,7 @@ namespace std {
 
 #include "tgba/bddprint.hh"
 #include "tgba/fwd.hh"
+#include "tgba/acc.hh"
 #include "tgba/tgba.hh"
 #include "tgba/taatgba.hh"
 #include "tgba/tgbaproduct.hh"
@@ -226,6 +227,8 @@ using namespace spot;
 #define ltl spot::ltl
 %include "tgba/bddprint.hh"
 %include "tgba/fwd.hh"
+%feature("flatnested") spot::acc_cond::mark_t;
+%include "tgba/acc.hh"
 %include "tgba/tgba.hh"
 %include "tgba/taatgba.hh"
 %include "tgba/tgbaproduct.hh"
@@ -359,6 +362,15 @@ empty_tgba_parse_error_list()
   return l;
 }
 
+spot::tgba_digraph_ptr
+ensure_digraph(const spot::tgba_ptr& a)
+{
+  auto aa = std::dynamic_pointer_cast<spot::tgba_digraph>(a);
+  if (aa)
+    return aa;
+  return spot::make_tgba_digraph(a);
+}
+
 std::ostream&
 get_cout()
 {
diff --git a/wrap/python/tests/ltl2tgba.py b/wrap/python/tests/ltl2tgba.py
index e6825bb25..615db9cc7 100755
--- a/wrap/python/tests/ltl2tgba.py
+++ b/wrap/python/tests/ltl2tgba.py
@@ -37,13 +37,14 @@ Options:
   -t   display reachable states in LBTT's format
   -T   use ltl2taa for translation
   -v   display the BDD variables used by the automaton
+  -W   minimize obligation properties
 """ % prog)
     sys.exit(2)
 
 
 prog = sys.argv[0]
 try:
-    opts, args = getopt.getopt(sys.argv[1:], 'dDftTv')
+    opts, args = getopt.getopt(sys.argv[1:], 'dDftTvW')
 except getopt.GetoptError:
     usage(prog)
 
@@ -53,6 +54,7 @@ degeneralize_opt = None
 output = 0
 fm_opt = 0
 taa_opt = 0
+wdba = 0
 
 for o, a in opts:
     if o == '-d':
@@ -67,6 +69,8 @@ for o, a in opts:
         taa_opt = 1
     elif o == '-v':
         output = 5
+    elif o == '-W':
+        wdba = 1
     else:
         usage(prog)
 
@@ -94,6 +98,11 @@ if f:
         a = concrete = spot.ltl_to_taa(f, dict)
     else:
         assert "unspecified translator"
+
+    if wdba:
+        a = spot.ensure_digraph(a)
+        a = spot.minimize_obligation(a, f)
+
     f.destroy()
     del f
 
diff --git a/wrap/python/tests/ltl2tgba.test b/wrap/python/tests/ltl2tgba.test
index d1d233a7c..70f09a37c 100755
--- a/wrap/python/tests/ltl2tgba.test
+++ b/wrap/python/tests/ltl2tgba.test
@@ -45,3 +45,6 @@ set -e
 ./run $srcdir/ltl2tgba.py -f 'Fa & Xb & GFc & Gd'
 ./run $srcdir/ltl2tgba.py -f 'Fa & Xa & GFc & Gc'
 ./run $srcdir/ltl2tgba.py -f 'Fc & X(a | Xb) & GF(a | Xb) & Gc'
+
+./run $srcdir/ltl2tgba.py -W -f 'Ga | Gb | Gc'
+./run $srcdir/ltl2tgba.py -W -T 'Ga | Gb | Gc'