From c5461335c9976264e91a067dc1c4fcca16611744 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 15 Jan 2013 19:14:22 +0100 Subject: [PATCH] ltl2tgba on-line: display edge and transition count * wrap/python/ajax/spot.in: Adjust display. * NEWS: Mention it. --- NEWS | 2 ++ wrap/python/ajax/spot.in | 14 ++++++++------ 2 files changed, 10 insertions(+), 6 deletions(-) diff --git a/NEWS b/NEWS index 50bbb72ec..e4ca683c7 100644 --- a/NEWS +++ b/NEWS @@ -17,6 +17,8 @@ New in spot 1.0a (not released): GF(a|Fb) = GF(a|b) FG(a&Xb) = FG(a&b) FG(a&Gb) = FG(a&b) + - The on-line version of ltl2tgba now displays edge and + transition counts, just as the ltlcross tool. * Pruning: - lbtt has been removed from the distribution. A copy of the last version we distributed is still available at diff --git a/wrap/python/ajax/spot.in b/wrap/python/ajax/spot.in index e6414b30b..4cba401b9 100755 --- a/wrap/python/ajax/spot.in +++ b/wrap/python/ajax/spot.in @@ -1,7 +1,7 @@ #!@PYTHON@ # -*- mode: python; coding: utf-8 -*- -# Copyright (C) 2011, 2012 Laboratoire de Recherche et Développement -# de l'Epita (LRDE). +# Copyright (C) 2011, 2012, 2013 Laboratoire de Recherche et +# Développement de l'Epita (LRDE). # # This file is part of Spot, a model checking library. # @@ -299,7 +299,7 @@ def render_formula(f): render_dot_maybe(dotsrc.str(), False) def print_stats(automaton, detinfo = False): - stats = spot.stats_reachable(automaton) + stats = spot.sub_stats_reachable(automaton) unbufprint("

%d state" % stats.states) if stats.states > 1: unbufprint("s") @@ -309,9 +309,11 @@ def print_stats(automaton, detinfo = False): unbufprint(" (deterministic)") else: unbufprint(" (%d nondeterministic)" % nondet) - unbufprint(", %d transition" % stats.transitions) - if stats.transitions > 1: - unbufprint("s") + unbufprint(", %d edge%s (%d transition%s)" + % (stats.transitions, + 's' if stats.transitions > 1 else '', + stats.sub_transitions, + 's' if stats.sub_transitions > 1 else '')) if hasattr(automaton, 'number_of_acceptance_conditions'): count = automaton.number_of_acceptance_conditions() if count > 0: