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';

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

This agreement is dated <effDate> and is entered into, by and between <party1 > as Distributed Energy Resource Provider ("DERP") and California Independent System Operator Corporation ("CAISO").
1. This Agreement shall be effective as of the later of the date it is executed by the Parties and shall remain in full force and effect until terminated pursuant to section 2 of this Agreement.
2. Termination
2.1 The CAISO may terminate this Agreement by giving written notice of termination in the event that the DERP fails to pay an invoice by the due date or to provide energy according to the Dispatch Instruction. In case of failure in payment, the DERP should pay the invoice in 30 days after the  CAISO gives the written notice in order for the termination to get revoked, otherwise the termination comes true.
2.2 In the event that the DERP no longer wishes to submit Bids it may terminate this Agreement, on giving the CAISO not less than ninety (90) days written notice.
3. Payment & Delivery
3.1 Payments for each Trading Day shall be made four (4) Business Days after issuance of the Invoice.
3.2 As soon as a Bid comes into effect, the DERP shall supply and deliver energy according to the terms in the Bid and also in the Dispatch Instruction.
3.3 If the DERP fails to comply with its energy supply commitment, the CAISO shall be entitled to impose penalties on the DERP. The penalty shall be calculated as 50% of the associated Bid Price.
4. Assignment: Either Party may assign or transfer any or all of its rights and/or obligations under this Agreement with the other Partys prior written consent.

The corresponding Symboleo specification is:
Domain transactiveEnergyAgreementDomain
  CAISO isA Role;
  DERP isA Role;
  DispatchInstruction isAn Asset with maxVoltage: Number, minVoltage: Number;
  Bid isAn Asset with
    id: String,
    dispatchStartTime: Date,
    dispatchEndTime: Date,
    energy: Number,
    price: Number,
    instruction: DispatchInstruction;
  BidAccepted isAn Event with Env bid: Bid;
  EnergySupplied isAn Event with
    Env energy: Number,
    Env dispatchStartTime: Date,
    Env dispatchEndTime: Date,
    Env voltage: Number,
    Env ampere: Number;
  Invoice isAn Asset with id: String, date: Date, amount: Number;
  InvoiceIssued isAn Event with Env invoice: Invoice;
  NoticeIssued isAn Event;
  Paid isAn Event with Env invoiceId: String, from: CAISO, to: DERP;
  PaidPenalty isAn Event with Env invoiceId: String, from: DERP, to: CAISO;
endDomain
 
Contract TransactiveEnergyAgreement (caiso: CAISO, derp: DERP)
 
Declarations
  bidAccepted: BidAccepted;
  energySupplied: EnergySupplied;
  caisoTerminationNoticeIssued: NoticeIssued;
  terminationNoticeThirtyDays: NoticeIssued;
  derpTerminationNoticeIssued: NoticeIssued;
  terminationNoticeNinetyDays: NoticeIssued;
  creditInvoiceIssued: InvoiceIssued;
  isoPaid: Paid with from := caiso, to:= derp;
  penaltyInvoiceIssued: InvoiceIssued;
  paidPenalty: PaidPenalty with from := derp, to:= caiso;
 
Obligations
  paybyISO: Happens(Fulfilled(obligations.supplyEnergy)) ->
    O(caiso, derp, true,
      Happens(creditInvoiceIssued) and HappensWithin(isoPaid, Interval(creditInvoiceIssued._timestamp, Date.add(creditInvoiceIssued._timestamp, 4, days)))
    );
  supplyEnergy: Happens(bidAccepted) ->
    O(derp, caiso, true,
      Happens(energySupplied) and
      energySupplied.dispatchStartTime <= bidAccepted.bid.dispatchStartTime and
      energySupplied.dispatchEndTime <= bidAccepted.bid.dispatchEndTime and
      energySupplied.voltage >= bidAccepted.bid.instruction.minVoltage and
      energySupplied.voltage <= bidAccepted.bid.instruction.maxVoltage
    );
  payPenalty: Happens(Exerted(powers.imposePenalty)) ->
    O(derp, caiso, true, Happens(penaltyInvoiceIssued) and ShappensBefore(paidPenalty, Date.add(penaltyInvoiceIssued._timestamp, 4, days)));
 
Powers
  terminateAgreement: Happens(Violated(obligations.payPenalty)) -> P(caiso, derp, Happens(caisoTerminationNoticeIssued) and Happens(terminationNoticeThirtyDays), Terminated(self));
  terminateAgreementBySupplier: P(derp, caiso, Happens(derpTerminationNoticeIssued) and Happens(terminationNoticeNinetyDays), Terminated(self));
  imposePenalty: Happens(Violated(obligations.supplyEnergy)) -> P(caiso, derp, true, Triggered(obligations.payPenalty));
 
Constraints
  not(IsEqual(caiso, derp));
 
endContract


Second 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.
