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

use crate::ast::{Model, Graph, Transition, Property, PropertySign, Formula, FormulaExpr, GraphState, TopLevelItem};

grammar;

pub TopLevel: Vec<Model> = {
    <items:TopLevelItem*> => {
        let mut models = Vec::new();
        for item in items {
            if let TopLevelItem::Model(model) = item {
                models.push(model);
            }
        }
        models
    }
};

TopLevelItem: TopLevelItem = {
    <model:Model> => TopLevelItem::Model(model),
    <formula:Formula> => TopLevelItem::Formula(formula)
};

pub Model: Model = {
    <model:ModelDecl> => model
};

ModelDecl: Model = {
    "model" <name:Ident> ":" <graphs:Graph*> => {
        let mut model = Model::new(name);
        for graph in graphs {
            model.add_graph(graph);
        }
        model
    }
};

Graph: Graph = {
    "graph" <name:Ident> ":" <transitions:Transition*> => {
        let mut graph = Graph::new(name);
        for transition in transitions {
            graph.add_transition(transition);
        }
        graph
    }
};

Transition: Transition = {
    <from:Ident> "-->" <to:Ident> => {
        Transition::new(from, to)
    },
    <from:Ident> "-->" <to:Ident> ":" <properties:PropertyList> => {
        let mut transition = Transition::new(from, to);
        for property in properties {
            transition.add_property(property);
        }
        transition
    }
};

PropertyList: Vec<Property> = {
    <property:Property> => vec![property],
    <properties:PropertyList> <property:Property> => {
        let mut props = properties;
        props.push(property);
        props
    }
};

Property: Property = {
    "+" <name:Ident> => Property::new(PropertySign::Plus, name),
    "-" <name:Ident> => Property::new(PropertySign::Minus, name)
};

// Formula parsing
pub Formula: Formula = {
    <formula:FormulaDecl> => formula
};

FormulaDecl: Formula = {
    "formula" <name:Ident> ":" <expr:FormulaExpr> => {
        Formula::new(name, expr)
    }
};

FormulaExpr: FormulaExpr = {
    <expr:FormulaOrExpr> => expr
};

FormulaOrExpr: FormulaExpr = {
    <expr:FormulaAndExpr> => expr,
    <expr:FormulaOrExpr> "or" <expr2:FormulaAndExpr> => {
        FormulaExpr::Or(Box::new(expr), Box::new(expr2))
    }
};

FormulaAndExpr: FormulaExpr = {
    <expr:FormulaAtom> => expr,
    <expr:FormulaAndExpr> "and" <expr2:FormulaAtom> => {
        FormulaExpr::And(Box::new(expr), Box::new(expr2))
    }
};

FormulaAtom: FormulaExpr = {
    "true" => FormulaExpr::True,
    "false" => FormulaExpr::False,
    "(" <expr:FormulaExpr> ")" => {
        FormulaExpr::Paren(Box::new(expr))
    },
    "<" <properties:PropertyList> ">" <expr:FormulaAtom> => {
        FormulaExpr::Diamond(properties, Box::new(expr))
    },
    "[" <properties:PropertyList> "]" <expr:FormulaAtom> => {
        FormulaExpr::Box(properties, Box::new(expr))
    }
};

Ident: String = {
    r#"[a-zA-Z_][a-zA-Z0-9_]*"# => <>.to_string()
};