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

Fix usage of minimize_obligation in the CGI script.

Browse source 
* wrap/python/cgi-bin/ltl2tgba.py (reduce_wdba): Use
minimize_obligation_new a pass the formula.
* wrap/python/spot.i (minimize_obligation_new): New function, to
cope with the strange specification of spot::minimize_obligation()
not always creating a new automaton.
This commit is contained in:
Alexandre Duret-Lutz 2011-01-07 23:21:04 +01:00
parent a8fb2c4b8e
commit 74f14567d1
3 changed files with 29 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

10
ChangeLog
View file

@ -1,3 +1,13 @@
2011-01-07 Alexandre Duret-Lutz <adl@lrde.epita.fr>
Fix usage of minimize_obligation in the CGI script.
* wrap/python/cgi-bin/ltl2tgba.py (reduce_wdba): Use
minimize_obligation_new a pass the formula.
* wrap/python/spot.i (minimize_obligation_new): New function, to
cope with the strange specification of spot::minimize_obligation()
not always creating a new automaton.
2011-01-06 Alexandre Duret-Lutz <adl@lrde.epita.fr> 2011-01-06 Alexandre Duret-Lutz <adl@lrde.epita.fr>
* NEWS: Convert to utf-8 and fix a few typos. * NEWS: Convert to utf-8 and fix a few typos.

5
wrap/python/cgi-bin/ltl2tgba.in
View file

@ -574,7 +574,10 @@ elif trans_taa:
if reduce_dmonitor: if reduce_dmonitor:
automaton = spot.minimize_monitor(automaton) automaton = spot.minimize_monitor(automaton)
elif reduce_wdba: elif reduce_wdba:
automaton = spot.minimize_obligation(automaton) minimized = spot.minimize_obligation_new(automaton, f)
if minimized:
automaton = minimized
minimized = 0
elif reduce_scc: elif reduce_scc:
# Do not suppress all useless acceptance conditions if # Do not suppress all useless acceptance conditions if
# degeneralization is requested: keeping those that lead to # degeneralization is requested: keeping those that lead to

16
wrap/python/spot.i
View file

@ -149,7 +149,6 @@ using namespace spot;
%feature("new") spot::ltl_to_tgba_lacim; %feature("new") spot::ltl_to_tgba_lacim;
%feature("new") spot::minimize_wdba; %feature("new") spot::minimize_wdba;
%feature("new") spot::minimize_monitor; %feature("new") spot::minimize_monitor;
%feature("new") spot::minimize_obligation;
%feature("new") spot::reduc_tgba_sim; %feature("new") spot::reduc_tgba_sim;
%feature("new") spot::scc_filter; %feature("new") spot::scc_filter;
%feature("new") spot::tgba_dupexp_bfs; %feature("new") spot::tgba_dupexp_bfs;
@ -229,8 +228,23 @@ namespace std {
}; };
} }
%feature("new") minimize_obligation_new;
%inline %{ %inline %{
// A variant of minimize_obligation() that always return a new object.
const spot::tgba*
minimize_obligation_new(const spot::tgba* a, const spot::ltl::formula* f)
{
const tgba* res = spot::minimize_obligation(a, f);
// Return 0 if the output is the same as the input, otherwise
// it is hard for swig to know if the output is "new" or not.
if (res == a)
return 0;
else
return res;
}
spot::ltl::parse_error_list spot::ltl::parse_error_list
empty_parse_error_list() empty_parse_error_list()
{ {