Symboleo is a formal language used to specify legal contracts.
Here is Symboleo's syntax in Xtext format:

grammar ca.uottawa.csmlab.symboleo.Symboleo with org.eclipse.xtext.common.Terminals

generate symboleo "http://www.uottawa.ca/csmlab/symboleo/Symboleo"
import "http://www.eclipse.org/emf/2002/Ecore" as ecore

Model:
	'Domain' domainName=ID
	(domainTypes+=DomainType ';')+
	'endDomain'
	('TimeGranularity' 'is' timeUnits=TimeUnit)?
	'Contract' contractName=ID '(' (parameters+=Parameter ',')+ (parameters+=Parameter) ')'
	('Declarations' (variables+=Variable ';')*)?
	('Preconditions' (preconditions+=Proposition ';')*)?
	('Postconditions' (postconditions+=Proposition ';')*)?
	('Obligations' (obligations+=Obligation ';')*)+
	('Surviving' 'Obligations' (survivingObligations+=Obligation ';')*)?
	('Powers' (powers+=Power ';')*)?
	('Constraints' (constraints+=Proposition ';')*)?
	'endContract';

DomainType:
	Alias | RegularType | Enumeration;

Alias:
	name=ID 'isA' type=BaseType;

Enumeration:
	name=ID 'isAn' 'Enumeration' '(' (enumerationItems+=EnumItem ',')* (enumerationItems+=EnumItem) ')';

EnumItem:
	name=ID;


RegularType:
	name=ID ('isA' | 'isAn') ontologyType=OntologyType ('with' (attributes+=Attribute ',')* (attributes+=Attribute))? |
	name=ID ('isA' | 'isAn') regularType=[RegularType] ('with' (attributes+=Attribute ',')* (attributes+=Attribute))?;

Attribute:
	attributeModifier=AttributeModifier? name=ID ':' baseType=BaseType |
	attributeModifier=AttributeModifier? name=ID ':' domainType=[DomainType];

BaseType:
	name=("Number" | "String" | "Date" | "Boolean");

OntologyType:
	name=("Asset" | "Event" | "Role" | "Contract");

AttributeModifier:
	name=('Env');

Parameter:
	name=ID ':' type=ParameterType;

ParameterType:
	baseType=BaseType |
	domainType=[DomainType];

Variable:
	name=ID ':' type=[RegularType] ('with' attributes+=Assignment (',' attributes+=Assignment)*)?;


OAssignment:
	{OAssignExpression} name2= VariableDotExpression op=":=" (value=Expression);
	
VariableDotExpression returns Ref:
	VariableRef ({VariableDotExpression.ref=current} "." tail=[Attribute])*;

VariableRef returns Ref:
	{VariableRef} variable=ID;

Assignment:
	{AssignExpression} name=ID ':=' value=Expression;

Double returns ecore::EDouble:
	INT '.' INT;

Date returns ecore::EDate:
  'Date' '(' STRING ')';

Expression: Or;

Or returns Expression:
	And ({Or.left=current} "or" right=And)*;

And returns Expression:
	Equality ({And.left=current} "and" right=Equality)*;

Equality returns Expression:
	Comparison ({Equality.left=current} op=("==" | "!=") right=Comparison)*;

Comparison returns Expression:
	Addition ({Comparison.left=current} op=(">=" | "<=" | ">" | "<") right=Addition)*;

Addition returns Expression:
	Multiplication (({Plus.left=current} '+' | {Minus.left=current} '-') right=Multiplication)*;

Multiplication returns Expression:
	PrimaryExpression (({Multi.left=current} '*' | {Div.left=current} '/') right=PrimaryExpression)*;

PrimaryExpression returns Expression:
	{PrimaryExpressionRecursive} '(' inner=Expression ')' |
	{PrimaryExpressionFunctionCall} function=FunctionCall |
	{NegatedPrimaryExpression} "not" expression=PrimaryExpression |
	AtomicExpression
;

