Logo Search packages:      
Sourcecode: maria version File versions

GraphReporter.h

Go to the documentation of this file.
// Reporting successor states in graph-based analysis -*- c++ -*-

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

# include "StateReporter.h"
# include "Search.h"

/** @file GraphReporter.h
 * Interface for reporting successor states in graph-based analysis
 */

/* Copyright © 2002-2003 Marko Mäkelä (msmakela@tcs.hut.fi).

   This file is part of MARIA, a reachability analyzer and model checker
   for high-level Petri nets.

   MARIA 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, or (at your option)
   any later version.

   MARIA 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.

   The GNU General Public License is often shipped with GNU software, and
   is generally kept in a file called COPYING or LICENSE.  If you do not
   have a copy of the license, write to the Free Software Foundation,
   59 Temple Place, Suite 330, Boston, MA 02111 USA. */

/** Reporting successor states in graph-based analysis */
00037 class GraphReporter : public StateReporter
{
public:
  /** Constructor
   * @param compilation the compiled model (optional)
   * @param net_  the net that is being analysed
   * @param printer_    printer object for diagnostic output
   * @param maxerrors   maximum number of allowed errors (0=infinity)
   * @param compress    flag: collapse deterministic sequences?
   * @param local flag: suppress transient (invisible) states?
   * @param flattened   flag: consider the flattened net?
   * @param threshold   threshold for reporting state space statistics
   * @param graph the reachability graph being generated
   */
  GraphReporter (
#ifdef EXPR_COMPILE
             const class Compilation* compilation,
#endif // EXPR_COMPILE
             const class Net& net_,
             const class Printer& printer_,
             unsigned maxerrors,
             bool compress,
             bool local,
             bool flattened,
             unsigned threshold,
             class Graph& graph);
private:
  /** Copy constructor */
  GraphReporter (const class GraphReporter& old);
  /** Assignment operator */
  class GraphReporter& operator= (const class GraphReporter& other);
public:
  /** Destructor */
  ~GraphReporter ();

  /** Get a reference to the reachability graph */
00073   const class Graph& getGraph () const { return myGraph; }
  /** Get the graph of strongly connected components */
00075   const class ComponentGraph* getComponents () const { return myComponents; }
  /** Get a GraphReporter by module
   * @param path  amount and indexes of path components (subnets)
   */
  class GraphReporter& getChild (const unsigned* path);
  /** Get a GraphReporter by module
   * @param path  amount and indexes of path components (subnets)
   */
00083   const class GraphReporter& getChild (const unsigned* path) const {
    return const_cast<class GraphReporter*>(this)->getChild (path);
  }

  /** Compute the strongly connected components for this graph
   * @param state start state of the search
   * @param cond  condition for exploring states (NULL=true)
   * @return            number of strongly connected components (0=fail)
   */
  unsigned strong (card_t state,
               const class Expression* cond);

  /** Initialize the search list
   * @param state the state to be analyzed
   */
00098   void init (card_t state) {
    assert (myStates.empty ()); myStates.push (state);
  }
  /** Assign the addOld flag */
00102   void setAddOld (bool addOld) { myAddOld = addOld; }

  /** Retrieve the successors of a state
   * @param state the state to be analyzed
   * @return            the successors of the state (must be cleared by caller)
   */
  class SearchList& getSuccessors (card_t state);

  /** Analyze an anonymous transition
   * @param transition  the transition
   * @return            the successor states (must be cleared by caller)
   */
  class SearchList& getSuccessors (const class Transition& transition);

  /** Prepare for computing the enabled fairness sets
   * @param state the state to be analyzed
   * @param buf         (output) the encoded event labels (deleted by caller)
   * @param u           (output) the bit unpacker object (deleted by caller)
   * @return            the successors of the state (deleted by caller)
   */
  card_t* prepareFair (card_t state,
                   word_t*& buf,
                   class BitUnpacker*& u);

  /** Compute the enabled fairness sets
   * @param state the state being analyzed (for diagnostics)
   * @param u           the bit unpacker object from prepareFair ()
   * @param strong      (output) the enabled strong fairness sets (optional)
   *              (static allocation; not deleted by caller)
   * @return            amount and numbers of enabled weak fairness sets
   *              (static allocation; not deleted by caller)
   */
  unsigned* computeFair (card_t state,
                   class BitUnpacker* u,
                   unsigned** strong);

  /** Evaluate the gates of a property automaton
   * @param state the state number of the reachability graph
   * @param prop  the state number of the property automaton
   * @param ps          current state in the property automaton
   * @return            the amount and numbers of enabled successor states
   */
  const unsigned* eval (card_t state,
                  unsigned prop,
                  const class PropertyState& ps);
  /** Finish evaluating the gates of a property automaton
   * @param enabled     an array of enabled states returned by eval ()
   */
#ifdef EXPR_COMPILE
  void eval_done (const unsigned* enabled) const
#else
00153   static void eval_done (const unsigned* enabled)
#endif // EXPR_COMPILE
  {
#ifdef EXPR_COMPILE
    if (!myCompilation)
#endif // EXPR_COMPILE
      delete[] enabled;
  }

  /** Search the state space in a modular way
   * @param kind  Type of search
   */
  void analyzeModular (enum SearchKind kind);

private:
  /** Add an encoded state to the state space
   * @param state the encoded state
   * @param size  length of the encoded state in bytes
   * @return            true if the state was new
   */
  bool do_addState (const void* state,
                size_t size);

  /** Add an encoded state to the state space, but do not enqueue it
   * @param state the encoded state
   * @param size  length of the encoded state in bytes
   * @return            true if the state was new
   */
  bool do_addStateOnly (const void* state,
                  size_t size);

  /** Fetch an encoded state
   * @param tail  flag: retrieve from tail of list instead of head
   * @param size  (output) length of the encoded stream
   * @return            the encoded state, or NULL if none available
   */
  word_t* do_popState (bool tail, size_t& size);

  /** Dequeue an unprocessed state
   * @param breadth     true=dequeue (FIFO, queue), false=pop (LIFO, stack)
   * @return            an unprocessed state, or NULL if all processed
   */
  class GlobalMarking* pop (bool breadth);

#ifdef EXPR_COMPILE
  /** Dequeue an unprocessed state
   * @param breadth     true=dequeue (FIFO, queue), false=pop (LIFO, stack)
   * @return            true if a state was found, or false if all processed
   */
  bool popCompiled (bool breadth);

  /** Determine whether arcs should be generated */
  bool isGraph () const { return true; }
#endif // EXPR_COMPILE

  /** Add all events from the current source state to the graph */
  void addEvents ();

  /** Report a successor state
   * @param transition  the transition fired
   * @param valuation   the binding of the transition
   * @param marking     the resulting marking
   * @param rejected    flag: is the state rejected?
   * @return            true if the state was new
   */
  bool report (const class Transition& transition,
             const class Valuation& valuation,
             const class GlobalMarking& marking,
             bool rejected);

  /** Report a deadlock or an error in the current state
   * @param deadlock    flag: is this a deadlock?
   */
  void reportError (bool deadlock);

public:
#ifdef EXPR_COMPILE
  /** Report a successor state
   * @param state the resulting encoded deflated state (mandatory)
   * @param size  length of the encoded state, in bytes
   * @param rejected    flag: is the state rejected?
   * @param hidden      flag: is the transition to the state hidden?
   * @return            true if the state was new
   */
  bool report (const void* state,
             size_t size,
             bool rejected,
             bool hidden);
#endif // EXPR_COMPILE

private:
  /** Report an inconsistent successor state */
  void reject ();

public:
  /** Display a state number
   * @param m           the state (to be decomposed into module states)
   * @param state the state number
   * @param out         the output stream
   */
  void printState (const class GlobalMarking& m,
               card_t state,
               const class Printer& out);

private:
  /** Threshold for reporting intermediate statistics */
00259   const unsigned myThreshold;
  /** The reachability graph being constructed */
00261   class Graph& myGraph;
  /** Graph of strongly connected components (optional) */
00263   class ComponentGraph* myComponents;
  /** GraphReporters for modules (only for non-flattened analysis) */
00265   class GraphReporter** const myChildren;
  /** Table for keeping track of visited states in non-flattened analysis */
00267   class BitVector* myVisited;
  /** Buffer for encoding events */
00269   class BitPacker myEventBuf;
  /** List of unprocessed states */
00271   class SearchList myStates;
  /** Number of the state being analyzed */
00273   card_t myStateNum;
  /** Number of the state last generated (set by do_addState) */
00275   card_t myTargetNum;
  /** Flag: is myStateNum being revisited? */
00277   bool myProcessed;
  /** Work area for computing enabled weak fairness sets */
00279   unsigned* myWeaklyFair;
  /** Work area for computing enabled strong fairness sets */
00281   unsigned* myStronglyFair;
  /** Flag: add also existing states to the state list */
00283   bool myAddOld;
};

#endif // GRAPHREPORTER_H_

Generated by  Doxygen 1.6.0   Back to index