Changelog
July 3, 2018: 3.0.2
 Fix an issue where libxml2 was unnecessarily made a mandatory dependency.
July 2, 2018: 3.0.1
 Fix an issue on macOS where libxml2 is not detected correctly.
June 19, 2018: 3.0.0
 Improvements to the symbolic backend (*2ltssym):
 Precise counting of sets using the bignum interface. Meaning you can now print the size of a set arbitrarily large without loss of precision.
 Add feature that allows counting the size of a set using long doubles (in addition to doubles). The symbolic backend will automatically switch to long doubles when necessary.
 Add option –nextunion that computes the application of a transition relation together with the identity.
 The symbolic backend is now capable of invariant checking.
 Multiple formulas, invariants are now supported through their respective commandline options. If LACE is used, these properties will be checked in parallel.
 It is now possible to output all Sylvan statistics, such as the size of the node table, number of GCs etc.
 Add option –muopt that enables a faster mucalculus model checker.
 Sylvan’s LDDmc is now the default decision diagram package.
 Improvements to the static variable ordering:
 Invert the permutation of rows/columns (transition groups/state variables) using options –regroup=hf –regroup=vf respectively.
 Transformations on the dependency matrix ignore read dependencies, since write dependencies seem to influence the actual size of Decision Diagrams to a much greater extent.
 Add option –colins (see manpage) that can pick a column/state variable and insert it at a specific index.
 A vast amount of static variable reordering algorithms have been added available through Boost and ViennaCL. Furthermore the FORCE algorithm and Noack’s algorithms have been implemented, see [1]. In addition to these algorithms metrics related to the quality of the static variable order can be shown with option –regroup=mm.
 A manual group/variable order can now be given with –rowperm/–colperm respectively.
 Improvements to the LTSmin language (see
man ltsminpred
): Added the enabledness operator
??
to the LTSMin language, seeman ltsminpred
.  Native LTSmin support for signed 32bit integers is added, including some basic arithmatic operators.
 Added a type format checker.
 Added the enabledness operator

A new Petri net frontend has been added to LTSmin, see [2]. The frontend reads Petri nets in the PNML format.

A frontend for B, EventB CSP, and Z is now available through ProB, see [3].

The mCRL2 frontend now accepts files with .txt extension.

Added support for SPOT’s LTL to Büchi translation [5]
 Improvements to the multicore backend (*2ltsmc):
 Added a parallel Strongly Connected Components algorithm [4] (–strategy=ufscc).
 Added Renault’s parallel SCC algorithm (–strategy=renault).
 Added support for transitionbased general büchi automata (TGBAs) via UFSCC/Renault and SPOT.
 Added Bosnacki’s closedset proviso to preserve safety under POR.
 Support for weak LTS formulae in DFSFIFO. Simply combine –ltl with –strategy=dfsfifo to benefit from this highly scalable algorithm (if the property is not weak, an error is raised).
 Support for tracing in DFSFIFO and all new SCC algorithms.
 Improvements to the PINS interface:
 A new PINS2PINS layer is added that checks the validity of dependency matrices. The option –check activates the layer. By default, all read/write matrices are checked. When partialorder reduction (–por) is used, then the POR matrices are checked as well via an expensive reachability over the unreduced state space (because commutativity should hold in all futures).
 Added experimental support for leaping partialorder reduction. Leap sets sequentially combine multiple disjoint POR sets to ‘leap’ through the state space (–leap in combination with –por).
 Add GBExit function that is called before a backend exits.
 Factored out chunk tables and other functionality from pins.c.
 Add functions GB<setget>VarPerm and GB<setget>GroupPerm that allows language frontends to provide permutations. This is useful when frontends have language specific algorithms for static variable reordering.
 Miscellaneous:
 All default autoconf files such as README, NEWS are moved to *.md and symlinked to their old file names. The markdown styling works better with Github.
 Major refactor to the PINS regrouping layer, simplifying its use for developers.
 LTSmin now uses Travis CI.
 LTSmin now fully supports the Windows platform, since CygWin is available in 64 bit.
 Bandwidth and Wavefront Reduction for Static Variable Ordering in Symbolic Reachability Analysis  http://dx.doi.org/10.1007/9783319406480_20
 Complete Results for the 2016 Edition of the Model Checking Contest  http://mcc.lip6.fr/
 Symbolic Reachability Analysis of B Through ProB and LTSmin  http://dx.doi.org/10.1007/9783319336930_18
 MultiCore OnTheFly SCC Decomposition  http://eprints.eemcs.utwente.nl/26873/
 Multicore SCCBased LTL Model Checking http://dx.doi.org/10.1007/9783319490526_2
