Logo Search packages:      
Sourcecode: maria version File versions

Product.C

Go to the documentation of this file.
// Product automaton -*- c++ -*-

#ifdef __GNUC__
# pragma implementation
#endif // __GNUC__
#include "Product.h"
#include "Property.h"
#include "GlobalMarking.h"
#include "Valuation.h"
#include "Net.h"
#include "Graph.h"
#include "GraphReporter.h"
#include "Printer.h"
#include "Transition.h"
#include "SetList.h"

#include <stdlib.h>

/** @file Product.C
 * Product of reachability graph and the negation of property being verified
 */

/* Copyright © 1999-2003 Marko Mäkelä (msmakela@tcs.hut.fi).
   Copyright © 1999-2001 Timo Latvala (timo@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. */

/** Look up the search depth associated with a product state
 * @param visited map of visited states
 * @param s       a visited state
 * @return        the search depth associated with the state
 */
inline static unsigned
00050 lookup (const Product::StateMap& visited,
      const Product::State& s)
{
  Product::StateMap::const_iterator i = visited.find (s);
  assert (i != visited.end ());
  return i->second;
}

/** Look up the search depth associated with a product state
 * @param visited map of visited states
 * @param s       a visited state
 * @return        the search depth associated with the state, or 0
 */
inline static unsigned
00064 lookup_maybe (const Product::StateMap& visited,
            const Product::State& s)
{
  Product::StateMap::const_iterator i = visited.find (s);
  return i == visited.end () ? 0 : i->second;
}

/** Look up the search depth associated with a product state and clear it
 * @param visited map of visited states
 * @param s       a visited state
 * @param init          the new value
 * @return        the search depth associated with the state
 */
inline static unsigned
00078 lookup_clear (Product::StateMap& visited,
            const Product::State& s,
            unsigned init = 0)
{
  Product::StateMap::iterator i = visited.find (s);
  assert (i != visited.end () && i->second);
  unsigned d = i->second;
  i->second = init;
  return d;
}

/** Offsets to the temporary files */
00090 struct offsets
{
  /** current offset to the automaton file */
00093   unsigned aut;
  /** current offset to the reachability graph file */
00095   unsigned rg;
};

/** The temporary files */
00099 struct files
{
  /** product automaton directory: map from search depth numbers to offsets */
00102   FILE* directory;
  /** successor state numbers in the property automaton */
00104   FILE* aut_succ;
  /** successor state numbers in the reachability graph */
00106   FILE* rg_succ;
  /** offsets in the files */
00108   struct offsets offset;
};

/** Open temporary files
 * @param f       (output) the temporary files
 * @return        true if everything succeeded
 */
inline static bool
00116 openFiles (struct files& f)
{
  if (!(f.directory = tmpfile ()));
  else if (!(f.aut_succ = tmpfile ()))
    fclose (f.directory), f.directory = 0;
  else if (!(f.rg_succ = tmpfile ()))
    fclose (f.directory), fclose (f.aut_succ),
      f.directory = f.aut_succ = 0;
  else {
    f.offset.aut = f.offset.rg = 0;
    return true;
  }

  perror ("tmpfile");
  return false;
}

/** Close temporary files
 * @param f       the temporary files
 */
inline static void
00137 closeFiles (struct files& f)
{
  fclose (f.directory);
  fclose (f.aut_succ);
  fclose (f.rg_succ);
}

/** Write the successors to the temporary files
 * @param f       the temporary files
 * @param aut           property automaton successor states (aut[1..*aut])
 * @param rgsize  number of reachability graph successor states
 * @param rgbegin begin iterator for reachability graph successor states
 * @param rgend         end iterator for reachability graph successor states
 */
inline static bool
00152 writeArcs (struct files& f,
         const unsigned* aut,
         size_t rgsize,
         const SearchList::const_iterator& rgbegin,
         const SearchList::const_iterator& rgend)
{
  assert (f.offset.aut == ftell (f.aut_succ) / sizeof (unsigned));
  assert (f.offset.rg == ftell (f.rg_succ) / sizeof (unsigned));

  if (1 != fwrite (&f.offset, sizeof f.offset, 1, f.directory) ||
      *aut + 1 != fwrite (aut, sizeof *aut, *aut + 1, f.aut_succ))
    return false;

  unsigned s = rgsize;
  if (1 != fwrite (&s, sizeof s, 1, f.rg_succ))
    return false;
  for (SearchList::const_iterator i = rgbegin; i != rgend; i++) {
    s = *i;
    if (1 != fwrite (&s, sizeof s, 1, f.rg_succ))
      return false;
  }

  f.offset.aut += *aut + 1;
  f.offset.rg += rgsize + 1;
  return true;
}

/** Fetch the offsets for the arc files
 * @param f       the files
 * @param depth         dfs number for the source state
 * @param ofs           (output) offsets to the arcs of source state
 */
inline static void
00185 fetchOffsets (const struct files& f,
            unsigned depth,
            struct offsets& ofs)
{
  if (fseek (f.directory, (depth - 1) * sizeof f.offset, SEEK_SET)) {
    perror ("Product: fseek (directory)");
    assert (false);
  }
  else if (1 != fread (&ofs, sizeof ofs, 1, f.directory)) {
    perror ("Product: fread (directory)");
    assert (false);
  }
}

/** A strongly connected component for Streett emptiness check */
00200 struct components
{
  /** number of temporary states */
00203   unsigned numTemp;
  /** the Streett transition relation */
00205   class SetList* trans;
  /** the L sets */
00207   class SetList* l;
  /** the U sets */
00209   class SetList* u;
  /** the component states (comp[1..*comp]) */
00211   unsigned* comp;
};


