Base class for random formula generators.
More...
#include <spot/tl/randomltl.hh>
|
| random_formula (unsigned proba_size, const atomic_prop_set *ap, const atomic_prop_set *output_ap=nullptr, std::function< bool(formula)> is_output=nullptr) |
|
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 |
|
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 (char *options) |
| Update the priorities used to generate the formulas.
|
|
bool | has_unary_ops () const |
| whether we can use unary operators
|
|
Base class for random formula generators.
◆ 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
◆ output_ap()
Return the set of atomic proposition used to build formulas.
◆ parse_options()
const char * spot::random_formula::parse_options |
( |
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.
◆ patterns()
Return the set of patterns (sub-formulas) used to build formulas.
The documentation for this class was generated from the following file: