/*************************************************************************
*   Ponder - Managing Distributed Systems
*
*	Author: Ponder Implementation Group, Imperial College
*   Version 2.3 -  June 2001
*
*   Grammar written in SabbleCC
***************************************************************************/

Package ponderToolkit.compiler.syntax;



/****************************************************************************
	HELPERS
*****************************************************************************/

Helpers

	all =				[0 .. 127];
	digit =				['0' .. '9'];
	non_digit =			['_' + [['a' .. 'z'] + ['A' .. 'Z']]];
	u_case =			['A' .. 'Z'];
	l_case = 			['a' .. 'z'];
	letter =			l_case | u_case;
	cr =				13;
	lf =				10;
	tab =				9;
	eol =				cr | lf | cr lf;
	non_eol =			[all - [10 + 13]];
	not_star =			[all - '*'];
	not_quotes = 		[all - '"'];
	not_star_slash =	[not_star - '/'];
	not_brace =			[all - '}'];
	path_seq =  		(non_digit ( digit | non_digit)*);
	l_comment = 		'//' non_eol* eol; /* or eof for that matter */
	c_comment = 		'/*' not_star* '*'+ (not_star_slash not_star* '*'+)* '/';
	not_gt =			[all - '>'];
	spec_chars =		'<<<' (not_gt* (('>'|'>>') not_gt)* not_gt*)+ '>>>';
	digit_seq = 		digit+;
	fractional_seq = 	digit_seq? '.' digit_seq ;
	sign = 				'+' | '-';
	exponent_part = 	('e' | 'E') sign? digit_seq;
	float_seq =  		fractional_seq exponent_part? |	digit_seq exponent_part ;
	integer_seq = 		digit digit*;
	string_seq = 		'"' (not_quotes | '\"')* '"';
	boolean_seq =		'TRUE' | 'FALSE' | 'true' | 'false' ;



/****************************************************************************
	STATES
*****************************************************************************/

States
	normal, 	// default state. When not in an ocl-expression.
	ocl,		// entered when in an ocl-expression
	pre_ocl;	// entered when you are about to enter an ocl-expression



/****************************************************************************
	TOKENS
*****************************************************************************/

Tokens

	/******************************* Keywords *********************************/

	auth_plus = 	'auth+';
	auth_minus = 	'auth-';
	boolean =		'boolean';
	catch = 		'catch';
	deleg_plus = 	'deleg+';
	deleg_minus =	'deleg-';
	do =			'do';
	domain =		'domain';
	extends = 		'extends';
	extern =		'extern';
	grantee =		'grantee';
	group = 		'group';
	hops = 			'hops';
	import =		'import';
	in =			'in';
	int =			'int';
	inst =			'inst';
	meta =			'meta';
	mstruct = 		'mstruct';
	oblig =			'oblig';
	on =			'on';
	out = 			'out';
	real =			'real';
	refrain =		'refrain';
	rel = 			'rel';
	result =		'result';
	role =			'role';
	spec = 			'spec';
	string =		'string';
 	type =			'type';
	user =			'user';
	valid =			'valid';
	when =			'when';

	// the following keywords, if in normal state they take you to pre_ocl state

	{normal->pre_ocl} raises =		'raises';
	{normal->pre_ocl} constraint =	'constraint';

	// the following are recognised only when in normal or pre_ocl state. They are not
	// recognised when in ocl state. That's because in ocl they can be used as identifiers

	{normal, pre_ocl->ocl} subject = 	'subject';
	{normal, pre_ocl->ocl} target =		'target';
	{normal, pre_ocl->ocl} event = 		'event';
	{normal, pre_ocl->ocl} action =		'action';

	// the following keywords are from the OCL Grammar. Not recognised in normal state

	{normal->ocl, pre_ocl, ocl}
	if =			'if';
	then =			'then';
	else =			'else';
	endif =			'endif';
	and = 			'and';
	or =			'or';
	xor =			'xor';
	implies =		'implies';
	not	=			'not';

	// the following keywords are only recognised when in OCL state
	// apart from 'set' which is also a type in Ponder

	 	  set =			'set';
	{ocl} bag =			'bag';
	{ocl} sequence =	'sequence';
	{ocl} collection =	'collection';

	/*********************** Characters and special symbols *******************/

	{normal, pre_ocl->ocl, ocl}
	equals =		'=';
	at_sign = 		'@';
	blank = 		(eol | tab | ' ')+;
	l_par = 		'(';
	r_par =			')';
	{normal, pre_ocl->ocl, ocl->normal}		// if in pre_ocl it takes you to ocl_state
	l_bra = 		'{';					// and if in ocl it takes you to normal
	{normal, pre_ocl, ocl->normal}			// if in ocl it takes you to normal state
	r_bra = 		'}';
	l_brk = 		'[';
	r_brk = 		']';
	dot = 			'.';
	comma = 		',';
	{normal, pre_ocl, ocl->normal}			// if in ocl it takes you to normal state
	semicolon =		';';
	excl_mark =		'!';
	arrow =			'->';
	bar =			'|';
	bar_bar =		'||';
	amper_amper =	'&&';
	caret =			'^';

	//  the following symbols are from OCL Grammar

	not_eq =		'<>';
	lt =			'<';
	lteq =			'<=';
	gt =			'>';
	gteq =			'>=';
	plus =			'+';
	minus = 		'-';
	star =			'*';
	slash = 		'/';
	colon = 		':';
	dot_dot =		'..';

	/***************************** Other useful tokens ************************/

	comment = 		l_comment | c_comment;
	spec_seq =		spec_chars;
	ident =			letter (letter | digit | '_')*;
	abs_path = 		'/.' | ('/' ( path_seq  | (path_seq ('/' path_seq)+) ) ('/' | '/-')? );
	rel_path = 		(('../'|'./') path_seq?) | ('../'|'./')? ((path_seq '/' '-'?) | (path_seq ('/' path_seq)+ ('/' | '/-')?));
	int_value =		integer_seq;
	real_value =	float_seq;
	string_value = 	string_seq;
	boolean_value =	boolean_seq;



