1


2

node Sofar( X : bool ) returns ( Sofar : bool );

3

let

4

Sofar = X > X or pre Sofar;

5

tel

6

node edge(X: bool) returns(Y: bool);

7

let

8

Y = X > X and not pre(X);

9

tel

10

node after(A: bool) returns(afterA: bool);

11

let

12

afterA = false > pre(A or afterA);

13

tel

14

node always_since(B, A: bool) returns(alwaysBsinceA: bool);

15

let

16

alwaysBsinceA = if A then B else if after(A) then

17

B and pre(alwaysBsinceA) else true;

18

tel

19

node once_since(C, A: bool) returns(onceCsinceA: bool);

20

let

21

onceCsinceA = if A then C else if after(A) then

22

C or pre(onceCsinceA) else true;

23

tel

24

node implies(A, B: bool) returns(AimpliesB: bool);

25

let

26

AimpliesB = not A or B;

27

tel

28

node always_from_to(B, A, C: bool) returns(X: bool);

29

let

30

X = implies(after(A), always_since(B, A) or once_since(C, A));

31

tel

32

node UMS(on_A, on_B, on_C, ack_AB, ack_BC: bool)

33

returns(grant_access, grant_exit, do_AB, do_BC: bool);

34

var

35

empty_section, only_on_B: bool;

36

let

37

grant_access = empty_section and ack_AB;

38

grant_exit = only_on_B and ack_BC;

39

do_AB = not ack_AB and empty_section;

40

do_BC = not ack_BC and only_on_B;

41

empty_section = not(on_A or on_B or on_C);

42

only_on_B = on_B and not(on_A or on_C);

43

tel

44

node top(on_A, on_B, on_C, ack_AB, ack_BC: bool)

45

returns(OK: bool);

46

@ contract guarantees OK;

47

var

48

grant_access, grant_exit: bool;

49

do_AB, do_BC: bool;

50

no_collision, exclusive_req: bool;

51

no_derail_AB, no_derail_BC: bool;

52

empty_section, only_on_B: bool;

53

env : bool;

54

let

55

empty_section = not(on_A or on_B or on_C);

56

only_on_B = on_B and not(on_A or on_C);

57

(grant_access, grant_exit, do_AB, do_BC) =

58

UMS(on_A, on_B, on_C, ack_AB, ack_BC);

59

env = Sofar( not(ack_AB and ack_BC) and

60

always_from_to(ack_AB, ack_AB, do_BC) and

61

always_from_to(ack_BC, ack_BC, do_AB) and

62

(empty_section > true) and

63

(true > implies(edge(not empty_section), pre grant_access)) and

64

(true > implies(edge(on_C), pre grant_exit)) and

65

implies(edge(not on_A), on_B) and

66

implies(edge(not on_B), on_A or on_C) );

67

no_collision = implies(grant_access, empty_section);

68

exclusive_req = not(do_AB and do_BC);

69

no_derail_AB = always_from_to(ack_AB, grant_access, only_on_B);

70

no_derail_BC = always_from_to(ack_BC, grant_exit, empty_section);

71

OK = env => no_collision and exclusive_req and

72

no_derail_AB and no_derail_BC;

73

%MAIN;

74

%PROPERTY OK=true;

75

tel
