Accumulating an amount in a cycle | Index |

The aim of this example is to show that STG is able to constraint the value of a threshold such that it will be lesser than the accumulating amount. This implies that STG uses a fixpoint solver as the amount value is incremented in a cycle.

The specification first reads two integer values: the threshold and the number of cycles, then the cycles takes place, incrementing the amount of 10 and after max cycles, it sends ok if the amount if greater then the threshold and nok otherwise.

The test purpose selects testcases where ok is emitted.

In the generated testcase, the values of the threshold and max are binded by the relation threshold <= max*10.

F Ployette, F-X Ponscarme, October 17, 2007

Accumulating an amount in a cycle | Contents | Index |