/** Read the arcs of a product state
 * @param rg            state numbers in the reachability graph
 * @param prop          state numbers in the property automaton
 * @param prod          state numbers in the product automaton
 * @param f       pointer to the arc files
 */
static void
00222 freadArc (unsigned*& rg,
        unsigned*& prop,
        unsigned*& prod,
        struct files& f)
{
  if ((1 != fread (&rg[1], sizeof *rg, 1, f.rg_succ)) ||
      (1 != fread (&prop[1], sizeof *prop, 1, f.aut_succ)))
    assert (false);
  if (rg[1] > *rg) {
    register unsigned u = rg[1]; delete[] rg; rg = new unsigned[u + 2];
    *rg = rg[1] = u;
  }
  if (prop[1] > *prop) {
    register unsigned u = prop[1]; delete[] prop; prop = new unsigned[u + 2];
    *prop = prop[1] = u;
  }
  register unsigned u = prop[1] * rg[1];
  if (u > *prod) {
    delete[] prod; prod = new unsigned[u + 1]; *prod = u;
  }

  if (rg[1] != fread (rg + 2, sizeof *rg, rg[1], f.rg_succ) ||
      prop[1] != fread (prop + 2, sizeof *prop, prop[1], f.aut_succ)) {
    perror ("decodeArc():fread");
    assert (false);
  }
}

/** Decode the arcs of one product state
 * @param visited statemap for checking in component
 * @param trans         the transition relation (output param)
 * @param minDepth      minimum value for being in the component
 * @param maxDepth      maximum value for being in the component
 * @param parent  index of the parent state
 * @param rg            state numbers in the reachability graph
 * @param prop          state numbers in the property automaton
 * @param prod          state numbers in the product automaton
 * @param f       pointer to the arc files
 */
static void
00262 decodeArc (const Product::StateMap& visited,
         class SetList& trans,
         unsigned minDepth,
         unsigned maxDepth,
         unsigned parent,
         unsigned*& rg,
         unsigned*& prop,
         unsigned*& prod,
         struct files& f)
{
  struct offsets ofs;
  fetchOffsets (f, maxDepth - parent, ofs);

  fseek (f.rg_succ, ofs.rg * sizeof *rg, SEEK_SET);
  fseek (f.aut_succ, ofs.aut * sizeof *prop, SEEK_SET);

  freadArc (rg, prop, prod, f);

  // compute the product: number of items, plus 1
  unsigned u = 1;

  //because of dfs num recycling all dfs nums in one component are contiguous
  //therefore we can use the dfs number to check if a state is in the component
  for (unsigned i = rg[1]; i--; ) {
    for (unsigned j = prop[1]; j--; ) {
      register unsigned p =
      lookup (visited, Product::State (rg[i + 2], prop[j + 2]));
      //if the edge leads out of the component, don't add it
      if (p < minDepth || p > maxDepth)
      continue;
      prod[u++] = maxDepth - p; // adjust the index
    }
  }
  if (unsigned v = --u) {
    u = *prod, *prod = v;
    trans.copy (parent, prod);
    *prod = u;
  }
}

/** Decode the arcs of one product state, not translating product state indices
 * @param visited statemap for checking in component
 * @param trans         the transition relation (output param)
 * @param maxDepth      maximum value for being in the component
 * @param parent  index of the parent state
 * @param rg            state numbers in the reachability graph
 * @param prop          state numbers in the property automaton
 * @param prod          state numbers in the product automaton
 * @param f       pointer to the arc files
 */
static void
00313 decodeProductArc (const Product::StateMap& visited,
              class SetList& trans,
              unsigned maxDepth,
              unsigned parent,
              unsigned*& rg,
              unsigned*& prop,
              unsigned*& prod,
              struct files& f)
{
  struct offsets ofs;
  fetchOffsets (f, parent, ofs);

  fseek (f.rg_succ, ofs.rg * sizeof *rg, SEEK_SET);
  fseek (f.aut_succ, ofs.aut * sizeof *prop, SEEK_SET);

  freadArc (rg, prop, prod, f);

  // compute the product: number of items, plus 1
  unsigned u = 1;

  //because of dfs num recycling all dfs nums in one component are contiguous
  //therefore we can use the dfs number to check if a state is in the component
  for (unsigned i = rg[1]; i--; ) {
    for (unsigned j = prop[1]; j--; ) {
      register unsigned p =
      lookup_maybe (visited, Product::State (rg[i + 2], prop[j + 2]));
      if (!p || p > maxDepth)
      continue;
      prod[u++] = maxDepth - p;
    }
  }
  if (unsigned v = --u) {
    u = *prod, *prod = v;
    trans.copy (parent, prod);
    *prod = u;
  }
}

/** Add intermediate states connected to a given source state;
 * update the transition relation and fairness set information
 * @param prodSucc      place holder for the successors
 * @param visited the statemap
 * @param c       the component for the Streett check
 * @param ci            index to the Streett transition relation
 * @param fair          the accepting successors of the property automaton
 * @param prop          the successor states in the property automaton
 * @param minDepth      the minimum dfs num for being in the component
 * @param maxDepth      the maximum dfs num for being in the component
 * @param rgSucc  the successor in the reachability graph
 */
