Recall the synchronous design of a cruise controller system from section 2.4.2 in Alurs book and Problem 3 in Homework Assignment 1. Consider the following requirement: when the cruise-controller is on, assuming the driver does not issue any further input events, eventually the speed becomes equal to the desired cruising speed and stays equal. Express this requirement in LTL using the variables on, speed, cruiseSpeed, cruise, inc, and dec.

prob 3 from assignment 1:

Problem 3 (40 points): In this problem, we will design a synchronous reactive component to set the cruising speed of a vehicle. This component corresponds to the SetSpeed component in the cruise-control system CruiseController.

The SetSpeed component takes the following inputs:

event(bool) cruise: This event models the user turning the cruise control on or off.

nat speed: This input models the speed input from the vehicle (corresponds to the current speed of the vehicle).

event inc: This input models the user requesting an increase in the cruising speed.

event dec: This input models the user requesting a decrease in the cruising speed. It has one output:

event(nat) cruiseSpeed: this output, if presents, contains the current cruising speed.

The component maintains two state variables: an enumerated type variable called mode = {on, off} that keeps track of whether the controller is turned on or off. a current desired (nat) speed s.

There are two constants called minSpeed and maxSpeed that we will use within the component. The operation of the component is as follows. The component updates the state variable on according to the following rule: every time the event cruise occurs, the variable mode is set to on. Then the component outputs the cruising speed using the cruiseSpeed output variable. If the current speed s is within the legal range minSpeed and maxSpeed, then the cruiseSpeed variable is set to s; if not, it is set to the closest legal value (i.e. minSpeed or maxSpeed). Also, when mode is on, if a dec event is received, then the cruising speed is decremented (restricting the lowest speed to minSpeed), and when the inc event is received, the cruising speed is incremented (restricting the highest speed to maxSpeed). If the mode variable is set to off, all input events except cruise are ignored, and there is no output.

a. Show the synchronous reactive component that implements this functionality.

b. Suppose we want to add another input control for the driver, pause, with the following desired behavior. When the cruise controller is on, if the driver presses pause, then the controller is temporarily turned off. In the resulting paused state, the output cruiseSpeed should be absent, and the events inc and dec should be ignored. Pressing pause again in this paused state should resume the operation of the cruise controller, restoring the desired speed on pausing. Pressing cruise in the paused state should switch the system off, and when the controller is off, pressing pause should have no effect. Redesign the component SetSpeed with this additional input event pause to capture the above specification. Hint: the component SetSpeed now maintains a state variable mode that can be either on, paused, or off, i.e., mode = {on, paused, off}.