Project

General

Profile

Bug #1528

Unable to model-check with NuSMV when one uses assignment of arrays

Added by Anonymous about 7 years ago. Updated about 7 years ago.

Status:
Closed
Priority:
Normal
Assignee:
-
Category:
-
Start date:
07/26/2013
Due date:
% Done:

0%

Estimated time:

Description

e.g. OutputPortWithArrayType = InputPortWithArrayType

It is unclear also how the NuSMV works - a question was posted on the NuSMV users list

https://list.fbk.eu/sympa/arc/nusmv-users/2013-07/msg00010.html

History

#1 Updated by Anonymous about 7 years ago

  • Status changed from New to Closed

nusmv does not support arrays assignment as described here:
https://list.fbk.eu/sympa/arc/nusmv-users/2013-07/msg00015.html

thereby, the assignment of arrays does not represent a language subset that we allow for model-checking

Also available in: Atom PDF