The alarm and pressure module, or amp module, consists of:
1. an interface
with out variables alarm (of type boolean), two clocks c1 and c2, and the
control variable apm_pressure.
2. a specification in
temporal logic (to be explained later)
3. a body, which
is a clockchart as shown below.
Get the StateClock tool up and running( see Getting
Started)
Create a new project( see Creating
A Project)
1. Call the project
alarm_pressure.
2. Press OK to close the window.
3. The project alarm_pressure now shows in the Project
and Modular Structure fields.
4. (Once there is at least one project listed, pressing
the middle button in the Project field will result in a list of three operations:
Add, Remove
and Rename).
Create the apm module( see Adding a Module)
1. This project will consist of exactly one
module called apm.
2.Enter "apm" for the module name and press OK to close
the window.
3. (Note: It is best to use very short names for modules,
because all private variables v of the module will be called apm_v.)
Declare the interface variables( see Interface)
1.The Actual Interface Variable window allows us to add
a Data variable or a Clock variable to the apm module interface. We want
to declare a data variable
alarm in the Variable declaration field,
add "alarm: bool" and click on OK. The alarm variable is now listed as
a share variable (by default) with type boolean.
2.We want alarm to have mode out. Use the left mouse button
to select alarm. With the middle button held down with the cursor on alarm,
select the operation Change Mode--->Out.
3.(Similarly, selecting the operation Detail will produce
the window below:
The default initial value of alarm is false.
This is just what we want so there is no need to change it. From the Detail
window above,
the Initial Value and Mode can be changed,
but not the Type. If a variable c is declared with type CLOCK, then there
is an
associated increment variable C_c whose increment
can be set to +1 or -1 depending on whether the clock is counting up or
down.)
1.Two clock variables c1 and c2 must also be declared (use
the middle button and operation Add). Clock variables need not be given
a type as
they are all of type CLOCK. The list of interface
variables thus looks like:
A clock variable has the symbol "*" after it
to denote that it is a clock variable. The mode of a clock variable is
always out. Close the
interface window by clicking on button Close.
Create the body ( see Adding a Sub Module or Body and see States and Control Variables)
1. We must now add two parallel objects pressure and generate_alarm
to the blank canvas in the body window. With the middle button.
click on the blank drawing canvas and select
operation Add Primitive Object. The user is given the option to choose
a serial (XOR) object or
a parallel (AND) object. If the Return key
is pressed, the default chosen which is the XOR (in bold). In this case
we choose the AND option
because we are adding parallel sub objects.
The following window then appears prompting the user to fill in the name
of the parallel object.
After typing in pressure, press the accept
button.
2. Repeat the above once again for the parallel object generate_alarm. The drawing canvas now shows the two parallel objects.
3. Refine pressure --- XOR decomposition
4. Zoom In to the pressure object to refine it. The user
is presented with a blank canvas labeled pressure. The pressure object
is
decomposed into serial objects labeled normal
(to denote when the pressure is ok) and hi (to denote when the pressure
is high). To create
the first sub object normal, click with the
middle button on the canvas and select the operation Add Primitive Object.
A window is produced
giving the user the option to create either
an XOR or AND sub objects. this time choose XOR.
5. Each XOR object that has internal structure, must have
a corresponding control variable. Since the pressure object is XOR
decomposed into sub objects (i.e. normal and
hi) it must have a control variable, in this case called apm_pressure.
Note that
type(apm_pressure) = {normal, hi}. Press OK,
and enter the next sub object hi using the Add Primitive Object operation.
Note: the default object is normal (in bold),
i.e. execution starts at normal. (To change the default, invoke the operation
Primitive
Object--->Set Default (the "Primitive Object"
menu is at the top left of the body window).
6. We must now create the events go_hi[1,*] and go_low[1,*].(
see Events) These events each
have lower time bound of one time unit, and an upper
time bound of infinity. This means that they
delay for 1 tick (after becoming enabled) before they become eligible to
be taken. After that, they
may occur at any time (or never).
7. Depress the middle button with the cursor on normal
(this is the source object), and select the operation add event. You are
then prompted to select the destination object:
with the left mouse button click on the hi object. This brings up the dialog
box where
you must name the event: go_hi.
Press the return key and also enter the event
go_low. After moving the event arrows (click on the event with the middle
button and
choose the move operation) to improve the
view.
The primitive sub objects are numbered normal
(0) and hi (1). This is because StateClock will really think of normal
as 0 and hi as
1, and the labels can be thought of as comments
(e.g. object 0 is the "normal" object). Hence type(apm_pressure) = {0,1}.
(The
association between comments and numbers can
be changed using the Mapping operation in the main window.).
8. We must now set the lower bound of each event to zero.
this can be done by depressing the middle mouse button with the cursor
on the event
and selecting the bounds operation. Alternatively,
the detail operation can be selected. The pressure object now looks like:
We are now finished with the pressure sub object.
Click with the left button on the Zoom Out button.
The "@" symbol after pressure@ indicates that it
now has internal structure. We can invoke the Zoom In operation to examine
its
internal structure.
9.We can resize the pressure object so as to see its internal
structure. Move generate_alarm out of the way to create space to resize
pressure. With the middle mouse button held
down on pressure, select the resize operation. Click on the bottom right
point to which you
want pressure to resize to the desired size.
You must then select the expose operation to display the internal structure
as follows:
The graphics for exposing internal structure
does not always work smoothly. It is therefore best to first layout the
complete structure
unexposed, before fiddling with it to get
it to display internal structure.
10.You can now Zoom In to generate_alarm to refine its
internal structure. Try to follow the previous example for pressure to
complete the body as shown in
this final view of the system.
Note that
The control variable apm_pressure has been
exported as an out variable in the interface. There is an operation Make
Interface in the
Control variable field to do this. ( see Interface)
The control variable apm_pressure is used
in the guard of the PressureIsHi event to check when the pressure is high.
Note that the numeric
value must be used, i.e. apm_pressure = 1
rather than apm_pressure = hi.
Two clock variables c1 and c2 are used. The
action cd(c1(30)) starts clock c1 counting down from 30 ticks. The action
stop(c1) stops
stops the clock from counting down any further.
Also ct(c1) then becomes false. The start(c2) action starts clock c2 counting
up. Syntax of
guards and actions.
Specification in Temporal
Logic
Below is an example of a possible specification
file for this project. All comments are preceded by a %. The first line,
apart from comments, must be SPEC.
The specification file allows you to check certain properties, written
as boolean statements, against the .fts file generated by StateClock.(see
Generating the
FTS file)
The properties must be presented as follows: PROPERTY property name:
boolean statement. Here property name is a label of your
choice. The examples below use a number of macros. These macros allow you
to make your properties simpler and more readable. To define a macro, use
the following:
macro macro_name: data type where macro_name = boolean
statement. Look at the properties below, and once you understand them
try to introduce additional properties of your own.
Once you have generated your alarm_pressure.fts
file use the example below to create an alarm_pressure.spec file. ( see
Creating
the specification file) Then submit both to STeP. ( see
Connecting to STeP)
% apm module --- alarm on pressure
SPEC
% Each clock c has an associated clock increment variable C_c.
% When the clock is counting up: C_c1 = 1.
% When the clock is counting down: C_c1 = -1.
% The predicate ct(C_c) asserts that clock "c" is ticking.
macro ct(i:int) = (i != 0)
macro hi : int where hi = 1
% Some other macros
macro ticks: bool where ticks = (Event = tick)
macro pressureIsHi: bool where pressureIsHi = (apm_pressure = hi)
macro pressureGoHi: bool where pressureGoHi = (Event = apm_go_hi)
macro pressureGoLow: bool where pressureGoLow = (Event = apm_go_low)
macro start_c1: bool where start_c1 = (c1 = 30 /\ ct(C_c1))
macro start_c2: bool where start_c2 = (c2 = 0 /\ ct(C_c2))
%Main specifications
PROPERTY sound alarm if pressure high for 30 ticks:
start_c1 /\ (ct(C_c1) Awaits
(c1 = 0))
==> ct(C_c1) Until (c1 =
0 /\ alarm /\ start_c2)
PROPERTY sound alarm for 20 ticks:
alarm /\ start_c2 ==> (alarm
/\ ct(C_c2) Until (c2 = 20))
% Some sanity checks
PROPERTY clock c1 ticking means pressure is hi or just gone low:
ct(C_c1) ==> pressureIsHi
\/ (~ticks Since pressureGoLow)
\/ pressureGoLow
PROPERTY non-Zeno:
[]<>ticks
Return to Top
1. await<x=0>
2. <x:=i>
3. await<x=i>
4. critical section.
In the above , the use of <> indicates an atomic step. Central to the algorithm are two delays. The first, up_b, is a maximum delay between the execution of step 1 and the beginning of step 2. The second, low_c, is a minimum delay between steps 2 and 3.
Here x is the only shared variable between the processes. Our task is
to show, under what conditions, that Fischer's protocol guarantees mutual
exclusion.
A simplified view of this protocol would be as follows: A number of
processes execute step 1. As soon as any of the processes execute step
2, no other process
can pass step 1. Now, the processes that have already passed
step 1 will each set x to their internal variable i. So each will try to
execute step 3.
How can we make use of the up_b and low_c delays to guarantee that only one process can execute step 3 and enter the critical section?
1. Open StateClock and declare two constants for the entire project, up_b and low_c. Set both to a value of 2. You can do this in the constant window of the initial StateClock screen. ( see Appendix 1. of the manual) You may wish to change the value of low_c later.
2. Construct a class F for Fischer ( see Classes
in the manual) Make x a shared variable of type int, and i an out variable
of type int. Your module should look like the following:
This module represents the code of the ith process seen earlier. Event
a_b represents step 1. Event b_c represents step 2. Event c_cs represents
step 3
and state cs represents step 4. The event b_c can be taken anytime
from 0 to up_b, however event c_cs can only be taken when low_c is zero.
Therefore
up_b is the upper limit for the taking of event b_c, whereas low_c
is a minimum limit before c_cs can be taken.
3. Now construct a system ( call the project Fischer) with two modules,
f1 and f2. ( see Creating
a project and Adding
a sub module). Instantiate both f1 and
f2 from class F. ( see Classes)
Finally link the two modules with x. ( see Linking
interface variables)
4. Initialize the variable i in each module so that f1's i = 1 and
f2's i = 2. Simply click and hold the middle mouse button over the module
and select the interface.
Then hilight the f1_i variable in the actual window and select change
initial value.
5. Use the simulation tool to check that the project behaves as you
expected. Try to test the mutual exclusion property by looking for a counter
example.
( see Running
a simulation)
6. Create a specification file at the project level for two requirements:
(1) mutual exclusion of critical regions. (2) Starvation freedom, any process
requesting entrance to the critical region will eventually be granted access.
( see Creating
the specification file)
Below is an example of such a spec file:
SPEC
PROPERTY mutual exclusion: [] ( ~ ( f1_cv = 4 /\ f2_cv = 4))
PROPERTY starvation freedom: ~( f1_cv = 0 ) ==> <>( f1_cv = 0) /\ ~( f2_cv = 0 ) ==> <> ( f2_cv = 0 )
7. Create your projects fts file and submit it with the spec file to
STeP to test the requirements. ( see Generating
the FTS file )
Does the project satisfy the properties? If not, change low_c to the
least value that will satisfy the first property. Use the simulation tool
to check the counter example provided by modelchecker in STeP. ( see Connecting
to STeP ) Also how will you change your project to satisfy the second
property.
8. Once you have found the minimum value of low_c that will satisfy
the mutual exclusion property, try to understand why Fischer's protocol
has trouble with
starvation freedom. Any of the processes that happened to initially
pass through step 1, apart from the process that gained the critical region,
will be still waiting at step 3. Since the process that gained the critical
region sets x back to 0 after leaving the critical region, none of the
processes waiting at step 3 will be able to proceed.
Try to find a solution without introducing any new interface variables.
You can use new events, or local variables to solve this problem. Your
solution must deal with those processes that are left waiting at step 3.
Look for your own solution before looking at the solution provided below.
9. This solution involves the introduction of a new local variable in the class. This variable stores the value of x before the process sets x to its internal variable i. Then when a process exits the critical region it restores x to the value stored before setting x to i. Why does this solve starvation freedom? Also find a solution involving the introduction of a new event.
1. You may look at the complete example by downloading train_gate.stc.
2. The project is train_gate. It consists of three modules; cont, obs and plant.
3. As with every project the first order of business is to describe the application domain. This is described by the module plant. Below is the class TRAIN_GATE.
You can see the details of the train_position module by scrolling down the modular window. Remember that the # symbol in the event means that the event is shared. This detail is critical to understanding how the application domain behaves.
4. Next we must identify the shared phenomena. Look at the interface of plant. The variable tps indicates the position of the train. The variable tgc is used by the machine to control the gate. (see Interface)
5. Next we must describe the requirements. R1, R2 and R3 can be seen by invoking Specification at the project level. See the SPEC file below.
SPEC
% Each clock c has a corresponding
clock incremental value C_
macro ct(C_c:int) = (C_c !=
0)
% location macros
macro far_away: bool where far_away
= (plant_tp = 0)
macro approaching: bool where
approaching = (plant_tp = 1)
macro at_intersection: bool
where at_intersection = (plant_tp=2)
macro gate_down: bool where
gate_down = (plant_tg = 3)
macro gate_up: bool where gate_up
= (plant_tg = 0)
macro light_flashing:bool where
light_flashing = (plant_tl = 1)
% REQUIRMENTS
PROPERTY R1 safety1 i.e. gate
is down and light flashes when train is at the intersection:
[](at_intersection --> gate_down
/\ light_flashing)
PROPERTY R2 liveness1 i.e. the
gate is returned to up when danger is over:
(far_away /\ c = 4) ==> <>(gate_up
/\ c = 1)
PROPERTY R3 safety2 i.e. no unnecessary
delay to traffic:
far_away /\ gate_up ==> (gate_up
Awaits approaching)
PROPERTY R4 controller cannot
respond faster than one tick:
(~(tgc = (-)tgc)) ==> ( tgc
= ()tgc) Until (Event = tick)
% SANITY CHECKS
PROPERTY SC1 liveness2 i.e. clock
must tick infinitely often:
[]<>(Event = tick)
PROPERTY SC 2 safety 2 i.e. plant_tp
always equals tps:
[](plant_tp = tps)
PROPERTY SC 3 safety3 i.e. we
don't need to address clock stops:
( (c=3) ==> (ct(C_c) Until (c=0))
)
<-->
((c = 3) ==> <>(c = 0))
Try to understand the importance of each of the properties. R1 is fairly
obvious, but the R2 requires some thought.
Why do we need to have c=4 in the antecedent and c=1 in the consequent,
and not c=3 in the antecedent and c=0 in the consequent?
R3 makes sure that the gate remains up until a train approachs.
R4 prevents the controller from responding faster than one tick. Why is
this important?
(see Creating
the Specification File)
6. In order to write R2 we need the obs module. Below is the class body of this module.
Here the interface variable signal is equivalent to tps. Once the train
exits the intersection the observer starts a clock counting down from 3
to 0.
In order to properly evaluate R2 you will have to change this clock's
initial value.
7. Once the application domain and the requirements have been described,
we can proceed to design a machine that will help to achieve
requirements. The machine in this case is the module cont. as seen
below.
The controller is relatively straight forward, however look at the low
and high time bounds on the return event. Why is d set to 1?
What does this have to do with property R4?
8. Having designed the machine, you should now use the StateClock simulator
to see if the project behaves as expected. If not, make any needed changes.
Note: you can use the simulator on individual
modules as well, as you design them. (see Running
a Simulation)
9. Finally, we must check that the project train_gate satisfies the
requirements. This is done by exporting the files and running the STeP
modelchecker.
(see Connecting
to STeP)