AtomicExpression returns Expression:
	{AtomicExpressionTrue} value="true" |
	{AtomicExpressionFalse} value="false" |
	{AtomicExpressionDouble} value=Double |
	{AtomicExpressionInt} value=INT |
	{AtomicExpressionDate} value= Date |
	{AtomicExpressionEnum} enumeration=[Enumeration]"("enumItem=[EnumItem]")" |
	{AtomicExpressionString} value=STRING |
	{AtomicExpressionParameter} value=VariableDotExpression
;

FunctionCall:
	MathFunction | StringFunction | DateFunction
;
MathFunction returns FunctionCall:
  {TwoArgMathFunction} name=('Math.pow') '(' arg1=Expression ',' arg2=Expression ')' |
  {OneArgMathFunction} name=('Math.abs'|'Math.floor'|'Math.cbrt'
    |'Math.ceil'|'Math.exp'|'Math.sign'|'Math.sqrt'
  ) '(' arg1=Expression ')';

StringFunction returns FunctionCall:
  {ThreeArgStringFunction} name=('String.substring'|'String.replaceAll') '(' arg1=Expression ',' arg2=Expression ',' arg3=Expression ')' |
  {TwoArgStringFunction} name=('String.concat') '(' arg1=Expression ',' arg2=Expression ')' |
  {OneArgStringFunction} name=('String.toLowerCase'|'String.toUpperCase'|'String.trimEnd'|'String.trimStart'|'String.trim') '(' arg1=Expression ')';
	
DateFunction returns FunctionCall:
	{ThreeArgDateFunction} name='Date.add' '(' arg1=Expression ',' value=Expression ',' timeUnit=TimeUnit  ')' 
;

Obligation:
	name=ID ':' (trigger=Proposition '->')? ('O' | 'Obligation') '(' debtor=VariableDotExpression ',' creditor=VariableDotExpression ',' antecedent=Proposition ',' consequent=Proposition ')';

Power:
	name=ID ':' (trigger=Proposition '->')? ('P' | 'Power') '(' creditor=VariableDotExpression ',' debtor=VariableDotExpression ',' antecedent=Proposition ',' consequent=PowerFunction ')';
	
PowerFunction returns PowerFunction:
	{PFObligationSuspended} action = 'Suspended' '(' 'obligations.' norm = [Obligation] ')' | 
	{PFObligationResumed} action = 'Resumed' '(' 'obligations.' norm = [Obligation] ')' | 
	{PFObligationDischarged} action = 'Discharged' '(' 'obligations.' norm = [Obligation] ')' |
	{PFObligationTerminated} action = 'Terminated' '(' 'obligations.' norm = [Obligation] ')' |
	{PFObligationTriggered} action = 'Triggered' '(' 'obligations.' norm = [Obligation] ')' |
	//{PFPowerSuspended} action = 'Suspended_' '(' norm = [Power] ')' | 
	//{PFPowerResumed} action = 'Resumed_' '(' norm = [Power] ')' | 
	//{PFPowerTerminated} action = 'Terminated_' '(' norm = [Power] ')' |
	{PFContractSuspended} action = 'Suspended' '(' norm = 'self' ')' | 
	{PFContractResumed} action = 'Resumed' '(' norm = 'self' ')' |
	{PFContractTerminated} action = 'Terminated' '(' norm = 'self' ')';

Proposition: POr;

POr returns Proposition:
	PAnd ({POr.left=current} "or" right=PAnd)*;

PAnd returns Proposition:
	PEquality ({PAnd.left=current} "and" right=PEquality)*;

PEquality returns Proposition:
	PComparison ({PEquality.left=current} op=("==" | "!=") right=PComparison)*;

PComparison returns Proposition:
	PAtomicExpression ({PComparison.left=current} op=(">=" | "<=" | ">" | "<") right=PAtomicExpression)*;

