momba_explore/model/
network.rs

1//! Data structures for representing automata networks.
2
3use std::collections::{HashMap, HashSet};
4
5use indexmap::{IndexMap, IndexSet};
6use serde::{Deserialize, Serialize};
7
8use super::actions::*;
9use super::expressions::*;
10use super::references::*;
11use super::types::*;
12use super::values::*;
13
14/// Represents a network of automata.
15#[derive(Serialize, Deserialize, Eq, PartialEq, Clone, Debug)]
16pub struct Network {
17    pub declarations: Declarations,
18    pub automata: IndexMap<String, Automaton>,
19    pub links: Vec<Link>,
20    pub initial_states: Vec<State>,
21}
22
23impl Network {
24    pub fn get_index_of_global_variable(&self, identifier: &str) -> Option<usize> {
25        self.declarations.global_variables.get_index_of(identifier)
26    }
27
28    pub fn get_index_of_transient_variable(&self, identifier: &str) -> Option<usize> {
29        self.declarations
30            .transient_variables
31            .get_index_of(identifier)
32    }
33
34    pub fn get_automaton(&self, reference: &AutomatonReference) -> &Automaton {
35        self.automata.get(&reference.name).unwrap()
36    }
37
38    pub fn get_location(&self, reference: &LocationReference) -> &Location {
39        self.get_automaton(&reference.automaton)
40            .locations
41            .get(&reference.name)
42            .unwrap()
43    }
44
45    pub fn get_edge(&self, reference: &EdgeReference) -> &Edge {
46        self.get_location(&reference.location)
47            .edges
48            .get(reference.index)
49            .unwrap()
50    }
51
52    pub fn get_destination(&self, reference: &DestinationReference) -> &Destination {
53        self.get_edge(&reference.edge)
54            .destinations
55            .get(reference.index)
56            .unwrap()
57    }
58}
59
60/// The index of an action label relative to [Declarations].
61pub type LabelIndex = usize;
62
63#[derive(Serialize, Deserialize, Eq, PartialEq, Clone, Debug)]
64pub struct Declarations {
65    pub global_variables: IndexMap<String, Type>,
66    pub transient_variables: IndexMap<String, Expression>,
67    pub clock_variables: IndexSet<String>,
68    pub action_labels: IndexMap<String, Vec<Type>>,
69}
70
71#[derive(Serialize, Deserialize, Eq, PartialEq, Clone, Debug)]
72pub struct Automaton {
73    pub locations: IndexMap<String, Location>,
74}
75
76#[derive(Serialize, Deserialize, Eq, PartialEq, Clone, Debug)]
77pub struct Location {
78    pub invariant: HashSet<ClockConstraint>,
79    pub edges: Vec<Edge>,
80}
81
82#[derive(Serialize, Deserialize, Eq, PartialEq, Clone, Hash, Debug)]
83pub struct ClockConstraint {
84    pub left: Clock,
85    pub right: Clock,
86    pub is_strict: bool,
87    pub bound: Expression,
88}
89
90#[derive(Serialize, Deserialize, Eq, PartialEq, Clone, Hash, Debug)]
91#[serde(rename_all = "SCREAMING_SNAKE_CASE", tag = "kind")]
92pub enum Clock {
93    Zero,
94    Variable { identifier: String },
95}
96
97#[derive(Serialize, Deserialize, Eq, PartialEq, Clone, Debug)]
98pub struct Edge {
99    pub pattern: ActionPattern,
100    pub guard: Guard,
101    pub destinations: Vec<Destination>,
102}
103
104#[derive(Serialize, Deserialize, Eq, PartialEq, Clone, Debug)]
105pub struct Guard {
106    pub boolean_condition: Expression,
107    pub clock_constraints: HashSet<ClockConstraint>,
108}
109
110#[derive(Serialize, Deserialize, Eq, PartialEq, Clone, Debug)]
111pub struct Destination {
112    pub location: String,
113    pub probability: Expression,
114    pub assignments: Vec<Assignment>,
115    pub reset: HashSet<Clock>,
116}
117
118#[derive(Serialize, Deserialize, Eq, PartialEq, Clone, Debug)]
119pub struct Assignment {
120    pub target: Expression,
121    pub value: Expression,
122    pub index: usize,
123}
124
125#[derive(Serialize, Deserialize, Eq, PartialEq, Clone, Debug)]
126pub struct State {
127    pub values: HashMap<String, Value>,
128    pub locations: HashMap<String, String>,
129    pub zone: HashSet<ClockConstraint>,
130}
131
132#[derive(Serialize, Deserialize, Eq, PartialEq, Clone, Debug)]
133pub struct Link {
134    pub slots: IndexSet<String>,
135    pub vector: IndexMap<String, LinkPattern>,
136    pub result: LinkResult,
137}
138
139#[derive(Serialize, Deserialize, Eq, PartialEq, Clone, Debug)]
140#[serde(rename_all = "SCREAMING_SNAKE_CASE", tag = "kind")]
141pub enum LinkResult {
142    Silent,
143    Labeled(LinkPattern),
144}
145
146#[derive(Serialize, Deserialize, Eq, PartialEq, Clone, Debug)]
147pub struct LinkPattern {
148    pub action_type: String,
149    pub arguments: Vec<String>,
150}
momba_explore/model/network.rs

momba_explore/model/
network.rs
