mpstthree 0.1.17

A library implementing Multiparty Session Types for 2 or more participants
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

global protocol HTTP(role Client, role Proxy1, role Proxy2, role Server)
{
    OpenTCPConnection() from Client to Proxy1;
    OpenTCPConnection() from Proxy1 to Proxy2;
    OpenTCPConnection() from Proxy2 to Server;

    choice at Server
    {
        Fail() from Server to Proxy2;
        Fail() from Proxy2 to Proxy1;
        Fail() from Proxy1 to Client;
    } or {
        Success() from Server to Proxy2;
        Success() from Proxy2 to Proxy1;
        Success() from Proxy1 to Client;

        rec Loop {
            choice at Client
            {
                RequestGet() from Client to Proxy1;
                RequestGet() from Proxy1 to Proxy2;
                RequestGet() from Proxy2 to Server;

                choice at Server
                {
                    Response200() from Server to Proxy2;
                    Response200() from Proxy2 to Proxy1;
                    Response200() from Proxy1 to Client;
                    continue Loop;
                } or {
                    Response404() from Server to Proxy2;
                    Response404() from Proxy2 to Proxy1;
                    Response404() from Proxy1 to Client;
                    continue Loop;
                } or {
                    Response418() from Server to Proxy2;
                    Response418() from Proxy2 to Proxy1;
                    Response418() from Proxy1 to Client;
                    continue Loop;
                }
            } or {
                RequestPut() from Client to Proxy1;
                RequestPut() from Proxy1 to Proxy2;
                RequestPut() from Proxy2 to Server;

                choice at Server
                {
                    Response200() from Server to Proxy2;
                    Response200() from Proxy2 to Proxy1;
                    Response200() from Proxy1 to Client;
                    continue Loop;
                } or {
                    Response404() from Server to Proxy2;
                    Response404() from Proxy2 to Proxy1;
                    Response404() from Proxy1 to Client;
                    continue Loop;
                } or {
                    Response418() from Server to Proxy2;
                    Response418() from Proxy2 to Proxy1;
                    Response418() from Proxy1 to Client;
                    continue Loop;
                }
            } or {
                RequestPost() from Client to Proxy1;
                RequestPost() from Proxy1 to Proxy2;
                RequestPost() from Proxy2 to Server;

                choice at Server
                {
                    Response200() from Server to Proxy2;
                    Response200() from Proxy2 to Proxy1;
                    Response200() from Proxy1 to Client;
                    continue Loop;
                } or {
                    Response404() from Server to Proxy2;
                    Response404() from Proxy2 to Proxy1;
                    Response404() from Proxy1 to Client;
                    continue Loop;
                } or {
                    Response418() from Server to Proxy2;
                    Response418() from Proxy2 to Proxy1;
                    Response418() from Proxy1 to Client;
                    continue Loop;
                }
            } or {
                Close() from Client to Proxy1;
                Close() from Proxy1 to Proxy2;
                Close() from Proxy2 to Server;
            }
        }
    }
}