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
|
// Labelled state transition system output interface -*- c++ -*-
#ifndef LSTS_H_
# define LSTS_H_
# ifdef __GNUC__
# pragma interface
# endif // __GNUC__
# include "BitBuffer.h"
# include <set>
# include <stdio.h>
/** @file LSTS.h
* Labelled state transition system output interface
*/
/* Copyright 2001-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. */
/** Interface for outputting labelled state transition systems */
class LSTS
{
public:
/** Less-than comparison for encoded actions */
struct ltact
{
/** Compare two encoded actions (length-tagged memory areas)
* @param a1 first action to compare
* @param a2 second action to compare
* @return true if act1 sorts before act2
*/
bool operator () (const size_t* a1, const size_t* a2) const {
return *a1 < *a2 || (*a1 == *a2 && memcmp (a1 + 2, a2 + 2, *a1) < 0);
}
};
/** Set of encoded actions */
typedef std::set<size_t*,struct ltact> Set;
/** Constructor
* @param net the net
* @param filebase base name for the files
*/
LSTS (const class Net& net,
const char* filebase);
private:
/** Copy constructor */
LSTS (const class LSTS& old);
/** Assignment operator */
class LSTS& operator= (const class LSTS& old);
public:
/** Destructor */
~LSTS ();
/** Open the files
* @return true on success (otherwise display diagnostics)
*/
bool openFiles ();
/** Dump a state
* @param m representation of the state
* @param state number of the state
*/
void outputState (const class GlobalMarking& m, card_t state);
# ifdef EXPR_COMPILE
/** Dump a state
* @param compilation the compilation for evaluating state properties
* @param state number of the state
*/
void outputState (const class Compilation& compilation, card_t state);
# endif // EXPR_COMPILE
/** Dump an arc
* @param source source state number
* @param target target state number
* @param transition the high-level transition
* @param valuation values for the transition variables
*/
void outputArc (card_t source,
card_t target,
const class Transition& transition,
const class Valuation& valuation);
/** Dump the arcs
* @param graph the graph whose arcs these are
* @param source source state number
* @param targets amount and numbers of target states
* @param buf encoded transition names and instances (inflated)
*/
void outputArcs (const class Graph& graph,
card_t source,
const card_t* targets,
word_t* buf);
private:
/** The net whose reachability graph is being processed */
const class Net& myNet;
/** Base name for the files */
char* myFilebase;
/** Number of state propositions */
const unsigned myNumProps;
/** Number of generated states */
unsigned myNumStates;
/** Number of generated transitions */
unsigned myNumTransitions;
/** Actions generated so far */
Set myActionSet;
/** Output streams for state proposition truth tables */
FILE** const myProps;
/** Output stream for LSTS transitions (reachability graph arcs) */
FILE* myTransitions;
/** Output stream for named LSTS actions (Petri net transition instances) */
FILE* myActions;
/** Output stream for the LSTS index */
FILE* myIndex;
};
#endif // LSTS_H_
|
