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