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. --- .../reasoner/builder/Logic2AlloyLanguageMapper.xtend | 20 +++++++++++++++++++- 1 file changed, 19 insertions(+), 1 deletion(-) (limited to 'Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper.xtend') 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