Dynasty contains algorithms for synthesis in probabilistic program sketches.
Some of the algorithms have been published:
-  Milan Ceska, Christian Hensel, Sebastian Junges, Joost-Pieter Katoen: Counterexample-Driven Synthesis for Probabilistic Program Sketches, FM 2019.
-  Milan Ceska, Nils Jansen, Sebastian Junges, Joost-Pieter Katoen: Shepherding Hordes of Markov chains, TACAS 2019.
An overview is given in:
-  Milan Ceska, Christian Dehnert, Nils Jansen, Sebastian Junges, Joost-Pieter Katoen: Model Repair Revamped: On the Automated Synthesis of Markov Chains.
And many more details can be found in:
-  Sebastian Junges: Parameter Synthesis in Markov Models, PhD Thesis, RWTH Aachen University, 2020.
We first give some installation guideline and then go into some usage examples. A tutorial that walks users through some options is provided seperately.
- Python bindings for z3.
- The model checker storm and the python bindings for storm. Please check the installation hints.
- The python packages:
python setup.py install
This will automatically install dynasty and its python dependencies. Notice that you have to install storm yourself (see above).
If you are planning to make changes to the code, we suggest to use
python setup.py develop
To run the tests, run:
python -m pytest dynasty_tests
We automatically provide a docker container with everything pre-installed.
We support solution of three types of problems:
- Feasibility Analysis (and its dual, Validity Analysis),
- Optimal Feasibility Analysis,
- Partitioning (or Threshold Analysis).
We support five methods of solving the above problems:
- CEGIS ,
- Lifting ,
- (Consistent) Scheduler enumeration ,
- SmartSearch [to be published],
- All-in-one [Chroszon et al, Formal Asp Comput].
As input, we take projects. Below, we first explain what a project is and then discuss the different analysis types and how to invoke the different methods for these problems. For details about the methods, we refer to the publications mentioned above.
Input: Project Folders
A project is a folder containing the various inputs for the synthesis.
- A .templ file, which is a PRISM file with various open integer constants (holes).
- A .allowed file, which describes sets of possible values for each hole. The instantiations are the Cartesian product of such sets of values.
- A .properties file, which contains a list of PCTL formulae.
Optionally, a project may contain:
- A .restrictions file, which contains restrictions on the intstantiations. Restrictions are currently only supported by CEGIS.
- A .optimality file, which contains a PCTL formula, a direction, and a relative precision. This file is relevant for optimal feasibility.
Notice that a project may contain more files than necessary, e.g., to allow for slight variations without duplicating everything.
For more information, look at the examples.
The goal of feasibility analysis is to find an instantiation of the holes such that the induced program satisfies the properties. All methods we provide for solving this problem are complete, i.e., the algorithms either report a feasible solution, or if there is no feasible instantiation, the algorithms eventually report so.
Notice that one has to be careful about potentially ill-formed sketches. The checks we perform are not necessarily sufficient.
Below, we provide examples of using the different supported methods for feasability analysis on the provided case studies.
python dynasty.py --project examples/virus/ --sketch virus.templ --constants CMAX=0,T=18.0 --allowed virus.allowed --restrictions virus.restrictions --properties virus.properties
python dynasty.py --project examples/grid/ --sketch 4x4grid_sl.templ --constants CMAX=11,T_EXP=10.0,T_SLOW=10.0,T_FAST=0.9 --allowed 4x4grid_sl.allowed --restrictions 4x4grid_sl.restrictions --properties single.properties
python dynasty.py --project examples/grid/ --sketch 4x4grid_sl.templ --constants CMAX=1,T_EXP=10.0,T_SLOW=10.0,T_FAST=0.9 --allowed 4x4grid_sl.allowed --restrictions 4x4grid_sl.restrictions --properties reward.properties --check-prerequisites True
python dynasty.py --project examples/grid/ --sketch 4x4grid_sl.templ --properties reward.properties --constants "CMAX=400,T_EXP=7.7,T_FAST=0.6,T_SLOW=0.995" --allowed 4x4grid_sl.allowed lift
python dynasty.py --project examples/grid/ --sketch 4x4grid_sl.templ --properties reward.properties --constants "CMAX=400,T_EXP=7.7,T_FAST=0.6,T_SLOW=0.995" --allowed 4x4grid_sl.allowed cschedenum
All other approaches
Optimal Feasibility Analysis
Optimal feasibility analysis differs from feasibility analysis in that an optimality criterion is added. An optimality criterion consists of a property, a direction, and a relative tolerance, described in a file containing, e.g., the following:
P=? [ F (o=2 & c<=5) ] max relative 0.0
The above optimality criterion says that the probability described by the first line should be maximized among all feasible options. By increasing the relative tolerance given on the last line, the hard optimality constraint can be relaxed to requiring that the obtained instantiation is at least (1-tolerance)* "global maximum." When given such a criterion, the tool automatically switches to solving optimal feasibility.
Below, we provide examples of using the different supported methods for optimal feasability analysis on the provided case studies.
python dynasty.py --project examples/grid/ --sketch 4x4grid_sl.templ --constants CMAX=11,T_EXP=10.0,T_SLOW=10.0,T_FAST=0.7 --allowed 4x4grid_sl.allowed --restrictions 4x4grid_sl.restrictions --optimality fast_to_target.optimal --properties none.properties cegis
A support for optimal feasibility analysis is not yet implemented.
This problem is also known as threshold synthesis. It aims to partition the set of instantiations into a set of accepting instantiations, i.e., instantiations that satisfy the property at hand, and rejecting instantiations, i.e., instantiations that do not satisfy the property at hand.
In general, partitioning can be enabled by adding a switch
--partitioning. Notice that this switch
cannot be combined with
Below, we provide examples of using the different supported methods for partitioning on the provided case studies.
Currently, there is no working implementation for this type of analysis.
python --project examples/grid/ --sketch 4x4grid_sl.templ --constants CMAX=11,T_EXP=10.0,T_SLOW=10.0,T_FAST=0.9 --allowed 4x4grid_sl.allowed --restrictions 4x4grid_sl.restrictions --properties single.properties --partitioning lift
All other approaches
--no-check-prerequiitesOne may omit the check prerequisites if the sketch already ensures that all rewards are less than infinity.
--print-statsPrint statistics at the end. Helpful to understand the algorithm performance but clutters the output.