[Analysis] fake enum values in nusmv enums
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):
- add a fake value to the enum. Currently it is done like that.
- explore if there is an option for nusmv to not consider single valued enums as constants.
- 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).
(from redmine: issue id 2657, created on 2016-08-01)