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 agreement is entered into as of <effDate>, between <party1 > as Seller with address <retAdd>, and <party2 > as Buyer with address <delAdd>.
1. Payment & Delivery
   1.1 Seller shall sell an amount of <qnt> meat with <qlt> quality (goods) to the Buyer.
   1.2 Title in the Goods shall not pass on to the Buyer until payment of the amount owed has been made in full.
   1.3 The Seller shall deliver the Order in one delivery within <delDueDateDays> days to the Buyer at its warehouse.
   1.4 The Buyer shall pay <amt> (amount) in <curr > (currency) to the Seller before <payDueDate>.
   1.5 In the event of late payment of the amount owed, the Buyer shall pay a late fee equal to <intRate>% of the amount owed, and the Seller may suspend performance of all of its obligations under the agreement until payment of amounts owed has been received in full.
2. Assignment
   2.1 The rights and obligations are not assignable by Buyer.
3. Termination
   3.1 Any delay in delivery of the goods will not entitle the Buyer to terminate the Contract unless such delay exceeds 10 Days.
4. Confidentiality
4.1 Both Seller and Buyer must keep the contents of this contract confidential during the execution of the contract and six months after its termination.

The corresponding Symboleo specification is:
// This is the domain model, which describes the concepts that subtype the Symboleo ontology
Domain meatSaleDomain
  Seller isA Role with returnAddress: String, name: String;
  Buyer isA Role with warehouse: String;
  Currency isAn Enumeration(CAD, USD, EUR);
  MeatQuality isAn Enumeration(PRIME, AAA, AA, A);
  PerishableGood isAn Asset with quantity: Number, quality: MeatQuality;
  Meat isA PerishableGood;
  Delivered isAn Event with item: Meat, deliveryAddress: String, delDueDate: Date;
  Paid isAn Event with amount: Number, currency: Currency, from: Buyer, to: Seller, payDueDate: Date;
  PaidLate isAn Event with amount: Number, currency: Currency, from: Buyer, to: Seller;
  Disclosed isAn Event;
endDomain
 
// This is the contract signature, with the typed parameters required at contract instantiation time
Contract MeatSale (buyer : Buyer, seller : Seller, qnt : Number, qlt : MeatQuality, amt : Number, curr : Currency, payDueDate: Date,
  delAdd : String, effDate : Date, delDueDateDays : Number, interestRate: Number
)
 
// These are local declarations for the contract.
Declarations
  goods: Meat with quantity := qnt, quality := qlt;
  delivered: Delivered with item := goods, deliveryAddress := delAdd, delDueDate := Date.add(effDate, delDueDateDays, days);
  paidLate: PaidLate with amount := (1 + interestRate / 100) * amt, currency := curr, from := buyer, to := seller;
  paid: Paid with amount := amt, currency := curr, from := buyer, to := seller, payDueDate := payDueDate;
  disclosed: Disclosed;
 
// Contracts can have pre- and post-conditions.
Preconditions
  IsOwner(goods, seller);
 
Postconditions
  IsOwner(goods, buyer) and not(IsOwner(goods, seller));
 
// Contracts are collections of obligations and powers
Obligations
  delivery: Obligation(seller, buyer, true, WhappensBefore(delivered, delivered.delDueDate));
  payment: O(buyer, seller , true, WhappensBefore(paid, paid.payDueDate)); // O() and Obligation() are equivalent (short and long form)
  latePayment: Happens(Violated(obligations.payment)) -> O(buyer, seller, true, Happens(paidLate));
 
Powers
  suspendDelivery : Happens(Violated(obligations.payment)) -> Power(seller, buyer, true, Suspended(obligations.delivery));
  resumeDelivery: HappensWithin(paidLate, Suspension(obligations.delivery)) -> P(buyer, seller, true, Resumed(obligations.delivery));
  terminateContract: Happens(Violated(obligations.delivery)) -> P(buyer, seller, true, Terminated(self));  // P() and Power() are equivalent (short and long form)
 
// Additional constraints can also be specified for a contract.
Constraints
  not(IsEqual(buyer, seller));

  CannotBeAssigned(suspendDelivery);
  CannotBeAssigned(resumeDelivery);
  CannotBeAssigned(terminateContract);
  CannotBeAssigned(delivery);
  CannotBeAssigned(payment);
  CannotBeAssigned(latePayment);
  delivered.delDueDate < paid.payDueDate;
 
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.

