use rand::{thread_rng, Rng};
use mpstthree::binary::struct_trait::{end::End, recv::Recv, send::Send, session::Session};
use mpstthree::functionmpst::fork::fork_mpst;
use mpstthree::meshedchannels::MeshedChannels;
use mpstthree::role::broadcast::RoleBroadcast;
use mpstthree::{checker_concat, checker_concat_impl};
use std::error::Error;
use mpstthree::role::a::RoleA;
use mpstthree::role::b::RoleB;
use mpstthree::role::c::RoleC;
use mpstthree::role::end::RoleEnd;
use mpstthree::name::a::NameA;
use mpstthree::name::b::NameB;
use mpstthree::name::c::NameC;
use mpstthree::choose_mpst_b_to_all;
use mpstthree::offer_mpst_a_to_b;
use mpstthree::offer_mpst_c_to_b;
use petgraph::dot::Dot;
type CtoBClose = End;
type CtoAClose = End;
type CtoAVideo = Send<i32, Recv<i32, End>>;
type CtoBVideo = Recv<i32, Send<i32, RecursCtoB>>;
type InitC = Recv<i32, Send<i32, RecursCtoB>>;
type AtoCClose = <CtoAClose as Session>::Dual;
type AtoBClose = End;
type AtoCVideo = <CtoAVideo as Session>::Dual;
type RecursCtoB = Recv<Branches0CtoB, End>;
type RecursAtoB = Recv<Branches0AtoB, End>;
enum Branches0CtoB {
End(MeshedChannels<CtoAClose, CtoBClose, StackCEnd, NameC>),
Video(MeshedChannels<CtoAVideo, CtoBVideo, StackCVideo, NameC>),
}
enum Branches0AtoB {
End(MeshedChannels<AtoBClose, AtoCClose, StackAEnd, NameA>),
Video(MeshedChannels<RecursAtoB, AtoCVideo, StackAVideo, NameA>),
}
type Choose0fromBtoC = Send<Branches0CtoB, End>;
type Choose0fromBtoA = Send<Branches0AtoB, End>;
type InitB = Send<i32, Recv<i32, Choose0fromBtoC>>;
type StackCEnd = RoleEnd;
type StackCVideo = RoleB<RoleA<RoleA<RoleB<RoleB<RoleEnd>>>>>;
type StackCRecurs = RoleB<RoleEnd>;
type StackCInit = RoleB<RoleB<RoleB<RoleEnd>>>;
type StackAEnd = RoleEnd;
type StackAVideo = RoleC<RoleC<RoleB<RoleEnd>>>;
type StackARecurs = RoleB<RoleEnd>;
type StackBRecurs = RoleBroadcast;
type StackBFull = RoleC<RoleC<StackBRecurs>>;
type EndpointBEnd = MeshedChannels<End, End, RoleEnd, NameB>;
type EndpointBVideo = MeshedChannels<
Send<Branches0AtoB, End>,
Send<i32, Recv<i32, Send<Branches0CtoB, End>>>,
RoleC<RoleC<RoleBroadcast>>,
NameB,
>;
type EndpointBRecurs = MeshedChannels<Choose0fromBtoA, Choose0fromBtoC, StackBRecurs, NameB>;
type EndpointBFull = MeshedChannels<Choose0fromBtoA, InitB, StackBFull, NameB>;
type EndpointCRecurs = MeshedChannels<End, RecursCtoB, StackCRecurs, NameC>;
type EndpointCFull = MeshedChannels<End, InitC, StackCInit, NameC>;
type EndpointAFull = MeshedChannels<RecursAtoB, End, StackARecurs, NameA>;
fn server(s: EndpointAFull) -> Result<(), Box<dyn Error>> {
offer_mpst_a_to_b!(s, {
Branches0AtoB::End(s) => {
s.close()
},
Branches0AtoB::Video(s) => {
let (request, s) = s.recv()?;
let s = s.send(request + 1);
server(s)
},
})
}
fn authenticator(s: EndpointCFull) -> Result<(), Box<dyn Error>> {
let (id, s) = s.recv()?;
let s = s.send(id + 1);
authenticator_recurs(s)
}
fn authenticator_recurs(s: EndpointCRecurs) -> Result<(), Box<dyn Error>> {
offer_mpst_c_to_b!(s, {
Branches0CtoB::End(s) => {
s.close()
},
Branches0CtoB::Video(s) => {
let (request, s) = s.recv()?;
let (video, s) = s.send(request + 1).recv()?;
let s = s.send(video + 1);
authenticator_recurs(s)
},
})
}
fn client(s: EndpointBFull) -> Result<(), Box<dyn Error>> {
let xs: Vec<i32> = (1..100).map(|_| thread_rng().gen()).collect();
let (_, s) = s.send(0).recv()?;
client_recurs(s, xs, 1)
}
fn client_recurs(s: EndpointBRecurs, mut xs: Vec<i32>, index: i32) -> Result<(), Box<dyn Error>> {
match xs.pop() {
Option::Some(_) => {
let s: EndpointBFull =
choose_mpst_b_to_all!(s, Branches0AtoB::Video, Branches0CtoB::Video);
let (_, s) = s.send(1).recv()?;
client_recurs(s, xs, index + 1)
}
Option::None => {
let s = choose_mpst_b_to_all!(s, Branches0AtoB::End, Branches0CtoB::End);
assert_eq!(index, 100);
s.close()
}
}
}
pub fn run_b_usecase_recursive() {
let (thread_a, thread_b, thread_c) = fork_mpst(server, client, authenticator);
assert!(thread_a.join().is_ok());
assert!(thread_b.join().is_ok());
assert!(thread_c.join().is_ok());
}
checker_concat_impl!(
[Branches0CtoB, Video, Branches0AtoB, Video],
[Branches0CtoB, End, Branches0AtoB, End]
);
pub fn run_b_usecase_recursive_checker() {
let (graphs, kmc) = checker_concat!(
"",
EndpointAFull,
EndpointCFull,
EndpointBFull
=>
[
EndpointBVideo,
Branches0CtoB, Video,
Branches0AtoB, Video
],
[
EndpointBEnd,
Branches0CtoB, End,
Branches0AtoB, End
]
)
.unwrap();
let graph_a = &graphs["RoleA"];
assert_eq!(
format!("{:?}", Dot::new(&graph_a)),
"digraph {\n \
0 [ label = \"\\\"0\\\"\" ]\n \
1 [ label = \"\\\"0.1\\\"\" ]\n \
2 [ label = \"\\\"0.1\\\"\" ]\n \
3 [ label = \"\\\"0.2\\\"\" ]\n \
0 -> 1 [ label = \"\\\"0\\\"\" ]\n \
0 -> 2 [ label = \"\\\"RoleA?RoleC: i32\\\"\" ]\n \
2 -> 3 [ label = \"\\\"RoleA!RoleC: i32\\\"\" ]\n \
3 -> 0 [ label = \"\\\"µ\\\"\" ]\n\
}\n"
);
let graph_b = &graphs["RoleB"];
assert_eq!(
format!("{:?}", Dot::new(&graph_b)),
"digraph {\n \
0 [ label = \"\\\"0\\\"\" ]\n \
1 [ label = \"\\\"1\\\"\" ]\n \
2 [ label = \"\\\"2\\\"\" ]\n \
3 [ label = \"\\\"2.1\\\"\" ]\n \
4 [ label = \"\\\"2.1\\\"\" ]\n \
5 [ label = \"\\\"2.2\\\"\" ]\n \
0 -> 1 [ label = \"\\\"RoleB!RoleC: i32\\\"\" ]\n \
1 -> 2 [ label = \"\\\"RoleB?RoleC: i32\\\"\" ]\n \
2 -> 3 [ label = \"\\\"0\\\"\" ]\n \
2 -> 4 [ label = \"\\\"RoleB!RoleC: i32\\\"\" ]\n \
4 -> 5 [ label = \"\\\"RoleB?RoleC: i32\\\"\" ]\n \
5 -> 2 [ label = \"\\\"µ\\\"\" ]\n\
}\n"
);
let graph_c = &graphs["RoleC"];
assert_eq!(
format!("{:?}", Dot::new(&graph_c)),
"digraph {\n \
0 [ label = \"\\\"0\\\"\" ]\n \
1 [ label = \"\\\"1\\\"\" ]\n \
2 [ label = \"\\\"2\\\"\" ]\n \
3 [ label = \"\\\"2.1\\\"\" ]\n \
4 [ label = \"\\\"2.1\\\"\" ]\n \
5 [ label = \"\\\"2.2\\\"\" ]\n \
6 [ label = \"\\\"2.3\\\"\" ]\n \
7 [ label = \"\\\"2.4\\\"\" ]\n \
0 -> 1 [ label = \"\\\"RoleC?RoleB: i32\\\"\" ]\n \
1 -> 2 [ label = \"\\\"RoleC!RoleB: i32\\\"\" ]\n \
2 -> 3 [ label = \"\\\"0\\\"\" ]\n \
2 -> 4 [ label = \"\\\"RoleC?RoleB: i32\\\"\" ]\n \
4 -> 5 [ label = \"\\\"RoleC!RoleA: i32\\\"\" ]\n \
5 -> 6 [ label = \"\\\"RoleC?RoleA: i32\\\"\" ]\n \
6 -> 7 [ label = \"\\\"RoleC!RoleB: i32\\\"\" ]\n \
7 -> 2 [ label = \"\\\"µ\\\"\" ]\n\
}\n"
);
assert_eq!(kmc, None);
}