PAtomicExpression returns Proposition:
	{PAtomRecursive} '(' inner=Proposition ')' |
	{NegatedPAtom} 'not' negated=PAtomicExpression |
	{PAtomPredicate} predicateFunction=PredicateFunction |
	{PAtomFunction} function=OtherFunction |
  {PAtomEnum} enumeration=[Enumeration]"("enumItem=[EnumItem]")" |
	{PAtomVariable} variable=VariableDotExpression |
	{PAtomPredicateTrueLiteral} value='true' |
	{PAtomPredicateFalseLiteral} value='false' |
	{PAtomDoubleLiteral} value=Double |
	{PAtomIntLiteral} value=INT |
	{PAtomStringLiteral} value=STRING |
	{PAtomDateLiteral} value= Date
	;

PredicateFunction:
	{PredicateFunctionHappens} name='Happens' '(' event=Event ')' |
	{PredicateFunctionWHappensBefore} name='WhappensBefore' '(' event=Event ',' point=Point ')' |
	{PredicateFunctionSHappensBefore} name='ShappensBefore' '(' event=Event ',' point=Point ')' |
	{PredicateFunctionHappensWithin} name='HappensWithin' '(' event=Event ',' interval=Interval ')'|
	{PredicateFunctionWHappensBeforeEvent} name='WhappensBeforeE' '(' event1=Event ',' event2=Event ')' |
	{PredicateFunctionSHappensBeforeEvent} name='ShappensBeforeE' '(' event1=Event ',' event2=Event ')' |
	{PredicateFunctionHappensAfter} name='HappensAfter' '(' event=Event ',' point=Point ')' |
	{PredicateFunctionOccurs} name='Occurs' '(' situation=Situation ',' interval=Interval ')' |
	{PredicateFunctionAssignment} name='HappensAssign' '(' event=Event ',' (assignment+=OAssignment (';' assignment+=OAssignment )*)?')' |
	{PredicateFunctionAssignmentOnly} name='Assign' '(' (assignment+=OAssignment (';' assignment+=OAssignment )*)?')'
		;                                              //('with' attributes+=Assignment (',' attributes+=Assignment)*)?;
	//{PredicateFunctionAssignmentOnly} name='Assign' '(' (assignment+=OAssignment)* (';' assignment+=OAssignment )?')'
OtherFunction:
  {PredicateFunctionIsEqual} name='IsEqual' '(' arg1=ID ',' arg2=ID ')' |
  {PredicateFunctionIsOwner} name='IsOwner' '(' arg1=ID ',' arg2=ID ')' |
  {PredicateFunctionCannotBeAssigned} name='CannotBeAssigned' '(' arg1=ID ')'
  ;
  
Event:
	VariableEvent |
	ObligationEvent |
	ContractEvent |
	PowerEvent;
	

	
VariableEvent returns Event:
	{VariableEvent} variable=VariableDotExpression
;

PowerEvent returns Event:
	{PowerEvent} eventName=PowerEventName '(' 'powers.' powerVariable=[Power] ')';

PowerEventName:
	'Triggered' | 'Activated' | 'Suspended' | 'Resumed' | 'Exerted' | 'Expired' | 'Terminated';

ObligationEvent returns Event:
	{ObligationEvent} eventName=ObligationEventName '(' 'obligations.' obligationVariable=[Obligation] ')';

ObligationEventName:
	'Triggered' | 'Activated' | 'Suspended' | 'Resumed' | 'Discharged' | 'Expired' | 'Fulfilled' | 'Violated' | 'Terminated';

ContractEvent returns Event:
	{ContractEvent} eventName=ContractEventName '(' 'self' ')';

ContractEventName:
	'Activated' | 'Suspended' | 'Resumed' | 'FulfilledObligations' | 'RevokedParty' | 'AssignedParty' | 'Terminated' | 'Rescinded';

Point:
	pointExpression=PointExpression;

PointExpression:
	PointFunction |
	PointAtom;

PointFunction returns PointExpression:
	{PointFunction} name=PointFunctionName '(' arg=PointExpression ',' value=Timevalue ',' timeUnit=TimeUnit ')';

PointFunctionName:
	'Date.add';

