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

Fix call to scc_filter in the CGI script.

Browse source 
* wrap/python/ajax/spot.in: Do full scc_filter for TGBA (-R3f),
and keep some extra acceptance conditions (-R3) when
degeneralizing.  The converse was done.
This commit is contained in:
Alexandre Duret-Lutz 2011-02-05 14:26:51 +01:00
parent 08ee714760
commit 97df5b4285
2 changed files with 9 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

8
ChangeLog
View file

@ -1,3 +1,11 @@
2011-02-05 Alexandre Duret-Lutz <adl@lrde.epita.fr>
Fix call to scc_filter in the CGI script.
* wrap/python/ajax/spot.in: Do full scc_filter for TGBA (-R3f),
and keep some extra acceptance conditions (-R3) when
degeneralizing. The converse was done.
2011-02-04 Alexandre Duret-Lutz <adl@lrde.epita.fr> 2011-02-04 Alexandre Duret-Lutz <adl@lrde.epita.fr>
* wrap/python/cgi-bin/ltl2tgba.in: Fix python error occurring * wrap/python/cgi-bin/ltl2tgba.in: Fix python error occurring

2
wrap/python/ajax/spot.in
View file

@ -309,7 +309,7 @@ if prune_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
# accepting states usually helps. # accepting states usually helps.
automaton = spot.scc_filter(automaton, degen) automaton = spot.scc_filter(automaton, not degen)
if wdba_minimize: if wdba_minimize:
minimized = spot.minimize_obligation_new(automaton, f) minimized = spot.minimize_obligation_new(automaton, f)