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

ajax: fix GTA construction

Browse source 
* python/ajax/spotcgi.in: Here.
* NEWS: Mention it.
This commit is contained in:
Alexandre Duret-Lutz 2016-07-06 10:55:54 +02:00
parent a4c7016f52
commit d4a385e341
2 changed files with 6 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

2
NEWS
View file

@ -10,6 +10,8 @@ New in spot 2.0.2a (Not yet released)
choice of the level is free, it used the last level used. This choice of the level is free, it used the last level used. This
caused some posterior simulation-based reductions to be less caused some posterior simulation-based reductions to be less
efficient at reducing automata (on the average). efficient at reducing automata (on the average).
* The generalized testing automata displayed by the on-line
translator were incorrect (those output by ltl2tgta were OK).
New in spot 2.0.2 (2016-06-17) New in spot 2.0.2 (2016-06-17)

8
python/ajax/spotcgi.in
View file

@ -695,9 +695,7 @@ elif buchi_type == 'i':
degen = True degen = True
neverclaim = True neverclaim = True
if output_type == 't': if output_type == 't' and ta_type == 't':
ta_type = form.getfirst('tf', 't')
if ta_type == 't':
degen = True degen = True
if prune_scc: if prune_scc:
@ -769,8 +767,8 @@ if output_type == 't':
if bisimulation: if bisimulation:
tautomaton = spot.minimize_tgta(tautomaton) tautomaton = spot.minimize_tgta(tautomaton)
else: else:
tautomaton = spot.tgba_to_ta(degen, propset, tautomaton = spot.tgba_to_ta(degen, propset, ta_type == 't',
True, True, singlepass, livelock) True, singlepass, livelock)
if bisimulation: if bisimulation:
tautomaton = spot.minimize_ta(tautomaton) tautomaton = spot.minimize_ta(tautomaton)
dont_run_dot = print_stats(tautomaton, ta = True) dont_run_dot = print_stats(tautomaton, ta = True)