aboutsummaryrefslogtreecommitdiffstats
path: root/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner
diff options
context:
space:
mode:
authorLibravatar OszkarSemerath <oszka@152.66.252.189>2017-06-10 19:05:05 +0200
committerLibravatar OszkarSemerath <oszka@152.66.252.189>2017-06-10 19:05:05 +0200
commit60f01f46ba232ed6416054f0a6115cb2a9b70b4e (patch)
tree5edf8aeb07abc51f3fec63bbd15c926e1de09552 /Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner
parentInitial commit, migrating from SVN (diff)
downloadVIATRA-Generator-60f01f46ba232ed6416054f0a6115cb2a9b70b4e.tar.gz
VIATRA-Generator-60f01f46ba232ed6416054f0a6115cb2a9b70b4e.tar.zst
VIATRA-Generator-60f01f46ba232ed6416054f0a6115cb2a9b70b4e.zip
Migrating Additional projects
Diffstat (limited to 'Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner')
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/.classpath9
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/.gitignore2
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/.project34
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/.settings/org.eclipse.jdt.core.prefs7
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/META-INF/MANIFEST.MF23
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/build.properties5
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ModelGenerationMethodBasedGlobalConstraint.xtend11
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasoner.xtend205
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasonerConfiguration.xtend42
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/diversity/StateCodeCoverageComparator.xtend8
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/BestFirstStrategyForModelGeneration.java372
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ModelGenerationCompositeObjective.xtend85
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/PartialModelAsLogicInterpretation.xtend30
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ScopeObjective.xtend41
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/SolutionStoreWithCopy.xtend35
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/SolutionStoreWithDiversityDescriptor.xtend77
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/UnfinishedMultiplicityObjective.xtend37
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/UnfinishedWFObjective.xtend56
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/WF2ObjectiveConverter.xtend36
19 files changed, 1115 insertions, 0 deletions
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/.classpath b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/.classpath
new file mode 100644
index 00000000..2b46fc9b
--- /dev/null
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/.classpath
@@ -0,0 +1,9 @@
1<?xml version="1.0" encoding="UTF-8"?>
2<classpath>
3 <classpathentry kind="con" path="org.eclipse.jdt.launching.JRE_CONTAINER/org.eclipse.jdt.internal.debug.ui.launcher.StandardVMType/JavaSE-1.8"/>
4 <classpathentry kind="con" path="org.eclipse.pde.core.requiredPlugins"/>
5 <classpathentry kind="src" path="src"/>
6 <classpathentry kind="src" path="xtend-gen"/>
7 <classpathentry kind="src" path="src-gen/"/>
8 <classpathentry kind="output" path="bin"/>
9</classpath>
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/.gitignore b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/.gitignore
new file mode 100644
index 00000000..b33f6aff
--- /dev/null
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/.gitignore
@@ -0,0 +1,2 @@
1/bin/
2/xtend-gen/
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/.project b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/.project
new file mode 100644
index 00000000..712083e9
--- /dev/null
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/.project
@@ -0,0 +1,34 @@
1<?xml version="1.0" encoding="UTF-8"?>
2<projectDescription>
3 <name>hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner</name>
4 <comment></comment>
5 <projects>
6 </projects>
7 <buildSpec>
8 <buildCommand>
9 <name>org.eclipse.xtext.ui.shared.xtextBuilder</name>
10 <arguments>
11 </arguments>
12 </buildCommand>
13 <buildCommand>
14 <name>org.eclipse.jdt.core.javabuilder</name>
15 <arguments>
16 </arguments>
17 </buildCommand>
18 <buildCommand>
19 <name>org.eclipse.pde.ManifestBuilder</name>
20 <arguments>
21 </arguments>
22 </buildCommand>
23 <buildCommand>
24 <name>org.eclipse.pde.SchemaBuilder</name>
25 <arguments>
26 </arguments>
27 </buildCommand>
28 </buildSpec>
29 <natures>
30 <nature>org.eclipse.pde.PluginNature</nature>
31 <nature>org.eclipse.jdt.core.javanature</nature>
32 <nature>org.eclipse.xtext.ui.shared.xtextNature</nature>
33 </natures>
34</projectDescription>
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/.settings/org.eclipse.jdt.core.prefs b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/.settings/org.eclipse.jdt.core.prefs
new file mode 100644
index 00000000..295926d9
--- /dev/null
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/.settings/org.eclipse.jdt.core.prefs
@@ -0,0 +1,7 @@
1eclipse.preferences.version=1
2org.eclipse.jdt.core.compiler.codegen.inlineJsrBytecode=enabled
3org.eclipse.jdt.core.compiler.codegen.targetPlatform=1.8
4org.eclipse.jdt.core.compiler.compliance=1.8
5org.eclipse.jdt.core.compiler.problem.assertIdentifier=error
6org.eclipse.jdt.core.compiler.problem.enumIdentifier=error
7org.eclipse.jdt.core.compiler.source=1.8
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/META-INF/MANIFEST.MF b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/META-INF/MANIFEST.MF
new file mode 100644
index 00000000..bc965aa4
--- /dev/null
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/META-INF/MANIFEST.MF
@@ -0,0 +1,23 @@
1Manifest-Version: 1.0
2Bundle-ManifestVersion: 2
3Bundle-Name: Reasoner
4Bundle-SymbolicName: hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner
5Bundle-Version: 1.0.0.qualifier
6Export-Package: hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner
7Require-Bundle: hu.bme.mit.inf.dslreasoner.ecore2logic;bundle-version="1.0.0",
8 hu.bme.mit.inf.dslreasoner.logic.model;bundle-version="1.0.0",
9 hu.bme.mit.inf.dslreasoner.viatra2logic;bundle-version="1.0.0",
10 hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatraquery;bundle-version="1.0.0",
11 hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage;bundle-version="1.0.0",
12 hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic;bundle-version="1.0.0",
13 com.google.guava,
14 org.eclipse.xtext.xbase.lib,
15 org.eclipse.xtend.lib,
16 org.eclipse.xtend.lib.macro,
17 org.eclipse.viatra.query.runtime.matchers;bundle-version="1.5.0",
18 org.eclipse.viatra.query.runtime;bundle-version="1.5.0",
19 org.eclipse.viatra.dse;bundle-version="0.15.0",
20 org.eclipse.viatra.dse.genetic;bundle-version="0.15.0",
21 org.eclipse.emf.ecore.edit;bundle-version="2.9.0"
22Bundle-RequiredExecutionEnvironment: JavaSE-1.8
23Import-Package: org.apache.log4j
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/build.properties b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/build.properties
new file mode 100644
index 00000000..aed85a48
--- /dev/null
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/build.properties
@@ -0,0 +1,5 @@
1bin.includes = META-INF/,\
2 .
3source.. = src/,\
4 src-gen/
5output.. = bin/
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ModelGenerationMethodBasedGlobalConstraint.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ModelGenerationMethodBasedGlobalConstraint.xtend
new file mode 100644
index 00000000..28cf986d
--- /dev/null
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ModelGenerationMethodBasedGlobalConstraint.xtend
@@ -0,0 +1,11 @@
1package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner
2
3import org.eclipse.viatra.dse.objectives.IGlobalConstraint
4import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationMethod
5
6abstract class ModelGenerationMethodBasedGlobalConstraint implements IGlobalConstraint {
7 val protected ModelGenerationMethod method
8 new(ModelGenerationMethod method) {
9 this.method = method
10 }
11} \ No newline at end of file
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasoner.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasoner.xtend
new file mode 100644
index 00000000..38cc9459
--- /dev/null
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasoner.xtend
@@ -0,0 +1,205 @@
1package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner
2
3import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner
4import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasonerException
5import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration
6import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LogiclanguagePackage
7import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem
8import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicproblemPackage
9import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicresultFactory
10import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult
11import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationMethodProvider
12import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.PartialInterpretationInitialiser
13import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialinterpretationPackage
14import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.statecoder.IdentifierBasedStateCoderFactory
15import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.statecoder.NeighbourhoodBasedStateCoderFactory
16import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.BestFirstStrategyForModelGeneration
17import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.ModelGenerationCompositeObjective
18import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.PartialModelAsLogicInterpretation
19import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.ScopeObjective
20import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.UnfinishedMultiplicityObjective
21import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.UnfinishedWFObjective
22import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.WF2ObjectiveConverter
23import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace
24import org.eclipse.viatra.dse.api.DesignSpaceExplorer
25import org.eclipse.viatra.dse.api.DesignSpaceExplorer.DseLoggingLevel
26import org.eclipse.viatra.dse.solutionstore.SolutionStore
27import org.eclipse.viatra.dse.statecode.IStateCoderFactory
28
29class ViatraReasoner extends LogicReasoner{
30 val PartialInterpretationInitialiser initialiser = new PartialInterpretationInitialiser()
31 val ModelGenerationMethodProvider modelGenerationMethodProvider = new ModelGenerationMethodProvider
32 val extension LogicresultFactory factory = LogicresultFactory.eINSTANCE
33 val WF2ObjectiveConverter wf2ObjectiveConverter = new WF2ObjectiveConverter
34
35 val LogicReasoner inconsistencyDetector
36
37 public new() {
38 this.inconsistencyDetector=null
39 }
40
41 public new(LogicReasoner inconsistencyDetector) {
42 this.inconsistencyDetector = inconsistencyDetector
43 }
44
45 override solve(LogicProblem problem, LogicSolverConfiguration configuration, ReasonerWorkspace workspace) throws LogicReasonerException {
46 val viatraConfig = configuration.asConfig
47 val DesignSpaceExplorer dse = new DesignSpaceExplorer();
48
49 /*
50 DesignSpaceExplorer.turnOnLogging(DseLoggingLevel.VERBOSE_FULL)
51 /*/
52 DesignSpaceExplorer.turnOnLogging(DseLoggingLevel.WARN)
53 //*/
54
55 dse.addMetaModelPackage(LogiclanguagePackage.eINSTANCE)
56 dse.addMetaModelPackage(LogicproblemPackage.eINSTANCE)
57 dse.addMetaModelPackage(PartialinterpretationPackage.eINSTANCE)
58
59 val transformationStartTime = System.nanoTime
60
61 val emptySolution = initialiser.initialisePartialInterpretation(problem,
62 viatraConfig.typeScopes.minNewElements,
63 viatraConfig.typeScopes.maxNewElements).output
64 emptySolution.problemConainer = problem
65
66 val method = modelGenerationMethodProvider.createModelGenerationMethod(
67 problem,
68 emptySolution,
69 viatraConfig.existingQueries,
70 workspace,
71 viatraConfig.nameNewElements,
72 viatraConfig.typeInferenceMethod
73 )
74
75 dse.addObjective(new ModelGenerationCompositeObjective(
76 new ScopeObjective,
77 method.unfinishedMultiplicities.map[new UnfinishedMultiplicityObjective(it)],
78 new UnfinishedWFObjective(method.unfinishedWF)
79 ))
80
81 dse.addGlobalConstraint(wf2ObjectiveConverter.createInvalidationObjective(method.invalidWF))
82 for(additionalConstraint : configuration.asConfig.additionalGlobalConstraints) {
83 dse.addGlobalConstraint(additionalConstraint.apply(method))
84 }
85
86 dse.setInitialModel(emptySolution)
87
88 var IStateCoderFactory statecoder = if(viatraConfig.stateCoderStrategy == StateCoderStrategy.Neighbourhood) {
89 new NeighbourhoodBasedStateCoderFactory
90 } else {
91 new IdentifierBasedStateCoderFactory
92 }
93 dse.stateCoderFactory = statecoder
94
95 dse.maxNumberOfThreads = 1
96
97 val solutionStore = new SolutionStore(configuration.solutionScope.numberOfRequiredSolution)
98 dse.solutionStore = solutionStore
99
100 for(rule : method.relationRefinementRules) {
101 dse.addTransformationRule(rule)
102 }
103 for(rule : method.objectRefinementRules) {
104 dse.addTransformationRule(rule)
105 }
106
107 val strategy = new BestFirstStrategyForModelGeneration(
108 workspace,inconsistencyDetector,
109 viatraConfig.inconsistencDetectorConfiguration,
110 viatraConfig.diversityRequirement)
111
112 val transformationTime = System.nanoTime - transformationStartTime
113 val solverStartTime = System.nanoTime
114 var boolean stoppedByTimeout
115 var boolean stoppedByException
116 try{
117 stoppedByTimeout = dse.startExplorationWithTimeout(strategy,configuration.runtimeLimit*1000);
118 stoppedByException = false
119 } catch (NullPointerException npe) {
120 stoppedByTimeout = false
121 stoppedByException = true
122 }
123
124 val solverTime = System.nanoTime - solverStartTime
125
126 val statecoderFinal = statecoder
127 val statistics = createStatistics => [
128 //it.solverTime = viatraConfig.runtimeLimit
129 it.solverTime = (solverTime/1000000) as int
130 it.transformationTime = (transformationTime/1000000) as int
131 it.entries += createIntStatisticEntry => [
132 it.name = "TransformationExecutionTime" it.value = (method.statistics.transformationExecutionTime/1000000) as int
133 ]
134 it.entries += createIntStatisticEntry => [
135 it.name = "TypeAnalysisTime" it.value = (method.statistics.PreliminaryTypeAnalisisTime/1000000) as int
136 ]
137 it.entries += createIntStatisticEntry => [
138 it.name = "StateCoderTime" it.value = (statecoderFinal.runtime/1000000) as int
139 ]
140 it.entries += createIntStatisticEntry => [
141 it.name = "StateCoderFailCount" it.value = strategy.numberOfStatecoderFaiL
142 ]
143 it.entries += createIntStatisticEntry => [
144 it.name = "SolutionCopyTime" it.value = (strategy.solutionStoreWithCopy.sumRuntime/1000000) as int
145 ]
146 if(strategy.solutionStoreWithDiversityDescriptor.isActive) {
147 it.entries += createIntStatisticEntry => [
148 it.name = "SolutionDiversityCheckTime" it.value = (strategy.solutionStoreWithDiversityDescriptor.sumRuntime/1000000) as int
149 ]
150 it.entries += createRealStatisticEntry => [
151 it.name = "SolutionDiversitySuccessRate" it.value = strategy.solutionStoreWithDiversityDescriptor.successRate
152 ]
153 }
154 ]
155
156 if(stoppedByTimeout) {
157 return createInsuficientResourcesResult=>[
158 it.problem = problem
159 it.resourceName="time"
160 it.statistics = statistics
161 ]
162 } else {
163 if(solutionStore.solutions.empty) {
164 return createInconsistencyResult => [
165 it.problem = problem
166 it.statistics = statistics
167 ]
168 } else {
169
170 /*solutionStore.solutions.head.trajectories.head
171 solutionTrajectory.doTransformation(emptySolution)
172 *
173 */
174 return factory.createModelResult => [
175 it.problem = problem
176 it.trace = null
177 it.representation += strategy.solutionStoreWithCopy.solutions
178 it.statistics = statistics
179 ]
180 }
181 }
182 }
183
184 /*private def simpleWeithts(List<IObjective> objectives) {
185 objectives.map[1.0].toList
186 }*/
187
188 private def dispatch long runtime(NeighbourhoodBasedStateCoderFactory sc) {
189 sc.sumStatecoderRuntime
190 }
191
192 private def dispatch long runtime(IdentifierBasedStateCoderFactory sc) {
193 sc.sumStatecoderRuntime
194 }
195
196 override getInterpretation(ModelResult modelResult) {
197 return new PartialModelAsLogicInterpretation
198 }
199
200 def ViatraReasonerConfiguration asConfig(LogicSolverConfiguration configuration) {
201 if(configuration instanceof ViatraReasonerConfiguration) {
202 return configuration
203 } else throw new IllegalArgumentException('''Wrong configuration. Expected: «ViatraReasonerConfiguration.name», but got: «configuration.class.name»"''')
204 }
205}
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasonerConfiguration.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasonerConfiguration.xtend
new file mode 100644
index 00000000..d638dd71
--- /dev/null
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasonerConfiguration.xtend
@@ -0,0 +1,42 @@
1package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner
2
3import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration
4import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration
5import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDeclaration
6import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationMethod
7import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.TypeInferenceMethod
8import java.util.LinkedList
9import java.util.List
10import java.util.Set
11import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery
12import org.eclipse.xtext.xbase.lib.Functions.Function1
13
14public enum StateCoderStrategy {
15 Neighbourhood, NeighbourhoodWithEquivalence, IDBased, DefinedByDiversity
16}
17
18class ViatraReasonerConfiguration extends LogicSolverConfiguration{
19 public var Iterable<PQuery> existingQueries
20 public var LogicSolverConfiguration inconsistencDetectorConfiguration = null
21 public var List<Function1<ModelGenerationMethod,ModelGenerationMethodBasedGlobalConstraint>> additionalGlobalConstraints = new LinkedList
22 int maxDepth = -1
23
24 public var TypeInferenceMethod typeInferenceMethod = TypeInferenceMethod.Generic
25
26 public var nameNewElements = false
27 public var StateCoderStrategy stateCoderStrategy = StateCoderStrategy.Neighbourhood
28
29 /**
30 * Describes the required diversity between the solutions.
31 * Null means that the solutions have to have different state codes only.
32 */
33 public var DiversityDescriptor diversityRequirement = null
34}
35
36public class DiversityDescriptor {
37 public var int range = -1
38 public var int parallels = Integer.MAX_VALUE
39 public var int maxNumber = Integer.MAX_VALUE
40 public var Set<TypeDeclaration> relevantTypes
41 public var Set<RelationDeclaration> relevantRelations
42} \ No newline at end of file
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/diversity/StateCodeCoverageComparator.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/diversity/StateCodeCoverageComparator.xtend
new file mode 100644
index 00000000..9a9446ba
--- /dev/null
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/diversity/StateCodeCoverageComparator.xtend
@@ -0,0 +1,8 @@
1package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.diversity
2
3abstract class StateCodeCoverageComparator<StateCodeType>{
4 def public boolean covers(Object superStateCode, Object subStateCode) {
5 return innerCover(superStateCode as StateCodeType, subStateCode as StateCodeType)
6 }
7 abstract def protected boolean innerCover(StateCodeType superStateCode, StateCodeType subStateCode)
8} \ No newline at end of file
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/BestFirstStrategyForModelGeneration.java b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/BestFirstStrategyForModelGeneration.java
new file mode 100644
index 00000000..5a6fee2c
--- /dev/null
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/BestFirstStrategyForModelGeneration.java
@@ -0,0 +1,372 @@
1/*******************************************************************************
2 * Copyright (c) 2010-2017, Andras Szabolcs Nagy and Daniel Varro
3 * All rights reserved. This program and the accompanying materials
4 * are made available under the terms of the Eclipse Public License v1.0
5 * which accompanies this distribution, and is available at
6 * http://www.eclipse.org/legal/epl-v10.html
7 * Contributors:
8 * Andras Szabolcs Nagy - initial API and implementation
9 *******************************************************************************/
10package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse;
11
12import java.util.ArrayList;
13import java.util.Arrays;
14import java.util.Collections;
15import java.util.Comparator;
16import java.util.Iterator;
17import java.util.List;
18import java.util.PriorityQueue;
19import java.util.Random;
20
21import org.apache.log4j.Logger;
22import org.eclipse.viatra.dse.api.strategy.interfaces.IStrategy;
23import org.eclipse.viatra.dse.base.ThreadContext;
24import org.eclipse.viatra.dse.objectives.Fitness;
25import org.eclipse.viatra.dse.objectives.ObjectiveComparatorHelper;
26import org.eclipse.viatra.dse.solutionstore.SolutionStore;
27
28import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner;
29import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration;
30import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult;
31import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic.PartialInterpretation2Logic;
32import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation;
33import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.visualisation.PartialInterpretation2Gml;
34import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.DiversityDescriptor;
35import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace;
36
37/**
38 * This exploration strategy eventually explorers the whole design space but goes in the most promising directions
39 * first, based on the {@link Fitness}.
40 *
41 * There are a few parameter to tune such as
42 * <ul>
43 * <li>maximum depth</li>
44 * <li>continue the exploration from a state that satisfies the hard objectives (the default that it will
45 * backtrack),</li>
46 * <li>whether to continue the exploration from the newly explored state if it is at least equally good than the
47 * previous one or only if it is better (default is "at least equally good").</li>
48 * </ul>
49 *
50 * @author Andras Szabolcs Nagy
51 *
52 */
53public class BestFirstStrategyForModelGeneration implements IStrategy {
54
55 private ThreadContext context;
56 private SolutionStore solutionStore;
57 private SolutionStoreWithCopy solutionStoreWithCopy;
58 private SolutionStoreWithDiversityDescriptor solutionStoreWithDiversityDescriptor;
59 private int numberOfStatecoderFail=0;
60
61 private int maxDepth = Integer.MAX_VALUE;
62 private boolean isInterrupted = false;
63 //private boolean backTrackIfSolution = true;
64 private boolean onlyBetterFirst = false;
65
66 private PriorityQueue<TrajectoryWithFitness> trajectoiresToExplore;
67 private Logger logger = Logger.getLogger(IStrategy.class);
68
69 private static class TrajectoryWithFitness {
70
71 public Object[] trajectory;
72 public Fitness fitness;
73
74 public TrajectoryWithFitness(Object[] trajectory, Fitness fitness) {
75 super();
76 this.trajectory = trajectory;
77 this.fitness = fitness;
78 }
79
80 @Override
81 public String toString() {
82 return Arrays.toString(trajectory) + fitness.toString();
83 }
84
85 }
86
87 public BestFirstStrategyForModelGeneration(ReasonerWorkspace workspace, LogicReasoner reasoner, LogicSolverConfiguration configuration, DiversityDescriptor descriptor) {
88 this.maxDepth = Integer.MAX_VALUE;
89 this.workspace = workspace;
90 this.reasoner = reasoner;
91 this.configuration = configuration;
92 this.solutionStoreWithDiversityDescriptor = new SolutionStoreWithDiversityDescriptor(descriptor);
93 }
94
95 @Override
96 public void initStrategy(ThreadContext context) {
97 this.context = context;
98 this.solutionStore = context.getGlobalContext().getSolutionStore();
99 this.solutionStoreWithCopy = new SolutionStoreWithCopy();
100
101
102 final ObjectiveComparatorHelper objectiveComparatorHelper = context.getObjectiveComparatorHelper();
103
104 Comparator<TrajectoryWithFitness> comparator = new Comparator<BestFirstStrategyForModelGeneration.TrajectoryWithFitness>() {
105
106 @Override
107 public int compare(TrajectoryWithFitness o1, TrajectoryWithFitness o2) {
108 return objectiveComparatorHelper.compare(o2.fitness, o1.fitness);
109 }
110 };
111
112 trajectoiresToExplore = new PriorityQueue<TrajectoryWithFitness>(11, comparator);
113
114 }
115
116 public SolutionStoreWithCopy getSolutionStoreWithCopy() {
117 return solutionStoreWithCopy;
118 }
119
120 public SolutionStoreWithDiversityDescriptor getSolutionStoreWithDiversityDescriptor() {
121 return solutionStoreWithDiversityDescriptor;
122 }
123
124 public int getNumberOfStatecoderFaiL() {
125 return numberOfStatecoderFail;
126 }
127
128 @Override
129 public void explore() {
130 final ObjectiveComparatorHelper objectiveComparatorHelper = context.getObjectiveComparatorHelper();
131
132 boolean globalConstraintsAreSatisfied = context.checkGlobalConstraints();
133 if (!globalConstraintsAreSatisfied) {
134 logger.info("Global contraint is not satisifed in the first state. Terminate.");
135 return;
136 }
137
138 final Fitness firstFittness = context.calculateFitness();
139 if (firstFittness.isSatisifiesHardObjectives()) {
140 context.newSolution();
141 logger.info("First state is a solution. Terminate.");
142 return;
143 }
144
145 if (maxDepth == 0) {
146 return;
147 }
148
149 final Object[] firstTrajectory = context.getTrajectory().toArray(new Object[0]);
150 TrajectoryWithFitness currentTrajectoryWithFittness = new TrajectoryWithFitness(firstTrajectory, firstFittness);
151 trajectoiresToExplore.add(currentTrajectoryWithFittness);
152
153 mainLoop: while (!isInterrupted) {
154
155 if (currentTrajectoryWithFittness == null) {
156 if (trajectoiresToExplore.isEmpty()) {
157 logger.debug("State space is fully traversed.");
158 return;
159 } else {
160 currentTrajectoryWithFittness = selectRandomState();// trajectoiresToExplore.element();
161 if (logger.isDebugEnabled()) {
162 logger.debug("Current trajectory: " + Arrays.toString(context.getTrajectory().toArray()));
163 logger.debug("New trajectory is chosen: " + currentTrajectoryWithFittness);
164 }
165// context.backtrackUntilRoot();
166// context.executeTrajectoryWithoutStateCoding(currentTrajectoryWithFittness.trajectory);
167 context.getDesignSpaceManager().executeTrajectoryWithMinimalBacktrackWithoutStateCoding(currentTrajectoryWithFittness.trajectory);
168 }
169
170 }
171
172 List<Object> activationIds;
173 try {
174 activationIds = new ArrayList<Object>(context.getUntraversedActivationIds());
175 Collections.shuffle(activationIds);
176 } catch (NullPointerException e) {
177 numberOfStatecoderFail++;
178 activationIds = Collections.emptyList();
179 }
180
181 Iterator<Object> iterator = activationIds.iterator();
182
183// writeCurrentState();
184// boolean consistencyCheckResult = checkConsistency(currentTrajectoryWithFittness);
185// if(consistencyCheckResult == true) {
186// continue mainLoop;
187// }
188
189 while (!isInterrupted && iterator.hasNext()) {
190 final Object nextActivation = iterator.next();
191 if (!iterator.hasNext()) {
192 logger.debug("Last untraversed activation of the state.");
193 trajectoiresToExplore.remove(currentTrajectoryWithFittness);
194 }
195
196 if (logger.isDebugEnabled()) {
197 logger.debug("Executing new activation: " + nextActivation);
198 }
199 context.executeAcitvationId(nextActivation);
200
201// writeCurrentState();
202
203 if (context.isCurrentStateAlreadyTraversed()) {
204 logger.info("The new state is already visited.");
205 context.backtrack();
206 } else if (!context.checkGlobalConstraints()) {
207 logger.debug("Global contraint is not satisifed.");
208 context.backtrack();
209 } else {
210 final Fitness nextFitness = context.calculateFitness();
211 if (nextFitness.isSatisifiesHardObjectives()) {
212 if(solutionStoreWithDiversityDescriptor.isDifferent(context)) {
213 solutionStoreWithCopy.newSolution(context);
214 solutionStoreWithDiversityDescriptor.newSolution(context);
215 solutionStore.newSolution(context);
216 logger.debug("Found a solution.");
217 }
218 }
219 if (context.getDepth() > maxDepth) {
220 logger.debug("Reached max depth.");
221 context.backtrack();
222 continue;
223 }
224
225 TrajectoryWithFitness nextTrajectoryWithFittness = new TrajectoryWithFitness(
226 context.getTrajectory().toArray(), nextFitness);
227 trajectoiresToExplore.add(nextTrajectoryWithFittness);
228
229 int compare = objectiveComparatorHelper.compare(currentTrajectoryWithFittness.fitness,
230 nextTrajectoryWithFittness.fitness);
231 if (compare < 0) {
232 logger.debug("Better fitness, moving on: " + nextFitness);
233 currentTrajectoryWithFittness = nextTrajectoryWithFittness;
234 continue mainLoop;
235 } else if (compare == 0) {
236 if (onlyBetterFirst) {
237 logger.debug("Equally good fitness, backtrack: " + nextFitness);
238 context.backtrack();
239 continue;
240 } else {
241 logger.debug("Equally good fitness, moving on: " + nextFitness);
242 currentTrajectoryWithFittness = nextTrajectoryWithFittness;
243 continue mainLoop;
244 }
245 } else {
246 logger.debug("Worse fitness.");
247// context.backtrack();
248 currentTrajectoryWithFittness = null;
249 continue mainLoop;
250 }
251 }
252 }
253
254 logger.debug("State is fully traversed.");
255 trajectoiresToExplore.remove(currentTrajectoryWithFittness);
256 currentTrajectoryWithFittness = null;
257
258 }
259 logger.info("Interrupted.");
260 }
261
262 @Override
263 public void interruptStrategy() {
264 isInterrupted = true;
265 }
266
267 Random random = new Random();
268 private TrajectoryWithFitness selectRandomState() {
269 int randomNumber = random.nextInt(100);
270 if(randomNumber < 5) {
271 int elements = trajectoiresToExplore.size();
272 int randomElementIndex = random.nextInt(elements);
273 logger.debug("Randomly backtract to the " + randomElementIndex + " best solution...");
274 Iterator<TrajectoryWithFitness> iterator = trajectoiresToExplore.iterator();
275 while(randomElementIndex!=0) {
276 iterator.next();
277 randomElementIndex--;
278 }
279 TrajectoryWithFitness res = iterator.next();
280 if(res == null) {
281 return trajectoiresToExplore.element();
282 } else {
283 return res;
284 }
285 } else {
286 return trajectoiresToExplore.element();
287 }
288 }
289
290 private PartialInterpretation2Logic partialInterpretation2Logic = new PartialInterpretation2Logic();
291 private LogicReasoner reasoner;
292 private PartialInterpretation2Gml partialInterpretation2Gml = new PartialInterpretation2Gml();
293 private ReasonerWorkspace workspace;
294 private LogicSolverConfiguration configuration;
295 int numberOfPrintedModel = 0;
296 public ModelResult modelResultByTheSolver = null;
297 public void writeCurrentState() {
298 PartialInterpretation p = (PartialInterpretation)(context.getModel());
299 int id= ++numberOfPrintedModel;
300 if(id%100 == 1) {
301 String text = this.partialInterpretation2Gml.transform(p);
302 this.workspace.writeText(id+".gml", text);
303 this.workspace.writeModel(p, id+".partialinterpretation");
304 logger.debug("State "+id+" is saved.");
305 }
306 }
307
308// int numberOfSolverCalls = 0;
309//
310// protected boolean checkConsistency(TrajectoryWithFitness t) {
311// if (reasoner != null) {
312// int id = ++numberOfSolverCalls;
313// if (id % 100 == 1) {
314// try {
315// PartialInterpretation interpretation = (PartialInterpretation) (context.getModel());
316// PartialInterpretation copied = EcoreUtil.copy(interpretation);
317// this.partialInterpretation2Logic.transformPartialIntepretation2Logic(copied.getProblem(), copied);
318// LogicProblem newProblem = copied.getProblem();
319//
320// this.configuration.typeScopes.maxNewElements = interpretation.getMaxNewElements();
321// this.configuration.typeScopes.minNewElements = interpretation.getMinNewElements();
322// LogicResult result = reasoner.solve(newProblem, configuration, workspace);
323// if (result instanceof InconsistencyResult) {
324// logger.debug("Solver found an Inconsistency!");
325// removeSubtreeFromQueue(t);
326// return true;
327// } else if (result instanceof ModelResult) {
328// logger.debug("Solver found a model!");
329// solutionStore.newSolution(context);
330
331// modelResultByTheSolver = (ModelResult) result;
332// return true;
333// } else {
334// logger.debug("Failed consistency check.");
335// return false;
336// }
337// } catch (Exception e) {
338// // TODO Auto-generated catch block
339// e.printStackTrace();
340// return false;
341// }
342// }
343//
344// }
345// return false;
346// }
347//
348// protected void removeSubtreeFromQueue(TrajectoryWithFitness t) {
349// PriorityQueue<TrajectoryWithFitness> previous = this.trajectoiresToExplore;
350// this.trajectoiresToExplore = new PriorityQueue<>(this.comparator);
351// for (TrajectoryWithFitness trajectoryWithFitness : previous) {
352// if(! containsAsSubstring(trajectoryWithFitness.trajectory,t.trajectory)) {
353// this.trajectoiresToExplore.add(trajectoryWithFitness);
354// } else {
355// logger.debug("State has been excluded due to inherent inconsistency");
356// }
357// }
358// }
359//
360// private boolean containsAsSubstring(Object[] full, Object[] substring) {
361// if(substring.length > full.length) {
362// return false;
363// } else if(substring.length == full.length) {
364// return Arrays.equals(full, substring);
365// } else {
366// Object[] part = Arrays.copyOfRange(full, 0, substring.length);
367// return Arrays.equals(part, substring);
368// }
369// }
370//
371
372}
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ModelGenerationCompositeObjective.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ModelGenerationCompositeObjective.xtend
new file mode 100644
index 00000000..1ca2343f
--- /dev/null
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ModelGenerationCompositeObjective.xtend
@@ -0,0 +1,85 @@
1package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse
2
3import java.util.Comparator
4import java.util.List
5import org.eclipse.viatra.dse.base.ThreadContext
6import org.eclipse.viatra.dse.objectives.Comparators
7import org.eclipse.viatra.dse.objectives.IObjective
8import org.eclipse.viatra.dse.objectives.impl.BaseObjective
9
10//class ViatraReasonerNumbers {
11// public static val scopePriority = 2
12// public static val unfinishedMultiplicityPriority = 2
13// public static val unifinshedWFPriority = 2
14// //public static val complexityPriority = 4
15//
16// public static val scopeWeigth = 1.0
17// public static val unfinishedMultiplicityWeigth = 1.5
18// public static val unfinishedWFWeigth = 1.5
19// //public static val complexityWeigth = 0.1
20//
21// public static val useCompositeObjective = true
22// public static val compositePriority = 2
23//}
24
25class ModelGenerationCompositeObjective implements IObjective{
26 val ScopeObjective scopeObjective
27 val List<UnfinishedMultiplicityObjective> unfinishedMultiplicityObjectives
28 val UnfinishedWFObjective unfinishedWFObjective
29
30 public new(
31 ScopeObjective scopeObjective,
32 List<UnfinishedMultiplicityObjective> unfinishedMultiplicityObjectives,
33 UnfinishedWFObjective unfinishedWFObjective)
34 {
35 this.scopeObjective = scopeObjective
36 this.unfinishedMultiplicityObjectives = unfinishedMultiplicityObjectives
37 this.unfinishedWFObjective = unfinishedWFObjective
38 }
39
40 override init(ThreadContext context) {
41 this.scopeObjective.init(context)
42 this.unfinishedMultiplicityObjectives.forEach[it.init(context)]
43 this.unfinishedWFObjective.init(context)
44 }
45
46 override createNew() {
47 return new ModelGenerationCompositeObjective(
48 this.scopeObjective, this.unfinishedMultiplicityObjectives, this.unfinishedWFObjective)
49 }
50
51 override getComparator() { Comparators.LOWER_IS_BETTER }
52 override getFitness(ThreadContext context) {
53 var sum = 0.0
54 val scopeFitnes = scopeObjective.getFitness(context)
55 //val unfinishedMultiplicitiesFitneses = unfinishedMultiplicityObjectives.map[x|x.getFitness(context)]
56 val unfinishedWFsFitness = unfinishedWFObjective.getFitness(context)
57
58 sum+=scopeFitnes
59 var multiplicity = 0.0
60 for(multiplicityObjective : unfinishedMultiplicityObjectives) {
61 multiplicity+=multiplicityObjective.getFitness(context)//*0.5
62 }
63 sum+=multiplicity
64 sum += unfinishedWFsFitness//*0.5
65
66// println('''Sum=«sum»|Scope=«scopeFitnes»|Multiplicity=«multiplicity»|WFs=«unfinishedWFsFitness»''')
67
68 return sum
69 }
70
71 override getLevel() { 2 }
72 override getName() { "CompositeUnfinishednessObjective"}
73
74 override isHardObjective() { true }
75 override satisifiesHardObjective(Double fitness) { fitness <= 0.001 }
76
77
78 override setComparator(Comparator<Double> comparator) {
79 throw new UnsupportedOperationException("TODO: auto-generated method stub")
80 }
81 override setLevel(int level) {
82 throw new UnsupportedOperationException("TODO: auto-generated method stub")
83 }
84
85} \ No newline at end of file
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/PartialModelAsLogicInterpretation.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/PartialModelAsLogicInterpretation.xtend
new file mode 100644
index 00000000..b2a7e3f5
--- /dev/null
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/PartialModelAsLogicInterpretation.xtend
@@ -0,0 +1,30 @@
1package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse
2
3import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicModelInterpretation
4import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type
5import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.FunctionDeclaration
6import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration
7import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDeclaration
8
9class PartialModelAsLogicInterpretation implements LogicModelInterpretation{
10
11
12 override getElements(Type type) {
13 throw new UnsupportedOperationException("TODO: auto-generated method stub")
14 }
15
16 override getInterpretation(FunctionDeclaration function, Object[] parameterSubstitution) {
17 throw new UnsupportedOperationException("TODO: auto-generated method stub")
18 }
19
20 override getInterpretation(RelationDeclaration relation, Object[] parameterSubstitution) {
21 throw new UnsupportedOperationException("TODO: auto-generated method stub")
22 }
23
24 override getInterpretation(ConstantDeclaration constant) {
25 throw new UnsupportedOperationException("TODO: auto-generated method stub")
26 }
27
28 override getMinimalInteger() { 0 }
29 override getMaximalInteger() {0 }
30} \ No newline at end of file
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ScopeObjective.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ScopeObjective.xtend
new file mode 100644
index 00000000..d3497ef2
--- /dev/null
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ScopeObjective.xtend
@@ -0,0 +1,41 @@
1package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse
2
3import org.eclipse.viatra.dse.objectives.IObjective
4import org.eclipse.viatra.dse.base.ThreadContext
5import java.util.Comparator
6import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation
7
8class ScopeObjective implements IObjective{
9 static val comparator = new Comparator<Double>() {
10 override compare(Double o1, Double o2) {
11
12 return o2.compareTo(o1)
13 }
14 }
15
16 //val static scopeLevel = 3
17
18 override createNew() { return new ScopeObjective }
19 override getName() { '''ScopeConstraint''' }
20 override init(ThreadContext context) { }
21
22 override getComparator() { comparator }
23
24 override getFitness(ThreadContext context) {
25 val interpretation = context.model as PartialInterpretation
26 val res = interpretation.minNewElements
27 return res.doubleValue
28 }
29
30 override isHardObjective() { true }
31 override satisifiesHardObjective(Double fitness) { return fitness <=0.01 }
32
33 override setComparator(Comparator<Double> comparator) {
34 throw new UnsupportedOperationException("TODO: auto-generated method stub")
35 }
36
37 override setLevel(int level) {
38 throw new UnsupportedOperationException("TODO: auto-generated method stub")
39 }
40 override getLevel() { 2 }
41} \ No newline at end of file
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/SolutionStoreWithCopy.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/SolutionStoreWithCopy.xtend
new file mode 100644
index 00000000..2892723b
--- /dev/null
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/SolutionStoreWithCopy.xtend
@@ -0,0 +1,35 @@
1package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse
2
3import java.util.List
4import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation
5import java.util.LinkedList
6import org.eclipse.emf.ecore.EObject
7import java.util.Map
8import org.eclipse.emf.ecore.util.EcoreUtil
9import org.eclipse.viatra.dse.base.ThreadContext
10
11class SolutionStoreWithCopy {
12 long runtime = 0
13 List<PartialInterpretation> solutions = new LinkedList
14 List<Map<EObject,EObject>> copyTraces = new LinkedList
15
16 long initTime = System.nanoTime
17
18 def newSolution(ThreadContext context) {
19 //print(System.nanoTime-initTime + ";")
20 val copyStart = System.nanoTime
21 val solution = context.model as PartialInterpretation
22 val copier = new EcoreUtil.Copier
23 val solutionCopy = copier.copy(solution) as PartialInterpretation
24 copier.copyReferences
25 solutions.add(solutionCopy)
26 copyTraces.add(copier)
27 runtime += System.nanoTime - copyStart
28 }
29 def getSumRuntime() {
30 return runtime
31 }
32 def getSolutions() {
33 solutions
34 }
35} \ No newline at end of file
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/SolutionStoreWithDiversityDescriptor.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/SolutionStoreWithDiversityDescriptor.xtend
new file mode 100644
index 00000000..ca39cada
--- /dev/null
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/SolutionStoreWithDiversityDescriptor.xtend
@@ -0,0 +1,77 @@
1package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse
2
3import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.neighbourhood.AbstractNodeDescriptor
4import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.neighbourhood.NeighbourhoodWithTraces
5import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.neighbourhood.PartialInterpretation2ImmutableTypeLattice
6import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation
7import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.DiversityDescriptor
8import java.util.LinkedList
9import java.util.List
10import java.util.Map
11import org.eclipse.viatra.dse.base.ThreadContext
12
13class SolutionStoreWithDiversityDescriptor {
14 val DiversityDescriptor descriptor
15 val PartialInterpretation2ImmutableTypeLattice solutionCoder = new PartialInterpretation2ImmutableTypeLattice
16 val List<NeighbourhoodWithTraces<Map<? extends AbstractNodeDescriptor, Integer>, AbstractNodeDescriptor>> solutionCodeList = new LinkedList
17
18 var long runtime
19 var int allCheck
20 var int successfulCheck
21
22 public new(DiversityDescriptor descriptor) {
23 this.descriptor = descriptor
24 }
25
26 def public isActive() {
27 descriptor!==null
28 }
29
30 def getSumRuntime() {
31 return runtime
32 }
33 def getSuccessRate() {
34 return successfulCheck as double / allCheck
35 }
36
37 def isDifferent(ThreadContext context) {
38 if(active) {
39 val start = System.nanoTime
40 val model = context.model as PartialInterpretation
41 val code = solutionCoder.createRepresentation(model,
42 descriptor.range,
43 descriptor.parallels,
44 descriptor.maxNumber,
45 descriptor.relevantTypes,
46 descriptor.relevantRelations)
47 val isDifferent = solutionCodeList.forall[previous | ! code.equals(previous)]
48 runtime += System.nanoTime - start
49 allCheck++
50 if(isDifferent) { successfulCheck++ }
51 return isDifferent
52 } else {
53 allCheck++
54 successfulCheck++
55 return true
56 }
57 }
58
59 def canBeDifferent(ThreadContext context) {
60 return true
61 }
62
63 def newSolution(ThreadContext context) {
64 if(active) {
65 val start = System.nanoTime
66 val model = context.model as PartialInterpretation
67 val code = solutionCoder.createRepresentation(model,
68 descriptor.range,
69 descriptor.parallels,
70 descriptor.maxNumber,
71 descriptor.relevantTypes,
72 descriptor.relevantRelations)
73 solutionCodeList += code
74 runtime += System.nanoTime - start
75 }
76 }
77} \ No newline at end of file
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/UnfinishedMultiplicityObjective.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/UnfinishedMultiplicityObjective.xtend
new file mode 100644
index 00000000..aad9a448
--- /dev/null
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/UnfinishedMultiplicityObjective.xtend
@@ -0,0 +1,37 @@
1package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse
2
3import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.MultiplicityGoalConstraintCalculator
4import java.util.Comparator
5import org.eclipse.viatra.dse.base.ThreadContext
6import org.eclipse.viatra.dse.objectives.IObjective
7import org.eclipse.viatra.dse.objectives.Comparators
8
9class UnfinishedMultiplicityObjective implements IObjective {
10 val MultiplicityGoalConstraintCalculator unfinishedMultiplicity;
11
12 public new(MultiplicityGoalConstraintCalculator unfinishedMultiplicity) {
13 this.unfinishedMultiplicity = unfinishedMultiplicity
14 }
15
16 override getName() '''unfinishedMultiplicity «unfinishedMultiplicity.name»'''
17 override createNew() {
18 return new UnfinishedMultiplicityObjective(new MultiplicityGoalConstraintCalculator(this.unfinishedMultiplicity))
19 }
20
21 override getComparator() { Comparators.LOWER_IS_BETTER }
22 override getFitness(ThreadContext context) {
23 val unfinishedMultiplicity = unfinishedMultiplicity.calculateValue
24 return unfinishedMultiplicity.doubleValue
25 }
26 override getLevel() { 2 }
27 override init(ThreadContext context) { unfinishedMultiplicity.init(context.model) }
28 override isHardObjective() { true }
29 override satisifiesHardObjective(Double fitness) { return fitness <=0.01 }
30
31 override setComparator(Comparator<Double> comparator) {
32 throw new UnsupportedOperationException("TODO: auto-generated method stub")
33 }
34 override setLevel(int level) {
35 throw new UnsupportedOperationException("TODO: auto-generated method stub")
36 }
37} \ No newline at end of file
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/UnfinishedWFObjective.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/UnfinishedWFObjective.xtend
new file mode 100644
index 00000000..0fd20fa3
--- /dev/null
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/UnfinishedWFObjective.xtend
@@ -0,0 +1,56 @@
1package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse
2
3import org.eclipse.viatra.dse.objectives.IObjective
4import org.eclipse.viatra.query.runtime.api.IPatternMatch
5import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher
6import org.eclipse.viatra.query.runtime.api.IQuerySpecification
7import java.util.Collection
8import org.eclipse.viatra.query.runtime.api.ViatraQueryEngine
9import org.eclipse.viatra.query.runtime.emf.EMFScope
10import org.eclipse.viatra.dse.base.ThreadContext
11import java.util.List
12import org.eclipse.viatra.dse.objectives.Comparators
13import java.util.ArrayList
14import java.util.Comparator
15
16class UnfinishedWFObjective implements IObjective {
17 Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> unfinishedWFs
18 val List<ViatraQueryMatcher<?>> matchers
19
20 public new(Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> unfinishedWFs) {
21 this.unfinishedWFs = unfinishedWFs
22 matchers = new ArrayList(unfinishedWFs.size)
23 }
24 override getName() '''unfinishedWFs'''
25 override createNew() {
26 return new UnfinishedWFObjective(unfinishedWFs)
27 }
28 override init(ThreadContext context) {
29 val engine = context.queryEngine//ViatraQueryEngine.on(new EMFScope(context.model))
30 for(unfinishedWF : unfinishedWFs) {
31 matchers += unfinishedWF.getMatcher(engine)
32 }
33 }
34
35 override getComparator() { Comparators.LOWER_IS_BETTER }
36 override getFitness(ThreadContext context) {
37 var sumOfMatches = 0
38 for(matcher : matchers) {
39 val number = matcher.countMatches
40// println('''«matcher.patternName» = «number»''')
41 sumOfMatches+=number
42 }
43 return sumOfMatches.doubleValue
44 }
45
46 override getLevel() { 2 }
47 override isHardObjective() { true }
48 override satisifiesHardObjective(Double fitness) { return fitness <=0.01 }
49
50 override setComparator(Comparator<Double> comparator) {
51 throw new UnsupportedOperationException("TODO: auto-generated method stub")
52 }
53 override setLevel(int level) {
54 throw new UnsupportedOperationException("TODO: auto-generated method stub")
55 }
56} \ No newline at end of file
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/WF2ObjectiveConverter.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/WF2ObjectiveConverter.xtend
new file mode 100644
index 00000000..4fd297ca
--- /dev/null
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/WF2ObjectiveConverter.xtend
@@ -0,0 +1,36 @@
1package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse
2
3import java.util.ArrayList
4import java.util.Collection
5import org.eclipse.viatra.dse.objectives.Comparators
6import org.eclipse.viatra.dse.objectives.IGlobalConstraint
7import org.eclipse.viatra.dse.objectives.impl.ConstraintsObjective
8import org.eclipse.viatra.dse.objectives.impl.ConstraintsObjective.QueryConstraint
9import org.eclipse.viatra.dse.objectives.impl.ModelQueriesGlobalConstraint
10import org.eclipse.viatra.query.runtime.api.IPatternMatch
11import org.eclipse.viatra.query.runtime.api.IQuerySpecification
12import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher
13
14class WF2ObjectiveConverter {
15
16 def createCompletenessObjective(
17 Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> unfinishedWF)
18 {
19 val res = new ConstraintsObjective('''unfinishedWFs''',
20 unfinishedWF.map[
21 new QueryConstraint(it.fullyQualifiedName,it,1.0)
22 ].toList
23 )
24 res.withComparator(Comparators.LOWER_IS_BETTER)
25 res.level = 2
26 return res
27 }
28
29 def IGlobalConstraint createInvalidationObjective(
30 Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> invalidatedByWF)
31 {
32 return new ModelQueriesGlobalConstraint('''invalidatedWFs''',
33 new ArrayList(invalidatedByWF)
34 )
35 }
36} \ No newline at end of file
generated by cgit v1.2.3-54-g00ecf (git 2.45.2) at 2024-06-29 08:54:23 +0000