Alloy cardinality fixes

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:
         find supertype(containerType,type);

         TypeDefinition.elements(containerType,element);

         TypeDefinition.elements(uncoveredOccurance,element);

-        neg find supertype(uncoveredOccurance,type);

+        neg find supertype(type,uncoveredOccurance);

 }
\ 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 {
         public def transformOutput(LogicProblem problem, int requiredNumberOfSolution, MonitoredAlloySolution monitoredAlloySolution, Logic2AlloyLanguageMapperTrace trace, long transformationTime) {

                 val models = monitoredAlloySolution.aswers.map[it.key].toList

                 

-                if(!monitoredAlloySolution.finishedBeforeTimeout) {

+                if(models.empty || !monitoredAlloySolution.finishedBeforeTimeout) {

                         return createInsuficientResourcesResult => [

                                 it.problem = problem

                                 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{
                 for(atom: allAtoms) {

                         val typeName = getName(atom.type)

                         val atomName = atom.name

-                        println(atom.toString + "  < -  " + typeName)

+//                      println(atom.toString + "  < -  " + typeName)

                         if(typeName == forwardTrace.logicLanguage.name) {

                                 this.logicLanguage = atom

                         } 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
                 for(type : types.filter[it.supertypes.size>=2]) {

                         trace.specification.factDeclarations += createALSFactDeclaration => [

                                 it.name = support.toIDMultiple("abstract",type.name)

-                                it.term = createALSEquals => [

+                                it.term = createALSSubset => [

                                         it.leftOperand = createALSReference => [ it.referred = type.lookup(typeTrace.type2ALSType) ]

                                         it.rightOperand = support.unfoldIntersection(type.supertypes.map[e|

                                                 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
 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!''')