; DynAlloy4 Grammar
; Jun 24 2010
; Author Juan Pablo Galeotti

ALLOY4_EXPRESSIONS ::= ALLOY4_EXPRESSION ("," ALLOY4_EXPRESSION)*

DYNALLOY_EXPRESSION ::= ALLOY4_EXPRESSION | 
                        "\pre" "[" VARIABLE_ID "]"

DYNALLOY_EXPRESSIONS ::= DYNALLOY_EXPRESSION ("," DYNALLOY_EXPRESSION)*

ACTION_DECLARATION ::=  "action" ACTION_ID "[" FORMAL_PARAMS "]" "{"
                           "pre" "{" PREDICATE_ID "[" ALLOY4_EXPRESSIONS "]" "}"
                           "post" "{" PREDICATE_ID "[" ALLOY4_EXPRESSIONS "]" "}"
                        "}"

PROGRAM_DECLARATION ::= "program" PROGRAM_ID "[" FORMAL_PARAMS "]" 
                        ; local variable declaration
                        (var "[" FORMAL_PARAMS "]")?
                        "{"
                              DYNALLOY_PROGRAM
                        "}"

ASSERTION_DECLARATION ::= "assertCorrectness" ASSERTION_ID "[" FORMAL_PARAMS "]"
                        "{"
                             "pre" "=" "{" PREDICATE_ID "[" DYNALLOY_EXPRESSIONS "]" "}"
                             "program" "=" "{" DYNALLOY_PROGRAM "}"
                             "post" "=" "{" PREDICATE_ID "[" DYNALLOY_EXPRESSIONS "]" "}"
                        "}"


DYNALLOY_PROGRAM ::= 
                     ; non-deterministic choice
		     DYNALLOY_PROGRAM "+" DYNALLOY_PROGRAM |

                     ; sequential composition
                     DYNALLOY_PROGRAM ";" DYNALLOY_PROGRAM |

                     ; if-then-else
                     "if" PREDICATE_ID "[" DYNALLOY_EXPRESSIONS "]" "{" DYNALLOY_PROGRAM "}" "else" "{" DYNALLOY_PROGRAM "}"

                     ; while-do
                     "while" PREDICATE_ID "[" DYNALLOY_EXPRESSIONS "]" do "{" DYNALLOY_PROGRAM "}"

                     ; assume
                     "assume" PREDICATE_ID "[" DYNALLOY_EXPRESSIONS "]" |

                     ; variable update
                     VARIABLE_ID ":=" DYNALLOY_EXPRESSION |

                     ; atomic action invokation
                     ACTION_ID "[" DYNALLOY_EXPRESSIONS "]" |

                     ; program invokation
                     "call" PROGRAM_ID "[" DYNALLOY_EXPRESSIONS "]" |

                     ; non-deterministic iteration
                     "repeat" "{" DYNALLOY_PROGRAM "}" |

                     ; do-nothing
                     "skip" |

                     ; non-deterministic iteration (syntactic sugar)
                     DYNALLOY_PROGRAM "*" |

                     ; assume (syntactic sugar)
                     "[" PREDICATE_ID "[" DYNALLOY_EXPRESSIONS "]" "]" "?" |

                     "(" DYNALLOY_PROGRAM ")"