diff options
Diffstat (limited to 'tests/kind2-examples/a_two_counters.scade')
| -rw-r--r-- | tests/kind2-examples/a_two_counters.scade | 25 |
1 files changed, 25 insertions, 0 deletions
diff --git a/tests/kind2-examples/a_two_counters.scade b/tests/kind2-examples/a_two_counters.scade new file mode 100644 index 0000000..687c54a --- /dev/null +++ b/tests/kind2-examples/a_two_counters.scade @@ -0,0 +1,25 @@ +node top + (x: bool) +returns + (OK: bool) + +var + V13_b: bool; + V14_d: bool; + V40_a: bool; + V41_b: bool; + V51_time: int; + +let + + V51_time = (0 -> (if ((pre V51_time) = 3) then 0 else ((pre V51_time) + 1))); + V41_b = (false -> (pre V40_a)); + V40_a = (false -> (not (pre V41_b))); + V14_d = (V51_time = 2); + V13_b = (V40_a and V41_b); + OK = (V13_b = V14_d); + + guarantee PROPERTY: OK; + +tel + |