inline static void
00364 memberships (unsigned* prodSucc,
           const Product::StateMap& visited,
           struct components& c,
           unsigned ci,
           const unsigned* fair,
           const unsigned* prop,
           unsigned minDepth,
           unsigned maxDepth,
           unsigned rgSucc)
{
  unsigned cnt = 1, i;
  // check those successor product states that are in the component
  for (i = *prop; i; ) {
    prodSucc[cnt] =
      ::lookup_maybe (visited, Product::State (rgSucc, prop[i--]));
    if (prodSucc[cnt] >= minDepth && prodSucc[cnt] <= maxDepth)
      prodSucc[cnt] = maxDepth - prodSucc[cnt], cnt++; // adjust the index
  }

  // we only make intermediate state for arcs
  // for the successors of this transition instance
  if ((*prodSucc = --cnt)) {
    unsigned oldCnt = c.trans->getNumSets ();
    for (i = cnt, cnt = 0; i; i--) {
      unsigned s = prodSucc[i];
      for (unsigned j = c.trans->getSize (ci); j--; ) {
      if ((*c.trans)[ci][j] != s)
        continue;
      (*c.trans)[ci][j] = oldCnt + cnt;
      c.trans->grow (oldCnt + cnt + 1);
      unsigned buffer[2] = {1, s};
      c.trans->copy (oldCnt + cnt, buffer);
      c.numTemp++;
      cnt++;
      break;
      }
    }
    assert (cnt == *prodSucc);
    //fix set memberships of the intermediate state
    c.u->grow (oldCnt + cnt);
    while (cnt--)
      c.u->copy (oldCnt + cnt, fair);
  }
}

/** Recover the arcs from the temporary files
 * @param f       the temporary files
 * @param visited map of visited states
 * @param states  the states in the strongly connected component
 * @param reporter      the reachability graph interface
 * @param property      the property automaton
 * @param minDepth      minimum value for being in the component
 * @param maxDepth      maximum value for being in the component
 * @param c       (output) the component for the Streett check
 */
static void
00420 readArcs (struct files& f,
        Product::StateMap& visited,
        Product::StateStack& states,
        class GraphReporter& reporter,
        const class Property& property,
        unsigned minDepth,
        unsigned maxDepth,
        struct components& c)
{
  unsigned size = maxDepth - minDepth + 1;
  c.numTemp = 0;
  c.trans = new class SetList (size);
  c.l = new class SetList (size);
  c.u = new class SetList (size);
  c.comp = 0;

  // assign the L-sets from the system and the property
  unsigned i, j, *t;
  for (i = size; i--; ) {
    j = property.getNumSets () + reporter.net.getNumWeaklyFair ();
    for (*(t = new unsigned[j + 1]) = j; j; j--)
      t[j] = j - 1;
    c.l->assign (i, t);
  }

  /** placeholder for reachability graph successors */
  unsigned* rg = new unsigned[2]; *rg = 0;
  /** placeholder for property automaton successors */
  unsigned* prop = new unsigned[2]; *prop = 0;
  /** placeholder for product automaton successors */
  unsigned* prod = new unsigned[1]; *prod = 0;

  Product::StateStack::const_iterator psi = states.begin ();
  for (unsigned s = 0; s < size; s++) {
    assert (psi != states.end ());
    const class Product::State& ps = *psi++;
    // assign the U-sets from the property
    for (j = 0, i = property.getNumSets (); i--; )
      if (property.accepts (ps.prop, i))
      j++;
    if (j) {
      *(t = new unsigned[j + 1]) = j;
      for (i = property.getNumSets (); i--; )
      if (property.accepts (ps.prop, i))
        t[j--] = i;
      c.u->assign (s, t);
    }

    // get the successors in the reachability graph

    /** Encoded transition instances */
    word_t* data;
    /** Interface for decoding the transition instances */
    class BitUnpacker* u;
    /** Successors in the reachability graph */
    card_t* rgSucc = reporter.prepareFair (ps.rg, data, u);
    // no successors: go to next state
    if (!rgSucc)
      continue;

    // read the transition relation
    decodeArc (visited, *c.trans, minDepth, maxDepth, s, rg, prop, prod, f);

    // assign the L- and U-sets from the system
    class BitVector stateWeak (reporter.net.getNumWeaklyFair ());
    /** successors within component */
    unsigned* prodSucc = new unsigned[prop[1] + 1];
    *prodSucc = 0;
    for (i = 1; i <= *rgSucc; i++) {
      /** enabled strong fairness sets */
      unsigned* sfair;
      /** enabled weak fairness sets */
      unsigned* wfair = reporter.computeFair (ps.rg, u, &sfair);
      if (!wfair) {
      delete[] prodSucc;
      delete[] rgSucc;
      break;
      }

      /** current number of states in the component */
      const unsigned oldCnt = size + c.numTemp;

      if (*wfair) {
      for (j = *wfair; j; j--)
        wfair[j] += property.getNumSets ();
      memberships (prodSucc, visited, c, s, wfair, prop + 1,
                 minDepth, maxDepth, rgSucc[i]);
      for (j = *wfair; j; j--)
        stateWeak.assign (wfair[j] - property.getNumSets (), true);
      }
      if (*sfair) {
      for (j = *sfair; j; j--)
        sfair[j] += property.getNumSets () +
          reporter.net.getNumWeaklyFair ();
      // assign the memberships for the intermediate states
      if (*wfair)
        for (j = *prodSucc; j--; )
          c.u->copy (oldCnt + j, sfair);
      else
        memberships (prodSucc, visited, c, s, sfair, prop + 1,
                   minDepth, maxDepth, rgSucc[i]);
      c.l->copy (s, sfair);
      }
      //allocate space for sets of intermediate states
      if (oldCnt < size + c.numTemp)
      c.l->grow (size + c.numTemp);
    }
    delete[] prodSucc;
    delete[] rgSucc;
    c.u->assign (s, stateWeak, property.getNumSets (), true);
  }

  delete[] rg; delete[] prop; delete[] prod;
}

