diff options
author | ArenBabikian <aren.babikian@mail.mcgill.ca> | 2019-10-25 04:15:39 -0400 |
---|---|---|
committer | ArenBabikian <aren.babikian@mail.mcgill.ca> | 2019-10-25 04:15:39 -0400 |
commit | 25a4b1b53add70e268c3083682f8a3508c618ec2 (patch) | |
tree | 6d46e62be49cfe6c5640e2e9af80aae90da6a212 /Solvers/Alloy-Solver2/hu.bme.mit.inf.dslreasoner.alloy.language/src/hu/bme/mit/inf/dslreasoner/AlloyLanguage.xtext | |
parent | mid-measurement push (diff) | |
download | VIATRA-Generator-25a4b1b53add70e268c3083682f8a3508c618ec2.tar.gz VIATRA-Generator-25a4b1b53add70e268c3083682f8a3508c618ec2.tar.zst VIATRA-Generator-25a4b1b53add70e268c3083682f8a3508c618ec2.zip |
VAMPIRE: post-submission push
Diffstat (limited to 'Solvers/Alloy-Solver2/hu.bme.mit.inf.dslreasoner.alloy.language/src/hu/bme/mit/inf/dslreasoner/AlloyLanguage.xtext')
-rw-r--r-- | Solvers/Alloy-Solver2/hu.bme.mit.inf.dslreasoner.alloy.language/src/hu/bme/mit/inf/dslreasoner/AlloyLanguage.xtext | 152 |
1 files changed, 152 insertions, 0 deletions
diff --git a/Solvers/Alloy-Solver2/hu.bme.mit.inf.dslreasoner.alloy.language/src/hu/bme/mit/inf/dslreasoner/AlloyLanguage.xtext b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dslreasoner.alloy.language/src/hu/bme/mit/inf/dslreasoner/AlloyLanguage.xtext new file mode 100644 index 00000000..fba3838c --- /dev/null +++ b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dslreasoner.alloy.language/src/hu/bme/mit/inf/dslreasoner/AlloyLanguage.xtext | |||
@@ -0,0 +1,152 @@ | |||
1 | grammar hu.bme.mit.inf.dslreasoner.AlloyLanguage with org.eclipse.xtext.common.Terminals | ||
2 | |||
3 | generate alloyLanguage "http://www.bme.hu/mit/inf/dslreasoner/AlloyLanguage" | ||
4 | |||
5 | ALSDocument: | ||
6 | ( enumDeclarations += ALSEnumDeclaration | | ||
7 | signatureBodies += ALSSignatureBody | | ||
8 | functionDefinitions += ALSFunctionDefinition | | ||
9 | relationDefinitions += ALSRelationDefinition | | ||
10 | factDeclarations += ALSFactDeclaration)+ | ||
11 | runCommand = ALSRunCommand | ||
12 | ; | ||
13 | |||
14 | ////////////////////////////////// | ||
15 | // ALS terminals | ||
16 | ////////////////////////////////// | ||
17 | |||
18 | terminal ID: ('a'..'z'|'A'..'Z'|'_') ('a'..'z'|'A'..'Z'|'_'|"'"|'"'|'0'..'9')*; | ||
19 | ALSID: ID; | ||
20 | |||
21 | enum ALSMultiplicity: all | no | some | lone | one | set; | ||
22 | |||
23 | |||
24 | ////////////////////////////////// | ||
25 | // ALS types | ||
26 | ////////////////////////////////// | ||
27 | |||
28 | ALSRelationDeclaration: ALSTypeDeclaration | ALSEnumLiteral | ALSFieldDeclaration | ALSVariableDeclaration; | ||
29 | |||
30 | ALSTypeDeclaration: | ||
31 | ALSEnumDeclaration | ALSSignatureDeclaration | ||
32 | ; | ||
33 | |||
34 | ALSEnumDeclaration: | ||
35 | 'enum' name=ALSID '{' | ||
36 | literal+=ALSEnumLiteral ("," literal+=ALSEnumLiteral)* | ||
37 | '}'; | ||
38 | ALSEnumLiteral: name = ALSID; | ||
39 | |||
40 | ALSSignatureDeclaration: name = ALSID; | ||
41 | |||
42 | ALSSignatureBody: | ||
43 | ((multiplicity = ALSMultiplicity?) & (abstract ?= 'abstract')?) | ||
44 | 'sig' | ||
45 | declarations += ALSSignatureDeclaration (',' declarations += ALSSignatureDeclaration)* | ||
46 | (('extends' supertype = [ALSSignatureDeclaration]) | ||
47 | | | ||
48 | ('in' superset += [ALSSignatureDeclaration] ('+' superset += [ALSSignatureDeclaration])*) )? | ||
49 | '{' (fields+=ALSFieldDeclaration ("," fields+=ALSFieldDeclaration)*)? '}' | ||
50 | ; | ||
51 | |||
52 | ALSFieldDeclaration: | ||
53 | name = ALSID ':' (multiplicity = ALSMultiplicity)? type = ALSTerm | ||
54 | ; | ||
55 | |||
56 | ALSDefinition : ALSFunctionDefinition | ALSRelationDefinition; | ||
57 | |||
58 | ALSFunctionDefinition: | ||
59 | "fun" name = ALSID "[" variables+=ALSVariableDeclaration (',' variables+=ALSVariableDeclaration)* "]" ":" type = ALSTerm | ||
60 | "{" value = ALSTerm "}" | ||
61 | ; | ||
62 | ALSRelationDefinition: | ||
63 | "pred" name = ALSID "[" variables+=ALSVariableDeclaration (',' variables+=ALSVariableDeclaration)* "]" | ||
64 | "{" value = ALSTerm "}" | ||
65 | ; | ||
66 | |||
67 | ALSFactDeclaration: {ALSFactDeclaration} 'fact' (name=ALSID)? '{' (term = ALSTerm) '}' ; | ||
68 | |||
69 | ////////////////////////////////// | ||
70 | // ALS terms | ||
71 | ////////////////////////////////// | ||
72 | ALSTerm: ALSQuantified; | ||
73 | |||
74 | ALSQuantified returns ALSTerm: ({ALSQuantifiedEx} type = ALSMultiplicity | ||
75 | (disj?='disj')? variables+=ALSVariableDeclaration (',' variables+=ALSVariableDeclaration)* '{' expression = ALSTerm '}') | ALSOr; | ||
76 | |||
77 | ALSOr returns ALSTerm: ALSIff ({ALSOr.leftOperand = current} ( "||" | "or" ) rightOperand = ALSIff)?; | ||
78 | ALSIff returns ALSTerm: ALSImpl ({ALSIff.leftOperand = current} ("<=>" | "iff") rightOperand = ALSImpl)?; | ||
79 | ALSImpl returns ALSTerm: ALSAnd ({ALSImpl.leftOperand = current} ("=>" | "implies") rightOperand = ALSAnd ('else' elseOperand = ALSAnd)?)?; | ||
80 | ALSAnd returns ALSTerm: ALSComparison ({ALSAnd.leftOperand = current} ( "&&" | "and" ) rightOperand = ALSComparison)?; | ||
81 | |||
82 | ALSComparison returns ALSTerm: | ||
83 | ALSOverride | ||
84 | (({ALSEquals.leftOperand = current} "=" | | ||
85 | {ALSNotEquals.leftOperand = current} "!=" | | ||
86 | {ALSSubset.leftOperand = current} "in" | | ||
87 | {ALSLess.leftOperand = current} ">" | | ||
88 | {ALSLeq.leftOperand = current} ">=" | | ||
89 | {ALSMore.leftOperand = current} "<" | | ||
90 | {ALSMeq.leftOperand = current} "<=") | ||
91 | rightOperand = ALSOverride)?; | ||
92 | |||
93 | ALSOverride returns ALSTerm: ALSRangeRestrictionRight ({ALSOverride.leftOperand = current} '++' rightOperand = ALSRangeRestrictionRight)?; | ||
94 | |||
95 | ALSRangeRestrictionRight returns ALSTerm: ALSRangeRestrictionLeft ({ALSRangeRestrictionRight.relation = current} ':>' filter = ALSRangeRestrictionLeft)?; | ||
96 | ALSRangeRestrictionLeft returns ALSTerm: ALSJoin ({ALSRangeRestrictionLeft.filter = current} '<:' relation = ALSJoin)?; | ||
97 | ALSJoin returns ALSTerm: ALSMinus ({ALSJoin.leftOperand = current} '.' rightOperand = ALSMinus )*; | ||
98 | |||
99 | ALSMinus returns ALSTerm: ALSPlus ({ALSMinus.leftOperand = current} '-' rightOperand = ALSPlus)*; | ||
100 | ALSPlus returns ALSTerm: ALSIntersection ({ALSPlus.leftOperand = current} '+' rightOperand = ALSIntersection)*; | ||
101 | ALSIntersection returns ALSTerm: ALSDirectProduct ({ALSIntersection.leftOperand = current} '&' rightOperand = ALSDirectProduct)*; | ||
102 | //ALSMultiply returns ALSTerm: ALSDirectProduct ({ALSMultiply.leftOperand = current} '*' rightOperand = ALSDirectProduct)*; | ||
103 | |||
104 | ALSDirectProduct returns ALSTerm: | ||
105 | ALSPreficed | ||
106 | ({ALSDirectProduct.leftOperand = current} (leftMultiplicit = ALSMultiplicity)? | ||
107 | '->' | ||
108 | (rightMultiplicit = ALSMultiplicity)? | ||
109 | rightOperand = ALSPreficed)? | ||
110 | ; | ||
111 | |||
112 | ALSPreficed returns ALSTerm: | ||
113 | {ALSNot}=>("!"|'not') operand = ALSBasicRelationTerm | | ||
114 | {ALSInverseRelation}=>"~" operand = ALSBasicRelationTerm | | ||
115 | {AlSTransitiveClosure} "^" operand = ALSBasicRelationTerm | | ||
116 | {ALSReflectiveTransitiveClosure} "*" operand = ALSBasicRelationTerm | | ||
117 | {ALSCardinality} '#' operand = ALSBasicRelationTerm | | ||
118 | {ALSUnaryMinus} =>'-' operand = ALSBasicRelationTerm | | ||
119 | {ALSSum} 'sum' variables+=ALSVariableDeclaration (',' variables+=ALSVariableDeclaration)* '{' expression = ALSTerm '}' | | ||
120 | // {ALSQuantifiedEx} type = ALSMultiplicity | ||
121 | // (disj?='disj')? variables+=ALSVariableDeclaration (',' variables+=ALSVariableDeclaration)* '{' expression = ALSTerm '}' | | ||
122 | {ALSFunctionCall} (referredDefinition=[ALSDefinition]|referredNumericOperator=ALSNumericOperator) '['params+=ALSTerm (',' params+=ALSTerm)*']' | | ||
123 | ALSBasicRelationTerm; | ||
124 | |||
125 | enum ALSNumericOperator: plus|sub|mul|rem|div; | ||
126 | |||
127 | //ALSVariable: name = ALSID; | ||
128 | ALSVariableDeclaration: name=ALSID ':' range = ALSTerm; | ||
129 | |||
130 | ALSBasicRelationTerm returns ALSTerm: | ||
131 | {ALSNone} 'none'| | ||
132 | {ALSIden} 'iden'| | ||
133 | {ALSUniv} 'univ'| | ||
134 | {ALSInt} 'Int' | | ||
135 | {ALSString} 'String' | | ||
136 | {ALSReference} referred = [ALSRelationDeclaration] | | ||
137 | {ALSNumberLiteral} value = INT| | ||
138 | {ALSStringLiteral} value = STRING| | ||
139 | '(' ALSTerm ')' | ||
140 | ; | ||
141 | |||
142 | ////////////////////////////////// | ||
143 | // ALS Commands and scopes | ||
144 | ////////////////////////////////// | ||
145 | ALSRunCommand: | ||
146 | {ALSRunCommand} 'run' '{' '}' ('for' typeScopes+=ALSTypeScope (',' typeScopes+=ALSTypeScope)*)?; | ||
147 | |||
148 | ALSTypeScope: ALSSigScope | ALSIntScope | ALSStringScope; | ||
149 | |||
150 | ALSSigScope: (exactly?='exactly')? number = INT type = [ALSSignatureDeclaration]; | ||
151 | ALSIntScope: number = INT 'Int'; | ||
152 | ALSStringScope: 'exactly' number = INT 'String'; \ No newline at end of file | ||