// marcie --net-file=travelPreparation.andl --ctl-file=travelPreparation-marcie-idd.ctl

// (1) this is a possible combination of choices
EF [hotel=1 & car=1];	

// (2) this is the only possible combination of choices
AF [hotel=1 & car=1];

// (3) this is an impossible combination of choices 
! EF [train=1 & car=1];

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

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

// (6) liveness of T end_preparations	
AG [EF [accommodation=1 & transport_means=1 & luggage=1] ];

// (7) livelock freedom/progress of T end_preparations 
AG [AF [accommodation=1 & transport_means=1 & luggage=1] ];

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

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

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

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

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