Advanced Contract Ananlysis
Analyzing property “CmadAcc <= 0 After BreakCmd >0 Until BreakCmd
0 || BreakCmd NoVal” fails with a 1-step-counterexample (in Context of
component AccelerationControl).
This seems to be incorrect — since at least 2 steps are needed to
falsify this property (or after has a somewhat unusual
interpretation).
The counterexample here check the after-proerty in the same state as the
property required to be true:
Verified System: 'AccelerationControl'
= State 1 =
AccelerationControl : Off
AccelerationControl.ReqSpeedAcc: NoVal
AccelerationControl.CmdAcc: NoVal
AccelerationControl.AccCmd: NoVal
AccelerationControl.ReqDistAcc: NoVal
AccelerationControl.AccMode: NoVal
AccelerationControl.BreakCmd: 126
(from redmine: issue id 1366, created on 2013-04-24, closed on 2018-04-09)