File: CHANGES

package info (click to toggle)
mcrl2 201007~rc1-1
  • links: PTS, VCS
  • area: main
  • in suites: squeeze
  • size: 28,524 kB
  • ctags: 34,862
  • sloc: cpp: 251,100; ansic: 19,553; python: 12,151; yacc: 10,042; sh: 3,185; lex: 2,040; xml: 279; makefile: 193
file content (221 lines) | stat: -rw-r--r-- 10,381 bytes parent folder | download
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
===============================================================================
Changes between toolset releases January 2010 and July 2010:
===============================================================================

 General:
   - developed new graphical user interface mcrl2-gui. Use of this tool is
     recommended above using squadt.
   - move to CMake build system. The bjam build system is still included, but
     not actively maintained. It will be removed in the January 2011 release.
   - increase the amount of generated code.
   - more extensive testing

 New functionality:
   - the language now supports function updates for functions of arity 1. It is
     now allowed to write f[d -> e] for a function f: D -> E, with d in D and
     e in E. The meaning is that (f[d -> e])(x) = e if x == d, and f(x)
     otherwise.

 Deprecated tools:
   - squadt is deprecated. It will be removed in the January 2011 release. We
     recommend using mcrl2-gui instead.

 Known issues:
   - ltsview and ltsgraph do not work when started from SQuADT in Windows 7 and
     Windows Vista; if started directly they do function properly. Using
     mcrl2-gui there are no problems.

===============================================================================
Changes between toolset releases January 2009 and January 2010:
===============================================================================

 General:
   - developed a new data and process library and adapted most tools and 
     libraries to use it. Ultimately the classes in core will all be replaced
     such that core will become obsolete.
   - introduced new tool classes and adapted all tools to it, leading to uniform
     command line interfaces for all tools.
   - adapted the user interface of mcrl2i.
   - bisimulation reduction algorithms are much faster.
   
 New functionality:
   - divergence preserving branching bisimulation has been implemented.
   - lps2lts can search for divergences, and generated traces to divergent
     states.
   - lps2lts can generate a state space steered by the first argument of
     actions (which must be a natural number). Only transitions with the
     lowest number will be taken. It is also possible to do a random walk
     in this way.
   - ltsgraph can display transition systems in 3d.
   - lps2pbes now properly supports the use of sorts in the modal formula that
     were defined under alias in the lps.
 
 The following tools have been marked stable:
   - grape: a graphical process editor.
   - mcrl2i: an mCRL2 interpreter that can be used for evaluating data
     expressions.
   - pbesconstelm: apply constant parameter elimination to a pbes.
   - pbesparelm: apply parameter elimination to a pbes.
   - lpsparunfold: unfold a set of given parameters in an lps. (Similar to the
     muCRL tool structelm).
   - lysa2mcrl2: convert a security protocol specified in Typed LySa to mCRL2.
   - txt2lps: read a textual description of a linear process into a binary lps
     file. Rejects anything that is not linear.
 
 The following tools have been added (but are marked experimental):
   - lpsbisim2pbes: encode process equivalences of two linear processes into a
     pbes.
   - lts2lps: convert a labelled transition system into an lps.
   - pbespareqelm: eliminate equivalence relations between parameters of a pbes.
   - pbespgsolve: solve a pbes using a parity game solver algorithm.
     (Contributed by Maks Verver).

The following tools have been removed:
   - mcrl2pp
   - pbessolve

 Notes:
   - SQuADT specific:
     + The tool catalog must be regenerated to add newly connected tools;
       to do this manually remove .squadt/tool_catalog in the home directory.
   - the CMake build system is provided as an alternative to boost build, but
     it is still experimental.
       
 Known issues:
   - ltsview and ltsgraph do not work when started from SQuADT in Windows 7 and
     Windows Vista; if started directly they do function properly.

===============================================================================
Changes between toolset releases July 2008 and January 2009:
===============================================================================

 General:
   - compatible with LTSmin toolset 1.1 van de Universiteit Twente
   - added support for importing LTSes from DOT format
   - extended mCRL2 LTS storage format to include extra information such data
     and parameter specifications. This new format uses the .lts suffix.
   - support for rational numbers (as part of sort Real):
     + rational numbers can be created using the division operator /
     + rational numbers can be converted to integers by means of functions
       floor, ceil and round
   - comparison operations <, <=, >= and > are now defined on all standard
     data types (including structured sorts)
   - sets and bags data structures have been reimplementated to better support
     the use of finite sets and bags. By guaranteeing a unique representation
     of finite sets/bags it is now no longer a problem to generate state spaces
     of processes with finite sets/bags as parameters, for instance.
   - numerous small improvements to tools and underlying infrastructure
   - lots of bug fixes

 Renamed tools:
   - formcheck is now called formulacheck

 New functionality:
   - ltsgraph is completely reimplemented and now uses OpenGL for rendering
   - ltsgraph, ltsview, diagraphica now support all LTS formats supported by
     the LTS library

 New tools:
   - pbesparelm: removes unused parameters from a PBES.
   - pbesconstelm: removes constant parameters from a PBES.

