Generate random LTL formulas. More...

#include <spot/tl/randomltl.hh>

Inheritance diagram for spot::random_ltl:

Collaboration diagram for spot::random_ltl:

Public Member Functions
	random_ltl (const atomic_prop_set ap, const atomic_prop_set output_ap=nullptr, std::function< bool(formula)> is_output=nullptr, const atomic_prop_set *subformulas=nullptr)

const atomic_prop_set *	ap () const
	Return the set of atomic proposition used to build formulas. More...

const atomic_prop_set *	output_ap () const
	Return the set of atomic proposition used to build formulas. More...

std::function< bool(formula)>	is_output_fun () const
	Return the predicate that classifies propositions as output. More...

const atomic_prop_set *	patterns () const
	Return the set of patterns (sub-formulas) used to build formulas. More...

bool	draw_literals () const
	Check whether relabeling APs should use literals. More...

void	draw_literals (bool lit)
	Set whether relabeling APs should use literals. More...

formula	generate (int n) const
	Generate a formula of size n. More...

std::ostream &	dump_priorities (std::ostream &os) const
	Print the priorities of each operator, constants, and atomic propositions. More...

const char *	parse_options (const char *options)
	Update the priorities used to generate the formulas. More...

bool	has_unary_ops () const
	whether we can use unary operators More...

Protected Member Functions
void	setup_proba_ (const atomic_prop_set *patterns)
	Initialize the probability table, optionally using patterns as atoms. More...

	random_ltl (int size, const atomic_prop_set ap, const atomic_prop_set output_ap=nullptr, std::function< bool(formula)> is_output=nullptr)
	Construct with explicit table size (for subclasses). More...

void	update_sums ()
	Recompute running probability sums after priorities have changed. More...

Protected Attributes
unsigned	proba_size_
	Number of entries in the operator table. More...

op_proba *	proba_
	Operator probability table. More...

double	total_1_
	Total weight of unary operators. More...

op_proba *	proba_2_
	Pointer to binary operators in the table. More...

double	total_2_
	Total weight of binary operators. More...

op_proba *	proba_2_or_more_

double	total_2_and_more_
	Total weight of operators needing two or more children. More...

const atomic_prop_set *	ap_

const atomic_prop_set *	output_ap_ = nullptr
	Output atomic propositions (may be null if not used). More...

const atomic_prop_set *	patterns_ = nullptr
	Sub-formula patterns used as atoms (may be null). More...

std::function< bool(formula)>	is_output_ = nullptr
	Predicate classifying a proposition as an output (may be null). More...

bool	draw_literals_
	Whether relabeling APs should use literals. More...

Detailed Description

Generate random LTL formulas.

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

By default each operator has equal chance to be selected. Also, each atomic proposition has as much chance as each constant (i.e., true and false) to be picked. This can be tuned using parse_options().

Constructor & Destructor Documentation

◆ random_ltl() [1/2]

spot::random_ltl::random_ltl	(	const atomic_prop_set *	ap,
		const atomic_prop_set *	output_ap = `nullptr`,
		std::function< bool(formula)>	is_output = `nullptr`,
		const atomic_prop_set *	subformulas = `nullptr`
	)

Create a random LTL generator using atomic propositions from ap.

The default priorities are defined as follows, depending on the presence of subformulas.

ap      n              sub     n
false   1              false   1
true    1              true    1
not     1              not     1
F       1              F       1
G       1              G       1
X       1              X       1
strongX 0              strongX 0
equiv   1              equiv   1
implies 1              implies 1
xor     1              xor     1
R       1              R       1
U       1              U       1
W       1              W       1
M       1              M       1
and     1              and     1
or      1              or      1

Where n is the number of atomic propositions in the set passed to the constructor.

This means that each operator has equal chance to be selected. Also, each atomic proposition has as much chance as each constant (i.e., true and false) to be picked.

These priorities can be changed using the parse_options method.

If a set of subformulas is passed to the constructor, the generator will build a Boolean formulas using patterns as atoms. Atomic propositions in patterns will be rewritten randomly by drawing some from ap. The probability of false/true to be generated default to 0 in this case.

◆ random_ltl() [2/2]

spot::random_ltl::random_ltl	(	int	size,
		const atomic_prop_set *	ap,
		const atomic_prop_set *	output_ap = `nullptr`,
		std::function< bool(formula)>	is_output = `nullptr`
	)

protected

Construct with explicit table size (for subclasses).

Member Function Documentation

◆ ap()

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

inlineinherited

Return the set of atomic proposition used to build formulas.

◆ 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

◆ is_output_fun()

std::function<bool(formula)> spot::random_formula::is_output_fun ( ) const

inlineinherited

Return the predicate that classifies propositions as output.

◆ output_ap()

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

inlineinherited

Return the set of atomic proposition used to build formulas.

◆ parse_options()

const char* spot::random_formula::parse_options ( const 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.

The input string is not modified.

◆ patterns()

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

inlineinherited

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

◆ setup_proba_()

void spot::random_ltl::setup_proba_ ( const atomic_prop_set * patterns )

protected

Initialize the probability table, optionally using patterns as atoms.

◆ update_sums()

void spot::random_formula::update_sums ( )

protectedinherited

Recompute running probability sums after priorities have changed.

Member Data Documentation

◆ ap_

const atomic_prop_set* spot::random_formula::ap_

protectedinherited

Atomic propositions used to build formulas.

◆ draw_literals_

bool spot::random_formula::draw_literals_

protectedinherited

Whether relabeling APs should use literals.

◆ is_output_

std::function<bool(formula)> spot::random_formula::is_output_ = nullptr

protectedinherited

Predicate classifying a proposition as an output (may be null).

◆ output_ap_

const atomic_prop_set* spot::random_formula::output_ap_ = nullptr

protectedinherited

Output atomic propositions (may be null if not used).

◆ patterns_

const atomic_prop_set* spot::random_formula::patterns_ = nullptr

protectedinherited

Sub-formula patterns used as atoms (may be null).

◆ proba_

op_proba* spot::random_formula::proba_

protectedinherited

Operator probability table.

◆ proba_2_

op_proba* spot::random_formula::proba_2_

protectedinherited

Pointer to binary operators in the table.

◆ proba_2_or_more_

op_proba* spot::random_formula::proba_2_or_more_

protectedinherited

Pointer to operators needing ≥2 children.

◆ proba_size_

unsigned spot::random_formula::proba_size_

protectedinherited

Number of entries in the operator table.

◆ total_1_

double spot::random_formula::total_1_

protectedinherited

Total weight of unary operators.

◆ total_2_

double spot::random_formula::total_2_

protectedinherited

Total weight of binary operators.

◆ total_2_and_more_

double spot::random_formula::total_2_and_more_

protectedinherited

Total weight of operators needing two or more children.

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

spot/tl/randomltl.hh

Public Member Functions

Protected Member Functions

Protected Attributes

Detailed Description

Constructor & Destructor Documentation

◆ random_ltl() [1/2]

◆ random_ltl() [2/2]

Member Function Documentation

◆ ap()

◆ draw_literals() [1/2]

◆ draw_literals() [2/2]

◆ dump_priorities()

◆ generate()

◆ has_unary_ops()

◆ is_output_fun()

◆ output_ap()

◆ parse_options()

◆ patterns()

◆ setup_proba_()

◆ update_sums()

Member Data Documentation

◆ ap_

◆ draw_literals_

◆ is_output_

◆ output_ap_

◆ patterns_

◆ proba_

◆ proba_2_

◆ proba_2_or_more_

◆ proba_size_

◆ total_1_

◆ total_2_

◆ total_2_and_more_