Logo Search packages:      
Sourcecode: maria version File versions

GraphReporter.C

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

/** @file GraphReporter.C
 * 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. */

#ifdef __GNUC__
# pragma implementation
#endif // __GNUC__
#include "GraphReporter.h"
#include "Graph.h"
#include "ComponentGraph.h"
#include "SyncStates.h"
#include "Net.h"
#include "Transition.h"
#include "Valuation.h"
#include "Printer.h"
#include "LSTS.h"
#include "PropertyState.h"
#include "GlobalMarking.h"
#include "BitVector.h"
#ifdef EXPR_COMPILE
# include "Compilation.h"
#endif // EXPR_COMPILE

/** Report graph size statistics
 * @param states  number of generated states
 * @param arcs          number of generated arcs
 * @param pending number of unprocessed states
 * @param printer the output stream
 */
static void
00053 showProgress (card_t states, card_t arcs, card_t pending,
            const class Printer& printer)
{
  printer.print (states);
  printer.printRaw (" states, ");
  printer.print (arcs);
  printer.printRaw (" arcs, ");
  printer.print (pending);
  printer.printRaw (" pending");
  printer.finish ();
}

/** Decode a state for interpreter-based analysis
 * @param buf           the encoded inflated state
 * @param net           the model the state belongs to
 * @return        the decoded state
 */
static class GlobalMarking*
00071 decode (const word_t* buf,
      const class Net& net)
{
  assert (!!buf);
  class GlobalMarking* marking = new class GlobalMarking (net);
  marking->decode (*net.getInitMarking (), buf);
  return marking;
}

#ifdef EXPR_COMPILE
/** Decoded a state for compiler-based analysis
 * @param net           the net
 * @param buf           the encoded deflated state
 * @param size          length of the state in bytes
 * @param compilation   interface to the compiled code
 * @return        the decoded state
 */
static void
decode (const class Net& net,
      word_t* buf,
      size_t size,
      const class Compilation& compilation)
{
  assert (!!buf);
  compilation.stateDecode (net.getIndex (), buf, size);
}
#endif // EXPR_COMPILE

00099 GraphReporter::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) :
  StateReporter (
#ifdef EXPR_COMPILE
             compilation,
#endif // EXPR_COMPILE
             net_, printer_, maxerrors, compress, local, flattened),
  myThreshold (threshold),
  myGraph (graph), myComponents (0),
  myChildren (flattened || !net_.getNumChildren ()
            ? 0
            : new class GraphReporter*[net_.getNumChildren ()]),
  myVisited (0),
  myStates (),
  myStateNum (CARD_T_MAX), myTargetNum (CARD_T_MAX), myProcessed (false),
  myWeaklyFair (new unsigned[net.getNumMaxFair () + 1]),
  myStronglyFair (new unsigned[net.getNumMaxFair () + 1]),
  myAddOld (false)
{
  if (!flattened) {
    class SyncStates* sync = myChildren ? new class SyncStates (net) : 0;
    class BitVector* visited = myChildren ? new class BitVector (1) : 0;
    for (unsigned i = net_.getNumChildren (); i--; ) {
      class Graph* g = new class Graph (net_.getChild (i));
      if (!g->openFiles (true)) {
      delete g;
      myChildren[i] = 0;
      }
      else {
      myChildren[i] =
        new class GraphReporter (
#ifdef EXPR_COMPILE
                           compilation,
#endif // EXPR_COMPILE
                           net_.getChild (i), printer_, maxerrors,
                           compress, local, false, 0, *g);
      myChildren[i]->mySync = sync;
      myChildren[i]->myVisited = visited;
      }
    }
  }
}

00152 GraphReporter::~GraphReporter ()
{
  if (!isFlattened ()) {
    if (myChildren) {
      delete (*myChildren)->mySync;
      delete (*myChildren)->myVisited;
    }
    for (unsigned i = net.getNumChildren (); i--; ) {
      if (!myChildren[i])
      continue;
      delete &myChildren[i]->myGraph;
      delete myChildren[i];
    }
  }
  delete myComponents;
  delete[] myChildren;
  delete[] myWeaklyFair;
  delete[] myStronglyFair;
}

class GraphReporter&
00173 GraphReporter::getChild (const unsigned* path)
{
  class GraphReporter* r = this;
  if (path) {
    for (unsigned i = 1; i <= *path; i++) {
      assert (!r->isFlattened ());
      assert (!!r->myChildren);
      assert (path[i] < r->net.getNumChildren ());
      assert (!!r->myChildren[path[i]]);
      r = r->myChildren[path[i]];
    }
  }
  return *r;
}

unsigned
00189 GraphReporter::strong (card_t state,
                   const class Expression* cond)
{
  assert (state < myGraph.getNumStates ());
  if (myComponents)
    delete myComponents;
  myComponents = new class ComponentGraph (myGraph);
  return myComponents->compute (state, cond);
}

class SearchList&
00200 GraphReporter::getSuccessors (card_t state)
{
  assert (myStates.empty ());
  if (!(myProcessed = myGraph.isProcessed (state))) {
    myStates.push (state);
    StateReporter::analyze (StateReporter::Single);
  }
  else if (card_t* data = myGraph.getSuccessors (state)) {
    for (card_t i = 1; i <= *data; i++)
      myStates.push (data[i]);
    delete[] data;
  }
  return myStates;
}

class SearchList&
00216 GraphReporter::getSuccessors (const class Transition& transition)
{
  class GlobalMarking* m = pop (false);
  assert (!!m);
  if (m) {
    transition.analyze (*m, *this);
    delete m;
  }
  return myStates;
}

card_t*
00228 GraphReporter::prepareFair (card_t state,
                      word_t*& buf,
                      class BitUnpacker*& u)
{
  card_t* succ = myGraph.getSuccessors (state, &buf);
  if (succ) {
    assert (*succ && buf);
#ifdef EXPR_COMPILE
    if (myCompilation)
      u = 0, myCompilation->eventInflate (buf, 0);
    else
#endif // EXPR_COMPILE
      u = new class BitUnpacker (buf);
  }
  return succ;
}

unsigned*
00246 GraphReporter::computeFair (card_t state,
                      class BitUnpacker* u,
                      unsigned** strong)
{
#ifdef EXPR_COMPILE
  if (myCompilation) {
    assert (!u);
    if (enum Error err = myCompilation->eventDecode (!!strong)) {
      printer.printRaw ("fairness constraint at state ");
      printer.printState (state);
      printer.delimiter (':');
      printer.printRaw (Valuation::msg (err));
      printer.finish ();
      flagFatal ();
      return 0;
    }
    if (strong)
      *strong = myCompilation->getStronglyFair ();
    return myCompilation->getWeaklyFair ();
  }
  else {
#endif // EXPR_COMPILE
    const class Transition* transition;
    class Valuation valuation;
    assert (!!u);
    net.decode (*u, transition, valuation, isFlattened ());
    transition->computeWeaklyFair (valuation, myWeaklyFair);
    if (!valuation.isOK ()) {
      printer.printRaw ("weakly_fair ");
    error:
      printer.printQuoted (transition->getName ());
      printer.printRaw ("at state ");
      printer.printState (state);
      printer.delimiter (':');
      printer.linebreak ();
      valuation.display (printer);
      printer.finish ();
      flagFatal ();
      return 0;
    }
    if (strong) {
      transition->computeStronglyFair (valuation, myStronglyFair);
      if (!valuation.isOK ()) {
      printer.printRaw ("strongly_fair ");
      goto error;
      }
      *strong = myStronglyFair;
    }
    return myWeaklyFair;
#ifdef EXPR_COMPILE
  }
#endif // EXPR_COMPILE
}

const unsigned*
00301 GraphReporter::eval (card_t state,
                 unsigned prop,
                 const class PropertyState& ps)
{
#ifdef EXPR_COMPILE
  if (myCompilation) {
    size_t size;
    word_t* buf = myGraph.fetchState (state, size, 0);
    ::decode (net, buf, size, *myCompilation);
    delete[] buf;
    if (enum Error err = myCompilation->propEval (prop)) {
      printer.printRaw ("property ");
      printer.print (prop);
      printer.printRaw (" evaluation error at state ");
      printer.printState (state);
      printer.printRaw (":");
      printer.delimiter (' ');
      printer.printRaw (Valuation::msg (err));
      printer.finish ();
      flagFatal ();
      return 0;
    }
    return myCompilation->getPropSucc ();
  }
  else {
#endif
    /** vector of enabled gates in the property automaton */
    unsigned* enabled;
    class GlobalMarking* m = myGraph.fetchState (state);
    class Valuation valuation;
    valuation.setGlobalMarking (m);
    if (!ps.eval (valuation, enabled)) {
      printer.printRaw ("property ");
      printer.print (prop);
      printer.printRaw (" evaluation error at state ");
      printer.printState (state);
      printer.printRaw (":");
      printer.finish ();
      valuation.display (printer);
      printer.finish ();
      delete[] enabled;
      enabled = 0;
      flagFatal ();
    }
    else
      assert (valuation.isOK ());
    delete m;
    return enabled;
#ifdef EXPR_COMPILE
  }
#endif // EXPR_COMPILE
}

