diff options
author | Kristóf Marussy <marussy@mit.bme.hu> | 2020-05-08 18:28:19 +0200 |
---|---|---|
committer | Kristóf Marussy <marussy@mit.bme.hu> | 2020-05-08 18:28:19 +0200 |
commit | 419e76265ecbdf65e960e0624be006d31ed1e191 (patch) | |
tree | dad200fe9fd0beae7adde969206b77691a51b85a /Application/org.eclipse.viatra.solver.language/src/org/eclipse/viatra | |
parent | Fix check expressions in generated VIATRA (diff) | |
download | VIATRA-Generator-419e76265ecbdf65e960e0624be006d31ed1e191.tar.gz VIATRA-Generator-419e76265ecbdf65e960e0624be006d31ed1e191.tar.zst VIATRA-Generator-419e76265ecbdf65e960e0624be006d31ed1e191.zip |
Update solver language grammar
First version, still needs TokenSource and Linker to work.
Diffstat (limited to 'Application/org.eclipse.viatra.solver.language/src/org/eclipse/viatra')
2 files changed, 222 insertions, 148 deletions
diff --git a/Application/org.eclipse.viatra.solver.language/src/org/eclipse/viatra/solver/language/SolverLanguage.xtext b/Application/org.eclipse.viatra.solver.language/src/org/eclipse/viatra/solver/language/SolverLanguage.xtext index 8a510a19..5abeb891 100644 --- a/Application/org.eclipse.viatra.solver.language/src/org/eclipse/viatra/solver/language/SolverLanguage.xtext +++ b/Application/org.eclipse.viatra.solver.language/src/org/eclipse/viatra/solver/language/SolverLanguage.xtext | |||
@@ -3,150 +3,224 @@ import "http://www.eclipse.org/emf/2002/Ecore" as ecore | |||
3 | generate solverLanguage "http://www.eclipse.org/viatra/solver/language/SolverLanguage" | 3 | generate solverLanguage "http://www.eclipse.org/viatra/solver/language/SolverLanguage" |
4 | 4 | ||
5 | Problem: | 5 | Problem: |
6 | statements+=Statement*; | 6 | (statements+=Statement)*; |
7 | Statement: Interpretation | Predicate; | 7 | |
8 | 8 | Statement: | |
9 | @Override terminal STRING returns ecore::EString: '"' ( '\\' . /* 'b'|'t'|'n'|'f'|'r'|'u'|'"'|"'"|'\\' */ | !('\\'|'"') )* '"'; | 9 | ( |
10 | REALLiteral returns ecore::EBigDecimal: '-'? INT '.' INT; | 10 | AssertionOrDefinition | PredicateDefinition | UnnamedErrorPrediateDefinition | DefaultDefinition | ExternPredicateDefinition | |
11 | INTLiteral returns ecore::EInt: '-'? INT; | 11 | MetricDefinition | ExternMetricDefinition | ClassDefinition | ScopeDefinition | ObjectiveDefinition |
12 | BooleanValue: {BooleanTrue} 'true' | 'false' {BooleanFalse}; | 12 | ) DOT; |
13 | TruthValue: {True} 'true' | {False} 'false' | {Unknown} 'unknown' | {Error} 'error' ; | 13 | |
14 | 14 | AssertionOrDefinition returns Statement: | |
15 | 15 | Expression ( | |
16 | /////////////////// | 16 | {Assertion.body=current} (":" range=Expression)? | |
17 | // Core grammar | 17 | {PredicateDefinition.head=current} ":-" body=Expression | |
18 | /////////////////// | 18 | {MetricDefinition.head=current} "=" body=Expression |
19 | Interpretation: BasicInterpretation | DefaultInterpretation | CDInterpretation; | 19 | ); |
20 | 20 | ||
21 | BasicInterpretation: symbol=Symbol ('(' (objects+=ComplexObject (',' objects+=ComplexObject)*)? ')')? ':' value = TruthValue; | 21 | PredicateDefinition: |
22 | 22 | (functional?="functional" error?="error"? | error?="error" functional?="functional"?) head=Call ":-" body=Expression; | |
23 | Symbol: ModelSymbol | PartialitySymbol | DataSymbol; | 23 | |
24 | 24 | UnnamedErrorPrediateDefinition: | |
25 | ModelSymbol: name = ID; | 25 | "error" argumentList=ArgumentList ":-" body=Expression; |
26 | 26 | ||
27 | PartialitySymbol: ExistSymbol | EqualsSymbol; | 27 | DefaultDefinition: |
28 | ExistSymbol:'exists'{ExistSymbol}; | 28 | "default" head=Call ":" range=Expression; |
29 | EqualsSymbol:'equals' {EqualsSymbol}; | 29 | |
30 | 30 | ExternPredicateDefinition: | |
31 | DataSymbol: BooleanSymbol | IntegerSymbol | RealSymbol | StringSymbol; | 31 | "extern" head=Call "."; |
32 | BooleanSymbol:'bool' {BooleanSymbol}; | 32 | |
33 | IntegerSymbol:'int' {IntegerSymbol}; | 33 | enum MetricType: |
34 | RealSymbol: 'real' {RealSymbol}; | 34 | INT="int" | REAL="real"; |
35 | StringSymbol:'string' {StringSymbol}; | 35 | |
36 | 36 | MetricDefinition: | |
37 | ComplexObject: Object | AllInstances | AllObjects; | 37 | type=MetricType head=Expression "=" body=Expression; |
38 | 38 | ||
39 | Object: NamedObject | UnnamedObject | DataObject; | 39 | ExternMetricDefinition: |
40 | NamedObject: "'" name = ID "'"; | 40 | "extern" type=MetricType head=Call; |
41 | UnnamedObject: name = ID; | 41 | |
42 | DataObject: BooleanObject | IntObject | RealObject | StringObject; | 42 | Expression: |
43 | BooleanObject: value = BooleanValue; | 43 | IfElse | DisjunctiveExpression; |
44 | IntObject: value = INTLiteral; | 44 | |
45 | RealObject: value = REALLiteral; | 45 | IfElse: |
46 | StringObject: value = STRING; | 46 | "if" condition=Expression "then" then=Expression "else" else=Expression; |
47 | 47 | ||
48 | /////////////////// | 48 | DisjunctiveExpression returns Expression: |
49 | // Predicte grammar | 49 | ConjunctiveExpression ( |
50 | /////////////////// | 50 | {Disjunction.children+=current} (";" children+=ConjunctiveExpression)+ | |
51 | 51 | {Case.condition=current} "->" body=ConjunctiveExpression {Switch.cases+=current} (";" cases+=Case)* | |
52 | Predicate: | 52 | )?; |
53 | (isError?='error')? symbol = ModelSymbol ('(' (parameters += Parameter (',' parameters += Parameter)*)? ')')? ':-' ('false' | (bodies += PatternBody ('|' bodies += PatternBody)*)) '.' | 53 | |
54 | ; | 54 | Case: |
55 | 55 | condition=ConjunctiveExpression "->" body=ConjunctiveExpression; | |
56 | Parameter: variable = Variable (':' type = Symbol)?; | 56 | |
57 | PatternBody: {PatternBody} ('true' | constraints += Constraint*) ; | 57 | ConjunctiveExpression returns Expression: |
58 | Polarity: {Positive} '+' | {Negative} '-'; | 58 | ComparisonExpression ({Conjunction.children+=current} ("," children+=ComparisonExpression)+)?; |
59 | Constraint: (polarity = Polarity)? symbol = ModelSymbol | 59 | |
60 | (('(' params += Literal? (',' params += Literal)* ')')?) | 60 | enum BinaryOperator: |
61 | | | 61 | EQ | NOT_EQ | LESS | LESS_EQ | GREATER | GREATER_EQ | IN | ADD | SUB | MUL | DIV | POW; |
62 | (closureType=ClosureType '(' params += Literal? (',' params += Literal)* ')'); | 62 | |
63 | ClosureType: {ReflexiveClosure} '*' | {IrreflexiveClosure} '+'; | 63 | enum ComparisonOperator returns BinaryOperator: |
64 | Literal: Variable | DataObject | NamedObject; | 64 | EQ="==" | NOT_EQ="!=" | LESS="<" | LESS_EQ="<=" | GREATER=">" | GREATER_EQ=">=" | IN="in"; |
65 | Variable: name = ID; | 65 | |
66 | 66 | ComparisonExpression returns Expression: | |
67 | /////////////////// | 67 | AdditiveExpression ({Comparison.left=current} op=ComparisonOperator right=AdditiveExpression)?; |
68 | // Complex Interpretation grammar | 68 | |
69 | /////////////////// | 69 | enum AdditiveBinaryOperator returns BinaryOperator: |
70 | 70 | ADD="+" | SUB="-"; | |
71 | AllInstances: ':' symbol = Symbol; | 71 | |
72 | AllObjects: {AllObjects} '*'; | 72 | AdditiveExpression returns Expression: |
73 | 73 | MultiplicativeExpression ({BinaryExpression.left=current} op=AdditiveBinaryOperator right=MultiplicativeExpression)*; | |
74 | /////////////////// | 74 | |
75 | // Defaul Interpretation grammar | 75 | enum MultiplicativeBinaryOperator returns BinaryOperator: |
76 | /////////////////// | 76 | MUL="*" | DIV="/"; |
77 | DefaultInterpretation: 'default' interpretation = BasicInterpretation; | 77 | |
78 | 78 | MultiplicativeExpression returns Expression: | |
79 | /////////////////// | 79 | ExponentialExpression ({BinaryExpression.left=current} op=MultiplicativeBinaryOperator right=ExponentialExpression)*; |
80 | // Advanced Class-Diagram interpretations | 80 | |
81 | /////////////////// | 81 | enum ExponentialOp returns BinaryOperator: |
82 | CDInterpretation: ClassInterpretation | EnumInterpretation| GlobalRelationInterpretation; | 82 | POW="^"; |
83 | ClassInterpretation: | 83 | |
84 | (abstract?='abstract')? 'class' symbol = ModelSymbol ('extends' supertypes += ModelSymbol+)?'{' | 84 | ExponentialExpression returns Expression: |
85 | fielt += FieldRelationInterpretation* | 85 | UnaryExpression ({BinaryExpression.left=current} op=ExponentialOp right=ExponentialExpression)?; |
86 | '}' | 86 | |
87 | ; | 87 | enum UnaryOp: |
88 | EnumInterpretation: 'enum' Symbol = ModelSymbol '{' objects+=NamedObject+ '}'; | 88 | NEG="!" | PLUS="+" | MINUS="-" | MAY="may" | MUST="must" | CURRENT="current"; |
89 | FieldRelationInterpretation: (containment ?= 'containment')? symbol = ModelSymbol ':' multiplicity = MultiplicityDefinition? target = Symbol; | 89 | |
90 | GlobalRelationInterpretation: (containment ?= 'containment')? 'relation' symbol = ModelSymbol ':' sourceMultiplicity = MultiplicityDefinition? source = Symbol targetMultiplicity = MultiplicityDefinition? target = Symbol; | 90 | UnaryExpression returns Expression: |
91 | MultiplicityDefinition: lower = INT '..' (upper = INT | unlimitedUpper?='*'); | 91 | AggregationExpression | {UnaryExpression} op=UnaryOp body=AggregationExpression; |
92 | 92 | ||
93 | ////SymbolIntroduction : Type | GlobalRelation | Predicate; | 93 | AggregationExpression returns Expression: |
94 | ////Symbol: Type | Relation | Predicate | Variable | Element; | 94 | AtomicExpression | Count | Aggregation; |
95 | // | 95 | |
96 | ////////////////////// | 96 | Count: |
97 | //// Types | 97 | "count" "{" body=Expression "}"; |
98 | ////////////////////// | 98 | |
99 | // | 99 | enum AggregationOp: |
100 | //Type: TypeDeclaration | /*TypeDefinition |*/ TypeEnumeration; | 100 | ONLY="only" | SUM="sum" | PROD="prod" | AVG="avg" | MIN="min" | MAX="max"; |
101 | // | 101 | |
102 | //TypeDeclaration: | 102 | Aggregation: |
103 | // abstract?= 'abstract' 'class' name = ID ('extends' supertypes += [Type] (',' supertypes += [Type])) '{' | 103 | op=AggregationOp "{" body=Expression "|" condition=Expression "}"; |
104 | // fieldDeclarations += FieldRelationDeclaration* | 104 | |
105 | // '}' | 105 | AtomicExpression returns Expression: |
106 | //; | 106 | Reference ({Call.functor=current} -> argumentList=ArgumentList)? | Interval | Literal | "(" Expression ")"; |
107 | //TypeEnumeration: | 107 | |
108 | // 'enum' name = ID 'extends' supertypes += [Type] (',' supertypes += [Type]) '{' | 108 | Call: |
109 | // (elements += Element)* | 109 | functor=Reference (transitiveClosure?=STAR | reflexiveTransitiveClosure?=PLUS)? argumentList=ArgumentList; |
110 | // '}' | 110 | |
111 | //; | 111 | ArgumentList: |
112 | //Element: | 112 | {ArgumentList} "(" (arguments+=Argument ("," arguments+=Argument)*)? ")"; |
113 | // name = ID | 113 | |
114 | //; | 114 | Argument: |
115 | // | 115 | ExpressionArgument | StarArgument | TypedArgument | TypedStarArgument; |
116 | ////////////////////// | 116 | |
117 | //// Relations | 117 | ExpressionArgument: |
118 | ////////////////////// | 118 | body=ComparisonExpression; |
119 | // | 119 | |
120 | //Relation: FieldRelationDeclaration | GlobalRelationDeclaration | RelationEnumeration; | 120 | StarArgument: |
121 | //GlobalRelation returns Relation: GlobalRelationDeclaration | /*RelationDefinition |*/ RelationEnumeration; | 121 | {StarArgument} "*"; |
122 | // | 122 | |
123 | //FieldRelationDeclaration: | 123 | TypedArgument: |
124 | // containment?='containment' target = [Type] name = ID | 124 | type=[NamedElement|QualifiedName] variable=[NamedElement|QualifiedName]; |
125 | //; | 125 | |
126 | // | 126 | TypedStarArgument: |
127 | //GlobalRelationDeclaration: | 127 | type=[NamedElement|QualifiedName] "*"; |
128 | // containment?='containment' 'relation' name = ID '(' source = [Type] ',' target = [Type] ')' | 128 | |
129 | //; | 129 | Reference: |
130 | // | 130 | referred=[NamedElement|QualifiedName]; |
131 | //RelationEnumeration: | 131 | |
132 | // 'relation' name = ID '{' links += Link* '}' | 132 | Interval: |
133 | //; | 133 | "[" lowerBound=Expression ".." upperBound=Expression "]"; |
134 | // | 134 | |
135 | //Link: '(' source = Element ',' target = Element ')'; | 135 | Literal: |
136 | // | 136 | LogicLiteral | NumericLiteral | InfinityLiteral | EmptyIntervalLiteral | StringLiteral; |
137 | // | 137 | |
138 | // | 138 | enum LogicValue: |
139 | // | 139 | TRUE="true" | FALSE="false" | UNKNOWN="unknown" | ERROR="error"; |
140 | // | 140 | |
141 | // | 141 | LogicLiteral: |
142 | //Model: | 142 | value=LogicValue; |
143 | // 'model' '{' | 143 | |
144 | // atoms += Atom (',' atoms += Atom ) | 144 | NumericLiteral: |
145 | // '}' | 145 | value=Real; |
146 | //; | 146 | |
147 | //Atom: referredSymbol = [Symbol] '(' (params += Element (',' params += Element)*)? ')'; | 147 | InfinityLiteral: |
148 | // | 148 | {InfinityLiteral} "inf"; |
149 | //ScopeDeclaration: | 149 | |
150 | // 'scope' | 150 | EmptyIntervalLiteral: |
151 | //; | 151 | {EmptyIntervalLiteral} "empty"; |
152 | // | 152 | |
153 | StringLiteral: | ||
154 | value=STRING; | ||
155 | |||
156 | ClassDefinition returns Statement: | ||
157 | abstract?="abstract"? "class" name=ID ("extends" superclasses+=[NamedElement|QualifiedName] ("," superclasses+=[NamedElement|QualifiedName])*)? | ||
158 | "{" members+=MemberDefinition* "}"; | ||
159 | |||
160 | MemberDefinition: | ||
161 | containment?="contains"? type=[NamedElement|QualifiedName] multiplicity=Multiplicity? name=ID ("opposite" opposite=[NamedElement|QualifiedName])? ";"?; | ||
162 | |||
163 | Multiplicity: | ||
164 | ManyMultiplicity | ExactMultiplicity | BoundedMultiplicity; | ||
165 | |||
166 | ManyMultiplicity: | ||
167 | {ManyMultiplicity} "[" "]"; | ||
168 | |||
169 | ExactMultiplicity: | ||
170 | "[" multiplicity=UpperMultiplicty "]"; | ||
171 | |||
172 | BoundedMultiplicity: | ||
173 | "[" lowerBound=INT ".." upperBound=UpperMultiplicty "]"; | ||
174 | |||
175 | ScopeDefinition: | ||
176 | ExactScopeDefinition | BoundedScopeDefinition | LowerBoundedScopeDefinition; | ||
177 | |||
178 | ExactScopeDefinition: | ||
179 | "scope" type=[NamedElement|QualifiedName] "==" exactScope=INT; | ||
180 | |||
181 | BoundedScopeDefinition: | ||
182 | "scope" ( | ||
183 | (lowerBound=INT "<=")? type=[NamedElement|QualifiedName] "<=" upperBound=INT | | ||
184 | upperBound=INT ">=" type=[NamedElement|QualifiedName] (">=" lowerBound=INT)? | ||
185 | ) "."; | ||
186 | |||
187 | LowerBoundedScopeDefinition: | ||
188 | "scope" ( | ||
189 | lowerBound=INT "<=" type=[NamedElement|QualifiedName] | | ||
190 | type=[NamedElement|QualifiedName] ">=" lowerBound=INT | ||
191 | ) "."; | ||
192 | |||
193 | enum ObjectiveKind: | ||
194 | MINIMIZE="minimize" | MAXIMIZE="maximize"; | ||
195 | |||
196 | ObjectiveDefinition: | ||
197 | kind=ObjectiveKind objective=Expression; | ||
198 | |||
199 | UpperMultiplicty returns ecore::EInt: | ||
200 | INT | "*"; | ||
201 | |||
202 | Real returns ecore::EBigDecimal hidden(): | ||
203 | INT ("." INT)?; | ||
204 | |||
205 | QualifiedName hidden(): | ||
206 | ID ("." ID)* | QUOTED_ID; | ||
207 | |||
208 | @Override | ||
209 | terminal STRING returns ecore::EString: | ||
210 | '"' ( '\\' . /* 'b'|'t'|'n'|'f'|'r'|'u'|'"'|"'"|'\\' */ | !('\\'|'"') )* '"'; | ||
211 | |||
212 | terminal QUOTED_ID returns ecore::EString: | ||
213 | '\'' ( '\\' . /* 'b'|'t'|'n'|'f'|'r'|'u'|'"'|"'"|'\\' */ | !('\\'|'\'') )* '\''; | ||
214 | |||
215 | terminal PLUS: | ||
216 | "synthetic::plus"; | ||
217 | |||
218 | terminal STAR: | ||
219 | "synthetic::star"; | ||
220 | |||
221 | terminal DOT: | ||
222 | "synthetic::dot"; | ||
223 | |||
224 | NamedElement: | ||
225 | name=QualifiedName; | ||
226 | |||
diff --git a/Application/org.eclipse.viatra.solver.language/src/org/eclipse/viatra/solver/language/validation/SolverLanguageValidator.xtend b/Application/org.eclipse.viatra.solver.language/src/org/eclipse/viatra/solver/language/validation/SolverLanguageValidator.xtend index a7ff7252..6701d465 100644 --- a/Application/org.eclipse.viatra.solver.language/src/org/eclipse/viatra/solver/language/validation/SolverLanguageValidator.xtend +++ b/Application/org.eclipse.viatra.solver.language/src/org/eclipse/viatra/solver/language/validation/SolverLanguageValidator.xtend | |||
@@ -1,5 +1,5 @@ | |||
1 | /* | 1 | /* |
2 | * generated by Xtext 2.18.0.M3 | 2 | * generated by Xtext 2.21.0 |
3 | */ | 3 | */ |
4 | package org.eclipse.viatra.solver.language.validation | 4 | package org.eclipse.viatra.solver.language.validation |
5 | 5 | ||