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

use mpstthree::binary::struct_trait::{end::End, recv::Recv, send::Send};
use mpstthree::generate;
use mpstthree::role::end::RoleEnd;
use std::error::Error;

generate!(
    "rec_and_cancel",
    MeshedChannels,
    Constellation,
    Layout,
    Script
);

// Payload types

struct GetCurrentState;
struct DocumentLoading;
struct WebFontLoaded;
struct GetWebPageLoadState;
struct OutstandingWebFonts;

// Binary types

type CtoL = Send<GetWebPageLoadState, Recv<OutstandingWebFonts, End>>;
type CtoS = Send<GetCurrentState, Recv<DocumentLoading, End>>;

type LtoC = Recv<GetWebPageLoadState, Send<OutstandingWebFonts, End>>;
type LtoS = Send<WebFontLoaded, End>;

type StoC = Recv<GetCurrentState, Send<DocumentLoading, End>>;
type StoL = Recv<WebFontLoaded, End>;

// Orderings

type OrderingC = RoleScript<RoleScript<RoleLayout<RoleLayout<RoleEnd>>>>;

type OrderingL = RoleScript<RoleConstellation<RoleConstellation<RoleEnd>>>;

type OrderingS = RoleConstellation<RoleConstellation<RoleLayout<RoleEnd>>>;

// MeshedChannels

type EndpointC = MeshedChannels<CtoL, CtoS, OrderingC, NameConstellation>;

type EndpointL = MeshedChannels<LtoC, LtoS, OrderingL, NameLayout>;

type EndpointS = MeshedChannels<StoC, StoL, OrderingS, NameScript>;

/////////////////////////

fn endpoint_c(s: EndpointC) -> Result<(), Box<dyn Error>> {
    let s = s.send(GetCurrentState {})?;
    let (_, s) = s.recv()?;
    let s = s.send(GetWebPageLoadState {})?;
    let (_, s) = s.recv()?;
    s.close()
}

/////////////////////////

fn endpoint_l(s: EndpointL) -> Result<(), Box<dyn Error>> {
    let s = s.send(WebFontLoaded {})?;
    let (_, s) = s.recv()?;
    let s = s.send(OutstandingWebFonts {})?;
    s.close()
}

/////////////////////////

fn endpoint_s(s: EndpointS) -> Result<(), Box<dyn Error>> {
    let (_, s) = s.recv()?;
    let s = s.send(DocumentLoading {})?;
    let (_, s) = s.recv()?;
    s.close()
}

/////////////////////////

fn main() {
    checking();

    let (thread_c, thread_l, thread_s) = fork_mpst(endpoint_c, endpoint_l, endpoint_s);

    thread_c.join().unwrap();
    thread_l.join().unwrap();
    thread_s.join().unwrap();
}

/////////////////////////

// Check for bottom-up approach
fn checking() {
    let (_graphs, _kmc) =
        mpstthree::checker_concat!("servo_8257_original", EndpointC, EndpointL, EndpointS).unwrap();

    // println!(
    //     "graph C: {:?}",
    //     petgraph::dot::Dot::new(&graphs["RoleConstellation"])
    // );
    // println!("\n/////////////////////////\n");
    // println!(
    //     "graph L: {:?}",
    //     petgraph::dot::Dot::new(&graphs["RoleLayout"])
    // );
    // println!("\n/////////////////////////\n");
    // println!(
    //     "graph S: {:?}",
    //     petgraph::dot::Dot::new(&graphs["RoleScript"])
    // );
    // println!("\n/////////////////////////\n");
    // println!("min kMC: {kmc:?}");
}