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


Go to the documentation of this file.
// -*- c++ -*-
/// @file LtlGraph.h
 * This file is based on code originally written by Mauno Rönkkö,
 * Copyright © 1998 Mauno Rönkkö <mronkko@abo.fi>.
 * Modifications by Heikki Tauriainen <Heikki.Tauriainen@hut.fi>
 * and Marko Mäkelä <Marko.Makela@hut.fi>.
 * This program is free software; you can redistribute it and/or modify
 * it under the terms of the GNU General Public License as published by
 * the Free Software Foundation; either version 2 of the License, or
 * (at your option) any later version.
 * This program is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * GNU General Public License for more details.
 * You should have received a copy of the GNU General Public License
 * along with this program; if not, write to the Free Software
 * Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA.

#ifndef LtlGraph_h_
# define LtlGraph_h_
# ifdef __GNUC__
#  pragma interface
# endif // __GNUC__

# include "Ltl.h"
# include "BitVector.h"
# include <map>

 * 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.
00041 class LtlGraphNode
  /// From which nodes can one come to this node.
00045   std::set<unsigned> m_incoming;
  /// A set of formulae to be processed.
00047   class BitVector m_new;
  /// A set of formulae that must hold, when this node is entered.
00049   class BitVector m_old;
  /// A set of atomic propositions that must hold, when this node is entered.
00051   class BitVector m_atomic;
  /// A set of formulae that must hold in immediate next nodes.
00053   class BitVector m_next;

  /// Default constructor
00056   LtlGraphNode () :
    m_incoming (), m_new (), m_old (), m_atomic (), m_next () {}

  /// Constructs a specific node.
00060   LtlGraphNode (const std::set<unsigned>& incoming,
            const class BitVector& neww,
            const class BitVector& old,
            const class BitVector& atomic,
            const class BitVector& next) :
    m_incoming (incoming), m_new (neww), m_old (old),
    m_atomic (atomic), m_next (next) {}
  /// Copy constructor
00068   LtlGraphNode (const class LtlGraphNode& node) :
    m_incoming (node.m_incoming), m_new (node.m_new),
    m_old (node.m_old), m_atomic (node.m_atomic), m_next (node.m_next) {}
  /// Assignment operator
  class LtlGraphNode& operator= (const class LtlGraphNode& node);
  /// Destructor
00076   ~LtlGraphNode () {}

 * 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.
00089 class LtlGraph
  /// Map from state numbers to graph nodes
00094   typedef std::map<unsigned,class LtlGraphNode> Map;
  /// Iterator to the map
00096   typedef Map::iterator iterator;
  /// Constant iterator to the map
00098   typedef Map::const_iterator const_iterator;
  /// Next available state number
00102   unsigned m_next;

  /// Map from state numbers to graph nodes (0=initial state)
00105   std::map<unsigned,class LtlGraphNode> m_nodes;

  /// Copy constructor
  LtlGraph (const class LtlGraph& old);
  /// Assignment operator
  class LtlGraph& operator= (const class LtlGraph& other);
  /// Constructs a graph from a given LTL formula.
  LtlGraph (const class Ltl& formula);

  /// Destructor
00117   ~LtlGraph () {}

  /** @name Accessors to the graph nodes */
  const_iterator begin () const { return m_nodes.begin (); }
  const_iterator end () const { return m_nodes.end (); }

#endif // LtlGraph_h_

Generated by  Doxygen 1.6.0   Back to index