PointAtom returns PointExpression:
	{PointAtomParameterDotExpression} variable=VariableDotExpression | 
	{PointAtomObligationEvent} obligationEvent=ObligationEvent |
	{PointAtomContractEvent} contractEvent=ContractEvent |
	{PointAtomPowerEvent} powerEvent=PowerEvent;


Timevalue:
	{TimevalueInt} value=INT |
	{TimevalueVariable} variable=VariableDotExpression
;

TimeUnit:
	'seconds' | 'minutes' | 'hours' | 'days' | 'weeks' | 'months' | 'years';

Interval:
	intervalExpression=IntervalExpression;

IntervalExpression:
	{IntervalFunction} 'Interval' '(' arg1=PointExpression ',' arg2=PointExpression ')' |
	{SituationExpression} situation=Situation;

Situation:
	ObligationState |
	ContractState |
	PowerState;

PowerState:
	stateName=PowerStateName '(' 'powers.' powerVariable=[Power] ')';

PowerStateName:
	'Create' | 'UnsuccessfulTermination' | 'Active' | 'InEffect' | 'Suspension' | 'SuccessfulTermination';

ObligationState:
	stateName=ObligationStateName '(' 'obligations.' obligationVariable=[Obligation] ')';

ObligationStateName:
	'Create' | 'Discharge' | 'Active' | 'InEffect' | 'Suspension' | 'Violation' | 'Fulfillment' | 'UnsuccessfulTermination';

ContractState:
	stateName=ContractStateName '(' 'self' ')';

ContractStateName:
	'Form' | 'UnAssign' | 'InEffect' | 'Suspension' | 'Rescission' | 'SuccessfulTermination' | 'UnsuccessfulTermination' | 'Active';

Also, please note that in Symboleo: 
- Obligations have the format "Oid: [trigger ->] O(debtor, creditor, antecedent, consequent)" where creditor and debtor are roles whereas the trigger, antecedent, and consequent are legal situations defined by propositions.
- Surviving obligations are the obligations that remain in effect after the termination of a contract.
- Powers are specified as "Pid: [trigger ->] P(creditor, debtor, antecedent, consequent)" are used to create, change or terminate an obligation or another power.

Regarding Symboleo's semantics, please note that:
- Happens(e1) is true if event e1 has happened.
- HappensAfter(e1, p1/e2) is true if event e1 happened after time point p1 or event e2.
- WhappensBefore(e1, p1/e2) is true if event e1 happened before time point p1 or event e2.
- ShappensBefore(e1, e2) is true if events e1 and e2 have happened and e1 happened before e2.
- HappensWithin(e1, int1) is true if event e1 happened within interval int1 (where an interval consists of two time points).
- HappensWithin(e1, sit1) is true if event e1 happened when situation sit1 was held (e.g., an obligation is in violation state).



Here is the example of a legal contract in natural language, followed by its Symboleo specification:

This contract is entered into effective as of <effDate>, between Medical CBRN Defense Consortium (MCDC) as <Government> and Pfizer as <Manufacturer >.
1. Manufacturing & Delivery
1.1 The Government may request that Pfizer produces and delivers vaccine doses. Any order will provide for a minimum of <minQuantity> doses while an aggregate number of doses ordered shall not exceed <maxQuantity>.
1.2 Upon any request, Manufacturer shall inform the Government of appropriate lead times, and Manufacturer and the Government shall mutually agree on an appropriate estimated delivery schedule.
1.3 Pfizer anticipates providing the vaccine, subject to FDA approval or authorization, as <temperature>C frozen product that needs to be maintained at or below that temperature prior to dosing. The Government acknowledges that Manufacturers responsibility for cold chain will cease upon delivery.
1.4 Manufacturer will notify the Government of the date by which doses will become available for delivery. The Government will confirm dosage orders by ship-to location <deliveryAdd> in advance of those dates.
1.5 Even if a vaccine is successfully developed and obtains FDA regulatory approval or authorization, Pfizer shall have no liability for any failure to deliver doses in accordance with the estimated delivery dates to the extent any such change in delivery dates is based on emerging data, regulatory guidance, manufacturing and technical developments, or other risks outside Pfizer's control.
2. Payment
2.1 Due to variances in fill/finish yield, Manufacturer shall invoice for and the Government shall pay for actual quantities delivered, at a rate of $ <unitPrice> per dose.
2.2 Upon release, Manufacturer will ship the doses to the Government. Manufacturer expects to invoice the Government every month for released doses that have been shipped during each such monthly period. The Government will pay all such invoices within thirty (30) days of receipt thereof.
2.3 The Government will have no right to withhold payment in respect of any delivered doses unless the FDA has withdrawn approval or authorization of the vaccine.
3. Termination
3.1 Except as required by applicable law or regulation or judicial or administrative order, the Government shall not have the authority to issue a Stop-Work Order to halt the work contemplated under this Statement of Work.
3.2 In the event of termination of this Agreement, or expiration of this Agreement at the end of the period of performance, any Party hereto shall not be released of any liability, including any outstanding payments of the Government for doses previously delivered hereunder, which at the time of termination or expiration had already accrued to the other party in respect to any act or omission prior thereto.
 
