Reference ManualUser ManualIntroductionBasic Examples



Basic Examples

A Coffee Machine Specification

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.

A Test Purpose

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.

The generated test Case

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

Another basic example

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

Reference ManualUser ManualIntroductionBasic ExamplesContentsIndex