mpstthree 0.1.17

A library implementing Multiparty Session Types for 2 or more participants
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
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128

#![allow(clippy::collapsible_else_if)]

//! This module contains the definition and associated functions and traits
//! for the Recv structure.

use crate::binary::struct_trait::session::Session;
use crate::binary_atmp::struct_trait::send::SendTimed;

use crossbeam_channel::Receiver;

use std::marker;

/// Receive `T`, then continue as `S`.
/// 6 additional parameters are present:
/// * CLOCK: a char to indicate which clock will be tested under the time constraints (in *seconds*)
/// * START: an i128 which represents the lower bound for the time constraint
/// * INCLUDE_START: a bool which indicates whether START is included in the bound
/// * END: an i128 which represents the upper bound for the time constraint
/// * INCLUDE_END: a bool which indicates whether END is included in the bound
/// * RESET: a char which whether CLOCK needs to be reset after the receive. Currently limited to
///   CLOCK, future feature will use a Vec<char>
#[must_use]
#[derive(Debug)]
pub struct RecvTimed<
    T,
    const CLOCK: char,
    const START: i128,
    const INCLUDE_START: bool,
    const END: i128,
    const INCLUDE_END: bool,
    const RESET: char,
    S,
> where
    T: marker::Send,
    S: Session,
{
    #[doc(hidden)]
    pub channel: Receiver<(T, S)>,
    #[doc(hidden)]
    pub clock: char,
    #[doc(hidden)]
    pub start: i128,
    #[doc(hidden)]
    pub include_start: bool,
    #[doc(hidden)]
    pub end: i128,
    #[doc(hidden)]
    pub include_end: bool,
    #[doc(hidden)]
    pub reset: char,
}

impl<
        T: marker::Send,
        const CLOCK: char,
        const START: i128,
        const INCLUDE_START: bool,
        const END: i128,
        const INCLUDE_END: bool,
        const RESET: char,
        S: Session,
    > RecvTimed<T, CLOCK, START, INCLUDE_START, END, INCLUDE_END, RESET, S>
{
    #[doc(hidden)]
    pub fn constraint(&self) -> String {
        if self.start < 0 {
            if self.end >= 0 {
                if self.include_end {
                    format!("{} <= {}", self.clock, self.end)
                } else {
                    format!("{} < {}", self.clock, self.end)
                }
            } else {
                panic!("Both start and end parameters are negative")
            }
        } else {
            if self.end < 0 {
                if self.include_start {
                    format!("{} <= {}", self.start, self.clock)
                } else {
                    format!("{} < {}", self.start, self.clock)
                }
            } else {
                match (self.include_start, self.include_end) {
                    (true, true) => format!("{} <= {} <= {}", self.start, self.clock, self.end),
                    (true, false) => format!("{} <= {} < {}", self.start, self.clock, self.end),
                    (false, true) => format!("{} < {} <= {}", self.start, self.clock, self.end),
                    (false, false) => format!("{} < {} < {}", self.start, self.clock, self.end),
                }
            }
        }
    }
}

impl<
        T: marker::Send,
        const CLOCK: char,
        const START: i128,
        const INCLUDE_START: bool,
        const END: i128,
        const INCLUDE_END: bool,
        const RESET: char,
        S: Session,
    > Session for RecvTimed<T, CLOCK, START, INCLUDE_START, END, INCLUDE_END, RESET, S>
{
    type Dual = SendTimed<T, CLOCK, START, INCLUDE_START, END, INCLUDE_END, RESET, S::Dual>;

    fn new() -> (Self, Self::Dual) {
        let (sender, receiver) = Self::Dual::new();
        (receiver, sender)
    }

    fn head_str() -> String {
        "Recv".to_string()
    }

    fn tail_str() -> String {
        format!("{}<{}>", S::head_str(), S::tail_str())
    }

    fn self_head_str(&self) -> String {
        "Recv".to_string()
    }

    fn self_tail_str(&self) -> String {
        format!("{}<{}>", S::head_str(), S::tail_str())
    }
}