UCSC CMPE 278 Flexi Homework

Homework 4: Interface Automata Homework

For this homework, you have to model a car locking/lights/climatization system in flexi.

How to Install Flexi

First, you have to log into a linux machine; if you don't know which one to use, try lauhau.cse.ucsc.edu. If you have problems with access, let me know.
Add /projects/bubble/code/ocaml-3.06/bin to your PATH variable.
Go to a directory you like, put flexi.tgz into it, and untar it with tar xfvz flexi.tgz
cd flexi
Look at the README file.
Start Flexi with ./flexi You should get the prompt #.
A sample session is contained in the README file.

NOTES

You can run Flexi only from the flexi directory.
I put some sample inputs in the subdirectory cmpe278-inputs. Other subdirectories, with plausible names, contain inputs that do not work. This is not a bug: what I am giving to you is a snapshot of our ongoing development project, and not all input files have been updated to the current input syntax yet.
Try this as soon as possible, and let me know of any problems (permissions, incompatible executables, etc).

The Assignment

You have to model the control system that controls door locks, headlights, courtesy lights, and climatization of a car. It helps, to do the assignment, to know how a car works, so if you don't have one, I advise you to rent one. Just kidding!

The control system must consist of four different modules; each module should be modeled as one (or more, if you like) interface automata. Below I list the four modules, with their (approximative) function, and a partial list of their inputs and outputs. You must try to build somewhat "smart" modules. In particular, below I list only the signals that each controller sends to and receives from the car; the controllers must communicate one to the other in order to carry out their function. I leave it to you to design the inter-controller communication. Your solution will be graded for correctness, but also for the sophistication of the inter-controller interaction, and for the smartness of the global control solution. I give sample names to the signals, you can choose other names, but be sure to explain their function.

If you need, you are welcome to create auxiliary modules, for instance, to work as timers.

1. Lock Controller

The lock controller decides whether the doors are locked or unlocked. It has many goals: avoid forgetting the car parked and unlocked, avoid locking the keys inside the car, avoid kids from being able to open the rear doors if the signal "kids_locks_on" is received, enable the driver to open all doors by turning the key in a door lock twice, etc etc. The limit is your imagination, and your frustration with the last car you drove.

If something is too difficult to implement, explain the source of the difficulty: you don't have to handle all signals below, but try to produce an interesting solution.

Inputs from car:

Key_door_turn_driver. Is the key being turned on the driver door?
Key_door_turn_passenger. Is the key being turned on the passenger door?
Key_into_ignition. The key has been inserted into the ignition.
Key_outof_ignition. The key has been removed from the ignition.
Key_start_engine. The key is being turned to start the engine.
Key_stop_engine. The key is being turned to stop the engine.
Child_locks_on. The child locks are active: the rear doors cannot be opened from inside.
Child_locks_off. The child locks are active: the rear doors can be opened from inside.
Door_opens_XY, where X is F (front) or B (back), and Y is L (left) or R (right): a sensor that senses whether the door opens.
Door_closes_XY, where X is F (front) or B (back), and Y is L (left) or R (right): a sensor that senses whether the door closes.
Outputs to car:

Motor_start. The engine should start.
Door_lock_XY (see above for XY).
Door_unlock_XY.
Beeper_on. This is the annoying car beeper. Points will be deducted if you use this output!
Beeper_off.

2. Headlights.
This should be a smart headlights controller. You should make it difficult to park with the lights on, and you should coordinate headlights usage with the lock system.

Inputs from car:

Headlights_switch_on.
Headlights_switch_off.
Ambient_light_high.
Ambient_light_night.
Hand_brake_on.
Hand_brake_off.

Outputs to the car:

Turn_headlights_on.
Turn_headlights_off.

3. Courtesy Lights.
This should be a smart courtesy lights controller. You should make it difficult to park with the lights on, and you should coordinate courtesy lights usage with the lock system.

Inputs from car:

Courtesy_switch_on.
Courtesy_switch_off.
Courtesy_switch_door. This is the setting in which they are on only when a door is open.

Outputs to the car:

Turn_courtesy_lights_on.
Turn_courtesy_lights_off.

4. Climatization.
This should be a smart climatization controller. You may want to switch climatization off when a door is open, or when the engine is not running.

Inputs from car:

Is_hot.
Is_cold.
User_says_no_AC. AC cannot be used.
User_says_yes_AC. AC can be used.

Outputs to the car:

Turn_AC_on.
Turn_AC_off.
Turn_heat_on.
Turn_heat_off.

Advice
Start simple, and add complexity to your model in a gradual way. In order to get a good grade, your model needs to compose without incompatibilities, and it's better to turn in a working, but simpler, example, rather than a complex non-working (or worse, non-parsing) model.
You may want to draw your examples on paper before putting them into the flexi input format.
What you have to do

First, make a model, and check that the interface automata are compatible.
Look (if you can) at the input assumptions; what do they say? Try to give a few environment scenarios that are not allowed. For example, will the system panic if two copies of the key are used, for instance, one to start the engine, the other to lock the doors?
Construct some interface automaton representing the driver and a chaotic family, and see if everything is compatible.
Formulate some properties, in English, that you would like to check about your design (e.g., don't get to a state where you cannot lock or unlock the doors). We will see later in class how to do this specification.