maria 1.3.5-4 / usr / share / maria / runtime / statefcn.h

/** @file runtime/statefcn.h
 * Definitions for encoding and decoding states
 */

/* Copyright © 2000-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. */

#include "mset.h"
#include "codec.h"
#define FCN(f) f##_##state
#include "codecfcn.h"

/** flag: has the analysis been interrupted? (defined in eventpriv.h) */
extern volatile char* intr;
/** flag: has a fatal error occurred? (defined in eventpriv.h) */
extern char* fatal;
/** flag: has modular analysis been disabled? */
char flattened;

/** call-back for adding an encoded state and arcs
 * @param buf		the encoded state
 * @param length	length of the encoded state, in bytes
 * @param err		status of evaluating the reject property
 * @param tr		the index number of the transition that fired
 * @param ftr		the number of the transition in the flattened net
 * @param hide		flag: is the transition hidden?
 * @param ctx		the call-back context
 */
void
(*addstate) (void* buf, size_t length, enum Error err,
	     unsigned tr, unsigned ftr, int hide,
	     void* ctx);

/** number of bits needed for representing
 * the state of the property automaton
 * (0=no property specified) */
unsigned propBits;
/** amount and numbers of successor states of the property automaton */
unsigned* propSucc;

/** current state, tokens bound from input arcs, successor state */
struct marking mSrc, mIn, mDest;

/** array of pointers to multi-set items sorted by multiplicty */
static struct tree** histogram = 0;
/** number of distinct items in the current multi-set (length of histogram) */
static card_t distinct = 0;
/** maximum number of distinct items so far (capacity of the buffer) */
static card_t maxdistinct = 0;

/** sort the multiplicities of a multi-set
 * @param mset	the multi-set to sort
 * @return	total number of items (CARD_T_MAX on error)
 */
static card_t
msort (void* mset)
{
  card_t total = 0;
  unsigned pos = 0, low, high;
  register struct tree* t = mset;
  FIRST (t);
  distinct = 0;
  while (t) {
    register card_t count = t->count;
    if (!count) { NEXT (t); continue; }
    if (count > CARD_T_MAX - total) return CARD_T_MAX;
    total += count;
    if (distinct) {
      for (low = 0, high = distinct; low != high; ) {
	pos = (low + high) >> 1;
	if (histogram[pos]->count > count)
	  high = pos;
	else if (++pos == high)
	  break;
	else
	  low = pos;
      }
      memmove (histogram + pos + 1, histogram + pos,
	       (distinct - pos) * sizeof *histogram);
    }
    if (++distinct > maxdistinct) {
      maxdistinct = distinct;
      if (!histogram)
	histogram = malloc ((maxdistinct + 1) * sizeof *histogram);
      else
	histogram = realloc (histogram, (maxdistinct + 1) * sizeof *histogram);
    }
    histogram[pos] = t;
    NEXT (t);
  }
  return total;
}

/** logarithm of base 2
 * @param num	number whose logarithm is to be computed
 * @return	number of bits required to represent 0..num
 */
static unsigned
log2 (card_t num)
{
#if CARD_T_MAX == 4294967295U
  if (num <= 0x2) return num - 1;
  if (num <= 0x4) return 2;
  if (num <= 0x8) return 3;
  if (num <= 0x10) return 4;
  if (num <= 0x20) return 5;
  if (num <= 0x40) return 6;
  if (num <= 0x80) return 7;
  if (num <= 0x100) return 8;
  if (num <= 0x200) return 9;
  if (num <= 0x400) return 10;
  if (num <= 0x800) return 11;
  if (num <= 0x1000) return 12;
  if (num <= 0x2000) return 13;
  if (num <= 0x4000) return 14;
  if (num <= 0x8000) return 15;
  if (num <= 0x10000) return 16;
  if (num <= 0x20000) return 17;
  if (num <= 0x40000) return 18;
  if (num <= 0x80000) return 19;
  if (num <= 0x100000) return 20;
  if (num <= 0x200000) return 21;
  if (num <= 0x400000) return 22;
  if (num <= 0x800000) return 23;
  if (num <= 0x1000000) return 24;
  if (num <= 0x2000000) return 25;
  if (num <= 0x4000000) return 26;
  if (num <= 0x8000000) return 27;
  if (num <= 0x10000000) return 28;
  if (num <= 0x20000000) return 29;
  if (num <= 0x40000000) return 30;
  if (num <= 0x80000000) return 31;
  return 32;
#else
  unsigned low = 0, high = CARD_T_BIT;

  for (;;) {
    unsigned log = (low + high) >> 1;

    card_t exp = 1u << log;
    if (exp < num) {
      if (low == high)
	return log;
      low = log + 1;
    }
    else if ((exp >> 1) >= num)
      high = log - 1;
    else
      return log;
  }
#endif
}

/** Encode an unconstrained cardinality
 * @param c	the cardinality
 */
static void
encc (card_t c)
{
  if (!c)
    FCN (enc) (0, 1);
  else {
    FCN (enc) (1, 1);
    if (c <= 8)
      FCN (enc) (0, 1), FCN (enc) (c - 1, 3);
    else {
      FCN (enc) (1, 1);
      if (c <= 0x108)
        FCN (enc) (0, 1), FCN (enc) (c - 9, 8);
      else {
        FCN (enc) (1, 1);
        if (c <= 0x10108)
          FCN (enc) (0, 1), FCN (enc) (c - 0x109, 16);
        else
          FCN (enc) (1, 1), FCN (enc) (c, CARD_T_BIT);
      }
    }
  }
}

/** Decode an unconstrained cardinality
 * @return	the cardinality
 */
static card_t
decc (void)
{
  if (!FCN (dec) (1))
    return 0;
  else if (!FCN (dec) (1))
    return 1 + FCN (dec) (3);
  else if (!FCN (dec) (1))
    return 9 + FCN (dec) (8);
  else if (!FCN (dec) (1))
    return 0x109 + FCN (dec) (16);
  else
    return FCN (dec) (CARD_T_BIT);
}

/** Clean up all dynamically allocated data structures for the encoder */
void
cleanup (void)
{
  FCN (cleanup) ();
  free (histogram), histogram = 0, maxdistinct = 0;
}