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

ltl2tgba on-line: display edge and transition count

Browse source 
* wrap/python/ajax/spot.in: Adjust display.
* NEWS: Mention it.
This commit is contained in:
Alexandre Duret-Lutz 2013-01-15 19:14:22 +01:00
parent b99cfa88bb
commit c5461335c9
2 changed files with 10 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

2
NEWS
View file

@ -17,6 +17,8 @@ New in spot 1.0a (not released):
GF(a|Fb) = GF(a|b) GF(a|Fb) = GF(a|b)
FG(a&Xb) = FG(a&b) FG(a&Xb) = FG(a&b)
FG(a&Gb) = 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: * Pruning:
- lbtt has been removed from the distribution. A copy of the last - lbtt has been removed from the distribution. A copy of the last
version we distributed is still available at version we distributed is still available at

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

@ -1,7 +1,7 @@
#!@PYTHON@ #!@PYTHON@
# -*- mode: python; coding: utf-8 -*- # -*- mode: python; coding: utf-8 -*-
# Copyright (C) 2011, 2012 Laboratoire de Recherche et Développement # Copyright (C) 2011, 2012, 2013 Laboratoire de Recherche et
# de l'Epita (LRDE). # Développement de l'Epita (LRDE).
# #
# This file is part of Spot, a model checking library. # This file is part of Spot, a model checking library.
# #
@ -299,7 +299,7 @@ def render_formula(f):
render_dot_maybe(dotsrc.str(), False) render_dot_maybe(dotsrc.str(), False)
def print_stats(automaton, detinfo = False): def print_stats(automaton, detinfo = False):
stats = spot.stats_reachable(automaton) stats = spot.sub_stats_reachable(automaton)
unbufprint("<p>%d state" % stats.states) unbufprint("<p>%d state" % stats.states)
if stats.states > 1: if stats.states > 1:
unbufprint("s") unbufprint("s")
@ -309,9 +309,11 @@ def print_stats(automaton, detinfo = False):
unbufprint(" (deterministic)") unbufprint(" (deterministic)")
else: else:
unbufprint(" (%d nondeterministic)" % nondet) unbufprint(" (%d nondeterministic)" % nondet)
unbufprint(", %d transition" % stats.transitions) unbufprint(", %d edge%s (%d transition%s)"
if stats.transitions > 1: % (stats.transitions,
unbufprint("s") 's' if stats.transitions > 1 else '',
stats.sub_transitions,
's' if stats.sub_transitions > 1 else ''))
if hasattr(automaton, 'number_of_acceptance_conditions'): if hasattr(automaton, 'number_of_acceptance_conditions'):
count = automaton.number_of_acceptance_conditions() count = automaton.number_of_acceptance_conditions()
if count > 0: if count > 0: