Logo Search packages:      
Sourcecode: maria version File versions

StateReporter.h

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

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

# include "BitBuffer.h"

/** @file StateReporter.h
 * Interface for reporting successor states
 */

/* 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 */
00036 class StateReporter
{
public:
  /** Search kinds */
00040   enum SearchKind {
00041     Breadth,      ///< exhaustive breadth-first search
00042     Depth,  ///< exhaustive depth-first search
00043     Single  ///< process a single state
  };

  /** 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?
   */
  StateReporter (
# 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);
  /** Copy constructor */
  StateReporter (const class StateReporter& old);
private:
  /** Assignment operator */
  class StateReporter& operator= (const class StateReportert& other);
public:
  /** Destructor */
  virtual ~StateReporter ();

  /** Get the number of errors that have been reported */
00075   unsigned getNumErrors () const { return myNumErrors; }
  /** Get the number of local states generated in modular analysis */
00077   unsigned getNumLocal () const { return myNumLocal; }

  /** Get the minimum length of state vectors */
00080   size_t getMinSize () const { return myMinSize; }
  /** Get the maximum length of state vectors */
00082   size_t getMaxSize () const { return myMaxSize; }
  /** Get the transition enabledness sets */
00084   const char* getEnabled () const { return myEnabled; }
  /** Determine if the flattened net is being considered */
00086   bool isFlattened () const { return myFlattened; }

  /** Determine whether this is a reduced state space */
00089   bool isReduced () const { return !!myLocal; }

  /** Note an enabled transition
   * @param transition  the transition
   */
  void enabled (const class Transition& transition);

# ifdef EXPR_COMPILE
protected:
  /** Analyze the successors of a transition
   * @param transition  the transition
   */
  void analyze (const class Transition& transition);
public:
  /** Report a successor state
   * @param buf         the encoded state
   * @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?
   * @param tr          the index of the transition that fired
   */
  void addState (const void* buf, size_t size,
             bool rejected, bool hidden, unsigned tr);
# endif // EXPR_COMPILE

  /** Search the state space
   * @param kind  Type of search
   */
  void analyze (enum SearchKind kind);

private:
  /** Search the state space of the flattened net
   * @param kind  Type of search
   */
  void analyzeFlattened (enum SearchKind kind);

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

protected:
  /** Initialize the state spaces of the modules
   * @return            the state spaces of the modules, or 0 if not modular
   */
  class FullSet* initModules () const;
  /** Search the state spaces of the modules
   * @param m           the source marking
   * @param sync  the synchronisation states
   * @param childset    the state spaces of the modules
   */
  void analyzeModules (const class GlobalMarking& m,
                   class SyncStates& sync,
                   class FullSet* childset);
# ifdef EXPR_COMPILE
  /** Search the state spaces of the modules
   * @param sync  the synchronisation states
   * @param childset    the state spaces of the modules
   */
  void analyzeModules (class SyncStates& sync,
                   class FullSet* childset);

public:
  /** Generate the successors of a synchronisation transition
   * @param transition  the transition
   */
  void sync (const class Transition& transition);
protected:
# endif // EXPR_COMPILE
  /** Determine if a state can be suppressed */
  bool suppress ();

public:
  /** Report a successor state
   * @param transition  the transition fired
   * @param valuation   the binding of the transition
   * @param marking     the resulting marking
   * @return            true if analysis should proceed; false on fatal error
   */
  bool report (const class Transition& transition,
             const class Valuation& valuation,
             const class GlobalMarking& marking);

  /** Report a synchronisation state
   * @param transition  the synchronisation transition
   */
  void reportSync (const class Transition& transition);

  /** Set the synchronisation source state (called by SyncStates)
   * @param src         the encoded source state
   * @param size  length of the encoded state in bytes
   */
00181   void setSyncSource (word_t* src, size_t size) {
    delete[] mySrc; mySrc = src; mySrcSize = size;
  }

protected:
  /** Report an error
   * @return            true when the maximum amount of errors has been reached
   */
00189   bool error () { return ++myNumErrors == myMaxErrors; }

  /** Add an encoded state to the state space (called by report ())
   * @param state the encoded state
   * @param size  length of the encoded state in bytes
   * @param hidden      flag: is the transition to the state hidden?
   * @return            true if the state was new
   */
  bool addState (const void* state,
             size_t size,
             bool hidden);

  /** Fetch an encoded state
   * @param tail  flag: retrieve from tail of list instead of head
   * @return            the encoded state (mySrc), or NULL if none available
   */
  word_t* popState (bool tail);

  /** Inflate the source state buffer */
00208   void inflate () {
    BitPacker::inflate (mySrc[(mySrcSize - 1) / sizeof (word_t)],
                  (-mySrcSize) % sizeof (word_t));
  }
  /** Deflate the source state buffer */
00213   void deflate () {
    BitPacker::deflate (mySrc[(mySrcSize - 1) / sizeof (word_t)],
                  (-mySrcSize) % sizeof (word_t));
  }

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
   */
  virtual bool do_addState (const void* state,
                      size_t size) = 0;

  /** 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
   */
  virtual word_t* do_popState (bool tail, size_t& size) = 0;

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

# 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
   */
  virtual bool popCompiled (bool breadth) = 0;

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

  /** Add all events from the current source state to the graph */
  virtual 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
   */
  virtual bool report (const class Transition& transition,
                   const class Valuation& valuation,
                   const class GlobalMarking& marking,
                   bool rejected) = 0;

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

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
   */
  virtual bool report (const void* state,
                   size_t size,
                   bool rejected,
                   bool hidden) = 0;
# endif // EXPR_COMPILE

  /** Report an inconsistent successor state
   * @param transition  the transition fired
   * @param valuation   the binding of the transition
   * @param marking     the resulting marking
   * @param reason      reason for failure (optional)
   * @param place the place whose marking could not be encoded (optional)
   */
  void reject (const class Transition& transition,
             const class Valuation& valuation,
             const class GlobalMarking& marking,
             const char* reason,
             const class Place* place);

  /** Determine whether a fatal condition has occurred */
00300   bool isFatal () const { return myFatal; }
  /** Flag a fatal condition */
00302   void flagFatal () { myFatal = true; }

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

public:
# ifdef EXPR_COMPILE
  /** The compiled model */
  const class Compilation* const myCompilation;
# endif // EXPR_COMPILE
  /** The net being analyzed */
00314   const class Net& net;
  /** Printer object for diagnostics */
00316   const class Printer& printer;
private:
  /** Maximum allowed number of errors (0=infinite) */
00319   const unsigned myMaxErrors;
  /** Number of errors that have occurred */
00321   unsigned myNumErrors;
  /** Number of local states generated in modular analysis */
00323   unsigned myNumLocal;
  /** Log of enabledness set occurrences (optional) */
00325   char* const myEnabled;
protected:
  /** Synchronisation states for modular analysis (optional) */
00328   class SyncStates* mySync;
  /** Flag: has a fatal condition occurred? */
00330   bool myFatal;
  /** Flag: is the source state a deadlock? */
00332   bool mySrcDeadlock;
  /** Priority level of the last fired transition */
00334   unsigned myPriority;
  /** Encoder for states */
00336   class BitPacker myStateBuf;
  /** The encoded state that is being analyzed */
00338   word_t* mySrc;
  /** Length of mySrc, in bytes */ 
00340   size_t mySrcSize;
private:
  /** Flag: apply search on flattened state space? */
00343   const bool myFlattened;
  /** Set of local (transient, invisible) states */
00345   class FullSet* const myLocal;
  /** Suppressed states (when applying path compression) */
00347   class States* const mySuppressed;
  /** Flag: how many successors does the state have (in path compression) */
  enum { None = 0, One, Many } mySuccessors;
  /** Minimum length of encoded state vectors */
00351   size_t myMinSize;
  /** Maximum length of encoded state vectors */
00353   size_t myMaxSize;
};

#endif // STATEREPORTER_H_

Generated by  Doxygen 1.6.0   Back to index