modality_lang/
ast.rs

1use serde::{Serialize, Deserialize};
2
3/// Represents a property with a sign (+ or -)
4#[derive(Debug, Clone, PartialEq, Serialize, Deserialize)]
5pub struct Property {
6    pub sign: PropertySign,
7    pub name: String,
8}
9
10/// The sign of a property
11#[derive(Debug, Clone, PartialEq, Serialize, Deserialize)]
12pub enum PropertySign {
13    Plus,
14    Minus,
15}
16
17/// Represents a transition between nodes
18#[derive(Debug, Clone, PartialEq, Serialize, Deserialize)]
19pub struct Transition {
20    pub from: String,
21    pub to: String,
22    pub properties: Vec<Property>,
23}
24
25/// Represents a graph within a model
26#[derive(Debug, Clone, PartialEq, Serialize, Deserialize)]
27pub struct Graph {
28    pub name: String,
29    pub transitions: Vec<Transition>,
30}
31
32/// Represents the current state of a graph
33#[derive(Debug, Clone, PartialEq, Serialize, Deserialize)]
34pub struct GraphState {
35    pub graph_name: String,
36    pub current_nodes: Vec<String>,
37}
38
39/// Represents a complete model
40#[derive(Debug, Clone, PartialEq, Serialize, Deserialize)]
41pub struct Model {
42    pub name: String,
43    pub graphs: Vec<Graph>,
44    pub state: Option<Vec<GraphState>>,
45}
46
47/// Represents a temporal modal formula
48#[derive(Debug, Clone, PartialEq, Serialize, Deserialize)]
49pub struct Formula {
50    pub name: String,
51    pub expression: FormulaExpr,
52}
53
54/// Represents a formula expression
55#[derive(Debug, Clone, PartialEq, Serialize, Deserialize)]
56pub enum FormulaExpr {
57    /// Boolean literals
58    True,
59    False,
60    /// Boolean operations
61    And(Box<FormulaExpr>, Box<FormulaExpr>),
62    Or(Box<FormulaExpr>, Box<FormulaExpr>),
63    Not(Box<FormulaExpr>),
64    /// Parenthesized expressions
65    Paren(Box<FormulaExpr>),
66    /// Modal operators
67    Diamond(Vec<Property>, Box<FormulaExpr>),
68    Box(Vec<Property>, Box<FormulaExpr>),
69}
70
71impl Model {
72    /// Create a new model with the given name
73    pub fn new(name: String) -> Self {
74        Self {
75            name,
76            graphs: Vec::new(),
77            state: None,
78        }
79    }
80
81    /// Add a graph to this model
82    pub fn add_graph(&mut self, graph: Graph) {
83        self.graphs.push(graph);
84    }
85
86    /// Set the state information for this model
87    pub fn set_state(&mut self, state: Vec<GraphState>) {
88        self.state = Some(state);
89    }
90}
91
92impl Graph {
93    /// Create a new graph with the given name
94    pub fn new(name: String) -> Self {
95        Self {
96            name,
97            transitions: Vec::new(),
98        }
99    }
100
101    /// Add a transition to this graph
102    pub fn add_transition(&mut self, transition: Transition) {
103        self.transitions.push(transition);
104    }
105}
106
107impl Transition {
108    /// Create a new transition
109    pub fn new(from: String, to: String) -> Self {
110        Self {
111            from,
112            to,
113            properties: Vec::new(),
114        }
115    }
116
117    /// Add a property to this transition
118    pub fn add_property(&mut self, property: Property) {
119        self.properties.push(property);
120    }
121}
122
123impl Property {
124    /// Create a new property
125    pub fn new(sign: PropertySign, name: String) -> Self {
126        Self { sign, name }
127    }
128}
129
130impl GraphState {
131    /// Create a new graph state
132    pub fn new(graph_name: String, current_nodes: Vec<String>) -> Self {
133        Self {
134            graph_name,
135            current_nodes,
136        }
137    }
138}
139
140impl Formula {
141    /// Create a new formula
142    pub fn new(name: String, expression: FormulaExpr) -> Self {
143        Self { name, expression }
144    }
145}
146
147/// Represents a top-level item in a modality file
148#[derive(Debug, Clone, PartialEq, Serialize, Deserialize)]
149pub enum TopLevelItem {
150    Model(Model),
151    Formula(Formula),
152}
modality_lang/ast.rs

modality_lang/
ast.rs
