Essential Temporal Logic Types

Classes
class	spot::formula
	Main class for temporal logic formula. More...

Enumerations
enum class	spot::op : uint8_t {   spot::ff , spot::tt , spot::eword , spot::ap ,   spot::Not , spot::X , spot::F , spot::G ,   spot::Closure , spot::NegClosure , spot::NegClosureMarked , spot::Xor ,   spot::Implies , spot::Equiv , spot::U , spot::R ,   spot::W , spot::M , spot::EConcat , spot::EConcatMarked ,   spot::UConcat , spot::Or , spot::OrRat , spot::And ,   spot::AndRat , spot::AndNLM , spot::Concat , spot::Fusion ,   spot::Star , spot::FStar , spot::first_match , spot::strong_X ,   spot::exists , spot::forall }
	Operator types. More...

Detailed Description

Enumeration Type Documentation

op

enum spot::op : uint8_t

strong

#include <spot/tl/formula.hh>

Operator types.

Enumerator
ff	False.
tt	True.
eword	Empty word.
ap	Atomic proposition.
Not	Negation.
X	Next.
F	Eventually.
G	Globally.
Closure	PSL Closure.
NegClosure	Negated PSL Closure.
NegClosureMarked	marked version of the Negated PSL Closure
Xor	Exclusive Or.
Implies	Implication.
Equiv	Equivalence.
U	until
R	release (dual of until)
W	weak until
M	strong release (dual of weak until)
EConcat	Seq.
EConcatMarked	Seq, Marked.
UConcat	Triggers.
Or	(omega-Rational) Or
OrRat	Rational Or.
And	(omega-Rational) And
AndRat	Rational And.
AndNLM	Non-Length-Matching Rational-And.
Concat	Concatenation.
Fusion	Fusion.
Star	Star.
FStar	Fusion Star.
first_match	first_match(sere)
strong_X	strong Next
exists	existential quantification of AP
forall	universal quantification of AP