Bug in Transformation to NuSMV: Selecting "default" value instead of NoVal
In the attached model, the model checker shows some strange behavior.
1) When checking the specification atom, the check fails and the counterexample says that “Component.lowBeamHeadlights: LowBeamHeadlights_Off()” in state 3. This, however, is not possible with respect to the given code specification. There is not a single assignement of lowBeamHeadlights to LowBeamHeadlights_Off() in the specification. I think this is a proble of the NoVal handling.
2) To avoid NoVal, one could add two assumptions to the component “exteriorBrightness!=NoVal” and “lightRotarySwitch!=NoVal”. After doing this, the original check succeeds. However, this is also not correct. The contract should fail with the given contract specification for an execution, with “exteriorBrightness ExteriorBrightness_SmallerThanS1() && lightRotarySwitch LightRotarySwitch_Auto()” in state 1 and “exteriorBrightness == ExteriorBrightness_BetweenS1andS2()” in state 2 (according to the code spec then the output is NoVal but accoring to the contract it should be LowBeamHeadlights_On())
I interpreted the used specification pattern in a way that P is true in each step between Q and R (and not only in at least one).
(from redmine: issue id 1846, created on 2013-11-28, closed on 2013-12-03)
- Uploads: