Logo Search packages:      
Sourcecode: maria version File versions

StateSetReporter.C

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

/** @file StateSetReporter.C
 * Interface for reporting successor states in safety property 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. */

#ifdef __GNUC__
# pragma implementation
#endif // __GNUC__
#include "StateSetReporter.h"
#include "FullSet.h"
#include "SyncStates.h"
#include "Net.h"
#include "Transition.h"
#include "Valuation.h"
#include "GlobalMarking.h"
#include "Property.h"
#include "Printer.h"
#include "Dotty.h"

00041 StateSetReporter::StateSetReporter (
#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,
                            const class Dotty* dotty,
                            bool merge,
                            class StateSet& states,
                            const class Property* prop) :
  StateReporter (
#ifdef EXPR_COMPILE
             compilation,
#endif // EXPR_COMPILE
             net_, printer_, maxerrors, compress, local, flattened),
  myThreshold (threshold),
  myDotty (dotty), myMerge (merge), myUpdate (true),
  myDest (0), myDestSize (0),
  myStates (states),
  myProp (prop), myPropBits (prop ? log2 (prop->getNumStates ()) : 0),
  myPropSucc (0), myPropReject (false)
{
}

00070 StateSetReporter::StateSetReporter (const class StateSetReporter& old,
                            bool update,
                            class StateSet& states,
                            const word_t* dest,
                            unsigned destsize) :
  StateReporter (
#ifdef EXPR_COMPILE
             old.myCompilation,
#endif // EXPR_COMPILE
             old.net, old.printer, 1, false, false, old.isFlattened ()),
  myThreshold (0),
  myDotty (old.myDotty), myMerge (old.myMerge), myUpdate (update),
  myDest (dest), myDestSize (destsize),
  myStates (states), myProp (old.myProp), myPropBits (old.myPropBits),
  myPropSucc (0), myPropReject (false)
{
}

00088 StateSetReporter::StateSetReporter (const class StateSetReporter& old,
                            class StateSet& states) :
  StateReporter (old),
  myThreshold (0),
  myDotty (old.myDotty), myMerge (old.myMerge), myUpdate (true),
  myDest (0), myDestSize (0), myStates (states),
  myProp (old.myProp), myPropBits (old.myPropBits),
  myPropSucc (0), myPropReject (false)
{
}

00099 StateSetReporter::~StateSetReporter ()
{
  delete[] myPropSucc;
}

void
00105 StateSetReporter::displayPrologue () const
{
  if (myDotty)
    myDotty->displayPrologue (myMerge);
}

void
00112 StateSetReporter::displayEpilogue () const
{
  if (myDotty)
    myDotty->displayEpilogue ();
}

void
00119 StateSetReporter::displayMarking (const class GlobalMarking& m) const
{
  if (myDotty)
    myDotty->displayMarking (m);
  else
    m.display (printer), printer.finish ();
}

void
00128 StateSetReporter::displayState (const word_t* s) const
{
  class GlobalMarking m (net);
  m.decode (*net.getInitMarking (), s, myPropBits);
  displayMarking (m);
}

void
00136 StateSetReporter::displayPath (const word_t* src,
                         const word_t* dest,
                         unsigned destsize) const
{
  class StateSetReporter reporter (*this, false, myStates, dest, destsize);
  reporter.displayPath (src);
}

bool
00145 StateSetReporter::do_addState (const void* state,
                         size_t size)
{
  return myStates.add (state, size);
}

word_t*
00152 StateSetReporter::do_popState (bool tail,
                         size_t& size)
{
  return myStates.pop (tail, size);
}

