The learning outcomes that are assessed by this coursework are:

1 Reason with a document written in a formal specification language

2 Use a formal notation to develop, analyse and critically review a (small-scale) system specification

3 Animate a specification using an appropriate practical tool and discuss the results

Exercise - Assessment Indicators:
- Clear English
- Correctness
- Conciseness
Give an English description of the interval that corresponds to each of the following Tempura formulae
a)
define test1() = {
exists I : {
len (7) and I = -2 and
chopstar (skip and I := I + 4) and always output (I)

}
}:

b)

define test2() = {
exists A; I; S : {
list (A; 6) and stable (struct (A)) and A = [2; 1; 4; 3; 6; 5] and stable (A) and I = 3 and I gets (I + 1) mod |A| and

always {output I} and len (|A|) and fin output S and
S = 1 and S gets S ∗ A[I]
}
}:

Exercise 2 Assessment Indicators:
- Correctness
- Elegance (clarity and conciseness)
Give for each of the following intervals the corresponding Tempura formula. Provide output from your formula to evidence its correctness.
a) - - - -
A = 0 A = 1 A = 1 A = 0
B = 1 B = 1 B = 0 B = 0
C = 1 C = 0 C = 1 C = 0

b) The Lucas numbers are similar to Fibonacci numbers, each Lucas number is defined to be the sum of its two immediate previous terms.
However, the first two Lucas numbers are lucas(0) = 2 and lucas(1) = 1 instead of 0 and 1. Give a Tempura specification that generates the first 8 Lucas numbers, i.e., generates the following interval:
- - - - - - - -
L = 2 L = 1 L = 3 L = 4 L = 7 L = 11 L = 18 L = 29
(7 marks)
c) Give a Tempura specification that generates the first n Lucas numbers squared. The specification should ask the user to input n (n > 0) in the first state.
- - : : : -
D = luc (0) ∗ luc (0) D = luc (1) ∗ luc (1) : : : D = luc (n) ∗ luc (n)
where luc (n) denotes the nth Lucas number.

Exercise 3. Assessment Indicators:

Ability to translate informal textual system description into formal description.

- Ability to justify system design decisions.
- Ability to analyse a formal system specification.
The following is an informal description for a traffic-light controller:

1. There are two sets of lights: one is positioned over the main road (MAIN) entering the cross-junction, and the other is over the secondary road (SEC).
2. During the daytime the controller operates according to one of two possible programs (option externally determined):

Program A gives two minutes for the vehicles on MAIN, and half a minute for the vehicles on SEC, alternating.
Program B gives half a minute for the vehicles in SEC once a signal SEC_FULL goes on (the SEC_FULL signal coming from an external sensor).

3. During the night the controller gives precedence to the cars in MAIN
until one of the following two possibilities occurs:

Two minutes have passed since MAIN became green and a new car appears on SEC;
- Three cars have appeared on SEC.
When one of these conditions occurs, vehicles on SEC are given half a minute.

4. Any transition from day to night and vice-versa, must start with 5 seconds of flashing amber lights after which the MAIN receives the green light.

First identify the external input events and conditions. The outputs of the controller are the Boolean signals:
MRED, MAMB, MGRN SRED, SAMB, SGRN
(MRED means: the RED light for the MAIN road).

a) Give a Tempura specification of the traffic-light controller. Log decisions on how you resolve any ambiguity.
Use the following scenarios to illustrate your answer with output from your program:
i) A behaviour of the controller in which program A is used during daytime (only the daytime portion of the behaviour should be given).
ii) A behaviour of the controller in which program B is used during daytime (only the daytime portion of the behaviour should be given).
iii) A behaviour of the controller in which the controller switches from daytime mode to nighttime mode (only the portion of the behaviour where the switch occurs should be given).

The following marking scheme will be used

b) The system that you have specified needs to satisfy certain safety conditions. Note, a safety condition specifies that something bad will never happen.

Give two examples of safety conditions that your system should satisfy and formulate them in ITL/Tempura.