On this page we make available to source code of the case studies considered in the thesis. For an informal description of the case studies and the properties that we check, we refer to the thesis itself. Here, we simply provide the actual probabilistic programs that have been checked. We first give a link to the source code for each case study. Then, we explain how to define preprocessor macros to enable the properties mentioned in the thesis. Finally, we discuss how the parameters of the program can be adjusted by various preprocessor macros.
The basic ANSI-C source for each case study is available via the links below. We remark that the difference between source code used in the QPROVER and PROBITY tool is minimal. Essentially, PROBITY requires that probability values are specified as rationals, whereas QPROVER takes floating point numbers, meaning that they use slightly different function prototypes to realise probabilistic behaviour.
|MGALE + AMP + FAC||source||source|
|BRP + ZERO + CONS||source|
Properties are embedded in the source code of the case studies and must be enabled with appropriate macro definitions. When compiling the case studies, either for use in QPROVER or PROBITY, the following preprocessing macros must be defined:
|PING + PING-||__PROP3__||__PROP2__||__COST__||__PROP1__|
Akin to properties, the parameter space of our case studies is also set via preprocessor macros. We describe the available macros for each case study here. The probability macros are only macros in the QPROVER source.