class GlobalMarking*
00159 StateSetReporter::pop (bool breadth)
{
  delete[] myPropSucc;
  myPropSucc = 0;
  while (popState (breadth)) {
    inflate ();
    class GlobalMarking* m = new class GlobalMarking (net);
    const unsigned ps = m->decode (*net.getInitMarking (), mySrc, myPropBits);
    if (myProp) {
      class Valuation valuation;
      valuation.setGlobalMarking (m);
      myPropReject = !(*myProp)[ps].eval (valuation, myPropSucc,
                                myProp->getFinalState ());
      if (myPropReject && !valuation.isOK ()) {
      printer.printRaw ("property ");
      printer.print (ps);
      printer.printRaw (" evaluation error");
      printer.finish ();
      flagFatal ();
      if (!myDest)
        myStates.reject (mySrc, mySrcSize, *this,
                     StateSet::propertyError, isReduced ());
      delete[] myPropSucc;
      myPropSucc = 0;
      delete m;
      return 0;
      }
      else if (!*myPropSucc) {
      delete[] myPropSucc;
      myPropSucc = 0;
      delete m;
      continue;
      }
    }
    return m;
  }
  return 0;
}

#ifdef EXPR_COMPILE
# include "Compilation.h"

bool
StateSetReporter::popCompiled (bool breadth)
{
  assert (!!myCompilation);
  delete[] myPropSucc;
  myPropSucc = 0;
  while (popState (breadth)) {
    myCompilation->stateDecode (net.getIndex (), mySrc, mySrcSize);
    if (myProp) {
      const unsigned ps = *myCompilation->getPropSucc ();
      enum Error err = myCompilation->propEval (ps);
      myPropReject = err == errComp;
      if (err && err != errComp) {
      printer.printRaw ("property ");
      printer.print (ps);
      printer.printRaw (" evaluation error");
      printer.finish ();
      flagFatal ();
      if (!myDest)
        myStates.reject (mySrc, mySrcSize, *this,
                     StateSet::propertyError, isReduced ());
      delete[] myPropSucc;
      myPropSucc = 0;
      return false;
      }
      else if (!*myCompilation->getPropSucc ()) {
      continue;
      }
    }
    return true;
  }
  return false;
}
#endif // EXPR_COMPILE

void
00237 StateSetReporter::addEvents ()
{
  delete[] myPropSucc;
  myPropSucc = 0;
}

bool
00244 StateSetReporter::report (const class Transition& transition,
                    const class Valuation& valuation,
                    const class GlobalMarking& marking,
                    bool rejected)
{
  /** flag: is the state new? */
  bool isNew = false;
  if (myPropReject)
    rejected = true;
  const unsigned* p = myPropBits ? (myPropSucc + *myPropSucc) : 0;
  do {
    if (myPropBits)
      myStateBuf.append (*p, myPropBits);
    if (myDest) {
      if (myDestSize == myStateBuf.getNumWords () &&
        !memcmp (myDest, myStateBuf.getBuf (),
               sizeof (word_t) * myDestSize)) {
      if (myDotty)
        myDotty->displayEdge (transition, valuation, marking);
      else
        transition.displayEdge (valuation, marking, printer);
      flagFatal ();
      return true;
      }
    }
    if (!myDest || myUpdate) {
      myStateBuf.deflate ();
      if (report (myStateBuf.getBuf (), myStateBuf.getNumBytes (),
              rejected, transition.isHidden (valuation), 0))
      isNew = true;
      myStateBuf.inflate ();
    }
    if (!myPropBits)
      break;
    myStateBuf.remove (myPropBits);
  }
  while (--p > myPropSucc);

  return isNew;
}

void
00286 StateSetReporter::reportError (bool deadlock)
{
  if (myDest)
    return; // reproducing a counterexample, not reporting an error
  deflate ();
  myStates.reject (mySrc, mySrcSize, *this, myFatal
               ? (deadlock
                  ? StateSet::deadlockFatal
                  : StateSet::rejectFatal)
               : (deadlock
                  ? StateSet::deadlockState
                  : StateSet::rejectState),
               isReduced ());
  inflate ();
  if (error ())
    flagFatal ();
}

#ifdef EXPR_COMPILE
bool
StateSetReporter::report (const void* state,
                    size_t size,
                    bool rejected,
                    bool hidden)
{
  return report (state, size, rejected, hidden, 0);
}
#endif // EXPR_COMPILE

