Skip to content

Commit cf060eb

Browse files
committed
SMV: KNOWNBUG test for integer range with negative numbers
1 parent 2c6ea1e commit cf060eb

File tree

2 files changed

+30
-0
lines changed

2 files changed

+30
-0
lines changed
Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
KNOWNBUG
2+
range_type10.smv
3+
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
--
7+
--
8+
This fails to parse.
Lines changed: 22 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,22 @@
1+
MODULE main
2+
3+
VAR x : 1..6;
4+
VAR y : -6..-1;
5+
6+
ASSIGN init(x) := 1;
7+
ASSIGN init(y) := -1;
8+
9+
ASSIGN next(x) :=
10+
case
11+
x=6 : 1;
12+
TRUE: x+1;
13+
esac;
14+
15+
ASSIGN next(y) :=
16+
case
17+
y=-6 : -1;
18+
TRUE: y + -1;
19+
esac;
20+
21+
-- should pass
22+
LTLSPEC G x + y = 0

0 commit comments

Comments
 (0)