This page shows the Xtext project for the SEAMS 2017 paper A Generated Property Specification Language forAdaptive Multirobot Missions.

Mission Specification Grammar in Xtext

The Eclipse project can be found here.

The five projects can be imported in Eclipse Luna with Xtext 2.9.0. An Eclipse plug-in of the Mission Specification Grammar can be built by right-clicking the project called "be.uantwerpen.ansymo.missionspecification", selecting "Run as", "Eclipse Application". This will spawn a new instance of Eclipse, with the plug-in loaded. In the new instance, create a new Java project, and create a file with extension ".spec", i.e., the extension of Mission Specification files. In the text editor, the Mission Specification Language can be used (including parse error visualisation, ctrl-tab, hierarchy, etc.).

Examples:

• Globally, if a Robot r performing a Spray and also r on a Coordinate p, then it must have been the case that a ReceiveCoordinates at p beforehand
• Globally, it is never the case that a Robot r in an Area with name as "lowflyzone" and also r on a GeoCoordinate with altitude less than 20
• Globally, it is always the case that a Robot performing a Task implies a Robot on a RelativeCoordinate with x as 100 and y as 200 and z as 10

Eclipse screenshot showing syntax highlighting and autocomplete:

The Xtext grammar is as follows:

grammar be.uantwerpen.ansymo.missionspecification.MissionSpecification with org.eclipse.xtext.common.Terminals

import "http://www.eclipse.org/emf/2002/Ecore" as ecore
generate missionSpecification "http://www.uantwerpen.be/ansymo/missionspecification/MissionSpecification"

MissionSpecification:
	properties+=Property+;
	
Property:
	scope=Scope ',' pattern=Pattern '.'?;

Scope:
	{GlobalScope} 'Globally' | 
	{BeforeScope} 'Before' r=Proposition | 
	{AfterScope} 'After' q=Proposition | 
	{BetweenScope} 'Between' q=Proposition ',' 'and' r=Proposition | 
	{AfterUntilScope} 'After' q=Proposition ',' 'until' r=Proposition;
	
Pattern:
	Occurence | Order;

Occurence:
	Universality | Absence | Existence | BoundedExistence;

Universality:
	'it' 'is' 'always' 'the' 'case' 'that' p=Proposition 'holds'?;
	
Absence:
	'it' 'is' 'never' 'the' 'case' 'that' p=Proposition 'holds'?; // . must be here and not in Property rule for some reason
	
Existence:
	p=Proposition 'holds'? 'eventually';
	
BoundedExistence:
	p=Proposition 'holds'? 'at' 'most' n=INT 'times';
	
Order:
	Precedence | Response;

Precedence:
	'if' p=Proposition 'holds'? ',' 'then' 'it' 'must' 'have' 'been' 'the' 'case' 'that' s=Proposition ('has' 'occurred')? 'beforehand';

Response:
	'if' p=Proposition ('has' 'occurred')? ',' 'then' 'in' 'response' s=Proposition ('eventually' 'holds')?;
	
Proposition:
	ImpliesProposition;

ImpliesProposition returns Proposition:
	OrProposition ({Implies.left=current} 'implies' right=OrProposition)*;

OrProposition returns Proposition:
	AndProposition ({Or.left=current} 'or' right=AndProposition)*;

AndProposition returns Proposition:
	AtomicProposition ({And.left=current} 'and' 'also' right=AtomicProposition)*;
	
AtomicProposition:
	inst=Instance ('with' cond+=BooleanExpression ('and' cond+=BooleanExpression)*)? (assoc=Association inst2=Instance ('with' cond2+=BooleanExpression ('and' cond2+=BooleanExpression)*)?)?;

BooleanExpression:
	BinaryExpression |
	UnaryExpression |
	{Condition} attr=Attribute;

BinaryExpression:
	{EqualsCondition} attr=Attribute 'as' val=Literal |
	{LessThanCondition} attr=Attribute 'less' 'than' val=Literal |
	{GreaterThanCondition} attr=Attribute 'greater' 'than' val=Literal;

UnaryExpression:
	{NotCondition} 'not' attr=Attribute;

Instance:
	InstanceRef | InstanceDecl;

InstanceDecl:
	('a' | 'an') type=Type (name=ID)?;

InstanceRef:
	ref=[InstanceDecl];

Association:
	 {TasksAssociation} 'that' 'is' 'a' 'task' 'of' | 
	 {TeamAssociation} 'that' 'is' 'a' 'team' 'of' | 
	 {RobotsAssociation} 'that' 'is' 'in' | 
	 {CurrentTaskAssociation} ('currently')? 'doing' | 
	 {CoveredTasksAssociation} 'that' 'has' 'scheduled' | 
	 {TodoTasksAssociation} 'that' 'has' 'planned' 'in' 'the' 'future' | 
	 {FinishedTasksAssociation} 'that' 'has' 'finished' | 
	 {PerformingActionAssociation} ('currently')? 'performing' | 
	 {InAssociation} ('currently')? 'in' | 
	 {CurrentPositionAssociation} ('currently')? 'on' | 
	 {HomeAssociation} 'with' 'as' 'home' | 
	 {TaskAreaAssociation} 'with' 'task' 'area' | 
	 {CoveredPointsAssociation} 'which' 'visits' | 
	 {TodoPointsAssociation} 'which' 'will' 'visit' 'in' 'the' 'future' | 
	 {FinishedPointsAssociation} 'which' 'has' 'visited' | 
	 {PointsAssociation} 'with' 'points' | 
	 {InitialPositionAssociation} 'with' 'initial' 'position' | 
	 {ReferenceAssociation} 'which' 'references';

Type:
	name=ID;
	
Attribute:
	name=ID;

Literal returns ArithmeticExpression:
	IntLiteral | RealLiteral | StringLiteral | BoolLiteral;

IntLiteral:
	value=SignedInt;
	
RealLiteral:
	value=SignedReal;
	
StringLiteral:
	value=STRING;
	
BoolLiteral:
	value=('true'|'false');

SignedInt returns ecore::EInt:
	'-'? INT;

SignedReal returns ecore::EBigDecimal:
	'-'? REAL;
	
terminal REAL returns ecore::EBigDecimal: INT? '.' INT;