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.

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.

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.

Used configuration file.

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

The verification results are displayed in the report below.

Assertion | States | Transitions | Time | Result |
---|---|---|---|---|

P_deadlock_free | 28 | 35 | 0.002 seconds | true |

Assertion | States | Transitions | Time | Result |
---|---|---|---|---|

P_out_1 | 28 | 35 | 0.005 seconds | 0.16666650772094727 |

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 | 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 | States | Transitions | Time | Result |
---|---|---|---|---|

R_out | 28 | 35 | 0.005 seconds | 3.6666641235351562 |

Model checking result:

Simulation result:

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.

Deramore Lane, University of York, Heslington, York, YO10 5GH, UK

Tel: 01904 325500

University of York legal statements