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 --- .../dse/api/strategy/impl/DepthFirstStrategy.java | 188 +++++++++++++++++++++ 1 file changed, 188 insertions(+) create mode 100644 Solvers/VIATRA-Solver/org.eclipse.viatra.dse/src/org/eclipse/viatra/dse/api/strategy/impl/DepthFirstStrategy.java (limited to 'Solvers/VIATRA-Solver/org.eclipse.viatra.dse/src/org/eclipse/viatra/dse/api/strategy/impl/DepthFirstStrategy.java') diff --git a/Solvers/VIATRA-Solver/org.eclipse.viatra.dse/src/org/eclipse/viatra/dse/api/strategy/impl/DepthFirstStrategy.java b/Solvers/VIATRA-Solver/org.eclipse.viatra.dse/src/org/eclipse/viatra/dse/api/strategy/impl/DepthFirstStrategy.java new file mode 100644 index 00000000..22a4a683 --- /dev/null +++ b/Solvers/VIATRA-Solver/org.eclipse.viatra.dse/src/org/eclipse/viatra/dse/api/strategy/impl/DepthFirstStrategy.java @@ -0,0 +1,188 @@ +/******************************************************************************* + * Copyright (c) 2010-2016, Andras Szabolcs Nagy, 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.api.strategy.impl; + +import java.util.Collection; +import java.util.Iterator; +import java.util.Random; +import java.util.concurrent.atomic.AtomicBoolean; + +import org.apache.log4j.Logger; +import org.eclipse.viatra.dse.api.DSEException; +import org.eclipse.viatra.dse.api.strategy.interfaces.IStrategy; +import org.eclipse.viatra.dse.base.ThreadContext; +import org.eclipse.viatra.dse.objectives.Fitness; + +/** + * A depth-first search algorithm implementation, that + * + * + * @author Andras Szabolcs Nagy + * + */ +public class DepthFirstStrategy implements IStrategy { + + private int maxDepth; + private AtomicBoolean isInterrupted = new AtomicBoolean(false); + private ThreadContext context; + + private Logger logger = Logger.getLogger(IStrategy.class); + + private Random random = new Random(); + private boolean backTrackIfSolution = true; + + /** + * Creates a new depth-first search algorithm without depth limit. + */ + public DepthFirstStrategy() { + this.maxDepth = Integer.MAX_VALUE; + } + + /** + * Creates a new depth-first search algorithm with depth limit. + * + * @param maxDepth + * A negative maxDepth means no depth limit, zero means the checking of the initial state. + */ + public DepthFirstStrategy(int maxDepth) { + if (maxDepth < 0) { + this.maxDepth = Integer.MAX_VALUE; + } else { + this.maxDepth = maxDepth; + } + } + + /** + * If called, the algorithm will not backtrack after the hard objectives are fulfilled, instead it goes deeper in + * the search space. + */ + public DepthFirstStrategy continueIfHardObjectivesFulfilled() { + backTrackIfSolution = false; + return this; + } + + @Override + public void initStrategy(ThreadContext context) { + this.context = context; + + if (context.getSharedObject() == null) { + context.setSharedObject(new Object()); + logger.info("Depth-first exploration strategy is initied."); + startThreads(); + } + + } + + private void startThreads() { + context.startAllThreads(() -> new DepthFirstStrategy(maxDepth)); + } + + @Override + public void explore() { + + mainloop: do { + + boolean globalConstraintsAreSatisfied = context.checkGlobalConstraints(); + if (!globalConstraintsAreSatisfied) { + boolean isSuccessfulUndo = context.backtrack(); + if (!isSuccessfulUndo) { + logger.info("Global contraint is not satisifed and cannot backtrack."); + break; + } else { + logger.debug("Global contraint is not satisifed, backtrack."); + continue; + } + } + + Fitness fitness = context.calculateFitness(); + if (fitness.isSatisifiesHardObjectives()) { + context.newSolution(); + if (backTrackIfSolution) { + boolean isSuccessfulUndo = context.backtrack(); + if (!isSuccessfulUndo) { + logger.info("Found a solution but cannot backtrack."); + break; + } else { + logger.debug("Found a solution, backtrack."); + continue; + } + } + } + + if (context.getDepth() >= maxDepth) { + boolean isSuccessfulUndo = context.backtrack(); + if (!isSuccessfulUndo) { + logger.info("Reached max depth but cannot bactrack."); + break; + } else { + logger.debug("Reached max depth, bactrack."); + continue; + } + } + + if (isInterrupted.get()) { + logger.info("Interrupted, stop exploration."); + break; + } + + Object activationId = null; + Collection activationIds; + + do { + activationIds = context.getUntraversedActivationIds(); + if (activationIds.isEmpty()) { + boolean isSuccessfulUndo = context.backtrack(); + if (!isSuccessfulUndo) { + logger.info("No more transitions from current state and cannot backtrack."); + break mainloop; + } else { + logger.debug("No more transitions from current state, backtrack."); + continue; + } + } + } while (activationIds.isEmpty()); + + int index = random.nextInt(activationIds.size()); + + Iterator iterator = activationIds.iterator(); + while (index-- > 0) { + iterator.next(); + } + activationId = iterator.next(); + + context.executeAcitvationId(activationId); + + boolean loopInTrajectory = context.isCurrentStateInTrajectory(); + if (loopInTrajectory) { + boolean isSuccessfulUndo = context.backtrack(); + if (!isSuccessfulUndo) { + throw new DSEException("The new state is present in the trajectoy but cannot bactkrack. Should never happen!"); + } else { + logger.info("The new state is already visited in the trajectory, backtrack."); + } + } + + } while (true); + + logger.info("Terminated."); + } + + @Override + public void interruptStrategy() { + isInterrupted.set(true); + } + +} -- cgit v1.2.3-70-g09d2