Logo Search packages:      
Sourcecode: maria version File versions

static void safetyP ( bool  breadth,
card_t  visual,
const class Property prop 
) [static]

Analyze the safety properties of the model

Parameters:
breadth flag: search breadth first instead of depth
visual visualization level for counterexample
prop the safety property to analyze (optional)

apply path compression?

suppress local (transient) states?

apply distributed search?

client socket number

The state space interface

Definition at line 1163 of file maria.C.

References StateSet::add(), StateReporter::analyze(), StateReporter::Breadth, Compilation::clearProp(), client_connect(), Compilation::compile(), compress, connect_addr, createJobs(), BitPacker::deflate(), demsg(), StateReporter::Depth, Printer::finish(), funcSize, BitPacker::getBuf(), StateReporter::getEnabled(), CompactSet::getHashSize(), StateReporter::getMaxSize(), StateReporter::getMinSize(), BitPacker::getNumBytes(), StateReporter::getNumErrors(), StateReporter::getNumLocal(), hashSize, CompactSet::init(), jobs, local, maxerrors, md5compact, modular, netname, notloaded, numTables, Printer::print(), Printer::printRaw(), probabilistic, serve(), showEnabled(), Dotty::startVisual(), states, thePrinter, thresold, and verbose.

Referenced by onthefly().

{
  if (!net) {
    if (!notloaded) {
      notloaded = true;
      thePrinter.printRaw ("no model has been loaded");
      thePrinter.finish ();
    }
    return;
  }
  else if (subnet != net) {
    thePrinter.printRaw ("need to be in root net");
    thePrinter.finish ();
    return;
  }

  class StateSet* states;
  /** apply path compression? */
  bool comp = compress;
  /** suppress local (transient) states? */
  bool loc = local;
  /** apply distributed search? */
  bool distributed = connect_addr || jobs;
  /** client socket number */
  int s = 0;

  if (connect_addr) {
    if (!(s = client_connect ()))
      comp = false; // this is the server
    else if (s > 0)
      goto client;
    else // failed to establish a connection
      return;
  }
  else if (jobs)
    comp = false;

  if (probabilistic && md5compact) {
    class CompactSet* cs = new class CompactSet (hashSize, funcSize);
    states = cs;
    if (!cs->init ()) {
      thePrinter.printRaw ("insufficient memory for ");
      thePrinter.print (card_t (cs->getHashSize ()));
      thePrinter.printRaw (" hash table entries of ");
      thePrinter.print (card_t (funcSize));
      thePrinter.printRaw (" bytes");
      thePrinter.finish ();
      goto done;
    }

    if (verbose)
      fprintf (stderr, "%s:using hash compaction -H%u,%u\n",
             netname, cs->getHashSize (), funcSize);
  }
  else if (probabilistic) {
    if (!static_cast<class HashGraph*>
      (states = new class HashGraph)->init
      (numTables, funcSize, hashSize)) {
      thePrinter.printRaw ("insufficient memory for ");
      thePrinter.print (card_t (numTables));
      thePrinter.printRaw (" tables of ");
      thePrinter.print (card_t (funcSize));
      thePrinter.printRaw (" functions and ");
      thePrinter.print (card_t (hashSize));
      thePrinter.printRaw (" bits");
      thePrinter.finish ();
      goto done;
    }

    if (verbose)
      fprintf (stderr, "%s:using bitstate hashing -H%u,%u,%u\n",
             netname, hashSize, funcSize, numTables);
  }
  else {
    if (!static_cast<class FullSet*>
      (states = new class FullSet)->init (true))
      goto done;
    if (verbose)
      fprintf (stderr, "%s:exploring the reachable states\n", netname);
  }

#ifdef EXPR_COMPILE
  if (compilation) {
    if (prop) {
      if (verbose)
      fprintf (stderr, "%s:compiling the property automaton\n", netname);
      if (!compilation->compile (*prop)) {
      thePrinter.printRaw ("could not compile the property automaton");
      thePrinter.finish ();
      return;
      }
    }
    else
      compilation->clearProp ();
  }
#endif // EXPR_COMPILE

  if (distributed) {
    bool server;
    if (0 > (s = createJobs (jobs, server))) {
      if (!server)
      exit (-1);
      else
      return;
    }
    if (server) {
      loc = false;
      goto server;
    }
    delete states;
  client:
    states = new class ParSet (s);
  }

  {
    class BitPacker buf;
    if (!net->getInitMarking ()->encode (buf, *net->getInitMarking (), 0)) {
      fprintf (stderr, "%s:invalid initial marking\n", netname);
      delete states;
      if (distributed)
      exit (0); // clients terminate here
      return;
    }
    else {
      buf.deflate ();
      if (!states->add (buf.getBuf (), buf.getNumBytes ()))
      assert (false);
    }
  }

  if (distributed)
    thresold = 0, visual = 0, distributed = false;
 server:
  {
    /** The state space interface */
    class StateSetReporter reporter (
#ifdef EXPR_COMPILE
                             compilation,
#endif // EXPR_COMPILE
                             *net, thePrinter, maxerrors,
                             comp, loc, !modular, thresold,
                             visual ? Dotty::startVisual () : 0,
                             visual > 1, *states, prop);
    thePrinter.setBOL (0);
    if (distributed)
      serve (s, reporter, breadth);
    else {
      reporter.analyze (breadth
                  ? StateReporter::Breadth
                  : StateReporter::Depth);
      if (s) {
      delete states;
      exit (0); // clients exit here
      }
    }
    thePrinter.printQuoted (netname);
    if (unsigned num = states->getNumStates ()) {
      thePrinter.printRaw (probabilistic ? ": at least " : ": ");
      thePrinter.print (num);
      if (reporter.getMinSize () <= reporter.getMaxSize ()) {
      thePrinter.printRaw (" states (");
      thePrinter.print (card_t (reporter.getMinSize ()));
      if (reporter.getMaxSize () != reporter.getMinSize ()) {
        thePrinter.printRaw ("..");
        thePrinter.print (card_t (reporter.getMaxSize ()));
      }
      thePrinter.printRaw (" bytes), ");
      }
      else
      thePrinter.printRaw (" states, ");
    }
    else
      thePrinter.printRaw (": no states, ");
    if (reporter.getNumLocal ()) {
      thePrinter.printRaw ("at most ");
      thePrinter.print (reporter.getNumLocal ());
      thePrinter.printRaw (" module states, ");
    }
    if (reporter.getNumErrors ()) {
      thePrinter.print (card_t (reporter.getNumErrors ()));
      thePrinter.printRaw (reporter.getNumErrors () == 1
                     ? " error, "
                     : " errors, ");
    }
    thePrinter.print (states->getNumArcs ());
    if (probabilistic && md5compact) {
      thePrinter.printRaw (" arcs, ");
      thePrinter.print (card_t (static_cast<class CompactSet*>
                        (states)->getNumCollisions ()));
      thePrinter.printRaw (" collisions");
    }
    else
      thePrinter.printRaw (" arcs");
    thePrinter.finish ();
    showEnabled (reporter.getEnabled ());
    thePrinter.setBOL (&demsg);
  }

 done:
  delete states;
}


Generated by  Doxygen 1.6.0   Back to index