[Analyses] Counter-example coming from NuSMV does not fill in all the values
To reproduce:
- open the attached model
- go to the “A/G Contracts Patterns” part of “Component0”
- check the only specification atom (“Check Selected”)
- in the counter-example view which just got filled in, click on the button “Open Simulator”
- in the simulator, open Component1
- run one step of the simulation
Expected:
- the left channel (from Component1.Input to Component2.Input) should get the value “2”
What actually happens:
- the left channel (from Component1.Input to Component2.Input) gets “NoVal”
Remark:
- By observing Component0 instead of Component1 during the simulation, one can see how the input indeed gets “2”.
- This can be observed even more directly by looking at the counter-example in the Counter-example view
So the problem is that some values are set to NoVal when they actually
have a value.
However NuSMV does not provide directly this value so a lil bit more
work than just parsing has to be achieved.
(from redmine: issue id 2123, created on 2014-09-04, closed on 2015-01-29)
- Relations:
- relates #2071 (closed)
- Uploads: