Other examplesA lift simulation exampleAccumulating an amount in a cycle

Contents

Index

Accumulating an amount in a cycle

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


Other examplesA lift simulation exampleAccumulating an amount in a cycleContentsIndex