Model-Checking/railgate.tla at master · Amithabh-A/Model-Checking · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
------------------------------ MODULE railgate ------------------------------


EXTENDS Integers

VARIABLES gate, train, controller

TypeOK == /\ gate \in {"up", "down"}
          /\ train \in {"far", "near", "in"}
          /\ controller \in 0..3


Init == /\ gate = "up" \* gate is in up state
        /\ train = "far" \* Train in far state
        /\ controller = 0 \* controller in 0 state


LowerGate == /\ gate = "up"
             /\ gate' = "down"

RaiseGate == /\ gate = "down"
             /\ gate' = "up"

ApproachTrain == /\ train = "far"
                 /\ train' = "near"

\*EnterTrain == /\ train = "near"
\*              /\ train' = "in"

EnterTrain == IF train = "near"
              THEN train' = "in"
              ELSE UNCHANGED<<train>>

\*ExitTrain == /\ train = "in"
\*             /\ train' = "far"

ExitTrain == IF train = "in"
              THEN train' = "far"
              ELSE UNCHANGED<<train>>


\*ControllerApproach == /\ controller = 0
\*                     /\ controller' = 1

ControllerApproach == IF controller = 0
                      THEN controller' = 1
                      ELSE UNCHANGED<<controller>>

\*ControllerLower == /\ controller = 1
\*                  /\ controller' = 2

ControllerLower == IF controller = 1
                  THEN controller' = 2
                  ELSE UNCHANGED<<controller>>

\*ControllerExit == /\ controller = 2
\*                 /\ controller' = 3

ControllerExit == IF controller = 2
                  THEN controller' = 3
                  ELSE UNCHANGED<<controller>>

\*ControllerRaise == /\ controller = 3
\*                  /\ controller' = 0

ControllerRaise == IF controller = 3
                   THEN controller' = 0
                   ELSE UNCHANGED<<controller>>

Approach ==  /\ ControllerApproach
             /\ ApproachTrain
             /\ UNCHANGED<<gate>>

Lower == /\ LowerGate
         /\ ControllerLower
         /\ UNCHANGED<<train>>

Exit == /\ ExitTrain
        /\ ControllerExit
        /\ UNCHANGED<<gate>>

Raise == /\ RaiseGate
         /\ ControllerRaise
         /\ UNCHANGED<<train>>

Enter == /\ EnterTrain
         /\ UNCHANGED<<gate, controller>>


Next == \/ Approach
        \/ Lower
        \/ Exit
        \/ Raise
        \/ Enter

SafetyCheck == ~(train = "in" /\ gate = "up")

Reachable == ~(train = "far"/\ controller = 2 /\ gate = "up")


=============================================================================
\* Modification History
\* Last modified Tue Feb 20 19:07:27 IST 2024 by amithabh_a
\* Created Tue Feb 20 17:23:09 IST 2024 by amithabh_a