Main Authors of LibDDD : Yann Thierry-Mieg (LIP6, [email protected], 2003-), Jean-Michel Couvreur (LaBRi, 2001), and Denis Poitrenaud (LIP6, 2001)
- Maximilien Colange < LIP6, [email protected] > (2010-present): split-equiv, ordering heuristics, symmetries, google hash support, maintenance and performance upgrades
- Alexandre Hamez < LIP6 and LRDE (EPITA), [email protected] > (2006-2009): maintenance, multi-threading, rewrite rules
- Vincent Beaudenon < LIP6 > (2004-2005) : serialisation, user (not strong) homomorphisms
- François Bréant < LIP6 > (2004) : INST_STL, multi-target build
- Samuel Charron < LRDE (EPITA) > (2005-2006) : tests
- We borrowed google's sparse hash table implementation in C++, which gives low memory footprints with limited time overhead. This (almost) drop-in replacement for standard STL hash tables gives up to 40% memory gain on some experiments. See :
- We borrowed several utility functions (process monitoring, hash functions...) from Spot's code base, due to Alexandre duret-Lutz, Denis Poitrenaud et al.
Main Author of LibITS and ITS-CTL: Yann Thierry-Mieg (LIP6, [email protected], 2003-).
Main Authors of ITS-LTL: Yann Thierry-Mieg, Denis Poitrenaud, Alexandre Duret-Lutz (EPITA) and Kais Klai (LIPN).
- Maximilien Colange < LIP6, [email protected] > (2010-present): GAL, Split-Equiv, Expressions, symmetries, maintenance and improvements
- Silien Hong < LIP6 > (2008-2011): CTL, parsers for JSON format.
- Didier Lime (2011): Romeo parser
The code base for libITS borrows from many open-source projects of other universities. In particular it builds on code from :
- VIS from Boulder University, Colorado. The CTL model-checker its-ctl reuses many packages of VIS (parsers and CTL forward model-checking).See VIS: A system for Verification and Synthesis, VIS homepage. The ctlp package is due to Gary York, Ramin Hojati, Tom Shiple, Adnan Aziz, Yuji Kukimoto, Jae-Young Jang, In-Ho Moon. The mc package is due to Adnan Aziz, Tom Shiple, In-Ho Moon.
- LTSmin, Univerity of Twente, Netherlands. Support of ETF files relies on parsers taken from their code base. The Divine to GAL translation was originally based on a patch to Divine by LTSmin's team. by Stefan Blom, Alfons Laarman, Elwin Pater, Jaco van de Pol, Michael Weber et al. of the Formal Methods and Tools group of the University of Twente (NL). Additional prototype code was provided by Jeroen Ketema of the same team.
- Divine, University of Brno, Poland. Rather than provide a patch for Divine, parsers and internal representations for Divine models were directly extracted from their code base. See
version 1.8 : January 2012. Release includes the new equiv-split mechanism and several significant performance improvements.
- New hash table implementation based on google's hash tables. Yields significantly (10 to 40%) lower memory foortprint.
- Reimplementation of low-level encoding and storage of DDD. Lowers memory footprint significantly (up to 30%) on 64bit architectures.
- Split-equiv functionality to evaluate complex expressions
- Added some additional rewriting rules for DDD homomorphisms
version 1.7 : February 2011. Release includes some "standard" homomorphisms to reason with integers, and a new way of defining operations as 2k level DD.
- New homomorphisms Select and Set pushed into libDDD (were duplicated in quite a few tools)
- New Apply2k operation to specify a transition relation as a decision diagram. Use case related to use of ETF files.
- Improved stats and dot export functionality
- Improved memory footprint by up to 30% on some examples (privilege use of std::vector over use of std::set wherever possible)
version 1.6 : May 2010. Release includes a few new rewriting rules and upgrades compatibility with newer compilers.
- More rules related to selector homomorphisms added
- Added an "invert" member function to homomorphisms allowing to compute the pre-image given a potential state space.
- Use evil macros and suchlike to support tr1 standard where available
version 1.5 : June 2009. Release includes enhanced auto-saturation, selector homomorphisms, and commutative rewriting rules.
- homomorphisms Range added as a simple commutativity criterion
- More rewriting rules implemented to enhance dynamic saturation effect
- Selector predicate introduced, allows use of not, ITE, ... To ease manipulation of atomic properties
- morpion (TicTacToe) tutorial example added to repository
- MT-SAFE version can be built for multi-threaded applications (although efficiency is badly impacted)
version 1.4 : January 2008. Release includes auto-saturation mechanisms and homomorphism rewrite rules.
- homomorphisms Skip predicate added
- rewriting rules implmented to produce dynamic saturation effect
- local apply mechanisms and related rules
- hanoi example added to repository
- INST_STL removed from build (was broken with gcc > 3.3 anyway)
- various cleanups and rewrites for compliance with gcc >= 4.1
- minor updates to allow build on 64 bit architectures
- added tests using uttk
- include a dot export example
- include serialization and user homomorphisms
- Cleaned up includes
- Added doxygen documentation
- Changed hash functions
- Some efficiency speedup
- Uses autotools for build procedure, tested on Mac, linux, cygwin.
- Compiles in three variants :
- libddd.a, the optimized version,
- libddd_d.a version with debugging symbols activated,
- libddd_otfg.a a version with experimental on the fly garbage collection
- Optionally, using gcc in versions 3.1, 3.2 or 3.3, it is possible to activate build of INST_STL version, modify src/Makefile.am for this.
Pre 1.0 : 2001-2003. Beta versions of the pure DDD library. Version 0.99 was version number for some time.