| For every shuttle it holds that in every state it can eventually form a convoy with another shuttle. | |
| forall s:Vehicle . val(isShuttle(s)) => ([true*] ( exists t:Vehicle. val(isShuttle(t)) && (<true*.createConvoy(s,t)> true )) ) | |
| For every shuttle it holds that in every state it can eventually form a convoy with another shuttle only by moving itself. | |
| forall s:Vehicle . val(isShuttle(s)) => ([true*] ( exists t:Vehicle. val(isShuttle(t)) && (<move(s)*.createConvoy(s,t)> true )) ) | |