// Collection of synchronisation states -*- c++ -*-

#ifdef __GNUC__
# pragma implementation
#endif // __GNUC__
#include "SyncStates.h"
#include "Net.h"
#include "Transition.h"
#include "GlobalMarking.h"
#include "StateReporter.h"

#ifdef ADD_CACHE
# include "FullSet.h"
#endif // ADD_CACHE

/** @file SyncStates.C
 * Collection of synchronisation states for modular analysis
 */

/* Copyright  2002-2003 Marko Mkel (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. */

SyncStates::SyncStates (const class Net& net) :
  myNumModules (net.getNumChildren ()),
  myTransitionMap (),
#ifdef SYNC_CACHE
  myStateMap (new StateMap[myNumModules]),
  myStateSet (0), myStateIndex (new unsigned[myNumModules]),
  myStateUsed (0), myStateAlloc (0)
#else // SYNC_CACHE
  myStateSet (0), myEnabled (0)
#endif // SYNC_CACHE
#ifdef ADD_CACHE
  , mySync (net.getParent () ? 0 : new class FullSet ())
#endif // ADD_CACHE
{
  assert (myNumModules > 0);
  unsigned i = net.getNumTransitions (), numLabels = 0;
  while (i--) {
    const class Transition& t = net.getTransition (i);
    if (t.getNumChildren ())
      const_cast<TransitionMap&>(myTransitionMap).insert
	(TransitionMap::value_type (&t, numLabels++));
  }
#ifdef SYNC_CACHE
  for (i = myNumModules; i--; )
    myStateIndex[i] = UINT_MAX;
#else // SYNC_CACHE
  *const_cast<StateSet***>(&myStateSet) =
    new StateSet*[myNumModules * numLabels];
  memset (myStateSet, 0, myNumModules * numLabels * sizeof *myStateSet);
  *const_cast<bool**>(&myEnabled) = new bool[numLabels];
  memset (myEnabled, 0, numLabels * sizeof *myEnabled);
#endif // SYNC_CACHE
#ifdef ADD_CACHE
  if (mySync && !mySync->init (false))
    assert (false);
#endif // ADD_CACHE
}

SyncStates::~SyncStates ()
{
#ifdef SYNC_CACHE
  for (StateMap* sm = myStateMap + myNumModules; sm-- > myStateMap; )
    for (StateMap::iterator si = sm->begin (); si != sm->end (); si++)
      delete[] si->first;
  delete[] myStateMap;
  if (myStateSet) {
    for (unsigned i = myStateUsed; i--; ) {
      if (!myStateSet[i])
	continue;
      for (StateSet::iterator j = myStateSet[i]->begin ();
	   j != myStateSet[i]->end (); j++)
	delete[] *j;
      delete myStateSet[i];
    }
    delete[] myStateSet;
  }
  else
    assert (!myStateUsed);
  delete[] myStateIndex;
#else // SYNC_CACHE
  for (unsigned i = myNumModules * myTransitionMap.size (); i--; ) {
    if (!myStateSet[i])
      continue;
    for (StateSet::iterator j = myStateSet[i]->begin ();
	 j != myStateSet[i]->end (); j++)
      delete[] *j;
    delete myStateSet[i];
  }
  delete[] myStateSet;
  delete[] myEnabled;
#endif // SYNC_CACHE
#ifdef ADD_CACHE
  delete mySync;
#endif // ADD_CACHE
}

/** Copy a state
 * @param buf	the state
 * @param size	length of the state in words
 * @return	a copy of the state, tagged with its length
 */
static word_t*
copy (const word_t* buf,
      word_t size)
{
  word_t* s = new word_t[size + 1];
  *s = size;
  memcpy (s + 1, buf, size * sizeof *buf);
  return s;
}

#ifdef SYNC_CACHE
bool
SyncStates::lookup (unsigned module,
		    const word_t* buf,
		    word_t size)
{
  word_t* state = ::copy (buf, size);
  std::pair<StateMap::iterator,bool> p =
    myStateMap[module].insert (StateMap::value_type (state, myStateUsed));
  if (!p.second) {
    delete[] state;
    myStateIndex[module] = p.first->second;
    return true;
  }
  // new source state: add it to the cache
  myStateIndex[module] = myStateUsed;
  myStateUsed += myTransitionMap.size ();
  // expand myStateSet[] if needed
  if (myStateAlloc < myStateUsed) {
    unsigned ssize = myStateAlloc ? myStateAlloc << 1 : 1;
    while (ssize < myStateUsed) ssize <<= 1;
    StateSet** s = new StateSet*[ssize];
    memcpy (s, myStateSet, myStateAlloc * sizeof *s);
    memset (s + myStateAlloc, 0, (ssize - myStateAlloc) * sizeof *s);
    delete[] myStateSet;
    myStateSet = s;
    myStateAlloc = ssize;
  }
  return false;
}
#else // SYNC_CACHE
void
SyncStates::cleanup ()
{
  memset (myEnabled, 0, myTransitionMap.size () * sizeof *myEnabled);
  for (unsigned i = myNumModules * myTransitionMap.size (); i--; ) {
    if (myStateSet[i]) {
      for (StateSet::iterator j = myStateSet[i]->begin ();
	   j != myStateSet[i]->end (); j++)
	delete[] *j;
      delete myStateSet[i];
      myStateSet[i] = 0;
    }
  }
}
#endif // SYNC_CACHE