void
00355 GraphReporter::analyzeModular (enum SearchKind kind)
{
  assert (!isFlattened ());
  const unsigned numTr = net.getNumTransitions ();
  extern bool interrupted;
#ifdef EXPR_COMPILE
  if (myCompilation) {
    while (!interrupted && !myFatal) {
      if (!popCompiled (kind == Breadth))
      break;
      myProcessed = myGraph.isProcessed (myStateNum);
      mySrcDeadlock = true, myPriority = 0;
      unsigned i;
      for (i = 0; !interrupted && !myFatal && i < numTr; i++) {
      const class Transition& t = net.getTransition (i);
      if ((!myPriority || t.getPriority () == myPriority) &&
          !t.getNumChildren ())
        analyze (t);
      // synchronisation transitions (which have children) are analysed
      // by SyncStates::sync (), called below
      }

      if (myChildren) {
      i = net.getNumChildren ();
      word_t** srcs = new word_t*[i];
      // analyze child state spaces
      for (; !interrupted && !myFatal && i--; ) {
        const class Net& child = net.getChild (i);
        unsigned bytes;
        const void* buf =
          myCompilation->stateProject (child.getIndex (), 0, 0, bytes);
        unsigned numWords = bytes ? (bytes - 1) / sizeof (word_t) + 1 : 0;
        /* back up the source state */
        srcs[i] = bytes ? new word_t[numWords] : 0;
        memcpy (srcs[i], buf, numWords * sizeof (word_t));
        BitPacker::inflate (srcs[i][numWords - 1],
                        (-bytes) % sizeof (word_t));
#ifdef SYNC_CACHE
        if ((*myChildren)->mySync->lookup (i, srcs[i], numWords))
          continue; // the modular state has already been analyzed
#endif // SYNC_CACHE
        class GraphReporter& reporter = *myChildren[i];
        class Graph::AddStatus src = reporter.myGraph.add (buf, bytes);
        reporter.init (src.number);
        reporter.myVisited->clear ();
        reporter.myVisited->extend (src.number, true);

        unsigned numErrors = reporter.getNumErrors ();
        reporter.analyzeModular (Breadth);
        /* restore the source state */
        myCompilation->stateDecode (child.getIndex (), srcs[i], 0);
        if (reporter.myFatal)
          myFatal = true;
        if (reporter.getNumErrors () > numErrors)
          reportError (false);
      }

      // find out enabled synchronisation transitions and synchronise
      for (i = net.getNumTransitions (); i--; ) {
        const class Transition& t = net.getTransition (i);
        if ((!myPriority || t.getPriority () == myPriority) &&
            t.getNumChildren ())
          (*myChildren)->mySync->sync (t, *this, srcs);
      }

      for (i = net.getNumChildren (); i--; )
        delete[] srcs[i];
      delete[] srcs;

#ifndef SYNC_CACHE
      (*myChildren)->mySync->cleanup ();
#endif // !SYNC_CACHE
      }

      if (mySrcDeadlock && !interrupted && !myFatal) {
      switch (myCompilation->stateDeadlock (net.getIndex ())) {
      case errNone:
        break;
      default:
        myFatal = true;
        // fall through
      case errComp:
        reportError (true);
      }
      }

      if (suppress ())
      continue;
      addEvents ();
      if (kind >= Single)
      break;
    }
    return;
  }
  else
#endif // EXPR_COMPILE
  while (!interrupted && !myFatal) {
    class GlobalMarking* m = pop (kind == Breadth);
    if (!m)
      break;
    myProcessed = myGraph.isProcessed (myStateNum);
    mySrcDeadlock = true, myPriority = 0;
    unsigned i;
    for (i = 0; !interrupted && !myFatal && i < numTr; i++) {
      const class Transition& t = net.getTransition (i);
      if ((!myPriority || t.getPriority () == myPriority) &&
        !t.getNumChildren ())
      t.analyze (*m, *this);
      // synchronisation transitions (which have children) are analysed
      // by SyncStates::sync (), called below
    }

    if (myChildren) {
      // analyze child state spaces
      for (i = net.getNumChildren (); !interrupted && !myFatal && i--; ) {
      const class Net& child = net.getChild (i);
      m->encode (myStateBuf, child);
#ifdef SYNC_CACHE
      if ((*myChildren)->mySync->lookup (i, myStateBuf.getBuf (),
                                 myStateBuf.getNumWords ()))
        continue; // the modular state has already been analyzed
#endif // SYNC_CACHE
      myStateBuf.deflate ();
      class GraphReporter& reporter = *myChildren[i];
      class Graph::AddStatus src =
        reporter.myGraph.add (myStateBuf.getBuf (),
                        myStateBuf.getNumBytes ());
      reporter.init (src.number);
      reporter.myVisited->clear ();
      reporter.myVisited->extend (src.number, true);

      unsigned numErrors = reporter.getNumErrors ();
      reporter.analyzeModular (Breadth);
      if (reporter.myFatal)
        myFatal = true;
      if (reporter.getNumErrors () > numErrors)
        reportError (false);
      }

      // find out enabled synchronisation transitions and synchronise
      for (i = net.getNumTransitions (); i--; ) {
      const class Transition& t = net.getTransition (i);
      if ((!myPriority || t.getPriority () == myPriority) &&
          t.getNumChildren ())
        (*myChildren)->mySync->sync (*m, t, *this);
      }

#ifndef SYNC_CACHE
      (*myChildren)->mySync->cleanup ();
#endif // !SYNC_CACHE
    }

    if (mySrcDeadlock && !interrupted && !myFatal) {
      switch (net.isDeadlock (*m, false)) {
      case Net::OK:
      break;
      case Net::Fatal:
      myFatal = true;
      // fall through
      case Net::Error:
      reportError (true);
      }
    }

    delete m;
    if (suppress ())
      continue;
    addEvents ();
    if (kind >= Single)
      break;
  }
}

