News

We have moved to github

Added by Jeroen Meijer over 5 years ago

LTSmin 2.0

Added by Alfons Laarman over 7 years ago

Major changes (see also extract from NEWS file below):
  • Code refactor / reorganization
  • Multi-core BDD package Sylvan
  • New frontend for timed Uppaal models
  • New frontend for PBESs
  • Symbolic parity game solver
  • New multi-core LTL algorithms
  • New lockless data structures for state compression
  • Support for Mcrl/Mcrl2/PBES in the multi-core backend
  • SpinJa renamed to SpinS and extended with partial order reduction
  • Test suite based on DejaGnu

LTSmin 1.8

Added by Anonymous over 8 years ago

  • Implementation of Evangelista et al.'s parallel nested depth-first
    search and a number of variations
  • Native implementations of Ciardo et al.'s saturation algorithms for
    AtermDD and ListDD (<spec>-reach --saturation=sat) (Tien-Loong 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 run-time environment
New tools employing the new I/O library and run-time environment:
  • lts-tracepp for pretty printing traces
  • sigmin-mpi for distributed reduction of labeled transition systems
  • sigmin-one for sequential reduction of labeled transition systems
  • ltstrans for conversion of labeled transition systems
  • ltscmp-one for sequential comparison of labeled transition systems
  • <spec>2lts-hre for distributed state space generation

LTSmin 1.7.1

Added by Anonymous over 8 years ago

  • Fix for Multi-Core NDFS algorithm: introduced wait counter
    (<spec>2lts-mc)
  • Introduced/improved color counters and option no-all-red
    (<spec>2lts-mc)

LTSmin 1.7

Added by Anonymous over 9 years ago

  • New tools <spec>2lts-gsea
    (General State Exploring Algorithms)
  • PINS LTL layer
  • Several multi-core LTL search algorithms
    (<spec>2lts-mc)
  • Several sequential LTL search algorithms
    (<spec>2lts-grey, <spec>2lts-gsea)
  • PINS Partial-Order Reduction Layer
    (<spec>2lts-gsea)
  • Bare-bones symbolic model checker for state-based mu-calculus
  • 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 clean-up
  • Connection to the libDDD decision diagram package
  • Conversion from ETF to DVE (etf-convert)

LTSmin 1.6

Added by Anonymous almost 10 years ago

  • New frontend DVE2 (requires DiVinE 2.2)
  • Enumerative Multi-Core backend
  • Finding error actions symbolically (<spec>-reach --action)
  • Symbolic saturation-like strategies
  • Faster trace generation for <spec>-reach
  • BDD reordering for BuDDy vset

LTSmin 1.5

Added by Anonymous almost 11 years ago

  • New frontend DVE (requires DiVinE-cluster)
  • Bignum support for state counts in spec-reach tools
    (Jeroen Ketema)
  • spec-reach clean-up
  • 'tree' vector set implementation based on AtermDD

LTSmin 1.4

Added by Anonymous about 11 years ago

  • New tool ce-mpi for distributed cycle elimination (Simona Orzan)
  • New tool ltsmin-tracepp for pretty-printing 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 (non-backwards compatible)
  • bash completion for LTSmin tools (see source:contrib/bash-completion/)

LTSmin 1.3

Added by Anonymous about 11 years ago

  • 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

Also available in: Atom