Skip to content

Commit 7aa4f8b

Browse files
committed
SMV: range types are enum types
The range types x..y are syntactic sugar for the explicit enumeration {x, ..., y}.
1 parent fd24964 commit 7aa4f8b

File tree

2 files changed

+19
-0
lines changed

2 files changed

+19
-0
lines changed
Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
KNOWNBUG
2+
range_is_enum1.smv
3+
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
--
7+
^warning: ignoring
8+
--
9+
Conversion from range to enum not supported.
Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
MODULE main
2+
3+
-- range types are syntactic sugar for enumeration types
4+
VAR x: 0..6;
5+
VAR y: {0, 1, 2, 3, 4, 5, 6};
6+
VAR z: 0..6;
7+
8+
ASSIGN x := y;
9+
ASSIGN y := z;
10+

0 commit comments

Comments
 (0)