INRIA_Internship/Sap_Tam/channels2.spthy at master · dchandak99/INRIA_Internship · 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
theory ChannelTestTwo
begin

functions: rep/2 [private], check_rep/2, get_rep/1
equations: check_rep(rep(m,loc),loc)=m, get_rep(rep(m,loc))=m

heuristic: p /* heuristic for SAPIC */

rule Init_: // [process=top-level] Init
 [] --[Init()]-> [State_()]

rule new_c_: // [process=top-level] new c
 [State_(), Fr(c)] --[]-> [State_1(c)]

rule new_a_1 [color=#569DC0]: // [process=P] new a
 [State_1(c), Fr(a)] --[]-> [State_11(a, c)]

rule out_c_a_0_11 [color=#569DC0]: // [process=P] out c,a, 0
 [State_11(a, c), In(c)] --[ChannelInEvent(c)]-> [Out(a), State_111(a, c)]

rule out_c_a_1_11 [color=#569DC0]: // [process=P] out c,a, 1
 [State_11(a, c)] --[]-> [Semistate_11(a, c), Message(c,a)]

rule out_c_a_2_11 [color=#569DC0]: // [process=P] out c,a, 2
 [Semistate_11(a, c), Ack(c,a)] --[]-> [State_111(a, c)]

rule event_Reached_111 [color=#569DC0]: // [process=P] event Reached()
 [State_111(a, c)] --[Event(), Reached()]-> [State_1111(a, c)]

rule Zero_1111 [color=#569DC0]: // [process=P] Zero
 [State_1111(a, c)] --[]-> []


restriction single_session: // for a single session
    "All #i #j. Init()@i & Init()@j ==> #i=#j"

lemma received :
"	not( Ex #i. Reached() @ i )"

end