Add Promela model for Car Alley
Add liveness property check (but still need to verify with the lecturer)