
Initial 

LTLSPEC
 

G((carStatus = PREPARE_FOR_PARALLEL_PARKING & obstacle = BLOCKED)
 

-> (keepCounterValue)
 

);
 

