Home | Case studies | Getting Started

Getting Started

• Prerequisites
• Installing fPMC
• Running fPMC for the first time
• The fPMC outputs

---

Prerequisites

fPMC has been tested on Mac OS from a MacBook Pro (early 2015 type) with 2.7GHz dual Core Intel i5 processor and 8GB RAM. Running fPMC requires the following prerequisites:

Storm is a Probabilistic Model Checker, which supports parametric model checker, verision 1.5.1 was used in the current verision of fPMC

* After installing Storm on your own computer, please make a note of the bin directory to location storm-pars (e.g., /usr/local/bin/storm-pars).

fPMC fPMC tool.

Matlab (Version R2020a) was used for evaluating the formulae returned by PMC only, not required for running fPMC.

---

Installing fPMC

Once you have installed Storm model checker, and downloaded and uncompressed the fPMC software to a new directory on your computer, the directory should now contain the following items:

• config.properties.txt

The configuration file should be updated to include:

• STORM_PATH = /usr/local/bin/storm-pars, this file path depends on where the Storm was installed.
• ALPHA = 5 was set as default, the selection of optimal value can be difficult. The rule of thumb of selecting an α is to increase the α if the fPMC spent too long or struggling in checking the abstract model; or to decrease the α if the fPMC struggling in checking one of the fragments.
• pDTMC =file path to the pDTMC model (specified in PRISM language) that to be analysed.
• PCTL_FILE =file path to where the non-functional properties (specified in PCTL) are stored.
• OUTPUT = file path to where the output of fPMC is stored.
• Switch = 30 was set as default meaning if the number of parameters in the pDTMC is smaller than the Switch, the Storm engine will be invoked, otherwise fPMC engine will be invoked.
• models

A folder that stores an exmaple of pDTMC and two non-functional properties specified in PCTL.

• libs

A folder that stores Java libaraies that are needed for running fPMC.

• fPMC.jar

The binary code files that are used to launch fPMC

• launch.sh

Launch file that prepares a couble of system variables and then executes the fPMC.jar file

Running fPMC for the first time

Once the fPMC software has been downloaded and uncompressed from fPMC zip file, you should extract the contents to a local directory and edit the configuration for the desired experiment.

Below we show an example of a configuration file, noting that STORM_PATH needs to be changed according to your local storm path:

• STORM_PATH = /usr/local/bin/storm-pars
• ...
• ALPHA = 5
• ...
• pDTMC = models/test/prismPARModel-2_P1.pm
• PCTL_FILE = models/test/Unbound.pctl
• OUTPUT = Locationofoutput
• ...
• Switch = 30

Having edited the configuration file we now execute fPMC by loading and executing launch.sh file in the terminal as follows:

> chmod 700 launch.sh
> ./launch.sh

If fPMC is running successfully, your terminal window should return the following:

• ...
• RewardStateInGraph Prism API Start
• P=?[!((state=3)|(state=24)|(state=25)|(state=26)|(state=27))U((state=15))]
• const double x;
• const double y1;
• const double y2;
• ...
• Checking:P=?[!((s=4)|(s=12)|(s=13)|(s=14)|(s=15))U((s=11))]
• ...
• Finished

A new folder will be created to store all output files, including the algebraic formulae, for evaluation.

The fPMC outputs

A number of files will be generated if the pDTMC is successfuly analysed by fPMC. That includes:

One of more models for the identified fragments, specided in PRISM language (e.g., fragment_*_model.pm)

The same number of property files as the number of fragments (e.g., fragment_*_property.pctl)

One abstract model, specided in PRISM language (e.g., fragment_abstract_model.pm)

One abstract property (e.g., fragment_abstract_property.pctl)

One text file containing all formulae and other releavent information (i.e., Model_expressions)

A Matlab file Old_model.m stores the graphical structure of the original pDTMC

A Matlab file new_model.m stores the graphical structure of the pDTMC after fPMC (additional states or tranisitions may be added)

Evaluating formulae

Open file Model_expressions, and scroll down to find a line that contains follwoing:

• ****************************The expressions start from here; Copying following expressions to MATLAB; Providing values for the parameters needed; Checking the result of Output_abstract_model ******

Copy everything below the line into Matlab. The analysed fPMC results will be returned by providing the value for each parameter.

fPMC source code

fPMC source code is also available to download.

---