Scope unsat benchmarks

9 files changed, 130 insertions, 75 deletions

diff --git a/Tests/hu.bme.mit.inf.dslreasoner.run/configs/FAM_useful_ViatraSolver_polyhedral_typeHierarchy_Clp.json b/Tests/hu.bme.mit.inf.dslreasoner.run/configs/FAM_useful_ViatraSolver_polyhedral_typeHierarchy_Clp.json
deleted file mode 100644
index 1e2d4dd4..00000000
--- a/Tests/hu.bme.mit.inf.dslreasoner.run/configs/FAM_useful_ViatraSolver_polyhedral_typeHierarchy_Clp.json
+++ /dev/null
@@ -1,16 +0,0 @@
-{
-        "inputPath": "initialModels",
-        "outputPath": "outputModels",
-        "timeout": 1200,
-        "saveModels": true,
-        "warmupIterations": 0,
-        "iterations": 5,
-        "domain": "FAM",
-        "scope": "none",
-        "sizes": [500],
-        "solver": "ViatraSolver",
-        "scopePropagator": "polyhedral",
-        "propagatedConstraints": "hints",
-        "polyhedronSolver": "Clp",
-        "scopeHeuristics": "polyhedral"
-}
diff --git a/Tests/hu.bme.mit.inf.dslreasoner.run/configs/Yakindu.json b/Tests/hu.bme.mit.inf.dslreasoner.run/configs/Yakindu.json
new file mode 100644
index 00000000..b602f2fe
--- /dev/null
+++ b/Tests/hu.bme.mit.inf.dslreasoner.run/configs/Yakindu.json
@@ -0,0 +1,13 @@
+{
+        "inputPath": "initialModels",
+        "outputPath": "outputModels",
+        "timeout": 300,
+        "saveModels": true,
+        "saveTemporaryFiles": false,
+        "warmupIterations": 0,
+        "iterations": 30,
+        "domain": "Yakindu",
+        "scope": "unsat",
+        "sizes": [20],
+        "solver": "AlloySolver"
+}
diff --git a/Tests/hu.bme.mit.inf.dslreasoner.run/configs/Yakindu_useful_ViatraSolver_polyhedral_typeHierarchy_Clp.json b/Tests/hu.bme.mit.inf.dslreasoner.run/configs/Yakindu_useful_ViatraSolver_polyhedral_typeHierarchy_Clp.json
deleted file mode 100644
index b4d51684..00000000
--- a/Tests/hu.bme.mit.inf.dslreasoner.run/configs/Yakindu_useful_ViatraSolver_polyhedral_typeHierarchy_Clp.json
+++ /dev/null
@@ -1,17 +0,0 @@
-{
-        "inputPath": "initialModels",
-        "outputPath": "outputModels",
-        "timeout": 1200,
-        "saveModels": false,
-        "saveTemporaryFiles": true,
-        "warmupIterations": 0,
-        "iterations": 5,
-        "domain": "Yakindu",
-        "scope": "none",
-        "sizes": [100],
-        "solver": "ViatraSolver",
-        "scopePropagator": "polyhedral",
-        "propagatedConstraints": "hints",
-        "polyhedronSolver": "Clp",
-        "scopeHeuristic": "polyhedral"
-}
diff --git a/Tests/hu.bme.mit.inf.dslreasoner.run/configs/fs_useful_ViatraSolver_polyhedral_typeHierarchy_Clp.json b/Tests/hu.bme.mit.inf.dslreasoner.run/configs/ecore.json
index a7e29a22..36fb0ea2 100644
--- a/Tests/hu.bme.mit.inf.dslreasoner.run/configs/fs_useful_ViatraSolver_polyhedral_typeHierarchy_Clp.json
+++ b/Tests/hu.bme.mit.inf.dslreasoner.run/configs/ecore.json
@@ -1,13 +1,14 @@
 {
         "inputPath": "initialModels",
         "outputPath": "outputModels",
-        "timeout": 1200,
+        "timeout": 300,
         "saveModels": true,
-        "warmupIterations": 1,
+        "saveTemporaryFiles": false,
+        "warmupIterations": 0,
         "iterations": 1,
-        "domain": "fs",
+        "domain": "ecoreUnsat",
         "scope": "none",
-        "sizes": [50, 100, 150, 200, 250, 300, 350, 400, 450, 500],
+        "sizes": [5, 10, 20, 30, 40, 50],
         "solver": "ViatraSolver",
         "scopePropagator": "polyhedral",
         "propagatedConstraints": "hints",
diff --git a/Tests/hu.bme.mit.inf.dslreasoner.run/configs/ecore_useful_ViatraSolver_polyhedral_typeHierarchy_Clp.json b/Tests/hu.bme.mit.inf.dslreasoner.run/configs/satellite.json
index 72e97957..16abb5d0 100644
--- a/Tests/hu.bme.mit.inf.dslreasoner.run/configs/ecore_useful_ViatraSolver_polyhedral_typeHierarchy_Clp.json
+++ b/Tests/hu.bme.mit.inf.dslreasoner.run/configs/satellite.json
@@ -1,13 +1,14 @@
 {
         "inputPath": "initialModels",
         "outputPath": "outputModels",
-        "timeout": 1200,
+        "timeout": 300,
         "saveModels": true,
+        "saveTemporaryFiles": false,
         "warmupIterations": 0,
-        "iterations": 5,
-        "domain": "ecore",
-        "scope": "quantiles",
-        "sizes": [50],
+        "iterations": 30,
+        "domain": "satelliteUnsat",
+        "scope": "none",
+        "sizes": [10],
         "solver": "ViatraSolver",
         "scopePropagator": "polyhedral",
         "propagatedConstraints": "hints",
diff --git a/Tests/hu.bme.mit.inf.dslreasoner.run/configs/satellite_useful_ViatraSolver_polyhedral_typeHierarchy_Clp.json b/Tests/hu.bme.mit.inf.dslreasoner.run/configs/satellite_useful_ViatraSolver_polyhedral_typeHierarchy_Clp.json
deleted file mode 100644
index d5469948..00000000
--- a/Tests/hu.bme.mit.inf.dslreasoner.run/configs/satellite_useful_ViatraSolver_polyhedral_typeHierarchy_Clp.json
+++ /dev/null
@@ -1,17 +0,0 @@
-{
-        "inputPath": "initialModels",
-        "outputPath": "outputModels",
-        "timeout": 120,
-        "saveModels": true,
-        "saveTemporaryFiles": true,
-        "warmupIterations": 0,
-        "iterations": 1,
-        "domain": "Yakindu",
-        "scope": "quantiles",
-        "sizes": [10, 20, 30, 40, 50, 60, 70, 80, 90, 100],
-        "solver": "ViatraSolver",
-        "scopePropagator": "polyhedral",
-        "propagatedConstraints": "hints",
-        "polyhedronSolver": "Clp",
-        "scopeHeuristic": "polyhedral"
-}
diff --git a/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/MetamodelLoader.xtend b/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/MetamodelLoader.xtend
index 1be03eed..bf9ca274 100644
--- a/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/MetamodelLoader.xtend
+++ b/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/MetamodelLoader.xtend
@@ -40,6 +40,8 @@ class TypeQuantiles {
 }

 

 abstract class MetamodelLoader {

+        public static val UNSAT_PREFIX = "unsat_"

+        

         protected val ReasonerWorkspace workspace

 

         new(ReasonerWorkspace workspace) {

@@ -61,6 +63,10 @@ abstract class MetamodelLoader {
         def Map<String, TypeQuantiles> getTypeQuantiles() {

                 emptyMap

         }

+        

+        def Map<String, TypeQuantiles> getUnsatTypeQuantiles() {

+                throw new UnsupportedOperationException("This domain has no type quantiles for unsatisfiable problems")

+        }

 

         def List<LinearTypeConstraintHint> getHints(Ecore2Logic ecore2Logic, Ecore2Logic_Trace trace) {

                 emptyList

@@ -136,9 +142,15 @@ class YakinduLoader extends MetamodelLoader {
         public static val patternsWithComplexStates = #["outgoingFromExit", "outgoingFromFinal", "choiceHasNoOutgoing",

                 "choiceHasNoIncoming"]

 

+        val boolean satisfiable 

+

         new(ReasonerWorkspace workspace) {

+                this(workspace, true)

+        }

+

+        new(ReasonerWorkspace workspace, boolean satisfiable) {

                 super(workspace)

-                YakindummPackage.eINSTANCE.eClass

+                this.satisfiable = satisfiable

         }

 

         def setUseSynchronization(boolean useSynchronization) {

@@ -173,6 +185,8 @@ class YakinduLoader extends MetamodelLoader {
                         useSynchInThisLoad || !patternsWithSynchronization.exists[spec.fullyQualifiedName.endsWith(it)]

                 ].filter [ spec |

                         useComplexStates || !patternsWithComplexStates.exists[spec.fullyQualifiedName.endsWith(it)]

+                ].filter [

+                        !satisfiable || !it.simpleName.startsWith(UNSAT_PREFIX)

                 ].toList

                 val wfPatterns = patterns.filter[it.allAnnotations.exists[it.name == "Constraint"]].toSet

                 val derivedFeatures = new LinkedHashMap

@@ -213,6 +227,19 @@ class YakinduLoader extends MetamodelLoader {
                         "Transition" -> new TypeQuantiles(0.581632653061224, 0.645161290322581)

                 }

         }

+        

+        override getUnsatTypeQuantiles() {

+                #{

+                        "Choice" -> new TypeQuantiles(0.118279569892473, 0.154020979020979),

+                        "Entry" -> new TypeQuantiles(0.2, 0.4),

+                        "Exit" -> new TypeQuantiles(0, 0),

+                        "FinalState" -> new TypeQuantiles(0, 0),

+                        "Region" -> new TypeQuantiles(0.0294117647058824, 0.0633258678611422),

+                        "State" -> new TypeQuantiles(0.132023636740618, 0.175925925925926),

+//                      "Statechart" -> new TypeQuantiles(0.00961538461538462, 0.010752688172043),

+                        "Transition" -> new TypeQuantiles(0.581632653061224, 0.645161290322581)

+                }

+        }

 

         override getHints(Ecore2Logic ecore2Logic, Ecore2Logic_Trace trace) {

                 #[new SGraphHint(ecore2Logic, trace)]

@@ -276,9 +303,15 @@ class FileSystemLoader extends MetamodelLoader {
 }

 

 class EcoreLoader extends MetamodelLoader {

+        val boolean satisfiable 

 

         new(ReasonerWorkspace workspace) {

+                this(workspace, true)

+        }

+

+        new(ReasonerWorkspace workspace, boolean satisfiable) {

                 super(workspace)

+                this.satisfiable = satisfiable

         }

 

         override loadMetamodel() {

@@ -307,7 +340,12 @@ class EcoreLoader extends MetamodelLoader {
         override loadQueries(EcoreMetamodelDescriptor metamodel) {

                 val patternGroup = Ecore.instance

                 val patterns = patternGroup.specifications.toList

-                val wfPatterns = patterns.filter[it.allAnnotations.exists[it.name == "Constraint"]].toSet

+                val allWfPatterns = patterns.filter[it.allAnnotations.exists[it.name == "Constraint"]].toSet

+                val wfPatterns = if (satisfiable) {

+                        allWfPatterns.filter[!it.simpleName.startsWith(UNSAT_PREFIX)].toSet

+                } else {

+                        allWfPatterns

+                }

                 val derivedFeatures = new HashMap

                 return new ViatraQuerySetDescriptor(

                         patterns,

@@ -346,9 +384,15 @@ class EcoreLoader extends MetamodelLoader {
 }

 

 class SatelliteLoader extends MetamodelLoader {

+        val boolean satisfiable 

 

         new(ReasonerWorkspace workspace) {

+                this(workspace, true)

+        }

+

+        new(ReasonerWorkspace workspace, boolean satisfiable) {

                 super(workspace)

+                this.satisfiable = satisfiable

         }

 

         override loadMetamodel() {

@@ -371,7 +415,9 @@ class SatelliteLoader extends MetamodelLoader {
 

         override loadQueries(EcoreMetamodelDescriptor metamodel) {

                 val i = SatelliteQueriesAll.instance

-                val patterns = i.specifications.toList

+                val patterns = i.specifications.filter [

+                        !satisfiable || !it.simpleName.startsWith(UNSAT_PREFIX)

+                ].toList

                 val wfPatterns = patterns.filter[it.allAnnotations.exists[it.name == "Constraint"]].toSet

                 val derivedFeatures = new LinkedHashMap

                 val res = new ViatraQuerySetDescriptor(

@@ -404,4 +450,15 @@ class SatelliteLoader extends MetamodelLoader {
                 }

         }

 

+        override getUnsatTypeQuantiles() {

+                #{

+                        "CubeSat3U" -> new TypeQuantiles(0.1, 0.25),

+                        "CubeSat6U" -> new TypeQuantiles(0.1, 0.25),

+                        "SmallSat" -> new TypeQuantiles(0.1, 0.25),

+                        "UHFCommSubsystem" -> new TypeQuantiles(0.08, 0.1),

+                        "XCommSubsystem" -> new TypeQuantiles(0, 0.1),

+                        "KaCommSubsystem" -> new TypeQuantiles(0, 0.05),

+                        "InterferometryPayload" -> new TypeQuantiles(0.15, 0.25)

+                }

+        }

 }

diff --git a/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/script/MeasurementScript.xtend b/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/script/MeasurementScript.xtend
index 56a65091..f842afb5 100644
--- a/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/script/MeasurementScript.xtend
+++ b/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/script/MeasurementScript.xtend
@@ -29,19 +29,26 @@ class MeasurementScript {
 enum Domain {
         fs,
         ecore,
+        ecoreUnsat,
         Yakindu,
+        YakinduUnsat,
         FAM,
-        satellite
+        satellite,
+        satelliteUnsat
 }
 
 enum Scope {
         none,
-        quantiles
+        quantiles,
+        upperOnly,
+        unsat,
+        exactly
 }
 
 enum Solver {
         ViatraSolver,
-        AlloySolver
+        AlloySolver,
+        AlloyMiniSat
 }
 
 enum ScopePropagator {
diff --git a/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/script/MeasurementScriptRunner.xtend b/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/script/MeasurementScriptRunner.xtend
index 1127f01a..973c3d13 100644
--- a/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/script/MeasurementScriptRunner.xtend
+++ b/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/script/MeasurementScriptRunner.xtend
@@ -54,6 +54,7 @@ import org.eclipse.viatra.query.patternlanguage.emf.EMFPatternLanguageStandalone
 import org.eclipse.viatra.query.runtime.api.ViatraQueryEngineOptions
 import org.eclipse.viatra.query.runtime.rete.matcher.ReteBackendFactory
 import org.eclipse.xtend.lib.annotations.Data
+import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloyBackendSolver
 
 class MeasurementScriptRunner {
         static val MODEL_SIZE_GAP = 0
@@ -75,9 +76,12 @@ class MeasurementScriptRunner {
                 metamodelLoader = switch (script.domain) {
                         case fs: new FileSystemLoader(inputWorkspace)
                         case ecore: new EcoreLoader(inputWorkspace)
+                        case ecoreUnsat: new EcoreLoader(inputWorkspace, false)
                         case Yakindu: new YakinduLoader(inputWorkspace) => [useSynchronization = false; useComplexStates = true]
+                        case YakinduUnsat: new YakinduLoader(inputWorkspace, false) => [useSynchronization = false; useComplexStates = true]
                         case FAM: new FAMLoader(inputWorkspace)
                         case satellite: new SatelliteLoader(inputWorkspace)
+                        case satelliteUnsat: new SatelliteLoader(inputWorkspace, false)
                         default: throw new IllegalArgumentException("Unsupported domain: " + script.domain)
                 }
         }
@@ -191,15 +195,17 @@ class MeasurementScriptRunner {
                 config
         }
 
-        private def createAlloyConfig() {
+        private def createAlloyConfig(AlloyBackendSolver backendSolver) {
                 val config = new AlloySolverConfiguration
+                config.solver = backendSolver
                 config
         }
 
         private def createConfig(int modelSize) {
                 val config = switch (solver : script.solver) {
                         case ViatraSolver: createViatraConfig()
-                        case AlloySolver: createAlloyConfig()
+                        case AlloySolver: createAlloyConfig(AlloyBackendSolver.SAT4J)
+                        case AlloyMiniSat: createAlloyConfig(AlloyBackendSolver.MiniSatJNI)
                         default: throw new IllegalArgumentException("Unknown solver: " + solver)
                 }
                 config.solutionScope.numberOfRequiredSolutions = 1
@@ -243,7 +249,8 @@ class MeasurementScriptRunner {
 
                 val solver = switch (solver : script.solver) {
                         case ViatraSolver: new ViatraReasoner
-                        case AlloySolver: new AlloySolver
+                        case AlloySolver,
+                        case AlloyMiniSat: new AlloySolver
                         default: throw new IllegalArgumentException("Unknown solver: " + solver)
                 }
                 val result = solver.solve(problem, config, outputWorkspace)
@@ -284,14 +291,31 @@ class MeasurementScriptRunner {
                 } else {
                         val numberOfKnownElements = knownElements.values.flatten.toSet.size
                         val newElementCount = modelSize - numberOfKnownElements
-                        config.typeScopes.minNewElements = newElementCount
-                        config.typeScopes.maxNewElements = newElementCount + MODEL_SIZE_GAP
+                        switch (script.scope) {
+                                case upperOnly:
+                                        config.typeScopes.maxNewElements = newElementCount + MODEL_SIZE_GAP
+                                case exactly: {
+                                        config.typeScopes.minNewElements = newElementCount
+                                        config.typeScopes.maxNewElements = newElementCount
+                                }
+                                default: {
+                                        config.typeScopes.minNewElements = newElementCount
+                                        config.typeScopes.maxNewElements = newElementCount + MODEL_SIZE_GAP
+                                }
+                        }
                 }
-                switch (script.scope) {
-                        case none:
+                switch (scope : script.scope) {
+                        case none,
+                        case exactly:
                                 return
-                        case quantiles: {
-                                val quantiles = metamodelLoader.typeQuantiles
+                        case quantiles,
+                        case unsat,
+                        case upperOnly: {
+                                val quantiles = if (scope == Scope.unsat) {
+                                        metamodelLoader.unsatTypeQuantiles
+                                } else {
+                                        metamodelLoader.typeQuantiles
+                                }
                                 for (eClassInScope : eClassMapper.allClassesInScope(trace)) {
                                         val quantile = quantiles.get(eClassInScope.name)
                                         if (quantile !== null) {
@@ -301,7 +325,9 @@ class MeasurementScriptRunner {
                                                 val lowCount = Math.floor(modelSize * quantile.low) as int
                                                 val highCount = Math.ceil((modelSize + MODEL_SIZE_GAP) * quantile.high) as int
 //                                              println('''«type.name» «lowCount» «highCount»''')
-                                                config.typeScopes.minNewElementsByType.put(type, Math.max(lowCount - currentCount, 0))
+                                                if (script.scope != Scope.upperOnly) {
+                                                        config.typeScopes.minNewElementsByType.put(type, Math.max(lowCount - currentCount, 0))
+                                                }
                                                 config.typeScopes.maxNewElementsByType.put(type, highCount - currentCount)
                                         }
                                 }