Project

General

Profile

Actions
Copy link

Task #6465

closed

SMV array element extraction using a variable

Added by Mikhail Lebedev over 8 years ago. Updated about 8 years ago.

Status:
Closed
Priority:
Low
Assignee:
Mikhail Lebedev
Category:
Engine (Printer)
Target version:
-
Start date:
12/01/2015
Due date:
% Done:

100%

Estimated time:
Detected in build:
svn
Published in build:
0.2.1

Description

NuSMV and NuXMV allows element extraction only by using a constant or a variable of a set type:

x : array 0..7 of integer;
i : 0..7;
y : word[32];
x[0] := 1; - OK.
x[i] := 2; - OK.
x[y] := 3; - causes "Array access out of bounds" error.
next(i) := i + 1; - causes "Cannot assign value 8 to variable" error.

This problem has been detected in b07 and b08 itc-99 examples.
It has to be solved.

Actions
Copy link

Also available in: Atom PDF