January 23, 2015: 2.1
This release is accompanied by the tool paper: LTSmin: HighPerformance LanguageIndependent Model Checking [6].
 Improvements to symbolic backend (*2ltssym):
 Parallelized transition relatioBandwidth and Wavefront Reduction for Static Variable Ordering in Symbolic Reachability Analysisn learning and application using Lace [5]
 Exploiting read, write and copy dependencies [3]
 Parallelized guard learning and application (–pinsguards, –nosoundnesscheck) [1]
 Improved regrouping algorithm for bandwidth reduction (rcw)
 New parallel MDD implementation from the Sylvan package: LDDmc (–vset=lddmc) [5,7]
 Support maximal progress for probabilistic LTSs
 New mucalculus PINS layer (–mucalc):
 Enables verification of mucalculus properties for any of the supported languages and all backends
 A parity game is generated (instead of an LTS), which can be solved with –pgsolve in the symbolic tool, or with any parity game solver that supports the pgsolver format.
 Symbolic Parity game solver (–pgsolve, spgsolver) [4]:
 Added parallel attractor computation (–attr=par)

New frontend for MAPA: Scoop (mapa2lts{sym,dist})
 New frontend for dlopen (pins2*):
 Example can be found in section 3.4 in [6].
 Improvements to the POR layer (PINS2PINS wrapper):
 Added Valmari’s weak POR dependencies (–weak)
 Added deletion algorithm [1] (–por=del)
 Added Valmari’s SCCbased algorithm (–por=scc)
 Improvements to the multicore backend (*2ltsmc):
 Added CNDFS proviso for efficient POR in LTL (–proviso=cndfs) [2]
 Refactored code and separated search algorithms in objects
 Improvements to distributed backend (*2ltsdist):
 Added counter example tracing
 Tau confluence detection
 Support maximal progress for probabilistic LTSs
 Guardbased PartialOrder Reduction (Extended Version)  http://dx.doi.org/10.1007/s1000901403639
 PartialOrder Reduction for MultiCore LTL Model Checking  http://dx.doi.org/10.1007/9783319133386_20
 Read, Write and Copy Dependencies for Symbolic Model Checking  http://dx.doi.org/10.1007/9783319133386_16
 Generating and Solving Symbolic Parity Games  http://dx.doi.org/10.4204/EPTCS.159.2
 Lace: nonblocking split deque for workstealing  http://dx.doi.org/10.1007/9783319143132_18
 LTSmin: HighPerformance LanguageIndependent Model Checking  http://wwwhome.ewi.utwente.nl/~meijerjjg/LTSmin_Highperformance_LanguageIndependent_Model_Checking.pdf
 Sylvan: Multicore Decision Diagrams  http://www.tvandijk.nl/wpcontent/uploads/2015/01/sylvan_tacas15.pdf
March 4, 2013: 2.0
 Refactored runtime and IO libraries, organized source and renamed tools:
 *reach > *2ltssym (Symbolic CTL/mu model checking, ETF output)
 *2ltsmc – *2ltsmc (Multicore LTL model checking, compression)
 *2ltsmpi > *2ltsdist (Distributed LTS generation, LTS output)
 *2ltsgsea > *2ltsseq (Sequential POR, LTL, LTS gen., BDD storage)
 *2ltsgrey – REMOVED (Old sequential tool)
 ltscompare – NEW (Branching/Strong bisim. equivalence check)
 ltsmintracepp> ltsminprinttrace (Trace pretty printing)
 ltsmin(mpi) > ltsminreduce(dist) (LTS minimization:LTSmin’s origin)
 ltstrans > ltsconvert (LTS file format conversion)
 New parallel BDD package: Sylvan [1,2]
 BDD operations are parallelized using the Wool framework (included)
 Use: *2ltssym –vset=sylvan *2ltsseq –state=vset –vset=sylvan
 New frontend for UPPAAL xml timed automata via opaal [10] (only opaal2ltsmc).
