Basic Examples | Index |

This is a specification of a coffee machine which can deliver coffee or tea.
The first transition from `PreInit_Start`

state to `Begin`

state is the initial transition, with an initial condition on symbolic constant(`price`

) of the system. The next transition
from `Begin`

to `Idle`

initializes local variable total, as in IOSTS model all the variables must be initialized to be used. Then coffee machine is waiting for customer to insert coin.
Here the condition to accept coin, is that coin must be greater than zero. In that case
the transition is fired, and the amount inserted is stored in variable total.
If the total is greater than the expected price, the machine get back money and the customer
is allowed to choose a beverage. If the total is lower than expected price the machine informs
the customer about the amount he must insert to choose beverage.
When the customer choose a beverage the machine store the choice in a variable. Then the machine
delivers the beverage. The customer can also cancels his actions and then the machine give him
his money back.

With this test purpose we want to test that the coffee machine is able to deliver some
coffee. Transitions which lead to `Reject`

state are used to discard executions involving Cancel command and we want that enough money is always given to the coffee machine.

This is the test case produced by stg. The transitions leading to `Fail`

state are removed
for readability. Moreover the selection and the simplification steps have removed
`Inconclusive`

state.
^{1}

The
specification
describes a program which is waiting for two successive integers `x`

and `y`

and emits `ok`

when their difference is greater than 2 and `nok`

otherwise.

The
test purpose
specifies that a test of interest is one that after three iterations, `ok(n)`

(with n<=300) is emitted.

The
product
IOSTS is performed and the
test case
is obtained after reachability and coreachability analysis.

F Ployette, F-X Ponscarme, April 5, 2007

Basic Examples | Contents | Index |