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
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113

#![allow(dead_code, non_camel_case_types, unused_variables)]

use mpstthree::binary::struct_trait::end::End;
use mpstthree::binary_atmp::struct_trait::{recv::RecvTimed, send::SendTimed};
use mpstthree::generate_atmp;
use mpstthree::role::end::RoleEnd;
use std::collections::HashMap;
use std::error::Error;
use std::time::Instant;

generate_atmp!(MeshedChannels, A, B, C);

// Types of the payloads
struct Payload;
struct Stri;
struct Integer;
struct Test2 { payload: Integer }
struct Test5 { payload: Payload }
struct Test1;
struct Test4 { payload: Payload }
struct Test3 { payload: Stri }

// Binary sessions in depth 0
// Binary sessions for C
type Message_0_v_0_FromCToB = RecvTimed<Test1, 'a', 0, true, 2, true, ' ', Message_0_v_1_FromCToB>;
type Message_0_v_1_FromCToB = End;
type Message_0_v_0_FromCToA = End;

// Binary sessions for B
type Message_0_v_0_FromBToC = SendTimed<Test1, 'a', 0, true, 2, true, ' ', Message_0_v_1_FromBToC>;
type Message_0_v_1_FromBToC = End;
type Message_0_v_0_FromBToA = RecvTimed<Test1, 'a', 0, true, 2, true, ' ', Message_0_v_1_FromBToA>;
type Message_0_v_1_FromBToA = RecvTimed<Test1, 'a', 0, true, 2, true, ' ', Message_0_v_2_FromBToA>;
type Message_0_v_2_FromBToA = RecvTimed<Test1, 'a', 0, true, 2, true, ' ', Message_0_v_3_FromBToA>;
type Message_0_v_3_FromBToA = RecvTimed<Test5, 'a', 0, true, 2, true, ' ', Message_0_v_4_FromBToA>;
type Message_0_v_4_FromBToA = RecvTimed<Test2, 'a', 0, true, 2, true, ' ', Message_0_v_5_FromBToA>;
type Message_0_v_5_FromBToA = RecvTimed<Test3, 'a', 0, true, 2, true, ' ', Message_0_v_6_FromBToA>;
type Message_0_v_6_FromBToA = RecvTimed<Test4, 'a', 0, true, 2, true, ' ', Message_0_v_7_FromBToA>;
type Message_0_v_7_FromBToA = End;

// Binary sessions for A
type Message_0_v_0_FromAToC = End;
type Message_0_v_0_FromAToB = SendTimed<Test1, 'a', 0, true, 2, true, ' ', Message_0_v_1_FromAToB>;
type Message_0_v_1_FromAToB = SendTimed<Test1, 'a', 0, true, 2, true, ' ', Message_0_v_2_FromAToB>;
type Message_0_v_2_FromAToB = SendTimed<Test1, 'a', 0, true, 2, true, ' ', Message_0_v_3_FromAToB>;
type Message_0_v_3_FromAToB = SendTimed<Test5, 'a', 0, true, 2, true, ' ', Message_0_v_4_FromAToB>;
type Message_0_v_4_FromAToB = SendTimed<Test2, 'a', 0, true, 2, true, ' ', Message_0_v_5_FromAToB>;
type Message_0_v_5_FromAToB = SendTimed<Test3, 'a', 0, true, 2, true, ' ', Message_0_v_6_FromAToB>;
type Message_0_v_6_FromAToB = SendTimed<Test4, 'a', 0, true, 2, true, ' ', Message_0_v_7_FromAToB>;
type Message_0_v_7_FromAToB = End;

// Stacks in depth 0
// Stacks for B
type Ordering_0_v_0_ForB = RoleA<Ordering_0_v_1_ForB>;
type Ordering_0_v_1_ForB = RoleC<Ordering_0_v_2_ForB>;
type Ordering_0_v_2_ForB = RoleA<Ordering_0_v_3_ForB>;
type Ordering_0_v_3_ForB = RoleA<Ordering_0_v_4_ForB>;
type Ordering_0_v_4_ForB = RoleA<Ordering_0_v_5_ForB>;
type Ordering_0_v_5_ForB = RoleA<Ordering_0_v_6_ForB>;
type Ordering_0_v_6_ForB = RoleA<Ordering_0_v_7_ForB>;
type Ordering_0_v_7_ForB = RoleA<Ordering_0_v_8_ForB>;
type Ordering_0_v_8_ForB = RoleEnd;

// Stacks for C
type Ordering_0_v_0_ForC = RoleB<Ordering_0_v_1_ForC>;
type Ordering_0_v_1_ForC = RoleEnd;

// Stacks for A
type Ordering_0_v_0_ForA = RoleB<Ordering_0_v_1_ForA>;
type Ordering_0_v_1_ForA = RoleB<Ordering_0_v_2_ForA>;
type Ordering_0_v_2_ForA = RoleB<Ordering_0_v_3_ForA>;
type Ordering_0_v_3_ForA = RoleB<Ordering_0_v_4_ForA>;
type Ordering_0_v_4_ForA = RoleB<Ordering_0_v_5_ForA>;
type Ordering_0_v_5_ForA = RoleB<Ordering_0_v_6_ForA>;
type Ordering_0_v_6_ForA = RoleB<Ordering_0_v_7_ForA>;
type Ordering_0_v_7_ForA = RoleEnd;

// Endpoints in depth 0
// Endpoint for role A
type Endpoint_0_ForA = MeshedChannels<Message_0_v_0_FromAToB, Message_0_v_0_FromAToC, Ordering_0_v_0_ForA, NameA>;

// Endpoint for role B
type Endpoint_0_ForB = MeshedChannels<Message_0_v_0_FromBToA, Message_0_v_0_FromBToC, Ordering_0_v_0_ForB, NameB>;

// Endpoint for role C
type Endpoint_0_ForC = MeshedChannels<Message_0_v_0_FromCToA, Message_0_v_0_FromCToB, Ordering_0_v_0_ForC, NameC>;

// Fill in the functions here.
fn endpoint_a_0_v_0(s: Endpoint_0_ForA, all_clocks: &mut HashMap<char, Instant>) -> Result<(), Box<dyn Error>> {
	all_clocks.insert('a', Instant::now());

	Ok(())
}

fn endpoint_b_0_v_0(s: Endpoint_0_ForB, all_clocks: &mut HashMap<char, Instant>) -> Result<(), Box<dyn Error>> {
	all_clocks.insert('a', Instant::now());

	Ok(())
}

fn endpoint_c_0_v_0(s: Endpoint_0_ForC, all_clocks: &mut HashMap<char, Instant>) -> Result<(), Box<dyn Error>> {
	all_clocks.insert('a', Instant::now());

	Ok(())
}

fn main() {
	let (thread_a, thread_b, thread_c, ) = fork_mpst(endpoint_a_0_v_0, endpoint_b_0_v_0, endpoint_c_0_v_0, );

	println!("Thread A: {:?}", thread_a.join());
	println!("Thread B: {:?}", thread_b.join());
	println!("Thread C: {:?}", thread_c.join());
}