MC2 - PLTL model checker and associated files

MC2 v1.0.zip - entire package, comprising:

  • gillespie0.11-modified/ - The modified gillespie2 v0.1.1 source used to generate stochastic simulations of the models. Please recompile to generate the gillespie2 binary for your architecture.
  • models/ - The Kholondenko, Levchenko and TwoReactionModel models with molar concentrations and the Levchenko and TwoReactionModel models with number of molecules (filename suffix: _#MOLECULES).
  • queries/ - Example queries for use with the MC2 tool and unix scripts to create queries at larger numbers of levels.
  • simulation_outputs/ - Example simulation outputs for use with the MC2 tool.

  • gillespie2-levchenko_4.run, gillespie2-tworeactionmodel_10.run - Example run commands for the modified gillespie2 simulator to produce a file of 100 simulation outputs.
  • MC2.jar - MC2 model checker compiled with Java v1.5.0_07.
  • MC2.run - Example run commands for the MC2 tool, checking the three types of outputs; deterministic, stochastic and (deterministic) parameter scan.
  • UserManual.pdf - The user manual for MC2, explaining how to install and run the various simulators and perform model checking.

    MC2 © is a product of the Bioinformatics Research Centre, University of Glasgow, UK. MC2 author: Robin Donaldson

    Overall queries to David Gilbert.

    Last updated: 19/01/08