1 // -*- coding: utf-8 -*-
2 // Copyright (C) 2012-2016, 2018-2019 Laboratoire de Recherche
3 // et Développement 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 <iostream>
23 #include <fstream>
24 #include <argp.h>
25 #include <cstdlib>
26 #include <iterator>
27 #include "error.h"
28
29 #include "common_setup.hh"
30 #include "common_output.hh"
31 #include "common_range.hh"
32 #include "common_r.hh"
33 #include "common_conv.hh"
34 #include "common_cout.hh"
35
36 #include <sstream>
37 #include <spot/tl/defaultenv.hh>
38 #include <spot/tl/randomltl.hh>
39 #include <spot/tl/simplify.hh>
40 #include <spot/misc/random.hh>
41 #include <spot/misc/optionmap.hh>
42
43 const char argp_program_doc[] ="\
44 Generate random temporal logic formulas.\n\n\
45 The formulas are built over the atomic propositions named by PROPS...\n\
46 or, if N is a nonnegative number, using N arbitrary names.\v\
47 Examples:\n\
48 \n\
49 The following generates 10 random LTL formulas over the propositions a, b,\n\
50 and c, with the default tree-size, and all available operators.\n\
51 % randltl -n10 a b c\n\
52 \n\
53 If you do not mind about the name of the atomic propositions, just give\n\
54 a number instead:\n\
55 % randltl -n10 3\n\
56 \n\
57 You can disable or favor certain operators by changing their priority.\n\
58 The following disables xor, implies, and equiv, and multiply the probability\n\
59 of X to occur by 10.\n\
60 % randltl --ltl-priorities='xor=0, implies=0, equiv=0, X=10' -n10 a b c\n\
61 ";
62
63 enum {
64 OPT_BOOLEAN_PRIORITIES = 1,
65 OPT_DUMP_PRIORITIES,
66 OPT_DUPS,
67 OPT_LTL_PRIORITIES,
68 OPT_PSL_PRIORITIES,
69 OPT_SEED,
70 OPT_SERE_PRIORITIES,
71 OPT_TREE_SIZE,
72 OPT_WF,
73 };
74
75 static const argp_option options[] =
76 {
77 // Keep this alphabetically sorted (expect for aliases).
78 /**************************************************/
79 { nullptr, 0, nullptr, 0, "Type of formula to generate:", 1 },
80 { "boolean", 'B', nullptr, 0, "generate Boolean formulas", 0 },
81 { "ltl", 'L', nullptr, 0, "generate LTL formulas (default)", 0 },
82 { "sere", 'S', nullptr, 0, "generate SERE", 0 },
83 { "psl", 'P', nullptr, 0, "generate PSL formulas", 0 },
84 /**************************************************/
85 { nullptr, 0, nullptr, 0, "Generation:", 2 },
86 { "weak-fairness", OPT_WF, nullptr, 0,
87 "append some weak-fairness conditions", 0 },
88 { "formulas", 'n', "INT", 0, "number of formulas to output (1)\n"\
89 "use a negative value for unbounded generation", 0 },
90 { "seed", OPT_SEED, "INT", 0,
91 "seed for the random number generator (0)", 0 },
92 { "tree-size", OPT_TREE_SIZE, "RANGE", 0,
93 "tree size of the formulas generated, before mandatory "\
94 "trivial simplifications (15)", 0 },
95 { "allow-dups", OPT_DUPS, nullptr, 0,
96 "allow duplicate formulas to be output", 0 },
97 DECLARE_OPT_R,
98 RANGE_DOC,
99 LEVEL_DOC(3),
100 /**************************************************/
101 { nullptr, 0, nullptr, 0, "Adjusting probabilities:", 4 },
102 { "dump-priorities", OPT_DUMP_PRIORITIES, nullptr, 0,
103 "show current priorities, do not generate any formula", 0 },
104 { "ltl-priorities", OPT_LTL_PRIORITIES, "STRING", 0,
105 "set priorities for LTL formulas", 0 },
106 { "sere-priorities", OPT_SERE_PRIORITIES, "STRING", 0,
107 "set priorities for SERE formulas", 0 },
108 { "boolean-priorities", OPT_BOOLEAN_PRIORITIES, "STRING", 0,
109 "set priorities for Boolean formulas", 0 },
110 { nullptr, 0, nullptr, 0, "STRING should be a comma-separated list of "
111 "assignments, assigning integer priorities to the tokens "
112 "listed by --dump-priorities.", 0 },
113 /**************************************************/
114 { nullptr, 0, nullptr, 0, "Output options:", -20 },
115 { nullptr, 0, nullptr, 0, "The FORMAT string passed to --format may use "
116 "the following interpreted sequences:", -19 },
117 { "%f", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
118 "the formula (in the selected syntax)", 0 },
119 { "%L", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
120 "the (serial) number of the formula", 0 },
121 { "%%", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
122 "a single %", 0 },
123 COMMON_LTL_OUTPUT_SPECS,
124 /**************************************************/
125 { nullptr, 0, nullptr, 0, "Miscellaneous options:", -1 },
126 { nullptr, 0, nullptr, 0, nullptr, 0 }
127 };
128
129
130 const struct argp_child children[] =
131 {
132 { &output_argp, 0, nullptr, 0 },
133 { &misc_argp, 0, nullptr, 0 },
134 { nullptr, 0, nullptr, 0 }
135 };
136
137 // We want all these variables to be destroyed when we exit main, to
138 // make sure it happens before all other global variables (like the
139 // atomic propositions maps) are destroyed. Otherwise we risk
140 // accessing deleted stuff.
141 static struct opt_t
142 {
143 spot::atomic_prop_set aprops;
144 }* opt;
145
146 static spot::randltlgenerator::output_type output =
147 spot::randltlgenerator::LTL;
148 static char* opt_pL = nullptr;
149 static char* opt_pS = nullptr;
150 static char* opt_pB = nullptr;
151 static bool opt_dump_priorities = false;
152 static int opt_formulas = 1;
153 static int opt_seed = 0;
154 static range opt_tree_size = { 15, 15 };
155 static bool opt_unique = true;
156 static bool opt_wf = false;
157 static bool ap_count_given = false;
158
159 static int
parse_opt(int key,char * arg,struct argp_state * as)160 parse_opt(int key, char* arg, struct argp_state* as)
161 {
162 // Called from C code, so should not raise any exception.
163 BEGIN_EXCEPTION_PROTECT;
164 // This switch is alphabetically-ordered.
165 switch (key)
166 {
167 case 'B':
168 output = spot::randltlgenerator::Bool;
169 break;
170 case 'L':
171 output = spot::randltlgenerator::LTL;
172 break;
173 case 'n':
174 opt_formulas = to_int(arg, "-n/--formulas");
175 break;
176 case 'P':
177 output = spot::randltlgenerator::PSL;
178 break;
179 case OPT_R:
180 parse_r(arg);
181 break;
182 case 'S':
183 output = spot::randltlgenerator::SERE;
184 break;
185 case OPT_BOOLEAN_PRIORITIES:
186 opt_pB = arg;
187 break;
188 case OPT_DUPS:
189 opt_unique = false;
190 break;
191 case OPT_LTL_PRIORITIES:
192 opt_pL = arg;
193 break;
194 case OPT_DUMP_PRIORITIES:
195 opt_dump_priorities = true;
196 break;
197 // case OPT_PSL_PRIORITIES: break;
198 case OPT_SERE_PRIORITIES:
199 opt_pS = arg;
200 break;
201 case OPT_SEED:
202 opt_seed = to_int(arg, "--seed");
203 break;
204 case OPT_TREE_SIZE:
205 opt_tree_size = parse_range(arg);
206 if (opt_tree_size.min > opt_tree_size.max)
207 std::swap(opt_tree_size.min, opt_tree_size.max);
208 break;
209 case OPT_WF:
210 opt_wf = true;
211 break;
212 case ARGP_KEY_ARG:
213 // If this is the unique non-option argument, it can
214 // be a number of atomic propositions to build.
215 //
216 // argp reorganizes argv[] so that options always come before
217 // non-options. So if as->argc == as->next we know this is the
218 // last non-option argument, and if aprops.empty() we know this
219 // is the also the first one.
220 if (opt->aprops.empty() && as->argc == as->next)
221 {
222 char* endptr;
223 int res = strtol(arg, &endptr, 10);
224 if (!*endptr && res >= 0) // arg is a number
225 {
226 ap_count_given = true;
227 opt->aprops = spot::create_atomic_prop_set(res);
228 break;
229 }
230 }
231 opt->aprops.insert(spot::default_environment::instance().require(arg));
232 break;
233 default:
234 return ARGP_ERR_UNKNOWN;
235 }
236 END_EXCEPTION_PROTECT;
237 return 0;
238 }
239
240 int
main(int argc,char ** argv)241 main(int argc, char** argv)
242 {
243 return protected_main(argv, [&] {
244 const argp ap = { options, parse_opt, "N|PROP...", argp_program_doc,
245 children, nullptr, nullptr };
246
247 // This will ensure that all objects stored in this struct are
248 // destroyed before global variables.
249 opt_t o;
250 opt = &o;
251
252 if (int err = argp_parse(&ap, argc, argv, ARGP_NO_HELP, nullptr, nullptr))
253 exit(err);
254
255 // running 'randltl 0' is one way to generate formulas using no
256 // atomic propositions so do not complain in that case.
257 if (opt->aprops.empty() && !ap_count_given)
258 error(2, 0, "No atomic proposition supplied? "
259 "Run '%s --help' for usage.", program_name);
260
261 spot::srand(opt_seed);
262
263 spot::randltlgenerator rg
264 (opt->aprops,
265 [&] (){
266 spot::option_map opts;
267 opts.set("output", output);
268 opts.set("tree_size_min", opt_tree_size.min);
269 opts.set("tree_size_max", opt_tree_size.max);
270 opts.set("wf", opt_wf);
271 opts.set("seed", opt_seed);
272 opts.set("simplification_level", simplification_level);
273 opts.set("unique", opt_unique);
274 return opts;
275 }(), opt_pL, opt_pS, opt_pB);
276
277 if (opt_dump_priorities)
278 {
279 switch (output)
280 {
281 case spot::randltlgenerator::LTL:
282 std::cout <<
283 "Use --ltl-priorities to set the following LTL priorities:\n";
284 rg.dump_ltl_priorities(std::cout);
285 break;
286 case spot::randltlgenerator::Bool:
287 std::cout <<
288 "Use --boolean-priorities to set the following Boolean "
289 "formula priorities:\n";
290 rg.dump_bool_priorities(std::cout);
291 break;
292 case spot::randltlgenerator::PSL:
293 std::cout <<
294 "Use --ltl-priorities to set the following LTL priorities:\n";
295 rg.dump_psl_priorities(std::cout);
296 SPOT_FALLTHROUGH;
297 case spot::randltlgenerator::SERE:
298 std::cout <<
299 "Use --sere-priorities to set the following SERE priorities:\n";
300 rg.dump_sere_priorities(std::cout);
301 std::cout <<
302 "Use --boolean-priorities to set the following Boolean "
303 "formula priorities:\n";
304 rg.dump_sere_bool_priorities(std::cout);
305 break;
306 }
307 exit(0);
308 }
309
310 while (opt_formulas < 0 || opt_formulas--)
311 {
312 static int count = 0;
313 spot::formula f = rg.next();
314 if (!f)
315 {
316 error(2, 0, "failed to generate a new unique formula after %d " \
317 "trials", spot::randltlgenerator::MAX_TRIALS);
318 }
319 else
320 {
321 output_formula_checked(f, nullptr, nullptr, ++count);
322 }
323 };
324 flush_cout();
325 return 0;
326 });
327 }
328