1



2

 Source: Magnus Ljung

3

 This is the source to the UMS example. It is taken from HLR92.

4



5


6

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

7

let

8

Sofar = X > X and pre Sofar;

9

tel

10


11

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

12

let

13

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

14

tel

15


16

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

17

let

18

afterA = false > pre(A or afterA);

19

tel

20


21

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

22

let

23

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

24

B and pre(alwaysBsinceA) else true;

25

tel

26


27

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

28

let

29

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

30

C or pre(onceCsinceA) else true;

31

tel

32


33

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

34

let

35

AimpliesB = not A or B;

36

tel

37


38

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

39

let

40

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

41

tel

42


43

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

44

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

45

var

46

empty_section, only_on_B: bool;

47

let

48

grant_access = empty_section and ack_AB;

49

grant_exit = only_on_B and ack_BC;

50

do_AB = not ack_AB and empty_section;

51

do_BC = not ack_BC and only_on_B;

52

empty_section = not(on_A or on_B or on_C);

53

only_on_B = on_B and not(on_A or on_C);

54

tel

55


56

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

57

returns(OK: bool);

58

@ contract guarantees OK;

59

var

60

grant_access, grant_exit: bool;

61

do_AB, do_BC: bool;

62

no_collision, exclusive_req: bool;

63

no_derail_AB, no_derail_BC: bool;

64

empty_section, only_on_B: bool;

65

env : bool;

66

let

67

empty_section = not(on_A or on_B or on_C);

68

only_on_B = on_B and not(on_A or on_C);

69


70

 UMS CALL

71

(grant_access, grant_exit, do_AB, do_BC) =

72

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

73


74

env = Sofar( not(ack_AB and ack_BC) and

75

always_from_to(ack_AB, ack_AB, do_BC) and

76

always_from_to(ack_BC, ack_BC, do_AB) and

77

(empty_section > true) and

78

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

79

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

80

implies(edge(not on_A), on_B) and

81

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

82


83

 PROPERTIES

84

no_collision = implies(grant_access, empty_section);

85

exclusive_req = not(do_AB and do_BC);

86

no_derail_AB = always_from_to(ack_AB, grant_access, only_on_B);

87

no_derail_BC = always_from_to(ack_BC, grant_exit, empty_section);

88


89

OK = env => no_collision and exclusive_req and

90

no_derail_AB and no_derail_BC;

91

%PROPERTY OK=true;

92

%MAIN;

93

tel
