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