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

LtlUntil Class Reference

#include <Ltl.h>

Inheritance diagram for LtlUntil:


List of all members.

Detailed Description

LTL 'until' and 'release' operators

Definition at line 502 of file Ltl.h.

Public Types

enum  Kind {
  Atom, Constant, Junct, Iff,
  Future, Until
 Formula kinds.

Public Member Functions

void expand (class LtlGraphNode &node, std::stack< class LtlGraphNode * > &to_expand) const
enum Kind getKind () const
 Determine the kind of the formula.
class LtlgetLeft () const
 Get the left-hand-side subformula.
class LtlgetRight () const
 Get the right-hand-side subformula.
bool isRelease () const
 Determine whether this is a release operator instead of until.
class LtlnegClone () const
 Returns a clone of the negation of this Ltl formula.
bool operator< (const class Ltl &other) const
 Less-than comparison.
bool operator< (const class LtlUntil &other) const
 Less-than comparison.
 ~LtlUntil ()

Static Public Member Functions

static class Ltlconstruct (bool release, class Ltl &l, class Ltl &r)
static class Ltlfetch (unsigned f)

Public Attributes

unsigned m_num
 Number of the LTL formula.

Static Protected Member Functions

static class Ltlinsert (class Ltl &ltl)

Private Member Functions

 LtlUntil (const class LtlUntil &old)
 Copy constructor.
 LtlUntil (bool release, class Ltl &l, class Ltl &r)
class LtlUntiloperator= (const class LtlUntil &old)
 Assignment operator.

Private Attributes

class Ltlm_left
 The left-hand-side sub-formula.
bool m_release
 Flag: release instead of until.
class Ltlm_right
 The right-hand-side sub-formula.

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

Generated by  Doxygen 1.6.0   Back to index