spot::random_sere Class Reference

Generate random SERE. More...

#include <spot/tl/randomltl.hh>

Inheritance diagram for spot::random_sere:

Collaboration diagram for spot::random_sere:

Public Member Functions
	random_sere (const atomic_prop_set *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
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

Public Attributes
random_boolean	rb

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

Generate random SERE.

This class recursively constructs SERE of a given size. The formulas will use the use atomic propositions from the set of propositions passed to the constructor, in addition to the constant and all SERE operators supported by Spot.

By default each operator has equal chance to be selected.

Constructor & Destructor Documentation

random_sere()

spot::random_sere::random_sere

(

const atomic_prop_set *

ap

)

Create a random SERE generator using atomic propositions from ap.

The default priorities are defined as follows:

eword    1
boolform 1
star     1
star_b   1
equal_b  1
goto_b   1
and      1
andNLM   1
or       1
concat   1
fusion   1

Where "boolfrom" designates a Boolean formula generated by random_boolean.

These priorities can be changed use the parse_options method.

In addition, you can set the properties of the Boolean formula generator used to build Boolean subformulas using the parse_options method of the rb attribute.

References spot::random_formula::ap().

Member Function Documentation

ap()

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

inlineinherited

Return the set of atomic proposition used to build formulas.

Referenced by spot::random_boolean::random_boolean(), spot::random_ltl::random_ltl(), spot::random_psl::random_psl(), and spot::random_sere::random_sere().

draw_literals() [1/2]

bool spot::random_formula::draw_literals ( ) const

inlineinherited

Check whether relabeling APs should use literals.

draw_literals() [2/2]

void spot::random_formula::draw_literals ( bool lit )

inlineinherited

Set whether relabeling APs should use literals.

dump_priorities()

std::ostream & spot::random_formula::dump_priorities ( std::ostream & os ) const

inherited

Print the priorities of each operator, constants, and atomic propositions.

generate()

formula spot::random_formula::generate ( int n ) const

inherited

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

inlineinherited

whether we can use unary operators

output_ap()

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

inlineinherited

Return the set of atomic proposition used to build formulas.

Referenced by spot::random_boolean::random_boolean(), and spot::random_ltl::random_ltl().

parse_options()

const char * spot::random_formula::parse_options ( char * options )

inherited

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

inlineinherited

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

Referenced by spot::random_ltl::random_ltl().

---

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

• spot/tl/randomltl.hh