-
Notifications
You must be signed in to change notification settings - Fork 2
/
Copy pathNEWS
153 lines (125 loc) · 6.29 KB
/
NEWS
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
DiVinE 2.4 (29.9.2010)
======================
- C3 check for parallel partial order reduction.
- Partial order reduction for (interpreted) DVE (--por).
- Real-time hashtable & queue statistics (--statistics).
- Custom generators are not allowed with pool-less builds.
- Further optimisations to the exploration engine (hash table, FIFOs, MPI).
- Better --version output.
- In addition to G++, DiVinE can be compiled with Clang now.
- More fixes in MPI.
- A curses-based interface for observing runtime algorithm behaviour.
- Dual-threaded nested DFS (Holzmann '07).
- Counterexamples in (single-threaded) nested DFS.
- Enable on-the-fly heuristic in distributed (MPI) OWCTY.
- Make "divine verify" work with non-DVE inputs correctly.
- Fix BA translation of F((F a) U b) form formulae (J. Strejcek &c.)
DiVinE 2.3 (8.8.2010)
=====================
- Basic support for Murphi model compilation and parallel verification.
- Fix a bug in DVE compiler that made some models uncompilable.
- Improved, distributed (MPI-enabled) MAP algorithm.
- Track state space statistics in OWCTY (--report).
- Proper deadlock detection (with traces) for all model types.
- Improved --report output format consistency.
- Fix handling of committed states in the DVE compiler.
- Multiple stability and correctness fixes in distributed memory support (MPI).
- Limit the override of global allocator to avoid occasional crashes in glibc.
- Add an option to limit maximum verification runtime (--max-time, POSIX only).
Furthermore, a new binary ABI is available in this release. There are two
caveats though:
1) The ABI is NOT STABLE and should not be relied upon. It will be subject of
further changes in future releases.
2) The win32 support is somewhat limited, since some models may expect access
to symbols exported by the divine binary itself, which is not supported on
win32.
DiVinE 2.2 (17.2.2010)
======================
- Further optimisations in compiled DVE.
- Improved overall performance of the verifier.
- "divine combine" can be used again (it's been broken in previous releases)
- Compiled models can now be loaded on Windows.
- New option, -i (--initial-table) to set intial hashtable size. This can be
used to further improve performance, assuming knowledge of model size.
An overall speed improvement of 20 - 30 % may be expected for dual-core
reachability and LTL verification when using compiled DVE, over version
2.1.1. Please note that dve.so files generated by this version are not
compatible with DiVinE 2.1.1.
KNOWN ISSUES: Error state handling is not consistent between interpreted and
compiled DVE. The profiled build (-DPROFILE=ON) is currently broken. (Both
issues exist since version 2.1.)
DiVinE 2.1.1 (26.1.2010)
========================
- Fixed a number of issues with compiled DVE models.
- Bugfixes in the custom model loader.
- Improved performance of compiled DVE.
- Fixed Windows build.
DiVinE 2.1 (17.1.2010)
======================
- A new DVE to C (to native binary) compiler available as `divine compile'.
- Fixed handling of error states in interpreted DVE.
- The GUI can now be compiled & used on Windows.
- A number of GUI improvements and usability fixes.
DiVinE 2.0 (19.11.2009)
=======================
- This version is a major rewrite of the parallel framework and algorithms.
- MPI is now partially supported in addition to shared memory parallelism
OpenMPI 1.3 is recommended.
- A new graphical user interface is available, including model editor,
simulator and a counterexample browser.
- Support for running on Windows (win32) machines (shared memory only).
- It is now possible to load models in form of ELF shared objects (POSIX only).
- More data available in --report (including machine-readable counterexample).
- The divine.combine binary has been removed, use "divine combine" instead.
DiVinE Multi-Core 1.4 (23.4.2009)
=================================
- Unfortunately, an incorrect implementation of Nested DFS has slipped into the
1.3 release. Version 1.4 fixes this problem.
- Early counterexample discovery in OWCTY has been improved: accepting
self-loops are now detected on-the-fly, and early termination is now more
efficient.
DiVinE Multi-Core 1.3 (17.11.2008)
==================================
- Improved and newly included algorithms:
- MAP: improved progress reports, early termination and counterexamples
- Nested DFS for single-threaded verification (no counterexamples)
- A new "verify" subcommand to run the most suitable algorithm for given
input and number of cores (currently does not produce counterexamples when
used with -w 1 due to the abovementioned Nested DFS limitation).
- Counterexample generation in OWCTY has suffered from a bug that prevented it
from finishing in any reasonable time on some property/model combinations.
This has been fixed.
- A few other user experience fixes: improved warnings and overall robustness.
DiVinE Multi-Core 1.2.1 (1.11.2008)
===================================
- Fix compilation with g++ 4.3.
- Update the bundled version of HOARD to 3.7.1.
- Include some updates to the bundled version of wibble (no major impact on
DiVinE itself).
DiVinE Multi-Core 1.2 (15.5.2008)
=================================
- A few minor bugfixes.
- The divine-mc.combine utility can now handle .mdve and .mprobdve files.
- Parallel shared-memory probabilistic model checker ProbDiVinE-MC has been
added to the distribution, built as divine-mc.probabilistic.
- NIPS interpreter updated to version 1.2.8
DiVinE Multi-Core 1.1
=====================
- The OWCTY algorithm now performs an on-the-fly heuristic to speed up
discovery of counterexample.
- Added divine-mc.combine to the distribution.
- Added report generation functionality (-r commandline switch) to facilitate
mass experimental runs.
- New commandline switch --max-memory to limit address space available to the
tool. Can be used to avoid swapping.
- Counterexample generation can now be disabled through --no-counterexample
commandline switch.
- A dummy high-speed state space generator for performance analysis. It is used
when no input file is given.
- A prototype ProMeLa state space generator and an accompanying bytecode
compiler. ProMeLa models can be verified, although no counterexample
generation is implemented.
- Developer documentation updates.
DiVinE Multi-Core 1.0
=====================
Initial release.