/** Check whether a strongly connected component of the product automaton
 * fulfills the generalized Buchi acceptance conditions
 * @param prop          the property automaton
 * @param states  states of the product automaton
 * @param selfLoops     bit vector of self loop states
 * @param visited map from states to bit vector indices
 * @param numStates     number of states to process, minus 1
 * @return        true if the acceptance condition is fulfilled
 */
static bool
00545 checkBuchi (const class Property& prop,
          const Product::StateStack& states,
          const class BitVector& selfLoops,
          const Product::StateMap& visited,
          unsigned numStates)
{
  /** number of acceptance sets */
  const unsigned numSets = prop.getNumSets ();
  assert (numStates < states.size ());

  if (!numStates) {
    /** product automaton state */
    const class Product::State& state = states.front ();
    /** property automaton state number */
    const unsigned ps = state.prop;
    unsigned d = ::lookup (visited, state);
    for (unsigned s = numSets; s--; )
      if (!prop.accepts (ps, s))
      return false;
    return selfLoops[d];
  }
  else {
    /** Acceptance sets that are visited */
    class BitVector visitedSets (prop.getNumSets ());
    Product::StateStack::const_iterator si = states.begin ();
    for (unsigned i = numStates + 1; i--; ) {
      /** product automaton state */
      const class Product::State& state = *si++;
      /** property automaton state number */
      const unsigned ps = state.prop;
      assert (visited.find (state) != visited.end ());
      for (unsigned s = numSets; s--; )
      if (prop.accepts (ps, s))
        visitedSets.assign (s, true);
    }
    return visitedSets.allSet ();
  }
}

/** Check whether weak fairness holds in a strongly connected component
 * @param reporter      the reachability graph interface
 * @param prop          the property automaton
 * @param states  the successor states in the product automaton
 * @param visited map from states to bit vector indices
 * @param minDepth      minimum Tarjan depth in the component
 * @param maxDepth      maximum Tarjan depth in the component
 * @return        true if the fairness constraints hold
 */
static bool
00594 checkWeaklyFair (class GraphReporter& reporter,
             const class Property& prop,
             const Product::StateStack& states,
             const Product::StateMap& visited,
             unsigned minDepth,
             unsigned maxDepth)
{
  const unsigned numWeak = reporter.net.getNumWeaklyFair ();
  if (!numWeak)
    return true;
  /** States for which a fair transition is enabled */
  class BitVector stateWeak (numWeak);
  /** Looping states for which a fair transition is enabled */
  class BitVector staticWeak (numWeak);

  unsigned numStates = maxDepth - minDepth + 1;
  for (Product::StateStack::const_iterator si = states.begin ();
       numStates--; si++) {
    assert (si != states.end ());
    const class Product::State& state = *si;
    const class PropertyState& propState = prop[state.prop];
    /** Encoded transition instances */
    word_t* data;
    /** Interface for decoding the transition instances */
    class BitUnpacker* u;
    /** Successors in the reachability graph */
    card_t* rgSucc = reporter.prepareFair (state.rg, data, u);
    if (!rgSucc)
      continue;
    for (card_t s = 1; s <= *rgSucc; s++) {
      unsigned* wf = reporter.computeFair (state.rg, u, 0);
      if (!wf) {
      delete[] data;
      delete[] rgSucc;
      return false;
      }
      unsigned nWeak = *wf;

      for (const card_t rgState = rgSucc[s]; nWeak; nWeak--) {
      const unsigned weak = wf[nWeak];
      stateWeak.assign (weak, true);
      for (unsigned i = propState.getNumSuccessors (); i--; ) {
        unsigned d =
	    ::lookup_maybe (visited, Product::State (rgState, propState[i]));
        if (d >= minDepth && d <= maxDepth) {
          staticWeak.assign (weak, true);
          break;
        }
      }
      }
    }

    staticWeak.orNot (stateWeak);
    stateWeak.clear ();
    delete[] data;
    delete[] rgSucc;
  }

  return staticWeak.allSet ();
}

/** Remove all bad states from the component
 * @param c       the component
 * @param l       (working area) the L set (and the Bad set)
 * @param u       (working area) the U set
 * @param removed (output) bit vector of removed states
 * @return        true if any states were removed
 */
inline static bool
00663 removeBad (struct components& c,
         class BitVector& l,
         class BitVector& u,
         class BitVector& removed)
{
  unsigned i, j;
  bool status = false;

  for (;;) {
    l.clear ();
    u.clear ();
    for (i = *c.comp; i; i--) {
      const unsigned node = c.comp[i];
      // compute L
      for (j = c.l->getSize (node); j--; )
      l.assign ((*c.l)[node][j], true);
      // compute U
      for (j = c.u->getSize (node); j--; )
      u.assign ((*c.u)[node][j], true);
    }
    if (!l.andNot (u))
      return status;
    status = true;
    for (i = *c.comp; i; i--) {
      const unsigned node = c.comp[i];
      // compute L
      for (j = c.l->getSize (node); j--; )
      if (l[(*c.l)[node][j]])
        goto remove;
      continue;
    remove:
      removed.assign (node, true);
      c.comp[i] = c.comp[(*c.comp)--];
    }
  }
}

/** Tarjan state */
00701 struct tarjan
{
  /** reachability graph state */
00704   card_t state;
  /** number of unprocessed successors */
00706   unsigned numSucc;
};
/** Stack for Tarjan's algorithm */
00709 typedef slist<struct tarjan> TarjanStack;

/** Flag: has the analysis been interrupted? */
extern volatile bool interrupted;

/** Compute the MSCCs of a component
 * @param c       the transition relation and the component
 * @param compStore     place holder for new MSCCs
 * @param removed bit vector of removed states
 * @param visited (working area) visited states
 * @param modified      (working area) processed states
 * @param compNums      (working area) component numbers
 */
