Random seed added to Alloy config

This adds <random> number of lines to the specification to prevemt alloy
to give the same solution.

3 files changed, 21 insertions, 3 deletions

diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/AlloyAnalyzerConfiguration.xtend b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/AlloyAnalyzerConfiguration.xtend
index cdf21174..992479da 100644
--- a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/AlloyAnalyzerConfiguration.xtend
+++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/AlloyAnalyzerConfiguration.xtend
@@ -8,9 +8,10 @@ class AlloySolverConfiguration extends LogicSolverConfiguration {
         public def setIntScopeFor(int max) {

                 intScope = 31 - Integer.numberOfLeadingZeros(max) + 1

         }*/

-        public var int symmetry = 0 // by default

+        public var int symmetry = 20 // by default

         public var AlloyBackendSolver solver = AlloyBackendSolver.SAT4J

         public var boolean writeToFile = false

+        public var randomise = 0

 }

 

 enum AlloyBackendSolver {

diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/AlloySolver.xtend b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/AlloySolver.xtend
index f5a9510d..a29af455 100644
--- a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/AlloySolver.xtend
+++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/AlloySolver.xtend
@@ -4,7 +4,6 @@ import edu.mit.csail.sdg.alloy4compiler.translator.A4Solution
 import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder.Alloy2LogicMapper

 import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder.AlloyHandler

 import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder.AlloyModelInterpretation

-import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder.AlloyModelInterpretation_TypeInterpretation_FilteredTypes

 import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder.Logic2AlloyLanguageMapper

 import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder.Logic2AlloyLanguageMapperTrace

 import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder.Logic2AlloyLanguageMapper_TypeMapper_FilteredTypes

diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper.xtend b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper.xtend
index ee7c092a..5c16f406 100644
--- a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper.xtend
+++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper.xtend
@@ -97,6 +97,7 @@ class Logic2AlloyLanguageMapper {
                         

                         it.incqueryEngine = ViatraQueryEngine.on(new EMFScope(problem))

                 ]

+                specification.transformRandomisation(config.randomise)

                 

                 typeMapper.transformTypes(problem.types,problem.elements,this,trace)

                 

@@ -146,7 +147,24 @@ class Logic2AlloyLanguageMapper {
                 return new TracedOutput(specification,trace)

         }

         

-

+        def transformRandomisation(ALSDocument document, int randomisation) {

+                if(randomisation !== 0) {

+                        document.signatureBodies += createALSSignatureBody => [

+                                val declaration = createALSSignatureDeclaration => [

+                                        it.name = support.toID(#["language","util","randomseed"])

+                                ]

+                                it.declarations += declaration

+                                it.multiplicity = ALSMultiplicity::ONE

+                                for(i : 1..randomisation) {

+                                        it.fields+=createALSFieldDeclaration => [

+                                                it.name = support.toID(#["language","util","randomseedField",i.toString])

+                                                it.multiplicity = ALSMultiplicity::ONE

+                                                it.type = createALSReference => [referred = declaration]

+                                        ]

+                                }

+                        ]

+                }

+        }

         

         def transformInverseAssertion(InverseRelationAssertion assertion, Logic2AlloyLanguageMapperTrace trace) {

                 val a = assertion.inverseA