Logo Search packages:      
Sourcecode: lbt version File versions  Download package

LtlFuture Class Reference

#include <Ltl.h>

Inheritance diagram for LtlFuture:


List of all members.

Detailed Description

LTL next-time, globally and finally formulae

Definition at line 414 of file Ltl.h.

Public Types

enum  Kind {
  Atom, Constant, Junct, Iff,
  Future, Until
 Formula kinds.
enum  Op { next, globally, finally }
 Operator kinds.

Public Member Functions

void expand (class LtlGraphNode &node, std::stack< class LtlGraphNode * > &to_expand) const
class LtlgetFormula () const
 Get the subformula.
enum Kind getKind () const
 Determine the kind of the formula.
enum Op getOp () const
 Get the temporal operator.
class LtlnegClone () const
 Returns a clone of the negation of this formula.
bool operator< (const class Ltl &other) const
 Less-than comparison.
bool operator< (const class LtlFuture &other) const
 Less-than comparison.

Static Public Member Functions

static class Ltlconstruct (enum Op op, class Ltl &f)
static class Ltlfetch (unsigned f)

Public Attributes

unsigned m_num
 Number of the LTL formula.

Protected Member Functions

 ~LtlFuture ()

Static Protected Member Functions

static class Ltlinsert (class Ltl &ltl)

Private Member Functions

 LtlFuture (const class LtlFuture &old)
 Copy constructor.
 LtlFuture (enum Op op, class Ltl &f)
class LtlFutureoperator= (const class LtlFuture &old)
 Assignment operator.

Private Attributes

class Ltlm_formula
 The formula being quantified.
enum Op m_op
 The operator.

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

Generated by  Doxygen 1.6.0   Back to index