diff options
author | 2019-10-29 17:32:38 +0100 | |
---|---|---|
committer | 2019-10-29 17:32:38 +0100 | |
commit | b15b3d49ead78c9124a98ab982a4488e4d7bc3d4 (patch) | |
tree | bdc39d57ddf0a31f6f8e87a9b5a6b4ec6136d44e /Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit | |
parent | Remove empty src directories from build path (diff) | |
download | VIATRA-Generator-b15b3d49ead78c9124a98ab982a4488e4d7bc3d4.tar.gz VIATRA-Generator-b15b3d49ead78c9124a98ab982a4488e4d7bc3d4.tar.zst VIATRA-Generator-b15b3d49ead78c9124a98ab982a4488e4d7bc3d4.zip |
Alloy cardinality fixes
Diffstat (limited to 'Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit')
4 files changed, 18 insertions, 7 deletions
diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Alloy2LogicMapper.xtend b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Alloy2LogicMapper.xtend index 2efd6b29..328ca176 100644 --- a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Alloy2LogicMapper.xtend +++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Alloy2LogicMapper.xtend | |||
@@ -9,7 +9,7 @@ class Alloy2LogicMapper { | |||
9 | public def transformOutput(LogicProblem problem, int requiredNumberOfSolution, MonitoredAlloySolution monitoredAlloySolution, Logic2AlloyLanguageMapperTrace trace, long transformationTime) { | 9 | public def transformOutput(LogicProblem problem, int requiredNumberOfSolution, MonitoredAlloySolution monitoredAlloySolution, Logic2AlloyLanguageMapperTrace trace, long transformationTime) { |
10 | val models = monitoredAlloySolution.aswers.map[it.key].toList | 10 | val models = monitoredAlloySolution.aswers.map[it.key].toList |
11 | 11 | ||
12 | if(!monitoredAlloySolution.finishedBeforeTimeout) { | 12 | if(models.empty || !monitoredAlloySolution.finishedBeforeTimeout) { |
13 | return createInsuficientResourcesResult => [ | 13 | return createInsuficientResourcesResult => [ |
14 | it.problem = problem | 14 | it.problem = problem |
15 | it.representation += models | 15 | it.representation += models |
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 107aa001..29eabe2c 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 | |||
@@ -117,7 +117,7 @@ class AlloyModelInterpretation implements LogicModelInterpretation{ | |||
117 | for(atom: allAtoms) { | 117 | for(atom: allAtoms) { |
118 | val typeName = getName(atom.type) | 118 | val typeName = getName(atom.type) |
119 | val atomName = atom.name | 119 | val atomName = atom.name |
120 | println(atom.toString + " < - " + typeName) | 120 | // println(atom.toString + " < - " + typeName) |
121 | if(typeName == forwardTrace.logicLanguage.name) { | 121 | if(typeName == forwardTrace.logicLanguage.name) { |
122 | this.logicLanguage = atom | 122 | this.logicLanguage = atom |
123 | } else if(typeName == "Int" || typeName == "seq/Int") { | 123 | } else if(typeName == "Int" || typeName == "seq/Int") { |
diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper_FilteredTypes.xtend b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper_FilteredTypes.xtend index 397fb84b..ae7a1e6b 100644 --- a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper_FilteredTypes.xtend +++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper_FilteredTypes.xtend | |||
@@ -124,7 +124,7 @@ class Logic2AlloyLanguageMapper_TypeMapper_FilteredTypes implements Logic2AlloyL | |||
124 | for(type : types.filter[it.supertypes.size>=2]) { | 124 | for(type : types.filter[it.supertypes.size>=2]) { |
125 | trace.specification.factDeclarations += createALSFactDeclaration => [ | 125 | trace.specification.factDeclarations += createALSFactDeclaration => [ |
126 | it.name = support.toIDMultiple("abstract",type.name) | 126 | it.name = support.toIDMultiple("abstract",type.name) |
127 | it.term = createALSEquals => [ | 127 | it.term = createALSSubset => [ |
128 | it.leftOperand = createALSReference => [ it.referred = type.lookup(typeTrace.type2ALSType) ] | 128 | it.leftOperand = createALSReference => [ it.referred = type.lookup(typeTrace.type2ALSType) ] |
129 | it.rightOperand = support.unfoldIntersection(type.supertypes.map[e| | 129 | it.rightOperand = support.unfoldIntersection(type.supertypes.map[e| |
130 | createALSReference => [it.referred = e.lookup(typeTrace.type2ALSType)]]) | 130 | createALSReference => [it.referred = e.lookup(typeTrace.type2ALSType)]]) |
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 | |||
9 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSTerm | 9 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSTerm |
10 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.AlloyLanguageFactory | 10 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.AlloyLanguageFactory |
11 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration | 11 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration |
12 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type | ||
13 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition | ||
12 | import java.util.List | 14 | import java.util.List |
13 | 15 | ||
16 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* | ||
17 | |||
14 | class RunCommandMapper { | 18 | class RunCommandMapper { |
15 | val extension AlloyLanguageFactory factory = AlloyLanguageFactory.eINSTANCE | 19 | val extension AlloyLanguageFactory factory = AlloyLanguageFactory.eINSTANCE |
16 | val Logic2AlloyLanguageMapper_Support support = new Logic2AlloyLanguageMapper_Support; | 20 | val Logic2AlloyLanguageMapper_Support support = new Logic2AlloyLanguageMapper_Support; |
@@ -89,16 +93,18 @@ class RunCommandMapper { | |||
89 | ] | 93 | ] |
90 | 94 | ||
91 | for(upperLimit : config.typeScopes.maxNewElementsByType.entrySet) { | 95 | for(upperLimit : config.typeScopes.maxNewElementsByType.entrySet) { |
92 | val limit = upperLimit.value | 96 | val type = upperLimit.key |
97 | val limit = upperLimit.value + getExistingCount(type) | ||
93 | if(limit != LogicSolverConfiguration::Unlimited) { | 98 | if(limit != LogicSolverConfiguration::Unlimited) { |
94 | this.typeScopeMapping.addUpperMultiplicity(specification,upperLimit.key,limit,mapper,trace) | 99 | this.typeScopeMapping.addUpperMultiplicity(specification,type,limit,mapper,trace) |
95 | } | 100 | } |
96 | } | 101 | } |
97 | 102 | ||
98 | for(lowerLimit : config.typeScopes.minNewElementsByType.entrySet) { | 103 | for(lowerLimit : config.typeScopes.minNewElementsByType.entrySet) { |
99 | val limit = lowerLimit.value | 104 | val type = lowerLimit.key |
105 | val limit = lowerLimit.value + getExistingCount(type) | ||
100 | if(limit != 0) { | 106 | if(limit != 0) { |
101 | this.typeScopeMapping.addLowerMultiplicity(specification,lowerLimit.key,limit,mapper,trace) | 107 | this.typeScopeMapping.addLowerMultiplicity(specification,type,limit,mapper,trace) |
102 | } | 108 | } |
103 | } | 109 | } |
104 | 110 | ||
@@ -106,6 +112,11 @@ class RunCommandMapper { | |||
106 | setStringScope(specification,config,specification.runCommand) | 112 | setStringScope(specification,config,specification.runCommand) |
107 | } | 113 | } |
108 | 114 | ||
115 | private def getExistingCount(Type type) { | ||
116 | val existing = type.transitiveClosureStar[it.subtypes].filter(TypeDefinition).map[elements].flatten.toSet | ||
117 | existing.size | ||
118 | } | ||
119 | |||
109 | protected def Boolean setStringScope(ALSDocument specification, AlloySolverConfiguration config, ALSRunCommand it) { | 120 | protected def Boolean setStringScope(ALSDocument specification, AlloySolverConfiguration config, ALSRunCommand it) { |
110 | if(config.typeScopes.maxNewStrings === LogicSolverConfiguration::Unlimited) { | 121 | if(config.typeScopes.maxNewStrings === LogicSolverConfiguration::Unlimited) { |
111 | throw new UnsupportedOperationException('''A string scope have to be specified for Alloy!''') | 122 | throw new UnsupportedOperationException('''A string scope have to be specified for Alloy!''') |