1 // -*- coding: utf-8 -*-
2 // Copyright (C) 2012-2016, 2018-2020 Laboratoire de Recherche et
3 // 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 <sstream>
27 #include <iterator>
28 #include "error.h"
29 #include "argmatch.h"
30
31 #include "common_setup.hh"
32 #include "common_range.hh"
33 #include "common_cout.hh"
34 #include "common_aoutput.hh"
35 #include "common_conv.hh"
36
37 #include <spot/misc/timer.hh>
38 #include <spot/misc/random.hh>
39
40 #include <spot/twa/bddprint.hh>
41 #include <spot/twaalgos/randomgraph.hh>
42 #include <spot/twaalgos/canonicalize.hh>
43
44
45 const char argp_program_doc[] = "\
46 Generate random connected automata.\n\n\
47 The automata are built over the atomic propositions named by PROPS...\n\
48 or, if N is a nonnegative number, using N arbitrary names.\n\
49 If the edge density is set to D, and the number of states to Q, the degree\n\
50 of each state follows a normal distribution with mean 1+(Q-1)D and\n\
51 variance (Q-1)D(1-D). In particular, for D=0 all states have a single\n\
52 successor, while for D=1 all states are interconnected.\v\
53 Examples:\n\
54 \n\
55 This builds a random neverclaim with 4 states and labeled using the two\n\
56 atomic propositions \"a\" and \"b\":\n\
57 % randaut --spin -Q4 a b\n\
58 \n\
59 This builds three random, complete, and deterministic TGBA with 5 to 10\n\
60 states, 1 to 3 acceptance sets, and three atomic propositions:\n\
61 % randaut -n3 -D -H -Q5..10 -A1..3 3\n\
62 \n\
63 Build 3 random, complete, and deterministic Rabin automata\n\
64 with 2 to 3 acceptance pairs, state-based acceptance, 8 states, \n\
65 a high density of edges, and 3 to 4 atomic propositions:\n\
66 % randaut -n3 -D -H -Q8 -e.8 -S -A 'Rabin 2..3' 3..4\n\
67 ";
68
69 enum {
70 OPT_SEED = 1,
71 OPT_COLORED,
72 };
73
74 static const argp_option options[] =
75 {
76 /**************************************************/
77 { nullptr, 0, nullptr, 0, "Generation:", 1 },
78 { "acceptance", 'A', "ACCEPTANCE", 0,
79 "specify the acceptance type of the automaton", 0 },
80 { "acc-probability", 'a', "FLOAT", 0,
81 "probability that an edge belongs to one acceptance set (0.2)", 0 },
82 { "automata", 'n', "INT", 0, "number of automata to output (1)\n"\
83 "use a negative value for unbounded generation", 0 },
84 { "sba", 'B', nullptr, 0,
85 "build a state-based Buchi automaton "
86 "(implies --acceptance=Buchi --state-acc)", 0 },
87 // historical name for --sba
88 { "ba", 0, nullptr, OPTION_ALIAS, nullptr, 0 },
89 { "buchi", 'b', nullptr, 0,
90 "build a Büchi automaton (same as --acceptance=Buchi)", 0 },
91 { "Buchi", 0, nullptr, OPTION_ALIAS, nullptr, 0 },
92 { "colored", OPT_COLORED, nullptr, 0,
93 "build an automaton in which each edge (or state if combined with "
94 "-S) belong to a single acceptance set", 0 },
95 { "density", 'e', "FLOAT", 0, "density of the edges (0.2)", 0 },
96 { "deterministic", 'D', nullptr, 0,
97 "build a complete, deterministic automaton ", 0 },
98 { "unique", 'u', nullptr, 0,
99 "do not output the same automaton twice (same in the sense that they "\
100 "are isomorphic)", 0 },
101 { "seed", OPT_SEED, "INT", 0,
102 "seed for the random number generator (0)", 0 },
103 { "states", 'Q', "RANGE", 0, "number of states to output (10)", 0 },
104 { "state-based-acceptance", 'S', nullptr, 0,
105 "used state-based acceptance", 0 },
106 { "sbacc", 0, nullptr, OPTION_ALIAS, nullptr, 0 },
107 RANGE_DOC,
108 { nullptr, 0, nullptr, 0, "ACCEPTANCE may be either a RANGE (in which case "
109 "generalized Büchi is assumed), or an arbitrary acceptance formula "
110 "such as 'Fin(0)|Inf(1)&Fin(2)' in the same syntax as in the HOA "
111 "format, or one of the following patterns:\n"
112 " none\n"
113 " all\n"
114 " Buchi\n"
115 " co-Buchi\n"
116 " generalized-Buchi RANGE\n"
117 " generalized-co-Buchi RANGE\n"
118 " Rabin RANGE\n"
119 " Streett RANGE\n"
120 " generalized-Rabin INT RANGE RANGE ... RANGE\n"
121 " parity (min|max|rand) (odd|even|rand) RANGE\n"
122 " random RANGE\n"
123 " random RANGE PROBABILITY\n"
124 "The random acceptance condition uses each set only once, "
125 "unless a probability (to reuse the set again every time it is used) "
126 "is given.", 2 },
127 /**************************************************/
128 { nullptr, 0, nullptr, 0, "Miscellaneous options:", -1 },
129 { nullptr, 0, nullptr, 0, nullptr, 0 }
130 };
131
132
133 static const struct argp_child children[] =
134 {
135 { &aoutput_argp, 0, nullptr, 3 },
136 { &aoutput_o_format_argp, 0, nullptr, 4 },
137 { &misc_argp, 0, nullptr, 0 },
138 { nullptr, 0, nullptr, 0 }
139 };
140
141 // We want all these variables to be destroyed when we exit main, to
142 // make sure it happens before all other global variables (like the
143 // atomic propositions maps) are destroyed. Otherwise we risk
144 // accessing deleted stuff.
145 static struct opt_t
146 {
147 spot::atomic_prop_set aprops;
148 }* opt;
149
150 static const char* opt_acceptance = nullptr;
151 typedef spot::twa_graph::graph_t::edge_storage_t tr_t;
152 typedef std::set<std::vector<tr_t>> unique_aut_t;
153 static range ap_count_given = {-1, -2}; // Must be two different negative val
154 static int opt_seed = 0;
155 static const char* opt_seed_str = "0";
156 static int opt_automata = 1;
157 static range opt_states = { 10, 10 };
158 static float opt_density = 0.2;
159 static range opt_acc_sets = { -1, 0 };
160 static float opt_acc_prob = 0.2;
161 static bool opt_deterministic = false;
162 static bool opt_state_acc = false;
163 static bool opt_colored = false;
164 static bool ba_wanted = false;
165 static bool generic_wanted = false;
166 static bool gba_wanted = false;
167 static std::unique_ptr<unique_aut_t> opt_uniq = nullptr;
168
169 static void
ba_options(bool sbacc)170 ba_options(bool sbacc)
171 {
172 opt_acc_sets = { 1, 1 };
173 opt_state_acc = sbacc;
174 }
175
176 // Range should have the form 12..34 or 12:34, maybe with spaces. The
177 // characters between '.' and ':' include all digits plus '/', but the
178 // parser will later choke on '/' if it is used, so let's not worry
179 // here.
180 static bool
looks_like_a_range(const char * str)181 looks_like_a_range(const char* str)
182 {
183 while (*str == ' ' || (*str >= '.' && *str <= ':'))
184 ++str;
185 return !*str;
186 }
187
188 static int
parse_opt(int key,char * arg,struct argp_state * as)189 parse_opt(int key, char* arg, struct argp_state* as)
190 {
191 // Called from C code, so should not raise any exception.
192 BEGIN_EXCEPTION_PROTECT;
193 // This switch is alphabetically-ordered.
194 switch (key)
195 {
196 case '8':
197 spot::enable_utf8();
198 break;
199 case 'a':
200 opt_acc_prob = to_probability(arg, "-a/--acc-probability");
201 break;
202 case 'A':
203 if (looks_like_a_range(arg))
204 {
205 opt_acc_sets = parse_range(arg);
206 if (opt_acc_sets.min > opt_acc_sets.max)
207 std::swap(opt_acc_sets.min, opt_acc_sets.max);
208 if (opt_acc_sets.min < 0)
209 error(2, 0, "number of acceptance sets should be positive");
210 gba_wanted = true;
211 }
212 else
213 {
214 opt_acceptance = arg;
215 generic_wanted = true;
216 }
217 break;
218 case 'b':
219 ba_options(false);
220 ba_wanted = true;
221 break;
222 case 'B':
223 ba_options(true);
224 ba_wanted = true;
225 break;
226 case 'e':
227 opt_density = to_probability(arg, "-e/--density");
228 break;
229 case 'D':
230 opt_deterministic = true;
231 break;
232 case 'n':
233 opt_automata = to_int(arg, "-n/--automata");
234 break;
235 case 'Q':
236 opt_states = parse_range(arg);
237 if (opt_states.min > opt_states.max)
238 std::swap(opt_states.min, opt_states.max);
239 if (opt_states.min == 0)
240 error(1, 0, "cannot build an automaton with 0 states");
241 break;
242 case 'S':
243 opt_state_acc = true;
244 break;
245 case 'u':
246 opt_uniq =
247 std::unique_ptr<unique_aut_t>(new std::set<std::vector<tr_t>>());
248 break;
249 case OPT_COLORED:
250 opt_colored = true;
251 break;
252 case OPT_SEED:
253 opt_seed = to_int(arg, "--seed");
254 opt_seed_str = arg;
255 break;
256 case ARGP_KEY_ARG:
257 // If this is the unique non-option argument, it can
258 // be a number of atomic propositions to build.
259 //
260 // argp reorganizes argv[] so that options always come before
261 // non-options. So if as->argc == as->next we know this is the
262 // last non-option argument, and if aprops.empty() we know this
263 // is the also the first one.
264 if (opt->aprops.empty()
265 && as->argc == as->next && looks_like_a_range(arg))
266 {
267 ap_count_given = parse_range(arg);
268 // Create the set once if the count is fixed.
269 if (ap_count_given.min == ap_count_given.max)
270 opt->aprops = spot::create_atomic_prop_set(ap_count_given.min);
271 break;
272 }
273 opt->aprops.insert(spot::formula::ap(arg));
274 break;
275
276 default:
277 return ARGP_ERR_UNKNOWN;
278 }
279 END_EXCEPTION_PROTECT;
280 return 0;
281 }
282
283
284 int
main(int argc,char ** argv)285 main(int argc, char** argv)
286 {
287 return protected_main(argv, [&] {
288 strcpy(F_doc, "seed number");
289 strcpy(L_doc, "automaton number");
290
291 const argp ap = { options, parse_opt, "N|PROP...", argp_program_doc,
292 children, nullptr, nullptr };
293
294 // This will ensure that all objects stored in this struct are
295 // destroyed before global variables.
296 opt_t o;
297 opt = &o;
298
299 if (int err = argp_parse(&ap, argc, argv, ARGP_NO_HELP, nullptr, nullptr))
300 exit(err);
301
302 // running 'randaut 0' is one way to generate automata using no
303 // atomic propositions so do not complain in that case.
304 if (opt->aprops.empty() && ap_count_given.max < 0)
305 error(2, 0,
306 "No atomic proposition supplied? Run '%s --help' for usage.",
307 program_name);
308
309 if (generic_wanted && automaton_format == Spin)
310 error(2, 0,
311 "--spin implies --ba so should not be used with --acceptance");
312 if (generic_wanted && ba_wanted)
313 error(2, 0, "--acceptance and %s may not be used together",
314 opt_state_acc ? "--ba" : "--buchi");
315
316 if (automaton_format == Spin && opt_acc_sets.max > 1)
317 error(2, 0, "--spin is incompatible with --acceptance=%d..%d",
318 opt_acc_sets.min, opt_acc_sets.max);
319 if (ba_wanted && opt_acc_sets.min != 1 && opt_acc_sets.max != 1)
320 error(2, 0, "%s is incompatible with --acceptance=%d..%d",
321 opt_state_acc ? "--ba" : "--buchi",
322 opt_acc_sets.min, opt_acc_sets.max);
323 if (ba_wanted && generic_wanted)
324 error(2, 0,
325 "--ba is incompatible with --acceptance=%s", opt_acceptance);
326
327 if (automaton_format == Spin)
328 ba_options(true);
329
330 if (opt_colored && opt_acc_sets.min == -1 && !generic_wanted)
331 error(2, 0, "--colored requires at least one acceptance set; "
332 "use --acceptance");
333 if (opt_colored && opt_acc_sets.min == 0)
334 error(2, 0, "--colored requires at least one acceptance set; "
335 "fix the range of --acceptance");
336
337 if (opt_acc_sets.min == -1)
338 opt_acc_sets.min = 0;
339
340 spot::srand(opt_seed);
341 auto d = spot::make_bdd_dict();
342
343 automaton_printer printer;
344
345 constexpr unsigned max_trials = 10000;
346 unsigned trials = max_trials;
347
348 int automaton_num = 0;
349
350 for (;;)
351 {
352 spot::process_timer timer;
353 timer.start();
354
355 if (ap_count_given.max > 0
356 && ap_count_given.min != ap_count_given.max)
357 {
358 int c = spot::rrand(ap_count_given.min, ap_count_given.max);
359 opt->aprops = spot::create_atomic_prop_set(c);
360 }
361
362 int size = opt_states.min;
363 if (size != opt_states.max)
364 size = spot::rrand(size, opt_states.max);
365
366 int accs = opt_acc_sets.min;
367 if (accs != opt_acc_sets.max)
368 accs = spot::rrand(accs, opt_acc_sets.max);
369
370 spot::acc_cond::acc_code code;
371 if (opt_acceptance)
372 {
373 code = spot::acc_cond::acc_code(opt_acceptance);
374 accs = code.used_sets().max_set();
375 if (opt_colored && accs == 0)
376 error(2, 0, "--colored requires at least one acceptance set; "
377 "fix the range of --acceptance");
378 }
379
380 auto aut =
381 spot::random_graph(size, opt_density, &opt->aprops, d,
382 accs, opt_acc_prob, 0.5,
383 opt_deterministic, opt_state_acc,
384 opt_colored);
385
386 if (opt_acceptance)
387 aut->set_acceptance(accs, code);
388
389 if (opt_uniq)
390 {
391 auto tmp = spot::canonicalize
392 (make_twa_graph(aut, spot::twa::prop_set::all()));
393 std::vector<tr_t> trans(tmp->edge_vector().begin() + 1,
394 tmp->edge_vector().end());
395 if (!opt_uniq->emplace(trans).second)
396 {
397 --trials;
398 if (trials == 0)
399 error(2, 0, "failed to generate a new unique automaton"
400 " after %d trials", max_trials);
401 continue;
402 }
403 trials = max_trials;
404 }
405
406 timer.stop();
407
408 printer.print(aut, timer, nullptr,
409 opt_seed_str, automaton_num, nullptr);
410
411 ++automaton_num;
412 if (opt_automata > 0 && automaton_num >= opt_automata)
413 break;
414 }
415 return 0;
416 });
417 }
418