$1.$ Consider the following informal specification of a traffic light controller for a bridge that has only one

lane $($for both directions$)$:

$$ At each end of the bridge, there is a traffic light that can be either red or green. This can

be modeled with a signal TA$,$ TB $\{$red; green$\}$ for the two ends A and B of the bridge.

$$ At each end, there are also sensors that detect the presence and number of cars that are

waiting to cross. Assume that there are at most $10$ cars at each end at any time. These

can be modeled with counters WA$,$ WB for the two ends of the bridge.

$$ At any time, a car travelling from A to B is either waiting at A$,$ or has passed across the

bridge. The presence of a car waiting at A is modeled with WA$.$ Passage across the bridge

only occurs when the traffic light TA is green; it is instantaneous and is modeled by a

decrement to WA$.$ There is no need to keep track of a car after it leaves the bridge.

$($Similarly for cars that travel B to A$.)$

$$ Once a car starts waiting at one end to use the bridge, it continues to wait until it passes

onto the bridge.

$$ Both lights start out red with no cars at either end.

$$ If there is at least one car waiting at end A and none at end B$,$ then TA turns green.

$($Similarly for the symmetric case at end B$).$ If both lights are red and cars arrive

simultaneously at both ends, then non$-$deterministically one of TA and TB is chosen to

turn green first.

$$ If light TA is green, and there are cars waiting at B$,$ the number of cars allowed to pass

the bridge from A to B is limited to $5$ from that time point; when that bound is reached

or no cars remain at A$,$ TA turns red and TB turns green. If there are no cars at end B$,$

then TA continues to stay green until a car arrives at B$,$ from which time point the bound

of $5$ is imposed on the A to B direction. $($Symmetrically for end B$.)$

$($Q$1)$ Model the above controller with an environment that models the arrival and passage of cars.

$($Q$2)$ Formulate the below$-$mentioned properties in LTL and verify whether your model satisfies

them. In case the model does not satisfy a property along a path, return the path as counterexample.

Safety Property: TA and TB are never green at the same time.

Liveness Property: If a car is waiting to pass the bridge at an end with a red traffic light, that

traffic light eventually turns green.