21#include <spot/tl/apcollect.hh>
24#include <unordered_set>
25#include <spot/misc/optionmap.hh>
26#include <spot/misc/hash.hh>
27#include <spot/tl/simplify.hh>
38 proba_size_(proba_size), proba_(
new op_proba[proba_size_]), ap_(
ap)
62 return draw_literals_;
95 return total_2_ > 0.0;
108 void setup(
const char* name,
int min_n, builder build);
110 unsigned proba_size_;
116 double total_2_and_more_;
334 typedef std::unordered_set<formula> fset_t;
338 enum output_type { Bool, LTL, SERE, PSL };
339 static constexpr unsigned MAX_TRIALS = 100000U;
342 char* opt_pL =
nullptr,
343 char* opt_pS =
nullptr,
344 char* opt_pB =
nullptr,
348 char* opt_pL =
nullptr,
349 char* opt_pS =
nullptr,
350 char* opt_pB =
nullptr,
357 void dump_ltl_priorities(std::ostream& os);
358 void dump_bool_priorities(std::ostream& os);
359 void dump_psl_priorities(std::ostream& os);
360 void dump_sere_priorities(std::ostream& os);
361 void dump_sere_bool_priorities(std::ostream& os);
371 int opt_tree_size_min_;
372 int opt_tree_size_max_;
375 int opt_simpl_level_;
Manage a map of options.
Definition optionmap.hh:34
Definition randomltl.hh:333
Generate random Boolean formulas.
Definition randomltl.hh:194
random_boolean(const atomic_prop_set *ap, const atomic_prop_set *subformulas=nullptr)
Generate random LTL formulas.
Definition randomltl.hh:136
random_ltl(const atomic_prop_set *ap, const atomic_prop_set *subformulas=nullptr)
Generate random PSL formulas.
Definition randomltl.hh:282
random_sere rs
The SERE generator used to generate SERE subformulas.
Definition randomltl.hh:329
random_psl(const atomic_prop_set *ap)
Generate random SERE.
Definition randomltl.hh:241
random_sere(const atomic_prop_set *ap)
Rewrite or simplify f in various ways.
Definition simplify.hh:109
std::set< formula > atomic_prop_set
Set of atomic propositions.
Definition apcollect.hh:33
Definition automata.hh:26