From 33afd9f0e2db37204c720c69d867d554c08961ae Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 7 Aug 2015 10:49:32 +0200 Subject: [PATCH] cgi: Display a message for weak TGBA. * wrap/python/ajax/spotcgi.in: If a weak BA is output as a TGBA, add a hint that this is pointless. --- wrap/python/ajax/spotcgi.in | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/wrap/python/ajax/spotcgi.in b/wrap/python/ajax/spotcgi.in index f9212907c..54e4a0f07 100755 --- a/wrap/python/ajax/spotcgi.in +++ b/wrap/python/ajax/spotcgi.in @@ -310,6 +310,11 @@ def print_stats(automaton, detinfo = False, ta = False): stats = spot.stats_reachable(automaton) detinfo = False else: + if (buchi_type == 't' and automaton.is_inherently_weak() and + automaton.acc().is_buchi()): + unbufprint("Note: this is a weak automaton, using transition-based " + "or generalized acceptance does not bring any benefit." + "
") stats = spot.sub_stats_reachable(automaton) unbufprint("

%d state" % stats.states) if stats.states > 1: