spot  2.3
 All Classes Files Functions Variables Typedefs Enumerations Enumerator Friends Modules Pages
Classes | Enumerations
Essential Temporal Logic Types

Classes

class  spot::formula
 Main class for temporal logic formula. More...
 
class  spot::formula::formula_child_iterator
 Allow iterating over children. More...
 

Enumerations

enum  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
}
 Operator types. More...
 

Detailed Description

Enumeration Type Documentation

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.

Next.

Eventually.

Globally.

Closure 

PSL Closure.

NegClosure 

Negated PSL Closure.

NegClosureMarked 

marked version of the Negated PSL Clusure

Xor 

Exclusive Or.

Implies 

Implication.

Equiv 

Equivalence.

until

release (dual of until)

weak until

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 

Fustion Star.


Please direct any question, comment, or bug report to the Spot mailing list at spot@lrde.epita.fr.
Generated on Thu Jan 19 2017 11:08:40 for spot by doxygen 1.8.8