org.eclipse.opencert.sam.agree/src/org/eclipse/opencert/sam/agree/Agreement.xtext

grammar org.eclipse.opencert.sam.agree.Agreement with org.eclipse.xtext.common.Terminals

generate agreement "http://www.opencert.org/sam/agree/Agreement"

Model:
	contracts+=Contract*;
	
Contract:
	'Agreement' name=ID  
	'modules:' (mod+=ID)*
	'premises:' '{'(code+=ID assertion+=assertionDefinition)*'}'
	'promises:' '{'(code+=ID guarantee+=assertionDefinition)*'}'
	'reasoning:' '{'(strategy+=strategyDefinition)*'}'
;
assertionDefinition:
	assertion+= viewpointId* 'for' p+=assertionpattern
;


strategyDefinition:
	strategy+=STRING
;
viewpointId:
	view= 'viewpoint' '<' (view1+=viewId|view3+=ID)* '>' 
;
enum viewId:
	inst='installation' | saf='safety' | func='functionality' | per='performance' | tim='timing'  
;


 assertionpattern :
	assertionpattern= Noun v=Verb f=Fact
	| 'viewpoint' '<'view+=viewpointId*'>' 'for' pattern=Pattern
;



Noun :
	noun=STRING
;
Verb :
	verb= (part1) v=simple 
;

simple:
	verb=STRING
;
part1:
	("is" | "are" | "has" | "have")*
;

Fact :
	fact=STRING
;

Pattern:
(premise=  nonfunctional 
		|behave
		|'whenever' '[' Event=ID ']'

)
;


nonfunctional:
	nonfunctional+= memory | timming
;
memory:
	memory=	'Parameter 'par=ID ' is defined by' def=ID ' with range' range=STRING | 
			'memory type is' type=ID | 
			'Partition' part=ID 'respects ' constrain=ID 
;
timming:
	time=	'WCET is'value=INT' units are' unit=ID 'is determined by method' method=STRING |
			'BCET is'value=INT' units are' unit=ID 'is determined by method' method=STRING
;

behave:
	behave = STRING
;