hibana 0.8.0

Const-projected Affine Multiparty Session Types for choreography-first Rust protocols
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

use hibana::g::{self, Msg};
use hibana::integration::cap::control::{LoopBreakKind, LoopContinueKind};
use hibana::integration::program::{RoleProgram, project};

const TEST_LOOP_CONTINUE_LOGICAL: u8 = 0xA1;
const TEST_LOOP_BREAK_LOGICAL: u8 = 0xA2;

#[test]
fn nested_loop_scope_balanced() {
    let tick = g::send::<2, 3, Msg<1, ()>, 0>();
    let ack_branch = g::seq(
        g::send::<2, 2, Msg<{ TEST_LOOP_CONTINUE_LOGICAL }, (), LoopContinueKind>, 0>()
            .policy::<10>(),
        g::send::<2, 2, Msg<{ TEST_LOOP_CONTINUE_LOGICAL }, (), LoopContinueKind>, 0>(),
    );
    let loss_branch = g::seq(
        g::send::<2, 2, Msg<{ TEST_LOOP_BREAK_LOGICAL }, (), LoopBreakKind>, 0>().policy::<10>(),
        g::send::<2, 2, Msg<{ TEST_LOOP_BREAK_LOGICAL }, (), LoopBreakKind>, 0>(),
    );
    let ack_loss_route = g::route(ack_branch, loss_branch);
    let continue_arm = g::seq(
        g::send::<2, 2, Msg<{ TEST_LOOP_CONTINUE_LOGICAL }, (), LoopContinueKind>, 0>()
            .policy::<11>(),
        g::seq(tick, ack_loss_route),
    );
    let break_arm =
        g::send::<2, 2, Msg<{ TEST_LOOP_BREAK_LOGICAL }, (), LoopBreakKind>, 0>().policy::<11>();
    let decision = g::route(continue_arm, break_arm);

    let role_program: RoleProgram<2> = project(&decision);
    drop(role_program);

    let handshake = g::send::<0, 1, Msg<10, ()>, 0>();
    let combined = g::par(handshake, decision);
    let transport_program: RoleProgram<2> = project(&combined);
    drop(transport_program);
}