From e0a3073dd0b3b78d1421cc200567618f99a8206c Mon Sep 17 00:00:00 2001 From: OszkarSemerath Date: Wed, 16 Aug 2017 15:19:47 +0200 Subject: Alloy mapping of integer scopes --- .../reasoner/builder/AlloyModelInterpretation.xtend | 18 ++++++++++++++---- .../reasoner/builder/Logic2AlloyLanguageMapper.xtend | 8 ++++++-- 2 files changed, 20 insertions(+), 6 deletions(-) (limited to 'Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme') diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyModelInterpretation.xtend b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyModelInterpretation.xtend index d00291e0..53674ca3 100644 --- a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyModelInterpretation.xtend +++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyModelInterpretation.xtend @@ -286,10 +286,7 @@ class AlloyModelInterpretation implements LogicModelInterpretation{ override getInterpretation(ConstantDeclaration constant) { constant.lookup(this.constant2Value) } - - override getMinimalInteger() { this.minInt } - override getMaximalInteger() { this.maxInt } - + // Alloy term -> logic term def private atomLabel2Term(String label) { if(label.number) return Integer.parseInt(label) @@ -306,6 +303,19 @@ class AlloyModelInterpretation implements LogicModelInterpretation{ return false } } + + override getAllIntegersInStructure() { + throw new UnsupportedOperationException("TODO: auto-generated method stub") + } + + override getAllRealsInStructure() { + throw new UnsupportedOperationException("TODO: auto-generated method stub") + } + + override getAllStringsInStructure() { + throw new UnsupportedOperationException("TODO: auto-generated method stub") + } + } /** diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper.xtend b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper.xtend index 65fdcfdf..e5c443f6 100644 --- a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper.xtend +++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper.xtend @@ -279,10 +279,14 @@ class Logic2AlloyLanguageMapper { it.number = typeMapper.getUndefinedSupertypeScope(config.typeScopes.maxNewElements,trace) it.exactly = (config.typeScopes.maxNewElements == config.typeScopes.minNewElements) ] - if(config.typeScopes.maxIntScope == LogicSolverConfiguration::Unlimited) throw new UnsupportedOperationException( + if(config.typeScopes.maxNewIntegers == LogicSolverConfiguration::Unlimited) throw new UnsupportedOperationException( '''An integer scope have to be specified for Alloy!''') it.typeScopes += createALSIntScope => [ - number = Integer.SIZE-Integer.numberOfLeadingZeros(config.typeScopes.maxIntScope) + val knownIntegerMax = config.typeScopes.knownIntegers.max + val knownIntegerMin = config.typeScopes.knownIntegers.min + val needNewPlaces = Math.max(knownIntegerMax - knownIntegerMin - config.typeScopes.maxNewIntegers,0) + val maxAbsoluteValue = Math.max(Math.abs(knownIntegerMax)+needNewPlaces+1/2, Math.abs(knownIntegerMin)+needNewPlaces/2) + number = Integer.SIZE-Integer.numberOfLeadingZeros(maxAbsoluteValue) ] // for(definedScope : config.typeScopes.allDefinedScope) { // it.typeScopes += createALSSigScope => [ -- cgit v1.2.3-54-g00ecf