bool
00529 GraphReporter::do_addState (const void* state,
                      size_t size)
{
  bool isNew = do_addStateOnly (state, size);
  if (myVisited) {
    if (myTargetNum >= myVisited->getSize ())
      myVisited->extend (myTargetNum, true);
    else if (myVisited->tset (myTargetNum)) {
      assert (!isNew);
      return false;
    }
  }
  if (myVisited || isNew || myAddOld)
    myStates.push (myTargetNum);
  return isNew;
}

bool
00547 GraphReporter::do_addStateOnly (const void* state,
                        size_t size)
{
  if (myProcessed) {
    myTargetNum = myGraph.lookup (state, size);
    assert (myTargetNum != CARD_T_MAX);
    return false;
  }
  class Graph::AddStatus target = myGraph.add (state, size);
  myGraph.add (myStateNum, myTargetNum = target.number);

  if (myThreshold && !(myGraph.getNumArcs () % myThreshold))
    ::showProgress (myGraph.getNumStates (), myGraph.getNumArcs (),
                myStates.size (), printer);

  return target.isNew;
}

word_t*
00566 GraphReporter::do_popState (bool tail,
                      size_t& size)
{
  if (myStates.empty ())
    return 0;
  myStateNum = myStates.pop (tail);
  assert (!isFlattened () || !myGraph.isProcessed (myStateNum));
  return myGraph.fetchState (myStateNum, size, 0);
}

class GlobalMarking*
00577 GraphReporter::pop (bool breadth)
{
  return popState (breadth)
    ? inflate (), ::decode (mySrc, net)
    : 0;
}

#ifdef EXPR_COMPILE
bool
GraphReporter::popCompiled (bool breadth)
{
  assert (!!myCompilation);
  if (popState (breadth))
    ::decode (net, mySrc, mySrcSize, *myCompilation);
  return !!mySrc;
}
#endif // EXPR_COMPILE

