use mpstthree::binary::struct_trait::{end::End, recv::Recv, send::Send}; // The basic types use mpstthree::generate; /* The macro for generating the roles and the MeshedChannels */ use mpstthree::role::broadcast::RoleBroadcast; use mpstthree::{checker_concat, checker_concat_impl}; /* Optional: used only for protocols with * choice/offer */ use mpstthree::role::end::RoleEnd; // The final type for the stacks and the names of the roles // Used for checking the protocol use std::error::Error; // Create new MeshedChannels for two participants generate!("rec_and_cancel", MeshedChannels, A, B); // Payload types struct Request; struct Response; struct Stop; // Types // Binary types for A type StartA0 = Recv>; // Recv a Request then Send a choice type OrderingA0 = RoleB; // Stack for recv then sending a choice type LoopA0 = Send; // Send a choice type OrderingLoopA0 = RoleBroadcast; // Stack for sending a choice type MoreA1 = Recv>; // Recv Response then send a choice type OrderingMoreA1 = RoleB; // Stack for the previous binary type type DoneA1 = Recv; // Recv Stop type OrderingDoneA1 = RoleB; // Stack for the previous binary type // Binary types for B type StartB0 = Send>; // Send a Request then Recv a choice type OrderingB0 = RoleA>; // Stack for send then receiving a choice from A type LoopB0 = Recv; // Recv a choice type OrderingLoopB0 = RoleA; // Stack for recv a choice type MoreB1 = Send>; // Recv Request then Send Response then receive a choice type OrderingMoreB1 = RoleA>; // Stack for the previous binary type type DoneB1 = Send; // Send Stop type OrderingDoneB1 = RoleA; // Stack for the previous binary type enum Branching0fromAtoB { // Sum type containing the different paths of the choice More(MeshedChannels), Done(MeshedChannels), } // Creating the endpoints // A type EndpointAMore = MeshedChannels; type EndpointADone = MeshedChannels; type EndpointALoop = MeshedChannels; type EndpointA = MeshedChannels; // B type EndpointBLoop = MeshedChannels; type EndpointB = MeshedChannels; fn endpoint_a(s: EndpointA) -> Result<(), Box> { let (_, s) = s.recv()?; recurs_a(s, 5) } fn recurs_a(s: EndpointALoop, loops: i32) -> Result<(), Box> { if loops > 0 { let s: EndpointAMore = choose_mpst_a_to_all!(s, Branching0fromAtoB::More); let (_, s) = s.recv()?; recurs_a(s, loops - 1) } else { let s: EndpointADone = choose_mpst_a_to_all!(s, Branching0fromAtoB::Done); let (_, s) = s.recv()?; s.close() } } fn endpoint_b(s: EndpointB) -> Result<(), Box> { let s = s.send(Request {})?; recurs_b(s) } fn recurs_b(s: EndpointBLoop) -> Result<(), Box> { offer_mpst!(s, { Branching0fromAtoB::More(s) => { let s = s.send(Response {})?; recurs_b(s) }, Branching0fromAtoB::Done(s) => { let s = s.send(Stop {})?; s.close() }, }) } checker_concat_impl!( [Branching0fromAtoB, More,], [Branching0fromAtoB, Done,] ); fn main() { let (thread_a, thread_b) = fork_mpst(endpoint_a, endpoint_b); thread_a.join().unwrap(); thread_b.join().unwrap(); let (_, _kmc) = checker_concat!( "basic", EndpointA, EndpointB => [ EndpointAMore, Branching0fromAtoB, More, ], [ EndpointADone, Branching0fromAtoB, Done, ] ) .unwrap(); // println!("min kMC: {kmc:?}"); }