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
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
|
Maria NEWS -- history of user-visible changes. 29th July 2005
Copyright 2002,2003,2004,2005 Marko Mkel
See the end for copying conditions.
* Maria 1.3.5 is a maintenance release with performance and portability fixes
** Identified performance bottlenecks with OProfile on GNU/Linux x86
*** Wrote non-looping log() functions for systems with 32-bit card_t.
The function is 2 to 3 times faster than the original. This improvement
may reduce the time for state space exploration by a couple of percent.
*** In interpreter-based operation, dynamic memory management consumes
almost half the execution time. This is a fundamental problem of the
expression evaluator, which makes extensive use of dynamic memory allocation.
*** In compiler-based operation, decoding and encoding states may consume
80% of the time spent in compiled code, depending on the data types used in
place markings and the number and complexity of the transitions. This may
amount to 10-20% of the total execution time, depending on the state storage
method and other options chosen.
*** The built-in LTL formula translator has been updated to lbt-1.2.2.
** Portability fixes
*** Replaced the non-standard slist template with std::list.
** Bug fixes
*** The output of error traces in graphless search leaked memory.
*** Memory could be leaked when an error was detected during
transition instance analysis.
*** Transition identifiers were improperly encoded by generated C code
in modular state space exploration.
*** The output of "dump" differed from "visual dump".
Thanks to Charles Lakos for pointing out the problem.
* Maria 1.3.4 is a maintenance release with bug fixes
mainly for modular state space exploration
** New features
*** The C code generator supports modular nets.
*** The graphical browser (maria-vis) supports multiple modular state spaces.
** Bug fixes
*** Clearing the common subexpression cache caused problems with modular nets.
It is not cleared any more.
*** The root node of B-trees was split incorrectly when USE_MMAP is disabled.
*** The lexical order of marking expressions was not total. Now it should be.
*** "reject" states will not be expanded by default.
In graph-based analysis, the "succ" command will still expand them.
*** If an error occurs in a prioritised transition, transitions with other
priority levels will not be explored. In other words, the faulty transition
instance is treated as if it were enabled, although it does not generate any
successor state.
*** LSTS output is now disabled for modular state spaces.
*** Modular nets are implicitly flattened in the following circumstances:
**** non-modular state space exploration
**** unfolding
**** pretty-printing ("dump" command)
*** In modular nets, the synchronisation transition can now have input
and output arcs and define functions. Thanks to Charles Lakos for
contributing an elegant patch.
*** Transitions in modules can now synchronise on multiple labels.
*** Graph files can now be reopened also when memory-mapped I/O is not used.
In other words, the -g option now works on Win32.
* Maria 1.3.3 is a maintenance release mainly with improved portability.
** Bug fixes
*** Possible memory leak in the computation of strongly connected components
** New targets
*** Debian GNU/Linux on Digital Alpha
*** Debian GNU/Linux on HP-PA
*** IBM AIX 4.3.2 with gcc 3.2.1 (use Makefile.BSD)
* Maria 1.3.2 is a maintenance release mainly with Win32 improvements.
** New features
*** The [VISUAL] DUMPGRAPH command exports the reachability graph.
** Bug fixes
*** The -Y option fix in Maria 1.3.1 introduced another bug. It is now fixed.
** Win32 inter-process communication bug work-arounds
*** lbt 1.2.1 is built-in when the compile-time option BUILTIN_LTL is enabled.
*** The "visual" commands write the graphs to a file "maria-vis.out".
* Maria 1.3.1 is a maintenance release mainly with bug fixes and optimisations.
** Optimisations
*** The generated of the C code was slightly optimised.
*** Multi-set operations (SetExpression) are simplified and canonised.
** New targets
*** HP-UX 11.22 with aCC: HP ANSI C++/C B3910B A.05.36 [May 20 2002]
*** FreeBSD, NetBSD, OpenBSD with gcc 2.95 (Makefile.BSD)
** Bug fixes
*** Modular analysis did not really work. Now the supplied "modular.pn" works.
*** Comparisons "A subset B" with A==empty did not always work.
*** Multi-set operations can now be used on input arcs.
*** The -Y option now produces correct arc labels for reachability graphs.
*** Memory leaks in transition fusion code were eliminated.
* Maria 1.3
** New features
*** Automatic interruption at too many errors (-t, --tolerance=NUMBER)
*** Modular analysis (-R, --modular) of nested SUBNETs reduces state spaces.
The synchronisation labels for transitions are indicated with
transition fusion. Each transition participating in a synchronisation
must "call" the "label" transition in its parent net.
** Bug fixes
*** "deadlock true" in an empty net (broken in version 1.1) works again
* Maria 1.2
** New features
*** Added options for transition declarations
**** Constantly disabled transition instances belonging to an ENABLED
set are reported at the end of each state space exploration run. The
enabledness sets are defined in an analogous way to fairness sets.
**** The HIDE keyword controls the omission of hidden states (-Y).
States that are reached via a hidden transition instance are omitted
from the state space, but safety properties are checked also in such
states. With some knowledge in the application, this reduction easily
outperforms path compression (-Z).
**** Prioritised transitions can share priority classes
**** Transition fusion eases the modular construction of models
*** Rewritten interfaces for generating state spaces
**** All reductions can also be applied to reachability graphs,
and with some caution to general LTL model checking.
**** The executable has become smaller.
** Bug fixes
*** Transitions accept "fatal" and "undefined" in gate expressions
*** Multi-set quantification conditions are now allocated properly
* Maria 1.1
** New features
*** Improved checker for safety properties
**** Properties can be input as finite automata (translated from LTL).
**** Counterexample traces are generated from the initial state to the error.
**** Lossless storage of the reachable state set (option -L) avoids omissions.
**** Path compression reduction (option -Z) minimises the memory usage.
**** Works on multi-processor computers (-j) and TCP/IP networks (-k).
*** Statistics for encoded state vector sizes are maintained and reported.
*** The multiplicity mapping operation for multi-sets was made more generic.
** Bug fixes
*** C code generation
**** The generated code was made compatible with the IRIX and Darwin.
**** The translation errors for multi-set mappings were corrected.
*** The n-ary selection operator ?: now handles multi-sets.
** The following targets have been successfully tested:
*** Apple Darwin 5.3 (Mac OS X 10.1)
*** Digital UNIX 4.0F (cxx V6.3-010)
*** GNU/Linux on IA-32 (GCC 2.95.4 and GCC 3.0.4)
*** SGI IRIX 6.5
**** GCC (32-bit)
**** native CC -n32 or CC -64
*** SunOS 5.x (Solaris)
**** GCC (32-bit)
**** Sun WorkShop 6 update 2 C 5.3 2001/05/15 for sparcv9 (64-bit)
*** Win32 (GCC 2.95.2 for mingw or Cygwin)
* Maria 1.0.1 is a maintenance release mainly with bug fixes and optimisations.
** Additions to the query language
*** The PRED! and SUCC! commands list all predecessors or successors of a state
until a branch is found, making it easier to follow deterministic behaviour.
*** Anonymous transitions can be fired in the reachability graph.
** Bug fixes
*** States may now have more than 65535 successors.
*** Some bugs in the liveness property checker were fixed.
*** Functions can take multi-sets as parameters.
** New targets
*** The Sun compiler is now supported.
*** Preliminary support for SGI IRIX was added.
** Optimisations
*** The computation of strongly connected components was optimised.
*** The liveness property checker was slightly optimised.
* Maria 1.0 was the first official release.
----------------------------------------------------------------------
Copyright information:
Copyright 2002,2003,2004,2005 Marko Mkel
Permission is granted to anyone to make or distribute verbatim copies
of this document as received, in any medium, provided that the
copyright notice and this permission notice are preserved,
thus giving the recipient permission to redistribute in turn.
Permission is granted to distribute modified versions
of this document, or of portions of it,
under the above conditions, provided also that they
carry prominent notices stating who last changed them.
Local variables:
mode: outline
paragraph-separate: "[ ]*$"
end:
|
