Base class for random formula generators.
More...
#include <spot/tl/randomltl.hh>
|
| struct | op_proba |
| | Entry describing one operator and its probability for random formula generation. More...
|
| |
|
| | random_formula (unsigned proba_size, const atomic_prop_set *ap, const atomic_prop_set *output_ap=nullptr, std::function< bool(formula)> is_output=nullptr) |
| | Construct with proba_size operator slots and atomic propositions ap.
|
| |
| const atomic_prop_set * | ap () const |
| | Return the set of atomic proposition used to build formulas.
|
| |
| const atomic_prop_set * | output_ap () const |
| | Return the set of atomic proposition used to build formulas.
|
| |
| std::function< bool(formula)> | is_output_fun () const |
| | Return the predicate that classifies propositions as output.
|
| |
| const atomic_prop_set * | patterns () const |
| | Return the set of patterns (sub-formulas) used to build formulas.
|
| |
| bool | draw_literals () const |
| | Check whether relabeling APs should use literals.
|
| |
| void | draw_literals (bool lit) |
| | Set whether relabeling APs should use literals.
|
| |
| formula | generate (int n) const |
| | Generate a formula of size n.
|
| |
| std::ostream & | dump_priorities (std::ostream &os) const |
| | Print the priorities of each operator, constants, and atomic propositions.
|
| |
| const char * | parse_options (const char *options) |
| | Update the priorities used to generate the formulas.
|
| |
| bool | has_unary_ops () const |
| | whether we can use unary operators
|
| |
|
| void | update_sums () |
| | Recompute running probability sums after priorities have changed.
|
| |
Base class for random formula generators.
◆ random_formula()
Construct with proba_size operator slots and atomic propositions ap.
References spot::ap.
◆ ap()
Return the set of atomic proposition used to build formulas.
◆ draw_literals() [1/2]
| bool spot::random_formula::draw_literals |
( |
| ) |
const |
|
inline |
Check whether relabeling APs should use literals.
◆ draw_literals() [2/2]
| void spot::random_formula::draw_literals |
( |
bool |
lit | ) |
|
|
inline |
Set whether relabeling APs should use literals.
◆ dump_priorities()
| std::ostream & spot::random_formula::dump_priorities |
( |
std::ostream & |
os | ) |
const |
Print the priorities of each operator, constants, and atomic propositions.
◆ generate()
| formula spot::random_formula::generate |
( |
int |
n | ) |
const |
Generate a formula of size n.
It is possible to obtain formulas that are smaller than n, because some simple simplifications are performed by the AST. (For instance the formula a | a is automatically reduced to a by spot::multop.)
◆ has_unary_ops()
| bool spot::random_formula::has_unary_ops |
( |
| ) |
const |
|
inline |
whether we can use unary operators
◆ is_output_fun()
| std::function< bool(formula)> spot::random_formula::is_output_fun |
( |
| ) |
const |
|
inline |
Return the predicate that classifies propositions as output.
◆ output_ap()
Return the set of atomic proposition used to build formulas.
◆ parse_options()
| const char * spot::random_formula::parse_options |
( |
const char * |
options | ) |
|
Update the priorities used to generate the formulas.
options should be comma-separated list of KEY=VALUE assignments, using keys from the above list. For instance "xor=0, F=3" will prevent xor from being used, and will raise the relative probability of occurrences of the F operator.
The input string is not modified.
◆ patterns()
Return the set of patterns (sub-formulas) used to build formulas.
◆ update_sums()
| void spot::random_formula::update_sums |
( |
| ) |
|
|
protected |
Recompute running probability sums after priorities have changed.
◆ ap_
Atomic propositions used to build formulas.
◆ draw_literals_
| bool spot::random_formula::draw_literals_ |
|
protected |
Whether relabeling APs should use literals.
◆ is_output_
| std::function<bool(formula)> spot::random_formula::is_output_ = nullptr |
|
protected |
Predicate classifying a proposition as an output (may be null).
◆ output_ap_
Output atomic propositions (may be null if not used).
◆ patterns_
Sub-formula patterns used as atoms (may be null).
◆ proba_
Operator probability table.
◆ proba_2_
| op_proba* spot::random_formula::proba_2_ |
|
protected |
Pointer to binary operators in the table.
◆ proba_2_or_more_
| op_proba* spot::random_formula::proba_2_or_more_ |
|
protected |
Pointer to operators needing ≥2 children.
◆ proba_size_
| unsigned spot::random_formula::proba_size_ |
|
protected |
Number of entries in the operator table.
◆ total_1_
| double spot::random_formula::total_1_ |
|
protected |
Total weight of unary operators.
◆ total_2_
| double spot::random_formula::total_2_ |
|
protected |
Total weight of binary operators.
◆ total_2_and_more_
| double spot::random_formula::total_2_and_more_ |
|
protected |
Total weight of operators needing two or more children.
The documentation for this class was generated from the following file:
