// -*- 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 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the * 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 { public: /// 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) {} private: /// Assignment operator class LtlGraphNode& operator= (const class LtlGraphNode& node); public: /// 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 { public: /*@{*/ /// 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; /*@}*/ private: /// 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; private: /// Copy constructor LtlGraph (const class LtlGraph& old); /// Assignment operator class LtlGraph& operator= (const class LtlGraph& other); public: /// 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