
);
 
-> (keepCounterValue)
 
G((carStatus = PREPARE_FOR_PARALLEL_PARKING & obstacle = BLOCKED)
 
Initial 
LTLSPEC
 
