From b15b3d49ead78c9124a98ab982a4488e4d7bc3d4 Mon Sep 17 00:00:00 2001 From: Kristóf Marussy Date: Tue, 29 Oct 2019 17:32:38 +0100 Subject: Alloy cardinality fixes --- .../alloy/reasoner/builder/RunCommandMapper.xtend | 19 +++++++++++++++---- 1 file changed, 15 insertions(+), 4 deletions(-) (limited to 'Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/RunCommandMapper.xtend') diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/RunCommandMapper.xtend b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/RunCommandMapper.xtend index 494197bc..b74017d8 100644 --- a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/RunCommandMapper.xtend +++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/RunCommandMapper.xtend @@ -9,8 +9,12 @@ import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSString import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSTerm import hu.bme.mit.inf.dslreasoner.alloyLanguage.AlloyLanguageFactory import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition import java.util.List +import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* + class RunCommandMapper { val extension AlloyLanguageFactory factory = AlloyLanguageFactory.eINSTANCE val Logic2AlloyLanguageMapper_Support support = new Logic2AlloyLanguageMapper_Support; @@ -89,16 +93,18 @@ class RunCommandMapper { ] for(upperLimit : config.typeScopes.maxNewElementsByType.entrySet) { - val limit = upperLimit.value + val type = upperLimit.key + val limit = upperLimit.value + getExistingCount(type) if(limit != LogicSolverConfiguration::Unlimited) { - this.typeScopeMapping.addUpperMultiplicity(specification,upperLimit.key,limit,mapper,trace) + this.typeScopeMapping.addUpperMultiplicity(specification,type,limit,mapper,trace) } } for(lowerLimit : config.typeScopes.minNewElementsByType.entrySet) { - val limit = lowerLimit.value + val type = lowerLimit.key + val limit = lowerLimit.value + getExistingCount(type) if(limit != 0) { - this.typeScopeMapping.addLowerMultiplicity(specification,lowerLimit.key,limit,mapper,trace) + this.typeScopeMapping.addLowerMultiplicity(specification,type,limit,mapper,trace) } } @@ -106,6 +112,11 @@ class RunCommandMapper { setStringScope(specification,config,specification.runCommand) } + private def getExistingCount(Type type) { + val existing = type.transitiveClosureStar[it.subtypes].filter(TypeDefinition).map[elements].flatten.toSet + existing.size + } + protected def Boolean setStringScope(ALSDocument specification, AlloySolverConfiguration config, ALSRunCommand it) { if(config.typeScopes.maxNewStrings === LogicSolverConfiguration::Unlimited) { throw new UnsupportedOperationException('''A string scope have to be specified for Alloy!''') -- cgit v1.2.3-54-g00ecf