diff options
author | 2017-10-27 17:00:25 +0200 | |
---|---|---|
committer | 2017-10-27 17:00:25 +0200 | |
commit | a9f6886b54107970dc8d4f5ff30a1bc5873e6c9b (patch) | |
tree | 033faa20423271d638d9c81e6800e8f167361b63 /Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf | |
parent | Runners (diff) | |
download | VIATRA-Generator-a9f6886b54107970dc8d4f5ff30a1bc5873e6c9b.tar.gz VIATRA-Generator-a9f6886b54107970dc8d4f5ff30a1bc5873e6c9b.tar.zst VIATRA-Generator-a9f6886b54107970dc8d4f5ff30a1bc5873e6c9b.zip |
Random seed added to Alloy config
This adds <random> number of lines to the specification to prevemt alloy
to give the same solution.
Diffstat (limited to 'Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf')
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 { | |||
8 | public def setIntScopeFor(int max) { | 8 | public def setIntScopeFor(int max) { |
9 | intScope = 31 - Integer.numberOfLeadingZeros(max) + 1 | 9 | intScope = 31 - Integer.numberOfLeadingZeros(max) + 1 |
10 | }*/ | 10 | }*/ |
11 | public var int symmetry = 0 // by default | 11 | public var int symmetry = 20 // by default |
12 | public var AlloyBackendSolver solver = AlloyBackendSolver.SAT4J | 12 | public var AlloyBackendSolver solver = AlloyBackendSolver.SAT4J |
13 | public var boolean writeToFile = false | 13 | public var boolean writeToFile = false |
14 | public var randomise = 0 | ||
14 | } | 15 | } |
15 | 16 | ||
16 | enum AlloyBackendSolver { | 17 | 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 | |||
4 | import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder.Alloy2LogicMapper | 4 | import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder.Alloy2LogicMapper |
5 | import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder.AlloyHandler | 5 | import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder.AlloyHandler |
6 | import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder.AlloyModelInterpretation | 6 | import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder.AlloyModelInterpretation |
7 | import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder.AlloyModelInterpretation_TypeInterpretation_FilteredTypes | ||
8 | import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder.Logic2AlloyLanguageMapper | 7 | import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder.Logic2AlloyLanguageMapper |
9 | import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder.Logic2AlloyLanguageMapperTrace | 8 | import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder.Logic2AlloyLanguageMapperTrace |
10 | import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder.Logic2AlloyLanguageMapper_TypeMapper_FilteredTypes | 9 | 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 { | |||
97 | 97 | ||
98 | it.incqueryEngine = ViatraQueryEngine.on(new EMFScope(problem)) | 98 | it.incqueryEngine = ViatraQueryEngine.on(new EMFScope(problem)) |
99 | ] | 99 | ] |
100 | specification.transformRandomisation(config.randomise) | ||
100 | 101 | ||
101 | typeMapper.transformTypes(problem.types,problem.elements,this,trace) | 102 | typeMapper.transformTypes(problem.types,problem.elements,this,trace) |
102 | 103 | ||
@@ -146,7 +147,24 @@ class Logic2AlloyLanguageMapper { | |||
146 | return new TracedOutput(specification,trace) | 147 | return new TracedOutput(specification,trace) |
147 | } | 148 | } |
148 | 149 | ||
149 | 150 | def transformRandomisation(ALSDocument document, int randomisation) { | |
151 | if(randomisation !== 0) { | ||
152 | document.signatureBodies += createALSSignatureBody => [ | ||
153 | val declaration = createALSSignatureDeclaration => [ | ||
154 | it.name = support.toID(#["language","util","randomseed"]) | ||
155 | ] | ||
156 | it.declarations += declaration | ||
157 | it.multiplicity = ALSMultiplicity::ONE | ||
158 | for(i : 1..randomisation) { | ||
159 | it.fields+=createALSFieldDeclaration => [ | ||
160 | it.name = support.toID(#["language","util","randomseedField",i.toString]) | ||
161 | it.multiplicity = ALSMultiplicity::ONE | ||
162 | it.type = createALSReference => [referred = declaration] | ||
163 | ] | ||
164 | } | ||
165 | ] | ||
166 | } | ||
167 | } | ||
150 | 168 | ||
151 | def transformInverseAssertion(InverseRelationAssertion assertion, Logic2AlloyLanguageMapperTrace trace) { | 169 | def transformInverseAssertion(InverseRelationAssertion assertion, Logic2AlloyLanguageMapperTrace trace) { |
152 | val a = assertion.inverseA | 170 | val a = assertion.inverseA |