CHANGES

===============================================================================
Changes between toolset releases 202307.1 and 202307.0:
===============================================================================

This is a minor release resolving some issues with ltsgraph and removing 
ltsgraph_deprecated since it is not functional.

===============================================================================
Changes between toolset releases 202307.0 and 202206.1:
===============================================================================

This release contains a major refactor of the code base to enable multi-threaded
exploration algorithms for lps2lts and pbes2bool/pbessolve, which can be enabled
with --threads flag. The other changes mostly focus on the usability and
stability of existing tools.

22 issues were resolved and 3 external pull request have been accepted since the
last release.

List of other changes:
  - The distinguishing formulas generated by ltscompare for strong bisimulation
    have been significantly reduced in size.
  - A new graph layout algorithm has been implemented LTSGraph that is
    significantly faster and allows the visualization of state spaces with
    thousands of states. In some cases the new layout algorithm is less visibly
    stable for small state spaces, so ltsgraph_deprecated remains available for 
    the time being with the original behaviour.
  - New algorithms have been implemented in the lpsparunfold tool, which can
    unfold structured parameters into its components. The new algorithms obtain
    better results by default, but can also deal better with complexer situations.
  - Several usability improvements have been made to diagraphica, updating and
    removing some outdated functionality.
  - Added lps2jani to translate a subset of stochastic specifications to the
    jani format (jani-spec.org), which can be further analysed by tools such as
    Modest (modestchecker.net) or Storm (stormchecker.org).
  - Several fixes for linearisation of stochastic processes.

===============================================================================
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
    ltsconvert.

===============================================================================
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
distinct. 

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
ltsgraph.

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
    complexity.  
  - 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
  symbol.
- 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
  robust.
- 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
(https://github.com/mCRL2org/mCRL2). 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
  cases.

===============================================================================
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
  supported.
- 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
  arithmetic.
- 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
  structures.
- 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
below.

It is important to note that LPS and PBES files generated using earlier
versions of mCRL2 cannot be loaded in this version.

Libraries:
  - 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
    (r11637).
  - 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).

Build:
  - 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:
===============================================================================
Features:
  - 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
below.

Libraries:
   - 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
     removed.
   - 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
     generation.
   - Added implementations of signature based algorithms for bisimulation,
     braching bisimulation and divergence preserving branching bisimulation to
     ltsconvert.
   - 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:
===============================================================================

Libraries:
   - 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
     games).
   - 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.

Build:
   - 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:
===============================================================================

 General:
   - 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
     (http://fmt.cs.utwente.nl/tools/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
     rewriters.
   - 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:
===============================================================================

 General:
   - 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
     algorithms.
   - 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.
     PBESs
   - 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:
===============================================================================

 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
     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)
     otherwise.
   - 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:
===============================================================================

 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.