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

LtlAtom Class Reference

#include <Ltl.h>

Inheritance diagram for LtlAtom:

Ltl

List of all members.


Detailed Description

LTL atom

Definition at line 130 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.
unsigned getValue () const
 Determine the value of the proposition.
bool isNegated () const
 Determine whether the atom is negated.
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 LtlAtom &other) const
 Less-than comparison.

Static Public Member Functions

static class Ltlconstruct (unsigned value, bool negated)
static class Ltlfetch (unsigned f)

Public Attributes

unsigned m_num
 Number of the LTL formula.

Protected Member Functions

 ~LtlAtom ()
 Destructor.

Static Protected Member Functions

static class Ltlinsert (class Ltl &ltl)

Private Member Functions

 LtlAtom (const class LtlAtom &old)
 Copy constructor.
 LtlAtom (unsigned value, bool negated=false)
 Constructor.
class LtlAtomoperator= (const class LtlAtom &old)
 Assignment operator.

Private Attributes

bool m_negated
 Flag: is the proposition negated?
unsigned m_value
 The proposition number.

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

Generated by  Doxygen 1.6.0   Back to index