/usr/share/maria/runtime/statefcn.h is in maria 1.3.5-4.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 | /** @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;
}
|