static void
00723 computeMSCC (const struct components& c,
           std::list<unsigned*>& compStore,
           const class BitVector& removed,
           class BitVector& visited,
           class BitVector& processed,
           unsigned* compNums)
{
  /** Current and allocated length of the component stack */
  unsigned cstsize = 0, cstalloc = 128;
  /** Component stack */
  card_t* cst = new card_t[cstalloc];

  TarjanStack st;
  // Combinations for   visited[state]    and   processed[state]:
  // initially                0                 0
  // visited in the search    1                 0
  // visited; depth adjusted  0                 1
  // processed component      1                 1
  visited.clear ();
  processed.clear ();

  /** Search depth */
  unsigned depth = 1;

  for (unsigned k = *c.comp; !interrupted && k; k--) {
    card_t state = c.comp[k];
    unsigned compNr = compNums[state + 1];
    while (!interrupted) {
      // compute a strongly connected component
      while (!interrupted) {
      if (processed[state] || visited.tset (state))
        break;
      // push the state on the component stack
      if (cstsize == cstalloc) {
        if (card_t* ncst = new card_t[cstalloc <<= 1]) {
          memcpy (ncst, cst, cstsize * sizeof *cst);
          delete[] cst; cst = ncst;
        }
        else {
          delete[] cst;
          interrupted = true;
          return;
        }
      }
      cst[cstsize++] = state;
      compNums[state + 1] = depth++;

      // determine the successors of the state
      struct tarjan t = { state, c.trans->getSize (state) };
      for (; t.numSucc; t.numSucc--) {
        unsigned s = (*c.trans)[state][t.numSucc - 1];
        if (visited[s] == processed[s] &&
            (compNums[s + 1] != compNr || removed[s]))
          c.trans->delElement (state, t.numSucc - 1);
        else if (!processed[s] || !visited[s]) {
          state = s;
          break;
        }
      }
      st.push_front (t);
      }

      // backtrack
      while (!interrupted) {
      if (st.empty ())
        goto compDone;
      /** Minimum search depth in the state */
      const card_t minDepth = processed[state] && visited[state]
        ? CARD_T_MAX
        : compNums[state + 1];
      struct tarjan& t = st.front ();
      state = t.state;
      if (compNums[state + 1] > minDepth) {
        compNums[state + 1] = minDepth;
        if (processed.tset (state))
          assert (!visited[state]);
        else
          assert (visited[state]), visited.assign (state, false);
      }
      if (t.numSucc-- > 1) {
        assert (c.trans->getSize (state) > t.numSucc);
        for (; t.numSucc; t.numSucc--) {
          card_t s = (*c.trans)[state][t.numSucc - 1];
          if (visited[s] == processed[s] &&
            (compNums[s + 1] != compNr || removed[s]))
            c.trans->delElement (state, t.numSucc - 1);
          else if (!(processed[s] && visited[s])) {
            state = s;
            break;
          }
        }
        if (t.numSucc)
          break;
      }

      st.pop_front ();

      if (processed[state])
        continue;

      // split the component
      (*compNums)++;
      unsigned i;
      for (i = cstsize;; ) {
        card_t s = cst[--i];
        assert (processed[s] != visited[s]);
        processed.assign (s, true);
        visited.assign (s, true);
        compNums[s + 1] = *compNums;
        if (s == state)
          break;
        assert (i > 0);
      }
      card_t* comp = new card_t[cstsize - i + 1];
      *comp = cstsize - i;
      memcpy (comp + 1, cst + i, (cstsize - i) * sizeof *comp);
      cstsize = i;
      compStore.push_back (comp);
      }
    }
  compDone:
    continue;
  }

  delete[] cst;
}

/** Check whether the strong fairness constraints hold
 * @param c       the transition relation and fairness sets
 * @param selfLoops     bitvector indicating states with arcs to themselves
 * @param size          maximum size of the L and U sets
 * @param maxDepth      maximum Tarjan depth in the component
 * @return        component root, or UINT_MAX if no counterexample
 */
inline static unsigned
00858 checkStreett (struct components& c,
            const class BitVector& selfLoops,
            unsigned size, unsigned maxDepth)
{
  class BitVector l (size);
  class BitVector u (size);
  unsigned ssize = c.trans->getNumSets ();
  class BitVector removed (ssize);
  /** Component numbers for Tarjan's algorithm
   * (index 0 = highest component number) */
  unsigned* compNums =
    reinterpret_cast<unsigned*>(calloc (ssize + 1, sizeof *compNums));
  if (!compNums) return UINT_MAX;
  unsigned i;
  /** Strongly connected component */
  c.comp = new unsigned[ssize + 1];
  for (i = ssize - c.numTemp; i; i--)
    c.comp[i] = ssize - c.numTemp - i;
  for (i = ssize - c.numTemp; i < ssize; i++)
    c.comp[i + 1] = i;
  *c.comp = ssize;

  for (std::list<unsigned*> compStore;;) {
    if (removeBad (c, l, u, removed) && *c.comp) {
      l.setSize (ssize), u.setSize (ssize);
      computeMSCC (c, compStore, removed, l, u, compNums);
      l.setSize (size), u.setSize (size);
    }
    else if (*c.comp &&
           (*c.comp > 1 ||
            (c.comp[1] < ssize - c.numTemp &&
             selfLoops[maxDepth - c.comp[1]]))) {
      // ensure that the component root is not an intermediate state
      for (i = *c.comp; c.comp[i] >= ssize - c.numTemp; i--)
      assert (i > 0); // there must be a non-intermediate state in c.comp
      i = c.comp[i];
      while (!compStore.empty ()) {
      delete[] compStore.front ();
      compStore.pop_front ();
      }
      free (compNums);
      return i;
    }
    delete[] c.comp;
    if (compStore.empty ()) {
      c.comp = 0;
      break;
    }
    c.comp = compStore.front ();
    compStore.pop_front ();
  }

  free (compNums);
  return UINT_MAX;
}

