spot::random_formula Class Reference

Base class for random formula generators. More...

#include <spot/tl/randomltl.hh>

Inheritance diagram for spot::random_formula:

Collaboration diagram for spot::random_formula:

Classes
struct	op_proba

Public Member Functions
	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

Protected Member Functions
void	update_sums ()

Protected Attributes
unsigned	proba_size_
op_proba *	proba_
double	total_1_
op_proba *	proba_2_
double	total_2_
op_proba *	proba_2_or_more_
double	total_2_and_more_
const atomic_prop_set *	ap_
const atomic_prop_set *	output_ap_ = nullptr
const atomic_prop_set *	patterns_ = nullptr
std::function< bool(formula)>	is_output_ = nullptr
bool	draw_literals_

Detailed Description

Base class for random formula generators.

Member Function Documentation

ap()

const atomic_prop_set * spot::random_formula::ap ( ) const

inline

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()

const atomic_prop_set * spot::random_formula::output_ap ( ) const

inline

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()

const atomic_prop_set * spot::random_formula::patterns ( ) const

inline

Return the set of patterns (sub-formulas) used to build formulas.

---

The documentation for this class was generated from the following file:

• spot/tl/randomltl.hh