From e11bce7ad3e803e80883499fec0ad6e4540ffe43 Mon Sep 17 00:00:00 2001 From: Kristóf Marussy Date: Tue, 30 Jun 2020 18:03:48 +0200 Subject: Add modified VIATRA-DSE version --- .../viatra/dse/base/DesignSpaceManager.java | 563 +++++++++++++++++++++ 1 file changed, 563 insertions(+) create mode 100644 Solvers/VIATRA-Solver/org.eclipse.viatra.dse/src/org/eclipse/viatra/dse/base/DesignSpaceManager.java (limited to 'Solvers/VIATRA-Solver/org.eclipse.viatra.dse/src/org/eclipse/viatra/dse/base/DesignSpaceManager.java') diff --git a/Solvers/VIATRA-Solver/org.eclipse.viatra.dse/src/org/eclipse/viatra/dse/base/DesignSpaceManager.java b/Solvers/VIATRA-Solver/org.eclipse.viatra.dse/src/org/eclipse/viatra/dse/base/DesignSpaceManager.java new file mode 100644 index 00000000..4c6b4097 --- /dev/null +++ b/Solvers/VIATRA-Solver/org.eclipse.viatra.dse/src/org/eclipse/viatra/dse/base/DesignSpaceManager.java @@ -0,0 +1,563 @@ +/******************************************************************************* + * Copyright (c) 2010-2014, Miklos Foldenyi, Andras Szabolcs Nagy, Abel Hegedus, Akos Horvath, Zoltan Ujhelyi and Daniel Varro + * This program and the accompanying materials are made available under the + * terms of the Eclipse Public License v. 2.0 which is available at + * http://www.eclipse.org/legal/epl-v20.html. + * + * SPDX-License-Identifier: EPL-2.0 + *******************************************************************************/ +package org.eclipse.viatra.dse.base; + +import java.lang.reflect.InvocationTargetException; +import java.util.ArrayList; +import java.util.Collection; +import java.util.HashMap; +import java.util.Iterator; +import java.util.List; +import java.util.Map; +import java.util.Random; + +import org.apache.log4j.Logger; +import org.eclipse.emf.common.notify.Notifier; +import org.eclipse.emf.edit.command.ChangeCommand; +import org.eclipse.emf.edit.domain.EditingDomain; +import org.eclipse.viatra.dse.api.DSEException; +import org.eclipse.viatra.dse.api.SolutionTrajectory; +import org.eclipse.viatra.dse.designspace.api.IBacktrackListener; +import org.eclipse.viatra.dse.designspace.api.IDesignSpace; +import org.eclipse.viatra.dse.designspace.api.TrajectoryInfo; +import org.eclipse.viatra.dse.objectives.ActivationFitnessProcessor; +import org.eclipse.viatra.dse.statecode.IStateCoder; +import org.eclipse.viatra.dse.visualizer.IExploreEventHandler; +import org.eclipse.viatra.query.runtime.api.AdvancedViatraQueryEngine; +import org.eclipse.viatra.query.runtime.api.IPatternMatch; +import org.eclipse.viatra.transformation.evm.api.Activation; +import org.eclipse.viatra.transformation.evm.api.Context; +import org.eclipse.viatra.transformation.evm.api.resolver.ChangeableConflictSet; +import org.eclipse.viatra.transformation.runtime.emf.rules.batch.BatchTransformationRule; + +public class DesignSpaceManager implements IBacktrackListener { + + private final IStateCoder stateCoder; + private final EditingDomain domain; + private Notifier model; + + private IDesignSpace designSpace; + + private final TrajectoryInfo trajectory; + + // the occurence vector callback + private List handlers; + + // Dummy context for evm + private final Context evmContext = Context.create(); + + private Logger logger = Logger.getLogger(this.getClass()); + + private boolean isNewState = false; + private Map, ActivationFitnessProcessor> activationFitnessProcessors; + private Map, String> activationFitnessProcessorNames; + private ThreadContext context; + + private ActivationCodesConflictSet activationCodes; + private ChangeableConflictSet conflictSet; + + private AdvancedViatraQueryEngine engine; + + private Random random = new Random(); + + private long forwardTime = 0; + private long backtrackingTime = 0; + + public DesignSpaceManager(ThreadContext context) { + + this.context = context; + model = context.getModel(); + designSpace = context.getGlobalContext().getDesignSpace(); + domain = context.getEditingDomain(); + + conflictSet = context.getConflictResolver().getLastCreatedConflictSet(); + + stateCoder = context.getStateCoder(); + Object initialStateId = stateCoder.createStateCode(); + designSpace.addState(null, null, initialStateId); + + activationCodes = context.getActivationCodesConflictSet(); + + engine = (AdvancedViatraQueryEngine) context.getQueryEngine(); + + this.trajectory = new TrajectoryInfo(initialStateId); + + logger.debug("DesignSpaceManager initialized with initial model: " + initialStateId); + } + + public void fireActivation(final Object transition) { + if (fireActivationSilent(transition)) { + return; + } + + StringBuilder sb = new StringBuilder(); + sb.append( + "A retrieved Transition SHOULD have a matching Activation. Possible causes: the state serializer is faulty; the algorithm choosed a wrong Transition."); + sb.append("\nSought transition: "); + sb.append(transition); + Object currentStateId = getCurrentState(); + sb.append("\nCurrent known state: "); + sb.append(currentStateId); + Object actualStateId = stateCoder.createStateCode(); + sb.append("\nActual state: "); + sb.append((actualStateId.equals(currentStateId) ? "same as current" : actualStateId)); + sb.append("\n"); + sb.append(trajectory); + sb.append("\nAvailable transitions:"); + for (Activation act : conflictSet.getNextActivations()) { + IPatternMatch match = (IPatternMatch) act.getAtom(); + Object code = generateMatchCode(match); + sb.append("\n\t"); + sb.append(code); + } + + throw new DSEException(sb.toString()); + } + + public boolean tryFireActivation(final Object transition) { + return fireActivationSilent(transition); + } + + private boolean fireActivationSilent(final Object transition) { + final Activation activation = getActivationById(transition); + + if (activation == null) { + return false; + } + + BatchTransformationRule rule = getRuleByActivation(activation); + + Map measureCosts = new HashMap(); + if (activationFitnessProcessors != null && activationFitnessProcessors.containsKey(rule)) { + IPatternMatch match = (IPatternMatch) activation.getAtom(); + ActivationFitnessProcessor processor = activationFitnessProcessors.get(rule); + double fitness = processor.process(match); + measureCosts.put(activationFitnessProcessorNames.get(rule), fitness); + } + + ChangeCommand rc = new ChangeCommand(model) { + @Override + protected void doExecute() { + activation.fire(evmContext); + } + }; + + Object previousState = trajectory.getCurrentStateId(); + + long start = System.nanoTime(); + domain.getCommandStack().execute(rc); + forwardTime += System.nanoTime() - start; + + Object newStateId = stateCoder.createStateCode(); + updateActivationCodes(); + + if (designSpace != null) { + isNewState = !designSpace.isTraversed(newStateId); + designSpace.addState(previousState, transition, newStateId); + } + + trajectory.addStep(transition, rule, newStateId, measureCosts); + + if (handlers != null) { + for (IExploreEventHandler iExploreEventHandler : handlers) { + iExploreEventHandler.transitionFired(transition); + } + } + + logger.debug("Executed activation: " + transition);/* + * + " from state: " + previousState + " to " + newStateId); + */ + + return true; + } + + public boolean executeRandomActivationId() { + Collection transitions = getTransitionsFromCurrentState(); + int size = transitions.size(); + if (size == 0) { + return false; + } + + int index = random.nextInt(size); + Iterator iterator = transitions.iterator(); + for (int i = 0; i < index; ++i) { + iterator.next(); + } + Object transition = iterator.next(); + + fireActivation(transition); + return true; + } + + public int executeTrajectory(Object[] trajectoryToExecute) { + return executeTrajectory(trajectoryToExecute, 0, trajectoryToExecute.length, false, true); + } + + public int executeTrajectory(Object[] trajectoryToExecute, int fromIncludedIndex, int toExcludedIndex) { + return executeTrajectory(trajectoryToExecute, fromIncludedIndex, toExcludedIndex, false, true); + } + + public int executeTrajectoryByTrying(Object[] trajectoryToExecute) { + return executeTrajectory(trajectoryToExecute, 0, trajectoryToExecute.length, true, true); + } + + public int executeTrajectoryByTrying(Object[] trajectoryToExecute, int fromIncludedIndex, int toExcludedIndex) { + return executeTrajectory(trajectoryToExecute, fromIncludedIndex, toExcludedIndex, true, true); + } + + public int executeTrajectoryWithoutStateCoding(Object[] trajectoryToExecute) { + return executeTrajectory(trajectoryToExecute, 0, trajectoryToExecute.length, false, false); + } + + public int executeTrajectoryWithoutStateCoding(Object[] trajectoryToExecute, int fromIncludedIndex, + int toExcludedIndex) { + return executeTrajectory(trajectoryToExecute, fromIncludedIndex, toExcludedIndex, false, false); + } + + public int executeTrajectoryByTryingWithoutStateCoding(Object[] trajectoryToExecute) { + return executeTrajectory(trajectoryToExecute, 0, trajectoryToExecute.length, true, false); + } + + public int executeTrajectoryByTryingWithoutStateCoding(Object[] trajectoryToExecute, int fromIncludedIndex, + int toExcludedIndex) { + return executeTrajectory(trajectoryToExecute, fromIncludedIndex, toExcludedIndex, true, false); + } + + private int executeTrajectory(Object[] trajectoryToExecute, int fromIncludedIndex, int toExcludedIndex, + boolean tryAllActivations, boolean createStateCode) { + logger.debug("Executing trajectory."); + int unsuccesfulIndex = -1; + if (tryAllActivations) { + unsuccesfulIndex = 0; + } + for (int i = fromIncludedIndex; i < toExcludedIndex; i++) { + Object activationId = trajectoryToExecute[i]; + final Activation activation = getActivationById(activationId); + + if (activation == null) { + logger.debug("Couldn't execute activation: " + activationId); + if (tryAllActivations) { + unsuccesfulIndex++; + continue; + } else { + unsuccesfulIndex = i; + logger.debug("Trajectory execution stopped at index " + i + "/" + trajectoryToExecute.length); + break; + } + } + + BatchTransformationRule rule = getRuleByActivation(activation); + + Map measureCosts = new HashMap(); + if (activationFitnessProcessors != null && activationFitnessProcessors.containsKey(rule)) { + IPatternMatch match = (IPatternMatch) activation.getAtom(); + ActivationFitnessProcessor processor = activationFitnessProcessors.get(rule); + double fitness = processor.process(match); + measureCosts.put(activationFitnessProcessorNames.get(rule), fitness); + } + + ChangeCommand rc = new ChangeCommand(model) { + @Override + protected void doExecute() { + activation.fire(evmContext); + } + }; + + long start = System.nanoTime(); + domain.getCommandStack().execute(rc); + forwardTime += System.nanoTime() - start; + + Object newStateId = null; + if (createStateCode) { + newStateId = stateCoder.createStateCode(); + } + updateActivationCodes(); + + trajectory.addStep(activationId, rule, newStateId, measureCosts); + + logger.debug("Activation executed: " + activationId); + } + if (!createStateCode) { + trajectory.modifyLastStateCode(stateCoder.createStateCode()); + } + logger.debug("Trajectory execution finished."); + return unsuccesfulIndex; + + } + + public Object getTransitionByActivation(Activation activation) { + return activationCodes.getActivationId(activation); + } + + public Activation getActivationById(Object activationId) { + return activationCodes.getActivation(activationId); + } + + public BatchTransformationRule getRuleByActivation(Activation activation) { + return context.getGlobalContext().getSpecificationRuleMap().get(activation.getInstance().getSpecification()); + } + + public BatchTransformationRule getRuleByActivationId(Object activationId) { + return getRuleByActivation(getActivationById(activationId)); + } + + /** + * Returns true if the given state is not owned by this crawler. + * + **/ + public boolean isNewModelStateAlreadyTraversed() { + return !isNewState; + } + + public List getTrajectoryFromRoot() { + return trajectory.getTrajectory(); + } + + public Collection getTransitionsFromCurrentState() { + return activationCodes.getCurrentActivationCodes(); + } + + public Collection getUntraversedTransitionsFromCurrentState() { + if (designSpace == null) { + throw new DSEException("Unsupported without a design space"); + } + Object currentState = trajectory.getCurrentStateId(); + Collection traversedIds = designSpace.getActivationIds(currentState); + + List untraversedTransitions = new ArrayList<>(); + for (Object activationId : activationCodes.getCurrentActivationCodes()) { + if (!traversedIds.contains(activationId)) { + untraversedTransitions.add(activationId); + } + } + + return untraversedTransitions; + } + + public boolean undoLastTransformation() { + + if (!trajectory.canStepBack()) { + return false; + } + + long start = System.nanoTime(); + try { + engine.delayUpdatePropagation(() -> { + domain.getCommandStack().undo(); + return null; + }); + } catch (InvocationTargetException e) { + throw new RuntimeException(e); + } + updateActivationCodes(); + + Object lastActivationId = trajectory.getLastActivationId(); + + trajectory.backtrack(); + + if (handlers != null) { + for (IExploreEventHandler iExploreEventHandler : handlers) { + iExploreEventHandler.undo(lastActivationId); + } + } + + logger.debug("Backtrack."); + backtrackingTime += System.nanoTime() - start; + + return true; + } + + public void backtrackXTimes(int steps) { + long start = System.nanoTime(); + try { + engine.delayUpdatePropagation(() -> { + for (int i = steps; i > 0; i--) { + domain.getCommandStack().undo(); + trajectory.backtrack(); + } + return null; + }); + } catch (InvocationTargetException e) { + throw new RuntimeException(e); + } + backtrackingTime += System.nanoTime() - start; + updateActivationCodes(); + logger.debug("Backtracked " + steps + " times."); + } + + public int backtrackUntilLastCommonActivation(Object[] newTrajectory) { + long start = System.nanoTime(); + Iterator currentTrajectoryIterator = trajectory.getTrajectory().iterator(); + if (!currentTrajectoryIterator.hasNext()) { + return 0; + } + int indexOfLastCommonActivation = 0; + for (Object activationCode : newTrajectory) { + if (currentTrajectoryIterator.hasNext()) { + Object activationCodeFromCurrent = currentTrajectoryIterator.next(); + if (activationCodeFromCurrent.equals(activationCode)) { + indexOfLastCommonActivation++; + } else { + break; + } + } else { + // current trajectory is smaller + break; + } + } + int numberOfBacktracks = trajectory.getDepth() - indexOfLastCommonActivation; + if (numberOfBacktracks > 0) { + try { + engine.delayUpdatePropagation(() -> { + for (int i = numberOfBacktracks; i > 0; i--) { + domain.getCommandStack().undo(); + trajectory.backtrack(); + } + return null; + }); + } catch (InvocationTargetException e) { + throw new RuntimeException(e); + } + } + backtrackingTime += System.nanoTime() - start; + updateActivationCodes(); + logger.debug("Backtracked " + numberOfBacktracks + " times."); + return indexOfLastCommonActivation; + } + + public void executeTrajectoryWithMinimalBacktrack(Object[] trajectory) { + executeTrajectoryWithMinimalBacktrack(trajectory, trajectory.length); + } + + public void executeTrajectoryWithMinimalBacktrack(Object[] trajectory, int toExcludedIndex) { + int fromIndex = backtrackUntilLastCommonActivation(trajectory); + executeTrajectory(trajectory, fromIndex, toExcludedIndex, false, true); + } + + public void executeTrajectoryWithMinimalBacktrackWithoutStateCoding(Object[] trajectory) { + executeTrajectoryWithMinimalBacktrackWithoutStateCoding(trajectory, trajectory.length); + } + + public void executeTrajectoryWithMinimalBacktrackWithoutStateCoding(Object[] trajectory, int toExcludedIndex) { + int fromIndex = backtrackUntilLastCommonActivation(trajectory); + executeTrajectory(trajectory, fromIndex, toExcludedIndex, false, false); + Object stateCode = stateCoder.createStateCode(); + this.trajectory.modifyLastStateCode(stateCode); + } + + public void undoUntilRoot() { + long start = System.nanoTime(); + try { + engine.delayUpdatePropagation(() -> { + while (trajectory.canStepBack()) { + domain.getCommandStack().undo(); + trajectory.backtrack(); + } + return null; + }); + } catch (InvocationTargetException e) { + throw new RuntimeException(e); + } + backtrackingTime += System.nanoTime() - start; + updateActivationCodes(); + logger.debug("Backtracked to root."); + } + + private Object generateMatchCode(IPatternMatch match) { + return stateCoder.createActivationCode(match); + } + + public Object getCurrentState() { + return trajectory.getCurrentStateId(); + } + + public SolutionTrajectory createSolutionTrajectroy() { + return trajectory.createSolutionTrajectory(context.getGlobalContext().getStateCoderFactory(), this); + } + + public TrajectoryInfo getTrajectoryInfo() { + return trajectory; + } + + public void setDesignSpace(IDesignSpace designSpace) { + this.designSpace = designSpace; + } + + public IDesignSpace getDesignSpace() { + return designSpace; + } + + public void registerExploreEventHandler(IExploreEventHandler handler) { + if (handler == null) { + return; + } + if (handlers == null) { + handlers = new ArrayList(); + } + handlers.add(handler); + } + + public void deregisterExploreEventHandler(IExploreEventHandler handler) { + if (handler == null) { + return; + } + if (handlers != null) { + handlers.remove(handler); + } + } + + public void registerActivationCostProcessor(String name, BatchTransformationRule rule, + ActivationFitnessProcessor activationFitnessProcessor) { + if (activationFitnessProcessors == null || activationFitnessProcessorNames == null) { + activationFitnessProcessors = new HashMap, ActivationFitnessProcessor>(); + activationFitnessProcessorNames = new HashMap, String>(); + } + activationFitnessProcessors.put(rule, activationFitnessProcessor); + activationFitnessProcessorNames.put(rule, name); + } + + public boolean isCurentStateInTrajectory() { + Object currentStateId = trajectory.getCurrentStateId(); + List stateTrajectory = trajectory.getStateTrajectory(); + int size = stateTrajectory.size(); + for (int i = 0; i < size - 1; i++) { + Object stateId = stateTrajectory.get(i); + if (currentStateId.equals(stateId)) { + return true; + } + } + return false; + } + + public IStateCoder getStateCoder() { + return stateCoder; + } + + private void updateActivationCodes() { + activationCodes.updateActivationCodes(); + } + + public long getForwardTime() { + return forwardTime; + } + + public long getBacktrackingTime() { + return backtrackingTime; + } + + @Override + public void forwardWorked(long nanos) { + forwardTime += nanos; + } + + @Override + public void backtrackWorked(long nanos) { + backtrackingTime += nanos; + } +} -- cgit v1.2.3-70-g09d2 From b0e3359574eb00e1eaab5a7286a6f8e163b7b87f Mon Sep 17 00:00:00 2001 From: Kristóf Marussy Date: Wed, 8 Jul 2020 02:33:06 +0200 Subject: Fix event storm on EMF transaction finish --- .../.ApplicationConfigurationIdeModule.xtendbin | Bin 1701 -> 1701 bytes .../ide/.ApplicationConfigurationIdeSetup.xtendbin | Bin 2526 -> 2526 bytes .../.SolverSemanticHighlightCalculator.xtendbin | Bin 5334 -> 5334 bytes .../.SolverSemanticTextAttributeProvider.xtendbin | Bin 4902 -> 4902 bytes .../validation/.SolverLanguageValidator.xtendbin | Bin 1717 -> 1717 bytes ....SolverLanguageTokenDefInjectingParser.xtendbin | Bin 2742 -> 2742 bytes ...nguageSyntheticTokenSyntacticSequencer.xtendbin | Bin 2758 -> 2758 bytes .../META-INF/MANIFEST.MF | 11 +- .../rules/RefinementRuleProvider.xtend | 516 +++++++++++---------- .../eclipse/viatra/dse/api/SolutionTrajectory.java | 9 +- .../viatra/dse/base/DesignSpaceManager.java | 18 +- 11 files changed, 293 insertions(+), 261 deletions(-) (limited to 'Solvers/VIATRA-Solver/org.eclipse.viatra.dse/src/org/eclipse/viatra/dse/base/DesignSpaceManager.java') diff --git a/Application/hu.bme.mit.inf.dslreasoner.application.ide/xtend-gen/hu/bme/mit/inf/dslreasoner/application/ide/.ApplicationConfigurationIdeModule.xtendbin b/Application/hu.bme.mit.inf.dslreasoner.application.ide/xtend-gen/hu/bme/mit/inf/dslreasoner/application/ide/.ApplicationConfigurationIdeModule.xtendbin index 51a755e5..bd1eabaf 100644 Binary files a/Application/hu.bme.mit.inf.dslreasoner.application.ide/xtend-gen/hu/bme/mit/inf/dslreasoner/application/ide/.ApplicationConfigurationIdeModule.xtendbin and b/Application/hu.bme.mit.inf.dslreasoner.application.ide/xtend-gen/hu/bme/mit/inf/dslreasoner/application/ide/.ApplicationConfigurationIdeModule.xtendbin differ diff --git a/Application/hu.bme.mit.inf.dslreasoner.application.ide/xtend-gen/hu/bme/mit/inf/dslreasoner/application/ide/.ApplicationConfigurationIdeSetup.xtendbin b/Application/hu.bme.mit.inf.dslreasoner.application.ide/xtend-gen/hu/bme/mit/inf/dslreasoner/application/ide/.ApplicationConfigurationIdeSetup.xtendbin index 27588633..f4956ec0 100644 Binary files a/Application/hu.bme.mit.inf.dslreasoner.application.ide/xtend-gen/hu/bme/mit/inf/dslreasoner/application/ide/.ApplicationConfigurationIdeSetup.xtendbin and b/Application/hu.bme.mit.inf.dslreasoner.application.ide/xtend-gen/hu/bme/mit/inf/dslreasoner/application/ide/.ApplicationConfigurationIdeSetup.xtendbin differ diff --git a/Application/org.eclipse.viatra.solver.language.ui/xtend-gen/org/eclipse/viatra/solver/language/ui/syntaxcoloring/.SolverSemanticHighlightCalculator.xtendbin b/Application/org.eclipse.viatra.solver.language.ui/xtend-gen/org/eclipse/viatra/solver/language/ui/syntaxcoloring/.SolverSemanticHighlightCalculator.xtendbin index 816f1516..0ee6ab93 100644 Binary files a/Application/org.eclipse.viatra.solver.language.ui/xtend-gen/org/eclipse/viatra/solver/language/ui/syntaxcoloring/.SolverSemanticHighlightCalculator.xtendbin and b/Application/org.eclipse.viatra.solver.language.ui/xtend-gen/org/eclipse/viatra/solver/language/ui/syntaxcoloring/.SolverSemanticHighlightCalculator.xtendbin differ diff --git a/Application/org.eclipse.viatra.solver.language.ui/xtend-gen/org/eclipse/viatra/solver/language/ui/syntaxcoloring/.SolverSemanticTextAttributeProvider.xtendbin b/Application/org.eclipse.viatra.solver.language.ui/xtend-gen/org/eclipse/viatra/solver/language/ui/syntaxcoloring/.SolverSemanticTextAttributeProvider.xtendbin index bc22802d..1fbc1b5a 100644 Binary files a/Application/org.eclipse.viatra.solver.language.ui/xtend-gen/org/eclipse/viatra/solver/language/ui/syntaxcoloring/.SolverSemanticTextAttributeProvider.xtendbin and b/Application/org.eclipse.viatra.solver.language.ui/xtend-gen/org/eclipse/viatra/solver/language/ui/syntaxcoloring/.SolverSemanticTextAttributeProvider.xtendbin differ diff --git a/Application/org.eclipse.viatra.solver.language.ui/xtend-gen/org/eclipse/viatra/solver/language/validation/.SolverLanguageValidator.xtendbin b/Application/org.eclipse.viatra.solver.language.ui/xtend-gen/org/eclipse/viatra/solver/language/validation/.SolverLanguageValidator.xtendbin index 6086ad61..6dfd9bdd 100644 Binary files a/Application/org.eclipse.viatra.solver.language.ui/xtend-gen/org/eclipse/viatra/solver/language/validation/.SolverLanguageValidator.xtendbin and b/Application/org.eclipse.viatra.solver.language.ui/xtend-gen/org/eclipse/viatra/solver/language/validation/.SolverLanguageValidator.xtendbin differ diff --git a/Application/org.eclipse.viatra.solver.language/xtend-gen/org/eclipse/viatra/solver/language/parser/antlr/.SolverLanguageTokenDefInjectingParser.xtendbin b/Application/org.eclipse.viatra.solver.language/xtend-gen/org/eclipse/viatra/solver/language/parser/antlr/.SolverLanguageTokenDefInjectingParser.xtendbin index 1fe63cb7..9e4a0e33 100644 Binary files a/Application/org.eclipse.viatra.solver.language/xtend-gen/org/eclipse/viatra/solver/language/parser/antlr/.SolverLanguageTokenDefInjectingParser.xtendbin and b/Application/org.eclipse.viatra.solver.language/xtend-gen/org/eclipse/viatra/solver/language/parser/antlr/.SolverLanguageTokenDefInjectingParser.xtendbin differ diff --git a/Application/org.eclipse.viatra.solver.language/xtend-gen/org/eclipse/viatra/solver/language/serializer/.SolverLanguageSyntheticTokenSyntacticSequencer.xtendbin b/Application/org.eclipse.viatra.solver.language/xtend-gen/org/eclipse/viatra/solver/language/serializer/.SolverLanguageSyntheticTokenSyntacticSequencer.xtendbin index 1c7b8eb2..2a1c8746 100644 Binary files a/Application/org.eclipse.viatra.solver.language/xtend-gen/org/eclipse/viatra/solver/language/serializer/.SolverLanguageSyntheticTokenSyntacticSequencer.xtendbin and b/Application/org.eclipse.viatra.solver.language/xtend-gen/org/eclipse/viatra/solver/language/serializer/.SolverLanguageSyntheticTokenSyntacticSequencer.xtendbin differ diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/META-INF/MANIFEST.MF b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/META-INF/MANIFEST.MF index f9090901..b9da0f0b 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/META-INF/MANIFEST.MF +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/META-INF/MANIFEST.MF @@ -17,15 +17,16 @@ Require-Bundle: hu.bme.mit.inf.dslreasoner.logic.model;bundle-version="1.0.0", org.eclipse.xtext.xbase.lib, org.eclipse.xtend.lib, org.eclipse.xtend.lib.macro, - org.eclipse.viatra.query.runtime;bundle-version="1.5.0", - org.eclipse.viatra.query.runtime.base.itc;bundle-version="1.5.0", - org.eclipse.viatra.query.patternlanguage.emf;bundle-version="1.5.0", + org.eclipse.viatra.query.runtime;bundle-version="2.0.0", + org.eclipse.viatra.query.runtime.base.itc;bundle-version="2.0.0", + org.eclipse.viatra.query.patternlanguage.emf;bundle-version="2.0.0", com.google.inject;bundle-version="3.0.0", org.eclipse.xtext;bundle-version="2.10.0", - org.eclipse.viatra.transformation.runtime.emf;bundle-version="1.5.0", + org.eclipse.viatra.transformation.runtime.emf;bundle-version="2.0.0", org.eclipse.xtext.xbase;bundle-version="2.10.0", com.microsoft.z3;bundle-version="4.8.5", - hu.bme.mit.inf.dslreasoner.ilp.cbc;bundle-version="1.0.0" + hu.bme.mit.inf.dslreasoner.ilp.cbc;bundle-version="1.0.0", + org.eclipse.viatra.query.runtime.rete;bundle-version="2.0.0" Bundle-RequiredExecutionEnvironment: JavaSE-1.8 Import-Package: org.apache.log4j Automatic-Module-Name: hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatraquery diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/RefinementRuleProvider.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/RefinementRuleProvider.xtend index 863ee18b..1d976e14 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/RefinementRuleProvider.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/RefinementRuleProvider.xtend @@ -27,6 +27,7 @@ import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.par import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialStringInterpretation import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialTypeInterpratation import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialinterpretationFactory +import java.lang.reflect.Field import java.util.HashMap import java.util.LinkedHashMap import java.util.LinkedList @@ -38,6 +39,7 @@ import org.eclipse.viatra.query.runtime.api.IQuerySpecification import org.eclipse.viatra.query.runtime.api.ViatraQueryEngine import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher import org.eclipse.viatra.query.runtime.emf.EMFScope +import org.eclipse.viatra.query.runtime.rete.matcher.ReteBackendFactory import org.eclipse.viatra.transformation.runtime.emf.rules.batch.BatchTransformationRule import org.eclipse.viatra.transformation.runtime.emf.rules.batch.BatchTransformationRuleFactory import org.eclipse.xtend.lib.annotations.Data @@ -47,186 +49,180 @@ class RefinementRuleProvider { val extension BatchTransformationRuleFactory factory = new BatchTransformationRuleFactory val extension PartialinterpretationFactory factory2 = PartialinterpretationFactory.eINSTANCE val extension LogiclanguageFactory factory3 = LogiclanguageFactory.eINSTANCE - + var AdvancedViatraQueryEngine queryEngine - + var Field delayMessageDelivery + def canonizeName(String name) { - return name.replace(' ','_') + return name.replace(' ', '_') } - + def LinkedHashMap>> createObjectRefinementRules( - LogicProblem p, - PartialInterpretation i, - GeneratedPatterns patterns, - ScopePropagator scopePropagator, - boolean nameNewElement, - ModelGenerationStatistics statistics - ) - { + LogicProblem p, + PartialInterpretation i, + GeneratedPatterns patterns, + ScopePropagator scopePropagator, + boolean nameNewElement, + ModelGenerationStatistics statistics + ) { val res = new LinkedHashMap - val recursiveObjectCreation = recursiveObjectCreation(p,i) + val recursiveObjectCreation = recursiveObjectCreation(p, i) queryEngine = ViatraQueryEngine.on(new EMFScope(i)) as AdvancedViatraQueryEngine - for(LHSEntry: patterns.refineObjectQueries.entrySet) { + delayMessageDelivery = queryEngine.class.getDeclaredField("delayMessageDelivery") + delayMessageDelivery.accessible = true + for (LHSEntry : patterns.refineObjectQueries.entrySet) { val containmentRelation = LHSEntry.key.containmentRelation val inverseRelation = LHSEntry.key.inverseContainment val type = LHSEntry.key.newType val lhs = LHSEntry.value as IQuerySpecification> - val rule = createObjectCreationRule(p,containmentRelation,inverseRelation,type,recursiveObjectCreation.get(type),lhs,nameNewElement,scopePropagator,statistics) - res.put(LHSEntry.key,rule) + val rule = createObjectCreationRule(p, containmentRelation, inverseRelation, type, + recursiveObjectCreation.get(type), lhs, nameNewElement, scopePropagator, statistics) + res.put(LHSEntry.key, rule) } return res } - - def private createObjectCreationRule( - LogicProblem p, - Relation containmentRelation, - Relation inverseRelation, - Type type, - List recursiceObjectCreations, - IQuerySpecification> lhs, - boolean nameNewElement, - ScopePropagator scopePropagator, - ModelGenerationStatistics statistics) - { - val name = '''addObject_«type.name.canonizeName»« - IF containmentRelation!==null»_by_«containmentRelation.name.canonizeName»«ENDIF»''' - val ruleBuilder = factory.createRule(lhs) - .name(name) - if(containmentRelation !== null) { - if(inverseRelation!== null) { - ruleBuilder.action[match | + + def private createObjectCreationRule(LogicProblem p, Relation containmentRelation, Relation inverseRelation, + Type type, List recursiceObjectCreations, + IQuerySpecification> lhs, boolean nameNewElement, + ScopePropagator scopePropagator, ModelGenerationStatistics statistics) { + val name = '''addObject_«type.name.canonizeName»«IF containmentRelation!==null»_by_«containmentRelation.name.canonizeName»«ENDIF»''' + val ruleBuilder = factory.createRule(lhs).name(name) + if (containmentRelation !== null) { + if (inverseRelation !== null) { + ruleBuilder.action [ match | statistics.incrementTransformationCount // println(name) - //val problem = match.get(0) as LogicProblem + // val problem = match.get(0) as LogicProblem val interpretation = match.get(1) as PartialInterpretation val relationInterpretation = match.get(2) as PartialRelationInterpretation val inverseRelationInterpretation = match.get(3) as PartialRelationInterpretation val typeInterpretation = match.get(4) as PartialComplexTypeInterpretation val container = match.get(5) as DefinedElement - - queryEngine.delayUpdatePropagation [ - val startTime = System.nanoTime - createObjectActionWithContainmentAndInverse( - nameNewElement, - interpretation, - typeInterpretation, - container, - relationInterpretation, - inverseRelationInterpretation, - [createDefinedElement], - recursiceObjectCreations, - scopePropagator - ) - statistics.addExecutionTime(System.nanoTime-startTime) - ] - + + val startTime = System.nanoTime + createObjectActionWithContainmentAndInverse( + nameNewElement, + interpretation, + typeInterpretation, + container, + relationInterpretation, + inverseRelationInterpretation, + [createDefinedElement], + recursiceObjectCreations, + scopePropagator + ) + statistics.addExecutionTime(System.nanoTime - startTime) + + flushQueryEngine + // Scope propagation - queryEngine.delayUpdatePropagation [ - val propagatorStartTime = System.nanoTime - scopePropagator.propagateAllScopeConstraints() - statistics.addScopePropagationTime(System.nanoTime-propagatorStartTime) - ] + val propagatorStartTime = System.nanoTime + scopePropagator.propagateAllScopeConstraints() + statistics.addScopePropagationTime(System.nanoTime - propagatorStartTime) ] } else { - ruleBuilder.action[match | + ruleBuilder.action [ match | statistics.incrementTransformationCount // println(name) - //val problem = match.get(0) as LogicProblem + // val problem = match.get(0) as LogicProblem val interpretation = match.get(1) as PartialInterpretation val relationInterpretation = match.get(2) as PartialRelationInterpretation val typeInterpretation = match.get(3) as PartialComplexTypeInterpretation val container = match.get(4) as DefinedElement - - queryEngine.delayUpdatePropagation [ - val startTime = System.nanoTime - createObjectActionWithContainment( - nameNewElement, - interpretation, - typeInterpretation, - container, - relationInterpretation, - [createDefinedElement], - recursiceObjectCreations, - scopePropagator - ) - statistics.addExecutionTime(System.nanoTime-startTime) - ] - - // Scope propagation - queryEngine.delayUpdatePropagation [ - val propagatorStartTime = System.nanoTime - scopePropagator.propagateAllScopeConstraints() - statistics.addScopePropagationTime(System.nanoTime-propagatorStartTime) - ] - ] - } - } else { - ruleBuilder.action[match | - statistics.incrementTransformationCount -// println(name) - //val problem = match.get(0) as LogicProblem - val interpretation = match.get(1) as PartialInterpretation - val typeInterpretation = match.get(2) as PartialComplexTypeInterpretation - queryEngine.delayUpdatePropagation [ val startTime = System.nanoTime - createObjectAction( + createObjectActionWithContainment( nameNewElement, interpretation, typeInterpretation, + container, + relationInterpretation, [createDefinedElement], recursiceObjectCreations, scopePropagator ) - statistics.addExecutionTime(System.nanoTime-startTime) - ] - - // Scope propagation - queryEngine.delayUpdatePropagation [ + statistics.addExecutionTime(System.nanoTime - startTime) + + flushQueryEngine + + // Scope propagation val propagatorStartTime = System.nanoTime scopePropagator.propagateAllScopeConstraints() - statistics.addScopePropagationTime(System.nanoTime-propagatorStartTime) + statistics.addScopePropagationTime(System.nanoTime - propagatorStartTime) ] + } + } else { + ruleBuilder.action [ match | + statistics.incrementTransformationCount +// println(name) + // val problem = match.get(0) as LogicProblem + val interpretation = match.get(1) as PartialInterpretation + val typeInterpretation = match.get(2) as PartialComplexTypeInterpretation + + val startTime = System.nanoTime + createObjectAction( + nameNewElement, + interpretation, + typeInterpretation, + [createDefinedElement], + recursiceObjectCreations, + scopePropagator + ) + statistics.addExecutionTime(System.nanoTime - startTime) + + flushQueryEngine + + // Scope propagation + val propagatorStartTime = System.nanoTime + scopePropagator.propagateAllScopeConstraints() + statistics.addScopePropagationTime(System.nanoTime - propagatorStartTime) ] } return ruleBuilder.build } - + def private recursiveObjectCreation(LogicProblem p, PartialInterpretation i) { - val Map> recursiveObjectCreation = new HashMap - for(type : p.types) { - recursiveObjectCreation.put(type,new LinkedList) + val Map> recursiveObjectCreation = new HashMap + for (type : p.types) { + recursiveObjectCreation.put(type, new LinkedList) } - + val containmentReferences = p.containmentHierarchies.head.containmentRelations - - for(relationInterpretation : i.partialrelationinterpretation) { + + for (relationInterpretation : i.partialrelationinterpretation) { val relation = relationInterpretation.interpretationOf val lowermultiplicities = p.annotations.filter(LowerMultiplicityAssertion).filter[it.relation === relation] - if((!lowermultiplicities.empty)) { + if ((!lowermultiplicities.empty)) { val number = lowermultiplicities.head.lower - if(number > 0) { - val sourceTypeInterpretation = getTypeInterpretation(i, relation, 0) as PartialComplexTypeInterpretation - val subtypeInterpretations = i.partialtypeinterpratation.filter(PartialComplexTypeInterpretation).filter[ - it === sourceTypeInterpretation || - it.supertypeInterpretation.contains(sourceTypeInterpretation) - ] - - if(containmentReferences.contains(relation)) { + if (number > 0) { + val sourceTypeInterpretation = getTypeInterpretation(i, relation, + 0) as PartialComplexTypeInterpretation + val subtypeInterpretations = i.partialtypeinterpratation.filter(PartialComplexTypeInterpretation). + filter [ + it === sourceTypeInterpretation || + it.supertypeInterpretation.contains(sourceTypeInterpretation) + ] + + if (containmentReferences.contains(relation)) { val targetTypeInterpretation = getTypeInterpretation(i, relation, 1) val targetType = (targetTypeInterpretation as PartialComplexTypeInterpretation).interpretationOf - if((!targetType.isIsAbstract) && (targetType.supertypes.empty)) { - val inverseAnnotation = p.annotations.filter(InverseRelationAssertion).filter[it.inverseA === relation || it.inverseB === relation] - if(!inverseAnnotation.empty) { - val onlyInverseAnnotation = if(inverseAnnotation.head.inverseA===relation) { - inverseAnnotation.head.inverseB - } else { - inverseAnnotation.head.inverseA - } - val inverseRelationInterpretation = i.partialrelationinterpretation.filter[it.interpretationOf === onlyInverseAnnotation].head - for(subTypeInterpretation : subtypeInterpretations) { - for(var times=0; times getTypeConstructor(PartialComplexTypeInterpretation reference) { + [createDefinedElement] + } + + private dispatch def Function0 getTypeConstructor(PartialBooleanInterpretation reference) { + [createBooleanElement] } - private dispatch def Function0 getTypeConstructor(PartialComplexTypeInterpretation reference) { [createDefinedElement] } - private dispatch def Function0 getTypeConstructor(PartialBooleanInterpretation reference) { [createBooleanElement] } - private dispatch def Function0 getTypeConstructor(PartialIntegerInterpretation reference) { [createIntegerElement] } - private dispatch def Function0 getTypeConstructor(PartialRealInterpretation reference) { [createRealElement] } - private dispatch def Function0 getTypeConstructor(PartialStringInterpretation reference) { [createStringElement] } - - - def createRelationRefinementRules(GeneratedPatterns patterns, ScopePropagator scopePropagator, ModelGenerationStatistics statistics) { + + private dispatch def Function0 getTypeConstructor(PartialIntegerInterpretation reference) { + [createIntegerElement] + } + + private dispatch def Function0 getTypeConstructor(PartialRealInterpretation reference) { + [createRealElement] + } + + private dispatch def Function0 getTypeConstructor(PartialStringInterpretation reference) { + [createStringElement] + } + + def createRelationRefinementRules(GeneratedPatterns patterns, ScopePropagator scopePropagator, + ModelGenerationStatistics statistics) { val res = new LinkedHashMap - for(LHSEntry: patterns.refinerelationQueries.entrySet) { + for (LHSEntry : patterns.refinerelationQueries.entrySet) { val declaration = LHSEntry.key.key val inverseReference = LHSEntry.key.value val lhs = LHSEntry.value as IQuerySpecification> - val rule = createRelationRefinementRule(declaration,inverseReference,lhs,scopePropagator,statistics) - res.put(LHSEntry.key,rule) + val rule = createRelationRefinementRule(declaration, inverseReference, lhs, scopePropagator, statistics) + res.put(LHSEntry.key, rule) } return res } - - def private BatchTransformationRule> - createRelationRefinementRule(RelationDeclaration declaration, Relation inverseRelation, IQuerySpecification> lhs, ScopePropagator scopePropagator, ModelGenerationStatistics statistics) - { + + def private BatchTransformationRule> createRelationRefinementRule( + RelationDeclaration declaration, Relation inverseRelation, + IQuerySpecification> lhs, ScopePropagator scopePropagator, + ModelGenerationStatistics statistics) { val name = '''addRelation_«declaration.name.canonizeName»«IF inverseRelation !== null»_and_«inverseRelation.name.canonizeName»«ENDIF»''' - val ruleBuilder = factory.createRule(lhs) - .name(name) + val ruleBuilder = factory.createRule(lhs).name(name) if (inverseRelation === null) { ruleBuilder.action [ match | statistics.incrementTransformationCount - + // println(name) // val problem = match.get(0) as LogicProblem // val interpretation = match.get(1) as PartialInterpretation val relationInterpretation = match.get(2) as PartialRelationInterpretation val src = match.get(3) as DefinedElement val trg = match.get(4) as DefinedElement - + queryEngine.delayUpdatePropagation [ val startTime = System.nanoTime createRelationLinkAction(src, trg, relationInterpretation) - statistics.addExecutionTime(System.nanoTime-startTime) + statistics.addExecutionTime(System.nanoTime - startTime) ] - + // Scope propagation if (scopePropagator.isPropagationNeededAfterAdditionToRelation(declaration)) { queryEngine.delayUpdatePropagation [ val propagatorStartTime = System.nanoTime scopePropagator.propagateAllScopeConstraints() - statistics.addScopePropagationTime(System.nanoTime-propagatorStartTime) + statistics.addScopePropagationTime(System.nanoTime - propagatorStartTime) ] } ] @@ -391,33 +398,31 @@ class RefinementRuleProvider { val src = match.get(4) as DefinedElement val trg = match.get(5) as DefinedElement - queryEngine.delayUpdatePropagation [ - val startTime = System.nanoTime - createRelationLinkWithInverse(src, trg, relationInterpretation, inverseInterpretation) - statistics.addExecutionTime(System.nanoTime-startTime) - ] - + val startTime = System.nanoTime + createRelationLinkWithInverse(src, trg, relationInterpretation, inverseInterpretation) + statistics.addExecutionTime(System.nanoTime - startTime) + // Scope propagation if (scopePropagator.isPropagationNeededAfterAdditionToRelation(declaration)) { - queryEngine.delayUpdatePropagation [ - val propagatorStartTime = System.nanoTime - scopePropagator.propagateAllScopeConstraints() - statistics.addScopePropagationTime(System.nanoTime-propagatorStartTime) - ] + flushQueryEngine + + val propagatorStartTime = System.nanoTime + scopePropagator.propagateAllScopeConstraints() + statistics.addScopePropagationTime(System.nanoTime - propagatorStartTime) } ] } return ruleBuilder.build } - - ///////////////////////// + + // /////////////////////// // Actions - ///////////////////////// - - protected def void createObjectAction(boolean nameNewElement, ObjectCreationInterpretationData data, DefinedElement container, ScopePropagator scopePropagator) { - if(data.containerInterpretation !== null) { - if(data.containerInverseInterpretation !== null) { + // /////////////////////// + protected def void createObjectAction(boolean nameNewElement, ObjectCreationInterpretationData data, + DefinedElement container, ScopePropagator scopePropagator) { + if (data.containerInterpretation !== null) { + if (data.containerInverseInterpretation !== null) { createObjectActionWithContainmentAndInverse( nameNewElement, data.interpretation, @@ -451,9 +456,9 @@ class RefinementRuleProvider { scopePropagator ) } - + } - + protected def createObjectActionWithContainmentAndInverse( boolean nameNewElement, PartialInterpretation interpretation, @@ -466,36 +471,36 @@ class RefinementRuleProvider { ScopePropagator scopePropagator ) { val newElement = constructor.apply - if(nameNewElement) { + if (nameNewElement) { newElement.name = '''new «interpretation.newElements.size»''' } - + // Types typeInterpretation.elements += newElement - if(typeInterpretation instanceof PartialComplexTypeInterpretation) { + if (typeInterpretation instanceof PartialComplexTypeInterpretation) { typeInterpretation.supertypeInterpretation.forEach[it.elements += newElement] } // ContainmentRelation val newLink1 = factory2.createBinaryElementRelationLink => [it.param1 = container it.param2 = newElement] - relationInterpretation.relationlinks+=newLink1 + relationInterpretation.relationlinks += newLink1 // Inverse Containment val newLink2 = factory2.createBinaryElementRelationLink => [it.param1 = newElement it.param2 = container] - inverseRelationInterpretation.relationlinks+=newLink2 - + inverseRelationInterpretation.relationlinks += newLink2 + // Scope propagation scopePropagator.decrementTypeScope(typeInterpretation) - + // Existence - interpretation.newElements+=newElement - + interpretation.newElements += newElement + // Do recursive object creation - for(newConstructor : recursiceObjectCreations) { - createObjectAction(nameNewElement,newConstructor,newElement,scopePropagator) + for (newConstructor : recursiceObjectCreations) { + createObjectAction(nameNewElement, newConstructor, newElement, scopePropagator) } - + return newElement } - + protected def createObjectActionWithContainment( boolean nameNewElement, PartialInterpretation interpretation, @@ -507,77 +512,82 @@ class RefinementRuleProvider { ScopePropagator scopePropagator ) { val newElement = constructor.apply - if(nameNewElement) { + if (nameNewElement) { newElement.name = '''new «interpretation.newElements.size»''' } - + // Types typeInterpretation.elements += newElement - if(typeInterpretation instanceof PartialComplexTypeInterpretation) { + if (typeInterpretation instanceof PartialComplexTypeInterpretation) { typeInterpretation.supertypeInterpretation.forEach[it.elements += newElement] } // ContainmentRelation val newLink = factory2.createBinaryElementRelationLink => [it.param1 = container it.param2 = newElement] - relationInterpretation.relationlinks+=newLink - + relationInterpretation.relationlinks += newLink + // Scope propagation scopePropagator.decrementTypeScope(typeInterpretation) - + // Existence - interpretation.newElements+=newElement - + interpretation.newElements += newElement + // Do recursive object creation - for(newConstructor : recursiceObjectCreations) { - createObjectAction(nameNewElement,newConstructor,newElement,scopePropagator) + for (newConstructor : recursiceObjectCreations) { + createObjectAction(nameNewElement, newConstructor, newElement, scopePropagator) } - + return newElement } - - protected def createObjectAction( - boolean nameNewElement, - PartialInterpretation interpretation, - PartialTypeInterpratation typeInterpretation, - Function0 constructor, - List recursiceObjectCreations, - ScopePropagator scopePropagator) - { + + protected def createObjectAction(boolean nameNewElement, PartialInterpretation interpretation, + PartialTypeInterpratation typeInterpretation, Function0 constructor, + List recursiceObjectCreations, ScopePropagator scopePropagator) { val newElement = constructor.apply - if(nameNewElement) { + if (nameNewElement) { newElement.name = '''new «interpretation.newElements.size»''' } - + // Types typeInterpretation.elements += newElement - if(typeInterpretation instanceof PartialComplexTypeInterpretation) { + if (typeInterpretation instanceof PartialComplexTypeInterpretation) { typeInterpretation.supertypeInterpretation.forEach[it.elements += newElement] } - + // Scope propagation scopePropagator.decrementTypeScope(typeInterpretation) - + // Existence - interpretation.newElements+=newElement - + interpretation.newElements += newElement + // Do recursive object creation - for(newConstructor : recursiceObjectCreations) { - createObjectAction(nameNewElement,newConstructor,newElement,scopePropagator) + for (newConstructor : recursiceObjectCreations) { + createObjectAction(nameNewElement, newConstructor, newElement, scopePropagator) } - + return newElement } - - protected def boolean createRelationLinkAction(DefinedElement src, DefinedElement trg, PartialRelationInterpretation relationInterpretation) { + + protected def boolean createRelationLinkAction(DefinedElement src, DefinedElement trg, + PartialRelationInterpretation relationInterpretation) { val link = createBinaryElementRelationLink => [it.param1 = src it.param2 = trg] relationInterpretation.relationlinks += link } - - protected def boolean createRelationLinkWithInverse(DefinedElement src, DefinedElement trg, PartialRelationInterpretation relationInterpretation, PartialRelationInterpretation inverseInterpretation) { + + protected def boolean createRelationLinkWithInverse(DefinedElement src, DefinedElement trg, + PartialRelationInterpretation relationInterpretation, PartialRelationInterpretation inverseInterpretation) { val link = createBinaryElementRelationLink => [it.param1 = src it.param2 = trg] relationInterpretation.relationlinks += link val inverseLink = createBinaryElementRelationLink => [it.param1 = trg it.param2 = src] inverseInterpretation.relationlinks += inverseLink } + + protected def flushQueryEngine() { + if (queryEngine.updatePropagationDelayed) { + delayMessageDelivery.setBoolean(queryEngine, false) + queryEngine.getQueryBackend(ReteBackendFactory.INSTANCE).flushUpdates + delayMessageDelivery.setBoolean(queryEngine, true) + } + } } @Data diff --git a/Solvers/VIATRA-Solver/org.eclipse.viatra.dse/src/org/eclipse/viatra/dse/api/SolutionTrajectory.java b/Solvers/VIATRA-Solver/org.eclipse.viatra.dse/src/org/eclipse/viatra/dse/api/SolutionTrajectory.java index d1a41065..500dd7d2 100644 --- a/Solvers/VIATRA-Solver/org.eclipse.viatra.dse/src/org/eclipse/viatra/dse/api/SolutionTrajectory.java +++ b/Solvers/VIATRA-Solver/org.eclipse.viatra.dse/src/org/eclipse/viatra/dse/api/SolutionTrajectory.java @@ -206,7 +206,14 @@ public class SolutionTrajectory { } }; long start = System.nanoTime(); - editingDomain.getCommandStack().execute(cc); + try { + ((AdvancedViatraQueryEngine) engine).delayUpdatePropagation(() -> { + editingDomain.getCommandStack().execute(cc); + return null; + }); + } catch (InvocationTargetException e) { + throw new RuntimeException(e); + } listener.forwardWorked(System.nanoTime() - start); } diff --git a/Solvers/VIATRA-Solver/org.eclipse.viatra.dse/src/org/eclipse/viatra/dse/base/DesignSpaceManager.java b/Solvers/VIATRA-Solver/org.eclipse.viatra.dse/src/org/eclipse/viatra/dse/base/DesignSpaceManager.java index 4c6b4097..7e7a6e51 100644 --- a/Solvers/VIATRA-Solver/org.eclipse.viatra.dse/src/org/eclipse/viatra/dse/base/DesignSpaceManager.java +++ b/Solvers/VIATRA-Solver/org.eclipse.viatra.dse/src/org/eclipse/viatra/dse/base/DesignSpaceManager.java @@ -151,7 +151,14 @@ public class DesignSpaceManager implements IBacktrackListener { Object previousState = trajectory.getCurrentStateId(); long start = System.nanoTime(); - domain.getCommandStack().execute(rc); + try { + engine.delayUpdatePropagation(() -> { + domain.getCommandStack().execute(rc); + return null; + }); + } catch (InvocationTargetException e) { + throw new RuntimeException(e); + } forwardTime += System.nanoTime() - start; Object newStateId = stateCoder.createStateCode(); @@ -270,7 +277,14 @@ public class DesignSpaceManager implements IBacktrackListener { }; long start = System.nanoTime(); - domain.getCommandStack().execute(rc); + try { + engine.delayUpdatePropagation(() -> { + domain.getCommandStack().execute(rc); + return null; + }); + } catch (InvocationTargetException e) { + throw new RuntimeException(e); + } forwardTime += System.nanoTime() - start; Object newStateId = null; -- cgit v1.2.3-70-g09d2 From 18d8ff15abeb2aecc3cdedb0eabb076b4b8f058c Mon Sep 17 00:00:00 2001 From: Kristóf Marussy Date: Wed, 29 Jul 2020 16:40:45 +0200 Subject: Fix time measurement --- .../.ApplicationConfigurationIdeModule.xtendbin | Bin 1701 -> 1701 bytes .../ide/.ApplicationConfigurationIdeSetup.xtendbin | Bin 2526 -> 2526 bytes .../.SolverSemanticHighlightCalculator.xtendbin | Bin 5334 -> 5334 bytes .../.SolverSemanticTextAttributeProvider.xtendbin | Bin 4902 -> 4902 bytes .../validation/.SolverLanguageValidator.xtendbin | Bin 1717 -> 1717 bytes ....SolverLanguageTokenDefInjectingParser.xtendbin | Bin 2742 -> 2742 bytes ...nguageSyntheticTokenSyntacticSequencer.xtendbin | Bin 2758 -> 2758 bytes .../rules/RefinementRuleProvider.xtend | 18 ++- .../viatra/dse/base/DesignSpaceManager.java | 2 +- .../case.study.familyTree.run/bin/.gitignore | 1 - .../config/genericFamilyTreeSMTQual.vsconfig | 3 + .../queries/SatelliteQueries.vql | 144 +-------------------- 12 files changed, 13 insertions(+), 155 deletions(-) delete mode 100644 Tests/MODELS2020-CaseStudies/case.study.familyTree.run/bin/.gitignore (limited to 'Solvers/VIATRA-Solver/org.eclipse.viatra.dse/src/org/eclipse/viatra/dse/base/DesignSpaceManager.java') diff --git a/Application/hu.bme.mit.inf.dslreasoner.application.ide/xtend-gen/hu/bme/mit/inf/dslreasoner/application/ide/.ApplicationConfigurationIdeModule.xtendbin b/Application/hu.bme.mit.inf.dslreasoner.application.ide/xtend-gen/hu/bme/mit/inf/dslreasoner/application/ide/.ApplicationConfigurationIdeModule.xtendbin index 96d7f77b..2a740f24 100644 Binary files a/Application/hu.bme.mit.inf.dslreasoner.application.ide/xtend-gen/hu/bme/mit/inf/dslreasoner/application/ide/.ApplicationConfigurationIdeModule.xtendbin and b/Application/hu.bme.mit.inf.dslreasoner.application.ide/xtend-gen/hu/bme/mit/inf/dslreasoner/application/ide/.ApplicationConfigurationIdeModule.xtendbin differ diff --git a/Application/hu.bme.mit.inf.dslreasoner.application.ide/xtend-gen/hu/bme/mit/inf/dslreasoner/application/ide/.ApplicationConfigurationIdeSetup.xtendbin b/Application/hu.bme.mit.inf.dslreasoner.application.ide/xtend-gen/hu/bme/mit/inf/dslreasoner/application/ide/.ApplicationConfigurationIdeSetup.xtendbin index 85768640..6fd0f505 100644 Binary files a/Application/hu.bme.mit.inf.dslreasoner.application.ide/xtend-gen/hu/bme/mit/inf/dslreasoner/application/ide/.ApplicationConfigurationIdeSetup.xtendbin and b/Application/hu.bme.mit.inf.dslreasoner.application.ide/xtend-gen/hu/bme/mit/inf/dslreasoner/application/ide/.ApplicationConfigurationIdeSetup.xtendbin differ diff --git a/Application/org.eclipse.viatra.solver.language.ui/xtend-gen/org/eclipse/viatra/solver/language/ui/syntaxcoloring/.SolverSemanticHighlightCalculator.xtendbin b/Application/org.eclipse.viatra.solver.language.ui/xtend-gen/org/eclipse/viatra/solver/language/ui/syntaxcoloring/.SolverSemanticHighlightCalculator.xtendbin index 287aa50d..0b252347 100644 Binary files a/Application/org.eclipse.viatra.solver.language.ui/xtend-gen/org/eclipse/viatra/solver/language/ui/syntaxcoloring/.SolverSemanticHighlightCalculator.xtendbin and b/Application/org.eclipse.viatra.solver.language.ui/xtend-gen/org/eclipse/viatra/solver/language/ui/syntaxcoloring/.SolverSemanticHighlightCalculator.xtendbin differ diff --git a/Application/org.eclipse.viatra.solver.language.ui/xtend-gen/org/eclipse/viatra/solver/language/ui/syntaxcoloring/.SolverSemanticTextAttributeProvider.xtendbin b/Application/org.eclipse.viatra.solver.language.ui/xtend-gen/org/eclipse/viatra/solver/language/ui/syntaxcoloring/.SolverSemanticTextAttributeProvider.xtendbin index e9b25b0a..930ba6bf 100644 Binary files a/Application/org.eclipse.viatra.solver.language.ui/xtend-gen/org/eclipse/viatra/solver/language/ui/syntaxcoloring/.SolverSemanticTextAttributeProvider.xtendbin and b/Application/org.eclipse.viatra.solver.language.ui/xtend-gen/org/eclipse/viatra/solver/language/ui/syntaxcoloring/.SolverSemanticTextAttributeProvider.xtendbin differ diff --git a/Application/org.eclipse.viatra.solver.language.ui/xtend-gen/org/eclipse/viatra/solver/language/validation/.SolverLanguageValidator.xtendbin b/Application/org.eclipse.viatra.solver.language.ui/xtend-gen/org/eclipse/viatra/solver/language/validation/.SolverLanguageValidator.xtendbin index 79d18e32..65fea578 100644 Binary files a/Application/org.eclipse.viatra.solver.language.ui/xtend-gen/org/eclipse/viatra/solver/language/validation/.SolverLanguageValidator.xtendbin and b/Application/org.eclipse.viatra.solver.language.ui/xtend-gen/org/eclipse/viatra/solver/language/validation/.SolverLanguageValidator.xtendbin differ diff --git a/Application/org.eclipse.viatra.solver.language/xtend-gen/org/eclipse/viatra/solver/language/parser/antlr/.SolverLanguageTokenDefInjectingParser.xtendbin b/Application/org.eclipse.viatra.solver.language/xtend-gen/org/eclipse/viatra/solver/language/parser/antlr/.SolverLanguageTokenDefInjectingParser.xtendbin index c529b829..340908fe 100644 Binary files a/Application/org.eclipse.viatra.solver.language/xtend-gen/org/eclipse/viatra/solver/language/parser/antlr/.SolverLanguageTokenDefInjectingParser.xtendbin and b/Application/org.eclipse.viatra.solver.language/xtend-gen/org/eclipse/viatra/solver/language/parser/antlr/.SolverLanguageTokenDefInjectingParser.xtendbin differ diff --git a/Application/org.eclipse.viatra.solver.language/xtend-gen/org/eclipse/viatra/solver/language/serializer/.SolverLanguageSyntheticTokenSyntacticSequencer.xtendbin b/Application/org.eclipse.viatra.solver.language/xtend-gen/org/eclipse/viatra/solver/language/serializer/.SolverLanguageSyntheticTokenSyntacticSequencer.xtendbin index 9ff56ed9..21b52163 100644 Binary files a/Application/org.eclipse.viatra.solver.language/xtend-gen/org/eclipse/viatra/solver/language/serializer/.SolverLanguageSyntheticTokenSyntacticSequencer.xtendbin and b/Application/org.eclipse.viatra.solver.language/xtend-gen/org/eclipse/viatra/solver/language/serializer/.SolverLanguageSyntheticTokenSyntacticSequencer.xtendbin differ diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/RefinementRuleProvider.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/RefinementRuleProvider.xtend index f7fe97a3..699b095d 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/RefinementRuleProvider.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/RefinementRuleProvider.xtend @@ -372,19 +372,17 @@ class RefinementRuleProvider { val src = match.get(3) as DefinedElement val trg = match.get(4) as DefinedElement - queryEngine.delayUpdatePropagation [ - val startTime = System.nanoTime - createRelationLinkAction(src, trg, relationInterpretation) - statistics.addExecutionTime(System.nanoTime - startTime) - ] + val startTime = System.nanoTime + createRelationLinkAction(src, trg, relationInterpretation) + statistics.addExecutionTime(System.nanoTime - startTime) // Scope propagation if (scopePropagator.isPropagationNeededAfterAdditionToRelation(declaration)) { - queryEngine.delayUpdatePropagation [ - val propagatorStartTime = System.nanoTime - scopePropagator.propagateAllScopeConstraints() - statistics.addScopePropagationTime(System.nanoTime - propagatorStartTime) - ] + flushQueryEngine(scopePropagator) + + val propagatorStartTime = System.nanoTime + scopePropagator.propagateAllScopeConstraints() + statistics.addScopePropagationTime(System.nanoTime - propagatorStartTime) } ] } else { diff --git a/Solvers/VIATRA-Solver/org.eclipse.viatra.dse/src/org/eclipse/viatra/dse/base/DesignSpaceManager.java b/Solvers/VIATRA-Solver/org.eclipse.viatra.dse/src/org/eclipse/viatra/dse/base/DesignSpaceManager.java index 7e7a6e51..133ef948 100644 --- a/Solvers/VIATRA-Solver/org.eclipse.viatra.dse/src/org/eclipse/viatra/dse/base/DesignSpaceManager.java +++ b/Solvers/VIATRA-Solver/org.eclipse.viatra.dse/src/org/eclipse/viatra/dse/base/DesignSpaceManager.java @@ -369,6 +369,7 @@ public class DesignSpaceManager implements IBacktrackListener { } catch (InvocationTargetException e) { throw new RuntimeException(e); } + backtrackingTime += System.nanoTime() - start; updateActivationCodes(); Object lastActivationId = trajectory.getLastActivationId(); @@ -382,7 +383,6 @@ public class DesignSpaceManager implements IBacktrackListener { } logger.debug("Backtrack."); - backtrackingTime += System.nanoTime() - start; return true; } diff --git a/Tests/MODELS2020-CaseStudies/case.study.familyTree.run/bin/.gitignore b/Tests/MODELS2020-CaseStudies/case.study.familyTree.run/bin/.gitignore deleted file mode 100644 index 7050a7e3..00000000 --- a/Tests/MODELS2020-CaseStudies/case.study.familyTree.run/bin/.gitignore +++ /dev/null @@ -1 +0,0 @@ -/queries/ diff --git a/Tests/MODELS2020-CaseStudies/case.study.pledge.run/config/genericFamilyTreeSMTQual.vsconfig b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/config/genericFamilyTreeSMTQual.vsconfig index 80ab2906..fa9cd6e2 100644 --- a/Tests/MODELS2020-CaseStudies/case.study.pledge.run/config/genericFamilyTreeSMTQual.vsconfig +++ b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/config/genericFamilyTreeSMTQual.vsconfig @@ -36,6 +36,9 @@ generate { log-level = normal, "fitness-punishSize" = "false", "fitness-scope" = "3", + "fitness-objectCreationCosts" = "true", + "scopePropagator" = "typeHierarchy", + "fitness-missing-containment" = "2", "numeric-solver-at-end" = "true" } diff --git a/Tests/MODELS2020-CaseStudies/case.study.pledge.run/queries/SatelliteQueries.vql b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/queries/SatelliteQueries.vql index 57b5933a..da889032 100644 --- a/Tests/MODELS2020-CaseStudies/case.study.pledge.run/queries/SatelliteQueries.vql +++ b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/queries/SatelliteQueries.vql @@ -245,146 +245,4 @@ pattern tooLowPathLengthForGroundStation(s:CommSubsystem) { GroundStationNetwork.commSubsystem(_,ts); check(l!=385000);//385.000km } -//// -//// Metrics -//// -// -//// Coverage -// -//pattern coverageMetric(Coverage : java Double) { -// Coverage == sum find missionCoverage(_, #_); -//} -// -//private pattern missionCoverage(Mission : InterferometryMission, Coverage : java Double) { -// InterferometryMission.observationTime(Mission, ObservationTime); -// ObserverCount == count find spacecraftWithInterferometryPayload(Mission, _); -// Coverage == eval(Math.pow(1 - 2.0 / ObserverCount, 1 + 9 * (1.0 / ObservationTime)) + 0.05 * ObservationTime / 3); -//} -// -//// Time -// -//pattern timeMetric(Time : java Double) { -// Time == sum find missionTime(_, #_); -//} -// -//private pattern missionTime(Mission : InterferometryMission, Time : java Double) { -// InterferometryMission.observationTime(Mission, ObservationTime); -// TrasmitTime == sum find transmitTime(Mission, _, #_); -// Time == eval(TrasmitTime + 60.0 * ObservationTime); -//} -// -//private pattern transmitTime(Mission : InterferometryMission, Spacecraft : Spacecraft, TransmitTime : java Double) { -// ConstellationMission.spacecraft(Mission, Spacecraft); -// find scienceData(Spacecraft, ScienceData); -// IncomingData == sum find incomingData(Spacecraft, _, #_); -// find transmitRate(Spacecraft, TransmitRate); -// TransmitTime == eval((ScienceData + IncomingData) / (7.5 * TransmitRate)); -//} -// -//private pattern incomingData(Spacecraft : Spacecraft, Source : Spacecraft, Data : java Double) { -// find indirectCommunicationLink(Source, Spacecraft); -// find scienceData(Source, Data); -//} -// -//private pattern scienceData(Spacecraft : Spacecraft, Data : java Double) { -// ConstellationMission.spacecraft(Mission, Spacecraft); -// InterferometryMission.observationTime(Mission, ObservationTime); -// Data == eval(12.0 * ObservationTime); -//} -// -//private pattern transmitRate(Spacecraft : Spacecraft, TransmitRate : java Double) { -// find spacecraftUplink(Spacecraft, Comm, Target); -// UHFCommSubsystem(Comm); -// Spacecraft(Target); -// TransmitRate == 5.0; -//} or { -// find spacecraftUplink(Spacecraft, Comm, Target); -// XCommSubsystem(Comm); -// Spacecraft(Target); -// TransmitRate == 1.6; -//} or { -// find spacecraftUplink(Spacecraft, Comm, Target); -// XCommSubsystem(Comm); -// GroundStationNetwork(Target); -// TransmitRate == 0.7; -//} or { -// find spacecraftUplink(Spacecraft, Comm, Target); -// KaCommSubsystem(Comm); -// Spacecraft(Target); -// TransmitRate == 220.0; -//} or { -// find spacecraftUplink(Spacecraft, Comm, Target); -// KaCommSubsystem(Comm); -// GroundStationNetwork(Target); -// TransmitRate == 80.0; -//} -// -//private pattern spacecraftUplink(Spacecraft : Spacecraft, TargetSubsystem : CommSubsystem, Target : CommunicatingElement) { -// CommunicatingElement.commSubsystem.target(Spacecraft, TargetSubsystem); -// CommunicatingElement.commSubsystem(Target, TargetSubsystem); -//} -// -//// Cost -// -//pattern costMetric(Cost : java Double) { -// Cost == sum find missionCost(_, #_); -//} -// -//private pattern missionCost(Mission : InterferometryMission, Cost : java Double) { -// InterferometryMission.observationTime(Mission, ObservationTime); -// SpacecraftCost == sum find spacecraftCost(Mission, _, #_); -// Cost == eval(SpacecraftCost + 100000.0 * ObservationTime); -//} -// -//private pattern spacecraftCost(Mission : InterferometryMission, Spacecraft : Spacecraft, Cost : java Double) { -// ConstellationMission.spacecraft(Mission, Spacecraft); -// find spacecraftOfKindCount(Spacecraft, KindCount); -// find basePrice(Spacecraft, BasePrice); -// find interferometryPayloadCost(Spacecraft, InterferometryPayloadCost); -// find additionalCommSubsystemCost(Spacecraft, AdditionalCommSubsystemCost); -// Cost == eval(BasePrice * Math.pow(KindCount, -0.25) + InterferometryPayloadCost + AdditionalCommSubsystemCost); -//} -// -//private pattern spacecraftOfKindCount(Sat : Spacecraft, Count : java Integer) { -// CubeSat3U(Sat); -// Count == count find cubeSat3U(_); -//} or { -// CubeSat6U(Sat); -// Count == count find cubeSat6U(_); -//} or { -// SmallSat(Sat); -// Count == count find smallSat(_); -//} -// -//private pattern basePrice(Spacecraft : Spacecraft, BasePrice : java Double) { -// CubeSat3U(Spacecraft); -// BasePrice == 250000.0; -//} or { -// CubeSat6U(Spacecraft); -// BasePrice == 750000.0; -//} or { -// SmallSat(Spacecraft); -// BasePrice == 3000000.0; -//} -// -//private pattern interferometryPayloadCost(Spacecraft : Spacecraft, Cost : java Double) { -// find spacecraftWithInterferometryPayload(_, Spacecraft); -// Cost == 50000.0; -//} or { -// neg find spacecraftWithInterferometryPayload(_, Spacecraft); -// Cost == 0.0; -//} -// -//private pattern additionalCommSubsystemCost(Spacecraft : Spacecraft, Cost : java Double) { -// find spacecraftWithTwoCommSubsystems(Spacecraft); -// Cost == 100000.0; -//} or { -// neg find spacecraftWithTwoCommSubsystems(Spacecraft); -// Cost == 0.0; -//} -// -//private pattern spacecraftWithTwoCommSubsystems(Spacecraft : Spacecraft) { -// Spacecraft.commSubsystem(Spacecraft, Subsystem1); -// Spacecraft.commSubsystem(Spacecraft, Subsystem2); -// Subsystem1 != Subsystem2; -//} + -- cgit v1.2.3-70-g09d2