momba-explore 0.1.1

State space exploration engine for PTAs and MDPs augmented with variables.
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

use serde::{Deserialize, Serialize};

use super::expressions::*;

/// Represents an *action pattern*.
///
/// Action patterns enable value passing.
/// A pattern is either *silent* or *labeled*.
/// Analogously to labeled actions, labeled patterns have a sequence of arguments
/// represented by [PatternArgument].
/// A pattern argument has a *direction* which is either *read* or *write*.
/// A read argument means that the pattern is able to receive a value via the
/// corresponding argument of an action.
/// A write argument means that the pattern will send a value via the corresponding
/// argument of an action.
#[derive(Serialize, Deserialize, Eq, PartialEq, Clone, Debug)]
#[serde(rename_all = "SCREAMING_SNAKE_CASE", tag = "kind")]
pub enum ActionPattern {
    /// The silent pattern.
    Silent,
    /// A labeled pattern.
    Labeled(LabeledPattern),
}

/// Represents a labeled pattern.
#[derive(Serialize, Deserialize, Eq, PartialEq, Clone, Debug)]
pub struct LabeledPattern {
    /// The label of the pattern.
    pub label: String,
    /// The pattern arguments.
    pub arguments: Vec<PatternArgument>,
}

/// Represents a pattern argument.
#[derive(Serialize, Deserialize, Eq, PartialEq, Clone, Debug)]
#[serde(rename_all = "SCREAMING_SNAKE_CASE", tag = "direction")]
pub enum PatternArgument {
    Write { value: Expression },
    Read { identifier: String },
}

#[derive(Serialize, Deserialize, Eq, PartialEq, Clone, Debug)]
pub struct WriteArgument {
    pub value: Expression,
}

#[derive(Serialize, Deserialize, Eq, PartialEq, Clone, Debug)]
pub struct ReadArgument {
    pub identifier: String,
}