Y2U: A Tool for Transforming Yakindu Statecharts to UPPAAL Timed Automata

Infinite Loop Test Case

Considering the program S ≡ x := 1; while x > 0 do S1 od, where S1 ≡ [x := 0||x := x + 1] is a parallel program with two threads. If the first thread of S1 executes once, the program S terminates; otherwise, S diverges. Fig. 5 depicts the automata executing S in Yakindu and UPPAAL, respectively. With finite simulations in Yakindu, we can not guarantee that the end state is reachable though all simulations reaches end. However, the result of checking the property A <> S.end by UPPAAL is not satisfied, indicating that the loop may diverge.

The test case shows that UPPAAL raises the issue of possible infinite loop within the model, while Yakindu is not able to identify with limited number of simulations.

Infinite Loop Test Case