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

timed global protocol HTTP(role Client, role Proxy1, role Proxy2, role Server)
{
    OpenTCPConnection() from Client to Proxy1 within [0;1] using a and resetting ();
    OpenTCPConnection() from Proxy1 to Proxy2 within [0;1] using a and resetting ();
    OpenTCPConnection() from Proxy2 to Server within [0;1] using a and resetting ();

    choice at Server
    {
        Fail() from Server to Proxy2 within [0;1] using a and resetting ();
        Fail() from Proxy2 to Proxy1 within [0;1] using a and resetting ();
        Fail() from Proxy1 to Client within [0;1] using a and resetting ();
    } or {
        Success() from Server to Proxy2 within [0;1] using a and resetting ();
        Success() from Proxy2 to Proxy1 within [0;1] using a and resetting ();
        Success() from Proxy1 to Client within [0;1] using a and resetting ();

        rec Loop {
            choice at Client
            {
                RequestGet() from Client to Proxy1 within [0;1] using a and resetting ();
                RequestGet() from Proxy1 to Proxy2 within [0;1] using a and resetting ();
                RequestGet() from Proxy2 to Server within [0;1] using a and resetting ();

                choice at Server
                {
                    Response200() from Server to Proxy2 within [0;1] using a and resetting ();
                    Response200() from Proxy2 to Proxy1 within [0;1] using a and resetting ();
                    Response200() from Proxy1 to Client within [0;1] using a and resetting ();
                    continue Loop within [0;1] using a and resetting ();
                } or {
                    Response404() from Server to Proxy2 within [0;1] using a and resetting ();
                    Response404() from Proxy2 to Proxy1 within [0;1] using a and resetting ();
                    Response404() from Proxy1 to Client within [0;1] using a and resetting ();
                    continue Loop within [0;1] using a and resetting ();
                } or {
                    Response418() from Server to Proxy2 within [0;1] using a and resetting ();
                    Response418() from Proxy2 to Proxy1 within [0;1] using a and resetting ();
                    Response418() from Proxy1 to Client within [0;1] using a and resetting ();
                    continue Loop within [0;1] using a and resetting ();
                }
            } or {
                RequestPut() from Client to Proxy1 within [0;1] using a and resetting ();
                RequestPut() from Proxy1 to Proxy2 within [0;1] using a and resetting ();
                RequestPut() from Proxy2 to Server within [0;1] using a and resetting ();

                choice at Server
                {
                    Response200() from Server to Proxy2 within [0;1] using a and resetting ();
                    Response200() from Proxy2 to Proxy1 within [0;1] using a and resetting ();
                    Response200() from Proxy1 to Client within [0;1] using a and resetting ();
                    continue Loop within [0;1] using a and resetting ();
                } or {
                    Response404() from Server to Proxy2 within [0;1] using a and resetting ();
                    Response404() from Proxy2 to Proxy1 within [0;1] using a and resetting ();
                    Response404() from Proxy1 to Client within [0;1] using a and resetting ();
                    continue Loop within [0;1] using a and resetting ();
                } or {
                    Response418() from Server to Proxy2 within [0;1] using a and resetting ();
                    Response418() from Proxy2 to Proxy1 within [0;1] using a and resetting ();
                    Response418() from Proxy1 to Client within [0;1] using a and resetting ();
                    continue Loop within [0;1] using a and resetting ();
                }
            } or {
                RequestPost() from Client to Proxy1 within [0;1] using a and resetting ();
                RequestPost() from Proxy1 to Proxy2 within [0;1] using a and resetting ();
                RequestPost() from Proxy2 to Server within [0;1] using a and resetting ();

                choice at Server
                {
                    Response200() from Server to Proxy2 within [0;1] using a and resetting ();
                    Response200() from Proxy2 to Proxy1 within [0;1] using a and resetting ();
                    Response200() from Proxy1 to Client within [0;1] using a and resetting ();
                    continue Loop within [0;1] using a and resetting ();
                } or {
                    Response404() from Server to Proxy2 within [0;1] using a and resetting ();
                    Response404() from Proxy2 to Proxy1 within [0;1] using a and resetting ();
                    Response404() from Proxy1 to Client within [0;1] using a and resetting ();
                    continue Loop within [0;1] using a and resetting ();
                } or {
                    Response418() from Server to Proxy2 within [0;1] using a and resetting ();
                    Response418() from Proxy2 to Proxy1 within [0;1] using a and resetting ();
                    Response418() from Proxy1 to Client within [0;1] using a and resetting ();
                    continue Loop within [0;1] using a and resetting ();
                }
            } or {
                Close() from Client to Proxy1 within [0;1] using a and resetting ();
                Close() from Proxy1 to Proxy2 within [0;1] using a and resetting ();
                Close() from Proxy2 to Server within [0;1] using a and resetting ();
            }
        }
    }
}