source: vis_dev/vis-2.1/examples/minmax/minMax.ltl @ 11

Last change on this file since 11 was 11, checked in by cecile, 13 years ago

Add vis
File size: 718 bytes
Line 
1#FAIL: a specified reset state must eventually be reached from every state.
2# This formula fails in spite of the fairness conditions.
3G(F(min[8:0]=b111111111 * last[8:0]=0 * max[8:0]=0));
4
5#PASS: The non-reset states reachable in one clock cycle from the reset
6# states have min == last == max.
7G(min[8:0]=b111111111 * max[8:0]=b000000000 ->
8  X(min[8:0]=b111111111 * max[8:0]=b000000000 +
9    min[8:0] == last[8:0] * last[8:0] == max[8:0]));
10
11#PASS: The non-reset states reachable in two clock cycles from the reset
12# states have either min == last or last == max.
13G(min[8:0]=b111111111 * max[8:0]=b000000000 ->
14  X:2(min[8:0]=b111111111 * max[8:0]=b000000000 +
15      min[8:0] == last[8:0] + last[8:0] == max[8:0]));
Note: See TracBrowser for help on using the repository browser.