Commit ec450e6c authored by Luca Cristoforetti's avatar Luca Cristoforetti
Browse files

Update OCRA grammar to support behaviours and add test files

parent 8d708cf4
COMPONENT system
INTERFACE
INPUT PORT inp : boolean;
INPUT PORT ev : event;
PARAMETER k : real;
CONTRACT foo
assume: true;
guarantee: G inp or in the future inp or (!inp U X inp);
REFINEMENT
SUB t : Test;
INIT fall(inp);
CONTRACT foo REFINEDBY t.a;
COMPONENT Test
INTERFACE
CONTRACT a
assume: true;
guarantee: true;
COMPONENT system
INTERFACE
INPUT PORT inp : boolean;
INPUT PORT ev : event;
PARAMETER k : real;
CONTRACT foo
assume: true;
guarantee: G inp or in the future inp or (!inp U X inp);
REFINEMENT
SUB t : Test;
INVAR fall(inp);
CONTRACT foo REFINEDBY t.a;
COMPONENT Test
INTERFACE
CONTRACT a
assume: true;
guarantee: true;
COMPONENT system
INTERFACE
INPUT PORT inp : boolean;
INPUT PORT ev : event;
PARAMETER k : real;
CONTRACT foo
assume: true;
guarantee: G inp or in the future inp or (!inp U X inp);
REFINEMENT
SUB t : Test;
TRANS inp or next(inp);
CONTRACT foo REFINEDBY t.a;
COMPONENT Test
INTERFACE
CONTRACT a
assume: true;
guarantee: true;
COMPONENT system
INTERFACE
INPUT PORT inp : boolean;
INPUT PORT ev : event;
PARAMETER k : real;
CONTRACT foo
assume: true;
guarantee: G inp or in the future inp or (!inp U X inp);
REFINEMENT
SUB t : Test;
VAR test : boolean;
CONTRACT foo REFINEDBY t.a;
COMPONENT Test
INTERFACE
CONTRACT a
assume: true;
guarantee: true;
COMPONENT system
INTERFACE
INPUT PORT inp : boolean;
INPUT PORT ev : event;
PARAMETER k : real;
CONTRACT foo
assume: true;
guarantee: G inp or in the future inp or (!inp U X inp);
REFINEMENT
SUB t : Test;
URGENT inp or next(inp);
CONTRACT foo REFINEDBY t.a;
URGENT fall(inp);
COMPONENT Test
INTERFACE
CONTRACT a
assume: true;
guarantee: true;
......@@ -53,7 +53,8 @@ RefinementInstance:
refinedby=RefinedBy |
formula=FormulaConstraint |
prop=ValidProp |
assertion=Assertion;
assertion=Assertion |
behaviour=Behaviour;
Variable:
(Port | Parameter | Operation);
......@@ -93,6 +94,13 @@ Assertion:
ParameterAssumptions:
'PARAMETER' 'ASSUMPTIONS' constraint=Expression SEMICOLON;
Behaviour:
'INIT' constraint=Expression SEMICOLON |
'VAR' name=ID COLON type=SimpleType SEMICOLON |
'INVAR' constraint=Expression SEMICOLON |
'TRANS' constraint=Expression SEMICOLON |
'URGENT' constraint=Expression SEMICOLON;
Connection:
('CONNECTION' | 'DEFINE') variable=(FullPortId | FullParameterId ) AssignementOp constraint=Expression
(iterativeCondition=IterativeCondition)? SEMICOLON;
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment