Generalize definition of SumExpr a little...Lets sum all elements of
[repair.git] / Repair / RepairCompiler / mdl.tex
1 Model Definition Language
2 xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx
3
4 rules ::= rules rule | rule
5
6 rule ::= ruletype OPENBRACKET quantifiers CLOSEBRACKET COMMA guard IMPLIES inclusions SEMICOLON
7
8 ruletype ::= STATIC | DELAY | /*nothing*/
9
10 quantifiers ::= quantifiers COMMA quantifier | quantifier | /* nothing */
11
12 quantifier ::= FORALL ID:var IN ID:set 
13              | FORALL LT ID:r1 COMMA ID:r2 GT IN ID:relation
14              | FOR ID:var EQUALS expr:lower TO expr:upper
15
16 guard ::= guard AND guard
17         | guard OR guard
18         | NOT guard
19         | expr EQUALS expr
20         | expr LT expr
21         | TRUE
22         | OPENPAREN guard CLOSEPAREN
23         | expr IN ID:set
24         | LT expr:r1 COMMA expr:r2 GT IN ID:relation
25         | ISVALID OPENPAREN expr CLOSEPAREN
26         | ISVALID OPENPAREN expr COMMA ID:var CLOSEPAREN
27
28 inclusion ::= expr IN ID:set
29             | LT expr:r1 COMMA expr:r2 GT IN ID:relation
30
31
32
33 expr ::= ID:var 
34        | OPENPAREN expr CLOSEPAREN 
35        | LITERAL OPENPAREN literal CLOSEPAREN
36        | expr operator expr
37        | expr DOT ID:field
38        | expr DOT ID:field OPENBRACKET expr:index CLOSEBRACKET
39        | CAST OPENPAREN ID:type COMMA expr CLOSEPAREN 
40
41 operator ::= ADD | SUB | MULT | DIV
42
43 literal ::= TRUE | DECIMAL | STRING | CHAR | ID
44