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