What is SMC Predictor?

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.
Example usage: java -jar SMCPredictor.jar -s “SBMLFilePath” -q “PatternQueryFilePath” -o “OutputDirectory”
For help: “java -jar SMCPredictor.jar -h”