safe_drive 0.4.3

safe_drive: Formally Specified Rust Bindings for ROS2
Documentation 
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
105

---- MODULE init_once ----
EXTENDS TLC, FiniteSets, Integers

CONSTANTS Processes

(* --algorithm init_once
variables
    lock = FALSE;
    is_init = FALSE;

    pids = {};

define
    just_once == <>[](Cardinality(pids) = 1) /\ [](Cardinality(pids) <= 1)
end define

\* initializer
fair+ process pid \in Processes
begin
    BeginInitOnce:
        while ~is_init do
            LoadLockRelaxed:
                if ~lock then
                    CompareExchange:
                        if ~lock then
                            lock := TRUE;
                            pids := pids \union {self};

                            Initialize:
                                skip;

                            StoreIsInit:
                                is_init := TRUE;
                        end if;
                end if;
        end while;
end process;

end algorithm; *)
\* BEGIN TRANSLATION (chksum(pcal) = "171ee2b4" /\ chksum(tla) = "1cd14bb5")
VARIABLES lock, is_init, pids, pc

(* define statement *)
just_once == <>[](Cardinality(pids) = 1) /\ [](Cardinality(pids) <= 1)


vars == << lock, is_init, pids, pc >>

ProcSet == (Processes)

Init == (* Global variables *)
        /\ lock = FALSE
        /\ is_init = FALSE
        /\ pids = {}
        /\ pc = [self \in ProcSet |-> "BeginInitOnce"]

BeginInitOnce(self) == /\ pc[self] = "BeginInitOnce"
                       /\ IF ~is_init
                             THEN /\ pc' = [pc EXCEPT ![self] = "LoadLockRelaxed"]
                             ELSE /\ pc' = [pc EXCEPT ![self] = "Done"]
                       /\ UNCHANGED << lock, is_init, pids >>

LoadLockRelaxed(self) == /\ pc[self] = "LoadLockRelaxed"
                         /\ IF ~lock
                               THEN /\ pc' = [pc EXCEPT ![self] = "CompareExchange"]
                               ELSE /\ pc' = [pc EXCEPT ![self] = "BeginInitOnce"]
                         /\ UNCHANGED << lock, is_init, pids >>

CompareExchange(self) == /\ pc[self] = "CompareExchange"
                         /\ IF ~lock
                               THEN /\ lock' = TRUE
                                    /\ pids' = (pids \union {self})
                                    /\ pc' = [pc EXCEPT ![self] = "Initialize"]
                               ELSE /\ pc' = [pc EXCEPT ![self] = "BeginInitOnce"]
                                    /\ UNCHANGED << lock, pids >>
                         /\ UNCHANGED is_init

Initialize(self) == /\ pc[self] = "Initialize"
                    /\ TRUE
                    /\ pc' = [pc EXCEPT ![self] = "StoreIsInit"]
                    /\ UNCHANGED << lock, is_init, pids >>

StoreIsInit(self) == /\ pc[self] = "StoreIsInit"
                     /\ is_init' = TRUE
                     /\ pc' = [pc EXCEPT ![self] = "BeginInitOnce"]
                     /\ UNCHANGED << lock, pids >>

pid(self) == BeginInitOnce(self) \/ LoadLockRelaxed(self)
                \/ CompareExchange(self) \/ Initialize(self)
                \/ StoreIsInit(self)

(* Allow infinite stuttering to prevent deadlock on termination. *)
Terminating == /\ \A self \in ProcSet: pc[self] = "Done"
               /\ UNCHANGED vars

Next == (\E self \in Processes: pid(self))
           \/ Terminating

Spec == /\ Init /\ [][Next]_vars
        /\ \A self \in Processes : SF_vars(pid(self))

Termination == <>(\A self \in ProcSet: pc[self] = "Done")

\* END TRANSLATION
====