modality-lang 0.1.6

Modality language lib
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
151
152
153

use wasm_bindgen::prelude::*;
use wasm_bindgen::JsValue;
use crate::ast::{Model, PropertySign, Formula};
use crate::lalrpop_parser::{parse_file_lalrpop, parse_content_lalrpop, parse_all_models_lalrpop, parse_all_models_content_lalrpop, parse_all_formulas_content_lalrpop};
use crate::mermaid::{generate_mermaid_diagram, generate_mermaid_diagrams, generate_mermaid_diagram_with_styling, generate_mermaid_diagram_with_state};
use crate::model_checker::{ModelChecker, State, ModelCheckResult};
use serde_json;

#[wasm_bindgen]
pub struct ModalityParser {
    // This struct can hold any state if needed in the future
}

#[wasm_bindgen]
impl ModalityParser {
    #[wasm_bindgen(constructor)]
    pub fn new() -> ModalityParser {
        ModalityParser { }
    }

    /// Parse a model from a string
    pub fn parse_model(&self, content: &str) -> Result<JsValue, JsValue> {
        let model = parse_content_lalrpop(content)
            .map_err(|e| JsValue::from_str(&e))?;
        wasm_bindgen::JsValue::from_serde(&model).map_err(|e| JsValue::from_str(&format!("Serde error: {}", e)))
    }

    /// Parse all models from a string
    pub fn parse_all_models(&self, content: &str) -> Result<JsValue, JsValue> {
        let models = parse_all_models_content_lalrpop(content)
            .map_err(|e| JsValue::from_str(&e))?;
        wasm_bindgen::JsValue::from_serde(&models).map_err(|e| JsValue::from_str(&format!("Serde error: {}", e)))
    }

    /// Generate Mermaid diagram from a model JSON string
    pub fn generate_mermaid(&self, model_json: &str) -> Result<String, JsValue> {
        let model: Model = serde_json::from_str(model_json)
            .map_err(|e| JsValue::from_str(&format!("JSON parse error: {}", e)))?;
        Ok(generate_mermaid_diagram(&model))
    }

    /// Generate Mermaid diagram with styling from a model JSON string
    pub fn generate_mermaid_styled(&self, model_json: &str) -> Result<String, JsValue> {
        let model: Model = serde_json::from_str(model_json)
            .map_err(|e| JsValue::from_str(&format!("JSON parse error: {}", e)))?;
        Ok(generate_mermaid_diagram_with_styling(&model))
    }

    /// Generate Mermaid diagram with current state highlighting from a model JSON string
    pub fn generate_mermaid_with_state(&self, model_json: &str) -> Result<String, JsValue> {
        let model: Model = serde_json::from_str(model_json)
            .map_err(|e| JsValue::from_str(&format!("JSON parse error: {}", e)))?;
        Ok(generate_mermaid_diagram_with_state(&model))
    }

    /// Parse formulas from a string
    pub fn parse_formulas(&self, content: &str) -> Result<JsValue, JsValue> {
        let formulas = parse_all_formulas_content_lalrpop(content)
            .map_err(|e| JsValue::from_str(&e))?;
        wasm_bindgen::JsValue::from_serde(&formulas).map_err(|e| JsValue::from_str(&format!("Serde error: {}", e)))
    }

    /// Check a formula against a model (per-graph requirement)
    pub fn check_formula(&self, model_json: &str, formula_json: &str) -> Result<JsValue, JsValue> {
        let model: Model = serde_json::from_str(model_json)
            .map_err(|e| JsValue::from_str(&format!("Model JSON parse error: {}", e)))?;
        let formula: Formula = serde_json::from_str(formula_json)
            .map_err(|e| JsValue::from_str(&format!("Formula JSON parse error: {}", e)))?;
        
        let checker = ModelChecker::new(model);
        let result = checker.check_formula(&formula);
        wasm_bindgen::JsValue::from_serde(&result).map_err(|e| JsValue::from_str(&format!("Serde error: {}", e)))
    }

