diff options
Diffstat (limited to 'Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner')
5 files changed, 19 insertions, 8 deletions
diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/queries/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/queries/typeQueries.vql b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/queries/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/queries/typeQueries.vql index 8d93cafb..14cf3594 100644 --- a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/queries/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/queries/typeQueries.vql +++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/queries/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/queries/typeQueries.vql | |||
@@ -81,5 +81,5 @@ private pattern typeDoesNotCoverElementOccurance(element: DefinedElement, type: | |||
81 | find supertype(containerType,type); | 81 | find supertype(containerType,type); |
82 | TypeDefinition.elements(containerType,element); | 82 | TypeDefinition.elements(containerType,element); |
83 | TypeDefinition.elements(uncoveredOccurance,element); | 83 | TypeDefinition.elements(uncoveredOccurance,element); |
84 | neg find supertype(uncoveredOccurance,type); | 84 | neg find supertype(type,uncoveredOccurance); |
85 | } \ No newline at end of file | 85 | } \ No newline at end of file |
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!''') |