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 a 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 a C++ library for model-checking of various formalisms using libDDD. It defines instantiable transition systems (ITS), a simple labeled transition system semantics, in a symbolic way. The its-tools are built on top of libITS and support model-checking of ITS models.

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.

What is ITS modeler

ITS modeler is a set of Eclipse plugins, offering access to ITS-tools in a convenient manner for end-users.

Main features include:

  • Guarded Action Language support : rich editor, code completions,...
  • One click install from update site
  • Embedded ITS-tools binary distribution, for most platforms. Reachability and CTL can be invoked from Eclipse.
  • Graphical modeling support for Petri net variants, using components of Coloane.
  • Import/Export to Romeo and Tina formats for Time Petri Nets (discrete time assumptions)
  • Uppaal XTA format editor and translation to GAL, supporting analysis of Timed automata (discrete time).
  • Divine DVE format editor and translation to GAL, supporting analysis of DVE models.
  • Spin Promela format editor and translation to GAL, supporting analysis of Promela models.
  • Analysis and rewriting of GAL specifications : static simplifications, variable domain analysis, control flow analyis, parameter analysis...

The ITS modeling front-end tools are distributed under the terms of EPL.