===============================================================================
Changes between toolset releases January 2008 and July 2008:
===============================================================================

 General:
   - improved command line interfaces and help information:
     + simplified interfaces of most tools, especially mcrl22lps, lps2lts,
       lps2torx, ltscompare, ltsmin, ltsconvert, tracepp and formcheck
     + improved consistency among tools
     + adherence to the GNU standard for command line interfaces
     + removed the undocumented feature that the argument '-' can be used
       for reading from standard input in or writing to standard output
     + improved error handling of loading and saving binary files
   - added manual pages for tools
   - changed SVC library license from the
     GNU General Public License, version 2 (or newer), to the
     GNU Lesser General Public License, version 2.1 (or newer).
   - libraries and header files are installed
   - improvements to existing tool and library documentation
   - improved regression testing
   - lots of bug fixes

 Added tools:
   - txt2pbes: translates a textual PBES specification to the binary format

 Removed tools:
   - pbes2bes: most functionality is incorporated in pbes2bool

 Renamed tools:
   - lpsdecluster is now called lpssuminst
   - lpsformcheck is now called formcheck

 Performance improvements:
   - improved performance of lpspp and pbespp for specifications
     involving many variable declarations
   - improved average case performance of div and mod calculations by
     a factor of 2
   - increased power of enumeration involving conditions on list length,
     e.g. enumerating all lists l such that #l == 2 or #l <= 2
   - lpssuminst: summands with a false condition are filtered out
   - lpssumelm: more time-efficient on specifications involving large
     conditions
   - squadt: more time-efficient initialisation process

 New functionality:
   - ltsview: added new option for marking states: mark separately for
     every mark rule
   - ltscompare: added comparison using simulation preorder/equivalence
   - ltsconvert: added minimisation modulo simulation equivalence
   - pbes2bool, lpsactionrename, diagraphica: functional improvements
   - lpssuminst: added (option -t/--tau) which only instantiates tau summands
   - formcheck: now also works with PBESes or without a context specification

 Notes:
   - LPS or PBES files produced with the previous release cannot be used
     anymore. They need to be regenerated using the tools in this release.
   - SQuADT specific:
     + The tool catalog must be regenerated to add newly connected tools;
       to do this manually remove .squadt/tool_catalog in the home directory.
     + Old project files cannot be loaded due to a limitation of the old
       format, automatic conversion is not possible so projects must be
       recreated manually.

===============================================================================
Changes between toolset releases July 2007 and January 2008:
===============================================================================

 General:
   - Numerous bug fixes.
   - Added documentation for all libraries and tools on the website.

 Added tools:
   - chi2mcrl2: translates a subset of Chi to mCRL2
   - lpsactionrename: selectively renames or hides actions in linear processes
   - pbesrewr: applies the rewriter to simplify data expressions in PBESes

 Removed tools:
   - lpsdataelm (its functionality has been integrated in other tools)

 New functionality:
   - Added full support for the verification of modal formulas with data using
     lps2pbes and pbes2bool.
   - Improved handling of time in the lineariser (mcrl22lps). Sometimes this
     slows the lineariser down. Added flags to suppress time if needed.
   - Improvement of the output of the pretty printers (lpspp and pbespp) that
     print linear processes and parameterised boolean equation systems.
   - Added simulation support to ltsview and improved its layout.
   - Functionality of sim is the same as that of xsim (as far as allowed with
     a command line interface).
   - Migrated from CVC Lite to CVC3 as supported external SMT-solver.

 Notes:
   - LPS or PBES files produced with the previous release cannot be used
     anymore. They need to be regenerated using the tools in this release.
   - SQuADT specific:
     + The tool catalog must be regenerated to add newly connected tools;
       to do this manually remove .squadt/tool_catalog in the home directory.
     + Old project files cannot be loaded due to a limitation of the old
       format, automatic conversion is not possible so projects must be
       recreated manually.