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.
simaffshould be present in the directory
./simaff in the
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.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
divine.distr_map --trail model.prop1.dve.bio
The trajectory violating the checked property appears in a file with suffix