forked from utwente-fmt/ltsmin
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathNEWS
227 lines (197 loc) · 10.5 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
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
January 23, 2015 - Release 2.1 of the LTSmin toolset
This release is accompanied by the tool paper:
LTSmin: High-Performance Language-Independent Model Checking [6].
* Improvements to symbolic backend (*2lts-sym):
o Parallelized transition relation learning and application using Lace [5]
o Exploiting read, write and copy dependencies [3]
o Parallelized guard learning and application (--pins-guards, --no-soundness-check) [1]
o Improved regrouping algorithm for bandwidth reduction (-rcw)
o New parallel MDD implementation from the Sylvan package: LDDmc (--vset=lddmc) [5,7]
o Support maximal progress for probabilistic LTSs
* New mu-calculus PINS layer (--mucalc):
o Enables verification of mu-calculus properties
for any of the supported languages and all backends
o A parity game is generated (instead of an LTS),
which can be solved with --pg-solve in the symbolic tool,
or with any parity game solver that supports the pgsolver format.
* Symbolic Parity game solver (--pg-solve, spgsolver) [4]:
o Added parallel attractor computation (--attr=par)
* New frontend for MAPA: Scoop (mapa2lts{sym,dist})
* New frontend for dl-open (pins2*):
o Example can be found in section 3.4 in [6].
* Improvements to the POR layer (PINS2PINS wrapper):
o Added Valmari's weak POR dependencies (--weak)
o Added deletion algorithm [1] (--por=del)
o Added Valmari's SCC-based algorithm (--por=scc)
* Improvements to the multi-core backend (*2lts-mc):
o Added CNDFS proviso for efficient POR in LTL (--proviso=cndfs) [2]
o Refactored code and separated search algorithms in objects
* Improvements to distributed backend (*2lts-dist):
o Added counter example tracing
o Tau confluence detection
o Support maximal progress for probabilistic LTSs
[1] Guard-based Partial-Order Reduction (Extended Version) -
http://dx.doi.org/10.1007/s10009-014-0363-9
[2] Partial-Order Reduction for Multi-Core LTL Model Checking -
http://dx.doi.org/10.1007/978-3-319-13338-6_20
[3] Read, Write and Copy Dependencies for Symbolic Model Checking -
http://dx.doi.org/10.1007/978-3-319-13338-6_16
[4] Generating and Solving Symbolic Parity Games -
http://dx.doi.org/10.4204/EPTCS.159.2
[5] Lace: non-blocking split deque for work-stealing -
http://dx.doi.org/10.1007/978-3-319-14313-2_18
[6] LTSmin: High-Performance Language-Independent Model Checking -
http://wwwhome.ewi.utwente.nl/~meijerjjg/LTSmin_High-performance_Language-Independent_Model_Checking.pdf
[7] Sylvan: Multi-core Decision Diagrams -
http://www.tvandijk.nl/wp-content/uploads/2015/01/sylvan_tacas15.pdf
March 4, 2013 - Release 2.0 of the LTSmin toolset
* Refactored runtime and IO libraries, organized source and renamed tools:
o *-reach -> *2lts-sym (Symbolic CTL/mu model checking, ETF output)
o *2lts-mc -- *2lts-mc (Multi-core LTL model checking, compression)
o *2lts-mpi -> *2lts-dist (Distributed LTS generation, LTS output)
o *2lts-gsea -> *2lts-seq (Sequential POR, LTL, LTS gen., BDD storage)
o *2lts-grey -- REMOVED (Old sequential tool)
o lts-compare -- NEW (Branching/Strong bisim. equivalence check)
o ltsmin-tracepp-> ltsmin-printtrace (Trace pretty printing)
o ltsmin(-mpi) -> ltsmin-reduce(-dist) (LTS minimization:LTSmin's origin)
o ltstrans -> lts-convert (LTS file format conversion)
* New parallel BDD package: Sylvan [1,2]
o BDD operations are parallelized using the Wool framework (included)
o Use: *2lts-sym --vset=sylvan
*2lts-seq --state=vset --vset=sylvan
* New frontend for UPPAAL xml timed automata via opaal [A] (only opaal2lts-mc).
This adds semi-symbolic states and inclusion checks to PINS [3]:
o Multi-core reachability on timed automata using inclusion abstraction
o Supports all multi-core features, including NDFS with abstraction [4]
o Added a strict BFS algorithm [3] to reduce abstracted state counts
(--strategy=sbfs, default for opaal)
* New frontend for PBESs generating parity games for the symbolic solver [5]:
o All backends: pbes2lts-sym, pbes2lts-mc, pbes2lts-dist, and pbes2lts-seq
o Added a symbolic parity game solver: spgsolver
o PGSolver file output format ('{ast}.pg')
* Extensions to the multi-core backend (*2lts-mc):
o Support for muCRL/mCRL2/PBES using processes ({lpo,lps,pbes}2lts-mc)
o Added CNDFS algorithm [6]
o Added OWCTY algorithm [B] in the multi-core backends
o Added DFS_FIFO algorithm for parallel livelock detection using POR [7]
o Added strict BFS algorithms (--strategy=sbfs,pbfs, see [3,C])
o Elementary support for writing LTSs (using pbfs) and POR (single core)
* Renamed SpinJa to SpinS [8], and added:
o Valid end-state filter, assertions (--action=assert) and never claims
o Guards and dependencies for POR
o Support for Java 1.5 and VMs from different vendors (previously JDK 1.7)
* Optimized multi-core data structures (mc-lib):
o Reduced initialization times by using calloc instead of malloc+memset
o Reduced tree memory usage by 50% by splitting table for roots and leafs.
Set the relative ratio using: --ratio=n (n=2 by default)
o Parallel Cleary tree (--state=cleary-tree) halving memory usage [9,8]
o Reduced memoized hash sizes to 16 bit
o Thread-local allocation for better NUMA performance
o New load balancer with simplified interface
* Added test suite, called via 'make check' (requires DejaGNU)
[1] Multi-Core BDD Operations for Symbolic Reachability -
http://eprints.eemcs.utwente.nl/22166/
[2] Multi-core and/or Symbolic Model Checking -
http://eprints.eemcs.utwente.nl/22550/
[3] Multi-Core Reachability for Timed Automata -
http://eprints.eemcs.utwente.nl/21972/
[4] Multi-Core Emptiness Checking of Timed Buchi Automata using Inclusion
Abstraction - http://eprints.eemcs.utwente.nl/23158
[5] Efficient Instantiation of Parameterised Boolean Equations Systems to
Parity Games - http://eprints.eemcs.utwente.nl/22278/
[6] Improved Multi-Core Nested Depth First Search -
http://eprints.eemcs.utwente.nl/21967/
[7] Improved On-The-Fly Livelock Detection -
http://eprints.eemcs.utwente.nl/23159
[8] SpinS: Extending LTSmin with Promela via SpinJa -
http://eprints.eemcs.utwente.nl/22042/
[9] A Parallel Compact Hash Table - http://eprints.eemcs.utwente.nl/20648/
[A] opaal:
https://code.launchpad.net/~opaal-developers/opaal/opaal-ltsmin-succgen
[B] J. Barnat et al. - A Time-Optimal On-the-Fly parallel algorithm for
model checking of weak LTL properties
[C] G.J. Holzmann - Parallelizing the Spin Model Checker
February 22, 2012 - Release 1.8 of the LTSmin toolset
* Implementation of Evangelista et al.'s parallel NDFS and variations, see:
http://eprints.eemcs.utwente.nl/20618/ (Variations on Multi-Core NDFS)
* Native implementations of Ciardo et al.'s saturation algorithms for
AtermDD and ListDD (<spec>-reach --saturation=sat) (Tien-Loong Siaw)
* Dependency matrix regrouping using simulated annealing (-rgsa, -rcsa)
* SpinJa support for channel operations, run expressions with arguments,
and preprocessor defines
* New experimental I/O library and run-time environment
* New tools employing the new I/O library and run-time environment:
o lts-tracepp for pretty printing traces
o sigmin-mpi for distributed reduction of labeled transition systems
o sigmin-one for sequential reduction of labeled transition systems
o ltstrans for conversion of labeled transition systems
o ltscmp-one for sequential comparison of labeled transition systems
o <spec>2lts-hre for distributed state space generation
July 24, 2011 - Release 1.7.1 of the LTSmin toolset
* Fix for Multi-Core NDFS algorithm: introduced wait counter
(<spec>2lts-mc)
* Introduced/improved color counters and option no-all-red
(<spec>2lts-mc)
June, 24, 2011 - Release 1.7 of the LTSmin toolset
* New tools <spec>2lts-gsea
(General State Exploring Algorithms)
* PINS LTL layer
* Several multi-core LTL search algorithms
(<spec>2lts-mc)
* Several sequential LTL search algorithms
(<spec>2lts-grey, <spec>2lts-gsea)
* PINS Partial-Order Reduction Layer
(<spec>2lts-gsea)
* Bare-bones symbolic model checker for state-based mu-calculus
* New SpinJa frontend
* Patched DiVinE 2.4 frontend required
* Reimplementation of mcrl2 PINS frontend
* Read/Write dependency matrices and combined printing
* Vector set improvements and clean-up
* Connection to the libDDD decision diagram package
* Conversion from ETF to DVE (etf-convert)
November 1, 2010 - Release 1.6 of the LTSmin toolset.
* New frontend DVE2 (requires DiVinE 2.2)
* Enumerative Multi-Core backend
(<spec>2lts-mc)
* Multi-Core TreeDBS compression for state vectors
(<spec>2lts-mc)
* Finding error actions symbolically (<spec>-reach --action)
* Symbolic saturation-like strategies
* Faster trace generation for <spec>-reach
* BDD reordering for BuDDy vset
December 1, 2009 - Release 1.5 of the LTSmin toolset.
* New frontend DVE (requires DiVinE-cluster)
* Bignum support for state counts in spec-reach tools
(Jeroen Ketema)
* spec-reach clean-up
* 'tree' vector set implementation based on AtermDD
September 17, 2009 - Release 1.4 of the LTSmin toolset.
* New tool ce-mpi for distributed cycle elimination
(Simona Orzan)
* New tool ltsmin-tracepp for pretty-printing traces to
deadlock states
* TorX support factored out into separate tools
{lpo,lps,nips}2torx
* Enumerative DFS support
* Enumerative deadlock detection and trace output
* Reworked ETF support (non-backwards compatible)
* bash completion for LTSmin tools (see contrib/)
July 10, 2009 - Release 1.3 of the LTSmin toolset.
* Regrouping optimizations of the PINS matrix
* Connection to the CADP toolkit via pins_open
* Tuning of the BDD usage
* Significant performance improvements
* Symbolic deadlock detection and trace output
March 31, 2009 - Release 1.2 of the LTSmin toolset.
The main improvements in this release are:
* Option parsing is now performed using the popt library. Thus, all
long options now start with a double minus.
* The user can choose between BuDDy and ATermDD as the decision diagram
library used in the symbolic tools.
* A new compressed file format for labeled transition systems with
arbitrary numbers of state and edge labels has been implemented.
* The symbolic tools can write the results of the reachability analysis
in the form of an ETF (Enumerated Table Format) file. This ETF file
can be used as input for the reachabilty tools and can be directly
translated to DVE.