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 None. 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)
	Copy-assignment operator. More...

const formula &	operator= (formula &&f) noexcept
	Move-assignment operator. More...

bool	operator< (const formula &other) const noexcept
	Less-than comparison (based on unique formula id). More...

bool	operator<= (const formula &other) const noexcept
	Less-than-or-equal comparison. More...

bool	operator> (const formula &other) const noexcept
	Greater-than comparison. More...

bool	operator>= (const formula &other) const noexcept
	Greater-than-or-equal comparison. More...

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

bool	operator== (std::nullptr_t) const noexcept
	Check whether the formula is null. More...

bool	operator!= (const formula &other) const noexcept
	Inequality comparison. More...

bool	operator!= (std::nullptr_t) const noexcept
	Check whether the formula is non-null. More...

	operator bool () const noexcept
	Return `true` iff the formula is non-null. More...

void	throw_if_quantified (const char *message)
	throw message if the formula is quantified More...

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
	Get the name of an atomic proposition. More...

unsigned	apid () const
	Get the number 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...

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

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

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

	SPOT_DEF_PROP (is_syntactic_stutter_invariant)
	Whether the formula is syntactically stutter_invariant. More...

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

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

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

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

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

	SPOT_DEF_PROP (is_eventual)
	Whether the formula is purely eventual. More...

	SPOT_DEF_PROP (is_universal)
	Whether a formula is purely universal. More...

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

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

	SPOT_DEF_PROP (is_delta1)
	Whether a PSL/LTL formula is in the Δ₁ syntactic fragment. More...

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

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

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

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

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

	SPOT_DEF_PROP (is_delta2)
	Whether a PSL/LTL formula is in the Δ₂ syntactic fragment. More...

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

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

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

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

	SPOT_DEF_PROP (is_quantified)
	Whether a PSL/LTL formula has ∃/∀ quantifiers. 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...


	SPOT_DEF_UNOP (Not)
	Construct a negation. More...


	SPOT_DEF_UNOP (X)
	Construct an X. More...


	SPOT_DEF_UNOP (strong_X)
	Construct a strong_X. More...


	SPOT_DEF_UNOP (F)
	Construct an F. More...


	SPOT_DEF_UNOP (G)
	Construct a G. More...


	SPOT_DEF_UNOP (Closure)
	Construct a PSL Closure. More...


	SPOT_DEF_UNOP (NegClosure)
	Construct a negated PSL Closure. More...


	SPOT_DEF_UNOP (NegClosureMarked)
	Construct a marked negated PSL Closure. More...


	SPOT_DEF_UNOP (first_match)
	Construct first_match(sere) More...


	SPOT_DEF_BINOP (Xor)
	Construct an `Xor` formula. More...


	SPOT_DEF_BINOP (Implies)
	Construct an `->` formula. More...


	SPOT_DEF_BINOP (Equiv)
	Construct an `<->` formula. More...


	SPOT_DEF_BINOP (U)
	Construct a `U` formula. More...


	SPOT_DEF_BINOP (R)
	Construct an `R` formula. More...


	SPOT_DEF_BINOP (W)
	Construct a `W` formula. More...


	SPOT_DEF_BINOP (M)
	Construct an `M` formula. More...


	SPOT_DEF_BINOP (EConcat)
	Construct a `<>->` PSL formula. More...


	SPOT_DEF_BINOP (EConcatMarked)
	Construct a marked `<>->` PSL formula. More...


	SPOT_DEF_BINOP (UConcat)
	Construct a `[]->` PSL formula. More...


	SPOT_DEF_MULTOP2 (Or)
	Construct an Or formula. More...


	SPOT_DEF_MULTOP (OrRat)
	Construct an Or SERE. More...


	SPOT_DEF_MULTOP2 (And)
	Construct an And formula. More...


	SPOT_DEF_MULTOP (AndRat)
	Construct an And SERE. More...


	SPOT_DEF_MULTOP (AndNLM)
	Construct a non-length-matching And SERE. More...


	SPOT_DEF_MULTOP (Concat)
	Construct a Concatenation SERE. More...


	SPOT_DEF_MULTOP (Fusion)
	Construct a Fusion SERE. More...


	SPOT_DEF_BUNOP (Star)
	Create SERE for `f[*min..max]` More...


	SPOT_DEF_BUNOP (FStar)
	Create SERE for `f[:*min..max]` More...


	SPOT_DEF_QUANTIFY (exists)
	Create formula for `exists ap : f` More...


	SPOT_DEF_QUANTIFY (forall)
	Create formula for `forall ap : f` More...