This adds semisymbolic states and inclusion checks to PINS [3]:
 Multicore reachability on timed automata using inclusion abstraction
 Supports all multicore features, including NDFS with abstraction [4]
 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]:
 All backends: pbes2ltssym, pbes2ltsmc, pbes2ltsdist, and pbes2ltsseq
 Added a symbolic parity game solver: spgsolver
 PGSolver file output format (‘{ast}.pg’)
 Extensions to the multicore backend (*2ltsmc):
 Support for muCRL/mCRL2/PBES using processes ({lpo,lps,pbes}2ltsmc)
 Added CNDFS algorithm [6]
 Added OWCTY algorithm [11] in the multicore backends
 Added DFS_FIFO algorithm for parallel livelock detection using POR [7]
 Added strict BFS algorithms (–strategy=sbfs,pbfs, see [3,12])
 Elementary support for writing LTSs (using pbfs) and POR (single core)
 Renamed SpinJa to SpinS [8], and added:
 Valid endstate filter, assertions (–action=assert) and never claims
 Guards and dependencies for POR
 Support for Java 1.5 and VMs from different vendors (previously JDK 1.7)
 Optimized multicore data structures (mclib):
 Reduced initialization times by using calloc instead of malloc+memset
 Reduced tree memory usage by 50% by splitting table for roots and leafs. Set the relative ratio using: –ratio=n (n=2 by default)
 Parallel Cleary tree (–state=clearytree) halving memory usage [9,8]
 Reduced memoized hash sizes to 16 bit
 Threadlocal allocation for better NUMA performance
 New load balancer with simplified interface
 Added test suite, called via ‘make check’ (requires DejaGNU)
 MultiCore BDD Operations for Symbolic Reachability  http://eprints.eemcs.utwente.nl/22166/
 Multicore and/or Symbolic Model Checking  http://eprints.eemcs.utwente.nl/22550/
 MultiCore Reachability for Timed Automata  http://eprints.eemcs.utwente.nl/21972/
 MultiCore Emptiness Checking of Timed Buchi Automata using Inclusion Abstraction  http://eprints.eemcs.utwente.nl/23158
 Efficient Instantiation of Parameterised Boolean Equations Systems to Parity Games  http://eprints.eemcs.utwente.nl/22278/
 Improved MultiCore Nested Depth First Search  http://eprints.eemcs.utwente.nl/21967/
 Improved OnTheFly Livelock Detection  http://eprints.eemcs.utwente.nl/23159
 SpinS: Extending LTSmin with Promela via SpinJa  http://eprints.eemcs.utwente.nl/22042/
 A Parallel Compact Hash Table  http://eprints.eemcs.utwente.nl/20648/
 opaal: https://code.launchpad.net/~opaaldevelopers/opaal/opaalltsminsuccgen
 J. Barnat et al.  A TimeOptimal OntheFly parallel algorithm for model checking of weak LTL properties
 G.J. Holzmann  Parallelizing the Spin Model Checker
February 22, 2012: 1.8
 Implementation of Evangelista et al.’s parallel NDFS and variations, see: http://eprints.eemcs.utwente.nl/20618/ (Variations on MultiCore NDFS)
 Native implementations of Ciardo et al.’s saturation algorithms for
AtermDD and ListDD (
reach saturation=sat) (TienLoong 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 runtime environment
 New tools employing the new I/O library and runtime environment:
o ltstracepp for pretty printing traces
o sigminmpi for distributed reduction of labeled transition systems
o sigminone for sequential reduction of labeled transition systems
o ltstrans for conversion of labeled transition systems
o ltscmpone for sequential comparison of labeled transition systems
o
2ltshre for distributed state space generation
July 24, 2011: 1.7.1
 Fix for MultiCore NDFS algorithm: introduced wait counter
(
2ltsmc)  Introduced/improved color counters and option noallred
(
2ltsmc)
June, 24, 2011: 1.7
 New tools
2ltsgsea (General State Exploring Algorithms)  PINS LTL layer
 Several multicore LTL search algorithms
(
2ltsmc)  Several sequential LTL search algorithms
(
2ltsgrey, 2ltsgsea)  PINS PartialOrder Reduction Layer
(
2ltsgsea)  Barebones symbolic model checker for statebased mucalculus
 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 cleanup
 Connection to the libDDD decision diagram package
 Conversion from ETF to DVE (etfconvert)
November 1, 2010: 1.6
 New frontend DVE2 (requires DiVinE 2.2)
 Enumerative MultiCore backend
(
2ltsmc)  MultiCore TreeDBS compression for state vectors
(
2ltsmc)  Finding error actions symbolically (
reach action)  Symbolic saturationlike strategies
 Faster trace generation for
reach  BDD reordering for BuDDy vset
December 1, 2009: 1.5
 New frontend DVE (requires DiVinEcluster)
 Bignum support for state counts in specreach tools (Jeroen Ketema)
 specreach cleanup
 ‘tree’ vector set implementation based on AtermDD
September 17, 2009: 1.4
 New tool cempi for distributed cycle elimination (Simona Orzan)
 New tool ltsmintracepp for prettyprinting 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 (nonbackwards compatible)
 bash completion for LTSmin tools (see contrib/)
July 10, 2009: 1.3
 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: 1.2
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.