| Output
agreement check |
|
|
|
|
|
|
|
|
|
|
|
|
| • | AG
((RA = Climb) implies (DMG > 0)) |
||||||||||
| – | If
Resolution Advisory is Climb, then |
||||||||||
| Display_Model_Goal is positive |
|||||||||||
| • | Counterexample
was found |
||||||||||
| – | t0 : RA = Descend, DMG = -1500 |
||||||||||
| – | t1 : RA = Increase-Descend, DMG = -2500 |
||||||||||
| – | t2 : RA = Climb, DMG = -1500 |
||||||||||