void
00596 GraphReporter::addEvents ()
{
#ifdef EXPR_COMPILE
  if (myCompilation) {
    if (!myProcessed) {
      size_t bytes;
      const void* buf = myCompilation->eventDeflate (bytes);
      myGraph.addEvents (myStateNum, buf, bytes);
    }
    myCompilation->eventClear ();
  }
  else {
#endif // EXPR_COMPILE
    if (!myProcessed) {
      myEventBuf.deflate ();
      myGraph.addEvents (myStateNum,
                   myEventBuf.getBuf (), myEventBuf.getNumBytes ());
    }
    myEventBuf.clear ();
#ifdef EXPR_COMPILE
  }
#endif // EXPR_COMPILE
}

bool
00621 GraphReporter::report (const class Transition& transition,
                   const class Valuation& valuation,
                   const class GlobalMarking& marking,
                   bool rejected)
{
  myStateBuf.deflate ();
  bool isNew;
  if (transition.getName ()) {
    const bool hidden = transition.isHidden (valuation);
    isNew = rejected
      ? do_addStateOnly (myStateBuf.getBuf (), myStateBuf.getNumBytes ())
      : addState (myStateBuf.getBuf (), myStateBuf.getNumBytes (), hidden);
    if (rejected || !hidden || !isReduced ())
      net.encode (myEventBuf, transition, valuation, isFlattened ());
    if (isNew && myGraph.getLSTS ())
      myGraph.getLSTS ()->outputState (marking, myTargetNum);
  }
  else {
    // do not add arcs for anonymous (interactively defined) transitions
    class Graph::AddStatus target =
      myGraph.add (myStateBuf.getBuf (), myStateBuf.getNumBytes ());
    isNew = target.isNew;
    myTargetNum = target.number;
  }

  if (rejected) {
    if (isNew) {
      myGraph.flagErroneous (myTargetNum);
      printer.printRaw (myFatal
                  ? "fatally rejected state "
                  : "rejected state ");
      printer.printState (myTargetNum);
    }
    else {
      printer.printRaw (myFatal
                  ? "fatally rejected state reachable from "
                  : "rejected state reachable from ");
      printer.printState (myStateNum);
    }
    printer.finish ();
    if (error ())
      flagFatal ();
  }

  return isNew;
}

void
00669 GraphReporter::reportError (bool deadlock)
{
  if (deadlock)
    printer.printRaw (myFatal
                  ? "fatal deadlock state "
                  : "deadlock state ");
  else {
    myGraph.flagErroneous (myStateNum);
    printer.printRaw (myFatal
                  ? "fatally rejected subnet state reachable from "
                  : "rejected subnet state reachable from ");
  }
  printer.printState (myStateNum);
  printer.finish ();
  if (error ())
    myFatal = true;
  if (myFatal)
    myStates.clear ();
}

#ifdef EXPR_COMPILE
bool
GraphReporter::report (const void* state,
                   size_t size,
                   bool rejected,
                   bool hidden)
{
  assert (!!myCompilation);
  const bool isNew = rejected
    ? do_addStateOnly (state, size)
    : addState (state, size, hidden);

  if (isNew && myGraph.getLSTS ())
    myGraph.getLSTS ()->outputState (*myCompilation, myTargetNum);

  if (rejected) {
    myGraph.flagErroneous (myTargetNum);
    printer.printRaw (myFatal
                  ? "fatally rejected state "
                  : "rejected state ");
    printer.printState (myTargetNum);
    printer.finish ();
    if (error ())
      flagFatal ();
  }

  return isNew;
}
#endif // EXPR_COMPILE

void
00720 GraphReporter::reject ()
{
  printer.printState (myStateNum);
  printer.delimiter (':');
  if (myFatal)
    myStates.clear ();
}

void
00729 GraphReporter::printState (const class GlobalMarking& m,
                     card_t state,
                     const class Printer& out)
{
  out.printState (state);
  if (!isFlattened () && net.getNumChildren ()) {
    out.delimiter ('(');
    for (unsigned i = 0; i < net.getNumChildren (); ) {
      const class Net& child = net.getChild (i);
      m.encode (myStateBuf, child);
      myStateBuf.deflate ();
      card_t s = myChildren[i]->myGraph.lookup (myStateBuf.getBuf (),
                                    myStateBuf.getNumBytes ());
      if (s != CARD_T_MAX)
      out.printState (s);
      else
      out.printRaw ("@?");
      if (++i >= net.getNumChildren ())
      break;
      out.delimiter (' ');
    }
    out.delimiter (')');
  }
}

Generated by  Doxygen 1.6.0   Back to index