Project

General

Profile

Support #2657

[Analysis] fake enum values in nusmv enums

Added by Anonymous about 4 years ago. Updated over 1 year ago.

Status:
New
Priority:
Normal
Assignee:
-
Category:
-
Target version:
Start date:
08/01/2016
Due date:
% Done:

0%

Estimated time:

Description

nusvm treats variables of single valued enums as constants, which results in an error in case an assignment is made to them. States and enums in AF3 models are converted to enums in nusmv. There are 3 (possible) ways to deal with that in my opinion (arranged in ascending order for the amount of work needed):
1) add a fake value to the enum. Currently it is done like that.
2) explore if there is an option for nusmv to not consider single valued enums as constants.
3) when transforming to nusmv consider such cases and do not use the assignments for them in the next expressions (possibly do not even need to create variables for them).

History

#1 Updated by Anonymous over 3 years ago

  • Assignee changed from Anonymous to Anonymous
  • Target version changed from AF3 2.10 Post-release to AF3 2.11 Post-release

#2 Updated by Simon Barner over 2 years ago

  • Target version changed from AF3 2.11 Post-release to AF3 2.13 RC1 (Feature Freeze)

#3 Updated by Anonymous over 2 years ago

  • Target version changed from AF3 2.13 RC1 (Feature Freeze) to AF3 2.14 RC1 (Feature Freeze)

#4 Updated by Johannes Eder over 1 year ago

  • Target version changed from AF3 2.14 RC1 (Feature Freeze) to Backlog

Also available in: Atom PDF