Department of Computer Science

Six-sided Die

Introduction

The six-sided die example, that use a fair coin to emulate a six-sided die, is a very basic example for the probabilistic analysis. Though it is not a robotic example, we still use it to show how RoboChart/RoboTool models and analyses it by using the PRISM model checker. The original PRISM model can be found here. This report documents the corresponding RoboChart model, analysis of its probabilistic behaviour through the automatically generated PRISM model.

Model (download)

The RoboChart model has only one state machine called dieSTM. A local variable d records the output of the die (from 1 to 6) when it is in the Out state. Additionally, an event flip indicates each flip of a fair coin.

Analysis with assertion language

We use the probabilistic assertion language of RoboChart. The assertion language finally will be translated to the PRISM’s property langauge, but the assertion language is a more user-friendly way to verify probabilistic properties. Information about how to use the probabilistic assertion language can be found in RoboChart and RoboTool reference manuals.

Generated PRISM model (download)

Used configuration file.

Assertions (download)

The assertion file that is used for verification is shown below.

Reports

The verification results are displayed in the report below.


Results of analysis of assertions in die.assertions using PRISM

Assertion: P_deadlock_free

Assertion States Transitions Time Result
P_deadlock_free 28 35 0.002 seconds true

Assertion: P_out_1

Assertion States Transitions Time Result
P_out_1 28 35 0.005 seconds 0.16666650772094727

Assertion: P_out_x

Assertion Const States Transitions Time Result
P_out_x xx=1 28 35 0.006 seconds 0.16666650772094727
P_out_x xx=2 28 35 0.004 seconds 0.16666650772094727
P_out_x xx=3 28 35 0.004 seconds 0.16666650772094727
P_out_x xx=4 28 35 0.005 seconds 0.16666650772094727
P_out_x xx=5 28 35 0.006 seconds 0.16666650772094727
P_out_x xx=6 28 35 0.004 seconds 0.16666650772094727

Assertion: P_out_x_sim

Assertion Const States Transitions Time Result
P_out_x_sim xx=1 0.1775
P_out_x_sim xx=2 0.163
P_out_x_sim xx=3 0.1495
P_out_x_sim xx=4 0.17
P_out_x_sim xx=5 0.177
P_out_x_sim xx=6 0.1525

Assertion: R_out

Assertion States Transitions Time Result
R_out 28 35 0.005 seconds 3.6666641235351562

Model checking result:

Simulation result:

Conclusion

The six-sided die is a very basic example in probabilistic verification. By using this, we demonstrate how our RoboChart models it using state machine diagrams and how RoboTool analyses its probabilistic behaviour using automatically generated PRISM model.

Department of Computer Science
Deramore Lane, University of York, Heslington, York, YO10 5GH, UK
Tel: 01904 325500