LIP6 UPMC CNRS Move-team LIP6 UPMC CNRS Move-team Macao FrameKit CPN-AMI
$Date:: 2013-05-17#$
LIP6 > Software > MoVe Sofware > SDD/DDD >

This is the home of libddd and the its-tools

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.