Contracts: checking
if P then Q in maximum N steps hangs (even for 1 ste
Reproducing:
- Simple Traffic Lights with Specification Patterns
- Contract Specifications ->Contracts
- P: behaviorInRequest Present(), Q: behaviorOutIndicatorSignal On()
- For “if P then Q one tick later” works and the correct result is “fail”.
- Same for “N = 1”: nothing happens, or at least, nothing visible
(from redmine: issue id 905, created on 2012-07-09, closed on 2012-07-09)
- Relations:
- parent #814 (closed)