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
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
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150

//! Data structures for representing automata networks.

use std::collections::{HashMap, HashSet};

use indexmap::{IndexMap, IndexSet};
use serde::{Deserialize, Serialize};

use super::actions::*;
use super::expressions::*;
use super::references::*;
use super::types::*;
use super::values::*;

/// Represents a network of automata.
#[derive(Serialize, Deserialize, Eq, PartialEq, Clone, Debug)]
pub struct Network {
    pub declarations: Declarations,
    pub automata: IndexMap<String, Automaton>,
    pub links: Vec<Link>,
    pub initial_states: Vec<State>,
}

impl Network {
    pub fn get_index_of_global_variable(&self, identifier: &str) -> Option<usize> {
        self.declarations.global_variables.get_index_of(identifier)
    }

    pub fn get_index_of_transient_variable(&self, identifier: &str) -> Option<usize> {
        self.declarations
            .transient_variables
            .get_index_of(identifier)
    }

    pub fn get_automaton(&self, reference: &AutomatonReference) -> &Automaton {
        self.automata.get(&reference.name).unwrap()
    }

    pub fn get_location(&self, reference: &LocationReference) -> &Location {
        self.get_automaton(&reference.automaton)
            .locations
            .get(&reference.name)
            .unwrap()
    }

    pub fn get_edge(&self, reference: &EdgeReference) -> &Edge {
        self.get_location(&reference.location)
            .edges
            .get(reference.index)
            .unwrap()
    }

    pub fn get_destination(&self, reference: &DestinationReference) -> &Destination {
        self.get_edge(&reference.edge)
            .destinations
            .get(reference.index)
            .unwrap()
    }
}

/// The index of an action label relative to [Declarations].
pub type LabelIndex = usize;

#[derive(Serialize, Deserialize, Eq, PartialEq, Clone, Debug)]
pub struct Declarations {
    pub global_variables: IndexMap<String, Type>,
    pub transient_variables: IndexMap<String, Expression>,
    pub clock_variables: IndexSet<String>,
    pub action_labels: IndexMap<String, Vec<Type>>,
}

#[derive(Serialize, Deserialize, Eq, PartialEq, Clone, Debug)]
pub struct Automaton {
    pub locations: IndexMap<String, Location>,
}

#[derive(Serialize, Deserialize, Eq, PartialEq, Clone, Debug)]
pub struct Location {
    pub invariant: HashSet<ClockConstraint>,
    pub edges: Vec<Edge>,
}

#[derive(Serialize, Deserialize, Eq, PartialEq, Clone, Hash, Debug)]
pub struct ClockConstraint {
    pub left: Clock,
    pub right: Clock,
    pub is_strict: bool,
    pub bound: Expression,
}

#[derive(Serialize, Deserialize, Eq, PartialEq, Clone, Hash, Debug)]
#[serde(rename_all = "SCREAMING_SNAKE_CASE", tag = "kind")]
pub enum Clock {
    Zero,
    Variable { identifier: String },
}

#[derive(Serialize, Deserialize, Eq, PartialEq, Clone, Debug)]
pub struct Edge {
    pub pattern: ActionPattern,
    pub guard: Guard,
    pub destinations: Vec<Destination>,
}

#[derive(Serialize, Deserialize, Eq, PartialEq, Clone, Debug)]
pub struct Guard {
    pub boolean_condition: Expression,
    pub clock_constraints: HashSet<ClockConstraint>,
}

#[derive(Serialize, Deserialize, Eq, PartialEq, Clone, Debug)]
pub struct Destination {
    pub location: String,
    pub probability: Expression,
    pub assignments: Vec<Assignment>,
    pub reset: HashSet<Clock>,
}

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

#[derive(Serialize, Deserialize, Eq, PartialEq, Clone, Debug)]
pub struct State {
    pub values: HashMap<String, Value>,
    pub locations: HashMap<String, String>,
    pub zone: HashSet<ClockConstraint>,
}

#[derive(Serialize, Deserialize, Eq, PartialEq, Clone, Debug)]
pub struct Link {
    pub slots: IndexSet<String>,
    pub vector: IndexMap<String, LinkPattern>,
    pub result: LinkResult,
}

#[derive(Serialize, Deserialize, Eq, PartialEq, Clone, Debug)]
#[serde(rename_all = "SCREAMING_SNAKE_CASE", tag = "kind")]
pub enum LinkResult {
    Silent,
    Labeled(LinkPattern),
}

#[derive(Serialize, Deserialize, Eq, PartialEq, Clone, Debug)]
pub struct LinkPattern {
    pub action_type: String,
    pub arguments: Vec<String>,
}