[Analyses] Counter-example coming from NuSMV does not fill in all the values
- 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
- 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"
- 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.
#1 Updated by Anonymous over 5 years ago
- Status changed from New to Resolved
- Assignee changed from Anonymous to Andreas Bayha
- % Done changed from 0 to 100
At least for channels. Might be some other situations where similar problems happen though.
An ideal solution would be to rethink the way components' behaviour is implemented, but ok for now.