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
 #1

Updated by Mikhail Lebedev about 8 years ago

b05 also encountered this problem.

Actions
Copy link
 #2

Updated by Mikhail Lebedev about 8 years ago

  • Status changed from Open to Resolved
  • % Done changed from 0 to 100

Solved by modulo division an array index by an array size:

MAR : word[32];
map0 : array 0..15 of integer;
map0[(MAR mod 0d32_16)]; - No error.

Actions
Copy link
 #3

Updated by Mikhail Lebedev about 8 years ago

  • Status changed from Resolved to Verified
Actions
Copy link
 #4

Updated by Sergey Smolov about 8 years ago

  • Status changed from Verified to Closed
  • Published in build set to 0.2.1
Actions
Copy link

Also available in: Atom PDF