void
SyncStates::add (const class Transition& transition,
		 const word_t* buf,
		 word_t size)
{
  assert (transition.getNumParents ());
  assert (&transition.getNet ()->getParent ()->getChild
	  (transition.getNet ()->getParentIndex ()) == transition.getNet ());
  assert (transition.getNet ()->getParentIndex () < myNumModules);

  for (unsigned parent = transition.getNumParents (); parent--; ) {
    TransitionMap::const_iterator i =
      myTransitionMap.find (&transition.getParent (parent));
    assert (i != myTransitionMap.end ());
#ifdef SYNC_CACHE
    StateSet*& s =
      myStateSet[myStateIndex[transition.getNet ()->getParentIndex ()] +
		 i->second];
#else // SYNC_CACHE
    const unsigned ti = i->second;
    myEnabled[ti] = true;
    StateSet*& s =
      myStateSet[transition.getNet ()->getParentIndex () + myNumModules * ti];
#endif // SYNC_CACHE
    if (!s)
      s = new StateSet ();
    // for simplicity, copy the state for each label the transition exports
    word_t* state = ::copy (buf, size);
    std::pair<StateSet::iterator,bool> p = s->insert (state);
    if (!p.second)
      delete[] state;
  }
}

/** Synchronise on a label
 * @param child		number of the child transition being checked
 * @param transition	the synchronisation label
 * @param ss		the local synchronisation states
 * @param ssi		base indexes to ss[], indexed by module
 * @param ti		index number of the synchronisation label
 * @param m		the source marking
 * @param tibits	number of bits for representing sync labels
 * @param syncset	set of already encountered sync states
 * @param buf		buffer for encoding states
 * @param reporter	the interface for reporting successor states
 */
static void
sync (unsigned child,
      const class Transition& transition,
      SyncStates::StateSet** ss,
#ifdef SYNC_CACHE
      const unsigned* ssi,
      unsigned ti,
#elif defined ADD_CACHE
      unsigned ti,
#endif // SYNC_CACHE
      class GlobalMarking& m,
#ifdef ADD_CACHE
      unsigned tibits,
      class FullSet* syncset,
#endif // ADD_CACHE
      class BitPacker& buf,
      class StateReporter& reporter)
{
  if (child < transition.getNumChildren ()) {
    const class Net& net = *transition.getChild (child).getNet ();
    assert (&net.getParent ()->getChild (net.getParentIndex ()) == &net);

#ifdef SYNC_CACHE
    if (ssi[net.getParentIndex ()] == UINT_MAX);
    else if (const SyncStates::StateSet* sset =
	     ss[ssi[net.getParentIndex ()] + ti])
#else // SYNC_CACHE
    if (const SyncStates::StateSet* sset = ss[net.getParentIndex ()])
#endif // SYNC_CACHE
    {
      for (SyncStates::StateSet::const_iterator i = sset->begin ();
	   i != sset->end (); i++) {
	m.decode (net, (*i) + 1);
	sync (child + 1, transition, ss,
#ifdef SYNC_CACHE
	      ssi, ti,
#elif defined ADD_CACHE
	      ti,
#endif // SYNC_CACHE
	      m,
#ifdef ADD_CACHE
	      tibits, syncset,
#endif // ADD_CACHE
	      buf, reporter);
      }
    }
  }
  else {
#ifdef ADD_CACHE
    if (syncset) {
      buf.clear ();
      if (!m.encode (buf, *transition.getNet ()->getInitMarking (), 0))
	assert (false); // rejected source state
      buf.append (ti, tibits);
      buf.deflate ();
      if (!syncset->add (buf.getBuf (), buf.getNumBytes ())) {
	reporter.enabled (transition);
	return; // this transition has been analysed in the state
      }
      else {
	// we do not need a search queue: we just want to eliminate duplicates
	size_t size;
	delete[] syncset->pop (false, size);
	assert (!syncset->pop (false, size));
      }
    }
#endif // ADD_CACHE
    buf.clear ();
    if (!m.encode (buf, *transition.getNet ()->getInitMarking (), 0))
      assert (false); // rejected source state
    word_t* s = new word_t[buf.getNumWords ()];
    memcpy (s, buf.getBuf (), buf.getNumWords () * sizeof *s);
    reporter.setSyncSource (s, buf.getNumBytes ());
    transition.analyze (m, reporter);
  }
}

