[Analysis] NuSMV transformation of boolean variables as expressions is faulty
having a Guard like “Input != NoVal && !Input” seems to produce a NoVal check after patching NoVal checks resulting in an undefined Variable “module.NoVal” in the NuSMV model.
Also, maybe fix != Noval Checks to be transformed to _PRESENT instead of !(!(_PRESENT))
(from redmine: issue id 2830, created on 2017-02-09, closed on 2017-02-20)
- Relations:
- parent #2834 (closed)
- Uploads:
- NoValtoFalse9-3508626057274148088.smv produced NuSMV file
- NoValtoFalse9-3508626057274148088.smvcmd NuSMV cmd to run
- BooleanBug.af3_23 Project demonstrating Bug