From 32a4f3392a7d0c44439c0c9b960ef1cfb5e3cc2f Mon Sep 17 00:00:00 2001 From: ArenBabikian Date: Fri, 25 Oct 2019 04:15:39 -0400 Subject: VAMPIRE: post-submission push --- .../hu/bme/mit/inf/dslreasoner/AlloyLanguage.xtext | 152 +++++++++++++++++++++ 1 file changed, 152 insertions(+) create mode 100644 Solvers/Alloy-Solver2/hu.bme.mit.inf.dslreasoner.alloy.language/src/hu/bme/mit/inf/dslreasoner/AlloyLanguage.xtext (limited to 'Solvers/Alloy-Solver2/hu.bme.mit.inf.dslreasoner.alloy.language/src/hu/bme/mit/inf/dslreasoner/AlloyLanguage.xtext') 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 @@ +grammar hu.bme.mit.inf.dslreasoner.AlloyLanguage with org.eclipse.xtext.common.Terminals + +generate alloyLanguage "http://www.bme.hu/mit/inf/dslreasoner/AlloyLanguage" + +ALSDocument: + ( enumDeclarations += ALSEnumDeclaration | + signatureBodies += ALSSignatureBody | + functionDefinitions += ALSFunctionDefinition | + relationDefinitions += ALSRelationDefinition | + factDeclarations += ALSFactDeclaration)+ + runCommand = ALSRunCommand +; + +////////////////////////////////// +// ALS terminals +////////////////////////////////// + +terminal ID: ('a'..'z'|'A'..'Z'|'_') ('a'..'z'|'A'..'Z'|'_'|"'"|'"'|'0'..'9')*; +ALSID: ID; + +enum ALSMultiplicity: all | no | some | lone | one | set; + + +////////////////////////////////// +// ALS types +////////////////////////////////// + +ALSRelationDeclaration: ALSTypeDeclaration | ALSEnumLiteral | ALSFieldDeclaration | ALSVariableDeclaration; + +ALSTypeDeclaration: + ALSEnumDeclaration | ALSSignatureDeclaration +; + +ALSEnumDeclaration: + 'enum' name=ALSID '{' + literal+=ALSEnumLiteral ("," literal+=ALSEnumLiteral)* + '}'; +ALSEnumLiteral: name = ALSID; + +ALSSignatureDeclaration: name = ALSID; + +ALSSignatureBody: + ((multiplicity = ALSMultiplicity?) & (abstract ?= 'abstract')?) + 'sig' + declarations += ALSSignatureDeclaration (',' declarations += ALSSignatureDeclaration)* + (('extends' supertype = [ALSSignatureDeclaration]) + | + ('in' superset += [ALSSignatureDeclaration] ('+' superset += [ALSSignatureDeclaration])*) )? + '{' (fields+=ALSFieldDeclaration ("," fields+=ALSFieldDeclaration)*)? '}' +; + +ALSFieldDeclaration: + name = ALSID ':' (multiplicity = ALSMultiplicity)? type = ALSTerm +; + +ALSDefinition : ALSFunctionDefinition | ALSRelationDefinition; + +ALSFunctionDefinition: + "fun" name = ALSID "[" variables+=ALSVariableDeclaration (',' variables+=ALSVariableDeclaration)* "]" ":" type = ALSTerm + "{" value = ALSTerm "}" +; +ALSRelationDefinition: + "pred" name = ALSID "[" variables+=ALSVariableDeclaration (',' variables+=ALSVariableDeclaration)* "]" + "{" value = ALSTerm "}" +; + +ALSFactDeclaration: {ALSFactDeclaration} 'fact' (name=ALSID)? '{' (term = ALSTerm) '}' ; + +////////////////////////////////// +// ALS terms +////////////////////////////////// +ALSTerm: ALSQuantified; + +ALSQuantified returns ALSTerm: ({ALSQuantifiedEx} type = ALSMultiplicity + (disj?='disj')? variables+=ALSVariableDeclaration (',' variables+=ALSVariableDeclaration)* '{' expression = ALSTerm '}') | ALSOr; + +ALSOr returns ALSTerm: ALSIff ({ALSOr.leftOperand = current} ( "||" | "or" ) rightOperand = ALSIff)?; +ALSIff returns ALSTerm: ALSImpl ({ALSIff.leftOperand = current} ("<=>" | "iff") rightOperand = ALSImpl)?; +ALSImpl returns ALSTerm: ALSAnd ({ALSImpl.leftOperand = current} ("=>" | "implies") rightOperand = ALSAnd ('else' elseOperand = ALSAnd)?)?; +ALSAnd returns ALSTerm: ALSComparison ({ALSAnd.leftOperand = current} ( "&&" | "and" ) rightOperand = ALSComparison)?; + +ALSComparison returns ALSTerm: + ALSOverride + (({ALSEquals.leftOperand = current} "=" | + {ALSNotEquals.leftOperand = current} "!=" | + {ALSSubset.leftOperand = current} "in" | + {ALSLess.leftOperand = current} ">" | + {ALSLeq.leftOperand = current} ">=" | + {ALSMore.leftOperand = current} "<" | + {ALSMeq.leftOperand = current} "<=") + rightOperand = ALSOverride)?; + +ALSOverride returns ALSTerm: ALSRangeRestrictionRight ({ALSOverride.leftOperand = current} '++' rightOperand = ALSRangeRestrictionRight)?; + +ALSRangeRestrictionRight returns ALSTerm: ALSRangeRestrictionLeft ({ALSRangeRestrictionRight.relation = current} ':>' filter = ALSRangeRestrictionLeft)?; +ALSRangeRestrictionLeft returns ALSTerm: ALSJoin ({ALSRangeRestrictionLeft.filter = current} '<:' relation = ALSJoin)?; +ALSJoin returns ALSTerm: ALSMinus ({ALSJoin.leftOperand = current} '.' rightOperand = ALSMinus )*; + +ALSMinus returns ALSTerm: ALSPlus ({ALSMinus.leftOperand = current} '-' rightOperand = ALSPlus)*; +ALSPlus returns ALSTerm: ALSIntersection ({ALSPlus.leftOperand = current} '+' rightOperand = ALSIntersection)*; +ALSIntersection returns ALSTerm: ALSDirectProduct ({ALSIntersection.leftOperand = current} '&' rightOperand = ALSDirectProduct)*; +//ALSMultiply returns ALSTerm: ALSDirectProduct ({ALSMultiply.leftOperand = current} '*' rightOperand = ALSDirectProduct)*; + +ALSDirectProduct returns ALSTerm: + ALSPreficed + ({ALSDirectProduct.leftOperand = current} (leftMultiplicit = ALSMultiplicity)? + '->' + (rightMultiplicit = ALSMultiplicity)? + rightOperand = ALSPreficed)? +; + +ALSPreficed returns ALSTerm: + {ALSNot}=>("!"|'not') operand = ALSBasicRelationTerm | + {ALSInverseRelation}=>"~" operand = ALSBasicRelationTerm | + {AlSTransitiveClosure} "^" operand = ALSBasicRelationTerm | + {ALSReflectiveTransitiveClosure} "*" operand = ALSBasicRelationTerm | + {ALSCardinality} '#' operand = ALSBasicRelationTerm | + {ALSUnaryMinus} =>'-' operand = ALSBasicRelationTerm | + {ALSSum} 'sum' variables+=ALSVariableDeclaration (',' variables+=ALSVariableDeclaration)* '{' expression = ALSTerm '}' | +// {ALSQuantifiedEx} type = ALSMultiplicity +// (disj?='disj')? variables+=ALSVariableDeclaration (',' variables+=ALSVariableDeclaration)* '{' expression = ALSTerm '}' | + {ALSFunctionCall} (referredDefinition=[ALSDefinition]|referredNumericOperator=ALSNumericOperator) '['params+=ALSTerm (',' params+=ALSTerm)*']' | + ALSBasicRelationTerm; + +enum ALSNumericOperator: plus|sub|mul|rem|div; + +//ALSVariable: name = ALSID; +ALSVariableDeclaration: name=ALSID ':' range = ALSTerm; + +ALSBasicRelationTerm returns ALSTerm: + {ALSNone} 'none'| + {ALSIden} 'iden'| + {ALSUniv} 'univ'| + {ALSInt} 'Int' | + {ALSString} 'String' | + {ALSReference} referred = [ALSRelationDeclaration] | + {ALSNumberLiteral} value = INT| + {ALSStringLiteral} value = STRING| + '(' ALSTerm ')' +; + +////////////////////////////////// +// ALS Commands and scopes +////////////////////////////////// +ALSRunCommand: + {ALSRunCommand} 'run' '{' '}' ('for' typeScopes+=ALSTypeScope (',' typeScopes+=ALSTypeScope)*)?; + +ALSTypeScope: ALSSigScope | ALSIntScope | ALSStringScope; + +ALSSigScope: (exactly?='exactly')? number = INT type = [ALSSignatureDeclaration]; +ALSIntScope: number = INT 'Int'; +ALSStringScope: 'exactly' number = INT 'String'; \ No newline at end of file -- cgit v1.2.3-70-g09d2