Essential Temporal Logic Types

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

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

Detailed Description

Enumeration Type Documentation

op

enum class 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