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.
	formula (std::nullptr_t) noexcept
	Create a null formula.
	formula () noexcept
	Default initialize a formula to nullptr.
	formula (const formula &f) noexcept
	Clone a formula.
	formula (formula &&f) noexcept
	Move-construct a formula.
	~formula ()
	Destroy a formula.
const formula &	operator= (std::nullptr_t)
	Reset a formula to null.
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.
op	kind () const
	Return top-most operator.
std::string	kindstr () const
	Return the name of the top-most operator.
bool	is (op o) const
	Return true if the formula is of kind o.
bool	is (op o1, op o2) const
	Return true if the formula is of kind o1 or o2.
bool	is (op o1, op o2, op o3) const
	Return true if the formula is of kind o1 or o2 or o3.
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.
formula	get_child_of (op o) const
	Remove operator o and return the child.
formula	get_child_of (std::initializer_list< op > l) const
	Remove all operators in l and return the child.
unsigned	min () const
	Return start of the range for star-like operators.
unsigned	max () const
	Return end of the range for star-like operators.
unsigned	size () const
	Return the number of children.
bool	is_leaf () const
	Whether the formula is a leaf.
size_t	id () const
	Return the id of a formula.
formula_child_iterator	begin () const
	Allow iterating over children.
formula_child_iterator	end () const
	Allow iterating over children.
formula	operator[] (unsigned i) const
	Return children number i.
bool	is_ff () const
	Whether the formula is the false constant.
bool	is_tt () const
	Whether the formula is the true constant.
bool	is_eword () const
	Whether the formula is the empty word constant.
bool	is_constant () const
	Whether the formula is op::ff, op::tt, or op::eword.
bool	is_Kleene_star () const
	Test whether the formula represent a Kleene star.
bool	is_literal () const
	Whether the formula is an atomic proposition or its negation.
const std::string &	ap_name () const
	Print the name of an atomic proposition.
std::ostream &	dump (std::ostream &os) const
	Print the formula for debugging.
formula	all_but (unsigned i) const
	clone this formula, omitting child i
unsigned	boolean_count () const
	number of Boolean children
formula	boolean_operands (unsigned *width=nullptr) const
	return a clone of the current node, restricted to its Boolean children
bool	is_boolean () const
	Whether the formula use only boolean operators.
bool	is_sugar_free_boolean () const
	Whether the formula use only AND, OR, and NOT operators.
bool	is_in_nenoform () const
	Whether the formula is in negative normal form.
bool	is_syntactic_stutter_invariant () const
	Whether the formula is syntactically stutter_invariant.
bool	is_sugar_free_ltl () const
	Whether the formula avoids the F and G operators.
bool	is_ltl_formula () const
	Whether the formula uses only LTL operators.
bool	is_psl_formula () const
	Whether the formula uses only PSL operators.
bool	is_sere_formula () const
	Whether the formula uses only SERE operators.
bool	is_finite () const
	Whether a SERE describes a finite language, or an LTL formula uses no temporal operator but X.
bool	is_eventual () const
	Whether the formula is purely eventual.
bool	is_universal () const
	Whether a formula is purely universal.
bool	is_syntactic_safety () const
	Whether a PSL/LTL formula is syntactic safety property.
bool	is_syntactic_guarantee () const
	Whether a PSL/LTL formula is syntactic guarantee property.
bool	is_delta1 () const
	Whether a PSL/LTL formula is in the Δ₁ syntactic fragment.
bool	is_syntactic_obligation () const
	Whether a PSL/LTL formula is syntactic obligation property.
bool	is_sigma2 () const
	Whether a PSL/LTL formula is in Σ₂
bool	is_pi2 () const
	Whether a PSL/LTL formula is in Π₂
bool	is_syntactic_recurrence () const
	Whether a PSL/LTL formula is syntactic recurrence property.
bool	is_syntactic_persistence () const
	Whether a PSL/LTL formula is syntactic persistence property.
bool	is_delta2 () const
	Whether a PSL/LTL formula is in the Δ₂ syntactic fragment.
bool	is_marked () const
	Whether the formula has an occurrence of EConcatMarked or NegClosureMarked.
bool	accepts_eword () const
	Whether the formula accepts [*0].
bool	has_lbt_atomic_props () const
	Whether the formula has only LBT-compatible atomic propositions.
