Regular Model Checking

Software

The implementation is available under the GNU Public License. There is also a Bugzilla bug tracking database which is public.

Current source

  • gbdd-0.10.tar.gz The GBDD package abstracts from BDDs providing a representation for finite relations based on BDDs, handling the details of BDD variable usage. It is currently used in conjunction with the BuDDy package, see configure --help for flags to compile with the BuDDy package.
  • gautomata-0.10.tar.gz This is a automata package based on GBDD. It contains a general BDD based representation of non-deterministic automata, with operations such as product, minimization and determinization.
  • rmc-0.6.tar.gz This is a package with the regular model checking engine. It takes formulas in LTL(MSO) as input and find models.

All packages use autoconf for their configuration. Just type ./configure and make. You have to install each package in some location (use --prefix as argument to configure), for the other packages to find them.

Current stable RPMS

NOTE: These are built under RedHat Fedore Core 2

yum repository

Include the following in your /etc/yum.conf file: 
[rmc]
name=Regular Model Checking
baseurl=http://www.regularmodelchecking.com/software/fedora/2/stable

Other

Documentation

You can browse the Doxygen documentation for the stable version:

Daily CVS snapshots

NOTE: These are built under RedHat Fedore Core 2

yum repository

Include the following in your /etc/yum.conf file: 
[rmc]
name=Regular Model Checking
baseurl=http://www.regularmodelchecking.com/software/fedora/2/snapshots/standard

Other

Configure packages for development

The following might be relevent flags for ./autogen.sh:

  • Solaris bug --target=NONE
  • Maintaining --disable-shared --enable-maintainer-mode

Compilation flags given by CXXFLAGS="..." ./autogen.sh

  • Profiling -O2 -g -pg -static
  • Debugging -g
Last changed: Thursday, 26-May-2005 18:19:07 CEST