A Quick Tour Through Prophesy¶

This tour focuses on the use of the Command Line Interface (CLI). While the tour is organised around a series of problems common in parameter synthesis, we recommend first-time users to follow the guide in a linear fashion.

Sampling¶

A parametric model can be instantiated with different values for the parameters (instantiations). Sampling explores the parameter space (i.e. the set of all instantiations) by evaluating various instantiated models

python scripts/parameter_synthesis.py load-problem model.pm property.pctl sample

The solution function problem¶

This problem asks for a closed-form representation that shows how the measure-of-interest (e.g., the probability to reach a predefined set of target states) depends on the parameter values. Many probabilistic model checkers support these computations: Prophesy can be used as a uniform gateway to these model checkers

python scripts/parameter_synthesis.py load-problem model.pm property.pctl compute-solution-function

This tells the CLI to load the problem instance described by the model file and the property file, and then to compute a solution function. The call can be adapted in several directions

python scripts/parameter_synthesis.py --mc storm load-problem model.pm property.pctl compute-solution-function --export sol.out

This call has been adapted in two directions: We now specified the model checker to be used, in this case storm, and that the result should be exported to a file sol.out.

The computed solution function can be used to speed up sampling:

TBD

The exact synthesis problem¶

The exact synthesis problem asks for an exact representation of all parameter instantiations that satisfy a specification. The solution function is a concise (but often very complex) solution. Prophesy currently does not support any other versions of the exact synthesis problem.

The feasible / optimal instantiation problem¶

The feasible instantiation problem asks for a parameter valuation such that the induced Markov model satisfies a given property.

There are various approaches to do so:

SMT
Particle Swarm Optimisation
Convex optimisation

Using particle swarm optimisation¶

The two essential arguments are whether you want to find a solution above or below the threshold, and what technique to use. Here, we specified to use PSO

$ python scripts/parameter_synthesis.py load-problem model.pm property.pctl set-threshold 0.1 find-feasible-instantiation below pso

The threshold and the direction in the property should not be specified, i.e., use P=? […] to specify your reachability property. Instead, we set the threshold to 0.1 by the command line, and then ask prophesy to find a feasible instantiation.

Using convex optimisation¶

To switch to convex optimisation, all you need to do is switch the last command to QCQP. We notice that this method requires gurobi

$ python scripts/parameter_synthesis.py load-problem model.pm property.pctl set-threshold 0.1 find-feasible-instantiation below qcqp

To speed things up, there are a couple of options that you want to set when using QCQP (they should soon become default flags)

$ python scripts/parameter_synthesis.py load-problem model.pm property.pctl set-threshold 0.1 find-feasible-instantiation --qcqp-incremental --qcqp-store-quadratic --qcqp-handle-violation minimisation --qcqp-mc full --precheck-welldefinedness below qcqp

Options¶

TBD

Using SMT¶

TBD

The parameter space partitioning problem¶

This problem asks to provide a partitioning into accepting, rejecting and unknown regions, trying to minimize the unknown regions.

$  python scripts/parameter_synthesis.py load-problem  benchmarkfiles/smallpmdp/smallpmdp.pm benchmarkfiles/smallpmdp/min.pctl set-threshold 3/10 set-parameter-space --region-string "0.1<=p<=0.2,0.4<=q<=0.6" parameter-space-partitioning --iterations 30 pla quads

This method runs using the quad heuristic for splitting the parameter space, and uses PLA (parameter lifting) for verifying the regions.

It is often beneficial to sample a bit before running the parameter space partitiong. We do so by adding the sample command.

$  python scripts/parameter_synthesis.py load-problem  benchmarkfiles/smallpmdp/smallpmdp.pm benchmarkfiles/smallpmdp/min.pctl set-threshold 3/10 set-parameter-space --region-string "0.1<=p<=0.2,0.4<=q<=0.6" sample --iterations 2 parameter-space-partitioning --iterations 30 pla quads