/** Append the traversed path to the counterexample path
 * @param state         the tail state of the path
 * @param unmatchedL    number of encountered unmatched L sets
 * @param c       the component and the fairness sets
 * @param l       encountered L sets
 * @param u       encountered U sets
 * @param father  map from visited states to their ancestors
 * @return        the new counterexample path (product automaton states)
 */
static card_t*
00924 lockPath (unsigned state,
        unsigned& unmatchedL,
        const struct components& c,
        class BitVector& l,
        class BitVector& u,
        unsigned* father,
        card_t* witness)
{
  unsigned size = c.trans->getNumSets (), i;
  /** path being constructed */
  slist<unsigned> path;
  do {
    assert (state < size);
    if (state < size - c.numTemp) // intermediate state?
      path.push_front (state); // no, add to witness path
    for (i = c.u->getSize (state); i--; ) {
      unsigned s = (*c.u)[state][i];
      if (!u.tset (s) && l[s])
      unmatchedL--;
    }
    unsigned t = state;
    state = father[state]; // climb up the path
    father[t] = UINT_MAX; // reset the ancestor relation
  }
  while (state != UINT_MAX && (!*witness || state != witness[*witness]));
  memset (father, 0xff, (size - c.numTemp) * sizeof *father);

  // append the constructed path to the witness path
  i = path.size ();
  card_t* w = new card_t[*witness + i + 1];
  *w = *witness + i;
  memcpy (w + 1, witness + 1, *witness * sizeof *witness);
  delete[] witness; witness = w;
  for (w += *w - i + 1; i--; path.pop_front ())
    *w++ = path.front ();
  return witness;
}

/** Check whether the path can be locked
 * @param state         the tail state of the path
 * @param unmatchedL    number of encountered unmatched L sets
 * @param c       the component and the fairness sets
 * @param l       encountered L sets
 * @param u       encountered U sets
 * @return        true if the path can be locked
 */
static bool
00971 checkState (unsigned state,
          unsigned& unmatchedL,
          const struct components& c,
          class BitVector& l,
          class BitVector& u)
{
  /** flag: can the path be locked? */
  bool lock = false;
  unsigned i, s;
  for (i = c.l->getSize (state); i--; ) {
    s = (*c.l)[state][i];
    if (!l.tset (s)) {
      lock = true;
      if (!u[s])
      unmatchedL++;
    }
  }
  for (i = c.u->getSize (state); i--; ) {
    s = (*c.u)[state][i];
    if (l[s] && !u.tset (s)) {
      lock = true;
      unmatchedL--;
    }
  }
  return lock;
}

/** Determine whether an element belongs to a set
 * @param e the element to be sought
 * @param s array representation of the set (s[1..*s])
 * @return  an index of s[] corresponding to e, or 0 if not found
 */
inline static unsigned
01004 memberIndex (card_t e, const card_t* s)
{
  register const card_t* t = s + *s;
  for (register unsigned i = 1; s++ < t; i++)
    if (*s == e)
      return i;
  return 0;
}

/** Generate a counterexample path
 * @param c       the component and the fairness sets
 * @param root          root state of the component
 * @param size          size of the L and U sets
 */
static card_t*
01019 streettWitness (const struct components& c,
            unsigned root,
            unsigned size)
{
  /** breadth-first search queue */
  std::list<unsigned> bfs;
  /** Encountered L and U sets */
  class BitVector l (size), u (size);
  size = c.trans->getNumSets ();
  assert (size >= 1);
  /** Visited states */
  class BitVector visited (size);
  /** Map from visited states to states through which they were entered */
  unsigned* father = new unsigned[size - c.numTemp];
  /** The witness path */
  card_t* witness = new card_t[1]; *witness = 0;

  /** Number of encountered unmatched L sets */
  unsigned unmatchedL = 0;

  // Display a message here, since the construction can take a long time
  extern class Printer thePrinter;
  thePrinter.printRaw ("constructing counterexample");
  thePrinter.finish ();

  memset (father, 0xff, (size - c.numTemp) * sizeof *father);
  bfs.push_back (root);
  visited.assign (root, true);
  if (checkState (root, unmatchedL, c, l, u))
    witness = lockPath (root, unmatchedL, c, l, u, father, witness);
  if (size == 1) {
    assert (witness && *witness == 1);
    card_t* w = new card_t[3];
    *w = 2, w[1] = w[2] = witness[1];
    delete[] witness;
    delete[] father;
    return w;
  }

  while (!bfs.empty ()) {
    unsigned s = bfs.front ();
    bfs.pop_front ();
    for (unsigned i = c.trans->getSize (s); i--; ) {
      /** flag: lock the path */
      bool lock = false;
      /** successor state */
      unsigned t = (*c.trans)[s][i];
      // if the state is not in a good component, proceed to the next state
      if (c.comp && !memberIndex (t, c.comp)) {
      (*c.trans).delElement (s, i);
      continue;
      }
      if (t >= size - c.numTemp) {
      // intermediate state
      assert (*witness);
      if ((lock = checkState (t, unmatchedL, c, l, u)) &&
          s != witness[*witness])
        witness = lockPath (s, unmatchedL, c, l, u, father, witness);
      t = (*c.trans)[t][0]; // skip to next state
      assert (t < size - c.numTemp);
      }
      if (father[t] == UINT_MAX)
      father[t] = s;
      if (t == root && !unmatchedL) {
      witness = lockPath (t, unmatchedL, c, l, u, father, witness);
      delete[] father;
      return witness;
      }
      else if (checkState (t, unmatchedL, c, l, u) || lock) {
      bfs.clear ();
      visited.clear ();
      if (!*witness || t != witness[*witness] || lock)
        witness = lockPath (t, unmatchedL, c, l, u, father, witness);
      visited.assign (t, true);
      bfs.push_back (t);
      break;
      }
      else if (!visited.tset (t))
      bfs.push_back (t);
    }
  }

  delete[] father;
  delete[] witness;
  assert (false);
  return 0;
}

