diff options
Diffstat (limited to 'Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf')
13 files changed, 1035 insertions, 0 deletions
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 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner | ||
2 | |||
3 | import org.eclipse.viatra.dse.objectives.IGlobalConstraint | ||
4 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationMethod | ||
5 | |||
6 | abstract 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 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner | ||
2 | |||
3 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner | ||
4 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasonerException | ||
5 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration | ||
6 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LogiclanguagePackage | ||
7 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem | ||
8 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicproblemPackage | ||
9 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicresultFactory | ||
10 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult | ||
11 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationMethodProvider | ||
12 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.PartialInterpretationInitialiser | ||
13 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialinterpretationPackage | ||
14 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.statecoder.IdentifierBasedStateCoderFactory | ||
15 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.statecoder.NeighbourhoodBasedStateCoderFactory | ||
16 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.BestFirstStrategyForModelGeneration | ||
17 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.ModelGenerationCompositeObjective | ||
18 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.PartialModelAsLogicInterpretation | ||
19 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.ScopeObjective | ||
20 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.UnfinishedMultiplicityObjective | ||
21 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.UnfinishedWFObjective | ||
22 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.WF2ObjectiveConverter | ||
23 | import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace | ||
24 | import org.eclipse.viatra.dse.api.DesignSpaceExplorer | ||
25 | import org.eclipse.viatra.dse.api.DesignSpaceExplorer.DseLoggingLevel | ||
26 | import org.eclipse.viatra.dse.solutionstore.SolutionStore | ||
27 | import org.eclipse.viatra.dse.statecode.IStateCoderFactory | ||
28 | |||
29 | class 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 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner | ||
2 | |||
3 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration | ||
4 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration | ||
5 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDeclaration | ||
6 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationMethod | ||
7 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.TypeInferenceMethod | ||
8 | import java.util.LinkedList | ||
9 | import java.util.List | ||
10 | import java.util.Set | ||
11 | import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery | ||
12 | import org.eclipse.xtext.xbase.lib.Functions.Function1 | ||
13 | |||
14 | public enum StateCoderStrategy { | ||
15 | Neighbourhood, NeighbourhoodWithEquivalence, IDBased, DefinedByDiversity | ||
16 | } | ||
17 | |||
18 | class 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 | |||
36 | public 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 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.diversity | ||
2 | |||
3 | abstract 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 | *******************************************************************************/ | ||
10 | package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse; | ||
11 | |||
12 | import java.util.ArrayList; | ||
13 | import java.util.Arrays; | ||
14 | import java.util.Collections; | ||
15 | import java.util.Comparator; | ||
16 | import java.util.Iterator; | ||
17 | import java.util.List; | ||
18 | import java.util.PriorityQueue; | ||
19 | import java.util.Random; | ||
20 | |||
21 | import org.apache.log4j.Logger; | ||
22 | import org.eclipse.viatra.dse.api.strategy.interfaces.IStrategy; | ||
23 | import org.eclipse.viatra.dse.base.ThreadContext; | ||
24 | import org.eclipse.viatra.dse.objectives.Fitness; | ||
25 | import org.eclipse.viatra.dse.objectives.ObjectiveComparatorHelper; | ||
26 | import org.eclipse.viatra.dse.solutionstore.SolutionStore; | ||
27 | |||
28 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner; | ||
29 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration; | ||
30 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult; | ||
31 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic.PartialInterpretation2Logic; | ||
32 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation; | ||
33 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.visualisation.PartialInterpretation2Gml; | ||
34 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.DiversityDescriptor; | ||
35 | import 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 | */ | ||
53 | public 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 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse | ||
2 | |||
3 | import java.util.Comparator | ||
4 | import java.util.List | ||
5 | import org.eclipse.viatra.dse.base.ThreadContext | ||
6 | import org.eclipse.viatra.dse.objectives.Comparators | ||
7 | import org.eclipse.viatra.dse.objectives.IObjective | ||
8 | import 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 | |||
25 | class 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 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse | ||
2 | |||
3 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicModelInterpretation | ||
4 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type | ||
5 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.FunctionDeclaration | ||
6 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration | ||
7 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDeclaration | ||
8 | |||
9 | class 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 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse | ||
2 | |||
3 | import org.eclipse.viatra.dse.objectives.IObjective | ||
4 | import org.eclipse.viatra.dse.base.ThreadContext | ||
5 | import java.util.Comparator | ||
6 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation | ||
7 | |||
8 | class 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 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse | ||
2 | |||
3 | import java.util.List | ||
4 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation | ||
5 | import java.util.LinkedList | ||
6 | import org.eclipse.emf.ecore.EObject | ||
7 | import java.util.Map | ||
8 | import org.eclipse.emf.ecore.util.EcoreUtil | ||
9 | import org.eclipse.viatra.dse.base.ThreadContext | ||
10 | |||
11 | class 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 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse | ||
2 | |||
3 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.neighbourhood.AbstractNodeDescriptor | ||
4 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.neighbourhood.NeighbourhoodWithTraces | ||
5 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.neighbourhood.PartialInterpretation2ImmutableTypeLattice | ||
6 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation | ||
7 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.DiversityDescriptor | ||
8 | import java.util.LinkedList | ||
9 | import java.util.List | ||
10 | import java.util.Map | ||
11 | import org.eclipse.viatra.dse.base.ThreadContext | ||
12 | |||
13 | class 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 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse | ||
2 | |||
3 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.MultiplicityGoalConstraintCalculator | ||
4 | import java.util.Comparator | ||
5 | import org.eclipse.viatra.dse.base.ThreadContext | ||
6 | import org.eclipse.viatra.dse.objectives.IObjective | ||
7 | import org.eclipse.viatra.dse.objectives.Comparators | ||
8 | |||
9 | class 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 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse | ||
2 | |||
3 | import org.eclipse.viatra.dse.objectives.IObjective | ||
4 | import org.eclipse.viatra.query.runtime.api.IPatternMatch | ||
5 | import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher | ||
6 | import org.eclipse.viatra.query.runtime.api.IQuerySpecification | ||
7 | import java.util.Collection | ||
8 | import org.eclipse.viatra.query.runtime.api.ViatraQueryEngine | ||
9 | import org.eclipse.viatra.query.runtime.emf.EMFScope | ||
10 | import org.eclipse.viatra.dse.base.ThreadContext | ||
11 | import java.util.List | ||
12 | import org.eclipse.viatra.dse.objectives.Comparators | ||
13 | import java.util.ArrayList | ||
14 | import java.util.Comparator | ||
15 | |||
16 | class 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 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse | ||
2 | |||
3 | import java.util.ArrayList | ||
4 | import java.util.Collection | ||
5 | import org.eclipse.viatra.dse.objectives.Comparators | ||
6 | import org.eclipse.viatra.dse.objectives.IGlobalConstraint | ||
7 | import org.eclipse.viatra.dse.objectives.impl.ConstraintsObjective | ||
8 | import org.eclipse.viatra.dse.objectives.impl.ConstraintsObjective.QueryConstraint | ||
9 | import org.eclipse.viatra.dse.objectives.impl.ModelQueriesGlobalConstraint | ||
10 | import org.eclipse.viatra.query.runtime.api.IPatternMatch | ||
11 | import org.eclipse.viatra.query.runtime.api.IQuerySpecification | ||
12 | import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher | ||
13 | |||
14 | class 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 | ||