|
Trull | ||||||||
| PREV PACKAGE NEXT PACKAGE | FRAMES NO FRAMES | ||||||||
See:
Description
| Interface Summary | |
|---|---|
| EventLabels | Event labels for the office demo. |
| Class Summary | |
|---|---|
| Building | An office building. |
| ControlPanelUI | The central control panel for an office building. |
| EconomyControl | The economy control logic for an office. |
| Main | A driver for running an office building. |
| OccupantControl | The occupant control logic for an office. |
| Office | An office in an office building. |
| OfficeControl | An office control logic that switches between occupant control and economy control. |
| OfficeControl.EmitSetTemp | A component that emits a SETTEMP event with the requested temperature. |
| OfficeUI | The occupant control panel for an office. |
| Temp | A representation of a temperature. |
| TemperatureStableOffice | A temperature-stabilized office. |
| Thermostat | A simple thermostat. |
Demonstrates an environmental control system for an office building (run this demo).
To introduce Trull and illustrate various features of Trull, we describe an environmental control system for an office building. The design of this system is compositional; aided by Trull constructs, the implementation reflects this structure.
We begin with the notion of an office I/O, which is a system that accepts as input the events that control the environment of an office (heating and lighting) and emits as output the various events necessary to communicate with the rest of the environment-control system. Some of these emitted events may originate from an action by a human occupant (switch on/off, door open/close, and temperature request). The remaining output event is a physical temperature reading, which may be automatically generated from time to time. Office I/O illustrates the decoupling of system components supported by Trull. The events emitted by an office I/O may be asynchronous with the rest of the system. Furthermore, an office I/O may contain its own autonomously evolving state--e.g., a process that controls how often temperature readings are emitted based on how fast the temperature is changing.
A thermostat partially automates the temperature control of an office. An office I/O combined with a thermostat is called a temperature-stable office. The pseudocode realization in Trull of these processes is shown below, along with a diagram giving the interface of each process in terms of the events that it emits and accepts. Note that some events carry temperature data.
Thermostat:
Temp actual_temp = INITIAL_ACTUAL_TEMP;
Temp target_temp = INITIAL_TARGET_TEMP;
loop
await TEMP(t) ->
actual_temp = t;
emit (t < target_temp) ? HEATON : HEATOFF
| SETTEMP(t) ->
target_temp = t;
emit (actual_temp < t) ? HEATON : HEATOFF
Temperature_Stable_Office:
Office_IO io;
Thermostat therm;
local HEATON HEATOFF TEMP in
io || therm
The loop combinator in the thermostat implements an ``event loop''; the body of the loop terminates after handling any event and restarts with the next event. The body of the loop is a parallel composition (using the || combinator) of two processes. The first process responds if the current event is of the form TEMP(t) (a physical temperature reading); on any other event, it terminates silently. It is similar for the second process and events of form SETTEMP(t). Thus, the body of the loop is essentially a selection construct on the input events { TEMP(t), SETTEMP(t) }. In both parallel components, two things happen on receipt of the specified event: an assignment takes place and an event is emitted to control a heater. The assignment is an action, written between braces, and may in general be any code in the host programming language (typically something that terminates quickly). The emit combinator emits an event. Events are delivered eventually (and simultaneously) to all interested listeners and the emitting process terminates. Trull thus distinguishes event emission from arbitrary Java actions.
A thermostat is attached to an office I/O simply by composing them in parallel, yielding a temperature-stable office process as illustrated above. The parallel composition automatically ensures that the HEATON, HEATOFF, and TEMP(t) events are transmitted between the two subprocesses. In this case, these three events are hidden with the local combinator so that they are not accessible externally as either inputs or outputs, as shown in the diagram above.
The occupant of an office should have manual control over the heat and lights. This is done with the occupant control process that essentially renames events.
Occupant_Control:
loop
await REQUESTTEMP(t) -> emit SETTEMP(t)
| SWITCHON -> emit LIGHTON
| SWITCHOFF -> emit LIGHTOFF
Upon SWITCHON, the above process will eventually emit LIGHTON. Trull makes no guarantee as to the timing of event emission, so it is possible that SWITCHOFF could arrive before LIGHTON is emitted and thus would not actually turn off the light. Later, we will show a programming style to bulletproof against such cases. But in this case, SWITCHON and SWITCHOFF originate from human actions, and because we can reasonably assume that the light comes on faster than a human can flip the switch, we would not expect the bad case ever to occur. Trull supports a notion of ``assert'' statements appropriate for concurrent programs, namely temporal-logic formulas, to express such safety properties. These properties express the assumptions under which a piece of Trull code functions correctly, in the spirit of preconditions in Hoare-style rules for sequential programs. For instance, the formula
LightOnPending =def ! LIGHTON since SWITCHON
expresses the property of a single point during an execution run that ``LIGHTON did not occur since the most recent SWITCHON.'' Then, the formula
SwOffSafety =def always (SWITCHOFF => ! LightOnPending)
expresses the property of an entire execution that ``whenever SWITCHOFF occurs, there is no pending LIGHTON''. Adding SwOffSafety (and the symmetric property for SWITCHON) to the office program generates a run-time error whenever the property is violated. Similar properties would be appropriate for the thermostat process.
An office can be in two modes, occupant mode and economy mode. Occupant mode is the normal mode of operation, as implemented by the occupant-control process above. In economy mode, the temperature is reduced to and held at a specified value, despite any requests otherwise, and the lights are turned off and the switch disabled. The ECONOMYMODE(t) event puts an office into economy mode, lowering the temperature to t, and the OCCUPANTMODE event returns the office to occupant mode, restoring the requested temperature to the most recent observed request. In addition, if an office is in economy mode, it should temporarily revert to occupant mode when the door is open, in case someone arrives in the middle of the night to work; in that case, the office returns to economy mode when the door is closed.
The economy control process implements this control, emitting SLEEP(t) whenever the office should enter economy mode, lowering the temperature to t, and emitting AWAKE(t) whenever the office should return to occupant mode, restoring the temperature to t. The process runs three subprocesses in parallel. The first one monitors continuously the last requested temperature (done is the ``skip'' of Trull ; it does nothing and terminates immediately). The second and third parallel components to determine when the office should change modes. The code structure
loop
ECONOMYMODE(t) -> do
...
watching OCCUPANTMODE
|| loop
OCCUPANTMODE -> do
...
watching ECONOMYMODE
establishes mutual exclusion between the occupant mode and economy mode. The invariant maintained is that the mode is determined by the last occurrence of the events ECONOMYMODE and OCCUPANTMODE. This structure also illustrates the technique of preempting a process to establish priorities on events -- the events ECONOMYMODE and OCCUPANTMODE have higher priority than the events occurring in the ... above.
On receipt of event ECONOMYMODE, a process enters a loop that monitors the status of the office door. The invariant upon entry to the loop is that the office has just been placed in economy mode and needs to be put to sleep. While SLEEP is being emitted, the await combinator waits until DOOROPEN occurs. In the case that DOOROPEN arrives while the emission of SLEEP is still pending, the emission is aborted via the do/watching combinator to ensure consistency. When the door becomes open, a symmetric process emits AWAKE and waits for DOORCLOSE. On receipt of OCCUPANTMODE, the door-monitoring loop is preempted and the office returns to occupant mode. The code handles the possibility that ECONOMYMODE will arrive while AWAKE is still pending.
Economy_Control:
Temp last_temp = INITIAL_TARGET_TEMP;
Temp economy;
loop
REQUESTTEMP(t) -> last_temp = t;
done
|| loop
ECONOMYMODE(t) -> economy = t;
do
loop
do emit SLEEP(economy) watching DOOROPEN
|| await DOOROPEN ->
do emit AWAKE(last_temp) watching DOORCLOSE
|| await DOORCLOSE -> done
watching OCCUPANTMODE
|| loop
await OCCUPANTMODE ->
do emit AWAKE(last_temp) watching ECONOMYMODE
Now we build an office control process from an occupant-control process and an economy-control process. Note that the occupant-control process must be disabled during economy mode. This is done with the suspend/resume combinator, which suspends a process on receipt of a specified event (SLEEP in this case) and resumes it on another event (AWAKE in this case). Thus, whenever the economy control sends a SLEEP event, the occupant will lose control of the light and heat until the economy control sends an AWAKE event. Two processes (not shown in the picture) run in parallel with the occupant control and the economy control to adjust the light and heat appropriately whenever the office toggles modes; each preempts the other to avoid inconsistency. Note that parallel composition automatically routes REQUESTTEMP(t) events to both subprocesses that accept them.
Office_Control:
Occupant_Control oc;
Economy_Control ec;
local SLEEP AWAKE in
ec
|| suspend SLEEP resume AWAKE in oc
|| loop
await SLEEP(t) ->
do
emit SETTEMP(t)
|| emit LIGHTOFF
watching AWAKE
|| loop
await AWAKE(t) ->
do
emit SETTEMP(t)
watching SLEEP
The office control is rather complex, and so we may want to sprinkle in some temporal safety properties to be checked during execution. For instance, using definitions
Slp =def ! AWAKE since SLEEP
Awk =def (! SLEEP since AWAKE) \/ always (! SLEEP)
SwOn =def ! SWITCHOFF since SWITCHON
SwOff =def ! SWITCHON since SWITCHOFF
where always (! SLEEP) means that SLEEP never occurred (i.e., an office is initially awake), we define the following property to specify the behavior of the light:
LightSafety =def always ( (LIGHTON => Awk /\ SwOn)
\/ (LIGHTOFF => Slp \/ SwOff))
This specifies that whenever LIGHTON occurs, both the office must be awake (no SLEEP since the last AWAKE) and the switch must be on (defined similarly). Also, whenever LightOff occurs, either the office must be asleep or the switch must be off. Note that SLEEP xor AWAKE is a tautology, but that this is not quite true of SwOn xor SwOff because neither SwOn nor SwOff is true during an execution until the first SWITCHON or SWITCHOFF event.
To complete the implementation of a single office, we compose a temperature-stable office with an office control. The resulting office process emits no events and accepts only events ECONOMYMODE(t) and OCCUPANTMODE. The local combinator hides all other events.
Office:
Temperature_Stable_Office tso;
Office_Control oc;
local SWITCHON SWITCHOFF LIGHTON LIGHTOFF
REQUESTTEMP SETTEMP DOOROPEN DOORCLOSE
in
tso || oc
Finally, multiple offices are combined into an entire floor of an office building. The implementation below allows offices to be added one by one. The entire floor is commanded to be placed in economy mode and to be restored to occupant mode as a whole. However, while in economy mode, individual offices may temporarily revert to occupant mode due to door activity, as described above.
Building_Floor: Building_Floor bf; Office o; bf || o
We conclude this example by recalling our earlier comments about asynchronous communication. In a building with many offices, each office is mostly decoupled from the others. Logically, the only communication shared between them is the ECONOMYMODE(t) and OCCUPANTMODE events. Furthermore, each office I/O typically generates events asynchronously with the other offices. Trull supports this kind of decoupling, allowing each office to evolve autonomously of the others.
|
Trull | ||||||||
| PREV PACKAGE NEXT PACKAGE | FRAMES NO FRAMES | ||||||||