use mpstthree::binary::struct_trait::{end::End, recv::Recv, send::Send}; use mpstthree::role::broadcast::RoleBroadcast; use mpstthree::role::end::RoleEnd; use mpstthree::{checker_concat, checker_concat_impl, generate}; use rand::{thread_rng, Rng}; use std::error::Error; use std::fs::read_to_string; // See the folder scribble_protocols for the related Scribble protocol // Create the new MeshedChannels for three participants and the close and fork functions generate!("recursive", MeshedChannels, Data, Handler, Regional); // Payload types struct FindNearestZone; struct ZoneResponse; struct ZoneDataRequest; struct ZoneDataResponse; struct InvalidZone; struct Received; // Types // REGIONAL type Choose0fromRegionalToData = Send; type Choose0fromRegionalToHandler = Send; // DATA enum Branching0fromRegionalToData { Loops( MeshedChannels< Recv>, Offer0fromRegionalToData, RoleHandler>>, NameData, >, ), Invalid( MeshedChannels< Recv>, End, RoleHandler>, NameData, >, ), } type Offer0fromRegionalToData = Recv; // HANDLER enum Branching0fromRegionalToHandler { Loops( MeshedChannels< Send>, Recv>, RoleRegional>>>>, NameHandler, >, ), Invalid( MeshedChannels< Send>, Recv, RoleRegional>>, NameHandler, >, ), } type Offer0fromRegionalToHandler = Recv; // Creating the MP sessions // DATA type EndpointData = MeshedChannels, NameData>; // HANDLER type EndpointHandler = MeshedChannels< End, Send, RoleRegional>, NameHandler, >; // REGIONAL type EndpointRegionalInvalid = MeshedChannels, RoleHandler, NameRegional>; type EndpointRegionalLoops = MeshedChannels< Choose0fromRegionalToData, Send>, RoleHandler>, NameRegional, >; type EndpointRegional = MeshedChannels< Choose0fromRegionalToData, Recv, RoleHandler, NameRegional, >; // Functions fn endpoint_data(s: EndpointData) -> Result<(), Box> { offer_mpst!(s, { Branching0fromRegionalToData::Loops(s) => { let (_, s) = s.recv(); let s = s.send(ZoneDataResponse {}); endpoint_data(s) }, Branching0fromRegionalToData::Invalid(s) => { let (_, s) = s.recv(); let s = s.send(Received {}); s.close() }, }) } fn endpoint_handler(s: EndpointHandler) -> Result<(), Box> { let s = s.send(FindNearestZone {}); offer_mpst!(s, { Branching0fromRegionalToHandler::Loops(s) => { let (_, s) = s.recv(); let s = s.send(ZoneDataRequest {} ); let (_, s) = s.recv(); endpoint_handler(s) }, Branching0fromRegionalToHandler::Invalid(s) => { let (_, s) = s.recv(); let s = s.send(InvalidZone {} ); let (_, s) = s.recv(); s.close() }, }) } fn endpoint_regional(s: EndpointRegional) -> Result<(), Box> { let choice: i32 = thread_rng().gen_range(1..3); let (_, s) = s.recv(); if choice == 1 { let s: EndpointRegionalLoops = choose_mpst_regional_to_all!( s, Branching0fromRegionalToData::Loops, Branching0fromRegionalToHandler::Loops ); let s = s.send(ZoneResponse {}); endpoint_regional(s) } else { let s: EndpointRegionalInvalid = choose_mpst_regional_to_all!( s, Branching0fromRegionalToData::Invalid, Branching0fromRegionalToHandler::Invalid ); let s = s.send(InvalidZone {}); s.close() } } checker_concat_impl!( [ Branching0fromRegionalToData, Loops, Branching0fromRegionalToHandler, Loops, ], [ Branching0fromRegionalToData, Invalid, Branching0fromRegionalToHandler, Invalid, ] ); // Check for bottom-up approach fn checking() { let _ = checker_concat!( "dns_fowler", EndpointHandler, EndpointData, EndpointRegional => [ EndpointRegionalLoops, Branching0fromRegionalToData, Loops, Branching0fromRegionalToHandler, Loops, ], [ EndpointRegionalInvalid, Branching0fromRegionalToData, Invalid, Branching0fromRegionalToHandler, Invalid, ] ) .unwrap(); assert_eq!( "CSA: \u{1b}[92mTrue\n\ \u{1b}[0mBasic: \u{1b}[92mTrue\n\ \u{1b}[0mreduced 1-exhaustive: \u{1b}[92mTrue\n\ \u{1b}[0mreduced 1-safe: \u{1b}[92mTrue\n\ \u{1b}[0m\n", read_to_string("outputs/dns_fowler_1_kmc.txt").unwrap() ); } fn main() { checking(); let (thread_handler, thread_regional, thread_data) = fork_mpst(endpoint_data, endpoint_handler, endpoint_regional); thread_data.join().unwrap(); thread_regional.join().unwrap(); thread_handler.join().unwrap(); }