-
Notifications
You must be signed in to change notification settings - Fork 0
/
NEWS
152 lines (130 loc) · 4.95 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
SLIM (2.2.2) -- 2012/05/12
* new features / support
+ extended state-space for optimization problems
++ add configure option --enable-opt-minmax
++ add --opt-min -opt-max option
* improve performances
+ modified the state compression for hyperlinks
* bug fixes
+ transition bug for switching hash function
+ --delta-mem (function "dmem_root_make") problem
+ --d-compress --mem-enc problem
+ and minor bug fixes
* and many codes refactored
SLIM (2.2.1) -- 2011/12/25
* updates for parallel LTL model checker
** new features / support
+ parallel execution on OSX Lion, Snow Leopard
+ uniq constraint rules for the delta-membrane method
+ new builtin foreign language interfaces for atomic operations
+ state compression using ZDelta Library (--d-compress)
+ programs using strings, floating point numbers
** reduce some redundant memory usages
- atom management in membranes
- state size
** improvement some time performances
+ graph isomorphism tester
+ Lv.2 profiler (calculate a Heap memory, hash conflictions, etc)
++ parallelization using openMP
++ replacement by faster hash table
+ a computational complexity of Nfreelinks procedure: O(N)-->O(1)
+ modified the mhash (a function of membranes) calculation
++ CHR (Uniq Constrait Rule) histories
++ floating point numbers using FNV-hash
++ membrane names
** bug fixes
+ graph isomorphism tester
+ builtin foreign language interfaces for atomic operations
+ memory leaks if race condition occurs in state-space
+ and minor bug fixes
** others
+ update the version of builtin-tcmalloc (1.6-->1.8.3)
+ fix some codes for hypergraph as MT-safe
- remove the execution with builtin-rulesets in default
(slim don't use builtin-rulesets/libraries in a default.
if you want to use it, add option "--use-builtin-rule")
- remove a option "--disable-compact"
+ and many codes refactored
SLIM (2.2.0) -- 2011/12/24
* new features / support
+ support Verification for hyper graph model
SLIM (2.1.7) -- 2011/08/20
* new features / support
+ add --show-hl option
+ improve the "REMOVEPROXIES" (membrane manager) performance
* minor bug fixes
SLIM (2.1.3) -- 2011/01/17
* RunTime
+ support hyper graph representation (--hl)
* Non-Deterministic Execution
+ update for partial order reduction (--por)
SLIM (2.1.1) -- 2011/01/12
* bug fix
+ fix a implementation of pthread_barrier for cygwin
SLIM (2.1.0) -- 2011/01/11
* LTL model checker
+ support OWCTY algorithm (--use-owcty --disable-map-h)
+ support MAP algorithm (--use-map)
+ support OWCTY + MAP heuristics (DEFAULT:--use-owcty --use-map-h)
+ support BLEDGE algorithm (--use-bledge)
* minor bug fixes
SLIM (2.0.7) -- 2010/10/20
* LTL Model Checker
** parallelization for State Space Search on shared-memory architecture
+ support Stack-Slicing Algorithm with Dynamic Load-Balancer
+ support Verification for LTL-Safety property
+ support Reachability execution with property automata
+ add tcmalloc as multi-threaded fast memory allocator
+ implement concurrent faster hash-table
** improve performace
+ support Canonical Membrane representation for ltl model checking
+ improve state generate procedure using Delta-Membrane technique
+ implement Fast Graph Traversal with Process ID
+ implement new rehash technique
** others
+ add options (please see --help)
- remove options (please see --help)
+ support GraphViz (Dot Language Style) output format for State Transition Graph
+ and many bug fixes
SLIM (1.1.0) -- 2010/06/26
* Nondeterministic execution
+ support combination of uniq constraint & canonical membrane representation
+ support Depth Limited BFS strategy
* Bug fixes
SLIM (1.0.0) -- 2009/11/18
* LTL Model Checking
+ support LTL formula
+ support never claim
* Nondeterministic execution
+ implement canonical membrane representation
+ replace membrane isomorphism testing
+ improve membrane hashing algorithm
+ drastic memory reduction
+ change output format
* Others
+ support external interface to C
+ support profiling for runtime
+ support new uniq constraint
+ support translation LMNtal to C
+ add LMNtal libralies
+ add -p option for profiling
+ add --mem-enc option
+ add --compact-stack option
- remove --nd_result option
-remove --nd_dump option
+ and many bug fixes
SLIM (0.4.0) -- 2008/11/7
* The conv_il was integrated to SLIM.
* Internal compilation
- You can give a LMNtal code to SLIM directly.
* Model Checking Mode
* support optimization flag
* support system libralies
* support -I option
* Bug fixes
SLIM (0.3.0) -- 2008/03/04 00:55
* module system is available
SLIM (0.2.0) -- 2008/02/21 08:55
* new features SHOULD be described here
SLIM (0.1.0) -- 2007/10/13 17:30
* new features SHOULD be described here