What is libDDD ?
libDDD is C++ library for manipulation of decision diagrams.
Main features include:
- Flexible and powerful encoding of operations using inductive homomorphisms
- Support for hierarchy of the description with SDD
- Automatic support for saturation style algorithms
- A priori unbounded integer domain variables
- Rich expressivity with equiv-split mechanism
- Weak ordering constraint allowing to store variable length decision paths
- Supports both Data Decision Diagrams which are integer valued and Hierarchical Set Decision Diagrams.
libDDD is distributed under the terms of LGPL.
What are ITS tools
libITS is C++ library for model-checking of various formalisms using libDDD.
Main features include:
- Instantiable Transition System as a framework, allow hierarchical composition of components specified in diverse formalisms.
- Optimized implementation taking full advantage of the features of libDDD, notably automatic saturation and hierarchy.
- Support for Petri nets and some of their extensions
- Support for discrete time in models such as Time Petri nets and their compositions
- Support for GAL format input which offers rich data manipulation.
- Support for ETF format input which is produced by the tool LTSmin from diverse formalisms.
- Support for Divine format input which is native to the tool Divine and used in BEEM models.
- Support for CTL model checking using forward transition relation.
- Support for LTL model checking using some classic and some original algorithms that exploit saturation.
The ITS tools are distributed under the terms of GPL.
|
