Skip to content
Switch branches/tags

Name already in use

A tag already exists with the provided branch name. Many Git commands accept both tag and branch names, so creating this branch may cause unexpected behavior. Are you sure you want to create this branch?
Go to file
Cannot retrieve contributors at this time
Changes between toolset releases 202206.0 and 202206.1:
This release contains two bug fixes:
* Write counterexample's structured output trace on a single line.
* Fixed that hidden actions (the --tau option) were not properly recognized in
Changes between toolset releases 202106.0 and 202206.0:
This release brings two new tools and several improvements to existing tools.
First of all, lpsreach is a new state space exploration tool that uses symbolic
representations to effectively operate on state spaces consisting with billions
of states. Next, pbessolvesymbolic is a tool to solve parameterised Boolean
equation systems (PBESs) based on similar techniques. Both tools are
unfortunately not yet available on Windows. Another major limitation of
pbessolvesymbolic is that it can not yet produce counter examples.
The ltscompare tool has been extended with generating distinguishing formulas
for trace and (divergence-preserving branching) bisimulation equivalences for
options 'bisim-gv', '(dp)branching-bisim-gv' and 'trace'. These formulas can be
used to generate counter examples that can explain why two state spaces are
28 bug reports were resolved since the last release.
List of other changes:
- Tool pbesconstelm has been extended with '--check-quantifiers' to
eliminate constant quantified parameters.
Changes between toolset releases 202006.0 and 202106.0:
This release brings several UI improvements and important bug fixes. For
mcrl2ide we have added a confirmation when the edit property dialog is closed
with unsaved changes. Furthermore, the find and replace functionality has also
been improved. Finally, we have also added matching bracket highlighting and
fixed other minor bugs. There have also been minor improvements to lpsxsim and
The ltscompare tool has been extended with coupled simulation equivalence
checking, available under the new flag '-ecoupled-sim', by an external
contributor. Two other external pull requests have been merged. We always
welcome pull requests even for minor usability improvements or to fix typos.
26 issues were closed since the last release.
List of other changes:
- Rewriting of function updates has been made significantly more efficient by
replacing the rewrite rules with exponential complexity by rules with linear
- Fixed reading of probabilistic labelled transition systems in the .lts
format. These can now be properly used with ltsgraph or ltsinfo.
Changes between toolset releases 201908.0 and 202006.0:
This release brings bug fixes and many changes under the hood. First, the format
of the binary files (including lps, lts and pbes) has been revised, which makes
reading and writing them far more memory efficient. It is important to note that
binary files created with previous versions can no longer be used.
The tools lps2lts and pbes2bool have both been replaced. The tool pbes2bool is
now identical to the pbessolve tool, which was introduced in the 201808.0
release. The lps2lts tool has been re-implemented with far better maintainable
code. It now supports writing the state space in the lts format on-the-fly,
which further reduces the amount of memory required.
Several parts of the code base now rely on a C++17 compliant compiler and
consequently the minimum supported compiler versions have been increased. These
are now GCC 7.0, Clang 5.0, and AppleClang 11.0. Finally, Visual Studio 2019 of
at least version 16.0 is required. These changes also mean that using the
compiling jitty rewriter (option --rewriter=jittyc) requires a C++17 compliant
compiler, where compilers satisfying the minimum version requirements are
confirmed to work properly.
31 bug reports were resolved since the last release.
List of other changes:
- LTSgraph can now export the graph to a vector image in the SVG format again.
The resulting export is also more accurate to what is shown on screen.
Furthermore, the graph presentation and the LaTeX export functionality have
also received some polishing.
- The tools lps2lts and ltsconvert now support piping using '-' as a special
- The tool lpsbinary has received a new option --select which can be used to
indicate the parameters or sorts that should be replaced by booleans.
- Python 2 has been declared deprecated and various testing and build related
scripts have been adapted to work with Python 3.6 at minimum.
- The documentation generation has also been refactored and now supports sphinx
version 2.2, which makes it easier to generate documentation locally.
Changes between toolset releases 201808.0 and 201908.0:
The 201908.0 release mainly contains improvements under the hood. First, the
ATerm library, which is the main internal data storage engine of mCRL2, has been
re-implemented completely. The new implementation should lend itself better to
future experiments, such as multi-threading.
The mCRL2ide, which was introduced in the previous release, has been developed
further. A major new feature is the possibility to compare processes under some
equivalence relation. This release also brings many small changes, improving
the overall ease of use.
59 issues were closed since the last release.
List of other changes:
- LTSgraph has been upgraded to use OpenGL 3.3. This should improve stability of
the tool. Furthermore, 3D mode (which can be actived from the 'View' menu) now
looks more realistic. The option to export the graph to a vector image was
broken and has been removed. This feature may return in the future.
- pbessolve, the new tool for solving PBESs and generating counter-examples,
has undergone significant changes to its higher optimisation levels
(available via the option --strategy). The higher levels should now be more
- The implementation of the Jansen/Groote/Keiren/Wijs branching bisimulation
algorithm that operates directly on LTSs is now standard. The old algorithm
that includes a translation to Kripke structures is still available in
ltsconvert/ltscompare with the option --equivalence=bisim-gjkw.
- The MAINTAINER build type has been removed from CMake. Builds for debugging
should now be build with the DEBUG build type.
- Writing large ATerm files (basically all binary files that the toolset
produces) is now faster and more memory efficient. We plan to further improve
this in the coming year.
- The quantifiers inside rewriter (available via 'pbesrewr -pquantifier-inside')
has been slightly generalised.
- The algorithm and implementation of failure refinement (ltscompare -pfailures)
have been greatly improved. This improves scalability and fixes a bug.
Changes between toolset releases 201707.0 and 201808.0:
This release sees the introduction of two new tools that should increase the
usability of the toolset significantly. First, pbessolve is a new tool for
solving parameterised Boolean equation systems (PBESs). Together with the new
option --counter-example in lps2pbes, this tool can generate counter-examples.
See the documentation on the website for more instructions.
The other new tool is mcrl2ide, which is an integrated editor for mCLR2
specifications and properties. With this tool, generating a state space and
checking properties is much easier, since no knowledge about the other tools and
their options is required. For new users, mcrl2ide is the ideal tool to write
small specifications. Advanced functionality is still available via mcrl2-gui or
the command line.
Finally, the development of mCRL2 moved to Github
( Issues can be submitted there.
56 issues were closed since the last release.
List of other changes:
- The minimal GCC version has been raised to 4.9. The minmal version of Sphinx
required to build the documentation is now 1.3.6.
- The minimal Qt version on macOS is now 5.10. Older versions contain a bug that
leads to strange behaviour of the menu bar in graphical tools.
- The performance of refinement checking for LTSs has been drastically improved.
- Linearising specifications containing time is more scalable and leads to
smaller specifications.
- The implementation for weak bisimulation reduction has been improved,
which decreases the number of transitions in the output.
- An experimental implementation of the Groote/Jansen/Keiren/Wijs algorithm for
branching bisimulation that works directly on LTSs was added to ltsconvert and
ltscompare. This avoids the translation to Kripke structures, which can be
expensive for large transition systems.
- lpsactionrename can now rename actions based on a regular expression given
with the command line option --regex. The existing algorithms in
lpsactionrename have also been tweaked to yield a more compact result in some
Changes between toolset releases 201409.0 and 201707.0:
153 tickets were closed in this period.
- The support for 32 bit machines is dropped. The minimal compiler versions that
can be used are GCC 4.8, Clang 3.2 and MSVC 14.0. Use of C++11 is now fully
- The graphical tools now use Qt5.5 or higher instead of Qt4. Numerous changes
were made to the graphical tools. In particular ltsgraph can now be used
to explore large transition systems.
- There is a new and faster algorithm for (branching) bisimulation (Groote/Jansen/
Keiren/Wijs). There is a new algorithm for weak bisimulation (upon request by
Matthew Hennessy). There are new equivalence checking algorithms for (weak) failure
(divergence) equivalence and inclusion with counter examples. There is a
new algorithm to apply ready simulation reduction and comparison (thanks to
Rafael Martinez Torres, Luis LLana and Carlos Gregorio-Rodriguez).
- Storing and loading of .lts transition systems is much faster. The format is
not compatible with the .lts format of the previous release.
- The states of .aut files are not renumbered anymore when loading. Each state
number must now be smaller than the total number of states.
- Support for labelled transition systems in .dot format is partially dropped.
Support for .bcg files is dropped completely.
- It is now possible to declare additional data types in a modal formula.
- Probabilities can now be used in mCRL2 specifications using the
dist keyword. Probabilistic transition systems can be generated in .aut, .lts and
.fsm format. These can be visualized in ltsgraph and reduced modulo strong
bisimulation using the new tool ltspbisim. All probabilities are calculated
using exact arithmetic.
- Saving of .pbes, .lps, .lts and .bes files is improved. Unfortunately, this format
is not compatible with the previous format and these files need to be regenerated.
- The bisimulation and trace reduction tools preserve state labels in .lts files
by joining them for equivalent states.
- Timed linearisation now uses Gauss- and Fourier-Motzkin elimination and the
simplex algorithm to simplify timed conditions. All these algorithms use exact
- Typechecking is strengthened by not allowing variables with the same name as
(predefined) function symbols. The type checking code is largely refactored.
- The meaning of <= and < on finite sets and bags have changed. It represented
the ordering generated by struct data types. Now it reflects the subset and strict
subset operations. This also influences >= and >.
- Printing of progress information is adapted. Under normal circumstances no time
tags and log statuses are printed anymore. This is only done when the debug
flag or the --timings flags are set, or when the status is error.
- The dependence of the compiling rewriter on BOOST is removed. Rewriters can be
compiled on Linux and the mac without the BOOST library present.
- The status of the tools bessolve, txt2bes, pbesinst and lpsbisim2pbes is set to
release. lps2torx and pbesabstract are now deprecated.
Known bugs:
- Rewriting of nested function updates does not work properly.
Changes between toolset releases 201310.0 and 201409.0:
54 tickets were closed since the previous release. The changes in this release
are for the greatest part refactoring efforts to prepare for coming changes.
- Enumeration of finite set sorts and finite function sorts has been added.
- PBES tools can now handle PBESs containing negations and implications. The
txt2pbes tool no longer eliminates these operators by default.
- PBES tools can now use textual representation as in- and output format.
- The implementation of the pbesstategraph has been thoroughly revised. A more
efficient local variant of the algorithm is now used by default.
- The internal ATerm format of mCRL2 data types has been changed. Variables
and function symbols now store a unique number, to make table lookups more
efficient. This change has no effect on the disk format.
- Stricter ATerm casting mechanism to prevent casts between incompatible Aterm
- A new, more generic implementation of the enumerator was made that also
operates on PBES expressions. It has been used to improve the performance of
some PBES rewriters.
- The dependencies between the mCRL2 libraries were minimized.
- Preparation for move to Qt5.
- Preparation to use more C++11 features.
Known bugs:
- The ltsgraph tool does not properly export images on all platforms. Notably,
the bitmap export functionality on Mac OSX Mavericks is broken. This seems to
be a combination of Qt4 issues and OSX OpenGL issues; this bug might be fixed
in a point-release, or it may be left until the next release, which should be
using Qt5.
Changes between toolset releases 201210.1 and 201310.0:
60 tickets were fixed for this release. We summarise the most important changes
It is important to note that LPS and PBES files generated using earlier
versions of mCRL2 cannot be loaded in this version.
- ATerm library was cleaned up and ported to C++, the directory
3rd-party/aterm has been removed, and relevant code has been merged
into libraries/atermpp, and the library is compiled as mcrl2_atermpp.
- WARNING: The file aterm_init.h and the MCRL2_ATERMPP_INIT macro are
still available, but will be removed in the next release (r11743).
- Code for modal mu-calculus formulae was moved to a separate library,
which is compiled as mcrl2_modal_formula.
- Type checking was lifted to a higher level of abstraction, and now
operates on classes representing conceptual objects, instead of ATerms.
- Specified and reimplemented the alphabet reductions, leading to
improved performance.
- Added absorption rules for set and bag union and intersection (#1089).
- Implemented capture avoiding substitutions, such that variables do not
need to be renamed a-priori.
- Improved one-point rule elimination in rewriters.
- Extend parser of PGSolver format to accept games produced by MLSolver
- Support for loading labelled transition systems from files in the DOT
file format was dropped.
- Typechecker now rejects redeclaration of built-in functions (r11689).
- Fix normalisation of modal mu-calculus formulae (r11696).
- Fix compiler warnings in the included DParser library.
- The jittyc compiler now checks that the version of the header files
with which it is compiled matches the version of the tool that is
loading the rewriter (#951).
- For compiling the rewriter, we do not depend on the DParser headers
anymore (#1176).
- Requires C++11 support of the C++ compiler. We tested using
GCC 4.4, 4.5, 4.6, 4.7 and Clang 3.2 on Linux, MSVC 2010 on Windows,
and Clang 3.2 on Mac OS X.
Tool changes:
- Fix handling of command line arguments with spaces for all tools (r11388).
- Fix opening and creation of files and folders in mcrl2-gui on OSX (#1123).
- Properly handle tools with multiple input file-types in mcrl2-gui (#1124).
- Fix name-clash resolution in lpsbisim2pbes (#1144).
- Use optimisations in lps2pbes, which leads to smaller right hand sides
in PBESes (#1155).
New experimental tools:
- complps2pbes
- pbesstategraph
The following tools have been removed:
- tbf2lps
The following tool has become deprecated as of this release:
- formulacheck
Changes between toolset releases 201210.0 and 201210.1:
- Dropped support for .dot files as input format. Output is still supported.
- New ATerm library which uses reference counting rather than mark & sweep
to do garbage collection.
Changes between toolset releases 201210.0 and 201210.1:
Fixed bugs:
- #1096 Allow filepicker to open file in mcrl2-gui
- #1100 Attempt to fix the build on ARM-based platforms.
- #1101 Enable selection of two inputs for tools in mcrl2-gui (if supported by
the tool)
- #1104 Fix link to "Compiling mCRL2 yourself" in docs.
- #1105 Fix link to regression test results in docs.
- #1107 Fix labels of optional tool options in mcrl2-gui.
- #1108 Fix generation of help descriptions in the online manual.
- r11245 Fix typos in log messages.
- r11278 Fix warnings in release mode.
- r11287 Fix spelling errors in docs.
Changes between toolset releases 201202.0 and 201210.0:
100 tickets were fixed for this release. We summarise the most important changes
- Header files are shown in IDEs like Visual Studio, XCode and QTCreator
- LTS library: removed support for the SVC format.
- Fixed installation path of dparser headers
(include/dparser instead of include)
- Remove unused quantifier variables when enumerating (r10356)
- Improved performance of alphabet reductions.
- Reimplemented nextstate generation on top of the LPS library.
- Added an interface to the LTSmin toolset for the PBES library.
- Cleaned up the ATerm library to remove unused functionality.
- Improved performance of parsers.
Tool changes:
- The graphical tools mcrl2-gui, ltsgraph, ltsview, diagraphica, lpsxsim
and mcrl2xi have been ported to QT, the wxWidgets versions have been
- lps2lts has been extended with the options --cached and --prune. The first
option enables caching of intermediate results, and gives rise to a
performance improvement in most cases. Note that in some cases this comes
with a significant memory penalty. The second argument uses a decision tree
such that, given a value of a parameter, only a subset of summands needs
to be considered.
- lps2lts, lpssim, lpsxsim, lps2torx use the new implementation of nextstate
- Added implementations of signature based algorithms for bisimulation,
braching bisimulation and divergence preserving branching bisimulation to
- The number of variables used internally for quantifier enumeration is
configurable using the -Q/--qlimit flag for all tools using the rewriter.
By default this value is set to 1000.
- Improved performance of lts2pbes.
The following tools have been removed:
- chi2mcrl2
- grapemcrl2
- ltsmin
- lysa2mcrl2
Changes between toolset releases 201107.1 and 201202.0:
- Core library: re-implemented parser on top of DParser. As input this uses
an EBNF grammar with associativities and priorities.
- Core library: re-implemented pretty printer on top of C++ libraries,
instead of the C libraries.
- Data library: improve treatment of quantification in enumerators. This
vastly improves the user experience when using quantifiers as well as sets
and bags.
- Data library: refactored the rewriters to carry substitutions as an
argument, instead of as a global value.
- Data library: clean up identifier generators and improve their performance.
- BES library: extend support for parity games in PGSolver format (max parity
- BES library: removed the translation to VASY format.
- LPS library: extend support for LTSmin.
- LPS library: improve performance of the next state iterator interface.
- Cleaned up direct uses of ATerms in all libraries.
- Support for MSVC9 has been dropped; MSVC10 is freely available as part of
the Windows SDK, and bugs in MSVC9 caused obscure compile errors.
- Use system provided gl2ps if available.
Tool changes:
- lps2lts: the default state format has changed from "vector" to "tree".
- lpspp: add -n/--print-summand_numbers option. This prints an identifier
for each summand that is printed.
- ltsview: fix non-termination of backtrace generation.
- mcrl22lps: assume untimed semantics by default (the behaviour of the
-D/--delta flag), for linearising timed specifications, the -T/--timed
flag must be used.
- mcrl22lps: remove support for n-parallel processes. This will be
reinstated more thoroughly in a future release (see bug #977).
- mcrl2xi: find and replace functionality has been implemented.
- pbes and bes tools: use uniform I/O handling.
- pbes2bool, pbes2pbes, lps2lts: make tool behave line a GNU tool: output on
stdout, additional information on stderr.
- pbesrewr: add rewrite strategy that eliminates quantifiers using the
one-point rule.
- gui tools: improve wxWidgets 2.9 support; the tools are alright in release
builds, but may still raise some assertion failures in debug builds due to
massive internal changes in wxWidgets.
New experimental tools:
- mcrl2parse: parsing of expressions adhering to the mCRL2 syntax.
- pbesabsinthe: abstract interpretation of PBESes.
The following tools have become deprecated as of this release:
- chi2mcrl2
- lysa2mcrl2
Changes between toolset releases March 2011 and July 2011:
- Removed the innermost rewriters; only the jitty, jittyc and jittyp
rewriters are available.
- Cleaned up the implementations of the remaining rewriters.
- Performance of the jittyc rewriter has been improved.
- Compiling rewriters using an external compile script.
- An interface for generating next states has been provided, in such a way
that it is independent of the internal structures of mCRL2.
This allows for a more reliable integration of mCRL2 and LTSmin
- By setting the CMake variable MCRL2_LTSMIN_INSTALL_PATH to the directory
containing the LTSmin sources, the mCRL2 make install will build the
LTSmin toolset with compatible settings.
- Fix compilation with GCC 4.6.
Library changes:
- Renamed library mcrl2_utilities_command_line to mcrl2_utilities.
- Moved some utility functionality from mcrl2_core to mcrl2_utilities.
- Incorporated and cleaned up ATerm library. The ATerm library included in
mCRL2 now is compiled as C++.
New functionality:
- Improved handling of universal and existential quantification in the
- A new logging library has been implemented and incorporated.
- Improved performance of parity game generator used by pbespgsolve.
- The tool lps2torx now uses the simulation backend.
- A major update of pbespgsolve has been imported from upstream.
New experimental tool:
- lts2pbes has been added, allowing to encode model checking problems
directly on LPSes.
Changed tool status:
- pbespgsolve has become a release tool.
Changes between toolset releases July 2010 and March 2011:
- Removed 3rd-party/boost, mCRL2 depends on Boost >= 1.37
- Removed bjam build system. Use of the CMake build system is now required.
- Developed a BES library as the basis for further solving/reduction
- The basic code for all data structures is now generated from a concise set
of specifications. Standard traversal and find/replace functionality is
available for all these data types.
- Stabilise ATerm library for 64-bit Windows platforms.
- Overal stabilisation of the code, including fixing compiler warnings/errors
on various supported platforms.
- The implementation of the LTS library has been cleaned up.
New functionality:
- pbes2bool and pbespgsolve accept BESs and PBESs as input.
- pbes2bes should be used to generate a BES from a PBES; this functionality
has been removed from pbes2bool. Use pbes2bool directly on the PBES if
you want proper counterexamples.
- The tool previously called pbes2bes is now named pbesinst.
- New tool besinfo that prints information on a BES.
- New tool bespp that prints a BES in human readable format.
- tau*a reduction is available from ltsconvert.
- New tool mcrl2xi that can be used to edit mCRL2 specifications.
It provides the functionality as the command-line tool mcrl2i.
New experimental tools:
- besconvert can be used to reduce BESs modulo strong bisimulation and
stuttering equivalence.
- lts2pbes can be used to generate a PBES form an LTS and a modal formula.
- bessolve can be used to solve a BES using small progress measures or the
recursive algorith due to Zielonka. For efficient solving the use of
pbespgsolve is recommended.
- pbesabstract provides a form of abstract interpretation for pbesses.
Parameters of pbes equations can be removed underapproximating or
overapproximating the solution of the PBES. This can dramatically reduce
the number of BES variables generated from a PBES.
Removed tools:
- squadt
- pnml2mcrl2
Changes between toolset releases January 2010 and July 2010:
- 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
will be removed in the January 2011 release.
- increase the amount of generated code.
- more extensive testing
Tool renamings:
- In order to have a more consistent tool naming scheme, some tools have
been renamed:
* sim -> lpssim
* xsim -> lpsxsim
* grape -> grapemcrl2
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)
- lps2lts has an extra option to detect divergences.
- for a number of equivalences, ltscompare can give countertraces in case
two processes are not equivalent. This is helpful in finding why two
processes are not equivalent.
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:
- 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
- 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
- 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
- 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
- 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:
- 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:
- 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
- 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
- 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:
- 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.
- 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.