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

LtlGraphNode Class Reference

#include <LtlGraph.h>

List of all members.


Detailed Description

A node in a graph representing an LTL formula.

The graph itself is a set of nodes of this kind. The LtlGraphNode class is merely a front end for the set representation.

Definition at line 41 of file LtlGraph.h.


Public Member Functions

 LtlGraphNode (const class LtlGraphNode &node)
 Copy constructor.
 LtlGraphNode (const std::set< unsigned > &incoming, const class BitVector &neww, const class BitVector &old, const class BitVector &atomic, const class BitVector &next)
 Constructs a specific node.
 LtlGraphNode ()
 Default constructor.
 ~LtlGraphNode ()
 Destructor.

Public Attributes

class BitVector m_atomic
 A set of atomic propositions that must hold, when this node is entered.
std::set< unsigned > m_incoming
 From which nodes can one come to this node.
class BitVector m_new
 A set of formulae to be processed.
class BitVector m_next
 A set of formulae that must hold in immediate next nodes.
class BitVector m_old
 A set of formulae that must hold, when this node is entered.

Private Member Functions

class LtlGraphNodeoperator= (const class LtlGraphNode &node)
 Assignment operator.

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

Generated by  Doxygen 1.6.0   Back to index