Model analysis can be error-prone, and time wasting process. SMC Predictor not only correctly maps the appropriate SMC tools to the property type being queried, but also predicts the fastest option by analysing topological properties of biological models. For a given SBML model and a property pattern, SMC Predictor can predict the fastest SMC tool among five statistical model checker tool, namely PRISM, PLASMA-Lab, Ymer , MRMC and MC2. Read More...»
Statistical Model Checking (SMC) tools can have different modelling and specification requirements. They may differ in performance too, for example, a tool may enable specifying a large set of property types, but they may perform property verifications slowly, while another may be less efficient at specifying properties, but yet may excel at handling larger models. Therefore, user may need to use more than one tool to cover all of their need, but using even a single tool can be cumbersome, error-prone, and time wasting process, the difficulty multiplies significantly when more than one tool needs to be used.
SMC Predictor not only correctly maps the appropriate SMC tools to the property being queried, but also predicts the fastest SMC tool by analysing topological properties of biological models. For a given SBML model and property pattern, the current implementation of SMC Predictor can predict the fastest SMC tool among five statistical model checker tool, namely PRISM, PLASMA-Lab, Ymer , MRMC and MC2.
Usage: The tool requires a biological model specified in
SBML format, and a property pattern file specified in Pattern Query
Language (PQL) format. The grammar of PQL can be accessed here. You can learn how to use SMC
predictor by investigating exemplary models under /examples folder
in the archive file, the folder includes the 3 SBML models in
different sizes, and a Pattern Query (.pq) file which includes 11
different property specifications expressed in PQL. The archive
file also includes a batch file which has a single command for
executing SMC Predictor.
To run the tool, Python 3, Java "1.8" and above version are required, and the config.properties file need to point the python3 path.
java -jar SMCPredictor.jar -s “SBMLFilePath” -q
“PatternQueryFilePath” -o “OutputDirectory”
“java -jar SMCPredictor.jar -h”
Download the resource model and data files used for experiments.
The resource file includes the bio-models, specified in SBML format, their topological properties and the performance records used for training SMC predictor.