spot  2.11.6
Classes | Public Member Functions | Static Public Member Functions | List of all members
spot::formula Class Referencefinal

Main class for temporal logic formula. More...

#include <spot/tl/formula.hh>

Collaboration diagram for spot::formula:

Classes

class  formula_child_iterator
 Allow iterating over children. More...
 

Public Member Functions

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

Static Public Member Functions

static constexpr uint8_t unbounded ()
 Unbounded constant to use as end of range for bounded operators. More...
 
static formula ap (const std::string &name)
 Build an atomic proposition. More...
 
static formula ap (const formula &a)
 Build an atomic proposition from... an atomic proposition. More...
 
static formula X (unsigned level, const formula &f)
 Construct an X[n]. More...
 
static formula F (unsigned min_level, unsigned max_level, const formula &f)
 Construct F[n:m]. More...
 
static formula G (unsigned min_level, unsigned max_level, const formula &f)
 Construct G[n:m]. More...
 
static const formula nested_unop_range (op uo, op bo, unsigned min, unsigned max, formula f)
 Nested operator construction (syntactic sugar). More...
 
static formula sugar_goto (const formula &b, unsigned min, unsigned max)
 Create a SERE equivalent to b[->min..max] More...
 
static formula sugar_equal (const formula &b, unsigned min, unsigned max)
 Create the SERE b[=min..max] More...
 
static formula ff ()
 Return the false constant. More...
 
static formula tt ()
 Return the true constant. More...
 
static formula eword ()
 Return the empty word constant. More...
 
static formula one_star ()
 Return a copy of the formula 1[*]. More...
 
static formula unop (op o, const formula &f)
 Build a unary operator. More...
 
static formula unop (op o, formula &&f)
 Build a unary operator. More...
 
static formula Not (const formula &f)
 Construct a negation. More...
 
static formula Not (formula &&f)
 Construct a negation. More...
 
static formula X (const formula &f)
 Construct an X. More...
 
static formula X (formula &&f)
 Construct an X. More...
 
static formula F (const formula &f)
 Construct an F. More...
 
static formula F (formula &&f)
 Construct an F. More...
 
static formula G (const formula &f)
 Construct a G. More...
 
static formula G (formula &&f)
 Construct a G. More...
 
static formula Closure (const formula &f)
 Construct a PSL Closure. More...
 
static formula Closure (formula &&f)
 Construct a PSL Closure. More...
 
static formula NegClosure (const formula &f)
 Construct a negated PSL Closure. More...
 
static formula NegClosure (formula &&f)
 Construct a negated PSL Closure. More...
 
static formula NegClosureMarked (const formula &f)
 Construct a marked negated PSL Closure. More...
 
static formula NegClosureMarked (formula &&f)
 Construct a marked negated PSL Closure. More...
 
static formula first_match (const formula &f)
 Construct first_match(sere) More...
 
static formula first_match (formula &&f)
 Construct first_match(sere) More...
 
static formula binop (op o, const formula &f, const formula &g)
 Construct a binary operator. More...
 
static formula binop (op o, const formula &f, formula &&g)
 Construct a binary operator. More...
 
static formula binop (op o, formula &&f, const formula &g)
 Construct a binary operator. More...
 
static formula binop (op o, formula &&f, formula &&g)
 Construct a binary operator. More...
 
static formula Xor (const formula &f, const formula &g)
 Construct an Xor formula. More...
 
static formula Xor (const formula &f, formula &&g)
 Construct an Xor formula. More...
 
static formula Xor (formula &&f, const formula &g)
 Construct an Xor formula. More...
 
static formula Xor (formula &&f, formula &&g)
 Construct an Xor formula. More...
 
static formula Implies (const formula &f, const formula &g)
 Construct an -> formula. More...
 
static formula Implies (const formula &f, formula &&g)
 Construct an -> formula. More...
 
static formula Implies (formula &&f, const formula &g)
 Construct an -> formula. More...
 
static formula Implies (formula &&f, formula &&g)
 Construct an -> formula. More...
 
static formula Equiv (const formula &f, const formula &g)
 Construct an <-> formula. More...
 
static formula Equiv (const formula &f, formula &&g)
 Construct an <-> formula. More...
 
static formula Equiv (formula &&f, const formula &g)
 Construct an <-> formula. More...
 
static formula Equiv (formula &&f, formula &&g)
 Construct an <-> formula. More...
 
static formula U (const formula &f, const formula &g)
 Construct a U formula. More...
 
static formula U (const formula &f, formula &&g)
 Construct a U formula. More...
 
static formula U (formula &&f, const formula &g)
 Construct a U formula. More...
 
static formula U (formula &&f, formula &&g)
 Construct a U formula. More...
 
static formula R (const formula &f, const formula &g)
 Construct an R formula. More...
 
static formula R (const formula &f, formula &&g)
 Construct an R formula. More...
 
static formula R (formula &&f, const formula &g)
 Construct an R formula. More...
 
static formula R (formula &&f, formula &&g)
 Construct an R formula. More...
 
static formula W (const formula &f, const formula &g)
 Construct a W formula. More...
 
static formula W (const formula &f, formula &&g)
 Construct a W formula. More...
 
static formula W (formula &&f, const formula &g)
 Construct a W formula. More...
 
static formula W (formula &&f, formula &&g)
 Construct a W formula. More...
 
static formula M (const formula &f, const formula &g)
 Construct an M formula. More...
 
static formula M (const formula &f, formula &&g)
 Construct an M formula. More...
 
static formula M (formula &&f, const formula &g)
 Construct an M formula. More...
 
static formula M (formula &&f, formula &&g)
 Construct an M formula. More...
 
static formula EConcat (const formula &f, const formula &g)
 Construct a <>-> PSL formula. More...
 
static formula EConcat (const formula &f, formula &&g)
 Construct a <>-> PSL formula. More...
 
static formula EConcat (formula &&f, const formula &g)
 Construct a <>-> PSL formula. More...
 
static formula EConcat (formula &&f, formula &&g)
 Construct a <>-> PSL formula. More...
 
static formula EConcatMarked (const formula &f, const formula &g)
 Construct a marked <>-> PSL formula. More...
 
static formula EConcatMarked (const formula &f, formula &&g)
 Construct a marked <>-> PSL formula. More...
 
static formula EConcatMarked (formula &&f, const formula &g)
 Construct a marked <>-> PSL formula. More...
 
static formula EConcatMarked (formula &&f, formula &&g)
 Construct a marked <>-> PSL formula. More...
 
static formula UConcat (const formula &f, const formula &g)
 Construct a []-> PSL formula. More...
 
static formula UConcat (const formula &f, formula &&g)
 Construct a []-> PSL formula. More...
 
static formula UConcat (formula &&f, const formula &g)
 Construct a []-> PSL formula. More...
 
static formula UConcat (formula &&f, formula &&g)
 Construct a []-> PSL formula. More...
 
static formula multop (op o, const std::vector< formula > &l)
 Construct an n-ary operator. More...
 
static formula multop (op o, std::vector< formula > &&l)
 Construct an n-ary operator. More...
 
static formula Or (const std::vector< formula > &l)
 Construct an Or formula. More...
 
static formula Or (std::vector< formula > &&l)
 Construct an Or formula. More...
 
static formula OrRat (const std::vector< formula > &l)
 Construct an Or SERE. More...
 
static formula OrRat (std::vector< formula > &&l)
 Construct an Or SERE. More...
 
static formula And (const std::vector< formula > &l)
 Construct an And formula. More...
 
static formula And (std::vector< formula > &&l)
 Construct an And formula. More...
 
static formula AndRat (const std::vector< formula > &l)
 Construct an And SERE. More...
 
static formula AndRat (std::vector< formula > &&l)
 Construct an And SERE. More...
 
static formula AndNLM (const std::vector< formula > &l)
 Construct a non-length-matching And SERE. More...
 
static formula AndNLM (std::vector< formula > &&l)
 Construct a non-length-matching And SERE. More...
 
static formula Concat (const std::vector< formula > &l)
 Construct a Concatenation SERE. More...
 
static formula Concat (std::vector< formula > &&l)
 Construct a Concatenation SERE. More...
 
static formula Fusion (const std::vector< formula > &l)
 Construct a Fusion SERE. More...
 
static formula Fusion (std::vector< formula > &&l)
 Construct a Fusion SERE. More...
 
static formula bunop (op o, const formula &f, unsigned min=0U, unsigned max=unbounded())
 Define a bounded unary-operator (i.e. star-like) More...
 
static formula bunop (op o, formula &&f, unsigned min=0U, unsigned max=unbounded())
 Define a bounded unary-operator (i.e. star-like) More...
 
static formula Star (const formula &f, unsigned min=0U, unsigned max=unbounded())
 Create SERE for f[*min..max] More...
 
static formula Star (formula &&f, unsigned min=0U, unsigned max=unbounded())
 Create SERE for f[*min..max] More...
 
static formula FStar (const formula &f, unsigned min=0U, unsigned max=unbounded())
 Create SERE for f[:*min..max] More...
 
static formula FStar (formula &&f, unsigned min=0U, unsigned max=unbounded())
 Create SERE for f[:*min..max] More...
 
static formula sugar_delay (const formula &a, const formula &b, unsigned min, unsigned max)
 Create the SERE a ##[n:m] b More...
 
static formula sugar_delay (const formula &b, unsigned min, unsigned max)
 Create the SERE a ##[n:m] b More...
 

Detailed Description

Main class for temporal logic formula.

Constructor & Destructor Documentation

◆ formula() [1/5]

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

Create a formula from an fnode.

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

◆ formula() [2/5]

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

Create a null formula.

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

◆ formula() [3/5]

spot::formula::formula ( )
inlinenoexcept

Default initialize a formula to nullptr.

◆ formula() [4/5]

spot::formula::formula ( const formula f)
inlinenoexcept

Clone a formula.

◆ formula() [5/5]

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

Move-construct a formula.

◆ ~formula()

spot::formula::~formula ( )
inline

Destroy a formula.

Member Function Documentation

◆ accepts_eword()

bool spot::formula::accepts_eword ( ) const
inline

Whether the formula accepts [*0].

◆ all_but()

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

clone this formula, omitting child i

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

◆ And() [1/2]

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

Construct an And formula.

◆ And() [2/2]

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

Construct an And formula.

◆ AndNLM() [1/2]

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

Construct a non-length-matching And SERE.

◆ AndNLM() [2/2]

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

Construct a non-length-matching And SERE.

◆ AndRat() [1/2]

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

Construct an And SERE.

◆ AndRat() [2/2]

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

Construct an And SERE.

◆ ap() [1/2]

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

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

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

References spot::ap, and kind().

◆ ap() [2/2]

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

Build an atomic proposition.

References spot::fnode::ap().

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

◆ ap_name()

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

Print the name of an atomic proposition.

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

◆ begin()

formula_child_iterator spot::formula::begin ( ) const
inline

Allow iterating over children.

◆ binop() [1/4]

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

Construct a binary operator.

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

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

◆ binop() [2/4]

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

Construct a binary operator.

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

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

◆ binop() [3/4]

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

Construct a binary operator.

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

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

◆ binop() [4/4]

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

Construct a binary operator.

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

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

◆ boolean_count()

unsigned spot::formula::boolean_count ( ) const
inline

number of Boolean children

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

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

◆ boolean_operands()

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

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

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

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

◆ bunop() [1/2]

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

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

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

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

◆ bunop() [2/2]

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

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

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

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

◆ Closure() [1/2]

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

Construct a PSL Closure.

◆ Closure() [2/2]

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

Construct a PSL Closure.

◆ Concat() [1/2]

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

Construct a Concatenation SERE.

◆ Concat() [2/2]

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

Construct a Concatenation SERE.

◆ dump()

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

Print the formula for debugging.

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

◆ EConcat() [1/4]

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

Construct a <>-> PSL formula.

◆ EConcat() [2/4]

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

Construct a <>-> PSL formula.

◆ EConcat() [3/4]

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

Construct a <>-> PSL formula.

◆ EConcat() [4/4]

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

Construct a <>-> PSL formula.

◆ EConcatMarked() [1/4]

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

Construct a marked <>-> PSL formula.

◆ EConcatMarked() [2/4]

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

Construct a marked <>-> PSL formula.

◆ EConcatMarked() [3/4]

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

Construct a marked <>-> PSL formula.

◆ EConcatMarked() [4/4]

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

Construct a marked <>-> PSL formula.

◆ end()

formula_child_iterator spot::formula::end ( ) const
inline

Allow iterating over children.

◆ Equiv() [1/4]

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

Construct an <-> formula.

◆ Equiv() [2/4]

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

Construct an <-> formula.

◆ Equiv() [3/4]

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

Construct an <-> formula.

◆ Equiv() [4/4]

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

Construct an <-> formula.

◆ eword()

static formula spot::formula::eword ( )
inlinestatic

Return the empty word constant.

References spot::fnode::eword().

◆ F() [1/3]

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

Construct an F.

◆ F() [2/3]

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

Construct an F.

◆ F() [3/3]

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

Construct F[n:m].

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

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

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

◆ ff()

static formula spot::formula::ff ( )
inlinestatic

Return the false constant.

References spot::fnode::ff().

◆ first_match() [1/2]

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

Construct first_match(sere)

◆ first_match() [2/2]

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

Construct first_match(sere)

◆ FStar() [1/2]

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

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

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

◆ FStar() [2/2]

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

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

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

◆ Fusion() [1/2]

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

Construct a Fusion SERE.

◆ Fusion() [2/2]

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

Construct a Fusion SERE.

◆ G() [1/3]

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

Construct a G.

◆ G() [2/3]

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

Construct a G.

◆ G() [3/3]

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

Construct G[n:m].

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

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

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

◆ get_child_of() [1/2]

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

Remove operator o and return the child.

This works only for unary operators.

References get_child_of().

Referenced by get_child_of().

◆ get_child_of() [2/2]

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

Remove all operators in l and return the child.

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

References get_child_of().

◆ has_lbt_atomic_props()

bool spot::formula::has_lbt_atomic_props ( ) const
inline

Whether the formula has only LBT-compatible atomic propositions.

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

◆ has_spin_atomic_props()

bool spot::formula::has_spin_atomic_props ( ) const
inline

Whether the formula has spin-compatible atomic propositions.

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

See also
spot::is_spin_ap()

◆ id()

size_t spot::formula::id ( ) const
inline

Return the id of a formula.

Can be used as a hash number.

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

◆ Implies() [1/4]

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

Construct an -> formula.

◆ Implies() [2/4]

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

Construct an -> formula.

◆ Implies() [3/4]

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

Construct an -> formula.

◆ Implies() [4/4]

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

Construct an -> formula.

◆ is() [1/5]

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

Return true if the formula is of kind o.

◆ is() [2/5]

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

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

◆ is() [3/5]

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

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

◆ is() [4/5]

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

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

◆ is() [5/5]

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

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

◆ is_boolean()

bool spot::formula::is_boolean ( ) const
inline

Whether the formula use only boolean operators.

◆ is_constant()

bool spot::formula::is_constant ( ) const
inline

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

◆ is_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. [19]

◆ is_eword()

bool spot::formula::is_eword ( ) const
inline

Whether the formula is the empty word constant.

◆ is_ff()

bool spot::formula::is_ff ( ) const
inline

Whether the formula is the false constant.

◆ is_finite()

bool spot::formula::is_finite ( ) const
inline

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

◆ is_in_nenoform()

bool spot::formula::is_in_nenoform ( ) const
inline

Whether the formula is in negative normal form.

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

◆ is_Kleene_star()

bool spot::formula::is_Kleene_star ( ) const
inline

Test whether the formula represent a Kleene star.

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

◆ is_leaf()

bool spot::formula::is_leaf ( ) const
inline

Whether the formula is a leaf.

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

◆ is_literal()

bool spot::formula::is_literal ( ) const
inline

Whether the formula is an atomic proposition or its negation.

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

◆ is_ltl_formula()

bool spot::formula::is_ltl_formula ( ) const
inline

Whether the formula uses only LTL operators.

◆ is_marked()

bool spot::formula::is_marked ( ) const
inline

Whether the formula has an occurrence of EConcatMarked or NegClosureMarked.

◆ is_psl_formula()

bool spot::formula::is_psl_formula ( ) const
inline

Whether the formula uses only PSL operators.

◆ is_sere_formula()

bool spot::formula::is_sere_formula ( ) const
inline

Whether the formula uses only SERE operators.

◆ is_sugar_free_boolean()

bool spot::formula::is_sugar_free_boolean ( ) const
inline

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

◆ is_sugar_free_ltl()

bool spot::formula::is_sugar_free_ltl ( ) const
inline

Whether the formula avoids the F and G operators.

◆ is_syntactic_guarantee()

bool spot::formula::is_syntactic_guarantee ( ) const
inline

Whether a PSL/LTL formula is syntactic guarantee property.

◆ is_syntactic_obligation()

bool spot::formula::is_syntactic_obligation ( ) const
inline

Whether a PSL/LTL formula is syntactic obligation property.

◆ is_syntactic_persistence()

bool spot::formula::is_syntactic_persistence ( ) const
inline

Whether a PSL/LTL formula is syntactic persistence property.

◆ is_syntactic_recurrence()

bool spot::formula::is_syntactic_recurrence ( ) const
inline

Whether a PSL/LTL formula is syntactic recurrence property.

◆ is_syntactic_safety()

bool spot::formula::is_syntactic_safety ( ) const
inline

Whether a PSL/LTL formula is syntactic safety property.

◆ is_syntactic_stutter_invariant()

bool spot::formula::is_syntactic_stutter_invariant ( ) const
inline

Whether the formula is syntactically stutter_invariant.

◆ is_tt()

bool spot::formula::is_tt ( ) const
inline

Whether the formula is the true constant.

◆ is_universal()

bool spot::formula::is_universal ( ) const
inline

Whether a formula is purely universal.

Purely universal formulae are defined in

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

◆ kind()

op spot::formula::kind ( ) const
inline