/** Compute a path leading to the counterexample loop
 * @param visited map of visited states
 * @param maxDepth      maximum Tarjan depth in the component
 * @param witness array containing the loop of the witness
 * @param f       the arc relation files
 */
static void
01114 computePrefix (Product::StateMap& visited,
             unsigned maxDepth,
             card_t *&witness,
             struct files& f)
{
  assert (witness && *witness);
  assert (witness[*witness] == witness[1]);
  /** Transition relation */
  class SetList trans (maxDepth + 1);
  /** breadth-first search queue */
  std::list<unsigned> bfs;
  /** Visited states (indexes are maxDepth - state) */
  class BitVector vis (maxDepth);
  /** Map from visited states to states through which they were entered */
  unsigned* father = new unsigned[maxDepth + 1];
  /** placeholder for reachability graph successors */
  unsigned* rg = new unsigned[2]; *rg = 0;
  /** placeholder for property automaton successors */
  unsigned* prop = new unsigned[2]; *prop = 0;
  /** placeholder for product automaton successors */
  unsigned* prod = new unsigned[1]; *prod = 0;

  memset (father, 0xff, (maxDepth + 1) * sizeof *father);
  unsigned length = 0;

  /* Start the search from the initial state (1) of the product automaton */
  bfs.push_back (1);
  vis.assign (maxDepth - 1, true);

  do {
    unsigned s = bfs.front ();
    bfs.pop_front ();
    length++;
    if (!trans.getSize (s))
      decodeProductArc (visited, trans, maxDepth, s, rg, prop, prod, f);
    for (unsigned i = trans.getSize (s); i--; ) {
      unsigned t = trans[s][i];
      assert (t < maxDepth);
      if (father[t] == UINT_MAX)
      father[t] = maxDepth - s;
      if (unsigned mi = memberIndex (t, witness)) {
      //Construct the witness path
      card_t* w = new card_t[length + *witness + 1];
      *w = length + *witness;
      memcpy (w + length + 1, witness + mi,
            (*witness - mi + 1) * sizeof *w);
      memcpy (w + length + 1 + (*witness - mi + 1), witness + 2,
            (mi - 1) * sizeof (card_t));
      do
        w[length--] = t = father[t];
      while (length && t != UINT_MAX);
      if (t == UINT_MAX) {
        length++;
        memmove (w + 1, w + length + 1, (*w - length) * sizeof *w);
        *w -= length;
      }
      delete[] witness;
      witness = w;
      goto finish;
      }
      else if (!vis.tset (t))
      bfs.push_back (maxDepth - t);
    }
  }
  while (!bfs.empty ());

 finish:
  delete[] rg; delete[] prop; delete[] prod; delete[] father;
}

/** Convert the product automaton states in the witness path
 * to reachability graph states
 * @param states  the product automaton states
 * @param witness the witness path
 */
inline static void
01190 project (Product::StateStack& states,
       card_t* witness)
{
  register card_t* w = witness + *witness + 1;

  while (--w > witness) {
    Product::StateStack::const_iterator psi = states.begin();
    assert (*w < states.size ());
    for (register card_t i = *w; i--; psi++);
    *w = psi->rg;
  }
}

/** Check the product component for a fair counterexample
 * @param reporter      the reachability graph interface
 * @param property      the property automaton
 * @param states  the component
 * @param selfLoops     bitvector indicating states with arcs to themselves
 * @param visited map of visited states
 * @param minDepth      minimum Tarjan depth in the component
 * @param maxDepth      maximum Tarjan depth in the component
 * @param f       the temporary files
 * @return        the counterexample path, or NULL if no counterexample
 */
static card_t*
01215 checkStronglyFair (class GraphReporter& reporter,
               const class Property& property,
               Product::StateStack& states,
               const class BitVector& selfLoops,
               Product::StateMap& visited,
               unsigned minDepth,
               unsigned maxDepth,
               struct files& f)
{
  /** data structure for strong fairness check and counterexample generation */
  struct components c;
  /** root state of the accepting component */
  unsigned root = 0;
  /* recover the transition relation */
  readArcs (f, visited, states, reporter, property, minDepth, maxDepth, c);
  /** maximum size of the L and U sets */
  unsigned size = property.getNumSets () +
    reporter.net.getNumWeaklyFair () +
    reporter.net.getNumStronglyFair ();
  /* check the strong fairness constraints */
  if (reporter.net.getNumStronglyFair () &&
      (root = checkStreett (c, selfLoops, size, maxDepth)) == UINT_MAX) {
    delete c.trans; delete c.l; delete c.u; delete[] c.comp;
    return 0;
  }
  /** counterexample path */
  card_t* witness = streettWitness (c, root, size);
  if (witness) {
    computePrefix (visited, maxDepth, witness, f);
    project (states, witness);
  }
  delete c.trans; delete c.l; delete c.u; delete[] c.comp;
  return witness;
}

/** mix -- mix two 32-bit values
 * Based on lookup2.c, by Bob Jenkins, December 1996, Public Domain.
 * Note that this version assumes that sizeof(unsigned)==4.
 * @param a the first 32-bit value
 * @param b the second 32-bit value
 * @return  a mix of the two values
 */
