-
Notifications
You must be signed in to change notification settings - Fork 3
/
ltl verifications.pml
57 lines (36 loc) · 4.56 KB
/
ltl verifications.pml
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
// If client's state is Committed, then coordinator's state can only be Committed
ltl client_Committed_Co {[] ( (Client_state == Committed) -> (Coordinator_state == Committed))}
// If client's state is Committed, then participants involved should be Prepared or Committed and eventually Committed And particpants not involved should not commit
ltl client_Committed_P0_involved {[] ( (Client_state == Committed && participants_involved[0] == 1) ->
((Participant_state[0] == Committed || Participant_state[0] == Prepared) && <> (Participant_state[0] == Committed)) )}
ltl client_Committed_P0_not_involved {[] ( (Client_state == Committed && participants_involved[0] == 0) -> (Participant_state[0] != Committed) )}
ltl client_Committed_P1_involved {[] ( (Client_state == Committed && participants_involved[1] == 1) ->
((Participant_state[1] == Committed || Participant_state[1] == Prepared) && <> (Participant_state[1] == Committed)) )}
ltl client_Committed_P1_not_involved {[] ( (Client_state == Committed && participants_involved[1] == 0) -> (Participant_state[1] != Committed) )}
ltl client_Committed_P2_involved {[] ( (Client_state == Committed && participants_involved[2] == 1) ->
((Participant_state[2] == Committed || Participant_state[2] == Prepared) && <> (Participant_state[2] == Committed)) )}
ltl client_Committed_P2_not_involved {[] ( (Client_state == Committed && participants_involved[2] == 0) -> (Participant_state[2] != Committed) )}
ltl client_Committed_P3_involved {[] ( (Client_state == Committed && participants_involved[3] == 1) ->
((Participant_state[3] == Committed || Participant_state[3] == Prepared) && <> (Participant_state[3] == Committed)) )}
ltl client_Committed_P3_not_involved {[] ( (Client_state == Committed && participants_involved[3] == 0) -> (Participant_state[3] != Committed) )}
// If client Aborted, then participants involved will abort eventually
ltl client_Aborted_P0_involved {[] ( (Client_state == Aborted && participants_involved[0] == 1) -> <> (Participant_state[0] == Aborted) )}
ltl client_Aborted_P1_involved {[] ( (Client_state == Aborted && participants_involved[1] == 1) -> <> (Participant_state[1] == Aborted) )}
ltl client_Aborted_P2_involved {[] ( (Client_state == Aborted && participants_involved[2] == 1) -> <> (Participant_state[2] == Aborted) )}
ltl client_Aborted_P3_involved {[] ( (Client_state == Aborted && participants_involved[3] == 1) -> <> (Participant_state[3] == Aborted) )}
// If participant commits, then coordinator commits and client not in Aborted (client will eventually commit)
ltl P0_committed {[] ( (Participant_state[0] == Committed) -> ( Coordinator_state == Committed && Client_state != Aborted && <> (Client_state == Committed) ) )}
ltl P1_committed {[] ( (Participant_state[1] == Committed) -> ( Coordinator_state == Committed && Client_state != Aborted && <> (Client_state == Committed) ) )}
ltl P2_committed {[] ( (Participant_state[2] == Committed) -> ( Coordinator_state == Committed && Client_state != Aborted && <> (Client_state == Committed) ) )}
ltl P3_committed {[] ( (Participant_state[3] == Committed) -> ( Coordinator_state == Committed && Client_state != Aborted && <> (Client_state == Committed) ) )}
////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
int num_p_involved = 0; //global var to denote the number of participants involved
// to verify the states when client commits
int client_committed_ver; // A global var. Client will set it to be 0 at the beginning.
/* we add 1.0 to client_committed_ver when one involved participant prepares,
add 2.0 to client_committed_ver when one involved participant commits,
add (-3)*num_p_involved to client_committed_ver when one involved participant aborts or when a participant not involved commits.
If client's state is Committed, then participants involved should be Prepared or Committed and eventually Committed.
In that way, when client's state is committed, client_committed_ver >= 1* num_p_involved and eventually client_committed_ver == 3* num_p_involved*/
ltl client_v {[]((Client_state == Committed) -> ( Coordinator_state == Committed && client_committed_ver >= num_p_involved && (<> client_committed_ver == 3* num_p_involved)))}
///////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////