    /// Check a formula against a model (any-state requirement)
    pub fn check_formula_any_state(&self, model_json: &str, formula_json: &str) -> Result<JsValue, JsValue> {
        let model: Model = serde_json::from_str(model_json)
            .map_err(|e| JsValue::from_str(&format!("Model JSON parse error: {}", e)))?;
        let formula: Formula = serde_json::from_str(formula_json)
            .map_err(|e| JsValue::from_str(&format!("Formula JSON parse error: {}", e)))?;
        
        let checker = ModelChecker::new(model);
        let result = checker.check_formula_any_state(&formula);
        wasm_bindgen::JsValue::from_serde(&result).map_err(|e| JsValue::from_str(&format!("Serde error: {}", e)))
    }
}

/// Standalone WASM functions
#[wasm_bindgen]
pub fn parse_model(content: &str) -> Result<JsValue, JsValue> {
    let model = parse_content_lalrpop(content)
        .map_err(|e| JsValue::from_str(&e))?;
    wasm_bindgen::JsValue::from_serde(&model).map_err(|e| JsValue::from_str(&format!("Serde error: {}", e)))
}

#[wasm_bindgen]
pub fn parse_all_models(content: &str) -> Result<JsValue, JsValue> {
    let models = parse_all_models_content_lalrpop(content)
        .map_err(|e| JsValue::from_str(&e))?;
    wasm_bindgen::JsValue::from_serde(&models).map_err(|e| JsValue::from_str(&format!("Serde error: {}", e)))
}

#[wasm_bindgen]
pub fn generate_mermaid(model_json: &str) -> Result<String, JsValue> {
    let model: Model = serde_json::from_str(model_json)
        .map_err(|e| JsValue::from_str(&format!("JSON parse error: {}", e)))?;
    Ok(generate_mermaid_diagram(&model))
}

#[wasm_bindgen]
pub fn generate_mermaid_styled(model_json: &str) -> Result<String, JsValue> {
    let model: Model = serde_json::from_str(model_json)
        .map_err(|e| JsValue::from_str(&format!("JSON parse error: {}", e)))?;
    Ok(generate_mermaid_diagram_with_styling(&model))
}

#[wasm_bindgen]
pub fn generate_mermaid_with_state(model_json: &str) -> Result<String, JsValue> {
    let model: Model = serde_json::from_str(model_json)
        .map_err(|e| JsValue::from_str(&format!("JSON parse error: {}", e)))?;
    Ok(generate_mermaid_diagram_with_state(&model))
}

#[wasm_bindgen]
pub fn parse_formulas(content: &str) -> Result<JsValue, JsValue> {
    let formulas = parse_all_formulas_content_lalrpop(content)
        .map_err(|e| JsValue::from_str(&e))?;
    wasm_bindgen::JsValue::from_serde(&formulas).map_err(|e| JsValue::from_str(&format!("Serde error: {}", e)))
}

#[wasm_bindgen]
pub fn check_formula(model_json: &str, formula_json: &str) -> Result<JsValue, JsValue> {
    let model: Model = serde_json::from_str(model_json)
        .map_err(|e| JsValue::from_str(&format!("Model JSON parse error: {}", e)))?;
    let formula: Formula = serde_json::from_str(formula_json)
        .map_err(|e| JsValue::from_str(&format!("Formula JSON parse error: {}", e)))?;
    
    let checker = ModelChecker::new(model);
    let result = checker.check_formula(&formula);
    wasm_bindgen::JsValue::from_serde(&result).map_err(|e| JsValue::from_str(&format!("Serde error: {}", e)))
}

#[wasm_bindgen]
pub fn check_formula_any_state(model_json: &str, formula_json: &str) -> Result<JsValue, JsValue> {
    let model: Model = serde_json::from_str(model_json)
        .map_err(|e| JsValue::from_str(&format!("Model JSON parse error: {}", e)))?;
    let formula: Formula = serde_json::from_str(formula_json)
        .map_err(|e| JsValue::from_str(&format!("Formula JSON parse error: {}", e)))?;
    
    let checker = ModelChecker::new(model);
    let result = checker.check_formula_any_state(&formula);
    wasm_bindgen::JsValue::from_serde(&result).map_err(|e| JsValue::from_str(&format!("Serde error: {}", e)))
}