From a9f6886b54107970dc8d4f5ff30a1bc5873e6c9b Mon Sep 17 00:00:00 2001 From: OszkarSemerath Date: Fri, 27 Oct 2017 17:00:25 +0200 Subject: Random seed added to Alloy config This adds number of lines to the specification to prevemt alloy to give the same solution. --- .../alloy/reasoner/AlloyAnalyzerConfiguration.xtend | 3 ++- .../inf/dlsreasoner/alloy/reasoner/AlloySolver.xtend | 1 - .../reasoner/builder/Logic2AlloyLanguageMapper.xtend | 20 +++++++++++++++++++- 3 files changed, 21 insertions(+), 3 deletions(-) (limited to 'Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme') 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 -- cgit v1.2.3-54-g00ecf