Graded-CTL NuSMV

Source Code for "Robot"

--
-- A robotics controller described in [1].
--
-- Sergio Campos -- 06/94
--

-- period: 40ms exec: 1ms at pri10, 5ms at pri7
MODULE T1(timeout, processor_granted, request)
VAR
state: 0..7;
DEFINE
start := state = 0 & timeout;
finish := state = 6;
request := case
state = 0: 0;
state = 1: 10;
state in 2..6: 7;
state = 7: 7;
esac;
ASSIGN
init(state) := 0;
next(state) := case
start: 1;
finish: 0;
processor_granted != p1: state;
state = 0: 0;
1: state + 1 mod 7;
esac;

-- period: 100ms exec: 10ms at pri4, 5ms at pri8, 5 at pri4
MODULE T2(timeout, processor_granted, request, finish)
VAR
state: 0..20;
DEFINE
start := state = 0 & timeout;
finish := state = 20;
request := case
state = 0: 0;
state in 1..10: 4;
state in 11..15: 8;
state in 16..20: 4;
esac;
ASSIGN
init(state) := 0;
next(state) := case
start: 1;
finish: 0;
processor_granted != p2: state;
state = 0: 0;
1: state + 1 mod 21;
esac;

-- period: 50ms exec: 8ms at pri5, 12ms at pri8
-- T3 receives two timeouts. One is from T2.finish, and the other is
-- from timeout100offset. T3 executes after T2 finishes and uses data
-- generated by T2. It also executes 50ms later and tries to use old data.
-- In this case it may decide not to execute.
MODULE T3(T2finishes, timeout, processor_granted, request)
VAR
state: 0..20;
timeoutlatch: boolean;
activation_count: 0..3;
DEFINE
start := state = 0 & (T2finishes | timeout) |
(finish & activation_count >= 1) |
((T2finishes | timeout) & finish);
finish := state = 20;
request := case
state = 0: 0;
state in 1..8: 5;
state in 9..20: 8;
esac;
ASSIGN
init(state) := 0;
next(state) := case
start & T2finishes: 1; -- runs after T2 finishes.
start & timeout: 1; --{0, 1};
-- In this case T3 does not run after T2.
-- May decide not to execute if it thinks
-- that not enough data has be generated
-- by previous activations of T2.
finish: 0;
processor_granted != p3: state;
state = 0: 0;
1: state + 1 mod 21;
esac;
init(timeoutlatch) := timeout;
next(timeoutlatch) := case
start: timeout;
1: timeoutlatch;
esac;
init(activation_count) := 0;
next(activation_count) := case
state = 0: 0;
(timeout | T2finishes) & finish: activation_count;
timeout | T2finishes: activation_count + 1 mod 4;
finish & activation_count > 0: activation_count - 1;
1: activation_count;
esac;

-- period: 200ms exec: 10ms at pri9, 20ms at pri2, 3 at pri3
MODULE T4(timeout, processor_granted, request, finish)
VAR
state: 0..33;
DEFINE
start := state = 0 & timeout;
finish := state = 33;
request := case
state = 0: 0;
state in 1..10: 9;
state in 11..30: 2;
state in 31..33: 3;
esac;
ASSIGN
init(state) := 0;
next(state) := case
start: 1;
finish: 0;
processor_granted != p4: state;
state = 0: 0;
1: state + 1 mod 34;
esac;

-- period: 400ms exec: 2ms at pri3, 12ms at pri1, 10 at pri6
MODULE T5(timeout, processor_granted, request)
VAR
state: 0..24;
data_count: boolean;
DEFINE
start := state = 0 & timeout;
finish := state = 24;
request := case
state = 0: 0;
state in 1..2: 3;
state in 3..14: 1;
state in 15..24: 6;
esac;
ASSIGN
init(state) := 0;
next(state) := case
start & data_count: 1;
finish: 0;
processor_granted != p5: state;
state = 0: 0;
1: state + 1 mod 34;
esac;
init(data_count) := 0;
next(data_count) := case
start: data_count + 1 mod 2;
1: data_count;
esac;

MODULE main
VAR
timer: 0..400;
ASSIGN
init(timer) := 0;
next(timer) := timer + 1 mod 400;
DEFINE
timeout400 := timer mod 400 = 0;
timeout200 := timer mod 200 = 0;
timeout100 := timer mod 100 = 0;
timeout100offset := timer mod 100 = 50;
timeout50 := timer mod 50 = 0;
timeout40 := timer mod 40 = 0;
VAR
pT1: T1(timeout40, processor_granted, req1);
pT2: T2(timeout100, processor_granted, req2, T2finish);
-- Two signals are sent to T3. One executes after T2 and uses data
-- generated by it. The other one executes 50ms after T2 starts, and
-- tries to use data generated by other activations of T2. It may
-- decide not to run, however.
pT3: T3(T2finish, 0, processor_granted, req3);
pT4: T4(timeout200, processor_granted, req4, T4finish);
pT5: T5(T4finish, processor_granted, req5);
aux: {idle, p1, p2, p3, p4, p5};
last24: boolean;

--
-- Scheduler code: Chooses maximum priority request and assigns grant to it.
--
DEFINE
max_r1r2 := case
req1 > req2: req1;
1: req2;
esac;
max_r3r4 := case
req3 > req4: req3;
1: req4;
esac;
max_r1_to_r4 := case
max_r1r2 > max_r3r4: max_r1r2;
1: max_r3r4;
esac;
max_r1_to_r5 := case
max_r1_to_r4 > req5: max_r1_to_r4;
1: req5;
esac;

-- conflicts between T2-T3 and T4-T5
VAR
processor_granted: {idle, p1, p2, p3, p4, p5};
ASSIGN
processor_granted := case
max_r1_to_r5 = 0: idle;
max_r1_to_r5 = req2 & max_r1_to_r5 = req3: case
last24: p3;
1: p2;
esac;
max_r1_to_r5 = req4 & max_r1_to_r5 = req5: case
last24: p5;
1: p4;
esac;
max_r1_to_r5 = req1: p1;
max_r1_to_r5 = req2: p2;
max_r1_to_r5 = req3: p3;
max_r1_to_r5 = req4: p4;
max_r1_to_r5 = req5: p5;
1: idle;
esac;
ASSIGN
init(last24) := 0;
next(last24) := case
processor_granted = p2: 1;
processor_granted = p3: 0;
processor_granted = p4: 1;
processor_granted = p5: 0;
1: last24;
esac;
-- property true, there is no overlapping of different activations of the
-- same task.
DEFINE
error := (timeout40 & pT1.state != 0) | (timeout100 & pT2.state != 0) |
(timeout50 & pT3.state != 0) | (timeout200 & pT4.state != 0) |
(timeout400 & pT5.state != 0);