search

moves-rwth / prophesy

Parameter Synthesis in Markov Models
https://moves-rwth.github.io/prophesy/
GNU General Public License v3.0
6 stars 3 forks source link

Help needed regarding utilization of region checking feature of prophesy #5

Closed oyendrila-dobe closed 4 years ago

oyendrila-dobe commented 4 years ago

Hi, I'm trying to utilize the region checking feature of prophesy to divide my parameter space (for a pDTMC) into acceptable, undecidable, and unsafe regions. I was wondering if you could provide an example on how to define a region, in the sense, how the input to the region generator would look like. I know the probable probability value range for the parameters, but how can I convert them into regions and check them? I could not quite figure it out from the documentation.

sjunges commented 4 years ago

Hi,

the following is an example call: python scripts/parameter_synthesis.py --mc=stormpy --solver=z3 set-bisimulation none 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

In particular, it means we use stormpy for model checking, z3 for smt-solving, we use no bisimulation, and we use the problem described in the given files (model and property) with the threshold in the property being 3/10. Then, we restrict the parameter space according to the region string passed, we sample with the argument that we do 2 iterations, and then we do parameter-space partitioning (with at most 30 iterations) using parameter lifting and splitting regions using the quad heuristic.

oyendrila-dobe commented 4 years ago

Thanks for the descriptive example. That clears a lot of doubts. But, I have a weird situation. Given a region, formula, and a set of instantiated states for a pDTMC, I need to find out if the formula is satisfied or not. Hence I'm looking to call a function in prophesy that checks for the satisfiability and I'd adjust my inputs likewise.