-
Notifications
You must be signed in to change notification settings - Fork 4
PCTL parameter synthesis
Parameter Synthesis can be performed on parametric models with respect
to the given PCTL formula expressing a property regarding the
probability of an event to occur. If the formula has defined probability
threshold, then the partitioning of the given parameter space (defined
by the user) to regions which satisfy (resp. violate) the property is
computed If the threshold is not given, a probability function of
parameters is computed instead, which evaluates to the probability of
satisfaction for particular parametrisation. PCTL Parameter Synthesis
procedure is performed using an external tool called Storm. A step by
step Galaxy tour showing how to use the tool can be found
here.
-
TS file: Generated transition system for the desired model (computed using Transition System generator)
-
PCTL formula: Given formula expressing property to be used to perform parameter synthesis on the transition system of the given model.
-
Intervals: Relevant only in the case when PCTL formula has defined probability threshold. Then, an interval of allowed values has to be specified for each unknown parameter in the model, together forming parameter space. If PCTL formula does not have defined probability threshold (i.e. starts with
P=?), the intervals should not be defined.
The textual result contains some details about Storm model checker
performance. It is stored in a .storm.sample or .storm.regions file,
depending on the particular scenario which was chosen (PCTL with vs.
without threshold).
.storm.sample file contains computed probability function of
parameters, which can be evaluated to the probability of satisfaction
for particular parametrisation. This result can be further analysed in Probability Sampling tool.
.storm.regions file contains segmentation of specified parameter space
to regions where the given property is satisfied and violated. For some
of the regions, the satisfiability might not be decided due to
efficiency reasons.
The Parameter Synthesis results stored in .storm.regions file can be visualised in Parameter synthesis result visualisation.
usage: PCTLParameterSynthesis.py [-h] --transition_file TRANSITION_FILE
--output OUTPUT
--formula FORMULA
[--region REGION]
[--local_storm]
Parameter synthesis
required arguments:
--transition_file TRANSITION_FILE
--output OUTPUT
--formula FORMULA
optional arguments:
--region REGION
--local_storm