From d4a385e341d20473e3f1f5dfa400e1c5fbfc3aaa Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 6 Jul 2016 10:55:54 +0200 Subject: [PATCH] ajax: fix GTA construction * python/ajax/spotcgi.in: Here. * NEWS: Mention it. --- NEWS | 2 ++ python/ajax/spotcgi.in | 10 ++++------ 2 files changed, 6 insertions(+), 6 deletions(-) diff --git a/NEWS b/NEWS index 198f803c2..b2b4e4211 100644 --- a/NEWS +++ b/NEWS @@ -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 caused some posterior simulation-based reductions to be less 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) diff --git a/python/ajax/spotcgi.in b/python/ajax/spotcgi.in index a00310088..308c5d840 100755 --- a/python/ajax/spotcgi.in +++ b/python/ajax/spotcgi.in @@ -695,10 +695,8 @@ elif buchi_type == 'i': degen = True neverclaim = True -if output_type == 't': - ta_type = form.getfirst('tf', 't') - if ta_type == 't': - degen = True +if output_type == 't' and ta_type == 't': + degen = True if prune_scc: # Do not suppress all useless acceptance conditions if @@ -769,8 +767,8 @@ if output_type == 't': if bisimulation: tautomaton = spot.minimize_tgta(tautomaton) else: - tautomaton = spot.tgba_to_ta(degen, propset, - True, True, singlepass, livelock) + tautomaton = spot.tgba_to_ta(degen, propset, ta_type == 't', + True, singlepass, livelock) if bisimulation: tautomaton = spot.minimize_ta(tautomaton) dont_run_dot = print_stats(tautomaton, ta = True)