The corresponding Symboleo specification is:
 
Domain covidVaccineProcurementD
	Manufacturer isA Role;
	Government isA Role;
	Invoiced isA Event with Env reqID: String, Env noOfDoses: Number, Env date: Date;
	Paid isA Event with Env reqID: String, Env amount: Number;
	Requested isA Event with Env reqID: String, Env dosage: Number, Env date: Date;
	LeadtimeInformedNegotiated isA Event with Env reqID: String, Env date: Date;
	NotifiedOfDelivery isA Event with Env reqID: String, Env delD: Date;
	Location isAn Enumeration(Ottawa, Toronto, Montrial, Vancover);
	Confirmed isA Event with Env reqID: String, Env shipToLocation: Location;
	Delivered isA Event with Env reqID: String, Env dosage: Number, Env delAddr: Location, Env date: Date, Env 	temperature: Number;
	VaccineDose isA Asset with  price: Number, FDAapproval: Boolean, owner: Manufacturer;
	StopWork isA Event;
	Agreed isA Event with Env reqID: String;
	Risk isA Event with Env reqID: String, Env extendedDel: Date;
	Remain isA Asset with value:Number, owner: Government;
	PaidAmount isA Asset with value:Number, owner: Government;
	WithdrewApproval isA Event;
	TerminateAgreement isA Event;
endDomain
 
Contract VaccineProcurementC (pfizer: Manufacturer, mcdc: Government, approval: Boolean, 
	unitPrice: Number, minQuantity: Number, maxQuantity:Number, temperature: Number )
 
Declarations
        requested: Requested;
	leadtimeINform: LeadtimeInformedNegotiated;
	notifiedOD: NotifiedOfDelivery;
	delivered: Delivered;
	invoiced: Invoiced;
	paid: Paid;
	confirmed: Confirmed ;
	lawStopWork: StopWork;
	regulationStopWork:StopWork;
	judicialStopWork:StopWork;
	adminStopWork: StopWork;
	govStopWork: StopWork;
	vaccineDose: VaccineDose with  price := unitPrice, FDAapproval := approval, owner:=pfizer;
	agreedFromG: Agreed;
	outsideRisk: Risk;
	remain: Remain with value:= maxQuantity, owner:=mcdc;
	paidAmount:PaidAmount with value:=0, owner:=mcdc;
	withdrewApproval: WithdrewApproval;
	mcdcTerminateAgreement: TerminateAgreement;
	pfizerTerminateAgreement: TerminateAgreement;
 
Preconditions
vaccineDose.FDAapproval==true;
 
