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
|
/** @file runtime/event.h
* Common definitions for code generated for transitions
*/
/* Copyright 2000-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. */
/** flag: has the analysis been interrupted? */
extern volatile char* intr;
/** flag: has a fatal error occurred? */
extern char* fatal;
/** flag: generate arcs? */
extern char arcs;
/** flag: generate a flat state space? */
extern char flat;
/** weak fairness sets */
extern unsigned wfair[];
/** strong fairness sets */
extern unsigned sfair[];
/** encode the marking and add an event from the current state to it
* @param net the net the transition belongs to (0=root)
* @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 to the state hidden?
* @param ctx the call-back context
*/
enum Error
encode (unsigned net, unsigned tr, unsigned ftr, int hide, void* ctx);
/** call-back for reporting an enabled synchronising transition
* @param tr the index number of the transition
* @param ctx the call-back context
*/
extern void
(*syncstate) (unsigned tr, void* ctx);
/** append data to the event encoding buffer
* @param data data to append
* @param bits number of bits (data < 1 << bits)
*/
extern void
enc (card_t data, unsigned bits);
/** extract data from the event encoding buffer
* @param bits number of bits to extract
* @return the extracted data (< 1 << bits)
*/
extern card_t
dec (unsigned bits);
/** clear the event encoding buffer */
extern void
event_clear (void);
/** clean up the event encoding buffer */
extern void
event_cleanup (void);
/** set up and inflate the event decoding buffer
* @param buf the decoding buffer
* @param bytes length of the decoding buffer
*/
extern void
inflate (void* buf, size_t bytes);
/** deflate the event encoding buffer
* @param size (output) number of bytes in the encoded buffer
* @return the start address of the encoding buffer
*/
extern void*
deflate (size_t *size);
/** decode an event and compute the fairness sets
* @param sf flag: compute strong fairness constraints
* @return number of the transition
*/
extern enum Error
event_decode (unsigned sf);
/** See if an optional variable has been assigned a value
* @param i the bit vector holding the "assigned" statuses
* @param v index number of the variable
*/
#define ASSIGNED(i,v) (i.y[v / sizeof *i.y] & (1 << (v % sizeof *i.y)))
/** Flag that an optional variable has been assigned a value
* @param i the bit vector holding the "assigned" statuses
* @param v index number of the variable
*/
#define ASSIGN(i,v) (i.y[v / sizeof *i.y] |= (1 << (v % sizeof *i.y)))
/** Flag that an optional variable has no assigned value
* @param i the bit vector holding the "assigned" statuses
* @param v index number of the variable
*/
#define DEASSIGN(i,v) (i.y[v / sizeof *i.y] &= ~(1 << (v % sizeof *i.y)))
|
