25 #include <spot/tl/apcollect.hh>
28 #include <unordered_set>
29 #include <spot/misc/optionmap.hh>
30 #include <spot/misc/hash.hh>
31 #include <spot/tl/simplify.hh>
42 proba_size_(proba_size), proba_(
new op_proba[proba_size_]), ap_(
ap)
89 void setup(
const char* name,
int min_n, builder build);
97 double total_2_and_more_;
298 typedef std::unordered_set<formula> fset_t;
302 enum output_type { Bool, LTL, SERE, PSL };
303 static constexpr
unsigned MAX_TRIALS = 100000U;
306 char* opt_pL =
nullptr,
307 char* opt_pS =
nullptr,
308 char* opt_pB =
nullptr);
311 char* opt_pL =
nullptr,
312 char* opt_pS =
nullptr,
313 char* opt_pB =
nullptr);
319 void dump_ltl_priorities(std::ostream& os);
320 void dump_bool_priorities(std::ostream& os);
321 void dump_psl_priorities(std::ostream& os);
322 void dump_sere_priorities(std::ostream& os);
323 void dump_sere_bool_priorities(std::ostream& os);
333 int opt_tree_size_min_;
334 int opt_tree_size_max_;
337 int opt_simpl_level_;
Manage a map of options.
Definition: optionmap.hh:38
Definition: randomltl.hh:297
Generate random Boolean formulae.
Definition: randomltl.hh:165
random_boolean(const atomic_prop_set *ap)
Generate random LTL formulae.
Definition: randomltl.hh:115
random_ltl(const atomic_prop_set *ap)
Generate random PSL formulae.
Definition: randomltl.hh:246
random_sere rs
The SERE generator used to generate SERE subformulae.
Definition: randomltl.hh:293
random_psl(const atomic_prop_set *ap)
Generate random SERE.
Definition: randomltl.hh:205
random_sere(const atomic_prop_set *ap)
Rewrite or simplify f in various ways.
Definition: simplify.hh:110
std::set< formula > atomic_prop_set
Set of atomic propositions.
Definition: apcollect.hh:36
Definition: automata.hh:27