Ignored Tokens
	blank,
	comment;



/****************************************************************************
	PRODUCTIONS
*****************************************************************************/

Productions

	// Two kinds of entities can be defined: types and instances.
	// They can be preceded by a general command

	ponder_specification =
		specification*;

	specification =
		{import_or_domain}	import_or_domain |
		{type_or_instance}	type_or_instance ;

	// These are the commands that can be specified outside structures :
	//	- An import statement
	//	- A domain statement that is used to declare the working domain

	import_or_domain =
		{import}	import_statement	|
		{domain}	domain_statement	;

	// A structure can be specified as a type or as an instance.
	// This forces to specify 'type' and 'inst' keyword within a structure e.g. group
	// even if there is an outer definition.

	type_or_instance =
		{type_section}		type type_definition+	|
		{instance_section}	inst inst_declaration+	;


	/**************************************************************************
		Types
	***************************************************************************/

	// These are all the possible structure types that can be specified
	// 	- A Policy type
	// 	- A Grouping structure type
	//	- A Meta-Policy (meta_pol) type

	type_definition =
		{policy}	policy_type		|
		{group}		group_type		|
		{role}		role_type		|
		{rel}		rel_type		|
		{mstruct}	mstruct_type	|
		{meta}		meta_type		;

	// All the (basic/simple) policy types that can be specified
	//	- authorisation
	//	- obligation
	//	- refrain
	//	- delegation

	policy_type =
		{auth_plus}		pos_auth_type	|
		{oblig}			oblig_type		|
		{neg}			neg_pol_type	|	// auth- and refrain
		{deleg}			deleg_type		;


	/**************************************************************************
		Instances
	***************************************************************************/

	inst_declaration =
		{policy} 	policy_inst		|
		{group}		group_inst		|
		{role}		role_inst		|
		{rel}		rel_inst		|
		{mstruct}	mstruct_inst	|
		{meta_pol}	meta_inst		;

	policy_inst =
		{auth_plus}	pos_auth_inst	|
		{oblig}		oblig_inst		|
		{neg}		neg_pol_inst	|	// auth- and refrain
		{deleg}		deleg_inst		;

	// The instantiation Command

	instantiation =
		ident_or_path equals actual_call_decl semicolon;


	/**************************************************************************
		Basic Policies
	***************************************************************************/

	/********************* positive authorisation policy **********************/

	pos_auth_type =
		auth_plus formal_call_decl l_bra pos_auth_type_body* r_bra;

	// The definition of an instance of a positive authorisation can be directly
	// specified or through an instantiation command.
	// The same is true with all the other types of structures

	pos_auth_inst =
		{def}			auth_plus ident_or_path l_bra pos_auth_type_body* r_bra	|
		{instantiation}	auth_plus instantiation+ 								;

	pos_auth_type_body =
		{common}	policy_elements 					|
		{action}	action pos_auth_actions	semicolon	;

	// Positive auth actions can have filters associated with them

	pos_auth_actions =
				pos_auth_action_decl pos_auth_action_tail* 	|
		{all}	star										; 	 // all actions

	// Authorisation actions are separated by commas.

	pos_auth_action_tail =
		comma pos_auth_action_decl;

	// Positive auth actions can have filters associated with them

	pos_auth_action_decl =
		auth_action filter*;

	// For auth, parameters can be omitted from the action eventhough the action
	// may have parameters. This indicates that we don't care about the parameters
	// The action can be prefixed with the name of the object on which the action
	// is called. This must be the target.

	auth_action =
		auth_action_prefix? ident auth_parameters_decl?;

	auth_action_prefix =
		ident_or_path dot;

	// authorisation parameters can only be identifiers (labels/placeholders). If
	// a restriction is to be placed on a parameter of the action, then the identifier
	// can be used in the constraint of the policy and the condition shall be
	// placed there.

	auth_parameters_decl =
		l_par ident_list? r_par;

	ident_list =
		ident ident_list_tail*;

	ident_list_tail =
		comma ident;

	// The specification of the filter for a positive authorisation policy

	filter =
		filter_condition? l_bra filter_body+ r_bra;

	filter_condition =
		if expression;

	filter_body =
		{in}		in		ident 	equals expression semicolon |
		{out}		out		ident 	equals expression semicolon |
		{result}	result			equals expression semicolon ;


	/*************** negative authorisation & refrain policy ******************/

	neg_pol_type =
		neg_sign formal_call_decl l_bra neg_type_body* r_bra;

	neg_pol_inst =
		{def}			neg_sign ident_or_path l_bra neg_type_body* r_bra	|
		{instantiation}	neg_sign instantiation+								;

	neg_type_body =
		{common}	policy_elements 					|
		{action}	action neg_pol_actions	semicolon 	;

	neg_pol_actions =
				auth_action neg_pol_action_tail*	|
		{all}	star								; 	 // all actions

	neg_pol_action_tail =
		comma auth_action;

	neg_sign =
		{auth_minus} auth_minus	|
		{refrain}	 refrain	;


	/*************************** obligation policy ****************************/

	oblig_type =
		oblig formal_call_decl l_bra oblig_type_body* r_bra;

	oblig_inst =
		{def}			oblig ident_or_path l_bra oblig_type_body* r_bra	|
		{instantiation}	oblig instantiation+									;

	oblig_type_body =
		{pol_elememts}	policy_elements_aux semicolon	|
		{common}		common_element_spec				|
						oblig_type_body_aux semicolon	;

	oblig_type_body_aux =
		{event}		event_spec					|
		{action}	do			oblig_actions 	|
		{exception}	catch		exception_spec	;

	// an obligation action consists of sequences of actions separated with
	// concurrency constraints.

	oblig_actions =
		basic_oblig_action next_oblig_action?	;

	next_oblig_action =
		concurrency_op oblig_actions ;

	basic_oblig_action =
		{single}	oblig_action_decl			|
		{parenth}	l_par oblig_actions r_par	;

	oblig_action_decl =
		oblig_action_name l_par actual_parameters? r_par ;

	oblig_action_name =
		object_prefix? ident;

	object_prefix =
		{path}	ident_or_path		dot |
				oblig_action_decl 	dot	;

	// Concurrency operators for obligation actions :
	//	- a1 -> a2	- a1 must follow a2
	//	- a1 | a2	- a1 is performed; if it fails a2 is performed
	//				  otherwise execution stops
	//	- a1 || a2	- a1 and a2 may be performed concurrently.
	//				  Execution continues when either has finished
	//	- a1 && a2	- a1 and a2 may be performed concurrently.
	//				  Execution continues when both have finished

	concurrency_op =
		{seq}		arrow		|
		{or}		bar			|
		{parallel}	bar_bar		|
		{and}		amper_amper	;

	// The specification of events in the body of an obligation policy

	event_spec =
		on event_expr ;

	// An exception is a single action.
	// This can be a script action. An exception "parameter" from the runtime
	// exception system is passed as an argument to the exception action.

	exception_spec =
		ident l_par actual_parameters? r_par;


	/************************** delegation policy *****************************/

	// The heading of a delegation policy type declaration has the following format:
	//	-	deleg+/- <del-name> ([auth+] <auth-policy>) [([<formal-parameters>])]
	// The keyword "auth+" is optional
	// If the policy is deleg+ then constraints on the validity of the actual delegation
	// plus the maximum number of delegation hops can be specified.

	deleg_type =
		{pos}	deleg_plus	deleg_formal_call_decl l_bra deleg_type_body* r_bra |
		{neg}	deleg_minus deleg_formal_call_decl l_bra deleg_type_body* r_bra	;

	deleg_formal_call_decl =
		ident_or_path	[lp1]:l_par auth_plus?	type_ident?	ident [rp1]:r_par
						[lp2]:l_par formal_parameters?	[rp2]:r_par	;

	// Delegation policy instance

	deleg_inst =
		{def}			deleg_inst_def	 	|
		{instantiation}	deleg_instantiation	;

	deleg_inst_def =
		{pos}	deleg_plus 	[id1]:ident_or_path l_par auth_plus?
				[id2]:ident_or_path r_par l_bra deleg_plus_type_body* r_bra |
		{neg}	deleg_minus	[id1]:ident_or_path l_par auth_plus?
				[id2]:ident_or_path r_par l_bra deleg_type_body* r_bra 		;

	// The delegation policy instantiation statement
	// The authorisation policies from which to delegate must be specified
	// before the rest of the parameters

	deleg_instantiation =
		{pos}	deleg_plus	deleg_actual_call_decl+	|
		{neg}	deleg_minus	deleg_actual_call_decl+	;

	deleg_actual_call_decl =
		[id1]:ident_or_path equals [id2]:ident_or_path deleg_actual_params semicolon;

	deleg_actual_params =	[lp1]:l_par ident_or_path		[rp1]:r_par
							[lp2]:l_par actual_parameters?	[rp2]:r_par	;

	// The delegation policy should still allow the specification of a target
	// to override the target of the authorisation policies. So, a separate "grantee"
	// entry should be there.

	deleg_type_body =
		{common}			policy_elements								  		|
		{grantee}			grantee	set_type?			subj_target semicolon 	|
		{access_rights}		action	deleg_access_rights	semicolon 				;

	// The body of a positive delegation policy also allows the specification of the
	// valid-clause to indicate delegation constraints.

	deleg_plus_type_body =
				deleg_type_body								|
		{valid}	valid 			constraint_spec semicolon	|
		{hops}	hops			deleg_hops					;

	// The access rights to be delegated.
	// These are just like actions of a negative authorisation policy (no filters)

	deleg_access_rights =
		neg_pol_actions;

	// If the policy is deleg+ then the maximum number of delegation hobs can
	// be specified. This must be an integer value

	deleg_hops =
		{ident}		ident 		|
		{int_value}	int_value	;


	/****************** common basic-policy body contents *********************/

	// Common single-policy body contents.
	// Individual policies can also contain the definition of common elements like
	// constants, constraints.
	// Obligation policies can also contain event declarations.
	// Each command must be separated by a semicolon.

	policy_elements =
						policy_elements_aux 		semicolon 	|
		{common_elem}	basic_common_element_spec				;

	policy_elements_aux =
		{subject}		subject	set_type? 	subj_target		|
		{target}		target 	set_type?	subj_target		|
		{constraint}	when				constraint_spec	;

	// A subject is a domain-scope-expression, and can be assigned to a name

	subj_target =
		{dse}	subj_target_name?	domain_scope_expr ;

	subj_target_name =
		ident equals;


	/**************************************************************************
		Composite Policies
	***************************************************************************/

	/******************************* group ************************************/

	group_type =
		group comp_type_formal_call_decl l_bra group_body* r_bra ;

	group_inst =
		{def}			group ident_or_path l_bra group_body* r_bra	|
		{instantiation}	group instantiation+						;

	group_body =
		{common}	comp_pol_body 	 |
		{nesting}	comp_nested_elem ;


	/******************************* role *************************************/

	role_type =
		role comp_type_formal_call_decl l_bra role_body* r_bra ;

	role_inst =
		{def}			role ident_or_path l_bra role_body* r_bra subject_domain? 	|
		{instantiation}	role role_instantiation+ 		 							;

	role_body =
		{common}	comp_pol_body    |
		{nesting}	comp_nested_elem ;

	role_instantiation =
		ident_or_path equals actual_call_decl subject_domain? semicolon;

	subject_domain =
		at_sign ident_or_path;


	/**************************** relationship ********************************/

	// A relationship can contain nested role types and instances in addition to
	// those that it may contain as a composite-policy sub-type.

	rel_type =
		rel comp_type_formal_call_decl l_bra rel_body* r_bra ;

	rel_inst =
		{def}			rel ident_or_path l_bra rel_body* r_bra	|
		{instantiation}	rel instantiation+						;

	rel_body =
		{common}	comp_pol_body 	|
		{nesting}	rel_nested_elem	;

	rel_nested_elem =
		{type} type rel_type_nested_elem+	|
		{inst} inst rel_inst_nested_elem+	;

	rel_type_nested_elem =
		{common} comp_type_nested_elem 	|
		{role}	 role_type 				;

	rel_inst_nested_elem =
		{common} comp_inst_nested_elem	|
		{role}	 role_inst 				;


	/*********************** management structure ******************************/

	// A management structure can contain nested role and relationship types and
	// instances in addition to those that it may contain as a composite-policy
	// sub-type.

	mstruct_type =
		mstruct comp_type_formal_call_decl l_bra mstruct_body* r_bra;

	mstruct_inst =
		{def}			mstruct ident_or_path l_bra mstruct_body* r_bra	|
		{instantiation}	mstruct instantiation+							;

	mstruct_body =
		{common}	comp_pol_body 		|
		{nesting}	mstruct_nested_elem	;

	mstruct_nested_elem =
		{type} type mstruct_type_nested_elem+ |
		{inst} inst mstruct_inst_nested_elem+ ;

	mstruct_type_nested_elem =
		{common}	comp_type_nested_elem  	|
		{role} 		role_type				|
		{rel} 		rel_type				|
		{mstruct} 	mstruct_type			;

	mstruct_inst_nested_elem =
		{common}	comp_inst_nested_elem  	|
		{role} 		role_inst				|
		{rel} 		rel_inst				|
		{mstruct} 	mstruct_inst			;


	/************ Common body contents for composite policies ******************/

	// All composite policty structures can contain nested basic policies, groups
	// and meta-policies.

	comp_pol_body =
		common_element_spec	;

	comp_nested_elem =
		{type} type comp_type_nested_elem+ |
		{inst} inst comp_inst_nested_elem+ ;

	comp_type_nested_elem =
		comp_type_nested_elem_aux ;

	comp_type_nested_elem_aux =
		{group} 	group_type	|
		{policy} 	policy_type	|
		{meta} 		meta_type	;

	comp_inst_nested_elem =
		comp_inst_nested_elem_aux ;

	comp_inst_nested_elem_aux =
		{group} 	group_inst	|
		{policy} 	policy_inst	|
		{meta} 		meta_inst	;


	/**************************************************************************
		Meta-Policies
	***************************************************************************/

	// The meta policy: "meta" ident (<formal-parameters>) "raises" action
	// The raises clause is ommitted if the meta policy contains only concurrency
	// constraints

	meta_type =
						meta formal_call_decl raises action_call l_bra meta_body r_bra 	|
		{concurrency}	meta formal_call_decl l_bra meta_body_conc r_bra				;

	meta_body =
		meta_expression next_meta_expression* semicolon ;

	meta_expression =
					expression							|
		{assign}	l_brk ident r_brk equals expression ;

	next_meta_expression =
		semicolon meta_expression;

	meta_inst =
		{def}			meta ident_or_path raises action_call l_bra meta_body r_bra	|
		{def_conc}		meta ident_or_path l_bra meta_body_conc r_bra				|
		{instantiation}	meta instantiation+											;

	meta_body_conc =
		  concurrency_expression next_concurrency_expression* semicolon ;

	next_concurrency_expression =
		semicolon concurrency_expression ;

	// a concurrency expression consists of sequences of activities separated with
	// concurrency constraints.

	concurrency_expression =
		activity next_activity?	;

	next_activity =
		concurrency_op concurrency_expression ;

	activity =
		{single}	activity_decl						|
		{parenth}	l_par concurrency_expression r_par	;

	activity_decl =
		activity_prefix? next_activity_prefix* ident ;

	activity_prefix =
		path dot ;

	next_activity_prefix =
		ident dot ;


	/**************************************************************************
		Parameters
	***************************************************************************/

	/************************** formal parameters *****************************/

	// The formal parameters call declaration used in the definition of types
	// The name can be a path instead of an identifier, if there is a need to
	// specify the domain where the definition should go. Composite types can also
	// include an extends-clause for inheritance.

	formal_call_decl =
		ident_or_path	l_par formal_parameters? r_par	;

	comp_type_formal_call_decl =
		formal_call_decl extends_type? ;

	formal_parameters =
		formal_param formal_param_tail* ;

	formal_param_tail =
		comma formal_param;

	// The type of the parameter can be ommited indicating a "don't care" situation
	// With this, we can use formal parameters for event-expressions too

	formal_param =
		type_decl? ident;

	// All the possible types that can be specified/declared.
	// For user-defined types, the name of the type can be specified optionally

	type_decl =
		{int}			int							|
		{real}			real						|
		{string}		string						|
		{boolean}		boolean						|
		{domain}		domain						|
		{set}			set 	set_type?		 	|
		{subject}		subject	set_type?			|
		{target}		target	set_type?			|
		{grantee}		grantee	set_type?			|
		{event}			event						|
		{action}		action						|
		{constraint}	constraint					|
		{auth_plus}		auth_plus					|
		{auth_minus}	auth_minus					|
		{oblig}			oblig						|
		{refrain}		refrain						|
		{deleg_plus}	deleg_plus					|
		{deleg_minus}	deleg_minus					|
		{role}			role						|
		{rel}			rel							|
		{group}			group						|
		{mstruct}		mstruct						|
		{meta}			meta						|
		{type_ident}	type_qualifier? type_ident	; // any type

	type_ident =
		ident_or_path;

	type_qualifier =
		{user_defined}	user 	|	// a user-defined (policy) type
		{extern}		extern	;	// an external (IDL) type

	set_type =
		lt ident gt;

	// The type to be extended can also be specified as a path
	// The syntax of the extends clause is the same as that of the actual_call_decl

	extends_type =
		extends extends_clause next_extends_clause* ;

	extends_clause =
		{with_params}	actual_call_decl	|
		{path}			ident_or_path		;

	next_extends_clause =
		comma extends_clause ;



	/************************** actual parameters *****************************/

	// The actual parameters call declaration used in the definition of instances
	// The name can be a path instead of an identifier, if there is a need to
	// specify the domain where the definition should go.

	actual_call_decl =
		ident_or_path	l_par actual_parameters? r_par	;

	actual_parameters =
		actual_param actual_param_tail*;

	actual_param  =
		{expr}	expression						|
		{dse}	l_brk domain_scope_expr	r_brk	;

	actual_param_tail =
		comma actual_param;


	/**************************************************************************
		Common Elements Specification
	***************************************************************************/

	// Common Elements can be defined within any of the defined structures (types
	// or instances). Common elements that can be specified are:
	//		- Events
	//		- Constraints
	//		- Constants (int, real, string, boolean etc)
	//		- Domains
	// Basic Common Elements are those that can be specified in Authorisation,
	// Delegation and Refrain policies - Events make no sense in those policies

	basic_common_element_spec =
		{constraint}		constraint		constraint_def+	|
		{spec}				spec			external_spec+ 	|
		{constant}			constant_def 					|
		{import_or_domain}	import_or_domain				;

	common_element_spec =
		{basic}	basic_common_element_spec	|
		{event}	event	event_def+			;


	/*************************** event definition *****************************/
	// The definition of an event.
	// e.g. circuitFailure(h,x,y) = envAlarm(h) -> rFailure(x,y)
	
	event_def =
		ident event_params? equals event_expr semicolon ;

	// An Event expression is:
	//	- basic event
	//	- e1 && e2	- occurs when both e1 and e2 occur irrespective of their order
	//	- e1 | e2	- occurs when e1 or e2 occurs
	//	- e1 -> e2	- occurs when e1 occurs before e2
	//	- e1 + time - occurs a specified period of time after e1 occurs
	//	- {e1 ; e2} ! e3 -	occurs when e1 occurs followed by e2 with no interleaving
	//						of e3
	//  - n * e     - occurs when e occurs n times

	event_expr =
		{basic}		basic_event 											|
		{next}		basic_event next_event 									|
		{multiple}	int_value star event_expr								|
		{no_inter}	l_bra [e1]:event_expr semicolon	[e2]:event_expr	r_bra
					excl_mark [e3]:event_expr								;

	next_event =
		{op}	event_op event_expr	|
		{time}	plus int_value		;

	event_op =
		{amper}	amper_amper	|
		{bar}	bar			|
		{arrow}	arrow		;

	// A basic event is:
	//		- the name of the event with any optional parameters: eventName ['(' ... ')']
	//		- a method call on the timer object to specify a time event
	//		- an arbitrary expression enclosed within brackets.

	basic_event =
		{parenth}	l_par	event_expr	r_par		|
		{ident}		ident	auth_parameters_decl?	|	// same as authorisation-parameters: list of idents
		{timer}		ident 	dot action_call			|
		{expr}		l_brk 	expression	r_brk		;

	event_params =
		l_par formal_parameters? r_par;


	/************************ constraint definition ***************************/

	constraint_def =
		ident constraint_params? equals constraint_spec	semicolon ;

	constraint_params =
		l_par formal_parameters? r_par;

	constraint_spec = expression;


	/************************ constants definition ****************************/

	constant_def =
		constant_def_aux ;

	constant_def_aux =
		{int}			int					basic_const_assign+ 	|
		{real}			real				basic_const_assign+		|
		{string}		string				basic_const_assign+		|
		{boolean}		boolean				basic_const_assign+		|
		{set}			set	set_type?		set_const_assign+		|
		{extern_type}	extern type_ident	type_const_assign+		|	// an IDL type
		{user_type}		user   type_ident	type_const_assign+		;	// a user-defined type

	basic_const_assign =
		ident equals expression semicolon;

	set_const_assign =
		ident equals domain_scope_expr semicolon;

	type_const_assign =
		ident equals expression semicolon;


	/************************ external specification **************************/

	// A specification that is external to Ponder.

	external_spec =
		ident spec_seq semicolon ;


	/**************************************************************************
		Import and Domain Statements
	***************************************************************************/

	// An Import statement can end with a "/-" meaning, import all, from the
	// specified domain path

	import_statement =
		import import_path+ ;

	import_path =
		{path}	path 	semicolon	|
		{ident}	ident	semicolon	;


	domain_statement =
		domain domain_statement_body+ ;

	domain_statement_body =
		{var_decl}		ident equals path		semicolon |
		{decl}			path					semicolon |
		{lib_action}	ident dot action_call	semicolon ;


	/**************************************************************************
		Expressions
	***************************************************************************/

	/********************** domain scope expressions **************************/

	domain_scope_expr =
		{basic}		basic_domain_scope_expr							|
		{composite}	basic_domain_scope_expr next_domain_scope_expr	;

	next_domain_scope_expr =
		domain_op domain_scope_expr	;

	basic_domain_scope_expr =
		{domain_object}	domain_object 						|
		{single_obj}	l_bra	domain_object	r_bra		|
		{star}			star	int_value?	domain_object	|
		{at_sign}		at_sign	int_value?	domain_object	|
		{par}			l_par domain_scope_expr r_par		;

	domain_op =
		{plus}		plus	|
		{minus}		minus	|
		{intersect}	caret	;

	domain_object =
		ident_or_path next_domain_object*;

	next_domain_object =
		{obj_attr} 		dot 	object_attr 	|
		{action_call}	dot 	action_call 	| 	// for domain library objects
		{arrow}			arrow	feature_call	;

	object_attr =
		{subject}	subject	|
		{target}	target	;

	ident_or_path =
		{ident}	ident	|
		{path}	path	;

	path =
		{abs} abs_path	|
		{rel} rel_path	;


	/****************************** expressions *******************************/

	// Expressions in Ponder Follow the OCL Syntax (version 1.3)

	expression =
		logical_expression;

	if_expression =
		if [if_branch]:expression then [then_branch]:expression
		else [else_branch]:expression endif ;

	logical_expression =
		relational_expression next_logical_expression* ;

	next_logical_expression =
		logical_operator relational_expression ;

	relational_expression =
		add_expression next_relational_expression? ;

	next_relational_expression =
		relational_operator add_expression ;

	add_expression =
		mult_expression next_add_expression* ;

	next_add_expression =
		add_operator mult_expression ;

	mult_expression =
		unary_expression next_mult_expression* ;

	next_mult_expression =
		mult_operator unary_expression ;

	unary_expression =
		{unary} unary_operator postfix_expression |
		{postfix} postfix_expression ;

	postfix_expression =
		primary_expression next_postfix_expression* ;

	next_postfix_expression =
		{action_call}	dot		action_call		|
		{arrow}			arrow	feature_call	;

	primary_expression =
		{lit_col} 	literal_collection 		|
		{literal}	literal 				|
		{action}	action_call				|
		{parenth} 	l_par expression r_par 	|
		{if} 		if_expression 			;

	feature_call_parameters =
		l_par declarator? expression r_par ;

	literal =
		{path}		path			|			// added. Not part of OCL grammar.
		{string}	string_value 	|
		{real}		real_value		|
		{int}		int_value		|
		{boolean} 	boolean_value	|
		{subject}	subject			|
		{target}	target			;

	simple_type_specifier =
		ident_or_path ;

	literal_collection =
		collection_kind l_bra expression_list_or_range? r_bra ;

	expression_list_or_range =
		expression expression_list_or_range_tail? ;

	expression_list_or_range_tail =
		{list} 	expression_list_tail+ 	|
		{range} dot_dot expression 		;

	expression_list_tail =
		comma expression ;

	feature_call =
		ident qualifiers? feature_call_parameters? 	;

	action_call =
		ident	action_call_params? ;

	action_call_params =
		l_par actual_parameters? r_par ;

	qualifiers =
		l_brk actual_parameter_list r_brk ;

	// "iterate" alternative added (missing in ocl specification)

	declarator =
		{standard} ident declarator_tail* declarator_type_declaration? bar |
		{iterate} [iterator]:ident [iter_type]:declarator_type_declaration
					semicolon [accumulator]:ident
					[acc_type]:declarator_type_declaration equals expression bar;

	declarator_tail =
		comma ident ;

	declarator_type_declaration =
		colon simple_type_specifier ;

	actual_parameter_list =
		expression actual_parameter_list_tail* ;

	actual_parameter_list_tail =
		comma expression ;

	logical_operator =
		{and} 		and 	|
		{or} 		or 		|
		{xor} 		xor 	|
		{implies} 	implies	;

	collection_kind =
		{set} 			set 		|
		{bag} 			bag 		|
		{sequence} 		sequence 	|
		{collection} 	collection 	;

	relational_operator =
		{equals} 	equals	|
		{not_eq} 	not_eq 	|
		{gt} 		gt 		|
		{lt} 		lt 		|
		{gteq} 		gteq 	|
		{lteq} 		lteq 	;

	add_operator =
		{plus} 	plus 	|
		{minus} minus	;

	mult_operator =
		{mult} 	star 	|
		{div} 	slash	;

	unary_operator =
		{minus} minus 	|
		{not} 	not		;


/******************************     END    **********************************/