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

LtlJunct Class Reference

#include <Ltl.h>

Inheritance diagram for LtlJunct:

Ltl

List of all members.


Detailed Description

LTL conjunction and disjunction

Definition at line 244 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 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 LtlJunct &other) const
 Less-than comparison.

Static Public Member Functions

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

Public Attributes

unsigned m_num
 Number of the LTL formula.

Protected Member Functions

 ~LtlJunct ()
 Destructor.

Static Protected Member Functions

static class Ltlinsert (class Ltl &ltl)

Private Member Functions

 LtlJunct (const class LtlJunct &old)
 Copy constructor.
 LtlJunct (bool con, class Ltl &l, class Ltl &r)
class LtlJunctoperator= (const class LtlJunct &old)
 Assignment operator.

Private Attributes

bool m_con
 Flag: conjunction instead of disjunction?
class Ltlm_left
 The left-hand-side sub-formula.
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