bool	has_spin_atomic_props () const
	Whether the formula has spin-compatible atomic propositions.
template<typename Trans, typename... Args>
formula	map (Trans trans, Args &&... args)
	Clone this node after applying trans to its children.
template<typename Func, typename... Args>
void	traverse (Func func, Args &&... args)
	Apply func to each subformula.

Static Public Member Functions
static constexpr uint8_t	unbounded ()
	Unbounded constant to use as end of range for bounded operators.
static formula	ap (const std::string &name)
	Build an atomic proposition.
static formula	ap (const formula &a)
	Build an atomic proposition from... an atomic proposition.
static formula	X (unsigned level, const formula &f)
	Construct an X[n].
static formula	strong_X (unsigned level, const formula &f)
	Construct a strong_X[n].
static formula	F (unsigned min_level, unsigned max_level, const formula &f)
	Construct F[n:m].
static formula	G (unsigned min_level, unsigned max_level, const formula &f)
	Construct G[n:m].
static const formula	nested_unop_range (op uo, op bo, unsigned min, unsigned max, formula f)
	Nested operator construction (syntactic sugar).
static formula	sugar_goto (const formula &b, unsigned min, unsigned max)
	Create a SERE equivalent to b[->min..max].
static formula	sugar_equal (const formula &b, unsigned min, unsigned max)
	Create the SERE b[=min..max].
static formula	ff ()
	Return the false constant.
static formula	tt ()
	Return the true constant.
static formula	eword ()
	Return the empty word constant.
static formula	one_star ()
	Return a copy of the formula 1[*].
static formula	one_plus ()
	Return a copy of the formula 1[+].

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

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

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

static formula	strong_X (const formula &f)
	Construct a strong_X.
static formula	strong_X (formula &&f)
	Construct a strong_X.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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.

Referenced by formula(), formula(), all_but(), ap(), ap(), binop(), binop(), binop(), binop(), boolean_operands(), bunop(), bunop(), eword(), F(), ff(), G(), get_child_of(), get_child_of(), map(), multop(), multop(), nested_unop_range(), one_plus(), one_star(), operator=(), operator[](), strong_X(), sugar_delay(), sugar_delay(), sugar_equal(), sugar_goto(), tt(), unop(), unop(), and X().

◆ 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.

References formula().

◆ formula() [5/5]

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

inlinenoexcept

Move-construct a formula.

References 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].

References accepts_eword().

Referenced by accepts_eword().

◆ 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.

References formula().

◆ And() [1/2]

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

inlinestatic

Construct an And formula.

References And().

Referenced by And().

◆ And() [2/2]

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

inlinestatic

Construct an And formula.

◆ AndNLM() [1/2]

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

inlinestatic

Construct a non-length-matching And SERE.

References AndNLM().

Referenced by AndNLM().

◆ AndNLM() [2/2]

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

inlinestatic

Construct a non-length-matching And SERE.

◆ AndRat() [1/2]

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

inlinestatic

Construct an And SERE.

References AndRat().

Referenced by AndRat().

◆ AndRat() [2/2]

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

inlinestatic

Construct an And SERE.

◆ ap() [1/2]

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 formula(), spot::ap, and kind().

◆ ap() [2/2]

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

inlinestatic

Build an atomic proposition.

References formula(), and 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]

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 formula(), spot::fnode::binop(), and spot::fnode::clone().

Referenced by map().

◆ binop() [2/4]

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 formula(), spot::fnode::binop(), and spot::fnode::clone().

◆ binop() [3/4]

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 formula(), spot::fnode::binop(), spot::fnode::clone(), and to_node_().

◆ binop() [4/4]

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 formula(), 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 to 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.

References formula().

◆ bunop() [1/2]

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 formula(), spot::fnode::bunop(), spot::fnode::clone(), max(), min(), U(), and unbounded().

Referenced by map().

◆ bunop() [2/2]

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 formula(), spot::fnode::bunop(), max(), min(), to_node_(), U(), and unbounded().

◆ Closure() [1/2]

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

inlinestatic

Construct a PSL Closure.

References Closure().

Referenced by Closure().

◆ Closure() [2/2]

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

inlinestatic

Construct a PSL Closure.

◆ Concat() [1/2]

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

inlinestatic

Construct a Concatenation SERE.

References Concat().

Referenced by Concat().

◆ Concat() [2/2]

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]

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

inlinestatic

Construct a <>-> PSL formula.

References EConcat().

Referenced by EConcat().

◆ EConcat() [2/4]

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

inlinestatic

Construct a <>-> PSL formula.

◆ EConcat() [3/4]

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

inlinestatic

Construct a <>-> PSL formula.

◆ EConcat() [4/4]

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

inlinestatic

Construct a <>-> PSL formula.

◆ EConcatMarked() [1/4]

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

inlinestatic

Construct a marked <>-> PSL formula.

References EConcatMarked().

Referenced by EConcatMarked().

◆ EConcatMarked() [2/4]

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

inlinestatic

Construct a marked <>-> PSL formula.

◆ EConcatMarked() [3/4]

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

inlinestatic

Construct a marked <>-> PSL formula.

◆ EConcatMarked() [4/4]

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]

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

inlinestatic

Construct an <-> formula.

References Equiv().

Referenced by Equiv().

◆ Equiv() [2/4]

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

inlinestatic

Construct an <-> formula.

◆ Equiv() [3/4]

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

inlinestatic

Construct an <-> formula.

◆ Equiv() [4/4]

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

inlinestatic

Construct an <-> formula.

◆ eword()

formula spot::formula::eword ( )

inlinestatic

Return the empty word constant.

References formula(), and spot::fnode::eword().

◆ F() [1/3]

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

inlinestatic

Construct an F.

References F().

Referenced by F().

◆ F() [2/3]

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

inlinestatic

Construct an F.

◆ F() [3/3]

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 formula(), nested_unop_range(), spot::Or, and spot::X.

◆ ff()

formula spot::formula::ff ( )

inlinestatic

Return the false constant.

References formula(), and spot::fnode::ff().

◆ first_match() [1/2]

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

inlinestatic

Construct first_match(sere).

References first_match().

Referenced by first_match().

◆ first_match() [2/2]

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

inlinestatic

Construct first_match(sere).

◆ FStar() [1/2]

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. [dax.09.atva]

References FStar().

Referenced by FStar().

◆ FStar() [2/2]

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. [dax.09.atva]

◆ Fusion() [1/2]

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

inlinestatic

Construct a Fusion SERE.

References Fusion().

Referenced by Fusion().

◆ Fusion() [2/2]

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

inlinestatic

Construct a Fusion SERE.

◆ G() [1/3]

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

inlinestatic

Construct a G.

References G().

◆ G() [2/3]

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

inlinestatic

Construct a G.

◆ G() [3/3]

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 formula(), spot::And, nested_unop_range(), and spot::X.

Referenced by G().

◆ 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 formula(), and get_child_of().

Referenced by get_child_of(), and 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 formula(), and 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.

References has_lbt_atomic_props().

Referenced by has_lbt_atomic_props().

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

References has_spin_atomic_props().

Referenced by has_spin_atomic_props().

◆ 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]

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

inlinestatic

Construct an -> formula.

References Implies().

Referenced by Implies().

◆ Implies() [2/4]

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

inlinestatic

Construct an -> formula.

◆ Implies() [3/4]

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

inlinestatic

Construct an -> formula.

◆ Implies() [4/4]

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.

Referenced by is_literal().

◆ 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.

References is_boolean().

Referenced by is_boolean(), and is_literal().

◆ 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 fragment.

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

References is_delta1().

Referenced by is_delta1().

◆ is_delta2()

bool spot::formula::is_delta2 ( ) const

inline

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

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

References is_delta2().

Referenced by is_delta2().

◆ 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. [etessami.00.concur]

References is_eventual().

Referenced by is_eventual().

◆ 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.

References is_finite().

Referenced by is_finite().

◆ 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.

References is_in_nenoform().

Referenced by is_in_nenoform(), and is_literal().

◆ 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, is(), is_boolean(), is_in_nenoform(), and spot::Not.

◆ is_ltl_formula()

bool spot::formula::is_ltl_formula ( ) const

inline

Whether the formula uses only LTL operators.

References is_ltl_formula().

Referenced by is_ltl_formula().

◆ is_marked()

bool spot::formula::is_marked ( ) const

inline

Whether the formula has an occurrence of EConcatMarked or NegClosureMarked.