Static Public Member Functions
static unsigned	apid_count () noexcept
	1+maximum APID used by atomic propositions More...

static bool	is_valid_apid (unsigned id) noexcept
	check if an APID is valid More...

static const std::string &	apname_from_apid (unsigned id)
	retrieve the name associated to a valid APID More...

static formula	ap_from_apid (unsigned id)
	retrieve the formula associated to a valid APID More...

static std::vector< formula >	apid_map ()
	return the map of APID to formulas More...

static constexpr unsigned	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	strong_X (unsigned level, const formula &f)
	Construct a strong_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 void	report_message (const char *message)
	Report a fatal formula error message and abort. 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	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	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	multop (op o, const formula &f, const formula &g)
	Construct an n-ary operator. More...

static formula	multop (op o, const formula &f, formula &&g)
	Construct an n-ary operator. More...

static formula	multop (op o, formula &&f, const formula &g)
	Construct an n-ary operator. More...

static formula	multop (op o, formula &&f, formula &&g)
	Construct an n-ary operator. 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	quantify (op quantifier, formula &&ap, formula &&f)
	Create a quantified formula (∃ or ∀ over an atomic proposition). More...

static formula	quantify (op quantifier, const formula &ap, const formula &f)
	Create a quantified formula (∃ or ∀ over an atomic proposition). More...

static formula	quantify (op quantifier, const std::vector< formula > &aps, const formula &f)
	Create a quantified formula (∃ or ∀ over an atomic proposition). More...

static formula	quantify (op quantifier, std::vector< formula > &&aps, const formula &f)
	Create a quantified formula (∃ or ∀ over an atomic proposition). 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 fnode objects 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 None.

◆ 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

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

◆ 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(), and spot::bdd_dict_preorder::register_proposition().

◆ ap_from_apid()

static formula spot::formula::ap_from_apid ( unsigned id )

static

retrieve the formula associated to a valid APID

See also: is_valid_apid

◆ ap_name()

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

inline

Get the name of an atomic proposition.

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

◆ apid()

unsigned spot::formula::apid ( ) const

inline

Get the number of an atomic proposition.

Atomic propositions are initially numbered with consecutive numbers in the order they are created, starting with 0. However once formulas representing some atomic propositions are no-longer referenced, their number are recycled (in LIFO order).

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

◆ apid_count()

static unsigned spot::formula::apid_count ( )

staticnoexcept

1+maximum APID used by atomic propositions

Each atomic proposition created by Spot is assigned a unique APID: an integer that is increased from 0.

Internally, the atomic proposition names are stored in an array indexed by APIDs. This function returns the size of this array.

This value may change when new atomic propositions are added or removed.

See also: is_valid_apid; apname_from_apid; ap_from_apid

◆ apid_map()

static std::vector<formula> spot::formula::apid_map ( )

static

return the map of APID to formulas

This builds and return a vector of formulas indexed by APIDs. The size of this vector is equal to apid_count(). The formulas will either correspond to an atomic proposition, or to nullptr if the corresponding APID is invalid (because the corresponding atomic proposition is not referenced anymore).

◆ apname_from_apid()

static const std::string& spot::formula::apname_from_apid ( unsigned id )

static

retrieve the name associated to a valid APID

See also: is_valid_apid

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

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

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

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

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

◆ end()

formula_child_iterator spot::formula::end ( ) const

inline

Allow iterating over children.

◆ eword()

static formula spot::formula::eword ( )

inlinestatic

Return the empty word constant.

References spot::fnode::eword().

◆ F()

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

◆ G()

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

◆ 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

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

bool spot::formula::is_constant ( ) const

inline

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

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

bool spot::formula::is_tt ( ) const

inline

Whether the formula is the true constant.

◆ is_valid_apid()

static bool spot::formula::is_valid_apid ( unsigned id )

staticnoexcept

check if an APID is valid

Because atomic propositions will be removed when they are no longer used, not all APIDs are valid.

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

◆ 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::exists, spot::F, spot::ff, spot::first_match, spot::forall, 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::strong_X, 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/6]

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

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.

This comes into two flavors: n-ary (where the arguments are passed via a vector), or binary (the two arguments can be passed separately.

When building complex formulas, be careful that Spot assigns a serial number to each new subformula it constructs, and that this number is later used to maintain a normal form of formulas by ordering children of commutative operators. Unfortunately, C++ does not guarantee the order in which function arguments are evaluated. So if you write formula::multop(op::And, formula::G(x), formula::F(y)). it is unspecified whether formula::G(x) or formula::F(y) will be created first, so it may cause your code to behave differently on different platform. Better use multiple instructions to name the intermediate subformulas, and ensure the same construction order everywhere.

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

◆ multop() [2/6]

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

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.

This comes into two flavors: n-ary (where the arguments are passed via a vector), or binary (the two arguments can be passed separately.

When building complex formulas, be careful that Spot assigns a serial number to each new subformula it constructs, and that this number is later used to maintain a normal form of formulas by ordering children of commutative operators. Unfortunately, C++ does not guarantee the order in which function arguments are evaluated. So if you write formula::multop(op::And, formula::G(x), formula::F(y)). it is unspecified whether formula::G(x) or formula::F(y) will be created first, so it may cause your code to behave differently on different platform. Better use multiple instructions to name the intermediate subformulas, and ensure the same construction order everywhere.

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

◆ multop() [3/6]

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.

This comes into two flavors: n-ary (where the arguments are passed via a vector), or binary (the two arguments can be passed separately.

When building complex formulas, be careful that Spot assigns a serial number to each new subformula it constructs, and that this number is later used to maintain a normal form of formulas by ordering children of commutative operators. Unfortunately, C++ does not guarantee the order in which function arguments are evaluated. So if you write formula::multop(op::And, formula::G(x), formula::F(y)). it is unspecified whether formula::G(x) or formula::F(y) will be created first, so it may cause your code to behave differently on different platform. Better use multiple instructions to name the intermediate subformulas, and ensure the same construction order everywhere.

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

◆ multop() [4/6]

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

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.

This comes into two flavors: n-ary (where the arguments are passed via a vector), or binary (the two arguments can be passed separately.

When building complex formulas, be careful that Spot assigns a serial number to each new subformula it constructs, and that this number is later used to maintain a normal form of formulas by ordering children of commutative operators. Unfortunately, C++ does not guarantee the order in which function arguments are evaluated. So if you write formula::multop(op::And, formula::G(x), formula::F(y)). it is unspecified whether formula::G(x) or formula::F(y) will be created first, so it may cause your code to behave differently on different platform. Better use multiple instructions to name the intermediate subformulas, and ensure the same construction order everywhere.

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

◆ multop() [5/6]

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

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.

This comes into two flavors: n-ary (where the arguments are passed via a vector), or binary (the two arguments can be passed separately.

When building complex formulas, be careful that Spot assigns a serial number to each new subformula it constructs, and that this number is later used to maintain a normal form of formulas by ordering children of commutative operators. Unfortunately, C++ does not guarantee the order in which function arguments are evaluated. So if you write formula::multop(op::And, formula::G(x), formula::F(y)). it is unspecified whether formula::G(x) or formula::F(y) will be created first, so it may cause your code to behave differently on different platform. Better use multiple instructions to name the intermediate subformulas, and ensure the same construction order everywhere.

References spot::fnode::multop().

◆ multop() [6/6]

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.

This comes into two flavors: n-ary (where the arguments are passed via a vector), or binary (the two arguments can be passed separately.

When building complex formulas, be careful that Spot assigns a serial number to each new subformula it constructs, and that this number is later used to maintain a normal form of formulas by ordering children of commutative operators. Unfortunately, C++ does not guarantee the order in which function arguments are evaluated. So if you write formula::multop(op::And, formula::G(x), formula::F(y)). it is unspecified whether formula::G(x) or formula::F(y) will be created first, so it may cause your code to behave differently on different platform. Better use multiple instructions to name the intermediate subformulas, and ensure the same construction order everywhere.

References spot::fnode::multop().

◆ 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 choose between the different numbers with bo.

For instance nested_unop_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().

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

spot::formula::operator bool ( ) const

inlineexplicitnoexcept

Return true iff the formula is non-null.

◆ operator!=() [1/2]

bool spot::formula::operator!= ( const formula & other ) const

inlinenoexcept

Inequality comparison.

◆ operator!=() [2/2]

bool spot::formula::operator!= ( std::nullptr_t ) const

inlinenoexcept

Check whether the formula is non-null.

◆ operator<()

bool spot::formula::operator< ( const formula & other ) const

inlinenoexcept

Less-than comparison (based on unique formula id).

◆ operator<=()

bool spot::formula::operator<= ( const formula & other ) const

inlinenoexcept

Less-than-or-equal comparison.

◆ operator=() [1/3]

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

inline

Copy-assignment operator.

◆ operator=() [2/3]

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

inlinenoexcept

Move-assignment operator.

◆ operator=() [3/3]

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==() [1/2]

bool spot::formula::operator== ( const formula & other ) const

inlinenoexcept

Equality comparison (formulas are hash-consed, so pointer equality suffices).

◆ operator==() [2/2]

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

inlinenoexcept

Check whether the formula is null.

◆ operator>()

bool spot::formula::operator> ( const formula & other ) const

inlinenoexcept

Greater-than comparison.

◆ operator>=()

bool spot::formula::operator>= ( const formula & other ) const

inlinenoexcept

Greater-than-or-equal comparison.

◆ operator[]()

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

inline

Return children number i.

◆ quantify() [1/4]

static formula spot::formula::quantify	(	op	quantifier,
		const formula &	ap,
		const formula &	f
	)

inlinestatic

Create a quantified formula (∃ or ∀ over an atomic proposition).

The quantifier must be op::Exists or op::ForAll.

References spot::ap, spot::fnode::clone(), and spot::fnode::quantify().

◆ quantify() [2/4]

static formula spot::formula::quantify	(	op	quantifier,
		const std::vector< formula > &	aps,
		const formula &	f
	)

inlinestatic

Create a quantified formula (∃ or ∀ over an atomic proposition).

The quantifier must be op::Exists or op::ForAll.

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

◆ quantify() [3/4]

static formula spot::formula::quantify	(	op	quantifier,
		formula &&	ap,
		formula &&	f
	)

inlinestatic

Create a quantified formula (∃ or ∀ over an atomic proposition).

The quantifier must be op::Exists or op::ForAll.

References spot::ap, spot::fnode::quantify(), and to_node_().

◆ quantify() [4/4]

static formula spot::formula::quantify	(	op	quantifier,
		std::vector< formula > &&	aps,
		const formula &	f
	)

inlinestatic

Create a quantified formula (∃ or ∀ over an atomic proposition).

The quantifier must be op::Exists or op::ForAll.

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

◆ report_message()

static void spot::formula::report_message ( const char * message )

static

Report a fatal formula error message and abort.

◆ size()

unsigned spot::formula::size ( ) const

inline

Return the number of children.

◆ SPOT_DEF_BINOP() [1/10]

spot::formula::SPOT_DEF_BINOP ( EConcat )

Construct a <>-> PSL formula.

◆ SPOT_DEF_BINOP() [2/10]

spot::formula::SPOT_DEF_BINOP ( EConcatMarked )

Construct a marked <>-> PSL formula.

◆ SPOT_DEF_BINOP() [3/10]

spot::formula::SPOT_DEF_BINOP ( Equiv )

Construct an <-> formula.

◆ SPOT_DEF_BINOP() [4/10]

spot::formula::SPOT_DEF_BINOP ( Implies )

Construct an -> formula.

◆ SPOT_DEF_BINOP() [5/10]

spot::formula::SPOT_DEF_BINOP ( M )

Construct an M formula.

◆ SPOT_DEF_BINOP() [6/10]

spot::formula::SPOT_DEF_BINOP ( R )

Construct an R formula.

◆ SPOT_DEF_BINOP() [7/10]

spot::formula::SPOT_DEF_BINOP ( U )

Construct a U formula.

◆ SPOT_DEF_BINOP() [8/10]

spot::formula::SPOT_DEF_BINOP ( UConcat )

Construct a []-> PSL formula.

◆ SPOT_DEF_BINOP() [9/10]

spot::formula::SPOT_DEF_BINOP ( W )

Construct a W formula.

◆ SPOT_DEF_BINOP() [10/10]

spot::formula::SPOT_DEF_BINOP ( Xor )

Construct an Xor formula.

◆ SPOT_DEF_BUNOP() [1/2]

spot::formula::SPOT_DEF_BUNOP ( FStar )

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

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

◆ SPOT_DEF_BUNOP() [2/2]

spot::formula::SPOT_DEF_BUNOP ( Star )

Create SERE for f[*min..max]

◆ SPOT_DEF_MULTOP() [1/5]

spot::formula::SPOT_DEF_MULTOP ( AndNLM )

Construct a non-length-matching And SERE.

◆ SPOT_DEF_MULTOP() [2/5]

spot::formula::SPOT_DEF_MULTOP ( AndRat )

Construct an And SERE.

◆ SPOT_DEF_MULTOP() [3/5]

spot::formula::SPOT_DEF_MULTOP ( Concat )

Construct a Concatenation SERE.

◆ SPOT_DEF_MULTOP() [4/5]

spot::formula::SPOT_DEF_MULTOP ( Fusion )

Construct a Fusion SERE.

◆ SPOT_DEF_MULTOP() [5/5]

spot::formula::SPOT_DEF_MULTOP ( OrRat )

Construct an Or SERE.

◆ SPOT_DEF_MULTOP2() [1/2]

spot::formula::SPOT_DEF_MULTOP2 ( And )

Construct an And formula.

◆ SPOT_DEF_MULTOP2() [2/2]

spot::formula::SPOT_DEF_MULTOP2 ( Or )

Construct an Or formula.

◆ SPOT_DEF_PROP() [1/25]

spot::formula::SPOT_DEF_PROP ( accepts_eword )

Whether the formula accepts [*0].

◆ SPOT_DEF_PROP() [2/25]

spot::formula::SPOT_DEF_PROP ( has_lbt_atomic_props )

Whether the formula has only LBT-compatible atomic propositions.

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

◆ SPOT_DEF_PROP() [3/25]

spot::formula::SPOT_DEF_PROP ( has_spin_atomic_props )

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

◆ SPOT_DEF_PROP() [4/25]

spot::formula::SPOT_DEF_PROP ( is_boolean )

Whether the formula use only boolean operators.

◆ SPOT_DEF_PROP() [5/25]

spot::formula::SPOT_DEF_PROP ( is_delta1 )

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.

◆ SPOT_DEF_PROP() [6/25]

spot::formula::SPOT_DEF_PROP ( is_delta2 )

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

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

◆ SPOT_DEF_PROP() [7/25]

spot::formula::SPOT_DEF_PROP ( is_eventual )

Whether the formula is purely eventual.

Pure eventuality formulas are defined in

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

◆ SPOT_DEF_PROP() [8/25]

spot::formula::SPOT_DEF_PROP ( is_finite )

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

◆ SPOT_DEF_PROP() [9/25]

spot::formula::SPOT_DEF_PROP ( is_in_nenoform )

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.

◆ SPOT_DEF_PROP() [10/25]

spot::formula::SPOT_DEF_PROP ( is_ltl_formula )

Whether the formula uses only LTL operators.

◆ SPOT_DEF_PROP() [11/25]

spot::formula::SPOT_DEF_PROP ( is_marked )

Whether the formula has an occurrence of EConcatMarked or NegClosureMarked.

◆ SPOT_DEF_PROP() [12/25]

spot::formula::SPOT_DEF_PROP ( is_pi2 )

Whether a PSL/LTL formula is in Π₂

◆ SPOT_DEF_PROP() [13/25]

spot::formula::SPOT_DEF_PROP ( is_psl_formula )

Whether the formula uses only PSL operators.

◆ SPOT_DEF_PROP() [14/25]

spot::formula::SPOT_DEF_PROP ( is_quantified )

Whether a PSL/LTL formula has ∃/∀ quantifiers.

◆ SPOT_DEF_PROP() [15/25]

spot::formula::SPOT_DEF_PROP ( is_sere_formula )

Whether the formula uses only SERE operators.

◆ SPOT_DEF_PROP() [16/25]

spot::formula::SPOT_DEF_PROP ( is_sigma2 )

Whether a PSL/LTL formula is in Σ₂

◆ SPOT_DEF_PROP() [17/25]

spot::formula::SPOT_DEF_PROP ( is_sugar_free_boolean )

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

◆ SPOT_DEF_PROP() [18/25]

spot::formula::SPOT_DEF_PROP ( is_sugar_free_ltl )

Whether the formula avoids the F and G operators.

◆ SPOT_DEF_PROP() [19/25]

spot::formula::SPOT_DEF_PROP ( is_syntactic_guarantee )

Whether a PSL/LTL formula is syntactic guarantee property.

This class is also called Σ₁.

◆ SPOT_DEF_PROP() [20/25]

spot::formula::SPOT_DEF_PROP ( is_syntactic_obligation )

Whether a PSL/LTL formula is syntactic obligation property.

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

◆ SPOT_DEF_PROP() [21/25]

spot::formula::SPOT_DEF_PROP ( is_syntactic_persistence )

Whether a PSL/LTL formula is syntactic persistence property.

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

◆ SPOT_DEF_PROP() [22/25]

spot::formula::SPOT_DEF_PROP ( is_syntactic_recurrence )

Whether a PSL/LTL formula is syntactic recurrence property.

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

◆ SPOT_DEF_PROP() [23/25]

spot::formula::SPOT_DEF_PROP ( is_syntactic_safety )

Whether a PSL/LTL formula is syntactic safety property.

This class is also called Π₁.

◆ SPOT_DEF_PROP() [24/25]

spot::formula::SPOT_DEF_PROP ( is_syntactic_stutter_invariant )

Whether the formula is syntactically stutter_invariant.

◆ SPOT_DEF_PROP() [25/25]

spot::formula::SPOT_DEF_PROP ( is_universal )

Whether a formula is purely universal.

Purely universal formulas are defined in

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

◆ SPOT_DEF_QUANTIFY() [1/2]

spot::formula::SPOT_DEF_QUANTIFY ( exists )

Create formula for exists ap : f

◆ SPOT_DEF_QUANTIFY() [2/2]

spot::formula::SPOT_DEF_QUANTIFY ( forall )

Create formula for forall ap : f

◆ SPOT_DEF_UNOP() [1/9]

spot::formula::SPOT_DEF_UNOP ( Closure )

Construct a PSL Closure.

◆ SPOT_DEF_UNOP() [2/9]

spot::formula::SPOT_DEF_UNOP ( F )

Construct an F.

◆ SPOT_DEF_UNOP() [3/9]

spot::formula::SPOT_DEF_UNOP ( first_match )

Construct first_match(sere)

◆ SPOT_DEF_UNOP() [4/9]

spot::formula::SPOT_DEF_UNOP ( G )

Construct a G.

◆ SPOT_DEF_UNOP() [5/9]

spot::formula::SPOT_DEF_UNOP ( NegClosure )

Construct a negated PSL Closure.

◆ SPOT_DEF_UNOP() [6/9]

spot::formula::SPOT_DEF_UNOP ( NegClosureMarked )

Construct a marked negated PSL Closure.

◆ SPOT_DEF_UNOP() [7/9]

spot::formula::SPOT_DEF_UNOP ( Not )

Construct a negation.

◆ SPOT_DEF_UNOP() [8/9]

spot::formula::SPOT_DEF_UNOP ( strong_X )

Construct a strong_X.

◆ SPOT_DEF_UNOP() [9/9]

spot::formula::SPOT_DEF_UNOP ( X )

Construct an X.

◆ strong_X()

static 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 spot::Or, and spot::strong_X.

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

◆ throw_if_quantified()

void spot::formula::throw_if_quantified ( const char * message )

inline

throw message if the formula is quantified

◆ 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 bunop(), and quantify().

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

◆ unbounded()

static constexpr unsigned 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 spot::fnode::unop().

◆ X()

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.

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

◆ all_but()

◆ ap() [1/2]

◆ ap() [2/2]

◆ ap_from_apid()

◆ ap_name()

◆ apid()

◆ apid_count()

◆ apid_map()

◆ apname_from_apid()

◆ begin()

◆ binop() [1/4]

◆ binop() [2/4]

◆ binop() [3/4]

◆ binop() [4/4]

◆ boolean_count()

◆ boolean_operands()

◆ bunop() [1/2]

◆ bunop() [2/2]

◆ dump()

◆ end()

◆ eword()

◆ F()

◆ ff()

◆ G()

◆ get_child_of() [1/2]

◆ get_child_of() [2/2]

◆ id()

◆ is() [1/5]

◆ is() [2/5]

◆ is() [3/5]

◆ is() [4/5]

◆ is() [5/5]

◆ is_constant()

◆ is_eword()

◆ is_ff()

◆ is_Kleene_star()

◆ is_leaf()

◆ is_literal()

◆ is_tt()

◆ is_valid_apid()

◆ kind()

◆ kindstr()

◆ map()

◆ max()

◆ min()

◆ multop() [1/6]

◆ multop() [2/6]

◆ multop() [3/6]

◆ multop() [4/6]

◆ multop() [5/6]

◆ multop() [6/6]

◆ nested_unop_range()

◆ one_plus()

◆ one_star()

◆ operator bool()

◆ operator!=() [1/2]

◆ operator!=() [2/2]

◆ operator<()

◆ operator<=()

◆ operator=() [1/3]

◆ operator=() [2/3]

◆ operator=() [3/3]

◆ operator==() [1/2]

◆ operator==() [2/2]

◆ operator>()

◆ operator>=()

◆ operator[]()