diff -u --new-file maria/README.modularcheck maria-modularcheck/README.modularcheck --- maria/README.modularcheck 1970-01-01 02:00:00.000000000 +0200 +++ maria-modularcheck/README.modularcheck 2005-07-30 00:23:00.000000000 +0300 @@ -0,0 +1,26 @@ +This patch is a prototype implementation of the modular model checking +algorithm for LTL-X, as described in "LTL Model Checking for Modular +Petri Nets" by Timo Latvala and Marko Mäkelä, to appear in +"Application and Theory of Petri Nets 2004". + +This prototype implementation is distributed as a patch that can be +applied against maria-1.3.5 and hopefully later versions. Known +limitations of the implementation include: + +(1) it does not work for nested modular nets with multiple levels of nesting +(2) the check for livelocks is incomplete: the second depth-first search should + be initiated when s\in F or s=s_0, instead of s\in F and s\in I +(3) the reported error traces are incomplete: see the comment in trace () in + Automata/Product.C + +Until these limitations have been removed (which might never happen), +this implementation will not be included in the main maria code base. + +This patch is Copyright © 2003,2005 Marko Mäkelä (marko.makela@hut.fi). It +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. + +June 20, 2004 (updated July 30, 2005) +Marko Mäkelä diff -u --recursive maria/Automata/Product.C maria-modularcheck/Automata/Product.C --- maria/Automata/Product.C 2003-12-17 13:37:04.000000000 +0200 +++ maria-modularcheck/Automata/Product.C 2004-06-19 20:44:39.000000000 +0300 @@ -1506,3 +1506,232 @@ ::closeFiles (f); return 0; } + +/** Search for a state in a stack + * @param st the stack + * @param s the state + * @return true if st contains s + */ +static bool +contains (const StateStack& st, + const class State& s) +{ + for (StateStack::const_iterator i = st.begin (); i != st.end (); i++) + if (*i == s) + return true; + return false; +} + +/** Construct a counterexample trace + * @param stack1 the first search stack + * @param stack2 the second search stack + * @param child the looping successor state (optional) + */ +static card_t* +trace (const StateStack& stack1, + const StateStack& stack2, + const class State* child) +{ + card_t numStates = stack1.size () + stack2.size () + !!child; + card_t* trace = new card_t[numStates + 1], t; + *trace = t = numStates; + if (child) + trace[t--] = child->rg; + StateStack::const_iterator i; + for (i = stack2.begin (); i != stack2.end (); i++) + trace[t--] = (*i).rg; + /* to do: fill the gap between stack1 and stack2 by breadth first search */ + for (i = stack1.begin (); i != stack1.end (); i++) + trace[t--] = (*i).rg; + assert (!t); + return trace; +} + +/** Determine if there is a hidden transition between two states + * @param reporter the state space interface + * @param src source state number + * @param dest destination state number + * @param visible map of visible transitions + */ +static bool +hidden (const class GraphReporter& reporter, + card_t src, + card_t dest, + const class BitVector& visible) +{ + assert (visible.getSize () == reporter.net.getNumAllTransitions ()); + bool hidden = true; + word_t* data; + if (card_t* succ = reporter.getGraph ().getSuccessors (src, &data)) { + assert (*succ); + class BitUnpacker buf (data); + for (card_t i = 1; i <= *succ; i++) { + const class Transition* transition; + class Valuation v; + reporter.net.decode (buf, transition, v, reporter.isFlattened ()); + if (!visible[transition->getRootIndex ()]) + continue; + hidden = false; + break; + } + + delete[] data; + delete[] succ; + } + else + assert (false); + return hidden; +} + +card_t* +Product::analyze (card_t state, + const class BitVector& visible) const +{ + assert (!myProp.isFinite ()); + assert (myProp.getNumSets () == 1); + assert (myReporter.net.getNumAllTransitions () == visible.getSize ()); + /** Stacks of states */ + StateStack stack1, stack2, mainset; + /** Numbers of processed successors in stack1 */ + std::list succ1; + /** Map of visited states */ + StateMap visited; + StateMap::iterator i; + SearchList::const_iterator si; + + /** Current state of the product automaton */ + class State s (state, myProp.getInitialState ()); + visited.insert (StateMap::value_type (s, 1)); + + modelcheck: + stack1.push_front (s); succ1.push_front (0); + while (!stack1.empty () && !interrupted && !myReporter.isFatal ()) { + assert (!succ1.empty ()); + s = stack1.front (); + class SearchList& rgSucc = myReporter.getSuccessors (s.rg); + if (interrupted || myReporter.isFatal ()) + return 0; + const unsigned* enabled = myReporter.eval (s.rg, s.prop, myProp[s.prop]); + if (!enabled) + return 0; + assert (*enabled <= myProp[s.prop].getNumSuccessors ()); + if (rgSucc.empty ()) + rgSucc.push (s.rg); // add a self loop for deadlock state + /** number of enabled successors */ + unsigned numEnabled = *enabled; + // descend into successors in the product automaton + for (unsigned pi = numEnabled; pi; pi--) { + const unsigned propSucc = enabled[pi]; + numEnabled--; + for (si = rgSucc.begin (); si != rgSucc.end (); si++, numEnabled++) { + class State child (*si, propSucc); + i = visited.find (child); + if (i == visited.end ()) + visited.insert (StateMap::value_type (child, 1)); + else if (!(i->second & 1)) + i->second |= 1; + else + continue; + if (numEnabled < succ1.front ()) + continue; + // update the number of processed successors for s + succ1.pop_front (); succ1.push_front (numEnabled); + // push the successor on the stack and check it + s = child; + rgSucc.clear (); + myReporter.eval_done (enabled); + goto modelcheck; + } + } + rgSucc.clear (); + myReporter.eval_done (enabled); + + s = stack1.front (); + const bool mc = myProp.accepts (s.prop, 0); + if (!mc) { + class GlobalMarking* m = myReporter.getGraph ().fetchState (s.rg); + const bool accepts = myProp.accepts (s.prop, *m); + delete m; + if (!accepts) + goto nocycle; + } + // check for cycles + assert (mainset.empty ()); + mainset.push_front (s); + while (!mainset.empty ()) { + assert (stack2.empty ()); + s = mainset.front (); mainset.pop_front (); + i = visited.find (s); + if (i == visited.end ()) + visited.insert (StateMap::value_type (s, 2)); + else if (!(i->second & 2)) + i->second |= 2; + else + continue; + stack2.push_front (s); + while (!stack2.empty () && !interrupted && !myReporter.isFatal ()) { + s = stack2.front (); + class SearchList& rgSucc = myReporter.getSuccessors (s.rg); + if (interrupted || myReporter.isFatal ()) + return 0; + const unsigned* enabled = myReporter.eval (s.rg, s.prop, + myProp[s.prop]); + if (!enabled) + return 0; + assert (*enabled <= myProp[s.prop].getNumSuccessors ()); + if (rgSucc.empty ()) + rgSucc.push (s.rg); // add a self loop for deadlock state + /** number of enabled successors */ + unsigned numEnabled = *enabled; + // descend into successors in the product automaton + for (unsigned pi = numEnabled; pi; pi--) { + const unsigned propSucc = enabled[pi]; + numEnabled--; + for (si = rgSucc.begin (); si != rgSucc.end (); si++, numEnabled++) { + class State child (*si, propSucc); + // check the successor + if (mc && ::contains (stack1, child)) { + rgSucc.clear (); + myReporter.eval_done (enabled); + return ::trace (stack1, stack2, &child); + } + i = visited.find (child); + if (i == visited.end () || !(i->second & 2)) { + if (::hidden (myReporter, s.rg, child.rg, visible)) { + if (i == visited.end ()) + visited.insert (StateMap::value_type (child, 2)); + else + i->second |= 2; + stack2.push_front (child); + } + else + mainset.push_front (child); + } + else if (::hidden (myReporter, s.rg, child.rg, visible) && + ::contains (stack2, child)) { + class GlobalMarking* m = + myReporter.getGraph ().fetchState (s.rg); + const bool accepts = myProp.accepts (s.prop, *m); + delete m; + if (accepts) { + rgSucc.clear (); + myReporter.eval_done (enabled); + return ::trace (stack1, stack2, 0); + } + } + } + } + rgSucc.clear (); + myReporter.eval_done (enabled); + stack2.pop_front (); + } + if (!mc) { + mainset.clear (); + break; + } + } + nocycle: + stack1.pop_front (); succ1.pop_front (); + } + return 0; +} diff -u --recursive maria/Automata/Product.h maria-modularcheck/Automata/Product.h --- maria/Automata/Product.h 2003-12-17 13:37:04.000000000 +0200 +++ maria-modularcheck/Automata/Product.h 2004-06-19 20:44:39.000000000 +0300 @@ -66,6 +66,16 @@ */ card_t* analyze (card_t state) const; + /** Check whether the property expressed by the property automaton holds, + * calculating the product of the reachability graph and the automaton, + * performing on-the-fly analysis in a modular model + * @param state number of the state where to start the analysis + * @param visible map of visible transitions + * @return the counterexample path, or NULL if the propery holds + */ + card_t* analyze (card_t state, + const class BitVector& visible) const; + private: /** The reachability graph */ class GraphReporter& myReporter; diff -u --recursive maria/Automata/Property.C maria-modularcheck/Automata/Property.C --- maria/Automata/Property.C 2003-12-17 13:37:04.000000000 +0200 +++ maria-modularcheck/Automata/Property.C 2004-06-19 20:44:39.000000000 +0300 @@ -34,6 +34,7 @@ # include # endif // __DECCXX #endif // BUILTIN_LTL +#include #include #include #include @@ -62,9 +63,13 @@ #include "Constant.h" #include "BooleanBinop.h" #include "NotExpression.h" +#include "PlaceContents.h" #include "LeafValue.h" #include "BoolType.h" #include "Net.h" +#include "Transition.h" +#include "Place.h" +#include "Arc.h" /** @file Property.C * Automaton representing the negation of a property being verified @@ -808,3 +813,210 @@ return 0; #endif // BUILTIN_LTL } + +/** Mark places */ +static bool +markPlaces (const class Expression& expr, + void* data) +{ + if (expr.getKind () == Expression::ePlaceContents) + static_cast(data)->assign + (static_cast(expr).getPlace ().getIndex (), + true); + return true; +} + +class BitVector* +Property::computeVisible (const class Net& net) const +{ + /** index of visible places */ + class BitVector visiblePlaces (net.getNumPlaces ()); + unsigned i; + // mark the visible places + for (i = myNumExprs; i--; ) + if (!myExprs[i]->forExpressions (&::markPlaces, &visiblePlaces)) + assert (false); + // mark the transitions attached to the marked places + class BitVector* visibleTransitions = + new class BitVector (net.getNumAllTransitions ()); + for (i = net.getNumAllTransitions (); i--; ) { + const class Transition& t = net.getTransition (i); + unsigned j; + for (j = t.getNumInputs (); j--; ) { + if (!visiblePlaces[t.getInput (j).getIndex ()]) + continue; + visibleTransitions->assign (i, true); + break; + } + } + return visibleTransitions; +} + +/** Tarjan state */ +struct tarjan +{ + /** state in the automaton */ + unsigned state; + /** number of unprocessed successors */ + unsigned numSucc; +}; + +/** Stack for Tarjan's algorithm */ +typedef std::list TarjanStack; + +/** Flag: has the analysis been interrupted? */ +extern volatile bool interrupted; + +bool +Property::accepts (unsigned state, + const class GlobalMarking& m) const +{ + assert (!isFinite ()); + /** Valuation for evaluating the gates */ + class Valuation valuation; + valuation.setGlobalMarking (&m); + TarjanStack st; + /** Visited states */ + class BitVector visited (myNumStates); + /** States belonging to a component */ + class BitVector processed (myNumStates); + // 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 + /** Search depth numbers */ + unsigned* depths = new unsigned[myNumStates]; + /** Search depth */ + unsigned depth = 1; + /** Current and allocated length of the component stack */ + unsigned cstsize = 0, cstalloc = 128; + /** Component stack */ + unsigned* cst = new unsigned[cstalloc]; + /** Successor state numbers */ + unsigned* succ; + memset (depths, 0, myNumStates * sizeof *depths); + + while (!interrupted) { + // compute a strongly connected component + while (!interrupted) { + assert (!processed[state] || !visited[state]); + if (processed[state] || visited.tset (state)) + break; + // push the state on the component stack + if (cstsize == cstalloc) { + if (unsigned* ncst = new unsigned[cstalloc <<= 1]) { + memcpy (ncst, cst, cstsize * sizeof *cst); + delete[] cst; cst = ncst; + } + else { + delete[] cst; + delete[] depths; + interrupted = true; + return false; + } + } + cst[cstsize++] = state; + + // determine the successors of the state + myStates[state].eval (valuation, succ); + depths[state] = ++depth; + struct tarjan t = { state, succ ? *succ : 0 }; + for (; t.numSucc; t.numSucc--) { + unsigned s = succ[t.numSucc]; + if (!(processed[s] && visited[s])) { + state = s; + break; + } + } + delete[] succ; + st.push_front (t); + } + + // backtrack + while (!interrupted) { + if (st.empty ()) { + lastComponent: + if (cstsize == 1) { + /* A component consisting of a single node + * may or may not be a self-loop, + * so we have to check it. */ + myStates[*cst].eval (valuation, succ); + unsigned i = succ ? *succ : 0; + for (; i; i--) { + if (succ[i] == *cst) + goto selfloop; + } + /* no self-loop found */ + delete[] succ; + delete[] cst; + return false; + selfloop: + delete[] succ; + } + /** Acceptance sets visited in the currently processed component */ + class BitVector accepted (myNumSets); + // see if all acceptance sets are part of the component + while (cstsize--) { + const unsigned s = cst[cstsize] * myNumSets; + for (unsigned i = myNumSets; i--; ) + if ((*myStatesAccept)[s + i]) + accepted.assign (i, true); + } + delete[] cst; + return accepted.allSet (); + } + /** Minimum search depth in the state */ + const unsigned minDepth = processed[state] && visited[state] + ? UINT_MAX + : depths[state] - 1; + struct tarjan& t = *st.begin (); + state = t.state; + if ((depths[state] - 1) > minDepth) { + depths[state] = minDepth + 1; + if (processed.tset (state)) + assert (!visited[state]); + else + assert (visited[state]), visited.assign (state, false); + } + + if (t.numSucc-- > 1) { + myStates[state].eval (valuation, succ); + assert (succ && *succ > t.numSucc); + for (; t.numSucc; t.numSucc--) { + unsigned s = succ[t.numSucc]; + if (!(processed[s] && visited[s])) { + state = s; + break; + } + } + delete[] succ; + if (t.numSucc) + break; + } + + st.pop_front (); + + if (processed[state]) + continue; + // completed a strongly connected component: mark the states + unsigned i = cstsize; + while (i--) { + unsigned s = cst[i]; + assert (!processed[s] || !visited[s]); + processed.assign (s, true); + visited.assign (s, true); + if (s == state) + break; + assert (i > 0); + } + if (!i) + goto lastComponent; + cstsize = i; + } + } + + delete[] cst; + delete[] depths; + return false; +} diff -u --recursive maria/Automata/Property.h maria-modularcheck/Automata/Property.h --- maria/Automata/Property.h 2003-12-17 13:37:04.000000000 +0200 +++ maria-modularcheck/Automata/Property.h 2004-06-19 20:45:43.000000000 +0300 @@ -13,7 +13,7 @@ * Automaton representing the negation of a property being verified */ -/* Copyright © 1999-2002 Marko Mäkelä (msmakela@tcs.hut.fi). +/* Copyright © 1999-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. @@ -129,6 +129,22 @@ /** Determine whether the automaton is a finite-word automaton */ bool isFinite () const { return !myNumSets; } + /** Compute the set of transitions that may affect + * the truth values of the atomic propositions + * @param net the net the atomic propositions refer to + * @return a bit vector indicating visible transitions + */ + class BitVector* computeVisible (const class Net& net) const; + + /** Determine whether the automaton accepts an infinite repetition + * of the current state of the model + * @param state start state in the automaton + * @param m the current state of the model + * @return true if the infinite repetition is accepted + */ + bool accepts (unsigned state, + const class GlobalMarking& m) const; + private: # ifdef BUILTIN_LTL /** Flag: is the formula negated? */ diff -u --recursive maria/parser/maria.C maria-modularcheck/parser/maria.C --- maria/parser/maria.C 2004-01-25 01:10:04.000000000 +0200 +++ maria-modularcheck/parser/maria.C 2004-06-19 20:44:39.000000000 +0300 @@ -1458,7 +1460,13 @@ #endif /* EXPR_COMPILE */ if (verbose) fprintf (stderr, "%s:performing model checking\n", netname); - counterexample = product.analyze (state); + if (graphreporter->isFlattened ()) + counterexample = product.analyze (state); + else { + class BitVector* visible = property.computeVisible (*net); + counterexample = product.analyze (state, *visible); + delete visible; + } graphreporter->setAddOld (false); #ifdef EXPR_COMPILE if (compilation)