BioDiVinE 1.0

BioDiVinE 1.0 is a tool set created for verifying properties of biochemical systems given as a system of ordinary differential equations. It is an evolutionary branch of the DiVinE tool accompanied by the GeNeSim GUI for model management.

• Download and unpack the installation package

• MPI - version 1.2 or higher
• Automake - version 1.10.1 or higher
• Autoconf - version 2.61 or higher
• C++ compiler gcc - version 4.3 or higher
• Ant - version 1.6.5 or higher

• BioDiVinE should be compiled before this compilation, because of the linking of the libraries
• you will need the Qt library - version 4 or higher

1. enter the BioDiVinE directory (/biodivine)
2. after executing the following sequence of commands, the runnable programs should be present in the directory biodivine/bin

./autogen
make

1. enter the directory biodivine/gui
2. QT version 4.0 or higher (4.x) is needed
3. after executing the following sequence of commands, the executable file simaff should be present in the directory biodivine/gui

qmake
make

1. download the BioDiVinE GUI from http://lsd.fi.muni.cz/trac/BioDivineGUI/
2. compile BioDiVinE (see instructions above)
3. enter the directory biodivine/gui/biovis
4. compile biovis utility

make

• finally configure the path to biovis in BioDiVinE GUI by following the BioDiVinE GUI documentation
• the path should be set to '{biodivinepath}/gui/biovis/'

Run ./simaff in the biodivine/gui directory.

Simaff Tutorial

For model checking of biochemical system, you need file of type *.ltl containing the checked LTL property and file of type *.bio containing a biochemical model (described here BIO format).

Run (divine.combine is in the biodivine/bin directory) the following command:

 divine.combine model.bio property.ltl

to get file named model.prop1.dve containing the original biochemical model with added Büchi automaton recognizing the negation of LTL property from property.ltl needed for model checking.

There are programs divine.owcty and divine.distr_map in the biodivine/bin directory. If you rename the file model.prop1.dve by adding the suffix .bio, you can use these programs for checking, whether the biochemical model satisfies the property given in file property.ltl or not. The result is YES (No Accepting Cycle Found) or NO (Accepting Cycle Found). If you are interested in the trajectory violating the property, use

 divine.owcty --trail model.prop1.dve.bio 

or

 divine.distr_map --trail model.prop1.dve.bio

The trajectory violating the checked property appears in a file with suffix .trail.

Model checking example