Return top-most operator.

Referenced by ap().

◆ kindstr()

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

Return the name of the top-most operator.

◆ M() [1/4]

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

Construct an M formula.

◆ M() [2/4]

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

Construct an M formula.

◆ M() [3/4]

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

Construct an M formula.

◆ M() [4/4]

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

Construct an M formula.

◆ map()

template<typename Trans , typename... Args>
formula spot::formula::map ( Trans  trans,
Args &&...  args 
)
inline

◆ max()

unsigned spot::formula::max ( ) const
inline

Return end of the range for star-like operators.

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

◆ min()

unsigned spot::formula::min ( ) const
inline

Return start of the range for star-like operators.

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

◆ multop() [1/2]

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

Construct an n-ary operator.

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

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

◆ multop() [2/2]

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

Construct an n-ary operator.

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

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

◆ NegClosure() [1/2]

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

Construct a negated PSL Closure.

◆ NegClosure() [2/2]

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

Construct a negated PSL Closure.

◆ NegClosureMarked() [1/2]

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

Construct a marked negated PSL Closure.

◆ NegClosureMarked() [2/2]

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

Construct a marked negated PSL Closure.

◆ nested_unop_range()

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

Nested operator construction (syntactic sugar).

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

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

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

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

◆ Not() [1/2]

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

Construct a negation.

◆ Not() [2/2]

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

Construct a negation.

◆ one_star()

static formula spot::formula::one_star ( )
inlinestatic

Return a copy of the formula 1[*].

References spot::fnode::one_star().

◆ operator=()

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

Reset a formula to null.

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

◆ operator[]()

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

Return children number i.

◆ Or() [1/2]

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

Construct an Or formula.

◆ Or() [2/2]

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

Construct an Or formula.

◆ OrRat() [1/2]

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

Construct an Or SERE.

◆ OrRat() [2/2]

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

Construct an Or SERE.

◆ R() [1/4]

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

Construct an R formula.

◆ R() [2/4]

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

Construct an R formula.

◆ R() [3/4]

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

Construct an R formula.

◆ R() [4/4]

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

Construct an R formula.

◆ size()

unsigned spot::formula::size ( ) const
inline

Return the number of children.

◆ Star() [1/2]

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

Create SERE for f[*min..max]

◆ Star() [2/2]

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

Create SERE for f[*min..max]

◆ sugar_delay() [1/2]

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

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

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

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

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

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

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

◆ sugar_delay() [2/2]

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

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

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

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

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

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

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

◆ sugar_equal()

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

Create the SERE b[=min..max]

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

◆ sugar_goto()

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

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

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

◆ to_node_()

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

Return the underlying pointer to the formula.

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

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

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

◆ traverse()

template<typename Func , typename... Args>
void spot::formula::traverse ( Func  func,
Args &&...  args 
)
inline

Apply func to each subformula.

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

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

References traverse().

Referenced by traverse().

◆ tt()

static formula spot::formula::tt ( )
inlinestatic

Return the true constant.

References spot::fnode::tt().

◆ U() [1/4]

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

Construct a U formula.

◆ U() [2/4]

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

Construct a U formula.

◆ U() [3/4]

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

Construct a U formula.

◆ U() [4/4]

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

Construct a U formula.

◆ UConcat() [1/4]

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

Construct a []-> PSL formula.

◆ UConcat() [2/4]

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

Construct a []-> PSL formula.

◆ UConcat() [3/4]

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

Construct a []-> PSL formula.

◆ UConcat() [4/4]

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

Construct a []-> PSL formula.

◆ unbounded()

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

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

References spot::fnode::unbounded().

◆ unop() [1/2]

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

Build a unary operator.

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

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

◆ unop() [2/2]

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

Build a unary operator.

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

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

◆ W() [1/4]

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

Construct a W formula.

◆ W() [2/4]

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

Construct a W formula.

◆ W() [3/4]

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

Construct a W formula.

◆ W() [4/4]

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

Construct a W formula.

◆ X() [1/3]

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

Construct an X.

◆ X() [2/3]

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

Construct an X.

◆ X() [3/3]

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

Construct an X[n].

X[3]f = XXXf

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

◆ Xor() [1/4]

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

Construct an Xor formula.

◆ Xor() [2/4]

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

Construct an Xor formula.

◆ Xor() [3/4]

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

Construct an Xor formula.

◆ Xor() [4/4]

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

Construct an Xor formula.


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

Please direct any question, comment, or bug report to the Spot mailing list at spot@lrde.epita.fr.
Generated on Fri Feb 27 2015 10:00:07 for spot by doxygen 1.9.1