1# -*- mode: python; coding: utf-8 -*- 2# Copyright (C) 2009, 2010, 2012, 2014-2016, 2021 Laboratoire de Recherche 3# et Développement de l'Epita (LRDE). 4# Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), 5# département Systèmes Répartis Coopératifs (SRC), Université Pierre 6# et Marie Curie. 7# 8# This file is part of Spot, a model checking library. 9# 10# Spot is free software; you can redistribute it and/or modify it 11# under the terms of the GNU General Public License as published by 12# the Free Software Foundation; either version 3 of the License, or 13# (at your option) any later version. 14# 15# Spot is distributed in the hope that it will be useful, but WITHOUT 16# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY 17# or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public 18# License for more details. 19# 20# You should have received a copy of the GNU General Public License 21# along with this program. If not, see <http://www.gnu.org/licenses/>. 22 23# This is a python implementation of a small ltl2tgba translator that calls the 24# translation and simplifications functions itself. It's better to use the 25# translate() function today. 26 27import sys 28import getopt 29import spot 30 31def usage(prog): 32 sys.stderr.write("""Usage: %s [OPTIONS...] formula 33 34Options: 35 -d turn on traces during parsing 36 -D degeneralize the automaton 37 -f use Couvreur's FM algorithm for translation 38 -t display reachable states in LBTT's format 39 -T use ltl2taa for translation 40 -v display the BDD variables used by the automaton 41 -W minimize obligation properties 42""" % prog) 43 sys.exit(2) 44 45 46prog = sys.argv[0] 47try: 48 opts, args = getopt.getopt(sys.argv[1:], 'dDftTvW') 49except getopt.GetoptError: 50 usage(prog) 51 52exit_code = 0 53debug_opt = False 54degeneralize_opt = None 55output = 0 56fm_opt = 0 57taa_opt = 0 58wdba = 0 59 60for o, a in opts: 61 if o == '-d': 62 debug_opt = True 63 elif o == '-D': 64 degeneralize_opt = 1 65 elif o == '-f': 66 fm_opt = 1 67 elif o == '-t': 68 output = 6 69 elif o == '-T': 70 taa_opt = 1 71 elif o == '-v': 72 output = 5 73 elif o == '-W': 74 wdba = 1 75 else: 76 usage(prog) 77 78if len(args) != 1: 79 usage(prog) 80 81 82cout = spot.get_cout() 83cerr = spot.get_cerr() 84 85e = spot.default_environment.instance() 86 87pf = spot.parse_infix_psl(args[0], e, debug_opt) 88if pf.format_errors(cerr): 89 exit_code = 1 90f = pf.f 91 92dict = spot.make_bdd_dict() 93 94if f: 95 if fm_opt: 96 a = spot.ltl_to_tgba_fm(f, dict) 97 concrete = 0 98 elif taa_opt: 99 a = concrete = spot.ltl_to_taa(f, dict) 100 else: 101 assert "unspecified translator" 102 103 if wdba: 104 a = spot.ensure_digraph(a) 105 a = spot.minimize_obligation(a, f) 106 107 del f 108 109 degeneralized = None 110 if degeneralize_opt: 111 a = degeneralized = spot.degeneralize(a) 112 113 if output == 0: 114 spot.print_dot(cout, a) 115 elif output == 5: 116 a.get_dict().dump(cout) 117 elif output == 6: 118 spot.print_lbtt(cout, a) 119 else: 120 assert "unknown output option" 121 122 if degeneralize_opt: 123 del degeneralized 124 # Must delete absolutely all references to an automaton 125 # so that the C++ destructor gets called. 126 del a, concrete 127 128else: 129 exit_code = 1 130 131del pf 132del dict 133 134 135# In CPython, reference counting will cause the above del() 136# to actually destruct the above formulas. However that is 137# not necessary in other implementations. 138from platform import python_implementation 139if python_implementation() == 'CPython': 140 assert spot.fnode_instances_check() 141