1 // -*- coding: utf-8 -*-
2 // Copyright (C) 2012-2020 Laboratoire de Recherche et Développement
3 // de l'Epita (LRDE).
4 //
5 // This file is part of Spot, a model checking library.
6 //
7 // Spot is free software; you can redistribute it and/or modify it
8 // under the terms of the GNU General Public License as published by
9 // the Free Software Foundation; either version 3 of the License, or
10 // (at your option) any later version.
11 //
12 // Spot is distributed in the hope that it will be useful, but WITHOUT
13 // ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
14 // or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
15 // License for more details.
16 //
17 // You should have received a copy of the GNU General Public License
18 // along with this program. If not, see <http://www.gnu.org/licenses/>.
19
20 #include "common_sys.hh"
21
22 #include <string>
23 #include <iostream>
24 #include <fstream>
25
26 #include <argp.h>
27 #include <unistd.h>
28 #include "error.h"
29
30 #include "common_setup.hh"
31 #include "common_r.hh"
32 #include "common_cout.hh"
33 #include "common_finput.hh"
34 #include "common_post.hh"
35
36 #include <spot/tl/parse.hh>
37 #include <spot/tl/print.hh>
38 #include <spot/tl/simplify.hh>
39 #include <spot/twaalgos/dot.hh>
40 #include <spot/twaalgos/ltl2tgba_fm.hh>
41 #include <spot/twaalgos/translate.hh>
42 #include <spot/twa/bddprint.hh>
43
44 #include <spot/taalgos/tgba2ta.hh>
45 #include <spot/taalgos/dot.hh>
46 #include <spot/taalgos/minimize.hh>
47 #include <spot/misc/optionmap.hh>
48
49 const char argp_program_doc[] ="\
50 Translate linear-time formulas (LTL/PSL) into Testing Automata.\n\n\
51 By default it outputs a transition-based generalized Testing Automaton \
52 the smallest Transition-based Generalized Büchi Automata, \
53 in GraphViz's format. The input formula is assumed to be \
54 stuttering-insensitive.";
55
56 enum {
57 OPT_GTA = 1,
58 OPT_INIT,
59 OPT_SPLV,
60 OPT_SPNO,
61 OPT_TA,
62 OPT_TGTA,
63 };
64
65 static const argp_option options[] =
66 {
67 /**************************************************/
68 { nullptr, 0, nullptr, 0, "Automaton type:", 1 },
69 { "tgta", OPT_TGTA, nullptr, 0,
70 "Transition-based Generalized Testing Automaton (default)", 0 },
71 { "ta", OPT_TA, nullptr, 0, "Testing Automaton", 0 },
72 { "gta", OPT_GTA, nullptr, 0, "Generalized Testing Automaton", 0 },
73 /**************************************************/
74 { nullptr, 0, nullptr, 0, "Options for TA and GTA creation:", 3 },
75 { "single-pass-lv", OPT_SPLV, nullptr, 0,
76 "add an artificial livelock state to obtain a single-pass (G)TA", 0 },
77 { "single-pass", OPT_SPNO, nullptr, 0,
78 "create a single-pass (G)TA without artificial livelock state", 0 },
79 { "multiple-init", OPT_INIT, nullptr, 0,
80 "do not create the fake initial state", 0 },
81 /**************************************************/
82 { nullptr, 0, nullptr, 0, "Output options:", 4 },
83 { "utf8", '8', nullptr, 0, "enable UTF-8 characters in output", 0 },
84 /**************************************************/
85 { nullptr, 0, nullptr, 0, "Miscellaneous options:", -1 },
86 { "extra-options", 'x', "OPTS", 0,
87 "fine-tuning options (see spot-x (7))", 0 },
88 { nullptr, 0, nullptr, 0, nullptr, 0 }
89 };
90
91 const struct argp_child children[] =
92 {
93 { &finput_argp, 0, nullptr, 1 },
94 { &post_argp_nooutput, 0, nullptr, 20 },
95 { &misc_argp, 0, nullptr, -1 },
96 { nullptr, 0, nullptr, 0 }
97 };
98
99 enum ta_types { TGTA, GTA, TA };
100 ta_types ta_type = TGTA;
101
102 bool utf8 = false;
103 const char* stats = "";
104 spot::option_map extra_options;
105 bool opt_with_artificial_initial_state = true;
106 bool opt_single_pass_emptiness_check = false;
107 bool opt_with_artificial_livelock = false;
108
109 static int
parse_opt(int key,char * arg,struct argp_state *)110 parse_opt(int key, char* arg, struct argp_state*)
111 {
112 // Called from C code, so should not raise any exception.
113 BEGIN_EXCEPTION_PROTECT;
114 // This switch is alphabetically-ordered.
115 switch (key)
116 {
117 case '8':
118 spot::enable_utf8();
119 break;
120 case 'x':
121 {
122 const char* opt = extra_options.parse_options(arg);
123 if (opt)
124 error(2, 0, "failed to parse --options near '%s'", opt);
125 }
126 break;
127 case OPT_TGTA:
128 ta_type = TGTA;
129 type = spot::postprocessor::GeneralizedBuchi;
130 break;
131 case OPT_GTA:
132 ta_type = GTA;
133 type = spot::postprocessor::GeneralizedBuchi;
134 break;
135 case OPT_TA:
136 ta_type = TA;
137 type = spot::postprocessor::Buchi;
138 sbacc = spot::postprocessor::SBAcc;
139 break;
140 case OPT_INIT:
141 opt_with_artificial_initial_state = false;
142 break;
143 case OPT_SPLV:
144 opt_with_artificial_livelock = true;
145 break;
146 case OPT_SPNO:
147 opt_single_pass_emptiness_check = true;
148 break;
149 case ARGP_KEY_ARG:
150 // FIXME: use stat() to distinguish filename from string?
151 if (*arg == '-' && !arg[1])
152 jobs.emplace_back(arg, true);
153 else
154 jobs.emplace_back(arg, false);
155 break;
156
157 default:
158 return ARGP_ERR_UNKNOWN;
159 }
160 END_EXCEPTION_PROTECT;
161 return 0;
162 }
163
164
165 namespace
166 {
167 class trans_processor final: public job_processor
168 {
169 public:
170 spot::translator& trans;
171
trans_processor(spot::translator & trans)172 trans_processor(spot::translator& trans)
173 : trans(trans)
174 {
175 }
176
177 int
process_formula(spot::formula f,const char * filename=nullptr,int linenum=0)178 process_formula(spot::formula f,
179 const char* filename = nullptr, int linenum = 0) override
180 {
181 auto aut = trans.run(&f);
182
183 // This should not happen, because the parser we use can only
184 // read PSL/LTL formula, but since our formula type can
185 // represent more than PSL formula, let's make this
186 // future-proof.
187 if (!f.is_psl_formula())
188 {
189 std::string s = spot::str_psl(f);
190 error_at_line(2, 0, filename, linenum,
191 "formula '%s' is not an LTL or PSL formula",
192 s.c_str());
193 }
194
195 bdd ap_set = atomic_prop_collect_as_bdd(f, aut);
196
197 if (ta_type != TGTA)
198 {
199 auto testing_automaton =
200 tgba_to_ta(aut, ap_set, type == spot::postprocessor::Buchi,
201 opt_with_artificial_initial_state,
202 opt_single_pass_emptiness_check,
203 opt_with_artificial_livelock);
204 if (level != spot::postprocessor::Low)
205 testing_automaton = spot::minimize_ta(testing_automaton);
206 spot::print_dot(std::cout, testing_automaton);
207 }
208 else
209 {
210 auto tgta = tgba_to_tgta(aut, ap_set);
211 if (level != spot::postprocessor::Low)
212 tgta = spot::minimize_tgta(tgta);
213 spot::print_dot(std::cout, tgta->get_ta());
214 }
215 // If we keep simplification caches around, atomic propositions
216 // will still be defined, and one translation may influence the
217 // variable order of the next one.
218 trans.clear_caches();
219 flush_cout();
220 return 0;
221 }
222 };
223 }
224
225 int
main(int argc,char ** argv)226 main(int argc, char** argv)
227 {
228 return protected_main(argv, [&] {
229 const argp ap = { options, parse_opt, "[FORMULA...]",
230 argp_program_doc, children, nullptr, nullptr };
231
232 simplification_level = 3;
233
234 if (int err = argp_parse(&ap, argc, argv, ARGP_NO_HELP, nullptr, nullptr))
235 exit(err);
236
237 check_no_formula();
238
239 spot::translator trans(&extra_options);
240 trans.set_pref(pref | comp | sbacc);
241 trans.set_type(type);
242 trans.set_level(level);
243
244 trans_processor processor(trans);
245 if (processor.run())
246 return 2;
247 // Diagnose unused -x options
248 extra_options.report_unused_options();
249 return 0;
250 });
251 }
252