References is_marked().

Referenced by is_marked().

◆ is_pi2()

bool spot::formula::is_pi2 ( ) const

inline

Whether a PSL/LTL formula is in Π₂

References is_pi2().

Referenced by is_pi2().

◆ is_psl_formula()

bool spot::formula::is_psl_formula ( ) const

inline

Whether the formula uses only PSL operators.

References is_psl_formula().

Referenced by is_psl_formula().

◆ is_sere_formula()

bool spot::formula::is_sere_formula ( ) const

inline

Whether the formula uses only SERE operators.

References is_sere_formula().

Referenced by is_sere_formula().

◆ is_sigma2()

bool spot::formula::is_sigma2 ( ) const

inline

Whether a PSL/LTL formula is in Σ₂

References is_sigma2().

Referenced by is_sigma2().

◆ is_sugar_free_boolean()

bool spot::formula::is_sugar_free_boolean ( ) const

inline

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

References is_sugar_free_boolean().

Referenced by is_sugar_free_boolean().

◆ is_sugar_free_ltl()

bool spot::formula::is_sugar_free_ltl ( ) const

inline

Whether the formula avoids the F and G operators.

References is_sugar_free_ltl().

Referenced by is_sugar_free_ltl().

◆ 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 Σ₁.

References is_syntactic_guarantee().

Referenced by is_syntactic_guarantee().

◆ 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.

References is_syntactic_obligation().

Referenced by is_syntactic_obligation().

◆ 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.

References is_syntactic_persistence().

Referenced by is_syntactic_persistence().

◆ 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.

References is_syntactic_recurrence().

Referenced by is_syntactic_recurrence().

◆ 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 Π₁.

References is_syntactic_safety().

Referenced by is_syntactic_safety().

◆ is_syntactic_stutter_invariant()

bool spot::formula::is_syntactic_stutter_invariant ( ) const

inline

Whether the formula is syntactically stutter_invariant.

References is_syntactic_stutter_invariant().

Referenced by is_syntactic_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. [etessami.00.concur]

References is_universal().

Referenced by is_universal().

◆ kind()

op spot::formula::kind ( ) const

inline

Return top-most operator.

Referenced by ap(), and map().

◆ kindstr()

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

inline

Return the name of the top-most operator.

◆ M() [1/4]

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

inlinestatic

Construct an M formula.

References M().

Referenced by M().

◆ M() [2/4]

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

inlinestatic

Construct an M formula.

◆ M() [3/4]

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

inlinestatic

Construct an M formula.

◆ M() [4/4]

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 formula(), spot::And, spot::AndNLM, spot::AndRat, spot::ap, binop(), bunop(), 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, kind(), spot::M, max(), min(), multop(), spot::NegClosure, spot::NegClosureMarked, spot::Not, spot::Or, spot::OrRat, spot::R, size(), spot::Star, spot::strong_X, spot::tt, spot::U, spot::UConcat, unop(), 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.

Referenced by bunop(), bunop(), map(), nested_unop_range(), sugar_delay(), sugar_delay(), sugar_equal(), and sugar_goto().

◆ 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.

Referenced by bunop(), bunop(), map(), nested_unop_range(), sugar_delay(), sugar_delay(), sugar_equal(), and sugar_goto().

◆ multop() [1/2]

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 formula(), spot::fnode::clone(), and spot::fnode::multop().

Referenced by map().

◆ multop() [2/2]

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 formula(), spot::fnode::multop(), and to_node_().

◆ NegClosure() [1/2]

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

inlinestatic

Construct a negated PSL Closure.

References NegClosure().

Referenced by NegClosure().

◆ NegClosure() [2/2]

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

inlinestatic

Construct a negated PSL Closure.

◆ NegClosureMarked() [1/2]

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

inlinestatic

Construct a marked negated PSL Closure.

References NegClosureMarked().

Referenced by NegClosureMarked().

◆ NegClosureMarked() [2/2]

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

inlinestatic

Construct a marked negated PSL Closure.

◆ nested_unop_range()

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 formula(), spot::fnode::clone(), max(), min(), and spot::fnode::nested_unop_range().

Referenced by F(), G(), strong_X(), and X().

◆ Not() [1/2]

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

inlinestatic

Construct a negation.

◆ Not() [2/2]

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

