forked from motib/erigone
-
Notifications
You must be signed in to change notification settings - Fork 0
/
erigone-release.html
113 lines (91 loc) · 4.31 KB
/
erigone-release.html
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
<HTML>
<HEAD>
<META HTTP-EQUIV="Content-Type" CONTENT="text/html; charset=iso-8859-1">
<TITLE>Erigone - Release Notes</TITLE>
</HEAD>
<BODY>
<CENTER><font size=+1><b>Erigone - Release Notes</font></b></CENTER>
<p><b>Version 3.2.5 (14.12.12)</b><br>
Fixed bug: statistics not printed as long integer.
Fixed bug: literal in ltl not being compiled.
Fixed bug: atomic not stored as part of the state.
Fixed bug: null transitions should not be written to trail.
<p><b>Version 3.2.4 (08.12.12)</b><br>
Fixed bug with atomic.
<p><b>Version 3.2.3 (19.11.12)</b><br>
Fixed bug for negative values of type short.
<p><b>Version 3.2.2 (07.11.12)</b><br>
Fixed bug: Trace was not displaying the last line of a
simulation.
<p><b>Version 3.2.1 (01.08.12)</b><br>
The VMC tool has been extended to generate graphical
representations of simulations in addition to verifications.
<p><b>Version 3.2.0 (16.07.12)</b><br>
Support for random search diversity. Some limits have been
increased for the Promela models for the Tseitin clauses and a Java
program is included to generating them.
<p><b>Version 3.1.2 (03.06.12)</b><br>
Since internal LTL formulas were allowed, an LTL to Buchi
automaton translation must be done within a compilation and not as a
separate step. This version performs clean-up of the deprecated mode.
<p><b>Version 3.1.1 (29.12.11)</b><br>
The number of transitions per process has been increased.
<p><b>Version 3.1.0 (7.11.11)</b><br>
The display of the state space from within Erigone has been
removed and replace by a separate program VMC that analyzes the trace
output of Erigone.
<p><b>Version 3.0.1 (17.04.11)</b><br>
"#define" can now take parameters and be used in LTL formulas.
<p><b>Version 3.0.0 (12.04.11)</b><br>
This is a major upgrade; the main changes are:<br>
Support for additional Promela constructs including the new
ones from Spin 6.<br>
The addressing was changed from a flat address space to one
where addresses are (process offset, variable offset).<br>
The addition of a preprocessor to support <tt>inline</tt>,
embedded LTL formulas and <tt>for</tt> and <tt>select</tt>.<br>
Bug fixes: short-circuit <tt>&&</tt> and <tt>||</tt>; nested
<tt>do-od</tt>.<br>
<tt>list</tt> program for formatting the compiler output.
<p><b>Version 2.1.5 (17.03.10)</b><br>
Give error messages for absent ; or ->.<br>
Bug fix: extra end of lines at end of file are ignored.<br>
Bug fix: "break" as only alternative of if or do.<br>
Bug fix: degeneralization of LTL formula did not clone byte code.<br>
Bug fix: backtracking over "run".
<p><b>Version 2.1.4 (26.02.10)</b><br>
User's guide and software documentation separated.<br>
Quick start guide added.
<p><b>Version 2.1.3 (27.09.09)</b><br>
Bug fix: "np_" is not supported but keyword was spelled
wrong.<br>
Increase size of byte codes for expression in LTL formula.<br>
Bug fix: compilation of "byte a[...], b[...]".<br>
Added increment and decrement of array elements.<br>
Bug fix: "run" in program with never claim.<br>
Added skip statement.<br>
Bug fix: nested if-statements.
<p><b>Version 2.1.2 (26.09.09)</b><br>
Bug fix: verification with rendezvous channels.<br>
Remove limitations on multiple mtype declarations, channel arrays
and declarations after statements.
<p><b>Version 2.1.1 (26.09.09)</b><br>
Erigone was used on the sample programs supplied with my book
<i>Principles of the Spin Model Checker</i>. This used many more
constructs in Promela and uncovered quite a few bugs that are fixed in
this version.<br>
<p><b>Version 2.1.0 (20.09.09)</b><br>
Supports display of the state space (like SpinSpider in jSpin).<br>
Support for remote reference to labels in LTL formulas.
<p><b>Version 2.0.0 (03.09.09)</b><br>
This is the first version with a new compiler.<br>
Additional constructs supported: proctype with parameters,
run, _nr_pr, _pid, end and accept labels.
<p><b>Version 1.1.4 (05.08.09)</b><br>
This was the last version with the old compiler.
It will not be supported in the future.
<p><b>Version 1.0.0 (12.02.09)</b><br>
Initial release.
<P><A HREF="../erigone/index.html"><IMG SRC="../home/LEFT.GIF" ></A>
</BODY>
</HTML>