Merge Parallel Trace Abstraction into Dev

trunk/source/Library-Automata/META-INF/MANIFEST.MF

@@ -311,5 +311,6 @@ Bundle-ClassPath: src/de/uni_freiburg/informatik/ultimate/automata/petrinet/petr
 Import-Package: de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.structure,
  de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.transitions,
  de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.smt,
+ de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.smt.predicates,
  de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder.cfg
 Automatic-Module-Name: de.uni.freiburg.informatik.ultimate.lib.automata

trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/IsEmptyHeuristic.java

@@ -64,6 +64,7 @@
 import de.uni_freiburg.informatik.ultimate.util.CoreUtil;
 import de.uni_freiburg.informatik.ultimate.util.HashUtils;
 import de.uni_freiburg.informatik.ultimate.util.datastructures.HashedPriorityQueue;
+import de.uni_freiburg.informatik.ultimate.util.datastructures.relation.Pair;
 
 /**
  * Check emptiness and obtain an accepting run of a nested word automaton using a modified version of A*.
@@ -83,7 +84,8 @@ public final class IsEmptyHeuristic<LETTER, STATE> extends UnaryNwaOperation<LET
 	private final Predicate<STATE> mIsForbiddenState;
 	private final NestedRun<LETTER, STATE> mAcceptingRun;
 	private final STATE mDummyEmptyStackState;
-
+	protected final List<Pair<STATE, LETTER>> mWayPoints;
+	private boolean stillFollowingWayPoint = true;
 	private final IHeuristic<STATE, LETTER> mHeuristic;
 
 	/**
@@ -116,7 +118,25 @@ public IsEmptyHeuristic(final AutomataLibraryServices services,
 			final INwaOutgoingLetterAndTransitionProvider<LETTER, STATE> operand,
 			final IHeuristic<STATE, LETTER> heuristic) throws AutomataOperationCanceledException {
 		this(services, operand, CoreUtil.constructHashSet(operand.getInitialStates()), a -> false, operand::isFinal,
-				heuristic);
+				heuristic, new ArrayList<>());
+	}
+
+	/**
+	 * Default constructor. Here we search a run from the initial states of the automaton to the final states of the
+	 * automaton and use the zero heuristic.
+	 *
+	 * @param services
+	 *            Ultimate services
+	 * @param operand
+	 *            input NWA
+	 * @see #IsEmpty(AutomataLibraryServices, INwaOutgoingLetterAndTransitionProvider)
+	 */
+	public IsEmptyHeuristic(final AutomataLibraryServices services,
+			final INwaOutgoingLetterAndTransitionProvider<LETTER, STATE> operand,
+			final IHeuristic<STATE, LETTER> heuristic, final ArrayList<Pair<STATE, LETTER>> wayPoints)
+			throws AutomataOperationCanceledException {
+		this(services, operand, CoreUtil.constructHashSet(operand.getInitialStates()), a -> false, operand::isFinal,
+				heuristic, wayPoints);
 	}
 
 	/**
@@ -128,15 +148,15 @@ public IsEmptyHeuristic(final AutomataLibraryServices services, final INestedWor
 			final Set<STATE> startStates, final Predicate<STATE> funIsForbiddenState,
 			final Predicate<STATE> funIsGoalState, final IHeuristic<STATE, LETTER> heuristic)
 			throws AutomataOperationCanceledException {
-		this(services, (INwaOutgoingLetterAndTransitionProvider<LETTER, STATE>) operand, startStates,
-				funIsForbiddenState, funIsGoalState, heuristic);
+		this(services, operand, startStates, funIsForbiddenState, funIsGoalState, heuristic, new ArrayList<>());
 		assert operand.getStates().containsAll(startStates) : "unknown states";
 	}
 
-	private IsEmptyHeuristic(final AutomataLibraryServices services,
+	public IsEmptyHeuristic(final AutomataLibraryServices services,
 			final INwaOutgoingLetterAndTransitionProvider<LETTER, STATE> operand, final Set<STATE> startStates,
 			final Predicate<STATE> funIsForbiddenState, final Predicate<STATE> funIsGoalState,
-			final IHeuristic<STATE, LETTER> heuristic) throws AutomataOperationCanceledException {
+			final IHeuristic<STATE, LETTER> heuristic, final ArrayList<Pair<STATE, LETTER>> wayPoints)
+			throws AutomataOperationCanceledException {
 		super(services);
 		mOperand = operand;
 		mIsGoalState = funIsGoalState;
@@ -148,7 +168,10 @@ private IsEmptyHeuristic(final AutomataLibraryServices services,
 		assert mOperand != null;
 
 		mDummyEmptyStackState = mOperand.getEmptyStackState();
-
+		mWayPoints = wayPoints;
+		if (!mWayPoints.isEmpty()) {
+			stillFollowingWayPoint = true;
+		}
 		if (mLogger.isInfoEnabled()) {
 			mLogger.info(startMessage());
 		}
@@ -172,12 +195,13 @@ private NestedRun<LETTER, STATE> getAcceptingRun(final Collection<STATE> startSt
 		final HashedPriorityQueue<Item> worklist =
 				new HashedPriorityQueue<>(Comparator.comparing(a -> a.mEstimatedCostToTarget));
 
+		final List<Pair<STATE, LETTER>> visited = new ArrayList<>();
+
 		for (final STATE state : startStates) {
 			final Item initialItem = new Item(state);
 			initialItem.setCostSoFar(0.0);
 			worklist.add(initialItem);
 		}
-
 		if (mLogger.isDebugEnabled()) {
 			mLogger.debug(String.format("Initial queue: %s", worklist));
 		}
@@ -190,6 +214,8 @@ private NestedRun<LETTER, STATE> getAcceptingRun(final Collection<STATE> startSt
 		final Map<CallTransition, Map<ReturnTransition, SummaryItem>> summaries = new HashMap<>();
 		final Map<CallTransition, Map<ReturnTransition, Set<Item>>> usedSummaries = new HashMap<>();
 
+		int lengthOfPrefixThatWeFollow = mWayPoints.size();
+
 		while (!worklist.isEmpty()) {
 			if (!mServices.getProgressAwareTimer().continueProcessing()) {
 				final String taskDescription = "searching accepting run (input had " + mOperand.size() + " states)";
@@ -202,7 +228,7 @@ private NestedRun<LETTER, STATE> getAcceptingRun(final Collection<STATE> startSt
 			if (mLogger.isDebugEnabled()) {
 				mLogger.debug(String.format("Current: %s", current));
 			}
-			if (mIsGoalState.test(current.mTargetState)) {
+			if (mIsGoalState.test(current.mTargetState) && !stillFollowingWayPoint) {
 				if (mLogger.isDebugEnabled()) {
 					mLogger.debug("  Is target");
 					printDebugStats(lowestCall, lowestOther, summaries);
@@ -218,7 +244,7 @@ private NestedRun<LETTER, STATE> getAcceptingRun(final Collection<STATE> startSt
 			}
 
 			final List<Item> unvaluatedSuccessors =
-					getUnvaluatedSuccessors(current, discoveredUniqueReturnStates, delayedCalls);
+					getUnvaluatedSuccessors(current, discoveredUniqueReturnStates, delayedCalls, visited);
 			if (mLogger.isDebugEnabled() && unvaluatedSuccessors.isEmpty()) {
 				mLogger.debug("  No successors");
 				continue;
@@ -234,6 +260,12 @@ private NestedRun<LETTER, STATE> getAcceptingRun(final Collection<STATE> startSt
 			}
 
 			for (final Item succ : successors) {
+				if (lengthOfPrefixThatWeFollow >= 0) {
+					// consider all successors, even the once seen before by prefix check
+					worklist.add(succ);
+					lengthOfPrefixThatWeFollow -= 1;
+					continue;
+				}
 				if (mLogger.isDebugEnabled()) {
 					mLogger.debug(String.format("  Succ: %s", succ));
 				}
@@ -334,6 +366,7 @@ private List<Item> addCostAndSummaries(final List<Item> succs,
 					for (final Entry<ReturnTransition, SummaryItem> entry : summary.entrySet()) {
 						final SummaryItem sumItem = entry.getValue();
 						final Item newSucc = new Item(succ, sumItem);
+
 						newSucc.setCostSoFar(succ.mCostSoFar + sumItem.mSummaryCost);
 						newSuccs.add(newSucc);
 
@@ -446,28 +479,38 @@ private boolean isCheapestAncestor(final Map<Item, Double> lowest,
 	}
 
 	private List<Item> getUnvaluatedSuccessors(final Item current,
-			final Map<STATE, Set<STATE>> discoveredUniqueReturnStates, final Map<STATE, Set<Item>> delayedCalls) {
+			final Map<STATE, Set<STATE>> discoveredUniqueReturnStates, final Map<STATE, Set<Item>> delayedCalls,
+			final List<Pair<STATE, LETTER>> visited) {
 		final List<Item> rtr = new ArrayList<>();
 
 		// process internal transitions
 		for (final OutgoingInternalTransition<LETTER, STATE> transition : mOperand
 				.internalSuccessors(current.mTargetState)) {
 			final LETTER symbol = transition.getLetter();
 			final STATE succ = transition.getSucc();
-			if (mIsForbiddenState.test(succ)) {
+
+			if (mIsForbiddenState.test(succ) || visited.contains(new Pair<>(current.mTargetState, symbol))
+					|| !followingWayPoint(succ, symbol)) {
 				continue;
 			}
 			rtr.add(new Item(succ, current.getHierPreState(), symbol, current, ItemType.INTERNAL));
+			if (stillFollowingWayPoint) {
+				break;
+			}
 		}
 
 		// process call transitions
 		for (final OutgoingCallTransition<LETTER, STATE> transition : mOperand.callSuccessors(current.mTargetState)) {
 			final LETTER symbol = transition.getLetter();
 			final STATE succ = transition.getSucc();
-			if (mIsForbiddenState.test(succ)) {
+			if (mIsForbiddenState.test(succ) || visited.contains(new Pair<>(current.mTargetState, symbol))
+					|| !followingWayPoint(succ, symbol)) {
 				continue;
 			}
 			rtr.add(new Item(succ, current.mTargetState, symbol, current, ItemType.CALL));
+			if (stillFollowingWayPoint) {
+				break;
+			}
 		}
 
 		final STATE hierPre = current.getHierPreState();
@@ -482,11 +525,15 @@ private List<Item> getUnvaluatedSuccessors(final Item current,
 				.returnSuccessorsGivenHier(current.mTargetState, hierPre)) {
 			final LETTER symbol = transition.getLetter();
 			final STATE succ = transition.getSucc();
-			if (mIsForbiddenState.test(succ)) {
+			if (mIsForbiddenState.test(succ) || visited.contains(new Pair<>(current.mTargetState, symbol))
+					|| !followingWayPoint(succ, symbol)) {
 				continue;
 			}
 			// hierarchical predecessor will be taken from current
 			rtr.add(new Item(succ, null, symbol, current, ItemType.RETURN));
+			if (stillFollowingWayPoint) {
+				break;
+			}
 		}
 		if (old != rtr.size()) {
 			// we found a new state from which a hierPre call can take at least one return
@@ -520,6 +567,21 @@ private boolean checkCost(final double expectedCost, final NestedRun<LETTER, STA
 		return true;
 	}
 
+	protected boolean followingWayPoint(final STATE state, final LETTER letter) {
+		final boolean empty = mWayPoints.isEmpty();
+		if (empty) {
+			stillFollowingWayPoint = false;
+			return true;
+		}
+		boolean contains = mWayPoints.getFirst().getFirst().equals(state);
+		contains = contains && mWayPoints.getFirst().getSecond().equals(letter);
+		if (contains) {
+			mWayPoints.removeFirst();
+
+		}
+		return contains || mWayPoints.isEmpty();
+	}
+
 	@Override
 	protected INwaOutgoingLetterAndTransitionProvider<LETTER, STATE> getOperand() {
 		return mOperand;