inline static unsigned
01258 mix (unsigned a, unsigned b)
{
  unsigned c = 0;
  a -= b, a -= c, a ^= c >> 13;
  b -= c, b -= a, b ^= a << 8;
  c -= a, c -= b, c ^= b >> 13;
  a -= b, a -= c, a ^= c >> 12;
  b -= c, b -= a, b ^= a << 16;
  c -= a, c -= b, c ^= b >> 5;
  a -= b, a -= c, a ^= c >> 3;
  b -= c, b -= a, b ^= a << 10;
  c -= a, c -= b, c ^= b >> 15;
  return c;
}

size_t
01274 Product::State::operator() () const
{
  return mix (rg, prop);
}

card_t*
01280 Product::analyze (card_t state) const
{
  assert (!myProp.isFinite ());
  /** Temporary files for the arcs */
  struct files f;
  if (!::openFiles (f)) {
    myReporter.flagFatal ();
    return 0;
  }
  /** Stack of father states (whose children are being investigated) */
  StateStack father;
  /** Stack of child states */
  StateStack children;
  /** Depth-first search stack for Tarjan's algorithm */
  TarjanStack dfs;
  /** Map of visited states for Tarjan's algorithm */
  StateMap visited;
  /** Search depth */
  unsigned depth = 1;

  /** Bit vector indexed by product automaton states: '1'=self loop present */
  class BitVector selfLoops;
  /** Current state of the product automaton */
  class State s (state, myProp.getInitialState ());

  while (!interrupted && !myReporter.isFatal ()) {
    // compute a strongly connected component
    while (!interrupted && !myReporter.isFatal ()) {
      std::pair<StateMap::iterator,bool> p =
      visited.insert (StateMap::value_type (s, depth));
      if (!p.second)
      break;
      father.push_front (s);
      class SearchList& rgSucc = myReporter.getSuccessors (s.rg);

      if (interrupted || myReporter.isFatal ()) {
	::closeFiles (f);
      return 0;
      }

      const unsigned* enabled = myReporter.eval (s.rg, s.prop, myProp[s.prop]);
      if (!enabled) {
	::closeFiles (f);
      return 0;
      }
      assert (*enabled <= myProp[s.prop].getNumSuccessors ());

      if (rgSucc.empty ())
      rgSucc.push (s.rg);     // add a self loop for deadlock state
      SearchList::const_iterator rgSuccBegin = rgSucc.begin ();
      SearchList::const_iterator rgSuccEnd = rgSucc.end ();
      if (!::writeArcs (f, enabled, rgSucc.size (), rgSuccBegin, rgSuccEnd)) {
      myReporter.eval_done (enabled);
	::closeFiles (f);
      myReporter.flagFatal ();
      return 0;
      }

      /** number of enabled successors */
      unsigned numEnabled = *enabled;

      // check for self loops in the product automaton
      for (unsigned pi = numEnabled; pi; pi--) {
      const unsigned propSucc = enabled[pi];
      numEnabled--;
      if (propSucc == s.prop) {
        for (SearchList::const_iterator i = rgSuccBegin; i != rgSuccEnd;
             i++, numEnabled++) {
          class State child (*i, propSucc);
          children.push_front (child);
          if (child.rg == s.rg)
            selfLoops.extend (depth, true);
        }
      }
      else
        for (SearchList::const_iterator i = rgSuccBegin; i != rgSuccEnd;
             i++, numEnabled++)
          children.push_front (State (*i, propSucc));
      }
      rgSucc.clear ();
      myReporter.eval_done (enabled);
      dfs.push_front (Tarjan (s, depth++, numEnabled));
      if (!numEnabled)
      break;

      assert (!children.empty ());
      s = children.front ();
      children.pop_front ();
    }

    if (interrupted || myReporter.isFatal ())
      break;

    /** Minimum search depth in the product state */
    unsigned minDepth = ::lookup (visited, s);

    // backtrack
    for (;;) {
      if (dfs.empty ()) {
	::closeFiles (f);
      return 0;
      }
      class Tarjan& t = dfs.front ();
      unsigned sDepth = t.depth;

      if (minDepth && minDepth < sDepth)
      t.depth = sDepth = minDepth;

      if (t.numSucc-- > 1) {
      assert (!children.empty ());
      s = children.front ();
      children.pop_front ();
      break;
      }

      s = t.state;
      dfs.pop_front ();

      if (sDepth == ::lookup (visited, s)) {
      unsigned maxDepth = ::lookup (visited, father.front ());
      assert (maxDepth >= sDepth);
      selfLoops.setSize (maxDepth + 1);
      if (::checkBuchi (myProp, father, selfLoops,
                    visited, maxDepth - sDepth) &&
          ::checkWeaklyFair (myReporter, myProp, father,
                         visited, sDepth, maxDepth)) {
        if (card_t* witness =
           ::checkStronglyFair (myReporter, myProp, father, selfLoops,
                          visited, sDepth, maxDepth, f)) {
	    ::closeFiles (f);
          return witness;
        }
      }

      for (depth = maxDepth + 1; depth > sDepth; depth--)
        ::lookup_clear (visited, father.front ()), father.pop_front ();

      selfLoops.truncate (depth = sDepth);
      fetchOffsets (f, depth, f.offset);
      fseek (f.directory, -sizeof f.offset, SEEK_CUR);
      fseek (f.aut_succ, f.offset.aut * sizeof (unsigned), SEEK_SET);
      fseek (f.rg_succ, f.offset.rg * sizeof (unsigned), SEEK_SET);
      }
      minDepth = t.depth;
    }
  }

  ::closeFiles (f);
  return 0;
}

Generated by  Doxygen 1.6.0   Back to index