alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

* wrap/python/spot.i: Process tgbaalgos/neverclaim.hh.

Browse source 
* wrap/python/cgi/ltl2tgba.in: Display the never claim on demand.
This commit is contained in:
Alexandre Duret-Lutz 2004-04-21 19:02:31 +00:00
parent 8d8af2e53a
commit 0c3d4fef9f
3 changed files with 21 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

5
ChangeLog
View file

@ -1,3 +1,8 @@
2004-04-21 Alexandre Duret-Lutz <adl@gnu.org>
* wrap/python/spot.i: Process tgbaalgos/neverclaim.hh.
* wrap/python/cgi/ltl2tgba.in: Display the never claim on demand.
2004-04-21 Denis Poitrenaud <dp@src.lip6.fr> 2004-04-21 Denis Poitrenaud <dp@src.lip6.fr>
* src/ltlvisit/tostring.hh (to_spin_string): New function. * src/ltlvisit/tostring.hh (to_spin_string): New function.

18
wrap/python/cgi/ltl2tgba.in
View file

@ -199,6 +199,7 @@ options = [(
('show_formula_png', 'draw the formula', 0), ('show_formula_png', 'draw the formula', 0),
('show_automaton_png', 'draw Büchi automaton', 1), ('show_automaton_png', 'draw Büchi automaton', 1),
('show_degen_png', 'draw degeneralized Büchi automaton', 0), ('show_degen_png', 'draw degeneralized Büchi automaton', 0),
('show_never_claim', 'output Spin never claim', 0),
('show_lbtt', 'convert automaton for LBTT', 0), ('show_lbtt', 'convert automaton for LBTT', 0),
]), ( ]), (
'Debugging options', 0, '', [ 'Debugging options', 0, '', [
@ -411,14 +412,23 @@ dont_run_dot = print_stats(automaton)
if show_automaton_png: if show_automaton_png:
render_automaton(imgprefix + '-a', automaton, dont_run_dot) render_automaton(imgprefix + '-a', automaton, dont_run_dot)
if show_degen_png: if show_degen_png or show_never_claim:
print '<H3>Degeneralized automaton</H3>'
degen = spot.tgba_tba_proxy(automaton) degen = spot.tgba_tba_proxy(automaton)
dont_run_dot = print_stats(degen)
render_automaton(imgprefix + '-d', degen, dont_run_dot)
else: else:
degen = 0 degen = 0
if show_degen_png:
print '<H3>Degeneralized automaton</H3>'
dont_run_dot = print_stats(degen)
render_automaton(imgprefix + '-d', degen, dont_run_dot)
if show_never_claim:
print '<H3>Never claim (for degeneralized automaton)</H3>'
print '<PRE>'
spot.never_claim_reachable(spot.get_cout(), degen)
print '</PRE>'
sys.stdout.flush()
if show_dictionnay: if show_dictionnay:
print '<H3>BDD dictionary</H3>' print '<H3>BDD dictionary</H3>'
print '<pre>' print '<pre>'

2
wrap/python/spot.i
View file

@ -78,6 +78,7 @@
#include "tgbaalgos/dupexp.hh" #include "tgbaalgos/dupexp.hh"
#include "tgbaalgos/lbtt.hh" #include "tgbaalgos/lbtt.hh"
#include "tgbaalgos/magic.hh" #include "tgbaalgos/magic.hh"
#include "tgbaalgos/neverclaim.hh"
#include "tgbaalgos/save.hh" #include "tgbaalgos/save.hh"
#include "tgbaalgos/stats.hh" #include "tgbaalgos/stats.hh"
@ -141,6 +142,7 @@ using namespace spot;
%include "tgbaalgos/dupexp.hh" %include "tgbaalgos/dupexp.hh"
%include "tgbaalgos/lbtt.hh" %include "tgbaalgos/lbtt.hh"
%include "tgbaalgos/magic.hh" %include "tgbaalgos/magic.hh"
%include "tgbaalgos/neverclaim.hh"
%include "tgbaalgos/save.hh" %include "tgbaalgos/save.hh"
%include "tgbaalgos/stats.hh" %include "tgbaalgos/stats.hh"
#undef ltl #undef ltl