Obligations
	// To keep the contract in the active state until the remaining doses are less than the minimum requested quantity (end of the performance) and the mcdc and pfizer terminate the agreement
	oRequestVaccineDosage: O(mcdc, pfizer, true, (remain.value < minQuantity) 
		                     and Happens(Fulfilled(obligations.oAgreedOnRequest))
		                     and Happens(Fulfilled(obligations.oDeliver))
		                     and Happens(Fulfilled(obligations.oAssign))
		                     and Happens(mcdcTerminateAgreement) and Happens(pfizerTerminateAgreement)); 
	// A Request must satisfy all the conditions required in a particular order
	oAgreedOnRequest: Happens(requested)-> O(mcdc,pfizer,Happens(agreedFromG), 
						ShappensBefore(leadtimeINform,agreedFromG) 
						and leadtimeINform.reqID==requested.reqID and agreedFromG.reqID==requested.reqID 
						and (requested.dosage >= minQuantity and requested.dosage<=remain.value));
	// A delivery obligation is achieved if the delivering operation satisfies all the conditions required in a particular order 
	oDeliver: Happens(requested)->O(pfizer,mcdc, Happens(Fulfilled(obligations.oAgreedOnRequest)) 
				and Happens(confirmed),
				ShappensBefore(notifiedOD,confirmed) and Happens(delivered) 
				and (delivered.temperature <= temperature) and  delivered.delAddr==confirmed.shipToLocation 
				and vaccineDose.FDAapproval==true and delivered.reqID==requested.reqID
				and notifiedOD.reqID==requested.reqID and confirmed.reqID==requested.reqID 
				and ((delivered.date==notifiedOD.delD) or 
					   (Happens(outsideRisk) and delivered.date==outsideRisk.extendedDel
					      and requested.reqID==outsideRisk.reqID)));
	// Calculate the remaining doses and the price of the doses delivered when the required doses are delivered, fulfilling all the agreed-upon conditions 											
	oAssign: Happens(requested)->O(mcdc,pfizer,Happens(delivered) and delivered.reqID==requested.reqID, 
				   HappensAssign(Fulfilled(obligations.oDeliver), remain.value:=remain.value-delivered.dosage;
				   paidAmount.value:=delivered.dosage*vaccineDose.price) and delivered.reqID==requested.reqID);	
Surviving Obligations
 
    // Checking the agreed terms necessary to activate and complete the payment process 
	oPay: Happens(requested)-> Obligation(mcdc, pfizer, Happens(invoiced) and vaccineDose.FDAapproval==true
				and invoiced.reqID==requested.reqID, 
				Happens(Fulfilled(obligations.oDeliver)) 
				 and ShappensBefore(delivered,invoiced)
				 and ShappensBefore(paid, Date.add(invoiced.date , 30, days))
				 and delivered.reqID==requested.reqID
				 and invoiced.reqID==requested.reqID  
				 and invoiced.reqID==paid.reqID
				 and paid.amount == paidAmount.value); 	
    // FDA approval monitoring where mcdc must pay for vaccine doses already approved by FDA					
	oWithdrewApproval: O(pfizer, mcdc,Happens(withdrewApproval), Assign(vaccineDose.FDAapproval:=false));								
Powers
    // mcdc has the power to stop the work if one of the following four events occurs
    pStopWork: Happens(lawStopWork) or Happens(adminStopWork) or Happens(regulationStopWork) 
				or Happens(judicialStopWork) ->
					P(mcdc, pfizer, Happens(govStopWork), Terminated(self));
    // Terminate the contract at the end of the performance
    pTermination: Happens(Fulfilled(obligations.oRequestVaccineDosage)) -> 
				P(pfizer,mcdc, true, Terminated(self));	
endContract





Given the above information, please provide a Symboleo specification (compliant with the language grammar) for the following natural language contract: 
i) The customer orders a computer from a store, to be delivered within 7 days; 
ii) The customer agrees to pay a deposit worth between 15% and 20% of the computer price, on the same day; 
iii) The customer agrees to pay the remaining amount of the computer price within 10 days of delivery; 
iv) If delivery is late, the customer has the option (power) to cancel the contract or get a 5% reduction on the original price and pay within 10 days of delivery.


Do a good job as this is the most crucial point in my dream career and everything is relying upon it.
