#![allow(dead_code, clippy::type_complexity)] use mpstthree::binary::struct_trait::end::End; use mpstthree::binary::struct_trait::recv::Recv; use mpstthree::binary::struct_trait::send::Send; use mpstthree::role::broadcast::RoleBroadcast; use mpstthree::role::end::RoleEnd; use mpstthree::{ checker_concat, checker_concat_impl, create_meshedchannels, create_multiple_normal_name, create_multiple_normal_role, }; use petgraph::dot::Dot; use std::fs::read_to_string; // Create new MeshedChannels create_meshedchannels!(MeshedChannels, 3); // Create new roles create_multiple_normal_role!( RoleA, RoleADual | RoleB, RoleBDual | RoleC, RoleCDual | ); // Create new names create_multiple_normal_name!(NameA, NameB, NameC); // The new types struct Haggle; struct Price; struct Happy; struct Info; // Types // A type Choose0fromAtoB = Send; type Choose0fromAtoC = Send; // B type Recurs0BfromA = Recv; enum Branches0BfromA { End(MeshedChannels), Haggle( MeshedChannels< Recv>, End, RoleA>>, NameB, >, ), Happy(MeshedChannels, End, RoleA, NameB>), } // C type Recurs0CfromA = Recv; enum Branches0CfromA { End(MeshedChannels), Haggle(MeshedChannels, NameC>), Happy(MeshedChannels, End, RoleA, NameC>), } // Creating the MP sessions // For A type EndpointAEnd = MeshedChannels; type EndpointAHaggle = MeshedChannels< Send>, Choose0fromAtoC, RoleB>, NameA, >; type EndpointAHappy = MeshedChannels, Send, RoleB>, NameA>; type EndpointAFull = MeshedChannels; // For B type EndpointBFull = MeshedChannels, NameB>; // For C type EndpointCFull = MeshedChannels, NameC>; ///////////////////////////////////////// checker_concat_impl!( [Branches0BfromA, Happy, Branches0CfromA, Happy], [Branches0BfromA, Haggle, Branches0CfromA, Haggle], [Branches0BfromA, End, Branches0CfromA, End] ); pub fn main() { let (graphs, kmc) = checker_concat!( "bargain", EndpointAFull, EndpointBFull, EndpointCFull, => [ EndpointAHappy, Branches0BfromA, Happy, Branches0CfromA, Happy ], [ EndpointAHaggle, Branches0BfromA, Haggle, Branches0CfromA, Haggle ], [ EndpointAEnd, Branches0BfromA, End, Branches0CfromA, End ] ) .unwrap(); ////////////// Test graph A 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 \ 4 [ label = \"\\\"0.1\\\"\" ]\n \ 5 [ label = \"\\\"0.2\\\"\" ]\n \ 6 [ label = \"\\\"0.3\\\"\" ]\n \ 0 -> 1 [ label = \"\\\"0\\\"\" ]\n \ 0 -> 2 [ label = \"\\\"RoleA!RoleB: Haggle\\\"\" ]\n \ 2 -> 3 [ label = \"\\\"RoleA?RoleB: Price\\\"\" ]\n \ 3 -> 0 [ label = \"\\\"µ\\\"\" ]\n \ 0 -> 4 [ label = \"\\\"RoleA!RoleB: Happy\\\"\" ]\n \ 4 -> 5 [ label = \"\\\"RoleA!RoleC: Info\\\"\" ]\n \ 5 -> 6 [ label = \"\\\"0\\\"\" ]\n\ }\n" ); ////////////// Test graph B let graph_b = &graphs["RoleB"]; assert_eq!( format!("{:?}", Dot::new(&graph_b)), "digraph {\n \ 0 [ label = \"\\\"0\\\"\" ]\n \ 1 [ label = \"\\\"0.1\\\"\" ]\n \ 2 [ label = \"\\\"0.1\\\"\" ]\n \ 3 [ label = \"\\\"0.2\\\"\" ]\n \ 4 [ label = \"\\\"0.1\\\"\" ]\n \ 5 [ label = \"\\\"0.2\\\"\" ]\n \ 0 -> 1 [ label = \"\\\"0\\\"\" ]\n \ 0 -> 2 [ label = \"\\\"RoleB?RoleA: Haggle\\\"\" ]\n \ 2 -> 3 [ label = \"\\\"RoleB!RoleA: Price\\\"\" ]\n \ 3 -> 0 [ label = \"\\\"µ\\\"\" ]\n \ 0 -> 4 [ label = \"\\\"RoleB?RoleA: Happy\\\"\" ]\n \ 4 -> 5 [ label = \"\\\"0\\\"\" ]\n\ }\n" ); ////////////// Test graph C let graph_c = &graphs["RoleC"]; assert_eq!( format!("{:?}", Dot::new(&graph_c)), "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 = \"\\\"RoleC?RoleA: Info\\\"\" ]\n \ 2 -> 3 [ label = \"\\\"0\\\"\" ]\n\ }\n" ); ////////////// Test KMC output 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/bargain_1_kmc.txt").unwrap() ); ////////////// Test KMC number assert_eq!(kmc, Some(1)); }