// WITH_BDD=1 marcie --net-file=travelPreparation.andl --ctl-file=travelPreparation-marcie-bdd.ctl
//
// caution: U operator requires [ ], otherwise one gets syntax error

// (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] );