Artifact and instructions to generate experimental results for TACAS 2019 paper: StocHy: automated verification and synthesis of stochastic processes

We provide an artifact of the tool called StocHy. This serves as an
accompaniment to the tool paper titled StocHy: automated verification
and synthesis of stochastic processes. The artifact consists of a
compiled version of StocHy which allows you to generate all the results
within the experimental evaluation section (i.e. Sec. 4). Within the
tool paper, we present four different case studies highlighting the
novelty, strengths and use of StocHy. The first case study deals with
the application of formal verification via two abstraction techniques:
FAUST 2 or IMDP based and their comparison in terms of computational
times and abstraction error for varying grid sizes. Using the artifact,
this analysis can be performed for all the different grids or a subset
of the grids used (as desired). In the second case study, we perform
strategy synthesis over an unbounded time horizon. Consequently, running
the artifact results in generating the policy itself, the probability
of satisfying the property of interest when using this policy and the
maximum abstraction error. The third case study, shows how we can scale
in the number of continuous variables (up to 12 dimensions) when
performing formal verification.
The artifacts gives the option to run the verification procedure for all (or
a
subset of) the dimensions considered. Lastly, it performs the
simulation for the stochastic hybrid system considered in the fourth
case study. We intend to employ the artifact as a demo of StocHy with
the aim of highlighting its ease of use and scalability.