Commit 10c4a92d authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz

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.
parent c494a347
......@@ -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):
......
......@@ -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()
{
......
......@@ -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
......
......@@ -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'
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment