Main class for temporal logic formula. More...

#include <spot/tl/formula.hh>

Collaboration diagram for spot::formula:

Classes
class	formula_child_iterator
	Allow iterating over children. More...

Public Member Functions
	formula (const fnode *f) noexcept
	Create a formula from an fnode. More...

	formula (std::nullptr_t) noexcept
	Create a null formula. More...

	formula () noexcept
	Default initialize a formula to nullptr. More...

	formula (const formula &f) noexcept
	Clone a formula. More...

	formula (formula &&f) noexcept
	Move-construct a formula. More...

	~formula ()
	Destroy a formula. More...

const formula &	operator= (std::nullptr_t)
	Reset a formula to null. More...

const formula &	operator= (const formula &f)

const formula &	operator= (formula &&f) noexcept

bool	operator< (const formula &other) const noexcept

bool	operator<= (const formula &other) const noexcept

bool	operator> (const formula &other) const noexcept

bool	operator>= (const formula &other) const noexcept

bool	operator== (const formula &other) const noexcept

bool	operator== (std::nullptr_t) const noexcept

bool	operator!= (const formula &other) const noexcept

bool	operator!= (std::nullptr_t) const noexcept

	operator bool () const noexcept

const fnode *	to_node_ ()
	Return the underlying pointer to the formula. More...

op	kind () const
	Return top-most operator. More...

std::string	kindstr () const
	Return the name of the top-most operator. More...

bool	is (op o) const
	Return true if the formula is of kind o. More...

bool	is (op o1, op o2) const
	Return true if the formula is of kind o1 or o2. More...

bool	is (op o1, op o2, op o3) const
	Return true if the formula is of kind o1 or o2 or o3. More...

bool	is (op o1, op o2, op o3, op o4) const

bool	is (std::initializer_list< op > l) const
	Return true if the formulas nests all the operators in l. More...

formula	get_child_of (op o) const
	Remove operator o and return the child. More...

formula	get_child_of (std::initializer_list< op > l) const
	Remove all operators in l and return the child. More...

unsigned	min () const
	Return start of the range for star-like operators. More...

unsigned	max () const
	Return end of the range for star-like operators. More...

unsigned	size () const
	Return the number of children. More...

bool	is_leaf () const
	Whether the formula is a leaf. More...

size_t	id () const
	Return the id of a formula. More...

formula_child_iterator	begin () const
	Allow iterating over children. More...

formula_child_iterator	end () const
	Allow iterating over children. More...

formula	operator[] (unsigned i) const
	Return children number i. More...

bool	is_ff () const
	Whether the formula is the false constant. More...

bool	is_tt () const
	Whether the formula is the true constant. More...

bool	is_eword () const
	Whether the formula is the empty word constant. More...

bool	is_constant () const
	Whether the formula is op::ff, op::tt, or op::eword. More...

bool	is_Kleene_star () const
	Test whether the formula represent a Kleene star. More...

bool	is_literal () const
	Whether the formula is an atomic proposition or its negation. More...

const std::string &	ap_name () const
	Print the name of an atomic proposition. More...

std::ostream &	dump (std::ostream &os) const
	Print the formula for debugging. More...

formula	all_but (unsigned i) const
	clone this formula, omitting child i More...

unsigned	boolean_count () const
	number of Boolean children More...

formula	boolean_operands (unsigned *width=nullptr) const
	return a clone of the current node, restricted to its Boolean children More...

bool	is_boolean () const
	Whether the formula use only boolean operators. More...

bool	is_sugar_free_boolean () const
	Whether the formula use only AND, OR, and NOT operators. More...

bool	is_in_nenoform () const
	Whether the formula is in negative normal form. More...

bool	is_syntactic_stutter_invariant () const
	Whether the formula is syntactically stutter_invariant. More...

bool	is_sugar_free_ltl () const
	Whether the formula avoids the F and G operators. More...

bool	is_ltl_formula () const
	Whether the formula uses only LTL operators. More...

bool	is_psl_formula () const
	Whether the formula uses only PSL operators. More...

bool	is_sere_formula () const
	Whether the formula uses only SERE operators. More...

bool	is_finite () const
	Whether a SERE describes a finite language, or an LTL formula uses no temporal operator but X. More...

bool	is_eventual () const
	Whether the formula is purely eventual. More...

bool	is_universal () const
	Whether a formula is purely universal. More...

bool	is_syntactic_safety () const
	Whether a PSL/LTL formula is syntactic safety property. More...

bool	is_syntactic_guarantee () const
	Whether a PSL/LTL formula is syntactic guarantee property. More...

bool	is_delta1 () const
	Whether a PSL/LTL formula is in the Δ₁ syntactic frament. More...

bool	is_syntactic_obligation () const
	Whether a PSL/LTL formula is syntactic obligation property. More...

bool	is_sigma2 () const
	Whether a PSL/LTL formula is in Σ₂ More...

bool	is_pi2 () const
	Whether a PSL/LTL formula is in Π₂ More...

bool	is_syntactic_recurrence () const
	Whether a PSL/LTL formula is syntactic recurrence property. More...

bool	is_syntactic_persistence () const
	Whether a PSL/LTL formula is syntactic persistence property. More...

bool	is_delta2 () const
	Whether a PSL/LTL formula is in the Δ₂ syntactic frament. More...

bool	is_marked () const
	Whether the formula has an occurrence of EConcatMarked or NegClosureMarked. More...

bool	accepts_eword () const
	Whether the formula accepts [*0]. More...

bool	has_lbt_atomic_props () const
	Whether the formula has only LBT-compatible atomic propositions. More...

bool	has_spin_atomic_props () const
	Whether the formula has spin-compatible atomic propositions. More...

template<typename Trans , typename... Args>
formula	map (Trans trans, Args &&... args)
	Clone this node after applying trans to its children. More...

template<typename Func , typename... Args>
void	traverse (Func func, Args &&... args)
	Apply func to each subformula. More...

Static Public Member Functions
static constexpr uint8_t	unbounded ()
	Unbounded constant to use as end of range for bounded operators. More...

static formula	ap (const std::string &name)
	Build an atomic proposition. More...

static formula	ap (const formula &a)
	Build an atomic proposition from... an atomic proposition. More...

static formula	X (unsigned level, const formula &f)
	Construct an X[n]. More...

static formula	F (unsigned min_level, unsigned max_level, const formula &f)
	Construct F[n:m]. More...

static formula	G (unsigned min_level, unsigned max_level, const formula &f)
	Construct G[n:m]. More...

static const formula	nested_unop_range (op uo, op bo, unsigned min, unsigned max, formula f)
	Nested operator construction (syntactic sugar). More...

static formula	sugar_goto (const formula &b, unsigned min, unsigned max)
	Create a SERE equivalent to `b[->min..max]` More...

static formula	sugar_equal (const formula &b, unsigned min, unsigned max)
	Create the SERE `b[=min..max]` More...

static formula	ff ()
	Return the false constant. More...

static formula	tt ()
	Return the true constant. More...

static formula	eword ()
	Return the empty word constant. More...

static formula	one_star ()
	Return a copy of the formula 1[*]. More...

static formula	one_plus ()
	Return a copy of the formula 1[+]. More...


static formula	unop (op o, const formula &f)
	Build a unary operator. More...

static formula	unop (op o, formula &&f)
	Build a unary operator. More...


static formula	Not (const formula &f)
	Construct a negation. More...

static formula	Not (formula &&f)
	Construct a negation. More...


static formula	X (const formula &f)
	Construct an X. More...

static formula	X (formula &&f)
	Construct an X. More...


static formula	F (const formula &f)
	Construct an F. More...

static formula	F (formula &&f)
	Construct an F. More...


static formula	G (const formula &f)
	Construct a G. More...

static formula	G (formula &&f)
	Construct a G. More...


static formula	Closure (const formula &f)
	Construct a PSL Closure. More...

static formula	Closure (formula &&f)
	Construct a PSL Closure. More...


static formula	NegClosure (const formula &f)
	Construct a negated PSL Closure. More...

static formula	NegClosure (formula &&f)
	Construct a negated PSL Closure. More...


static formula	NegClosureMarked (const formula &f)
	Construct a marked negated PSL Closure. More...

static formula	NegClosureMarked (formula &&f)
	Construct a marked negated PSL Closure. More...


static formula	first_match (const formula &f)
	Construct first_match(sere) More...

static formula	first_match (formula &&f)
	Construct first_match(sere) More...


static formula	binop (op o, const formula &f, const formula &g)
	Construct a binary operator. More...

static formula	binop (op o, const formula &f, formula &&g)
	Construct a binary operator. More...

static formula	binop (op o, formula &&f, const formula &g)
	Construct a binary operator. More...

static formula	binop (op o, formula &&f, formula &&g)
	Construct a binary operator. More...


static formula	Xor (const formula &f, const formula &g)
	Construct an `Xor` formula. More...

static formula	Xor (const formula &f, formula &&g)
	Construct an `Xor` formula. More...

static formula	Xor (formula &&f, const formula &g)
	Construct an `Xor` formula. More...

static formula	Xor (formula &&f, formula &&g)
	Construct an `Xor` formula. More...


static formula	Implies (const formula &f, const formula &g)
	Construct an `->` formula. More...

static formula	Implies (const formula &f, formula &&g)
	Construct an `->` formula. More...

static formula	Implies (formula &&f, const formula &g)
	Construct an `->` formula. More...

static formula	Implies (formula &&f, formula &&g)
	Construct an `->` formula. More...


static formula	Equiv (const formula &f, const formula &g)
	Construct an `<->` formula. More...

static formula	Equiv (const formula &f, formula &&g)
	Construct an `<->` formula. More...

static formula	Equiv (formula &&f, const formula &g)
	Construct an `<->` formula. More...

static formula	Equiv (formula &&f, formula &&g)
	Construct an `<->` formula. More...


static formula	U (const formula &f, const formula &g)
	Construct a `U` formula. More...

static formula	U (const formula &f, formula &&g)
	Construct a `U` formula. More...

static formula	U (formula &&f, const formula &g)
	Construct a `U` formula. More...

static formula	U (formula &&f, formula &&g)
	Construct a `U` formula. More...


static formula	R (const formula &f, const formula &g)
	Construct an `R` formula. More...

static formula	R (const formula &f, formula &&g)
	Construct an `R` formula. More...

static formula	R (formula &&f, const formula &g)
	Construct an `R` formula. More...

static formula	R (formula &&f, formula &&g)
	Construct an `R` formula. More...


static formula	W (const formula &f, const formula &g)
	Construct a `W` formula. More...

static formula	W (const formula &f, formula &&g)
	Construct a `W` formula. More...

static formula	W (formula &&f, const formula &g)
	Construct a `W` formula. More...

static formula	W (formula &&f, formula &&g)
	Construct a `W` formula. More...


static formula	M (const formula &f, const formula &g)
	Construct an `M` formula. More...

static formula	M (const formula &f, formula &&g)
	Construct an `M` formula. More...

static formula	M (formula &&f, const formula &g)
	Construct an `M` formula. More...

static formula	M (formula &&f, formula &&g)
	Construct an `M` formula. More...


static formula	EConcat (const formula &f, const formula &g)
	Construct a `<>->` PSL formula. More...

static formula	EConcat (const formula &f, formula &&g)
	Construct a `<>->` PSL formula. More...

static formula	EConcat (formula &&f, const formula &g)
	Construct a `<>->` PSL formula. More...

static formula	EConcat (formula &&f, formula &&g)
	Construct a `<>->` PSL formula. More...


static formula	EConcatMarked (const formula &f, const formula &g)
	Construct a marked `<>->` PSL formula. More...

static formula	EConcatMarked (const formula &f, formula &&g)
	Construct a marked `<>->` PSL formula. More...

static formula	EConcatMarked (formula &&f, const formula &g)
	Construct a marked `<>->` PSL formula. More...

static formula	EConcatMarked (formula &&f, formula &&g)
	Construct a marked `<>->` PSL formula. More...


static formula	UConcat (const formula &f, const formula &g)
	Construct a `[]->` PSL formula. More...

static formula	UConcat (const formula &f, formula &&g)
	Construct a `[]->` PSL formula. More...

static formula	UConcat (formula &&f, const formula &g)
	Construct a `[]->` PSL formula. More...

static formula	UConcat (formula &&f, formula &&g)
	Construct a `[]->` PSL formula. More...


static formula	multop (op o, const std::vector< formula > &l)
	Construct an n-ary operator. More...

static formula	multop (op o, std::vector< formula > &&l)
	Construct an n-ary operator. More...


static formula	Or (const std::vector< formula > &l)
	Construct an Or formula. More...

static formula	Or (std::vector< formula > &&l)
	Construct an Or formula. More...


static formula	OrRat (const std::vector< formula > &l)
	Construct an Or SERE. More...

static formula	OrRat (std::vector< formula > &&l)
	Construct an Or SERE. More...


static formula	And (const std::vector< formula > &l)
	Construct an And formula. More...

static formula	And (std::vector< formula > &&l)
	Construct an And formula. More...


static formula	AndRat (const std::vector< formula > &l)
	Construct an And SERE. More...

static formula	AndRat (std::vector< formula > &&l)
	Construct an And SERE. More...


static formula	AndNLM (const std::vector< formula > &l)
	Construct a non-length-matching And SERE. More...

static formula	AndNLM (std::vector< formula > &&l)
	Construct a non-length-matching And SERE. More...


static formula	Concat (const std::vector< formula > &l)
	Construct a Concatenation SERE. More...

static formula	Concat (std::vector< formula > &&l)
	Construct a Concatenation SERE. More...


static formula	Fusion (const std::vector< formula > &l)
	Construct a Fusion SERE. More...

static formula	Fusion (std::vector< formula > &&l)
	Construct a Fusion SERE. More...


static formula	bunop (op o, const formula &f, unsigned min=0U, unsigned max=unbounded())
	Define a bounded unary-operator (i.e. star-like) More...

static formula	bunop (op o, formula &&f, unsigned min=0U, unsigned max=unbounded())
	Define a bounded unary-operator (i.e. star-like) More...


static formula	Star (const formula &f, unsigned min=0U, unsigned max=unbounded())
	Create SERE for `f[*min..max]` More...

static formula	Star (formula &&f, unsigned min=0U, unsigned max=unbounded())
	Create SERE for `f[*min..max]` More...


static formula	FStar (const formula &f, unsigned min=0U, unsigned max=unbounded())
	Create SERE for `f[:*min..max]` More...

static formula	FStar (formula &&f, unsigned min=0U, unsigned max=unbounded())
	Create SERE for `f[:*min..max]` More...


static formula	sugar_delay (const formula &a, const formula &b, unsigned min, unsigned max)
	Create the SERE `a ##[n:m] b` More...

static formula	sugar_delay (const formula &b, unsigned min, unsigned max)
	Create the SERE `a ##[n:m] b` More...

Friends
struct	formula_ptr_less_than_bool_first

Detailed Description

Main class for temporal logic formula.

Constructor & Destructor Documentation

◆ formula() [1/5]

spot::formula::formula ( const fnode * f )

inlineexplicitnoexcept

Create a formula from an fnode.

This constructor is mainly for internal use, as spot::fnode object should usually not be manipulated from user code.

◆ formula() [2/5]

spot::formula::formula ( std::nullptr_t )

inlinenoexcept

Create a null formula.

This could be used to default-initialize a formula, however null formula should be short lived: most algorithms and member functions assume that formulas should not be null.

◆ formula() [3/5]

spot::formula::formula ( )

inlinenoexcept

Default initialize a formula to nullptr.

◆ formula() [4/5]

spot::formula::formula ( const formula & f )

inlinenoexcept

Clone a formula.

◆ formula() [5/5]

spot::formula::formula ( formula && f )

inlinenoexcept

Move-construct a formula.

◆ ~formula()

spot::formula::~formula ( )

inline

Destroy a formula.

Member Function Documentation

◆ accepts_eword()

bool spot::formula::accepts_eword ( ) const

inline

Whether the formula accepts [*0].

◆ all_but()

formula spot::formula::all_but ( unsigned i ) const

inline

clone this formula, omitting child i

Precondition: The current node should be an n-ary operator such as op::And, op::AndRat, op::AndNLM, op::Or, op::OrRat, op::Concat, or op::Fusion.

◆ And() [1/2]

static formula spot::formula::And ( const std::vector< formula > & l )

inlinestatic

Construct an And formula.

◆ And() [2/2]

static formula spot::formula::And ( std::vector< formula > && l )

inlinestatic

Construct an And formula.

◆ AndNLM() [1/2]

static formula spot::formula::AndNLM ( const std::vector< formula > & l )

inlinestatic

Construct a non-length-matching And SERE.

◆ AndNLM() [2/2]

static formula spot::formula::AndNLM ( std::vector< formula > && l )

inlinestatic

Construct a non-length-matching And SERE.

◆ AndRat() [1/2]

static formula spot::formula::AndRat ( const std::vector< formula > & l )

inlinestatic

Construct an And SERE.

◆ AndRat() [2/2]

static formula spot::formula::AndRat ( std::vector< formula > && l )

inlinestatic

Construct an And SERE.

◆ ap() [1/2]

static formula spot::formula::ap ( const formula & a )

inlinestatic

Build an atomic proposition from... an atomic proposition.

The only practical interest of this methods is for the Python bindings, where ap() can therefore work both from string or atomic propositions.

References spot::ap, and kind().

◆ ap() [2/2]

static formula spot::formula::ap ( const std::string & name )

inlinestatic

Build an atomic proposition.

References spot::fnode::ap().

Referenced by spot::twa::register_ap().

◆ ap_name()

const std::string & spot::formula::ap_name ( ) const

inline

Print the name of an atomic proposition.

Precondition: the formula should be of kind op::ap.

◆ begin()

formula_child_iterator spot::formula::begin ( ) const

inline

Allow iterating over children.

◆ binop() [1/4]

static formula spot::formula::binop	(	op	o,
		const formula &	f,
		const formula &	g
	)

inlinestatic

Construct a binary operator.

Precondition: o should be one of op::Xor, op::Implies, op::Equiv, op::U, op::R, op::W, op::M, op::EConcat, op::EConcatMarked, or op::UConcat.

References spot::fnode::binop(), and spot::fnode::clone().

◆ binop() [2/4]

static formula spot::formula::binop	(	op	o,
		const formula &	f,
		formula &&	g
	)

inlinestatic

Construct a binary operator.

Precondition: o should be one of op::Xor, op::Implies, op::Equiv, op::U, op::R, op::W, op::M, op::EConcat, op::EConcatMarked, or op::UConcat.

References spot::fnode::binop(), and spot::fnode::clone().

◆ binop() [3/4]

static formula spot::formula::binop	(	op	o,
		formula &&	f,
		const formula &	g
	)

inlinestatic

Construct a binary operator.

Precondition: o should be one of op::Xor, op::Implies, op::Equiv, op::U, op::R, op::W, op::M, op::EConcat, op::EConcatMarked, or op::UConcat.

References spot::fnode::binop(), spot::fnode::clone(), and to_node_().

◆ binop() [4/4]

static formula spot::formula::binop	(	op	o,
		formula &&	f,
		formula &&	g
	)

inlinestatic

Construct a binary operator.

Precondition: o should be one of op::Xor, op::Implies, op::Equiv, op::U, op::R, op::W, op::M, op::EConcat, op::EConcatMarked, or op::UConcat.

References spot::fnode::binop(), and to_node_().

◆ boolean_count()

unsigned spot::formula::boolean_count ( ) const

inline

number of Boolean children

Precondition: The current node should be an n-ary operator such as op::And, op::AndRat, op::AndNLM, op::Or, or op::OrRat.

Note that the children of an n-ary operator are always sorted when the node is constructed, and such that Boolean children appear at the beginning. This function therefore return the number of the first non-Boolean child if it exists.

◆ boolean_operands()

formula spot::formula::boolean_operands ( unsigned * width = nullptr ) const

inline

return a clone of the current node, restricted to its Boolean children

Precondition: The current node should be an n-ary operator such as op::And, op::AndRat, op::AndNLM, op::Or, or op::OrRat.

On a formula such as And({a,b,c,d,F(e),G(f)}), this returns And({a,b,c,d}). If width is not nullptr, it is set the the number of Boolean children gathered. Note that the children of an n-ary operator are always sorted when the node is constructed, and such that Boolean children appear at the beginning. width would therefore give the number of the first non-Boolean child if it exists.

◆ bunop() [1/2]

static formula spot::formula::bunop	(	op	o,
		const formula &	f,
		unsigned	min = `0U`,
		unsigned	max = `unbounded()`
	)

inlinestatic

Define a bounded unary-operator (i.e. star-like)

Precondition: o should be op::Star or op::FStar.

References spot::fnode::bunop(), and spot::fnode::clone().

◆ bunop() [2/2]

static formula spot::formula::bunop	(	op	o,
		formula &&	f,
		unsigned	min = `0U`,
		unsigned	max = `unbounded()`
	)

inlinestatic

Define a bounded unary-operator (i.e. star-like)

Precondition: o should be op::Star or op::FStar.

References spot::fnode::bunop(), and to_node_().

◆ Closure() [1/2]

static formula spot::formula::Closure ( const formula & f )

inlinestatic

Construct a PSL Closure.

◆ Closure() [2/2]

static formula spot::formula::Closure ( formula && f )

inlinestatic

Construct a PSL Closure.

◆ Concat() [1/2]

static formula spot::formula::Concat ( const std::vector< formula > & l )

inlinestatic

Construct a Concatenation SERE.

◆ Concat() [2/2]

static formula spot::formula::Concat ( std::vector< formula > && l )

inlinestatic

Construct a Concatenation SERE.

◆ dump()

std::ostream & spot::formula::dump ( std::ostream & os ) const

inline

Print the formula for debugging.

In addition to the operator and children, this also display the formula's unique id, and its reference count.

◆ EConcat() [1/4]

static formula spot::formula::EConcat	(	const formula &	f,
		const formula &	g
	)

inlinestatic

Construct a <>-> PSL formula.

◆ EConcat() [2/4]

static formula spot::formula::EConcat	(	const formula &	f,
		formula &&	g
	)

inlinestatic

Construct a <>-> PSL formula.

◆ EConcat() [3/4]

static formula spot::formula::EConcat	(	formula &&	f,
		const formula &	g
	)

inlinestatic

Construct a <>-> PSL formula.

◆ EConcat() [4/4]

static formula spot::formula::EConcat	(	formula &&	f,
		formula &&	g
	)

inlinestatic

Construct a <>-> PSL formula.

◆ EConcatMarked() [1/4]

static formula spot::formula::EConcatMarked	(	const formula &	f,
		const formula &	g
	)

inlinestatic

Construct a marked <>-> PSL formula.

◆ EConcatMarked() [2/4]

static formula spot::formula::EConcatMarked	(	const formula &	f,
		formula &&	g
	)

inlinestatic

Construct a marked <>-> PSL formula.

◆ EConcatMarked() [3/4]

static formula spot::formula::EConcatMarked	(	formula &&	f,
		const formula &	g
	)

inlinestatic

Construct a marked <>-> PSL formula.

◆ EConcatMarked() [4/4]

static formula spot::formula::EConcatMarked	(	formula &&	f,
		formula &&	g
	)

inlinestatic

Construct a marked <>-> PSL formula.

◆ end()

formula_child_iterator spot::formula::end ( ) const

inline

Allow iterating over children.

◆ Equiv() [1/4]

static formula spot::formula::Equiv	(	const formula &	f,
		const formula &	g
	)

inlinestatic

Construct an <-> formula.

◆ Equiv() [2/4]

static formula spot::formula::Equiv	(	const formula &	f,
		formula &&	g
	)

inlinestatic

Construct an <-> formula.

◆ Equiv() [3/4]

static formula spot::formula::Equiv	(	formula &&	f,
		const formula &	g
	)

inlinestatic

Construct an <-> formula.

◆ Equiv() [4/4]

static formula spot::formula::Equiv	(	formula &&	f,
		formula &&	g
	)

inlinestatic

Construct an <-> formula.

◆ eword()

static formula spot::formula::eword ( )

inlinestatic

Return the empty word constant.

References spot::fnode::eword().

◆ F() [1/3]

static formula spot::formula::F ( const formula & f )

inlinestatic

Construct an F.

◆ F() [2/3]

static formula spot::formula::F ( formula && f )

inlinestatic

Construct an F.

◆ F() [3/3]

static formula spot::formula::F	(	unsigned	min_level,
		unsigned	max_level,
		const formula &	f
	)

inlinestatic

Construct F[n:m].

F[2:3]a = XX(a | Xa) F[2:$]a = XXFa

This syntax is from TSLF; the operator is called next_e![n..m] in PSL.

References spot::Or, and spot::X.

◆ ff()

static formula spot::formula::ff ( )

inlinestatic

Return the false constant.

References spot::fnode::ff().

◆ first_match() [1/2]

static formula spot::formula::first_match ( const formula & f )

inlinestatic

Construct first_match(sere)

◆ first_match() [2/2]

static formula spot::formula::first_match ( formula && f )

inlinestatic

Construct first_match(sere)

◆ FStar() [1/2]

static formula spot::formula::FStar	(	const formula &	f,
		unsigned	min = `0U`,
		unsigned	max = `unbounded()`
	)

inlinestatic

Create SERE for f[:*min..max]

This operator is a generalization of the (+) operator defined by Dax et al. [16]

◆ FStar() [2/2]

static formula spot::formula::FStar	(	formula &&	f,
		unsigned	min = `0U`,
		unsigned	max = `unbounded()`
	)

inlinestatic

Create SERE for f[:*min..max]

This operator is a generalization of the (+) operator defined by Dax et al. [16]

◆ Fusion() [1/2]

static formula spot::formula::Fusion ( const std::vector< formula > & l )

inlinestatic

Construct a Fusion SERE.

◆ Fusion() [2/2]

static formula spot::formula::Fusion ( std::vector< formula > && l )

inlinestatic

Construct a Fusion SERE.

◆ G() [1/3]

static formula spot::formula::G ( const formula & f )

inlinestatic

Construct a G.

◆ G() [2/3]

static formula spot::formula::G ( formula && f )

inlinestatic

Construct a G.

◆ G() [3/3]

static formula spot::formula::G	(	unsigned	min_level,
		unsigned	max_level,
		const formula &	f
	)

inlinestatic

Construct G[n:m].

G[2:3]a = XX(a & Xa) G[2:$]a = XXGa

This syntax is from TSLF; the operator is called next_a![n..m] in PSL.

References spot::And, and spot::X.

◆ get_child_of() [1/2]

formula spot::formula::get_child_of ( op o ) const

inline

Remove operator o and return the child.

This works only for unary operators.

References get_child_of().

Referenced by get_child_of().

◆ get_child_of() [2/2]

formula spot::formula::get_child_of ( std::initializer_list< op > l ) const

inline

Remove all operators in l and return the child.

This works only for a list of unary operators. For instance if f is a formula for XG(a U b), then f.get_child_of({op::X, op::G}) will return the subformula a U b.

References get_child_of().

◆ has_lbt_atomic_props()

bool spot::formula::has_lbt_atomic_props ( ) const

inline

Whether the formula has only LBT-compatible atomic propositions.

LBT only supports atomic propositions of the form p1, p12, etc.

◆ has_spin_atomic_props()

bool spot::formula::has_spin_atomic_props ( ) const

inline

Whether the formula has spin-compatible atomic propositions.

In Spin 5 (and hence ltl2ba, ltl3ba, ltl3dra), atomic propositions should start with a lowercase letter, and can then consist solely of alphanumeric characters and underscores.

See also: spot::is_spin_ap()

◆ id()

size_t spot::formula::id ( ) const

inline

Return the id of a formula.

Can be used as a hash number.

The id is almost unique as it is an unsigned number incremented for each formula construction, and the number may wrap around zero. If this is used for ordering, make sure to deal with equality

◆ Implies() [1/4]

static formula spot::formula::Implies	(	const formula &	f,
		const formula &	g
	)

inlinestatic

Construct an -> formula.

◆ Implies() [2/4]

static formula spot::formula::Implies	(	const formula &	f,
		formula &&	g
	)

inlinestatic

Construct an -> formula.

◆ Implies() [3/4]

static formula spot::formula::Implies	(	formula &&	f,
		const formula &	g
	)

inlinestatic

Construct an -> formula.

◆ Implies() [4/4]

static formula spot::formula::Implies	(	formula &&	f,
		formula &&	g
	)

inlinestatic

Construct an -> formula.

◆ is() [1/5]

bool spot::formula::is ( op o ) const

inline

Return true if the formula is of kind o.

◆ is() [2/5]

bool spot::formula::is	(	op	o1,
		op	o2
	)		const

inline

Return true if the formula is of kind o1 or o2.

◆ is() [3/5]

bool spot::formula::is	(	op	o1,
		op	o2,
		op	o3
	)		const

inline

Return true if the formula is of kind o1 or o2 or o3.

◆ is() [4/5]

bool spot::formula::is	(	op	o1,
		op	o2,
		op	o3,
		op	o4
	)		const

inline

Return true if the formula is of kind o1 or o2 or o3 or a4.

◆ is() [5/5]

bool spot::formula::is ( std::initializer_list< op > l ) const

inline

Return true if the formulas nests all the operators in l.

◆ is_boolean()

bool spot::formula::is_boolean ( ) const

inline

Whether the formula use only boolean operators.

◆ is_constant()

bool spot::formula::is_constant ( ) const

inline

Whether the formula is op::ff, op::tt, or op::eword.

◆ is_delta1()

bool spot::formula::is_delta1 ( ) const

inline

Whether a PSL/LTL formula is in the Δ₁ syntactic frament.

A formula is in Δ₁ if it is a boolean combination of syntactic safety and syntactic guarantee properties.

◆ is_delta2()

bool spot::formula::is_delta2 ( ) const

inline

Whether a PSL/LTL formula is in the Δ₂ syntactic frament.

A formula is in Δ₂ if it is a boolean combination of Σ₂ and Π₂ properties.

◆ is_eventual()

bool spot::formula::is_eventual ( ) const

inline

Whether the formula is purely eventual.

Pure eventuality formulae are defined in

A word that satisfies a pure eventuality can be prefixed by anything and still satisfies the formula. [22]

◆ is_eword()

bool spot::formula::is_eword ( ) const

inline

Whether the formula is the empty word constant.

◆ is_ff()

bool spot::formula::is_ff ( ) const

inline

Whether the formula is the false constant.

◆ is_finite()

bool spot::formula::is_finite ( ) const

inline

Whether a SERE describes a finite language, or an LTL formula uses no temporal operator but X.

◆ is_in_nenoform()

bool spot::formula::is_in_nenoform ( ) const

inline

Whether the formula is in negative normal form.

A formula is in negative normal form if the not operators occur only in front of atomic propositions.

◆ is_Kleene_star()

bool spot::formula::is_Kleene_star ( ) const

inline

Test whether the formula represent a Kleene star.

That is, it should be of kind op::Star, with min=0 and max=unbounded().

◆ is_leaf()

bool spot::formula::is_leaf ( ) const

inline

Whether the formula is a leaf.

Leaves are formulas without children. They are either constants (true, false, empty word) or atomic propositions.

◆ is_literal()

bool spot::formula::is_literal ( ) const

inline

Whether the formula is an atomic proposition or its negation.

References spot::ap, and spot::Not.

◆ is_ltl_formula()

bool spot::formula::is_ltl_formula ( ) const

inline

Whether the formula uses only LTL operators.

◆ is_marked()

bool spot::formula::is_marked ( ) const

inline

Whether the formula has an occurrence of EConcatMarked or NegClosureMarked.

◆ is_pi2()

bool spot::formula::is_pi2 ( ) const

inline

Whether a PSL/LTL formula is in Π₂

◆ is_psl_formula()

bool spot::formula::is_psl_formula ( ) const

inline

Whether the formula uses only PSL operators.

◆ is_sere_formula()

bool spot::formula::is_sere_formula ( ) const

inline

Whether the formula uses only SERE operators.

◆ is_sigma2()

bool spot::formula::is_sigma2 ( ) const

inline

Whether a PSL/LTL formula is in Σ₂

◆ is_sugar_free_boolean()

bool spot::formula::is_sugar_free_boolean ( ) const

inline

Whether the formula use only AND, OR, and NOT operators.

◆ is_sugar_free_ltl()

bool spot::formula::is_sugar_free_ltl ( ) const

inline

Whether the formula avoids the F and G operators.

◆ is_syntactic_guarantee()

bool spot::formula::is_syntactic_guarantee ( ) const

inline

Whether a PSL/LTL formula is syntactic guarantee property.

Is class is also called Σ₁.

◆ is_syntactic_obligation()

bool spot::formula::is_syntactic_obligation ( ) const

inline

Whether a PSL/LTL formula is syntactic obligation property.

This class is a proper syntactic superset of Δ₁, but has the same expressive power.

◆ is_syntactic_persistence()

bool spot::formula::is_syntactic_persistence ( ) const

inline

Whether a PSL/LTL formula is syntactic persistence property.

This class is a proper syntactic superset of Π₂, but has the same expressive power.

◆ is_syntactic_recurrence()

bool spot::formula::is_syntactic_recurrence ( ) const

inline

Whether a PSL/LTL formula is syntactic recurrence property.

This class is a proper syntactic superset of Σ₂ syntactically, expressive power.

◆ is_syntactic_safety()

bool spot::formula::is_syntactic_safety ( ) const

inline

Whether a PSL/LTL formula is syntactic safety property.

Is class is also called Π₁.

◆ is_syntactic_stutter_invariant()

bool spot::formula::is_syntactic_stutter_invariant ( ) const

inline

Whether the formula is syntactically stutter_invariant.

◆ is_tt()

bool spot::formula::is_tt ( ) const

inline

Whether the formula is the true constant.

◆ is_universal()

bool spot::formula::is_universal ( ) const

inline

Whether a formula is purely universal.

Purely universal formulae are defined in

Any (non-empty) suffix of a word that satisfies a purely universal formula also satisfies the formula. [22]

◆ kind()

op spot::formula::kind ( ) const

inline

Return top-most operator.

Referenced by ap().

◆ kindstr()

std::string spot::formula::kindstr ( ) const

inline

Return the name of the top-most operator.

◆ M() [1/4]

static formula spot::formula::M	(	const formula &	f,
		const formula &	g
	)

inlinestatic

Construct an M formula.

◆ M() [2/4]

static formula spot::formula::M	(	const formula &	f,
		formula &&	g
	)

inlinestatic

Construct an M formula.

◆ M() [3/4]

static formula spot::formula::M	(	formula &&	f,
		const formula &	g
	)

inlinestatic

Construct an M formula.

◆ M() [4/4]

static formula spot::formula::M	(	formula &&	f,
		formula &&	g
	)

inlinestatic

Construct an M formula.

◆ map()

template<typename Trans , typename... Args>

formula spot::formula::map	(	Trans	trans,
		Args &&...	args
	)

inline

Clone this node after applying trans to its children.

Any additional argument is passed to trans.

References spot::And, spot::AndNLM, spot::AndRat, spot::ap, spot::Closure, spot::Concat, spot::EConcat, spot::EConcatMarked, spot::Equiv, spot::eword, spot::F, spot::ff, spot::first_match, spot::FStar, spot::Fusion, spot::G, spot::Implies, spot::M, spot::NegClosure, spot::NegClosureMarked, spot::Not, spot::Or, spot::OrRat, spot::R, spot::Star, spot::tt, spot::U, spot::UConcat, spot::W, spot::X, and spot::Xor.

◆ max()

unsigned spot::formula::max ( ) const

inline

Return end of the range for star-like operators.

Precondition: The formula should have kind op::Star or op::FStar.

◆ min()

unsigned spot::formula::min ( ) const

inline

Return start of the range for star-like operators.

Precondition: The formula should have kind op::Star or op::FStar.

◆ multop() [1/2]

static formula spot::formula::multop	(	op	o,
		const std::vector< formula > &	l
	)

inlinestatic

Construct an n-ary operator.

Precondition: o should be one of op::Or, op::OrRat, op::And, op::AndRat, op::AndNLM, op::Concat, op::Fusion.

References spot::fnode::clone(), and spot::fnode::multop().

◆ multop() [2/2]

static formula spot::formula::multop	(	op	o,
		std::vector< formula > &&	l
	)

inlinestatic

Construct an n-ary operator.

Precondition: o should be one of op::Or, op::OrRat, op::And, op::AndRat, op::AndNLM, op::Concat, op::Fusion.

References spot::fnode::multop(), and to_node_().

◆ NegClosure() [1/2]

static formula spot::formula::NegClosure ( const formula & f )

inlinestatic

Construct a negated PSL Closure.

◆ NegClosure() [2/2]

static formula spot::formula::NegClosure ( formula && f )

inlinestatic

Construct a negated PSL Closure.

◆ NegClosureMarked() [1/2]

static formula spot::formula::NegClosureMarked ( const formula & f )

inlinestatic

Construct a marked negated PSL Closure.

◆ NegClosureMarked() [2/2]

static formula spot::formula::NegClosureMarked ( formula && f )

inlinestatic

Construct a marked negated PSL Closure.

◆ nested_unop_range()

static const formula spot::formula::nested_unop_range	(	op	uo,
		op	bo,
		unsigned	min,
		unsigned	max,
		formula	f
	)

inlinestatic

Nested operator construction (syntactic sugar).

Build between min and max nested uo, and chose between the different numbers with bo.

For instance nested_unup_range(op::X, op::Or, 2, 4, a) returns XX(a | X(a | Xa)).

For max==unbounded(), uo is repeated min times, and its child is set to F(a) if bo is op::Or or to G(a) otherwise.

References spot::fnode::clone(), and spot::fnode::nested_unop_range().

◆ Not() [1/2]

static formula spot::formula::Not ( const formula & f )

inlinestatic

Construct a negation.

◆ Not() [2/2]

static formula spot::formula::Not ( formula && f )

inlinestatic

Construct a negation.

◆ one_plus()

static formula spot::formula::one_plus ( )

inlinestatic

Return a copy of the formula 1[+].

References spot::fnode::one_plus().

◆ one_star()

static formula spot::formula::one_star ( )

inlinestatic

Return a copy of the formula 1[*].

References spot::fnode::one_star().

◆ operator=()

const formula & spot::formula::operator= ( std::nullptr_t )

inline

Reset a formula to null.

Note that null formula should be short lived: most algorithms and member function assume that formulas should not be null. Assigning nullptr to a formula can be useful when cleaning an array of formula using multiple passes and marking some formula as nullptr before actually erasing them.

◆ operator[]()

formula spot::formula::operator[] ( unsigned i ) const

inline

Return children number i.

◆ Or() [1/2]

static formula spot::formula::Or ( const std::vector< formula > & l )

inlinestatic

Construct an Or formula.

◆ Or() [2/2]

static formula spot::formula::Or ( std::vector< formula > && l )

inlinestatic

Construct an Or formula.

◆ OrRat() [1/2]

static formula spot::formula::OrRat ( const std::vector< formula > & l )

inlinestatic

Construct an Or SERE.

◆ OrRat() [2/2]

static formula spot::formula::OrRat ( std::vector< formula > && l )

inlinestatic

Construct an Or SERE.

◆ R() [1/4]

static formula spot::formula::R	(	const formula &	f,
		const formula &	g
	)

inlinestatic

Construct an R formula.

◆ R() [2/4]

static formula spot::formula::R	(	const formula &	f,
		formula &&	g
	)

inlinestatic

Construct an R formula.

◆ R() [3/4]

static formula spot::formula::R	(	formula &&	f,
		const formula &	g
	)

inlinestatic

Construct an R formula.

◆ R() [4/4]

static formula spot::formula::R	(	formula &&	f,
		formula &&	g
	)

inlinestatic

Construct an R formula.

◆ size()

unsigned spot::formula::size ( ) const

inline

Return the number of children.

◆ Star() [1/2]

static formula spot::formula::Star	(	const formula &	f,
		unsigned	min = `0U`,
		unsigned	max = `unbounded()`
	)

inlinestatic

Create SERE for f[*min..max]

◆ Star() [2/2]

static formula spot::formula::Star	(	formula &&	f,
		unsigned	min = `0U`,
		unsigned	max = `unbounded()`
	)

inlinestatic

Create SERE for f[*min..max]

◆ sugar_delay() [1/2]

static formula spot::formula::sugar_delay	(	const formula &	a,
		const formula &	b,
		unsigned	min,
		unsigned	max
	)

static

Create the SERE a ##[n:m] b

This ##[n:m] operator comes from SVA. When n=m, it is simply written ##n.

The operator does not exist in Spot it is handled as syntactic sugar by the parser. This function is used by the parser to create the equivalent SERE using PSL operators.

The rewriting rules depends on the values of a, n, and b. If n≥1 a ##[n:m] b is encoded as a;1[*n-1,m-1];b. Otherwise:

a ##[0:0] b is encoded as a:b,
For m>0, a ##[0:m] b is encoded as
- a:(1[*0:m];b) is a rejects [*0],
- (a;1[*0:m]):b is b rejects [*0],
- (a:b) | (a;1[*0:m-1];b) is a and b accept [*0].

The left operand can also be missing, in which case ##[n:m] b is rewritten as 1[*n:m];b.

◆ sugar_delay() [2/2]

static formula spot::formula::sugar_delay	(	const formula &	b,
		unsigned	min,
		unsigned	max
	)

static

Create the SERE a ##[n:m] b

This ##[n:m] operator comes from SVA. When n=m, it is simply written ##n.

The operator does not exist in Spot it is handled as syntactic sugar by the parser. This function is used by the parser to create the equivalent SERE using PSL operators.

The rewriting rules depends on the values of a, n, and b. If n≥1 a ##[n:m] b is encoded as a;1[*n-1,m-1];b. Otherwise:

a ##[0:0] b is encoded as a:b,
For m>0, a ##[0:m] b is encoded as
- a:(1[*0:m];b) is a rejects [*0],
- (a;1[*0:m]):b is b rejects [*0],
- (a:b) | (a;1[*0:m-1];b) is a and b accept [*0].

The left operand can also be missing, in which case ##[n:m] b is rewritten as 1[*n:m];b.

◆ sugar_equal()

static formula spot::formula::sugar_equal	(	const formula &	b,
		unsigned	min,
		unsigned	max
	)

static

Create the SERE b[=min..max]

The operator does not exist: it is handled as syntactic sugar by the parser and the printer. This function is used by the parser to create the equivalent SERE.

◆ sugar_goto()

static formula spot::formula::sugar_goto	(	const formula &	b,
		unsigned	min,
		unsigned	max
	)

static

Create a SERE equivalent to b[->min..max]

The operator does not exist: it is handled as syntactic sugar by the parser and the printer. This function is used by the parser to create the equivalent SERE.

◆ to_node_()

const fnode * spot::formula::to_node_ ( )

inline

Return the underlying pointer to the formula.

It is not recommended to call this function, which is mostly meant for internal use.

By calling this function you take ownership of the fnode instance pointed by this formula instance, and should take care of calling its destroy() methods once you are done with it. Otherwise the fnode will be leaked.

Referenced by binop(), bunop(), multop(), and unop().

◆ traverse()

template<typename Func , typename... Args>

void spot::formula::traverse	(	Func	func,
		Args &&...	args
	)

inline

Apply func to each subformula.

This does a simple DFS without checking for duplicate subformulas. If func returns true, the children of the current node are skipped.

Any additional argument is passed to func when it is invoked.

References traverse().

Referenced by traverse().

◆ tt()

static formula spot::formula::tt ( )

inlinestatic

Return the true constant.

References spot::fnode::tt().

◆ U() [1/4]

static formula spot::formula::U	(	const formula &	f,
		const formula &	g
	)

inlinestatic

Construct a U formula.

◆ U() [2/4]

static formula spot::formula::U	(	const formula &	f,
		formula &&	g
	)

inlinestatic

Construct a U formula.

◆ U() [3/4]

static formula spot::formula::U	(	formula &&	f,
		const formula &	g
	)

inlinestatic

Construct a U formula.

◆ U() [4/4]

static formula spot::formula::U	(	formula &&	f,
		formula &&	g
	)

inlinestatic

Construct a U formula.

◆ UConcat() [1/4]

static formula spot::formula::UConcat	(	const formula &	f,
		const formula &	g
	)

inlinestatic

Construct a []-> PSL formula.

◆ UConcat() [2/4]

static formula spot::formula::UConcat	(	const formula &	f,
		formula &&	g
	)

inlinestatic

Construct a []-> PSL formula.

◆ UConcat() [3/4]

static formula spot::formula::UConcat	(	formula &&	f,
		const formula &	g
	)

inlinestatic

Construct a []-> PSL formula.

◆ UConcat() [4/4]

static formula spot::formula::UConcat	(	formula &&	f,
		formula &&	g
	)

inlinestatic

Construct a []-> PSL formula.

◆ unbounded()

static constexpr uint8_t spot::formula::unbounded ( )

inlinestaticconstexpr

Unbounded constant to use as end of range for bounded operators.

References spot::fnode::unbounded().

◆ unop() [1/2]

static formula spot::formula::unop	(	op	o,
		const formula &	f
	)

inlinestatic

Build a unary operator.

Precondition: o should be one of op::Not, op::X, op::F, op::G, op::Closure, op::NegClosure, op::NegClosureMarked.

References spot::fnode::clone(), and spot::fnode::unop().

◆ unop() [2/2]

static formula spot::formula::unop	(	op	o,
		formula &&	f
	)

inlinestatic

Build a unary operator.

Precondition: o should be one of op::Not, op::X, op::F, op::G, op::Closure, op::NegClosure, op::NegClosureMarked.

References to_node_(), and spot::fnode::unop().

◆ W() [1/4]

static formula spot::formula::W	(	const formula &	f,
		const formula &	g
	)

inlinestatic

Construct a W formula.

◆ W() [2/4]

static formula spot::formula::W	(	const formula &	f,
		formula &&	g
	)

inlinestatic

Construct a W formula.

◆ W() [3/4]

static formula spot::formula::W	(	formula &&	f,
		const formula &	g
	)

inlinestatic

Construct a W formula.

◆ W() [4/4]

static formula spot::formula::W	(	formula &&	f,
		formula &&	g
	)

inlinestatic

Construct a W formula.

◆ X() [1/3]

static formula spot::formula::X ( const formula & f )

inlinestatic

Construct an X.

◆ X() [2/3]

static formula spot::formula::X ( formula && f )

inlinestatic

Construct an X.

◆ X() [3/3]

static formula spot::formula::X	(	unsigned	level,
		const formula &	f
	)

inlinestatic

Construct an X[n].

X[3]f = XXXf

References spot::Or, and spot::X.

◆ Xor() [1/4]

static formula spot::formula::Xor	(	const formula &	f,
		const formula &	g
	)

inlinestatic

Construct an Xor formula.

◆ Xor() [2/4]

static formula spot::formula::Xor	(	const formula &	f,
		formula &&	g
	)

inlinestatic

Construct an Xor formula.

◆ Xor() [3/4]

static formula spot::formula::Xor	(	formula &&	f,
		const formula &	g
	)

inlinestatic

Construct an Xor formula.

◆ Xor() [4/4]

static formula spot::formula::Xor	(	formula &&	f,
		formula &&	g
	)

inlinestatic

Construct an Xor formula.

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

spot/tl/formula.hh

Classes

Public Member Functions

Static Public Member Functions

Friends

Detailed Description

Constructor & Destructor Documentation

◆ formula() [1/5]

◆ formula() [2/5]

◆ formula() [3/5]

◆ formula() [4/5]

◆ formula() [5/5]

◆ ~formula()

Member Function Documentation

◆ accepts_eword()

◆ all_but()

◆ And() [1/2]

◆ And() [2/2]

◆ AndNLM() [1/2]

◆ AndNLM() [2/2]

◆ AndRat() [1/2]

◆ AndRat() [2/2]

◆ ap() [1/2]

◆ ap() [2/2]

◆ ap_name()

◆ begin()

◆ binop() [1/4]

◆ binop() [2/4]

◆ binop() [3/4]

◆ binop() [4/4]

◆ boolean_count()

◆ boolean_operands()

◆ bunop() [1/2]

◆ bunop() [2/2]

◆ Closure() [1/2]

◆ Closure() [2/2]

◆ Concat() [1/2]

◆ Concat() [2/2]

◆ dump()

◆ EConcat() [1/4]

◆ EConcat() [2/4]

◆ EConcat() [3/4]

◆ EConcat() [4/4]

◆ EConcatMarked() [1/4]

◆ EConcatMarked() [2/4]

◆ EConcatMarked() [3/4]

◆ EConcatMarked() [4/4]

◆ end()

◆ Equiv() [1/4]

◆ Equiv() [2/4]

◆ Equiv() [3/4]

◆ Equiv() [4/4]

◆ eword()

◆ F() [1/3]

◆ F() [2/3]

◆ F() [3/3]

◆ ff()

◆ first_match() [1/2]

◆ first_match() [2/2]

◆ FStar() [1/2]

◆ FStar() [2/2]

◆ Fusion() [1/2]

◆ Fusion() [2/2]

◆ G() [1/3]

◆ G() [2/3]

◆ G() [3/3]

◆ get_child_of() [1/2]

◆ get_child_of() [2/2]

◆ has_lbt_atomic_props()

◆ has_spin_atomic_props()

◆ id()

◆ Implies() [1/4]

◆ Implies() [2/4]

◆ Implies() [3/4]

◆ Implies() [4/4]

◆ is() [1/5]

◆ is() [2/5]

◆ is() [3/5]

◆ is() [4/5]

◆ is() [5/5]

◆ is_boolean()