Uppaal (model checking tool) and Corectness Criteria for Beginners
Channel: Maria Bianca
Date: 10/07/2017

Scenario:
In the first activity, we assume that there are  two cars that simultaneously search for parking space.  The cars can move forward and backwards and their sensors will query a parallel automaton that models the street layout. Upon finding an available parking space they will move forward to reach the end of the available parking space and perform parallel reverse parking. Afterwards (after a fixed or arbitrary delay) they will move out of the parking space and move forward to the end of the street. For simplicity, assume that the street is 5 meters long, it has 2 suitable parking spaces (they may be fixed or randomly assigned in your model) and each car needs 1 meter space for parking. The only way for parallel automata to communicate is through shared channels; no other globally shared variables are allowed. 

Corectness Criteria Cases:
1.  There is no state of deadlock when both cars end up at the end of the street.
A[] (deadlock imply (rLane.end_street and lLane.end_street))

2. Only one car can park in the first parking space at a time
A[] ((carOne.position == 2 and carOne.parked == true) imply ((carTwo.position != 2 or carTwo.parked == false) or (carTwo.position != 2 and carTwo.parked == true) or (carTwo.position == 2 and carTwo.parked == false))

3. The cars should not be able to drive longer than the 5 meters street.
A[] rLane.street_length smaller 6 and lLane.street_length smaller 6

The case that failed:
A[] rLane.street_length smaller 6 and lLane.street_length smaller 3