|
|
|
| Bug example, preservation of |
||
| invariants |
||
|
|
|
|
|
|
|
|
|
|
| • | Assert
that the safety condition is preserved |
||||||||
| assert
PolicyWorks { |
|||||||||
| all t | TrainsMove(t) &&
Safety-> Safety’ |
|||||||||
| } |
|||||||||
| • | Counterexample
returned: a new train was |
||||||||
| created
during the operation…crunch! |
|||||||||
| • | Fix
by adding to operation |
||||||||
| Trains
= Trains’ |
|||||||||
