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

LtlGraph Class Reference

#include <LtlGraph.h>

List of all members.

Detailed Description

Graph representation of a generalized Büchi automaton corresponding to an LTL formula

A LtlGraph is automatically constructed from a given Ltl formula. All relevant information is fully stored to the graph, so that the formula itself may well be destoyed right after the conversion. The Ltl operators/operands provide themselves the knowledge of how to be expanded into a LtlGraph.

Definition at line 89 of file LtlGraph.h.

Public Types

typedef Map::const_iterator const_iterator
 Constant iterator to the map.
typedef Map::iterator iterator
 Iterator to the map.
typedef std::map< unsigned,
class LtlGraphNode
 Map from state numbers to graph nodes.

Public Member Functions

 LtlGraph (const class Ltl &formula)
 Constructs a graph from a given LTL formula.
 ~LtlGraph ()
Accessors to the graph nodes

const_iterator begin () const
const_iterator end () const

Private Member Functions

 LtlGraph (const class LtlGraph &old)
 Copy constructor.
class LtlGraphoperator= (const class LtlGraph &other)
 Assignment operator.

Private Attributes

unsigned m_next
 Next available state number.
std::map< unsigned, class
 Map from state numbers to graph nodes (0=initial state).

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

Generated by  Doxygen 1.6.0   Back to index