inlinestatic

Construct a negation.

◆ one_plus()

formula spot::formula::one_plus ( )

inlinestatic

Return a copy of the formula 1[+].

References formula(), and spot::fnode::one_plus().

◆ one_star()

formula spot::formula::one_star ( )

inlinestatic

Return a copy of the formula 1[*].

References formula(), and 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.

References formula().

◆ operator[]()

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

inline

Return children number i.

References formula().

◆ Or() [1/2]

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

inlinestatic

Construct an Or formula.

◆ Or() [2/2]

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

inlinestatic

Construct an Or formula.

◆ OrRat() [1/2]

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

inlinestatic

Construct an Or SERE.

References OrRat().

Referenced by OrRat().

◆ OrRat() [2/2]

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

inlinestatic

Construct an Or SERE.

◆ R() [1/4]

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

inlinestatic

Construct an R formula.

References R().

Referenced by R().

◆ R() [2/4]

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

inlinestatic

Construct an R formula.

◆ R() [3/4]

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

inlinestatic

Construct an R formula.

◆ R() [4/4]

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.

Referenced by map().

◆ Star() [1/2]

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

inlinestatic

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

References Star().

Referenced by Star().

◆ Star() [2/2]

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

inlinestatic

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

◆ strong_X() [1/3]

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

inlinestatic

Construct a strong_X.

References strong_X().

Referenced by strong_X().

◆ strong_X() [2/3]

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

inlinestatic

Construct a strong_X.

◆ strong_X() [3/3]

formula spot::formula::strong_X	(	unsigned	level,
		const formula &	f )

inlinestatic

Construct a strong_X[n].

strong_X[3]f = strong_X strong_X strong_X f

References formula(), nested_unop_range(), spot::Or, and spot::strong_X.

◆ sugar_delay() [1/2]

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.

References formula(), max(), and min().

◆ sugar_delay() [2/2]

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.

References formula(), max(), and min().

◆ sugar_equal()

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.

References formula(), max(), and min().

◆ sugar_goto()

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.

References formula(), max(), and min().

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

formula spot::formula::tt ( )

inlinestatic

Return the true constant.

References formula(), and spot::fnode::tt().

◆ U() [1/4]

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

inlinestatic

Construct a U formula.

References U().

Referenced by bunop(), bunop(), and U().

◆ U() [2/4]

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

inlinestatic

Construct a U formula.

◆ U() [3/4]

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

inlinestatic

Construct a U formula.

◆ U() [4/4]

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

inlinestatic

Construct a U formula.

◆ UConcat() [1/4]

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

inlinestatic

Construct a []-> PSL formula.

References UConcat().

Referenced by UConcat().

◆ UConcat() [2/4]

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

inlinestatic

Construct a []-> PSL formula.

◆ UConcat() [3/4]

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

inlinestatic

Construct a []-> PSL formula.

◆ UConcat() [4/4]

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

inlinestatic

Construct a []-> PSL formula.

◆ unbounded()

constexpr uint8_t spot::formula::unbounded ( )

inlinestaticconstexpr

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

References spot::fnode::unbounded().

Referenced by bunop(), and bunop().

◆ unop() [1/2]

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 formula(), spot::fnode::clone(), and spot::fnode::unop().

Referenced by map().

◆ unop() [2/2]

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 formula(), to_node_(), and spot::fnode::unop().

◆ W() [1/4]

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

inlinestatic

Construct a W formula.

References W().

Referenced by W().

◆ W() [2/4]

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

inlinestatic

Construct a W formula.

◆ W() [3/4]

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

inlinestatic

Construct a W formula.

◆ W() [4/4]

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

inlinestatic

Construct a W formula.

◆ X() [1/3]

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

inlinestatic

Construct an X.

References X().

Referenced by X().

◆ X() [2/3]

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

inlinestatic

Construct an X.

◆ X() [3/3]

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

inlinestatic

Construct an X[n].

X[3]f = XXXf

References formula(), nested_unop_range(), spot::Or, and spot::X.

◆ Xor() [1/4]

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

inlinestatic

Construct an Xor formula.

◆ Xor() [2/4]

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

inlinestatic

Construct an Xor formula.

◆ Xor() [3/4]

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

inlinestatic

Construct an Xor formula.

◆ Xor() [4/4]

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