bool
00316 StateSetReporter::report (const void* state,
                    size_t size,
                    bool rejected,
                    bool hidden,
                    unsigned pending)
{
  if (rejected || myPropReject) {
    if (!myDest) {
      myStates.reject (state, size, *this, myFatal
                   ? StateSet::rejectFatal
                   : StateSet::rejectState,
                   isReduced ());
      if (error ())
      flagFatal ();
    }
    return true;
  }
  bool status = addState (state, size, hidden);
  if (myThreshold) {
    const unsigned numArcs = myStates.getNumArcs ();
    if (!(numArcs % myThreshold)) {
      const unsigned numStates = myStates.getNumStates ();
      printer.print (numStates), printer.printRaw (" states, ");
      printer.print (numArcs), printer.printRaw (" arcs, ");
      printer.print (myStates.getNumPending ());
      if (pending)
      printer.delimiter ('+'), printer.print (pending);
      printer.printRaw (" pending");
      printer.finish ();
    }
  }
  return status;
}

void
00351 StateSetReporter::reject (const void* dstate,
                    size_t dlen,
                    long offset,
                    bool reduced,
                    unsigned reason)
{
  myStates.setOffset (offset);
  myStates.reject (dstate, dlen, *this,
               static_cast<enum StateSet::Code>(reason), reduced);
}

word_t*
00363 StateSetReporter::pop (bool tail, size_t& size, long& offset)
{
  word_t* buf = myStates.pop (tail, size);
  offset = myStates.getOffset ();
  return buf;
}

void
00371 StateSetReporter::setOffset (long offset)
{
  myStates.setOffset (offset);
}

void
00377 StateSetReporter::reject ()
{
  if (!myDest)
    myStates.reject (mySrc, mySrcSize, *this,
                 StateSet::inconsistent, isReduced ());
}

void
00385 StateSetReporter::displayPath (const word_t* src)
{
  assert (src && myDest);
  /** state spaces of the child nets (optional) */
  class FullSet* childset = initModules ();
  /** the synchronising state space */
  class SyncStates* sync = childset ? new class SyncStates (net) : 0;
  /** Flag: has the analysis been interrupted? */
  extern volatile bool interrupted;
  const unsigned numTr = childset
    ? net.getNumTransitions ()
    : net.getNumAllTransitions ();
  unsigned ps, i;
  class GlobalMarking m (net);

  // Initialize the context and fetch the source state
  ps = m.decode (*net.getInitMarking (), src, myPropBits);
 again:
  myFatal = false;
  if (myProp) {
    class Valuation valuation;
    valuation.setGlobalMarking (&m);
    myPropReject =
      !(*myProp)[ps].eval (valuation, myPropSucc, myProp->getFinalState ());
    if (myPropReject && !valuation.isOK ()) {
      assert (false);
      delete[] childset; delete sync;
      return;
    }
    assert (*myPropSucc > 0);
  }
  else
    myPropSucc = 0;

#ifndef NDEBUG
  mySrcDeadlock = true;
#endif // NDEBUG
  for (i = 0, myPriority = 0; !interrupted && !myFatal && i < numTr; i++) {
    const class Transition& t = net.getTransition (i);
    if ((!myPriority || t.getPriority () == myPriority) &&
      (!childset || !t.getNumChildren ()))
      t.analyze (m, *this);
    // synchronisation transitions (which have children) are analysed
    // by SyncStates::sync (), called via analyzeModules () below
  }
  if (childset)
    analyzeModules (m, *sync, childset);
  assert (i == numTr || interrupted || myFatal);
  if (!interrupted && !myFatal) {
    // path compression has eliminated the state; reconstruct it
    assert (!myPropSucc || *myPropSucc == 1);
    assert (!mySrcDeadlock);
    ps = myPropSucc ? myPropSucc[1] : 0;
    addEvents ();
    for (i = 0, myPriority = 0; !interrupted && !myFatal && i < numTr; i++) {
      const class Transition& t = net.getTransition (i);
      if ((!myPriority || t.getPriority () == myPriority) &&
        (!childset || !t.getNumChildren ()))
      t.analyze (m, *this);
    }
    assert (myFatal);
    goto again;
  }

  assert (interrupted || myFatal);
  delete[] childset; delete sync;
}

Generated by  Doxygen 1.6.0   Back to index