// VERIFY travelPreparation  AGAINST
// BEGIN

// (1) this is a possible combination of choices
EF (hotel * car);											

// (2) this is the only possible combination of choices
AF (hotel * car);		

// (3) this is an impossible combination of choices 
! EF (train * car);	

// (4) any travel planning will be finished finally 						
AG (next_vacation -> AF (ready) );									

// (5) atomic use of the phone only, the phone is never reserved over several steps
AG (phone);					

// (6) liveness of T end_preparations						
AG (EF (accommodation * transport_means * luggage) );

// (7) livelock freedom/progress of T end_preparations  	
AG (AF (accommodation * transport_means * luggage) );

// (8) undone luggage will always be done in one step
AG (luggage_open -> AX (luggage) );

// (9) it is possible that undone luggage will be done in one step
AG (luggage_open -> EX (luggage) );

// (10) undone luggage will be done finally
AG (luggage_open -> AF (luggage) );

// (11) luggage will remain undone until it is done
A (luggage_open U luggage);

// (12) if the luggage is undone, it remains undone until it is done
AG (luggage_open -> A (luggage_open U luggage) );

// END.