void
SyncStates::sync (const class GlobalMarking& m,
		  const class Transition& transition,
		  class StateReporter& reporter) const
{
  assert (transition.getNumChildren () > 0);
  assert (myTransitionMap.find (&transition) != myTransitionMap.end ());
  class GlobalMarking succ (m);
  class BitPacker buf;
#ifndef SYNC_CACHE
  if (!myEnabled[myTransitionMap.find (&transition)->second])
    return;
#endif // SYNC_CACHE
  ::sync (0, transition,
#ifdef SYNC_CACHE
	  myStateSet, myStateIndex,
	  myTransitionMap.find (&transition)->second,
#else // SYNC_CACHE
	  myStateSet + myNumModules *
	  myTransitionMap.find (&transition)->second,
# ifdef ADD_CACHE
	  myTransitionMap.find (&transition)->second,
# endif // ADD_CACHE
#endif // SYNC_CACHE
	  succ,
#ifdef ADD_CACHE
	  mySync ? ::log2 (myTransitionMap.size ()) : 0, mySync,
#endif // ADD_CACHE
	  buf, reporter);
}

#ifdef EXPR_COMPILE
# include "Compilation.h"

/** Synchronise on a label
 * @param child		number of the child transition being checked
 * @param transition	the synchronisation label
 * @param ss		the local synchronisation states
 * @param ssi		base indexes to ss[], indexed by module
 * @param ti		index number of the synchronisation label
 * @param tibits	number of bits for representing sync labels
 * @param syncset	set of already encountered sync states
 * @param reporter	the interface for reporting successor states
 * @param srcs		encoded deflated states (for restoring the state)
 */
static void
sync (unsigned child,
      const class Transition& transition,
      SyncStates::StateSet** ss,
#ifdef SYNC_CACHE
      const unsigned* ssi,
      unsigned ti,
#elif defined ADD_CACHE
      unsigned ti,
#endif // SYNC_CACHE
#ifdef ADD_CACHE
      unsigned tibits,
      class FullSet* syncset,
#endif // ADD_CACHE
      class StateReporter& reporter,
      word_t** srcs)
{
  if (child < transition.getNumChildren ()) {
    const class Net& net = *transition.getChild (child).getNet ();
    assert (&net.getParent ()->getChild (net.getParentIndex ()) == &net);

#ifdef SYNC_CACHE
    if (ssi[net.getParentIndex ()] == UINT_MAX);
    else if (const SyncStates::StateSet* sset =
	     ss[ssi[net.getParentIndex ()] + ti])
#else // SYNC_CACHE
    if (const SyncStates::StateSet* sset = ss[net.getParentIndex ()])
#endif // SYNC_CACHE
    {
      for (SyncStates::StateSet::const_iterator i = sset->begin ();
	   i != sset->end (); i++) {
	reporter.myCompilation->stateDecode (net.getIndex (), (*i) + 1, 0);
	sync (child + 1, transition, ss,
#ifdef SYNC_CACHE
	      ssi, ti,
#elif defined ADD_CACHE
	      ti,
#endif // SYNC_CACHE
#ifdef ADD_CACHE
	      tibits, syncset,
#endif // ADD_CACHE
	      reporter, srcs);
      }
      reporter.myCompilation->stateDecode (net.getIndex (),
					   srcs[net.getParentIndex ()], 0);
    }
  }
  else {
#ifdef ADD_CACHE
    if (syncset) {
      unsigned bytes;
      const void* buf = reporter.myCompilation->stateProject
	(transition.getNet ()->getIndex (), ti, tibits, bytes);
      if (!syncset->add (buf, bytes)) {
	reporter.enabled (transition);
	return; // this transition has been analysed in the state
      }
      else {
	// we do not need a search queue: we just want to eliminate duplicates
	size_t size;
	delete[] syncset->pop (false, size);
	assert (!syncset->pop (false, size));
      }
    }
#endif // ADD_CACHE
    reporter.sync (transition);
  }
}

void
SyncStates::sync (const class Transition& transition,
		  class StateReporter& reporter,
		  word_t** srcs) const
{
  assert (transition.getNumChildren () > 0);
  assert (myTransitionMap.find (&transition) != myTransitionMap.end ());
#ifndef SYNC_CACHE
  if (!myEnabled[myTransitionMap.find (&transition)->second])
    return;
#endif // SYNC_CACHE
  ::sync (0, transition,
#ifdef SYNC_CACHE
	  myStateSet, myStateIndex,
	  myTransitionMap.find (&transition)->second,
#else // SYNC_CACHE
	  myStateSet + myNumModules *
	  myTransitionMap.find (&transition)->second,
# ifdef ADD_CACHE
	  myTransitionMap.find (&transition)->second,
# endif // ADD_CACHE
#endif // SYNC_CACHE
#ifdef ADD_CACHE
	  mySync ? ::log2 (myTransitionMap.size ()) : 0, mySync,
#endif // ADD_CACHE
	  reporter, srcs);
}
#endif // EXPR_COMPILE