Generator of random LTL/PSL/SERE/Boolean formulas with configurable options. More...

#include <spot/tl/randomltl.hh>

Collaboration diagram for spot::randltlgenerator:

Public Types
enum	output_type { Bool , LTL , SERE , PSL }
	Output formula type produced by the generator. More...

Public Member Functions
	randltlgenerator (int aprops_n, const option_map &opts, const char opt_pL=nullptr, const char opt_pS=nullptr, const char opt_pB=nullptr, const atomic_prop_set subformulas=nullptr, std::function< bool(formula)> is_output=nullptr)
	Construct with aprops_n random atomic propositions. More...

	randltlgenerator (atomic_prop_set aprops, const option_map &opts, const char opt_pL=nullptr, const char opt_pS=nullptr, const char opt_pB=nullptr, const atomic_prop_set subformulas=nullptr, std::function< bool(formula)> is_output=nullptr)
	Construct with an explicit set of atomic propositions. More...

formula	next ()
	Generate the next random formula (up to MAX_TRIALS attempts). More...

void	dump_ltl_priorities (std::ostream &os)
	Print LTL operator priorities to os. More...

void	dump_bool_priorities (std::ostream &os)
	Print Boolean operator priorities to os. More...

void	dump_psl_priorities (std::ostream &os)
	Print PSL operator priorities to os. More...

void	dump_sere_priorities (std::ostream &os)
	Print SERE operator priorities to os. More...

void	dump_sere_bool_priorities (std::ostream &os)
	Print SERE Boolean operator priorities to os. More...

void	remove_some_props (atomic_prop_set &s)
	Remove some propositions from s (used for well-formed generation). More...

formula	GF_n ()
	Return a GF(p1 & ... & pn) formula over n random propositions. More...

Static Public Attributes
static constexpr unsigned	MAX_TRIALS = 100000U
	Maximum number of attempts to generate a unique formula. More...

Detailed Description

Generator of random LTL/PSL/SERE/Boolean formulas with configurable options.

Member Enumeration Documentation

◆ output_type

enum spot::randltlgenerator::output_type

Output formula type produced by the generator.

Constructor & Destructor Documentation

◆ randltlgenerator() [1/2]

spot::randltlgenerator::randltlgenerator	(	int	aprops_n,
		const option_map &	opts,
		const char *	opt_pL = `nullptr`,
		const char *	opt_pS = `nullptr`,
		const char *	opt_pB = `nullptr`,
		const atomic_prop_set *	subformulas = `nullptr`,
		std::function< bool(formula)>	is_output = `nullptr`
	)

Construct with aprops_n random atomic propositions.

◆ randltlgenerator() [2/2]

spot::randltlgenerator::randltlgenerator	(	atomic_prop_set	aprops,
		const option_map &	opts,
		const char *	opt_pL = `nullptr`,
		const char *	opt_pS = `nullptr`,
		const char *	opt_pB = `nullptr`,
		const atomic_prop_set *	subformulas = `nullptr`,
		std::function< bool(formula)>	is_output = `nullptr`
	)

Construct with an explicit set of atomic propositions.

Member Function Documentation

◆ dump_bool_priorities()

void spot::randltlgenerator::dump_bool_priorities ( std::ostream & os )

Print Boolean operator priorities to os.

◆ dump_ltl_priorities()

void spot::randltlgenerator::dump_ltl_priorities ( std::ostream & os )

Print LTL operator priorities to os.

◆ dump_psl_priorities()

void spot::randltlgenerator::dump_psl_priorities ( std::ostream & os )

Print PSL operator priorities to os.

◆ dump_sere_bool_priorities()

void spot::randltlgenerator::dump_sere_bool_priorities ( std::ostream & os )

Print SERE Boolean operator priorities to os.

◆ dump_sere_priorities()

void spot::randltlgenerator::dump_sere_priorities ( std::ostream & os )

Print SERE operator priorities to os.

◆ GF_n()

formula spot::randltlgenerator::GF_n ( )

Return a GF(p1 & ... & pn) formula over n random propositions.

◆ next()

formula spot::randltlgenerator::next ( )

Generate the next random formula (up to MAX_TRIALS attempts).

◆ remove_some_props()

void spot::randltlgenerator::remove_some_props ( atomic_prop_set & s )

Remove some propositions from s (used for well-formed generation).

Member Data Documentation

◆ MAX_TRIALS

constexpr unsigned spot::randltlgenerator::MAX_TRIALS = 100000U

staticconstexpr

Maximum number of attempts to generate a unique formula.

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

spot/tl/randomltl.hh

Public Types

Public Member Functions

Static Public Attributes