diff options
| author | Alex Auvolat <alex.auvolat@ansys.com> | 2014-07-23 17:41:49 +0200 |
|---|---|---|
| committer | Alex Auvolat <alex.auvolat@ansys.com> | 2014-07-23 17:41:49 +0200 |
| commit | 743f5cd5fb39e3ec58f94e43fe25ae8c25de7443 (patch) | |
| tree | 34a3e7e660c1d1400f33704a6fc2468407b87c6c /tests/kind2-examples/a_two_counters.scade | |
| parent | d3010ba184f1b2f066efa1b6683e797558e7a21a (diff) | |
| download | scade-analyzer-743f5cd5fb39e3ec58f94e43fe25ae8c25de7443.tar.gz scade-analyzer-743f5cd5fb39e3ec58f94e43fe25ae8c25de7443.zip | |
Add a few examples from KIND2 distribution.
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 + |