Part (a). Draw a state diagram for a car with the following state variables: D indicating whether the car is in drive; B indicating the brake pedal is depressed; G indicating the gas pedal is depressed; and M indicating whether the car is moving. (For example, the state DB¬G¬M says that the car is in drive, the brake pedal is down, the gas pedal is not down, and the car is not moving). Your state diagram should obey the following properties:
The start state is ¬D¬B¬G¬M.
- To put the car in drive, the brake pedal must be down.
- To push the gas pedal, the car must be in drive.
- It is not possible to push both the gas and the brake at the same time.
- Once the gas is down, the car will eventually move.
- Once the car is moving, it is possible to stop the car by depressing the brake.
Part (b). For each of properties 1-4 listed in Part (a), write an LTL formula specifying the property, and make an informal argument why the property holds for your diagram.
Part (c). Is it possible to specify property 5 using an LTL formula? Justify your answer.