diff --git a/trunk/source/Library-Automata/META-INF/MANIFEST.MF b/trunk/source/Library-Automata/META-INF/MANIFEST.MF index 96a7893b878..569350d856a 100644 --- a/trunk/source/Library-Automata/META-INF/MANIFEST.MF +++ b/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 diff --git a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/IsEmpty.java b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/IsEmpty.java index 48fa794dc50..1950267d49d 100644 --- a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/IsEmpty.java +++ b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/IsEmpty.java @@ -71,7 +71,7 @@ * @param * state type */ -public final class IsEmpty extends UnaryNwaOperation> { +public class IsEmpty extends UnaryNwaOperation> { /** * Search strategy. * @@ -85,51 +85,55 @@ public enum SearchStrategy { /** * Depth-first search. */ - DFS + DFS, + /** + * use IsEmptyParallel with BFS + */ + PARALLEL } /** * Operand. */ - private final INwaOutgoingLetterAndTransitionProvider mOperand; + protected final INwaOutgoingLetterAndTransitionProvider mOperand; /** * Set of states in which the run we are searching has to begin. */ - private final Collection mStartStates; + protected final Collection mStartStates; /** * Set of states in which the run we are searching has to end. */ - private final Collection mGoalStates; + protected final Collection mGoalStates; /** * If set, the goal states are exactly the accepting states of the automaton, the set mGoalStates is null, and we * use the automaton to check if a state is a goal state. */ - private final boolean mGoalStateIsAcceptingState; + protected final boolean mGoalStateIsAcceptingState; /** * Set of states in which the run we are searching must not visit. */ - private final Collection mForbiddenStates; + protected final Collection mForbiddenStates; - private final NestedRun mAcceptingRun; + protected NestedRun mAcceptingRun; /** * Pairs of states visited, but possibly not processed, so far. */ - private final Map> mVisitedPairs = new HashMap<>(); + protected final Map> mVisitedPairs = new HashMap<>(); /** * Queue of states that have to be processed and have been visited while processing a internal transition, a return * transition or a computed summary. */ - private final Deque> mQueue = new ArrayDeque<>(); + protected final Deque> mQueue = new ArrayDeque<>(); /** * Queue of states that have to be processed and have been visited while processing a call transition. */ - private final Deque> mQueueCall = new ArrayDeque<>(); + protected final Deque> mQueueCall = new ArrayDeque<>(); /** * Assigns to a pair of states (state,stateK) the run of length 2 that is labeled to the incoming edge of @@ -137,14 +141,14 @@ public enum SearchStrategy { * (state,stateK) in the reachability graph is (pred,predK), where pred is the first state of the run and predK is * stateK. */ - private final Map>> mInternalSubRun = new HashMap<>(); + protected final Map>> mInternalSubRun = new HashMap<>(); /** * Assigns to a triple of states (state,stateK,predK) the run of length 2 that is labeled to the incoming edge of * the state pair (state,stateK) in the reachability graph. The symbol of the run has to be a call symbol. The * predecessor of (state,stateK) in the reachability graph is (pred,predK), where pred is stateK. */ - private final Map>>> mCallSubRun = new HashMap<>(); + protected final Map>>> mCallSubRun = new HashMap<>(); /** * Assigns to a pair of states (state,stateK) a state predK. predK is the second component of the state pair @@ -158,46 +162,46 @@ public enum SearchStrategy { * (state,stateK) in the reachability graph is (pred,predK), where pred is the first state of the run. predK can be * obtained from mreturnPredStateK */ - private final Map>> mReturnSubRun = new HashMap<>(); + protected final Map>> mReturnSubRun = new HashMap<>(); /** * Assigns to a pair of states (state,stateK) a state predK. predK is the second component of the predecessor * (pred,predK) of (state,stateK) in the reachability graph. */ - private final Map> mReturnPredStateK = new HashMap<>(); + protected final Map> mReturnPredStateK = new HashMap<>(); /** * If a triple (state,succ,returnPred) is contained in this map, a summary from state to succ has been discovered * and returnPred is the predecessor of the return transition of this summary. */ - private final Map> mSummaryReturnPred = new HashMap<>(); + protected final Map> mSummaryReturnPred = new HashMap<>(); /** * If a triple (state,succ,symbol) is contained in this map, a summary from state to succ has been discovered and * symbol is the label of the return transition of this summary. */ - private final Map> mSummaryReturnSymbol = new HashMap<>(); + protected final Map> mSummaryReturnSymbol = new HashMap<>(); /** * Second Element of the initial state pair. This state indicates that nothing is on the stack of the automaton, in * other words while processing we have taken the same number of calls and returns. */ - private final STATE mDummyEmptyStackState; + protected final STATE mDummyEmptyStackState; /** * Stack for the constructing a run if non-emptiness was detected. Contains an element for every return that was * processed and to corresponding call was processed yet. Corresponds to the * stack-of-returned-elements-that-have-not-been-called of the automaton but all elements are shifted by one. */ - private final ArrayDeque mReconstructionStack = new ArrayDeque<>(); + protected final ArrayDeque mReconstructionStack = new ArrayDeque<>(); /** * Search strategy. */ - private final SearchStrategy mStrategy; + protected final SearchStrategy mStrategy; - private NestedRun mReconstructionOneStepRun; - private STATE mReconstructionPredK; + protected NestedRun mReconstructionOneStepRun; + protected STATE mReconstructionPredK; /** * Default constructor. Here we search a run from the initial states of the automaton to the final states of the @@ -256,7 +260,7 @@ public IsEmpty(final AutomataLibraryServices services, final INestedWordAutomato assert operand.getStates().containsAll(goalStates) : "unknown states"; } - private IsEmpty(final AutomataLibraryServices services, + protected IsEmpty(final AutomataLibraryServices services, final INwaOutgoingLetterAndTransitionProvider operand, final Set startStates, final Set forbiddenStates, final Set goalStates, final boolean goalStateIsAcceptingState, final SearchStrategy strategy) throws AutomataOperationCanceledException { @@ -285,12 +289,45 @@ private IsEmpty(final AutomataLibraryServices services, } } + protected IsEmpty(final AutomataLibraryServices services, + final INwaOutgoingLetterAndTransitionProvider operand, final Set startStates, + final Set forbiddenStates, final Set goalStates, final boolean goalStateIsAcceptingState, + final SearchStrategy strategy, final boolean initializeOnly) throws AutomataOperationCanceledException { + super(services); + mOperand = operand; + mDummyEmptyStackState = mOperand.getEmptyStackState(); + mStartStates = startStates; + mGoalStateIsAcceptingState = goalStateIsAcceptingState; + mGoalStates = goalStates; + if (mGoalStateIsAcceptingState) { + assert mGoalStates == null : "if we search accepting states, mGoalStates is null"; + } else { + assert mGoalStates != null : "mGoalStates must not be null"; + } + mForbiddenStates = forbiddenStates; + mStrategy = strategy; + + if (mLogger.isInfoEnabled()) { + mLogger.info(startMessage()); + } + + if (initializeOnly) { + mAcceptingRun = null; + } else { + mAcceptingRun = getAcceptingRun(); + } + + if (mLogger.isInfoEnabled()) { + mLogger.info(exitMessage()); + } + } + /** * If we use the accepting states of mnwa as goal states (in this case mGoalStateIsAcceptingState is set and * mGoalStates is null) then we return true iff state is an accepting state. Otherwise we return true iff * mGoalStates.contains(state). */ - private boolean isGoalState(final STATE state) { + protected boolean isGoalState(final STATE state) { if (mGoalStateIsAcceptingState) { return mOperand.isFinal(state); } @@ -301,7 +338,7 @@ private boolean isGoalState(final STATE state) { * Enqueue a state pair that has been discovered by taking an internal transition, a return transition or a summary. * Mark the state pair as visited afterwards. */ - private void enqueueAndMarkVisited(final STATE state, final STATE stateK) { + protected void enqueueAndMarkVisited(final STATE state, final STATE stateK) { final DoubleDecker pair = new DoubleDecker<>(stateK, state); mQueue.addLast(pair); markVisited(state, stateK); @@ -336,7 +373,7 @@ private void enqueueAndMarkVisitedCall(final STATE state, final STATE callPred) * Dequeue a state pair. If available take a state pair that has been discovered by taking a call transition. If not * take a state pair that has been discovered by taking an internal transition, a return transition or a summary. */ - private DoubleDecker dequeue() { + protected DoubleDecker dequeue() { return switch (mStrategy) { // If available, take a state pair that has been discovered by taking a call transition. If not, take a // state pair that has been discovered by taking an internal or a return transition or a summary. @@ -345,6 +382,7 @@ private DoubleDecker dequeue() { // If available, take a state pair that has been discovered by taking an internal or a return transition or a // summary. If not, take a state pair that has been discovered by taking a call transition. case DFS -> dequeueGivenQueues(mQueue, mQueueCall); + default -> throw new IllegalArgumentException("Unexpected value: " + mStrategy); }; } @@ -362,7 +400,7 @@ private DoubleDecker dequeueGivenQueues(final Deque> /** * @return true iff the queue (is internally represented by two queues) is empty. */ - private boolean isQueueEmpty() { + protected boolean isQueueEmpty() { return mQueue.isEmpty() && mQueueCall.isEmpty(); } @@ -381,7 +419,7 @@ private void markVisited(final STATE state, final STATE stateK) { /** * @return true iff the state pair (state,stateK) was already visited. */ - private boolean wasVisited(final STATE state, final STATE stateK) { + protected boolean wasVisited(final STATE state, final STATE stateK) { final Set callPreds = mVisitedPairs.get(state); if (callPreds == null) { return false; @@ -394,7 +432,7 @@ private boolean wasVisited(final STATE state, final STATE stateK) { * nested word. */ @SuppressWarnings("squid:S1698") - private NestedRun getAcceptingRun() throws AutomataOperationCanceledException { + protected NestedRun getAcceptingRun() throws AutomataOperationCanceledException { for (final STATE state : mStartStates) { enqueueAndMarkVisited(state, mDummyEmptyStackState); } @@ -430,7 +468,7 @@ private NestedRun getAcceptingRun() throws AutomataOperationCance return null; } - private void getAcceptingRunHelperInternal(final STATE state, final STATE stateK) { + protected void getAcceptingRunHelperInternal(final STATE state, final STATE stateK) { for (final OutgoingInternalTransition transition : mOperand.internalSuccessors(state)) { final LETTER symbol = transition.getLetter(); final STATE succ = transition.getSucc(); @@ -441,7 +479,7 @@ private void getAcceptingRunHelperInternal(final STATE state, final STATE stateK } } - private void getAcceptingRunHelperCall(final STATE state, final STATE stateK) { + protected void getAcceptingRunHelperCall(final STATE state, final STATE stateK) { for (final OutgoingCallTransition transition : mOperand.callSuccessors(state)) { final LETTER symbol = transition.getLetter(); final STATE succ = transition.getSucc(); @@ -455,7 +493,7 @@ private void getAcceptingRunHelperCall(final STATE state, final STATE stateK) { } } - private void getAcceptingRunHelperReturn(final STATE state, final STATE stateK) { + protected void getAcceptingRunHelperReturn(final STATE state, final STATE stateK) { for (final OutgoingReturnTransition transition : mOperand.returnSuccessorsGivenHier(state, stateK)) { final LETTER symbol = transition.getLetter(); @@ -478,7 +516,7 @@ private void getAcceptingRunHelperReturn(final STATE state, final STATE stateK) * in the reachability graph. succK is stateK. For adding run information for (succ,succK) information about the * summary is fetched. */ - private void processSummaries(final STATE state, final STATE stateK) { + protected void processSummaries(final STATE state, final STATE stateK) { if (mSummaryReturnPred.containsKey(state)) { assert mSummaryReturnSymbol.containsKey(state); final Map succ2ReturnPred = mSummaryReturnPred.get(state); @@ -556,7 +594,7 @@ private void addRunInformationCall(final STATE succ, final STATE succK, final LE * Store for a state pair (succ,succK) in the reachability graph information about the predecessor (state,stateK) * under a return transition and a run of length two from state to succ. Store also succK to mreturnPredStateK. */ - private void addRunInformationReturn(final STATE succ, final STATE succK, final LETTER symbol, final STATE state, + protected void addRunInformationReturn(final STATE succ, final STATE succK, final LETTER symbol, final STATE state, final STATE stateK) { Map> succK2SubRun = mReturnSubRun.get(succ); Map succK2PredStateK = mReturnPredStateK.get(succ); @@ -578,7 +616,7 @@ private void addRunInformationReturn(final STATE succ, final STATE succK, final * Get all states which occur as the second component of a state pair (callState,*) in the reachability graph, where * the first component is callState. */ - private Set getCallStatesOfCallState(final STATE callState) { + protected Set getCallStatesOfCallState(final STATE callState) { final Set callStatesOfCallStates = mVisitedPairs.get(callState); if (callStatesOfCallStates == null) { return Collections.emptySet(); @@ -597,7 +635,7 @@ private Set getCallStatesOfCallState(final STATE callState) { /** * Store information about a discovered summary. */ - private void addSummary(final STATE stateBeforeCall, final STATE stateAfterReturn, final STATE stateBeforeReturn, + protected void addSummary(final STATE stateBeforeCall, final STATE stateAfterReturn, final STATE stateBeforeReturn, final LETTER returnSymbol) { Map succ2ReturnPred = mSummaryReturnPred.get(stateBeforeCall); Map succ2ReturnSymbol = mSummaryReturnSymbol.get(stateBeforeCall); @@ -645,7 +683,7 @@ private NestedRun constructRun(final STATE stateIn, final STATE s * Return true iff the run that lead to the accepting state contains an internal transition which is succeeded by * state and where stateK is the topmost stack element. */ - private boolean computeInternalSubRun(final STATE state, final STATE stateK) { + protected boolean computeInternalSubRun(final STATE state, final STATE stateK) { final Map> k2InternalMap = mInternalSubRun.get(state); if (k2InternalMap != null) { final NestedRun run = k2InternalMap.get(stateK); @@ -662,7 +700,7 @@ private boolean computeInternalSubRun(final STATE state, final STATE stateK) { * Return true iff the run that lead to the accepting state contains a call transition which is succeeded by state * and where stateK is the topmost stack element. */ - private boolean computeCallSubRun(final STATE state, final STATE stateK) { + protected boolean computeCallSubRun(final STATE state, final STATE stateK) { final Map>> k2CallMap = mCallSubRun.get(state); if (k2CallMap != null) { final Map> callMap = k2CallMap.get(stateK); @@ -690,7 +728,7 @@ private boolean computeCallSubRun(final STATE state, final STATE stateK) { * Return true iff the run that lead to the accepting state contains a return transition which is succeeded by state * and where stateK is the topmost stack element. */ - private boolean computeReturnSubRun(final STATE state, final STATE stateK) { + protected boolean computeReturnSubRun(final STATE state, final STATE stateK) { final Map> succK2SubRun = mReturnSubRun.get(state); if (succK2SubRun != null) { final Map succK2PredStateK = mReturnPredStateK.get(state); @@ -747,4 +785,4 @@ public String exitMessage() { } return "Finished " + getOperationName() + ". Found accepting run of length " + mAcceptingRun.getLength(); } -} +} \ No newline at end of file diff --git a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/IsEmptyHeuristic.java b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/IsEmptyHeuristic.java index e26b682ceca..712b6f12780 100644 --- a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/IsEmptyHeuristic.java +++ b/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 extends UnaryNwaOperation mIsForbiddenState; private final NestedRun mAcceptingRun; private final STATE mDummyEmptyStackState; - + protected final List> mWayPoints; + private boolean stillFollowingWayPoint = true; private final IHeuristic mHeuristic; /** @@ -116,7 +118,25 @@ public IsEmptyHeuristic(final AutomataLibraryServices services, final INwaOutgoingLetterAndTransitionProvider operand, final IHeuristic 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 operand, + final IHeuristic heuristic, final ArrayList> 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 startStates, final Predicate funIsForbiddenState, final Predicate funIsGoalState, final IHeuristic heuristic) throws AutomataOperationCanceledException { - this(services, (INwaOutgoingLetterAndTransitionProvider) 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 operand, final Set startStates, final Predicate funIsForbiddenState, final Predicate funIsGoalState, - final IHeuristic heuristic) throws AutomataOperationCanceledException { + final IHeuristic heuristic, final ArrayList> 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 getAcceptingRun(final Collection startSt final HashedPriorityQueue worklist = new HashedPriorityQueue<>(Comparator.comparing(a -> a.mEstimatedCostToTarget)); + final List> 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 getAcceptingRun(final Collection startSt final Map> summaries = new HashMap<>(); final Map>> 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 getAcceptingRun(final Collection 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 getAcceptingRun(final Collection startSt } final List 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 getAcceptingRun(final Collection 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 addCostAndSummaries(final List succs, for (final Entry 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,7 +479,8 @@ private boolean isCheapestAncestor(final Map lowest, } private List getUnvaluatedSuccessors(final Item current, - final Map> discoveredUniqueReturnStates, final Map> delayedCalls) { + final Map> discoveredUniqueReturnStates, final Map> delayedCalls, + final List> visited) { final List rtr = new ArrayList<>(); // process internal transitions @@ -454,20 +488,29 @@ private List getUnvaluatedSuccessors(final Item current, .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 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 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 getOperand() { return mOperand; diff --git a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/IsEmptyParallel.java b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/IsEmptyParallel.java new file mode 100644 index 00000000000..25567e6b2e7 --- /dev/null +++ b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/IsEmptyParallel.java @@ -0,0 +1,711 @@ +/* + * Copyright (C) 2011-2015 Matthias Heizmann (heizmann@informatik.uni-freiburg.de) + * Copyright (C) 2016 Christian Schilling (schillic@informatik.uni-freiburg.de) + * Copyright (C) 2009-2016 University of Freiburg + * Copyright (C) 2025 Max Barth (Max.Barth@lmu.de) + * Copyright (C) 2025 LMU Munich + * + * This file is part of the ULTIMATE Automata Library. + * + * The ULTIMATE Automata Library is free software: you can redistribute it and/or modify + * it under the terms of the GNU Lesser General Public License as published + * by the Free Software Foundation, either version 3 of the License, or + * (at your option) any later version. + * + * The ULTIMATE Automata Library is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU Lesser General Public License for more details. + * + * You should have received a copy of the GNU Lesser General Public License + * along with the ULTIMATE Automata Library. If not, see . + * + * Additional permission under GNU GPL version 3 section 7: + * If you modify the ULTIMATE Automata Library, or any covered work, by linking + * or combining it with Eclipse RCP (or a modified version of Eclipse RCP), + * containing parts covered by the terms of the Eclipse Public License, the + * licensors of the ULTIMATE Automata Library grant you additional permission + * to convey the resulting work. + */ +package de.uni_freiburg.informatik.ultimate.automata.nestedword.operations; + +import java.util.ArrayList; +import java.util.Collection; +import java.util.Collections; +import java.util.Comparator; +import java.util.HashMap; +import java.util.HashSet; +import java.util.Iterator; +import java.util.List; +import java.util.Map; +import java.util.Map.Entry; +import java.util.PriorityQueue; +import java.util.Set; +import java.util.function.Predicate; + +import de.uni_freiburg.informatik.ultimate.automata.AutomataLibraryServices; +import de.uni_freiburg.informatik.ultimate.automata.AutomataOperationCanceledException; +import de.uni_freiburg.informatik.ultimate.automata.nestedword.DoubleDecker; +import de.uni_freiburg.informatik.ultimate.automata.nestedword.INwaOutgoingLetterAndTransitionProvider; +import de.uni_freiburg.informatik.ultimate.automata.nestedword.NestedRun; +import de.uni_freiburg.informatik.ultimate.automata.nestedword.operations.IsEmptyHeuristic.AStarHeuristic; +import de.uni_freiburg.informatik.ultimate.automata.nestedword.operations.IsEmptyHeuristic.IHeuristic; +import de.uni_freiburg.informatik.ultimate.automata.nestedword.transitions.OutgoingCallTransition; +import de.uni_freiburg.informatik.ultimate.automata.nestedword.transitions.OutgoingInternalTransition; +import de.uni_freiburg.informatik.ultimate.automata.nestedword.transitions.OutgoingReturnTransition; +import de.uni_freiburg.informatik.ultimate.core.lib.exceptions.RunningTaskInfo; +import de.uni_freiburg.informatik.ultimate.core.lib.models.annotation.LoopEntryAnnotation; +import de.uni_freiburg.informatik.ultimate.core.lib.models.annotation.LoopExitAnnotation; +import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.structure.IcfgLocation; +import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.smt.predicates.ISLPredicate; +import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.smt.predicates.UnknownState; +import de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder.cfg.CodeBlock; +import de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder.cfg.Return; +import de.uni_freiburg.informatik.ultimate.util.datastructures.relation.Pair; + +/** + * Get an accepting run of a nested word automaton. Based on IsEmpty but adapted for Parallel CEGAR Loop. + * + * The idea is to have a preprocessing that finds a path (prefix) to an arbitrary state not taken by any other + * counterexample. Then we call BFS in this arbitrary state to find a path (suffix) to a goal state. At the end both + * paths are merged. + * + * This class uses recursion. It recursively explores the successor of a state. TODO: non recursive + * + * Non-terminating if every existing counterexample is in the @mActiveCounterexamples set but the state space is + * infinite. + * + * @author Max Barth (Max.Barth@lmu.de) + * + * @param + * letter type + * @param + * state type + */ +public final class IsEmptyParallel extends IsEmpty { + + private final Map> mVisitedCallPairs = new HashMap<>(); + private long mStart = 0; + private long mTimeSpendSearching = 0; + private final long mTimeOut; + private int mCountRecursionSteps = 0; // To prevent stack overflows + private int countFailedRunConstruction = 0; + private boolean mTimedout = false; + private int mLoopBound = -1; + // a -> b then state is a + private final List> mCurrentPrefix = new ArrayList<>(); + + /** + * HashMap used for parallel trace abstraction Maps TraceHash to Trace, has an entry for every counterexample + * currently checked by a thread + */ + private final HashMap> mActiveCounterexamples; + + /** + * Constructor for parallel search strategy. Gets as additional argument the list of all counterexamples currently + * investigated. Tries to find a new counterexample as much different as possible from the once considered. + * + * @param services + * Ultimate services + * @param operand + * input NWA + * @param strategy + * search strategy + * @see #IsEmptyParallel(AutomataLibraryServices, INwaOutgoingLetterAndTransitionProvider) + */ + public IsEmptyParallel(final AutomataLibraryServices services, + final INwaOutgoingLetterAndTransitionProvider operand, final Set startStates, + final Set forbiddenStates, final Set goalStates, final boolean goalStateIsAcceptingState, + final SearchStrategy strategy, final HashMap> counterexamples, + final int loopBound) throws AutomataOperationCanceledException { + super(services, operand, startStates, forbiddenStates, goalStates, goalStateIsAcceptingState, strategy, true); + + // BFS or DFS for search when we call IsEmpty at the end of parallel search + assert mStrategy.equals(SearchStrategy.BFS); + mLoopBound = loopBound; + + // In case the search is non terminating + mStart = System.nanoTime() / 1000000000; + mTimeOut = mStart + 50000; // 5 sec timeout atm + + if (mLogger.isInfoEnabled()) { + mLogger.info(startMessage()); + } + mActiveCounterexamples = counterexamples; + + mAcceptingRun = getAcceptingRunParallel(mActiveCounterexamples.keySet()); + + if (mLogger.isInfoEnabled()) { + mLogger.info(exitMessage()); + } + } + + /** + * Mark a call state pair a visited. Only used for tracking the caller of a call not for the bfs search + */ + private void markCallVisited(final STATE state, final STATE stateK) { + Set callPreds = mVisitedCallPairs.get(state); + if (callPreds == null) { + callPreds = new HashSet<>(); + mVisitedCallPairs.put(state, callPreds); + } + assert !callPreds.contains(stateK); + callPreds.add(stateK); + } + + // unmark incase we backtrack or explore a return + private void unmarkCall(final STATE state, final STATE stateK) { + final Set callPreds = mVisitedCallPairs.get(state); + assert callPreds != null : "Call was not visited! " + state + " " + stateK; + callPreds.remove(stateK); + } + + @Override + protected void getAcceptingRunHelperReturn(final STATE state, final STATE stateK) { + for (final OutgoingReturnTransition transition : mOperand.returnSuccessorsGivenHier(state, + stateK)) { + final LETTER symbol = transition.getLetter(); + final STATE succ = transition.getSucc(); + if (mForbiddenStates.contains(succ)) { + continue; + } + for (final STATE stateKk : getCallStatesOfCallState(stateK)) { + if (!wasVisited(succ, stateKk)) { + unmarkCall(stateK, stateKk); + enqueueAndMarkVisited(succ, stateKk); + addRunInformationReturn(succ, stateKk, symbol, state, stateK); + } + } + } + } + + @Override + protected Set getCallStatesOfCallState(final STATE callState) { + Set callStatesOfCallStates = mVisitedPairs.get(callState); + if (callStatesOfCallStates == null) { + callStatesOfCallStates = mVisitedCallPairs.get(callState); + if (callStatesOfCallStates == null) { + return Collections.emptySet(); + } + } + return callStatesOfCallStates; + } + + private PQState getSuccFromSummary(final Entry entry, final int position, final STATE state, + final ArrayList counterexamples) { + final Map succ2ReturnSymbol = mSummaryReturnSymbol.get(state); + final ArrayList activeCounterexamples = new ArrayList<>(); + final STATE succ = entry.getKey(); + if (!succ2ReturnSymbol.containsKey(succ)) { + throw new AssertionError("Getting Summary failed!"); + } + final STATE returnPred = entry.getValue(); + final LETTER symbol = succ2ReturnSymbol.get(succ); + int currentScore = 0; + for (final int cexHash : counterexamples) { + final NestedRun counterexample = mActiveCounterexamples.get(cexHash); + if (counterexample.getLength() > position) { + IcfgLocation programPoint = null; + final STATE stateInCEx = (STATE) counterexample.getStateAtPosition(position); + if (stateInCEx instanceof Return || succ instanceof Return) { + if (symbol == counterexample.getSymbol(position - 1)) { + currentScore += 1; + activeCounterexamples.add(cexHash); + } + } else if (stateInCEx instanceof ISLPredicate && succ instanceof ISLPredicate) { + programPoint = ((ISLPredicate) stateInCEx).getProgramPoint(); + if (programPoint.equals(((ISLPredicate) succ).getProgramPoint())) { + if (symbol == counterexample.getSymbol(position - 1)) { + currentScore += 1; + activeCounterexamples.add(cexHash); + } + } else { + if (!(succ instanceof UnknownState + || !counterexample.getStateAtPosition(position).equals(succ))) { + throw new AssertionError("unexpected state in counterexample"); + } + } + } else { + throw new AssertionError("unexpected state in counterexample"); + } + + } + } + return new PQState(currentScore, returnPred, symbol, succ, state, activeCounterexamples, false, true); + } + + private boolean increaseScore(final NestedRun counterexample, final STATE state, final STATE succ, + final LETTER symbol, final int position) { + final boolean stateBasedScore = false; + if (stateBasedScore) { + return increaseScoreBasedOnStates(counterexample, succ); + } + return increaseScoreDefault(counterexample, state, succ, symbol, position); + } + + /** + * increases the score only if a previous counterexample took this edge * AND @position is equal to the position of + * the @succ in the counterexample (Prefixes match) + * + * @param succ + */ + private boolean increaseScoreDefault(final NestedRun counterexample, final STATE state, final STATE succ, + final LETTER symbol, final int position) { + if (counterexample.getLength() > position) { + IcfgLocation programPoint = null; + final STATE stateInCEx = (STATE) counterexample.getStateAtPosition(position); + if (stateInCEx instanceof ISLPredicate) { + programPoint = ((ISLPredicate) stateInCEx).getProgramPoint(); + } else { + throw new AssertionError("Unexpected Predicate"); + } + // can have different serial numbers! is that a problem? + if (programPoint.equals(((ISLPredicate) succ).getProgramPoint()) + && (symbol == counterexample.getSymbol(position - 1))) { + return true; + } + } + return false; + } + + /* + * We are less strict here and increase already if the succ occurs in the counterexample no matter the position + * Doesnt seem to pay of in our evaluation. + */ + private boolean increaseScoreBasedOnStates(final NestedRun counterexample, final STATE succ) { + + final Set stateSet = new HashSet<>(counterexample.getStateSequence()); + if (stateSet.contains(succ)) { + return true; + } + return false; + } + + // Calculates the score of an internal successor and tracks how many counterexamples in the given set take this + // successor + private PQState getSuccOfInternal(final OutgoingInternalTransition transition, final int position, + final STATE state, final STATE stateK, final ArrayList counterexamples) { + final LETTER symbol = transition.getLetter(); + final STATE succ = transition.getSucc(); + final ArrayList activeCounterexamples = new ArrayList<>(); + int currentScore = 0; + for (final int cexHash : counterexamples) { + final NestedRun counterexample = mActiveCounterexamples.get(cexHash); + if (increaseScore(counterexample, state, succ, symbol, position)) { + currentScore += 1; + activeCounterexamples.add(cexHash); + } + } + return new PQState(currentScore, state, symbol, transition.getSucc(), stateK, activeCounterexamples, false, + false); + } + + private PQState getSuccOfCall(final OutgoingCallTransition transition, final int position, + final STATE state, final STATE stateK, final ArrayList counterexamples) { + final LETTER symbol = transition.getLetter(); + final STATE succ = transition.getSucc(); + final ArrayList activeCounterexamples = new ArrayList<>(); + int currentScore = 0; + for (final int cexHash : counterexamples) { + final NestedRun counterexample = mActiveCounterexamples.get(cexHash); + if (increaseScore(counterexample, state, succ, symbol, position)) { + currentScore += 1; + activeCounterexamples.add(cexHash); + } + } + return new PQState(currentScore, state, symbol, transition.getSucc(), stateK, activeCounterexamples, true, + false); + } + + private PQState getSuccOfReturn(final OutgoingReturnTransition transition, final int position, + final STATE state, final STATE stateKk, final ArrayList counterexamples) { + final LETTER symbol = transition.getLetter(); + final STATE succ = transition.getSucc(); + final ArrayList activeCounterexamples = new ArrayList<>(); + int currentScore = 0; + for (final int cexHash : counterexamples) { + final NestedRun counterexample = mActiveCounterexamples.get(cexHash); + if (increaseScore(counterexample, state, succ, symbol, position)) { + currentScore += 1; + activeCounterexamples.add(cexHash); + } + } + return new PQState(currentScore, state, symbol, transition.getSucc(), stateKk, activeCounterexamples, false, + true); + } + + // This can be used to restrict the search to omit exploring certain successors, e.g., loop entry locations + private boolean exploreThisSuccessor(final STATE state, final LETTER letter, final STATE succ) { + if (mForbiddenStates.contains(succ)) { + return false; + } + if (atLoopBound(state, letter)) { + return false; + } + return true; + } + + private boolean atLoopBound(final STATE state, final LETTER letter) { + if (mLoopBound == -1) { + return false; + } + if (isLoopEntryLocation(state) && entersLoopBody(letter)) { + int countLetters = 0; // amount of loop unrollings + int countStates = 0; // amount of new loop unrollings + for (final Pair transition : mCurrentPrefix) { + if (transition.getSecond().equals(letter)) { + countLetters += 1; + } + // letter can be the same but state different + // Then its an unknownstate and the loop was already unrolled + if (transition.getFirst().equals(state)) { + countStates += 1; + } + } + if (countLetters >= mLoopBound && countStates > 1) { // we see it once when exiting the loop + return true; + } + } + return false; + + } + + private boolean entersLoopBody(final LETTER letter) { + final CodeBlock stmt = ((CodeBlock) letter); + if (stmt.getPayload().getAnnotations().containsKey(LoopExitAnnotation.class.getName())) { + return false; + } + return true; + } + + private boolean isLoopEntryLocation(final STATE state) { + final IcfgLocation a = ((ISLPredicate) state).getProgramPoint(); + if (a.getPayload().getAnnotations().containsKey(LoopEntryAnnotation.class.getName())) { + return true; + } + return false; + } + + /** + * Sort the outgoing transitions by how many @param counterexamples cover them. The least has highest priority. + */ + private PriorityQueue pickSuccToExplore(final int position, final STATE state, final STATE stateK, + final ArrayList counterexamples) { + final PriorityQueue pq = new PriorityQueue<>(Comparator.comparingInt(PQState::getScore)); + + if (mSummaryReturnPred.containsKey(state)) { + if (!mSummaryReturnSymbol.containsKey(state)) { + throw new AssertionError("Summary Failed"); + } + final Map succ2ReturnPred = mSummaryReturnPred.get(state); + for (final Entry entry : succ2ReturnPred.entrySet()) { + pq.add(getSuccFromSummary(entry, position, state, counterexamples)); + } + // after we process a summary we must not process the return anymore!! + return pq; + } + + boolean firstIteration = true; + final Iterator> internalIterator = + mOperand.internalSuccessors(state).iterator(); + while (internalIterator.hasNext()) { + final OutgoingInternalTransition transition = internalIterator.next(); + final STATE succ = transition.getSucc(); + if (!exploreThisSuccessor(state, transition.getLetter(), succ)) { + continue; + } + if (firstIteration && !internalIterator.hasNext()) { + pq.add(new PQState(1, state, transition.getLetter(), transition.getSucc(), stateK, counterexamples, + false, false)); + } else { + pq.add(getSuccOfInternal(transition, position, state, stateK, counterexamples)); + } + firstIteration = false; + } + + final Iterator> callIterator = mOperand.callSuccessors(state).iterator(); + while (callIterator.hasNext()) { + final OutgoingCallTransition transition = callIterator.next(); + final STATE succ = transition.getSucc(); + if (!exploreThisSuccessor(state, transition.getLetter(), succ)) { + continue; + } + if (firstIteration && !callIterator.hasNext()) { + pq.add(new PQState(1, state, transition.getLetter(), transition.getSucc(), stateK, counterexamples, + true, false)); + } else { + pq.add(getSuccOfCall(transition, position, state, stateK, counterexamples)); + } + firstIteration = false; + } + + if (stateK == mOperand.getEmptyStackState()) { + // there is no return transition + return pq; + } + for (final STATE stateKk : getCallStatesOfCallState(stateK)) { + final Iterator> returnIterator = + mOperand.returnSuccessorsGivenHier(state, stateK).iterator(); + while (returnIterator.hasNext()) { + final OutgoingReturnTransition transition = returnIterator.next(); + final STATE succ = transition.getSucc(); + if (!exploreThisSuccessor(state, transition.getLetter(), succ)) { + continue; + } + if (firstIteration && !returnIterator.hasNext()) { + pq.add(new PQState(1, state, transition.getLetter(), transition.getSucc(), stateKk, counterexamples, + false, true)); + } else { + pq.add(getSuccOfReturn(transition, position, state, stateKk, counterexamples)); + } + firstIteration = false; + } + } + return pq; + } + + private PriorityQueue pickStartToExplore(final Collection states, final Set set) { + final PriorityQueue pq = new PriorityQueue<>(Comparator.comparingInt(PQState::getScore)); + + for (final STATE state : states) { + final ArrayList activeCounterexamples = new ArrayList<>(); + int currentScore = 0; + for (final int cexHash : set) { + IcfgLocation programPoint = null; + + final STATE stateInCEx = (STATE) mActiveCounterexamples.get(cexHash).getStateAtPosition(0); + if (stateInCEx instanceof ISLPredicate) { + programPoint = ((ISLPredicate) stateInCEx).getProgramPoint(); + } else { + throw new AssertionError("Unexpected Predicate"); + } + + if (programPoint.equals(((ISLPredicate) state).getProgramPoint())) { + currentScore += 1; + activeCounterexamples.add(cexHash); + } else { + if (mActiveCounterexamples.get(cexHash).getStateAtPosition(0).equals(state)) { + throw new AssertionError("Program Point mismatch"); + } + } + } + pq.add(new PQState(currentScore, null, null, state, null, activeCounterexamples, false, false)); + } + return pq; + } + + /* + * Only check if visited after we reached score 0 + */ + private NestedRun constructRunFromStateToNextBranch(final int position, + final DoubleDecker pair, final ArrayList counterexamples) + throws AutomataOperationCanceledException { + mCountRecursionSteps += 1; + if (System.nanoTime() / 1000000000 > mTimeOut || mTimedout) { + mTimedout = true; + mLogger.warn("IsEmpyParallel timeout"); + return null; + } + if (mCountRecursionSteps > 700) { + mTimedout = true; + mLogger.warn("IsEmpyParallel Recursion Limit"); + return null; + } + int positionOfThisSubSearch = position; + + if (!mServices.getProgressAwareTimer().continueProcessing()) { + final String taskDescription = "searching accepting run (input had " + mOperand.size() + " states)"; + final RunningTaskInfo rti = new RunningTaskInfo(getClass(), taskDescription); + throw new AutomataOperationCanceledException(rti); + } + + positionOfThisSubSearch += 1; + final STATE state = pair.getUp(); + final STATE stateK = pair.getDown(); + + mVisitedPairs.clear(); // reset visited Pairs, then add start of subsearch + if (counterexamples.isEmpty()) { + final IsEmptyHeuristic runsearch; + if (mGoalStates != null) { + final Predicate funIsForbiddenState = a -> false; + final Predicate goals = a -> mGoalStates.contains(a); + final Set startset = new HashSet<>(mStartStates); + runsearch = new IsEmptyHeuristic<>(mServices, mOperand, startset, funIsForbiddenState, goals, + IHeuristic.getHeuristic(AStarHeuristic.ZERO, null, 0), new ArrayList<>(mCurrentPrefix)); + } else { + runsearch = new IsEmptyHeuristic<>(mServices, mOperand, + IHeuristic.getHeuristic(AStarHeuristic.ZERO, null, 0), new ArrayList<>(mCurrentPrefix)); + } + final NestedRun run = runsearch.getNestedRun(); + if (run == null) { + return run; + } + for (final Integer cexHash : mActiveCounterexamples.keySet()) { + if (cexHash == run.getWord().asList().hashCode()) { + throw new AssertionError("Not a fresh counterexample!"); + } + } + return run; // is null if isEmpty fails, leads to backtracking + } + + // equality intended here + if (stateK != mOperand.getEmptyStackState()) { + // there is no return transition + // getAcceptingRunHelperReturn(state, stateK); + } + + // enqueues successors + if (!counterexamples.isEmpty()) { + + final PriorityQueue pqStart = + pickSuccToExplore(positionOfThisSubSearch, state, stateK, counterexamples); // statek is not + if (pqStart.isEmpty()) { + return null; + } + while (!pqStart.isEmpty()) { + final PQState startpq = pqStart.poll(); + if (startpq == null) { + throw new AssertionError("No Priority Queue"); + } + final STATE newState = startpq.getState(); // only needed for summaries + final STATE newStateK = startpq.getStateK(); + final STATE succ = startpq.getSucc(); + final LETTER symbol = startpq.getLetter(); + + NestedRun runToGoal; + addToCurrentPrefix(succ, symbol); + if (startpq.isCall()) { + markCallVisited(newState, newStateK); + runToGoal = constructRunFromStateToNextBranch(positionOfThisSubSearch, + new DoubleDecker<>(newState, succ), startpq.getCounterexamplesUnderConsideration()); + + unmarkCall(newState, newStateK); + + } else if (startpq.isReturn()) { + // stateK is the hierarchical pre of state + // newStateK is the stateKK + unmarkCall(stateK, newStateK); + addSummary(newStateK, succ, newState, symbol); + runToGoal = constructRunFromStateToNextBranch(positionOfThisSubSearch, + new DoubleDecker<>(newStateK, succ), startpq.getCounterexamplesUnderConsideration()); + markCallVisited(stateK, newStateK); + } else { + runToGoal = constructRunFromStateToNextBranch(positionOfThisSubSearch, + new DoubleDecker<>(newStateK, succ), startpq.getCounterexamplesUnderConsideration()); + } + removeFromCurrentPrefix(succ, symbol); + if (runToGoal != null) { + return runToGoal; + } + } + } + mCountRecursionSteps -= 1; + return null; + } + + private void addToCurrentPrefix(final STATE state, final LETTER letter) { + mCurrentPrefix.add(new Pair<>(state, letter)); + } + + private void removeFromCurrentPrefix(final STATE state, final LETTER letter) { + assert mCurrentPrefix.getLast().getFirst().equals(state) && mCurrentPrefix.getLast().getSecond().equals(letter); + mCurrentPrefix.removeLast(); + } + + @SuppressWarnings("squid:S1698") + private NestedRun getAcceptingRunParallel(final Set set) + throws AutomataOperationCanceledException { + final PriorityQueue pqStart = pickStartToExplore(mStartStates, set); + // if abstraction is empty, there might not be a start anymore + while (!pqStart.isEmpty()) { + final PQState startpq = pqStart.poll(); + final STATE start = startpq.getSucc(); + final NestedRun runToGoal = constructRunFromStateToNextBranch(0, + new DoubleDecker<>(mDummyEmptyStackState, start), startpq.getCounterexamplesUnderConsideration()); + + if (runToGoal != null) { + for (final Integer cexHash : set) { + if (cexHash == runToGoal.getWord().asList().hashCode()) { + throw new AssertionError("Not a fresh counterexample!"); + } + } + return runToGoal; + } + } + return null; + } + + @Override + public NestedRun getNestedRun() { + if (!getResult()) { + for (int i = 0; i < mAcceptingRun.getLength() - 1; i++) { + if (mAcceptingRun.getWord().isPendingReturn(i)) { + countFailedRunConstruction += 1; + return null; + } + } + } + return mAcceptingRun; + } + + public long getTimeSpend() { + mTimeSpendSearching = System.nanoTime() / 1000000000 - mStart; + return mTimeSpendSearching; + } + + private class PQState { + Integer mScore; + STATE mState; + STATE mSucc; + STATE mStateK; + ArrayList mCounterexamples = new ArrayList<>(); + LETTER mSymbol; + boolean mCallTransition; + boolean mReturnTransition; + + public PQState(final int score, final STATE state, final LETTER symbol, final STATE succ, final STATE stateK, + final ArrayList counterexamples, final boolean call, final boolean ret) { + mScore = score; + mState = state; + mSucc = succ; + mStateK = stateK; + mCounterexamples = counterexamples; + mSymbol = symbol; + mCallTransition = call; + mReturnTransition = ret; + assert !mCallTransition || !mReturnTransition; + } + + public Integer getScore() { + return mScore; + } + + public STATE getState() { + return mState; + } + + public STATE getStateK() { + return mStateK; + } + + public STATE getSucc() { + return mSucc; + } + + public boolean isCall() { + return mCallTransition; + } + + public boolean isReturn() { + return mReturnTransition; + } + + public LETTER getLetter() { + return mSymbol; + } + + public ArrayList getCounterexamplesUnderConsideration() { + return mCounterexamples; + } + } +} diff --git a/trunk/source/Library-ModelCheckerUtils/src/de/uni_freiburg/informatik/ultimate/lib/modelcheckerutils/boogie/Term2Expression.java b/trunk/source/Library-ModelCheckerUtils/src/de/uni_freiburg/informatik/ultimate/lib/modelcheckerutils/boogie/Term2Expression.java index b653bb34e71..8d15efed44d 100644 --- a/trunk/source/Library-ModelCheckerUtils/src/de/uni_freiburg/informatik/ultimate/lib/modelcheckerutils/boogie/Term2Expression.java +++ b/trunk/source/Library-ModelCheckerUtils/src/de/uni_freiburg/informatik/ultimate/lib/modelcheckerutils/boogie/Term2Expression.java @@ -731,4 +731,8 @@ public boolean equals(final Object obj) { } } + + public TypeSortTranslator getTypeSortTranslator() { + return mTypeSortTranslator; + } } diff --git a/trunk/source/Library-ModelCheckerUtils/src/de/uni_freiburg/informatik/ultimate/lib/modelcheckerutils/boogie/TypeSortTranslator.java b/trunk/source/Library-ModelCheckerUtils/src/de/uni_freiburg/informatik/ultimate/lib/modelcheckerutils/boogie/TypeSortTranslator.java index 05c8cb68c7b..513ba6f8269 100644 --- a/trunk/source/Library-ModelCheckerUtils/src/de/uni_freiburg/informatik/ultimate/lib/modelcheckerutils/boogie/TypeSortTranslator.java +++ b/trunk/source/Library-ModelCheckerUtils/src/de/uni_freiburg/informatik/ultimate/lib/modelcheckerutils/boogie/TypeSortTranslator.java @@ -42,6 +42,8 @@ import de.uni_freiburg.informatik.ultimate.boogie.type.BoogieType; import de.uni_freiburg.informatik.ultimate.core.model.models.IBoogieType; import de.uni_freiburg.informatik.ultimate.core.model.services.IUltimateServiceProvider; +import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.smt.scripttransfer.TermTransferrer; +import de.uni_freiburg.informatik.ultimate.lib.smtlibutils.ManagedScript; import de.uni_freiburg.informatik.ultimate.lib.smtlibutils.SmtSortUtils; import de.uni_freiburg.informatik.ultimate.logic.SMTLIBException; import de.uni_freiburg.informatik.ultimate.logic.Script; @@ -62,6 +64,7 @@ public class TypeSortTranslator { private final Map mSort2Type = new HashMap<>(); private final Map> mType2Attributes; private final IUltimateServiceProvider mServices; + private ManagedScript mCfgScriptFromWorker = null; public TypeSortTranslator(final Collection declarations, final Script script, final IUltimateServiceProvider services) { @@ -121,7 +124,11 @@ public TypeSortTranslator(final Script script, final IUltimateServiceProvider se } } - public IBoogieType getType(final Sort sort) { + public IBoogieType getType(Sort sort) { + if (mCfgScriptFromWorker != null) { + final TermTransferrer tf = new TermTransferrer(mCfgScriptFromWorker.getScript(), mScript); + sort = tf.transferSort(sort); + } IBoogieType type = mSort2Type.get(sort); if (type == null) { // TODO Matthias: The following special treatment of arrays is only @@ -273,4 +280,9 @@ private void cacheSort(final IBoogieType boogieType, final Sort result) { mSort2Type.put(result, boogieType); } + // called by @RCFGBacktranslator used to translate the sort form the worker cfg script to the main cfg script + public void setCfgScriptFromWorker(final ManagedScript cfgScriptFromWorker) { + mCfgScriptFromWorker = cfgScriptFromWorker; + } + } diff --git a/trunk/source/Library-ModelCheckerUtils/src/de/uni_freiburg/informatik/ultimate/lib/modelcheckerutils/cfg/IcfgProgramExecution.java b/trunk/source/Library-ModelCheckerUtils/src/de/uni_freiburg/informatik/ultimate/lib/modelcheckerutils/cfg/IcfgProgramExecution.java index af6406de14f..82bf355aa0a 100644 --- a/trunk/source/Library-ModelCheckerUtils/src/de/uni_freiburg/informatik/ultimate/lib/modelcheckerutils/cfg/IcfgProgramExecution.java +++ b/trunk/source/Library-ModelCheckerUtils/src/de/uni_freiburg/informatik/ultimate/lib/modelcheckerutils/cfg/IcfgProgramExecution.java @@ -53,6 +53,7 @@ import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.structure.IIcfgReturnTransition; import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.structure.IIcfgTransition; import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.structure.IcfgForkThreadOtherTransition; +import de.uni_freiburg.informatik.ultimate.lib.smtlibutils.ManagedScript; import de.uni_freiburg.informatik.ultimate.logic.Term; import de.uni_freiburg.informatik.ultimate.logic.TermVariable; @@ -69,6 +70,7 @@ public class IcfgProgramExecution implements IProgramExecutio private final Map[] mBranchEncoders; private final boolean mIsConcurrent; private final Class mTransitionClazz; + private ManagedScript mScript = null; // the cfg script used on creation public IcfgProgramExecution(final List> trace, final Map> partialProgramStateMapping, @@ -359,5 +361,12 @@ public IBacktranslationValueProvider getBacktranslationValueProvider() public boolean isConcurrent() { return mIsConcurrent; } + + public void setOriginCfgScript(ManagedScript managedScript) { + mScript = managedScript; + } + public ManagedScript getOriginCfgScript() { + return mScript; + } } diff --git a/trunk/source/Library-SmtLibUtils/src/de/uni_freiburg/informatik/ultimate/lib/smtlibutils/ManagedScript.java b/trunk/source/Library-SmtLibUtils/src/de/uni_freiburg/informatik/ultimate/lib/smtlibutils/ManagedScript.java index f4c2cf99980..f7140b3fc51 100644 --- a/trunk/source/Library-SmtLibUtils/src/de/uni_freiburg/informatik/ultimate/lib/smtlibutils/ManagedScript.java +++ b/trunk/source/Library-SmtLibUtils/src/de/uni_freiburg/informatik/ultimate/lib/smtlibutils/ManagedScript.java @@ -144,6 +144,10 @@ public LBool assertTerm(final Object lockOwner, final Term term) throws SMTLIBEx public LBool checkSat(final Object lockOwner) throws SMTLIBException { assert lockOwner == mLockOwner : generateLockErrorMessage(lockOwner, mLockOwner); + if (Thread.interrupted()) { + mScript.exit(); + throw new SMTLIBException("Thread Was Interrupted, crashing before checkSat"); + } return mScript.checkSat(); } @@ -327,9 +331,11 @@ public TermVariable constructFreshTermVariable(final String name, final Sort sor public TermVariable constructFreshCopy(final TermVariable tv) { String basename = mTv2Basename.get(tv); if (basename == null) { + // Variable Names are not synchronized in Parallel CEGAR loop, this warning will be triggered! mLogger.warn("TermVariable " + tv + " not constructed by VariableManager. Cannot ensure absence of name clashes."); basename = SmtUtils.removeSmtQuoteCharacters(tv.getName()); + mTv2Basename.put(tv, basename); } final TermVariable result = constructFreshTermVariable(basename, tv.getSort()); return result; diff --git a/trunk/source/Library-SmtLibUtils/src/de/uni_freiburg/informatik/ultimate/lib/smtlibutils/SmtSortUtils.java b/trunk/source/Library-SmtLibUtils/src/de/uni_freiburg/informatik/ultimate/lib/smtlibutils/SmtSortUtils.java index f4094777ba0..ddfcffc40b9 100644 --- a/trunk/source/Library-SmtLibUtils/src/de/uni_freiburg/informatik/ultimate/lib/smtlibutils/SmtSortUtils.java +++ b/trunk/source/Library-SmtLibUtils/src/de/uni_freiburg/informatik/ultimate/lib/smtlibutils/SmtSortUtils.java @@ -112,6 +112,10 @@ public static Sort getRealSort(final Script script) { return script.sort(REAL_SORT); } + public static Sort getFloatSort(final Script script, final BigInteger index1, final BigInteger index2) { + return script.sort(FLOATINGPOINT_SORT, new String[] { index1.toString(), index2.toString() }); + } + /** * @param size * number of bits diff --git a/trunk/source/Library-SmtLibUtils/src/de/uni_freiburg/informatik/ultimate/lib/smtlibutils/SmtUtils.java b/trunk/source/Library-SmtLibUtils/src/de/uni_freiburg/informatik/ultimate/lib/smtlibutils/SmtUtils.java index 1f3be6ce768..e6f156ffa66 100644 --- a/trunk/source/Library-SmtLibUtils/src/de/uni_freiburg/informatik/ultimate/lib/smtlibutils/SmtUtils.java +++ b/trunk/source/Library-SmtLibUtils/src/de/uni_freiburg/informatik/ultimate/lib/smtlibutils/SmtUtils.java @@ -1574,6 +1574,9 @@ public static Term unfTerm(final Script script, final String funcname, final Str case "bvsge": result = BitvectorUtils.unfTerm(script, funcname, toBigIntegerArray(indices), params); break; + case "fp": + result = script.term(funcname, null, null, params); + break; default: result = script.term(funcname, indices, resultSort, params); break; diff --git a/trunk/source/Library-TraceCheckerUtils/src/de/uni_freiburg/informatik/ultimate/lib/tracecheckerutils/singletracecheck/InterpolatingTraceCheckCraig.java b/trunk/source/Library-TraceCheckerUtils/src/de/uni_freiburg/informatik/ultimate/lib/tracecheckerutils/singletracecheck/InterpolatingTraceCheckCraig.java index c7126af2605..a5d189aeedc 100644 --- a/trunk/source/Library-TraceCheckerUtils/src/de/uni_freiburg/informatik/ultimate/lib/tracecheckerutils/singletracecheck/InterpolatingTraceCheckCraig.java +++ b/trunk/source/Library-TraceCheckerUtils/src/de/uni_freiburg/informatik/ultimate/lib/tracecheckerutils/singletracecheck/InterpolatingTraceCheckCraig.java @@ -119,6 +119,7 @@ public InterpolatingTraceCheckCraig(final IPredicate precondition, final IPredic mInterpolantComputationStatus = new InterpolantComputationStatus(ItpErrorStatus.SMT_SOLVER_CANNOT_INTERPOLATE_INPUT, null); } + mgdScriptTc.getScript().exit(); } public InterpolatingTraceCheckCraig(final IPredicate precondition, final IPredicate postcondition, diff --git a/trunk/source/Library-TraceCheckerUtils/src/de/uni_freiburg/informatik/ultimate/lib/tracecheckerutils/singletracecheck/RelevantVariables.java b/trunk/source/Library-TraceCheckerUtils/src/de/uni_freiburg/informatik/ultimate/lib/tracecheckerutils/singletracecheck/RelevantVariables.java index cc7f03d6e8d..c12228b4a57 100644 --- a/trunk/source/Library-TraceCheckerUtils/src/de/uni_freiburg/informatik/ultimate/lib/tracecheckerutils/singletracecheck/RelevantVariables.java +++ b/trunk/source/Library-TraceCheckerUtils/src/de/uni_freiburg/informatik/ultimate/lib/tracecheckerutils/singletracecheck/RelevantVariables.java @@ -728,7 +728,7 @@ private Set computePredecessorRvReturn(final Set retur private static boolean isHavoced(final UnmodifiableTransFormula globalVarAssignment, final UnmodifiableTransFormula oldVarAssignment, final IProgramVar bv) { - if (bv instanceof GlobalProgramVar) { + if (bv.isGlobal()) { boolean result; if (bv instanceof IProgramOldVar) { result = oldVarAssignment.isHavocedOut(bv); diff --git a/trunk/source/Library-TraceCheckerUtils/src/de/uni_freiburg/informatik/ultimate/lib/tracecheckerutils/singletracecheck/TraceCheckSpWp.java b/trunk/source/Library-TraceCheckerUtils/src/de/uni_freiburg/informatik/ultimate/lib/tracecheckerutils/singletracecheck/TraceCheckSpWp.java index 3d2cfa537e2..2551671f0a4 100644 --- a/trunk/source/Library-TraceCheckerUtils/src/de/uni_freiburg/informatik/ultimate/lib/tracecheckerutils/singletracecheck/TraceCheckSpWp.java +++ b/trunk/source/Library-TraceCheckerUtils/src/de/uni_freiburg/informatik/ultimate/lib/tracecheckerutils/singletracecheck/TraceCheckSpWp.java @@ -172,6 +172,7 @@ public TraceCheckSpWp(final IPredicate precondition, final IPredicate postcondit mInterpolantComputationStatus = new InterpolantComputationStatus(ItpErrorStatus.SMT_SOLVER_CANNOT_INTERPOLATE_INPUT, null); } + mTcSmtManager.getScript().exit(); } @Override diff --git a/trunk/source/Library-UltimateCore/src/de/uni_freiburg/informatik/ultimate/core/lib/models/BasePayloadContainer.java b/trunk/source/Library-UltimateCore/src/de/uni_freiburg/informatik/ultimate/core/lib/models/BasePayloadContainer.java index 22e0417b44b..59e7fbc75b7 100644 --- a/trunk/source/Library-UltimateCore/src/de/uni_freiburg/informatik/ultimate/core/lib/models/BasePayloadContainer.java +++ b/trunk/source/Library-UltimateCore/src/de/uni_freiburg/informatik/ultimate/core/lib/models/BasePayloadContainer.java @@ -47,7 +47,7 @@ public abstract class BasePayloadContainer implements IElement { */ private static final long serialVersionUID = 1L; - private IPayload mPayload; + protected IPayload mPayload; protected BasePayloadContainer() { this(null); diff --git a/trunk/source/RCFGBuilder/src/de/uni_freiburg/informatik/ultimate/plugins/generator/rcfgbuilder/RCFGBacktranslator.java b/trunk/source/RCFGBuilder/src/de/uni_freiburg/informatik/ultimate/plugins/generator/rcfgbuilder/RCFGBacktranslator.java index 9580fa9909c..fe15319229d 100644 --- a/trunk/source/RCFGBuilder/src/de/uni_freiburg/informatik/ultimate/plugins/generator/rcfgbuilder/RCFGBacktranslator.java +++ b/trunk/source/RCFGBuilder/src/de/uni_freiburg/informatik/ultimate/plugins/generator/rcfgbuilder/RCFGBacktranslator.java @@ -242,11 +242,14 @@ private void addCodeBlock(final IIcfgTransition cb, final IRelevan @Override public IProgramExecution - translateProgramExecution(final IProgramExecution, Term> programExecution) { if (!(programExecution instanceof final IcfgProgramExecution> rcfgProgramExecution)) { throw new IllegalArgumentException(); } + + // passes the worker cfg script from the rcfgProgramExecution through to the TypeSortTranslator + mTerm2Expression.getTypeSortTranslator().setCfgScriptFromWorker(rcfgProgramExecution.getOriginCfgScript()); + assert checkCallStackSourceProgramExecution(mLogger, programExecution) : "callstack of initial program execution already broken"; diff --git a/trunk/source/RCFGBuilder/src/de/uni_freiburg/informatik/ultimate/plugins/generator/rcfgbuilder/cfg/Call.java b/trunk/source/RCFGBuilder/src/de/uni_freiburg/informatik/ultimate/plugins/generator/rcfgbuilder/cfg/Call.java index d942c9f66f4..c78ec5c258f 100644 --- a/trunk/source/RCFGBuilder/src/de/uni_freiburg/informatik/ultimate/plugins/generator/rcfgbuilder/cfg/Call.java +++ b/trunk/source/RCFGBuilder/src/de/uni_freiburg/informatik/ultimate/plugins/generator/rcfgbuilder/cfg/Call.java @@ -29,6 +29,7 @@ import de.uni_freiburg.informatik.ultimate.boogie.ast.CallStatement; import de.uni_freiburg.informatik.ultimate.boogie.output.BoogiePrettyPrinter; +import de.uni_freiburg.informatik.ultimate.core.model.models.IPayload; import de.uni_freiburg.informatik.ultimate.core.model.models.annotation.Visualizable; import de.uni_freiburg.informatik.ultimate.core.model.services.ILogger; import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.structure.IIcfgCallTransition; @@ -52,7 +53,7 @@ public class Call extends CodeBlock implements IIcfgCallTransition protected CallStatement mCallStatement; protected String mPrettyPrintedStatements; - Call(final int serialNumber, final BoogieIcfgLocation source, final BoogieIcfgLocation target, + public Call(final int serialNumber, final BoogieIcfgLocation source, final BoogieIcfgLocation target, final CallStatement st, final ILogger logger) { super(serialNumber, source, target, logger); mCallStatement = st; @@ -86,5 +87,8 @@ public UnmodifiableTransFormula getLocalVarsAssignment() { protected int getNumberOfOpenCalls() { return 1; } - + + public void setPayload(IPayload payload) { + mPayload = payload; + } } diff --git a/trunk/source/RCFGBuilder/src/de/uni_freiburg/informatik/ultimate/plugins/generator/rcfgbuilder/cfg/Return.java b/trunk/source/RCFGBuilder/src/de/uni_freiburg/informatik/ultimate/plugins/generator/rcfgbuilder/cfg/Return.java index f73093ee165..acda7a01553 100644 --- a/trunk/source/RCFGBuilder/src/de/uni_freiburg/informatik/ultimate/plugins/generator/rcfgbuilder/cfg/Return.java +++ b/trunk/source/RCFGBuilder/src/de/uni_freiburg/informatik/ultimate/plugins/generator/rcfgbuilder/cfg/Return.java @@ -27,6 +27,7 @@ package de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder.cfg; import de.uni_freiburg.informatik.ultimate.boogie.ast.CallStatement; +import de.uni_freiburg.informatik.ultimate.core.model.models.IPayload; import de.uni_freiburg.informatik.ultimate.core.model.models.annotation.Visualizable; import de.uni_freiburg.informatik.ultimate.core.model.services.ILogger; import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.structure.IIcfgReturnTransition; @@ -48,7 +49,7 @@ public class Return extends CodeBlock implements IIcfgReturnTransition stmts, final ILogger logger) { super(serialNumber, source, target, logger); mStatements = new ArrayList<>(); @@ -163,4 +164,7 @@ public static boolean isAssumeTrueStatement(final Statement st) { return false; } + public void setPayload(IPayload payload) { + mPayload = payload; + } } diff --git a/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/AbstractCegarLoop.java b/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/AbstractCegarLoop.java index 9185e9c2c15..4de35dba292 100644 --- a/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/AbstractCegarLoop.java +++ b/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/AbstractCegarLoop.java @@ -139,7 +139,7 @@ public abstract class AbstractCegarLoop, A extends /** * Current Iteration of this CEGAR loop. */ - private int mIteration; + protected int mIteration; /** * Accepting run of the abstraction obtained in this iteration. @@ -397,7 +397,7 @@ private boolean computeInitialAbstraction() throws AutomataLibraryException { return false; } - private void iterate() throws AutomataLibraryException { + protected void iterate() throws AutomataLibraryException { mTimeBudget = initializeTimeBudget(); for (mIteration = 1; mIteration <= mPref.maxIterations(); mIteration++) { abortIfTimeout(); @@ -508,7 +508,7 @@ protected void performAbstractionSanityCheck() { // Empty implementation. Subclasses may override this method. } - private IcfgLocation getErrorLocFromCounterexample() { + protected IcfgLocation getErrorLocFromCounterexample() { return mCounterexample.getSymbol(mCounterexample.getLength() - 2).getTarget(); } @@ -583,7 +583,7 @@ private Map initializeTimeBudget() { return rtr; } - private IUltimateServiceProvider createIterationTimer(final IcfgLocation currentErrorLoc) { + protected IUltimateServiceProvider createIterationTimer(final IcfgLocation currentErrorLoc) { if (!mPref.hasErrorLocTimeLimit()) { // do not limit single counterexample if there is no limit on assert return mServices; @@ -766,7 +766,7 @@ public static final Result convert(final TaskCanceledException.UserDefinedLimit } - private final class CegarLoopResultBuilder { + protected final class CegarLoopResultBuilder { private final Map> mResults = new LinkedHashMap<>(); public CegarLoopResultBuilder addResultForAllRemaining(final Result result) { @@ -787,6 +787,7 @@ public CegarLoopResultBuilder addResultForProgramExecution(final Result result, final AtomicTraceElement lastElem = programExecution.getTraceElement(programExecution.getLength() - 1); final IcfgLocation loc = lastElem.getStep().getTarget(); return addResult(loc, result, programExecution, rtsp, reasonUnknown); + } public CegarLoopResultBuilder addResult(final IcfgLocation loc, final Result result, diff --git a/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/BasicCegarLoop.java b/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/BasicCegarLoop.java index 1de6f62c7c5..aa097fa94db 100644 --- a/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/BasicCegarLoop.java +++ b/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/BasicCegarLoop.java @@ -156,6 +156,8 @@ public abstract class BasicCegarLoop, A extends IAu protected boolean mFallbackToFpIfInterprocedural = false; protected IRefinementEngineResult> mRefinementResult; + protected InterpolationTechnique mInterpolationTechnique; + protected Class mTransitionClazz; private boolean mFirstReuseDump = true; @@ -166,14 +168,14 @@ public BasicCegarLoop(final DebugIdentifier name, final A initialAbstraction, fi final PredicateFactoryRefinement stateFactoryForRefinement) { super(services, name, initialAbstraction, rootNode, csToolkit, predicateFactory, taPrefs, errorLocs); mPathProgramDumpController = new PathProgramDumpController<>(getServices(), mPref, mIcfg); - + mTransitionClazz = transitionClazz; InterpolationTechnique interpolation = taPrefs.interpolation(); if (mFallbackToFpIfInterprocedural && rootNode.getProcedureEntryNodes().size() > 1 && interpolation == InterpolationTechnique.FPandBP) { mLogger.info("fallback from FPandBP to FP because CFG is interprocedural"); interpolation = InterpolationTechnique.ForwardPredicates; } - + mInterpolationTechnique = interpolation; mStoreFloydHoareAutomata = taPrefs.getFloydHoareAutomataReuse() != FloydHoareAutomataReuse.NONE; mStateFactoryForRefinement = stateFactoryForRefinement; mPredicateFactoryInterpolantAutomata = new PredicateFactoryForInterpolantAutomata(mCsToolkit.getManagedScript(), diff --git a/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/CegarLoopFactory.java b/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/CegarLoopFactory.java index 2f27c6dbdf7..4e9cfc7be02 100644 --- a/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/CegarLoopFactory.java +++ b/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/CegarLoopFactory.java @@ -221,16 +221,24 @@ private NwaCegarLoop createFiniteAutomataCegarLoop(final IUltimateServiceProv errorLocs, proofProducer, services, mTransitionClazz, stateFactoryForRefinement); } - return switch (mPrefs.getFloydHoareAutomataReuse()) { - case EAGER -> new EagerReuseCegarLoop<>(name, abstraction, root, csToolkit, predicateFactory, mPrefs, errorLocs, - proofProducer, services, Collections.emptyList(), rawFloydHoareAutomataFromFile, mTransitionClazz, - stateFactoryForRefinement); - case LAZY_IN_ORDER -> new LazyReuseCegarLoop<>(name, abstraction, root, csToolkit, predicateFactory, mPrefs, - errorLocs, proofProducer, services, Collections.emptyList(), rawFloydHoareAutomataFromFile, - mTransitionClazz, stateFactoryForRefinement); - case NONE -> new NwaCegarLoop<>(name, abstraction, root, csToolkit, predicateFactory, mPrefs, errorLocs, - proofProducer, services, mTransitionClazz, stateFactoryForRefinement); - }; + switch (mPrefs.getFloydHoareAutomataReuse()) { + case EAGER: + return new EagerReuseCegarLoop<>(name, abstraction, root, csToolkit, predicateFactory, mPrefs, errorLocs, + proofProducer, services, Collections.emptyList(), rawFloydHoareAutomataFromFile, mTransitionClazz, + stateFactoryForRefinement); + case LAZY_IN_ORDER: + return new LazyReuseCegarLoop<>(name, abstraction, root, csToolkit, predicateFactory, mPrefs, errorLocs, + proofProducer, services, Collections.emptyList(), rawFloydHoareAutomataFromFile, mTransitionClazz, + stateFactoryForRefinement); + case NONE: + if (mPrefs.isParallelCegarLoop()) { + return new ParallelNwaCegarLoop<>(name, abstraction, root, csToolkit, predicateFactory, mPrefs, + errorLocs, proofProducer, services, mTransitionClazz, stateFactoryForRefinement); + } + return new NwaCegarLoop<>(name, abstraction, root, csToolkit, predicateFactory, mPrefs, errorLocs, + proofProducer, services, mTransitionClazz, stateFactoryForRefinement); + } + throw new AssertionError("Unknown Setting: " + mPrefs.getFloydHoareAutomataReuse()); } private void requireNoReuse(final String analysis) { diff --git a/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/CegarNwaWorkerThread.java b/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/CegarNwaWorkerThread.java new file mode 100644 index 00000000000..9aa7b48e9d1 --- /dev/null +++ b/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/CegarNwaWorkerThread.java @@ -0,0 +1,578 @@ +/* + * Copyright (C) 2025 University of Freiburg + * Copyright (C) 2025 LMU Munich + * Copyright (C) 2025 Max Barth (Max.Barth@lmu.de) + * + * This file is part of the ULTIMATE Automata Library. + * + * The ULTIMATE Automata Library is free software: you can redistribute it and/or modify + * it under the terms of the GNU Lesser General Public License as published + * by the Free Software Foundation, either version 3 of the License, or + * (at your option) any later version. + * + * The ULTIMATE Automata Library is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU Lesser General Public License for more details. + * + * You should have received a copy of the GNU Lesser General Public License + * along with the ULTIMATE Automata Library. If not, see . + * + * Additional permission under GNU GPL version 3 section 7: + * If you modify the ULTIMATE Automata Library, or any covered work, by linking + * or combining it with Eclipse RCP (or a modified version of Eclipse RCP), + * containing parts covered by the terms of the Eclipse Public License, the + * licensors of the ULTIMATE Automata Library grant you additional permission + * to convey the resulting work. + */ +package de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction; + +import java.util.List; +import java.util.concurrent.BlockingQueue; +import java.util.stream.Collectors; + +import de.uni_freiburg.informatik.ultimate.automata.AutomataLibraryException; +import de.uni_freiburg.informatik.ultimate.automata.AutomataLibraryServices; +import de.uni_freiburg.informatik.ultimate.automata.AutomataOperationCanceledException; +import de.uni_freiburg.informatik.ultimate.automata.IAutomaton; +import de.uni_freiburg.informatik.ultimate.automata.IRun; +import de.uni_freiburg.informatik.ultimate.automata.nestedword.INestedWordAutomaton; +import de.uni_freiburg.informatik.ultimate.automata.nestedword.INwaOutgoingLetterAndTransitionProvider; +import de.uni_freiburg.informatik.ultimate.automata.nestedword.NestedRun; +import de.uni_freiburg.informatik.ultimate.automata.nestedword.NestedWordAutomaton; +import de.uni_freiburg.informatik.ultimate.automata.nestedword.operations.Difference; +import de.uni_freiburg.informatik.ultimate.automata.nestedword.operations.PowersetDeterminizer; +import de.uni_freiburg.informatik.ultimate.automata.nestedword.operations.oldapi.IOpWithDelayedDeadEndRemoval; +import de.uni_freiburg.informatik.ultimate.automata.nestedword.senwa.DifferenceSenwa; +import de.uni_freiburg.informatik.ultimate.core.lib.exceptions.RunningTaskInfo; +import de.uni_freiburg.informatik.ultimate.core.lib.exceptions.TaskCanceledException; +import de.uni_freiburg.informatik.ultimate.core.lib.exceptions.TaskCanceledException.UserDefinedLimit; +import de.uni_freiburg.informatik.ultimate.core.lib.exceptions.ToolchainCanceledException; +import de.uni_freiburg.informatik.ultimate.core.lib.results.UnprovabilityReason; +import de.uni_freiburg.informatik.ultimate.core.model.services.ILogger; +import de.uni_freiburg.informatik.ultimate.core.model.services.IUltimateServiceProvider; +import de.uni_freiburg.informatik.ultimate.core.model.translation.IProgramExecution; +import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.CfgSmtToolkit; +import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.IcfgProgramExecution; +import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.structure.IIcfg; +import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.structure.IIcfgTransition; +import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.structure.IcfgLocation; +import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.hoaretriple.HoareTripleCheckerCache; +import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.hoaretriple.HoareTripleCheckerUtils; +import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.hoaretriple.IHoareTripleChecker; +import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.smt.predicates.IPredicate; +import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.smt.predicates.IPredicateUnifier; +import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.smt.predicates.ISLPredicate; +import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.smt.predicates.PredicateFactory; +import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.taskidentifier.SubtaskIterationIdentifier; +import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.tracehandling.IRefinementEngineResult; +import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.tracehandling.ITraceCheckStrategyModule; +import de.uni_freiburg.informatik.ultimate.lib.smtlibutils.SmtUtils.SimplificationTechnique; +import de.uni_freiburg.informatik.ultimate.lib.tracecheckerutils.Counterexample; +import de.uni_freiburg.informatik.ultimate.lib.tracecheckerutils.singletracecheck.TraceCheckUtils; +import de.uni_freiburg.informatik.ultimate.logic.SMTLIBException; +import de.uni_freiburg.informatik.ultimate.logic.Script; +import de.uni_freiburg.informatik.ultimate.logic.Script.LBool; +import de.uni_freiburg.informatik.ultimate.logic.Term; +import de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.AbstractCegarLoop.CegarLoopResultBuilder; +import de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.AbstractCegarLoop.Result; +import de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.NwaCegarLoop.AutomatonType; +import de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TransferBetweenMainAndWorker.Mode; +import de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.errorabstraction.ErrorGeneralizationEngine; +import de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.interpolantautomata.transitionappender.AbstractInterpolantAutomaton; +import de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.interpolantautomata.transitionappender.DeterministicInterpolantAutomaton; +import de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.interpolantautomata.transitionappender.NondeterministicInterpolantAutomaton; +import de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.preferences.TAPreferences; +import de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.preferences.TAPreferences.InterpolantAutomatonEnhancement; +import de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.preferences.TraceAbstractionPreferenceInitializer.RefinementStrategy; +import de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.tracehandling.IpTcStrategyModuleAcceleratedTraceCheck; +import de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.tracehandling.StrategyFactory; +import de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.tracehandling.TaCheckAndRefinementPreferences; +import de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.tracehandling.TraceAbstractionRefinementEngine; +import de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.tracehandling.TraceAbstractionRefinementEngine.ITARefinementStrategy; +import de.uni_freiburg.informatik.ultimate.util.datastructures.relation.Pair; + +public class CegarNwaWorkerThread, A extends IAutomaton> + implements ICegarNwaWorkerThread { + private final ILogger mLogger; + private final TAPreferences mPref; + private final CegarLoopResultBuilder mResultBuilder; + private final IUltimateServiceProvider mServices; + private final CfgSmtToolkit mCfgSmtToolkit; + private final PredicateFactory mPredicateFactory; + private final PredicateFactoryForInterpolantAutomata mPredicateFactoryInterpolantAutomata; + private int mIteration; + private final ErrorGeneralizationEngine mErrorGeneralizationEngine; + private IRefinementEngineResult> mRefinementResult = null; + private NestedWordAutomaton mInterpolAutomaton = null; + private IRun mCounterexample = null; + private final TaCheckAndRefinementPreferences mTaCheckAndRefinementPrefs; + private final PredicateFactoryRefinement mStateFactoryForRefinement; + private final boolean mComputeHoareAnnotation; + private IcfgLocation mCurrentErrorLoc; + private final SimplificationTechnique mSimplificationTechnique; + protected static final boolean REMOVE_DEAD_ENDS = true; + private final ParallelNwaCegarLoop mMainThread; + private final INestedWordAutomaton mAbstraction; + private StrategyFactory mStrategyFactory; + // communication with controller + private WorkerThreadResult mThreadResult = null; + private final BlockingQueue> mBlockingQueueForResults; + private final BlockingQueue> mWorkerTaskQueue; + private final TransferBetweenMainAndWorker mNwaCexTransferrer; + + /** + * CegarNwaWorkerThread is a runnable that will be executed by an executinor service. It takes counterexamples from + * the workerTaskQueue and puts the resulting automata into the blockingQueueForResults. It takes the current + * abstraction from the controller, every time it does a difference calculation. + * + * transferWorkerUtils is used to transfer between worker and controller/main cfgScript + * + * TODO provide CEGAR loop statistics + * + * @author Max Barth (max.barth@lmu.de) + */ + public CegarNwaWorkerThread(final ILogger logger, final TAPreferences pref, final int id, + final CegarLoopResultBuilder resultBuilder, final IUltimateServiceProvider services, + final CfgSmtToolkit cfgSmtToolkit, final IIcfg icfg, + final PredicateFactory predicateFactory, final TaCheckAndRefinementPreferences taCheckAndRefinementPrefs, + final PredicateFactoryForInterpolantAutomata predicateFactoryInterpolantAutomata, + final PredicateFactoryRefinement stateFactoryForRefinement, final boolean computeHoareAnnotation, + final ParallelNwaCegarLoop mainThread, + final BlockingQueue> blockingQueueForResults, + final BlockingQueue> workerTaskQueue, + final TransferBetweenMainAndWorker transferWorkerUtils) throws InterruptedException { + + mLogger = logger; + mPref = pref; + mIteration = id; + mResultBuilder = resultBuilder; + mErrorGeneralizationEngine = new ErrorGeneralizationEngine<>(services); + mServices = services; + mCfgSmtToolkit = cfgSmtToolkit; + mTaCheckAndRefinementPrefs = taCheckAndRefinementPrefs; + mPredicateFactory = predicateFactory; + mPredicateFactoryInterpolantAutomata = predicateFactoryInterpolantAutomata; + mStateFactoryForRefinement = stateFactoryForRefinement; + mComputeHoareAnnotation = computeHoareAnnotation; + mSimplificationTechnique = pref.getSimplificationTechnique(); + mMainThread = mainThread; + mBlockingQueueForResults = blockingQueueForResults; + mWorkerTaskQueue = workerTaskQueue; + mNwaCexTransferrer = transferWorkerUtils; + mAbstraction = (INestedWordAutomaton) getAbstraction(); + + final Thread.UncaughtExceptionHandler exhandler = (th, ex) -> { + // TODO seems to work not sure if it is usefull + mThreadResult = new WorkerThreadResult<>(null, null, null, false, null, false, AutomatonType.ERROR, null, + mCounterexample, null, true); + try { + mBlockingQueueForResults.put(mThreadResult); + } catch (final InterruptedException e) { + // TODO Auto-generated catch block + e.printStackTrace(); + } + mMainThread.reportFailedContinuesWorkerThread(); + }; + Thread.currentThread().setUncaughtExceptionHandler(exhandler); + + } + + /* + * Gets a counterexamples from the blocking queue, sets up a strategy (checks how often the pathprogram has been + * seen). Checks feasibility, interpolates, creates an Error or Interpolant automaton. Calculates the difference to + * generalize the interpolant automaton and then puts a @WorkerThreadResult into the blocking queue for results. + * + * Terminates if the Thread is interrupted (not used atm) or the Executioner service triggers a shutdown. + */ + @Override + public void run() { + while (!Thread.currentThread().isInterrupted()) { + try { + mLogger.info("WorkerThread: " + Thread.currentThread() + " is Waiting for a Task"); + mIteration += 1; + mCounterexample = mNwaCexTransferrer.transferRun((NestedRun) mWorkerTaskQueue.take(), Mode.MAIN2WORKER); + final List trace = mCounterexample.getWord().asList(); + mCurrentErrorLoc = mCounterexample.getSymbol(mCounterexample.getLength() - 2).getTarget(); + final int traceHash = trace.hashCode(); + mLogger.info("Starting Thread: " + Thread.currentThread().getId() + "# for Trace Check: " + traceHash); + Thread.currentThread().setName("Worker for " + traceHash); + try { + final var locations = getControlConfigurationsFromCounterexample(mCounterexample); + final Counterexample counterexample = new Counterexample<>(mCounterexample.getWord(), locations); + final ITARefinementStrategy strategy = setUpStrategy(counterexample); + final Pair> isCexResult = isCounterexampleFeasible(strategy); + + final AbstractCegarLoop.AutomatonType automatonType = processFeasibilityCheckResult(strategy, + isCexResult.getFirst(), isCexResult.getSecond(), mCurrentErrorLoc); + constructRefinementAutomaton(automatonType); + mThreadResult = refineAbstractionInternally(); + } catch (AutomataLibraryException | ToolchainCanceledException | SMTLIBException e) { + throw new AssertionError("WorkerThread Failed: " + e); + } + mLogger.info("Done with Thread: " + Thread.currentThread().getId() + "#"); + mBlockingQueueForResults.put(mThreadResult); + } catch (final InterruptedException e) { + Thread.currentThread().interrupt(); + } + } + } + + protected List getControlConfigurationsFromCounterexample(final IRun run) { + return getIcfgLocationsFromRun(run); + } + + private List getIcfgLocationsFromRun(final IRun run) { + return run.getStateSequence().stream().map(p -> ((ISLPredicate) p).getProgramPoint()) + .collect(Collectors.toList()); + } + + /* + * The worker creates for each counterexample a new strategy module. We can switch between different + * RefinementStrateies here. For example we can use @RefinementStrategy.ACCELERATED_TRACE_CHECK if we have seen the + * pp 7 times. + * + * Warning, we have shared (read and write) access to the PathProgramCache here. But the PathProgramCache uses + * thread save lists and maps. + */ + private ITARefinementStrategy setUpStrategy(final Counterexample counterexample) { + mStrategyFactory = new StrategyFactory<>(mLogger, mPref, mTaCheckAndRefinementPrefs, mCfgSmtToolkit, + mPredicateFactory, mPredicateFactoryInterpolantAutomata, mMainThread.mTransitionClazz, + mMainThread.getCurrentProgramCache()); + + final ITARefinementStrategy strategy; + + if (mStrategyFactory.getPathProgramCache().getPathProgramCount(mCounterexample.getWord()) == 7 && false) { + strategy = mStrategyFactory.constructStrategy(getServices(), counterexample, mAbstraction, + new SubtaskIterationIdentifier(mMainThread.mTaskIdentifier, mIteration), + mPredicateFactoryInterpolantAutomata, getPreconditionProvider(), getPostconditionProvider(), + RefinementStrategy.ACCELERATED_TRACE_CHECK); + } else { + strategy = mStrategyFactory.constructStrategy(getServices(), counterexample, mAbstraction, + new SubtaskIterationIdentifier(mMainThread.mTaskIdentifier, mIteration), + mPredicateFactoryInterpolantAutomata, getPreconditionProvider(), getPostconditionProvider(), + mPref.getRefinementStrategy()); + } + return strategy; + } + + /** + * Worker takes the current abstraction from the main thread (read only). Then transfers it to worker script. + */ + private INwaOutgoingLetterAndTransitionProvider getAbstraction() { + final INwaOutgoingLetterAndTransitionProvider mainAbstraction = mMainThread.getAbstraction(); + final INwaOutgoingLetterAndTransitionProvider workerAbstraction = mNwaCexTransferrer + .transferAutomaton(mainAbstraction, mPredicateFactoryInterpolantAutomata, Mode.MAIN2WORKER); + return workerAbstraction; + } + + private IPreconditionProvider getPreconditionProvider() { + return IPreconditionProvider.constructDefaultPreconditionProvider(); + } + + private IPostconditionProvider getPostconditionProvider() { + return IPostconditionProvider.constructDefaultPostconditionProvider(); + } + + protected Pair> + isCounterexampleFeasible(final ITARefinementStrategy strategy) { + try { + if (mPref.hasLimitPathProgramCount() && mPref.getLimitPathProgramCount() < mStrategyFactory + .getPathProgramCache().getPathProgramCount(mCounterexample.getWord())) { + final String taskDescription = "bailout by path program count limit in iteration " + mIteration; + throw new TaskCanceledException(UserDefinedLimit.PATH_PROGRAM_ATTEMPTS, getClass(), taskDescription); + } + + final TraceAbstractionRefinementEngine refinementEngine = + new TraceAbstractionRefinementEngine<>(getServices(), mLogger, strategy); + mRefinementResult = refinementEngine.getResult(); + + } catch (final ToolchainCanceledException | SMTLIBException tce) { + throw tce; + } + final LBool feasibility = mRefinementResult.getCounterexampleFeasibility(); + IProgramExecution rcfgProgramExecution = null; + if (feasibility != LBool.UNSAT) { + mLogger.info("Counterexample %s feasible", feasibility == LBool.SAT ? "is" : "might be"); + if (mRefinementResult.providesIcfgProgramExecution()) { + rcfgProgramExecution = mRefinementResult.getIcfgProgramExecution(); + } else { + rcfgProgramExecution = + TraceCheckUtils.computeSomeIcfgProgramExecutionWithoutValues(mCounterexample.getWord()); + } + ((IcfgProgramExecution) rcfgProgramExecution).setOriginCfgScript(mCfgSmtToolkit.getManagedScript()); + } + // TODO use some kind of mCegarLoopBenchmark (currently leads to concurrency problems) + return new Pair<>(feasibility, rcfgProgramExecution); + } + + /** + * Report results from a feasibility check if necessary and return the type of the refinement automaton + * + * @param strategy + */ + private AbstractCegarLoop.AutomatonType processFeasibilityCheckResult(final ITARefinementStrategy strategy, + final LBool isCounterexampleFeasible, final IProgramExecution programExecution, + final IcfgLocation currentErrorLoc) { + if (isCounterexampleFeasible == Script.LBool.SAT) { + mResultBuilder.addResultForProgramExecution(Result.UNSAFE, programExecution, null, null); + if (mPref.stopAfterFirstViolation()) { + mResultBuilder.addResultForAllRemaining(Result.UNKNOWN); + } + return AbstractCegarLoop.AutomatonType.ERROR; + } + if (isCounterexampleFeasible != Script.LBool.UNKNOWN) { + return AbstractCegarLoop.AutomatonType.INTERPOLANT; + } + Result actualResult; + if (programExecution != null) { + for (final ITraceCheckStrategyModule module : strategy.getTraceCheckModules()) { + if (module instanceof IpTcStrategyModuleAcceleratedTraceCheck) { + throw new AssertionError( + "TraceCheck Unknown, dont return result. Might be just this Strategy that fails"); + } + } + final UnprovabilityReason reasonUnknown = + new UnprovabilityReason("unable to decide satisfiability of path constraint"); + actualResult = Result.UNKNOWN; + mResultBuilder.addResultForProgramExecution(actualResult, programExecution, null, reasonUnknown); + } + actualResult = Result.TIMEOUT; + mResultBuilder.addResult(currentErrorLoc, actualResult, null, null, null); + + if (mPref.stopAfterFirstViolation()) { + mResultBuilder.addResultForAllRemaining(actualResult); + } + + return AbstractCegarLoop.AutomatonType.UNKNOWN; + } + + /** + * This Method does not do the sanity checks done in NWA for the correctness of Error and Interpolant automata! + * + * @param automatonType + * @throws AutomataOperationCanceledException + */ + private void constructRefinementAutomaton(final AbstractCegarLoop.AutomatonType automatonType) + throws AutomataOperationCanceledException { + switch (automatonType) { + case ERROR: + case UNKNOWN: + mLogger.info("Excluding counterexample to continue analysis with %s automaton", automatonType); + mErrorGeneralizationEngine.constructErrorAutomaton(mCounterexample, mPredicateFactory, + mRefinementResult.getPredicateUnifier(), mCfgSmtToolkit, mSimplificationTechnique, + mCfgSmtToolkit.getSymbolTable(), mPredicateFactoryInterpolantAutomata, mAbstraction, mIteration); + mInterpolAutomaton = null; + break; + case INTERPOLANT: + mInterpolAutomaton = mRefinementResult.getInfeasibilityProof(); + break; + default: + throw new UnsupportedOperationException("Unknown automaton type: " + automatonType); + } + } + + protected IUltimateServiceProvider getServices() { + return mServices; + } + + private WorkerThreadResult refineAbstractionInternally() throws AutomataLibraryException { + mStateFactoryForRefinement.setIteration(mIteration); + // mCegarLoopBenchmark.start(CegarLoopStatisticsDefinitions.AutomataDifference.toString()); + final IPredicateUnifier predicateUnifier = mRefinementResult.getPredicateUnifier(); + final IHoareTripleChecker htc = getHoareTripleChecker(); + + final AutomatonType automatonType; + final boolean useErrorAutomaton; + final NestedWordAutomaton subtrahendBeforeEnhancement; + final InterpolantAutomatonEnhancement enhanceMode; + final INwaOutgoingLetterAndTransitionProvider subtrahend; + final boolean exploitSigmaStarConcatOfIa; + if (mErrorGeneralizationEngine.hasAutomatonInIteration(mIteration)) { + mErrorGeneralizationEngine.startDifference(); + automatonType = AutomatonType.ERROR; + useErrorAutomaton = true; + exploitSigmaStarConcatOfIa = false; + enhanceMode = mErrorGeneralizationEngine.getEnhancementMode(); + subtrahendBeforeEnhancement = mErrorGeneralizationEngine.getResultBeforeEnhancement(); + subtrahend = mErrorGeneralizationEngine.getResultAfterEnhancement(); + + } else { + automatonType = AutomatonType.FLOYD_HOARE; + useErrorAutomaton = false; + exploitSigmaStarConcatOfIa = !mComputeHoareAnnotation; + subtrahendBeforeEnhancement = mInterpolAutomaton; + enhanceMode = mPref.interpolantAutomatonEnhancement(); + subtrahend = enhanceInterpolantAutomaton(enhanceMode, predicateUnifier, htc, subtrahendBeforeEnhancement); + + } + + mLogger.info("Difference in Worker for Generalization"); + computeAutomataDifference(mAbstraction, subtrahend, subtrahendBeforeEnhancement, predicateUnifier, + exploitSigmaStarConcatOfIa, htc, enhanceMode, useErrorAutomaton, automatonType); + + final WorkerThreadResult workerResult = new WorkerThreadResult<>( + mNwaCexTransferrer.transferAutomaton(subtrahend, mPredicateFactoryInterpolantAutomata, + Mode.WORKER2MAIN), + mNwaCexTransferrer.transferAutomaton(subtrahendBeforeEnhancement, mPredicateFactoryInterpolantAutomata, + Mode.WORKER2MAIN), + predicateUnifier, exploitSigmaStarConcatOfIa, enhanceMode, useErrorAutomaton, automatonType, + mCfgSmtToolkit.getManagedScript(), + mNwaCexTransferrer.transferRun((NestedRun) mCounterexample, Mode.WORKER2MAIN), mPredicateFactory, + false); + + // TODO missing a lot of stuff from NwaCegarLoop + + return workerResult; + } + + /* + * WARNING The real difference has to be computed in the Main Thrad / CEGAR loop This is only used to enhance the + * interpolant automaton + */ + private IOpWithDelayedDeadEndRemoval computeAutomataDifference( + final INestedWordAutomaton minuend, + final INwaOutgoingLetterAndTransitionProvider subtrahend, + final INwaOutgoingLetterAndTransitionProvider subtrahendBeforeEnhancement, + final IPredicateUnifier predicateUnifier, final boolean explointSigmaStarConcatOfIA, + final IHoareTripleChecker htc, final InterpolantAutomatonEnhancement enhanceMode, + final boolean useErrorAutomaton, final AutomatonType automatonType) + throws AutomataLibraryException, AssertionError { + if (enhanceMode == InterpolantAutomatonEnhancement.NONE) { + return null; + } + try { + mLogger.debug("WORKER: Start constructing difference for enhancing interpolant automaton in worker"); + final PowersetDeterminizer psd = + new PowersetDeterminizer<>(subtrahend, true, mPredicateFactoryInterpolantAutomata); + IOpWithDelayedDeadEndRemoval diff; + try { + if (mPref.differenceSenwa()) { + diff = new DifferenceSenwa<>(new AutomataLibraryServices(getServices()), mStateFactoryForRefinement, + minuend, subtrahend, psd, false); + } else { + diff = new Difference<>(new AutomataLibraryServices(getServices()), mStateFactoryForRefinement, + minuend, subtrahend, psd, explointSigmaStarConcatOfIA); + } + } catch (final AutomataOperationCanceledException | ToolchainCanceledException tce) { + final RunningTaskInfo runningTaskInfo = executeDifferenceTimeoutActions(minuend, subtrahend, + subtrahendBeforeEnhancement, automatonType); + tce.addRunningTaskInfo(runningTaskInfo); + throw tce; + } finally { + + assert subtrahend instanceof AbstractInterpolantAutomaton + : "if enhancement is used, we need AbstractInterpolantAutomaton"; + ((AbstractInterpolantAutomaton) subtrahend).switchToReadonlyMode(); + + } + + if (REMOVE_DEAD_ENDS) { + if (mComputeHoareAnnotation) { + // TODO missing stuff + } + diff.removeDeadEnds(); + } + return diff; + } finally { + mLogger.info(predicateUnifier.collectPredicateUnifierStatistics()); + mLogger.info(htc.getStatistics()); + mLogger.info(htc); + mLogger.debug("WORKER: Finished constructing difference"); + } + + } + + private RunningTaskInfo executeDifferenceTimeoutActions(final INestedWordAutomaton minuend, + final INwaOutgoingLetterAndTransitionProvider subtrahend, + final INwaOutgoingLetterAndTransitionProvider subtrahendBeforeEnhancement, + final AutomatonType automatonType) throws AutomataLibraryException { + final RunningTaskInfo runningTaskInfo = + getDifferenceTimeoutRunningTaskInfo(minuend, subtrahend, subtrahendBeforeEnhancement, automatonType); + return runningTaskInfo; + } + + private RunningTaskInfo getDifferenceTimeoutRunningTaskInfo(final INestedWordAutomaton minuend, + final INwaOutgoingLetterAndTransitionProvider subtrahend, + final INwaOutgoingLetterAndTransitionProvider subtrahendBeforeEnhancement, + final AutomatonType automatonType) { + final String taskDescription = "WORKER: constructing difference of abstraction (" + minuend.size() + + "states) and " + automatonType + " automaton (currently " + subtrahend.size() + " states, " + + subtrahendBeforeEnhancement.size() + " states before enhancement)"; + return new RunningTaskInfo(getClass(), taskDescription); + } + + protected final IHoareTripleChecker getHoareTripleChecker() { + final IHoareTripleChecker refinementHtc = mRefinementResult.getHoareTripleChecker(); + if (refinementHtc != null) { + return refinementHtc; + } + final HoareTripleCheckerCache initialCache = + TraceAbstractionUtils.extractHoareTriplesfromAutomaton(mRefinementResult.getInfeasibilityProof()); + return HoareTripleCheckerUtils.constructEfficientHoareTripleCheckerWithCaching(getServices(), + mPref.getHoareTripleChecks(), mCfgSmtToolkit, mRefinementResult.getPredicateUnifier(), initialCache); + } + + protected INwaOutgoingLetterAndTransitionProvider enhanceInterpolantAutomaton( + final InterpolantAutomatonEnhancement enhanceMode, final IPredicateUnifier predicateUnifier, + final IHoareTripleChecker htc, final NestedWordAutomaton interpolantAutomaton) { + final INwaOutgoingLetterAndTransitionProvider subtrahend; + if (enhanceMode == InterpolantAutomatonEnhancement.NONE) { + subtrahend = interpolantAutomaton; + } else { + final AbstractInterpolantAutomaton ia = constructInterpolantAutomatonForOnDemandEnhancement( + interpolantAutomaton, predicateUnifier, htc, enhanceMode); + subtrahend = ia; + } + return subtrahend; + } + + protected AbstractInterpolantAutomaton constructInterpolantAutomatonForOnDemandEnhancement( + final NestedWordAutomaton inputInterpolantAutomaton, + final IPredicateUnifier predicateUnifier, final IHoareTripleChecker htc, + final InterpolantAutomatonEnhancement enhanceMode) { + final AbstractInterpolantAutomaton result; + switch (enhanceMode) { + case NONE: + throw new IllegalArgumentException("In setting NONE we will not do any enhancement"); + case PREDICATE_ABSTRACTION: + case PREDICATE_ABSTRACTION_CONSERVATIVE: + case PREDICATE_ABSTRACTION_CANNIBALIZE: + result = constructInterpolantAutomatonForOnDemandEnhancementPredicateAbstraction(inputInterpolantAutomaton, + predicateUnifier, htc, enhanceMode); + break; + case EAGER: + case NO_SECOND_CHANCE: + case EAGER_CONSERVATIVE: + result = constructInterpolantAutomatonForOnDemandEnhancementEager(inputInterpolantAutomaton, + predicateUnifier, htc, enhanceMode); + break; + default: + throw new UnsupportedOperationException("unknown " + enhanceMode); + } + return result; + } + + private NondeterministicInterpolantAutomaton constructInterpolantAutomatonForOnDemandEnhancementEager( + final NestedWordAutomaton inputInterpolantAutomaton, + final IPredicateUnifier predicateUnifier, final IHoareTripleChecker htc, + final InterpolantAutomatonEnhancement enhanceMode) { + final boolean conservativeSuccessorCandidateSelection = + enhanceMode == InterpolantAutomatonEnhancement.EAGER_CONSERVATIVE; + final boolean secondChance = enhanceMode != InterpolantAutomatonEnhancement.NO_SECOND_CHANCE; + return new NondeterministicInterpolantAutomaton<>(getServices(), mCfgSmtToolkit, htc, inputInterpolantAutomaton, + predicateUnifier, conservativeSuccessorCandidateSelection, secondChance); + } + + private DeterministicInterpolantAutomaton + constructInterpolantAutomatonForOnDemandEnhancementPredicateAbstraction( + final NestedWordAutomaton inputInterpolantAutomaton, + final IPredicateUnifier predicateUnifier, final IHoareTripleChecker htc, + final InterpolantAutomatonEnhancement enhanceMode) { + final boolean conservativeSuccessorCandidateSelection = + enhanceMode == InterpolantAutomatonEnhancement.PREDICATE_ABSTRACTION_CONSERVATIVE; + final boolean cannibalize = enhanceMode == InterpolantAutomatonEnhancement.PREDICATE_ABSTRACTION_CANNIBALIZE; + return new DeterministicInterpolantAutomaton<>(getServices(), mCfgSmtToolkit, htc, inputInterpolantAutomaton, + predicateUnifier, conservativeSuccessorCandidateSelection, cannibalize); + } +} diff --git a/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/ICegarNwaWorkerThread.java b/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/ICegarNwaWorkerThread.java new file mode 100644 index 00000000000..03dcf169d2b --- /dev/null +++ b/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/ICegarNwaWorkerThread.java @@ -0,0 +1,35 @@ +/* + * Copyright (C) 2025 University of Freiburg + * Copyright (C) 2025 LMU Munich + * Copyright (C) 2025 Max Barth (Max.Barth@lmu.de) + * + * This file is part of the ULTIMATE Automata Library. + * + * The ULTIMATE Automata Library is free software: you can redistribute it and/or modify + * it under the terms of the GNU Lesser General Public License as published + * by the Free Software Foundation, either version 3 of the License, or + * (at your option) any later version. + * + * The ULTIMATE Automata Library is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU Lesser General Public License for more details. + * + * You should have received a copy of the GNU Lesser General Public License + * along with the ULTIMATE Automata Library. If not, see . + * + * Additional permission under GNU GPL version 3 section 7: + * If you modify the ULTIMATE Automata Library, or any covered work, by linking + * or combining it with Eclipse RCP (or a modified version of Eclipse RCP), + * containing parts covered by the terms of the Eclipse Public License, the + * licensors of the ULTIMATE Automata Library grant you additional permission + * to convey the resulting work. + */ +package de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction; + +/* + * Interface for grouping different kinds of WorkerThreads + */ +public interface ICegarNwaWorkerThread extends Runnable { + +} diff --git a/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/NwaCegarLoop.java b/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/NwaCegarLoop.java index d889b9e5632..d0c4e23585d 100644 --- a/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/NwaCegarLoop.java +++ b/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/NwaCegarLoop.java @@ -120,7 +120,7 @@ */ public class NwaCegarLoop> extends BasicCegarLoop> { - private enum AutomatonType { + protected enum AutomatonType { FLOYD_HOARE, ERROR; } @@ -135,13 +135,13 @@ private enum AutomatonType { protected final Collection> mStoredRawInterpolantAutomata; - private final SearchStrategy mSearchStrategy; - private final ErrorGeneralizationEngine mErrorGeneralizationEngine; + protected final SearchStrategy mSearchStrategy; + protected final ErrorGeneralizationEngine mErrorGeneralizationEngine; private final boolean mUseHeuristicEmptinessCheck; private final ScoringMethod mScoringMethod; private final AStarHeuristic mAStarHeuristic; - private final Integer mAStarRandomHeuristicSeed; + protected final Integer mAStarRandomHeuristicSeed; protected final NwaHoareProofProducer mProofUpdater; diff --git a/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/ParallelNwaCegarLoop.java b/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/ParallelNwaCegarLoop.java new file mode 100644 index 00000000000..06be3279770 --- /dev/null +++ b/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/ParallelNwaCegarLoop.java @@ -0,0 +1,747 @@ +/* + * Copyright (C) 2025 University of Freiburg + * Copyright (C) 2025 LMU Munich + * Copyright (C) 2025 Max Barth (Max.Barth@lmu.de) + * + * This file is part of the ULTIMATE Automata Library. + * + * The ULTIMATE Automata Library is free software: you can redistribute it and/or modify + * it under the terms of the GNU Lesser General Public License as published + * by the Free Software Foundation, either version 3 of the License, or + * (at your option) any later version. + * + * The ULTIMATE Automata Library is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU Lesser General Public License for more details. + * + * You should have received a copy of the GNU Lesser General Public License + * along with the ULTIMATE Automata Library. If not, see . + * + * Additional permission under GNU GPL version 3 section 7: + * If you modify the ULTIMATE Automata Library, or any covered work, by linking + * or combining it with Eclipse RCP (or a modified version of Eclipse RCP), + * containing parts covered by the terms of the Eclipse Public License, the + * licensors of the ULTIMATE Automata Library grant you additional permission + * to convey the resulting work. + */ +package de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction; + +import java.util.Arrays; +import java.util.Collections; +import java.util.HashMap; +import java.util.HashSet; +import java.util.List; +import java.util.Map; +import java.util.Set; +import java.util.concurrent.BlockingQueue; +import java.util.concurrent.CancellationException; +import java.util.concurrent.ExecutorService; +import java.util.concurrent.Executors; +import java.util.concurrent.LinkedBlockingQueue; +import java.util.function.Function; +import java.util.stream.Collectors; + +import de.uni_freiburg.informatik.ultimate.automata.AutomataLibraryException; +import de.uni_freiburg.informatik.ultimate.automata.AutomataLibraryServices; +import de.uni_freiburg.informatik.ultimate.automata.AutomataOperationCanceledException; +import de.uni_freiburg.informatik.ultimate.automata.IAutomaton; +import de.uni_freiburg.informatik.ultimate.automata.IRun; +import de.uni_freiburg.informatik.ultimate.automata.nestedword.IDoubleDeckerAutomaton; +import de.uni_freiburg.informatik.ultimate.automata.nestedword.INestedWordAutomaton; +import de.uni_freiburg.informatik.ultimate.automata.nestedword.INwaOutgoingLetterAndTransitionProvider; +import de.uni_freiburg.informatik.ultimate.automata.nestedword.NestedRun; +import de.uni_freiburg.informatik.ultimate.automata.nestedword.NestedWordAutomaton; +import de.uni_freiburg.informatik.ultimate.automata.nestedword.operations.Difference; +import de.uni_freiburg.informatik.ultimate.automata.nestedword.operations.IsEmpty; +import de.uni_freiburg.informatik.ultimate.automata.nestedword.operations.IsEmptyParallel; +import de.uni_freiburg.informatik.ultimate.automata.nestedword.operations.PowersetDeterminizer; +import de.uni_freiburg.informatik.ultimate.automata.nestedword.operations.oldapi.IOpWithDelayedDeadEndRemoval; +import de.uni_freiburg.informatik.ultimate.automata.nestedword.senwa.DifferenceSenwa; +import de.uni_freiburg.informatik.ultimate.core.lib.exceptions.ToolchainCanceledException; +import de.uni_freiburg.informatik.ultimate.core.model.preferences.IPreferenceProvider; +import de.uni_freiburg.informatik.ultimate.core.model.services.IUltimateServiceProvider; +import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.CfgSmtToolkit; +import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.structure.IIcfg; +import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.structure.IIcfgTransition; +import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.structure.IcfgLocation; +import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.structure.debugidentifiers.DebugIdentifier; +import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.hoaretriple.IHoareTripleChecker; +import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.smt.predicates.IMLPredicate; +import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.smt.predicates.IPredicate; +import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.smt.predicates.IPredicateUnifier; +import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.smt.predicates.ISLPredicate; +import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.smt.predicates.PredicateFactory; +import de.uni_freiburg.informatik.ultimate.lib.proofs.floydhoare.NwaHoareProofProducer; +import de.uni_freiburg.informatik.ultimate.lib.smtlibutils.ManagedScript; +import de.uni_freiburg.informatik.ultimate.lib.smtlibutils.solverbuilder.SolverBuilder; +import de.uni_freiburg.informatik.ultimate.lib.smtlibutils.solverbuilder.SolverBuilder.SolverMode; +import de.uni_freiburg.informatik.ultimate.lib.smtlibutils.solverbuilder.SolverBuilder.SolverSettings; +import de.uni_freiburg.informatik.ultimate.logic.Logics; +import de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder.Activator; +import de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder.preferences.RcfgPreferenceInitializer; +import de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.automataminimization.AutomataMinimization; +import de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.automataminimization.AutomataMinimization.AutomataMinimizationTimeout; +import de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.preferences.TAPreferences; +import de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.preferences.TAPreferences.InterpolantAutomatonEnhancement; +import de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.preferences.TraceAbstractionPreferenceInitializer.Minimization; +import de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.preferences.TraceAbstractionPreferenceInitializer.RelevanceAnalysisMode; +import de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.tracehandling.TaCheckAndRefinementPreferences; + +public class ParallelNwaCegarLoop, A extends IAutomaton> + extends NwaCegarLoop { + + boolean mComputeHoareAnnotation; + final String mDestroyEverything = "destroyEverything"; + + // Parallel Setup + private final ExecutorService mExec; + private int mThreadLimit; + private int mRunningThreads = 0; + + // private final CompletionService> mECS; + BlockingQueue> mWorkerTaskQueue = new LinkedBlockingQueue<>(); + BlockingQueue> mWorkerResultQueue = new LinkedBlockingQueue<>(); + + // need global program cache, but worker need to get copy otherwise we + // synchronize + private final PathProgramCache mProgramCache = new PathProgramCache<>(mLogger); + + // Strategies + public final HashMap> mActiveCounterexamples = new HashMap<>(); + private final Set mCounterexamplesToBeRemovedFromActiveCexMap = new HashSet<>(); + + // Addtional Statistiks for Evaluation + private Integer mCounterexamplesChecked = 0; + private Integer mRefinementsDone = 0; + private final Integer mCountTimeoutsInSearch = 0; + private final Integer mCountFailedRunConstructions = 0; + private Integer mCountFailedToFindCex = 0; + private Integer mCountBfsFoundCex = 1; + private final Integer mCountIsEmptyParallel = 0; + private Integer maxActiveThreads = 0; + private final Integer mActiveExecutors = 0; + private long mSearchTime = 0; + private long mWorkerSetUpTime = 0; + private int mIterationsWithMaxThreads = 0; + private int mIterationsWithOneThread = 0; + private final int mExceptionInWorker = 0; + + private long mRefinementTime = 0; + + /** + * Based on the @NwaCegarLoop. Given a ThreadLimit, creates a ExecutionerService that will manage the worker + * threads. Executes each tracecheck in a new thread called worker. This loop, only searches for counterexamples and + * updates the abstraction. The feasiblity check and generalization of interpolant automata is done by the workers. + * + * TODO option to save memory, measure heap, then dont spawn worker / kill a worker + * + * @author Max Barth (max.barth@lmu.de) + */ + + public ParallelNwaCegarLoop(final DebugIdentifier name, + final INestedWordAutomaton initialAbstraction, final IIcfg rootNode, + final CfgSmtToolkit csToolkit, final PredicateFactory predicateFactory, final TAPreferences taPrefs, + final Set errorLocs, final NwaHoareProofProducer proofProducer, + final IUltimateServiceProvider services, final Class transitionClazz, + final PredicateFactoryRefinement stateFactoryForRefinement) { + super(name, initialAbstraction, rootNode, csToolkit, predicateFactory, taPrefs, errorLocs, proofProducer, + services, transitionClazz, stateFactoryForRefinement); + // Start thread pool + mThreadLimit = mPref.getThreadLimit(); + if (mThreadLimit == 0) { // maximum of available cores + mThreadLimit = Runtime.getRuntime().availableProcessors(); + mThreadLimit -= 1; // one for main thread + } + + mExec = Executors.newFixedThreadPool(mThreadLimit); + Thread.currentThread().setName("Main Cegar Thread"); + getServices().getStorage().pushMarker(mDestroyEverything); + } + + /* + * Sets up a worker with that communicates via blocking queues and stays alive after one counterexample check. Every + * transfer between controller and worker goes via @TransferBetweenMainAndWorker. + * + */ + private ICegarNwaWorkerThread setUpContinuesWorker(final IUltimateServiceProvider iterationServices, + final int id) throws InterruptedException { + + final TransferBetweenMainAndWorker transferUtils = new TransferBetweenMainAndWorker<>( + new AutomataLibraryServices(mServices), mLogger, mCsToolkit.getManagedScript(), iterationServices, + getSolverSettings(iterationServices, + getIteration() + mRunningThreads + mCounterexample.getWord().asList().hashCode() + "parallel"), + mCsToolkit); + + final CfgSmtToolkit freshToolKit = transferUtils.constructWorkerCfgSmtToolkit(); + + // Create predicateFactory with worker script + final PredicateFactory predicateFactory = + new PredicateFactory(mServices, freshToolKit.getManagedScript(), freshToolKit.getSymbolTable()); + + // Create PredicateFactoryForInterpolantAutomata with worker script + final PredicateFactoryForInterpolantAutomata predicateFactoryInterpolantAutomata = + new PredicateFactoryForInterpolantAutomata(freshToolKit.getManagedScript(), predicateFactory, + mComputeHoareAnnotation); + + final Set hoareAnnotationLocs = Collections.emptySet(); + if (mComputeHoareAnnotation) { + // TODO need different hoareAnnotationLocs + throw new AssertionError("Hoare Annotations not yet supported in Parallel cegar loop"); + } + final PredicateFactoryRefinement stateFactoryForRefinement = new PredicateFactoryRefinement(mServices, + freshToolKit.getManagedScript(), predicateFactory, mComputeHoareAnnotation, hoareAnnotationLocs); + + // make sure that mPref.getCfgSmtToolkit returns the worker toolkit + final TaCheckAndRefinementPreferences taCheckAndRefinementPrefs = + new TaCheckAndRefinementPreferences<>(getServices(), mPref, mInterpolationTechnique, + mSimplificationTechnique, freshToolKit, predicateFactory, mIcfg); + + // initialize worker + return new CegarNwaWorkerThread<>(mLogger, mPref, id, mResultBuilder, iterationServices, freshToolKit, mIcfg, + predicateFactory, taCheckAndRefinementPrefs, predicateFactoryInterpolantAutomata, + stateFactoryForRefinement, mComputeHoareAnnotation, this, mWorkerResultQueue, mWorkerTaskQueue, + transferUtils); + } + + /* + * Parallel CEGAR loop. In each iteration we pick a counterexample and put it into a blocking queue for a worker to + * check its feasibility + ** + * As soon as we obtain a worker result via blocking queue, we refine our abstraction. If abstraction is not empty, + * we continue with the loop. If no worker is done, continue with the loop. If no thread is available and no worker + * is done we sleep. + */ + @Override + protected void iterate() throws AutomataLibraryException { + // TODO manage time and timeout + boolean didntFindCexLastIteration = false; + final IcfgLocation currentErrorLoc = getErrorLocFromCounterexample(); + final IUltimateServiceProvider iterationServices = createIterationTimer(currentErrorLoc); + for (int i = 0; i < mThreadLimit; i++) { + try { + mExec.submit(setUpContinuesWorker(iterationServices, i)); + } catch (final InterruptedException e) { + throw new AssertionError("TODO"); + } + } + + // start worker for initial cex: + startWorker(); + + for (mIteration = 1; mIteration <= mPref.maxIterations(); mIteration++) { + // TODO deal with crashing workers, currently we just sleep thats bad!!!! + abortIfTimeout(); + boolean abstractionWasRefined = false; + mLogger.info(String.format("=== Iteration %s ===", getIteration())); + + try { + // we sleep if not: thread or counterexample is available + WorkerThreadResult workerResult = getWorkerResult(didntFindCexLastIteration); + + // go through all done workerResult + while (workerResult != null) { + final long time = System.nanoTime() / 1000000000; + try { + mLogger.info("Main: A Thread is Done"); + if (workerResult.workerCrashed()) { + mLogger.error("Main: Worker Crashed! exiting CEGAR loop."); + // TODO how do we want to handle a worker crash? + shutDownAndDestroy(mDestroyEverything); + throw new AssertionError("Worker Crashed!, Exiting CEGAR loop!"); + } + // If Error automaton terminate immediately + if (mPref.stopAfterFirstViolation() + && workerResult.getAutomatonType().equals(AutomatonType.ERROR)) { + shutDownAndDestroy(mDestroyEverything); + updateAndPrintStatistics(true); + return; + } + + mLogger.info("Worker Automaton Type: " + workerResult.getAutomatonType()); + mLogger.info("Refining Abstraction"); + refinement(workerResult); + mRefinementsDone += 1; + abstractionWasRefined = true; + // Not sure if necessary + workerResult.garbageCollect(); + // If new abstraction is empty terminate immediately + if (isSafeThenTerminate()) { + updateAndPrintStatistics(true); + return; + } + + } catch (final CancellationException e) { + mLogger.warn("Worker was cancelled! " + e); + } catch (final Exception e) { + mLogger.warn("Worker Failed! " + e); + throw e; + } finally { + + } + workerResult = mWorkerResultQueue.poll(); + mRefinementTime += ((System.nanoTime() / 1000000000) - time); + } + mLogger.info("No more worker results to process"); + assert workerResult == null; + + } catch (final ToolchainCanceledException e) { + mLogger.warn("Worker Failed! " + e); + throw e; + } catch (final InterruptedException ie) { + ie.printStackTrace(); + mLogger.warn("Worker was interrupted! " + ie); + } + if (abstractionWasRefined && !mPref.minimizeAbstractionPerWorker()) { + // uses NWA CEGAR loop + // When do we minimize how often? + minimizeAbstractionIfEnabled(); + } + if (abstractionWasRefined) { + // If we didnt find one we wait until we refine the abstraction + didntFindCexLastIteration = false; + } + + /* + * In the first iteration we search via BFS, then we use IsEmptyParallel + */ + boolean firstIteration = true; + while (mRunningThreads < mThreadLimit && !didntFindCexLastIteration) { + assert mRunningThreads >= 0; + mCounterexample = searchForErrorTrace(!firstIteration); + if (mCounterexample == null) { + didntFindCexLastIteration = true; + break; + } + if (mCounterexample != null) { + startWorker(); + } + firstIteration = false; + } + updateAndPrintStatistics(false); + } + mExec.shutdownNow(); + mResultBuilder.addResultForAllRemaining(Result.USER_LIMIT_ITERATIONS); + + } + + private void updateAndPrintStatistics(final boolean printStatistics) { + + if (mRunningThreads > maxActiveThreads) { + maxActiveThreads = mRunningThreads; + } + if (mRunningThreads == mThreadLimit) { + mIterationsWithMaxThreads += 1; + } + if (mRunningThreads == 1) { + mIterationsWithOneThread += 1; + } + if (printStatistics) { + mLogger.info("Iteration " + getIteration()); + mLogger.info("Refinements: " + mRefinementsDone); + mLogger.info("Counterexamples: " + mCounterexamplesChecked); + mLogger.info("SearchTimeout: " + mCountTimeoutsInSearch); + mLogger.info("RunConstructionFailed: " + mCountFailedRunConstructions); + mLogger.info("SearchFailed: " + mCountFailedToFindCex); + mLogger.info("BFS: " + mCountBfsFoundCex); + mLogger.info("IsEmptyParallel: " + mCountIsEmptyParallel); + mLogger.info("ActiveThreads: " + maxActiveThreads); + mLogger.info("ActiveExecutorsForPathPrograms: " + mActiveExecutors); + mLogger.info("IterationsWithMaxThreads: " + mIterationsWithMaxThreads); + mLogger.info("IterationsWithONEThread: " + mIterationsWithOneThread); + mLogger.info("SearchTime: " + mSearchTime + " s"); + mLogger.info("WorkerSetUpTime: " + mWorkerSetUpTime + " s"); + mLogger.info("ExceptionInWorker: " + mExceptionInWorker); + mLogger.info("mRefinementTime: " + mRefinementTime); + } + } + + private boolean isSafeThenTerminate() throws AutomataOperationCanceledException { + // If IsEmpty says its empty, then we can terminate even if threads are still + // running + mLogger.info("Checking if program is safe"); + if (super.isAbstractionEmpty() || mAbstraction.size() == 0) { + mResultBuilder.addResultForAllRemaining(Result.SAFE); + shutDownAndDestroy(mDestroyEverything); + return true; + } + // set cex to null to be certain we dont check counterexamples from the old + // abstraction (super.isAbstractionEmpty() will set mCounterexample) + mCounterexample = null; + return false; + } + + /* + * When we reach this method, we will always start at least one new worker. + */ + private void startWorker() { + mWorkerTaskQueue.add(mCounterexample); + final long time = System.nanoTime() / 1000000000; + mLogger.info("Main: Starting Thread"); + final IcfgLocation currentErrorLoc = getErrorLocFromCounterexample(); + final IUltimateServiceProvider iterationServices = createIterationTimer(currentErrorLoc); + mServices = iterationServices; + mRunningThreads += 1; + mCounterexamplesChecked += 1; + // add mCounterexample to list such that we dont get it twice in our search + addCounterexampleToSet((NestedRun) mCounterexample); + mWorkerSetUpTime += ((System.nanoTime() / 1000000000) - time); + } + + private WorkerThreadResult getWorkerResult(final boolean didntFindCexLastIteration) + throws InterruptedException { + WorkerThreadResult doneFuture = null; + + if (mRunningThreads >= mThreadLimit || didntFindCexLastIteration) { + assert mRunningThreads > 0; + mLogger.info("All threads busy, going to sleep."); + // No busy waiting via BlockingQueue + doneFuture = mWorkerResultQueue.take(); + mLogger.info("Waking up, a worker is done."); + } else { + doneFuture = mWorkerResultQueue.poll(); + } + return doneFuture; + } + + private void shutDownAndDestroy(final Object marker) { + mExec.shutdownNow(); + final Set destroyedStorables = getServices().getStorage().destroyMarker(marker); + if (!destroyedStorables.isEmpty()) { + mLogger.warn("Destroyed unattended storables created during the last iteration: " + + destroyedStorables.stream().collect(Collectors.joining(","))); + } + } + + private void refinement(final WorkerThreadResult threadResult) + throws AutomataOperationCanceledException, AutomataLibraryException { + // mInterations equals the amount of refinements + mCegarLoopBenchmark.announceNextIteration(); + + removeCounterexampleFromSet(threadResult.getCounterexample()); + + final Set hoareAnnotationLocs; + // TODO support for HoareAnnotations + hoareAnnotationLocs = Collections.emptySet(); + + final PredicateFactoryRefinement stateFactoryForRefinement = + new PredicateFactoryRefinement(getServices(), threadResult.getWorkerMgdScript(), + threadResult.getPredicateFactory(), mComputeHoareAnnotation, hoareAnnotationLocs); + mLogger.info("Difference in Main"); + final IOpWithDelayedDeadEndRemoval diff = + computeAutomataDifference(mAbstraction, threadResult, stateFactoryForRefinement); + + mAbstraction = diff.getResult(); + + if (mPref.minimizeAbstractionPerWorker()) { + minimizeAbstractionIfEnabled(stateFactoryForRefinement, + new PredicateFactoryResultChecking(mPredicateFactory)); + } + mRunningThreads -= 1; + mLogger.info("Main: Refinement done."); + } + + /* + * Only add a counterexample if it is being checked by a thread otherwise we are unsound + */ + private void addCounterexampleToSet(final NestedRun counterexample) { + final List trace = counterexample.getWord().asList(); + final int traceHash = trace.hashCode(); + if (mActiveCounterexamples.containsKey(traceHash)) { + throw new AssertionError("IsEmpty(Parallel) Found the same counterexample twice!"); + } + mActiveCounterexamples.put(traceHash, counterexample); + } + + /* + * OnlyActive means only countereamples actively being checked by workers. The alternative is all previously found + * counterexamples. + */ + private void removeCounterexampleFromSet(final IRun cex) { + final List trace = cex.getWord().asList(); + final int traceHash = trace.hashCode(); + mLogger.info("Subtrahend traceHash: " + traceHash); + // Only remove after the counterexample is no longer in the abstraction + if (mPref.considerOnlyActiveCounterexamplesInIsEmptyParallel()) { + mActiveCounterexamples.remove(traceHash); + } else { + if (mCounterexamplesToBeRemovedFromActiveCexMap == null) { + return; + } + mCounterexamplesToBeRemovedFromActiveCexMap.add(traceHash); + } + } + + /* + * The worker usign this method to get the Abstraction need to ensure, they use the @TransferBetweenMainAndWorker To + * transfer the abstraction to their cfgscript. Worker may only use this to read-only access the abstraction! + */ + public INestedWordAutomaton getAbstraction() { + return mAbstraction; + } + + private IsEmpty getSearch(final IsEmpty.SearchStrategy strategy, + final Set possibleEndPoints) throws AutomataOperationCanceledException { + switch (strategy) { + case PARALLEL: + return new IsEmptyParallel<>(new AutomataLibraryServices(mServices), mAbstraction, + mAbstraction.getInitialStates(), Collections.emptySet(), possibleEndPoints, + possibleEndPoints == null, IsEmpty.SearchStrategy.BFS, mActiveCounterexamples, + mPref.getSearchLoopBound()); + default: + return new IsEmpty<>(new AutomataLibraryServices(getServices()), mAbstraction, strategy); + } + } + + // If search was BFS, the counterexample might not be fresh. + private boolean isSearchCorrectAndTraceFresh(final IsEmpty search) { + boolean correct = false; + boolean fresh = true; + try { + correct = search.checkResult(mStateFactoryForRefinement); + } catch (final AutomataLibraryException e) { + e.printStackTrace(); + assert false; + } + + final NestedRun run = search.getNestedRun(); + if (run != null) { + final List trace = run.getWord().asList(); + final int traceHash = trace.hashCode(); + if (mActiveCounterexamples.containsKey(traceHash)) { + fresh = false; + } + return correct && fresh; + } + return false; + } + + /* + * Search for an error trace in the current mAbstraction. First time with a new abstraction we try BFS, then + * IsEmptyParallel + */ + private NestedRun searchForErrorTrace(final boolean onlyDoIsEmptyParallel) + throws AutomataOperationCanceledException { + final long time = System.nanoTime() / 1000000000; + final Set possibleEndPoints = null; + + IsEmpty search; + if (!onlyDoIsEmptyParallel) { + search = getSearch(IsEmpty.SearchStrategy.BFS, possibleEndPoints); + if (isSearchCorrectAndTraceFresh(search)) { + mCountBfsFoundCex += 1; + mLogger.info("Found new Counterexample via BFS!"); + return search.getNestedRun(); + } + } + search = getSearch(IsEmpty.SearchStrategy.PARALLEL, possibleEndPoints); + if (isSearchCorrectAndTraceFresh(search)) { + mLogger.info("Found new Counterexample via IsEmptyParallel!"); + return search.getNestedRun(); + } + mLogger.info("Did not Find a Counterexample!"); + mCountFailedToFindCex += 1; + assert mRunningThreads > 0; + + mSearchTime += ((System.nanoTime() / 1000000000) - time); + return null; + } + + @Override + protected INwaOutgoingLetterAndTransitionProvider enhanceInterpolantAutomaton( + final InterpolantAutomatonEnhancement enhanceMode, final IPredicateUnifier predicateUnifier, + final IHoareTripleChecker htc, final NestedWordAutomaton interpolantAutomaton) { + final INwaOutgoingLetterAndTransitionProvider subtrahend; + // Worker does the enhancement or nobody! + subtrahend = interpolantAutomaton; + return subtrahend; + } + + /* + * Difference is calculated twice first in worker and then in master. All automata obtained from the worker need to + * be transferred to the master cfg script! + */ + private IOpWithDelayedDeadEndRemoval computeAutomataDifference( + final INestedWordAutomaton minuend, final WorkerThreadResult workerResult, + final PredicateFactoryRefinement stateFactoryForRefinement) + throws AutomataLibraryException, AssertionError { + try { + mLogger.debug("Start constructing difference"); + + final PowersetDeterminizer psd = new PowersetDeterminizer<>(workerResult.getSubtrahend(), + true, mPredicateFactoryInterpolantAutomata); + IOpWithDelayedDeadEndRemoval diff; + try { + if (mPref.differenceSenwa()) { + diff = new DifferenceSenwa<>(new AutomataLibraryServices(getServices()), stateFactoryForRefinement, + minuend, workerResult.getSubtrahend(), psd, false); + } else { + diff = new Difference<>(new AutomataLibraryServices(getServices()), stateFactoryForRefinement, + minuend, workerResult.getSubtrahend(), psd, workerResult.exploitSigmaStarConcatOfIa()); + } + mCegarLoopBenchmark.reportInterpolantAutomatonStates(workerResult.getSubtrahend().size()); + + } catch (final AutomataOperationCanceledException | ToolchainCanceledException tce) { + throw tce; + } finally { + // We never enhance in main thread! + } + + if (!workerResult.useErrorAutomaton()) { + // TODO needs to get the worker counterexample + // checkEnhancement(workerResult.getSubtrahendBeforeEnhancement(), + // workerResult.getSubtrahend()); + } + // Future work: + assert !mPref.dumpOnlyReuseAutomata(); + assert mFaultLocalizationMode == RelevanceAnalysisMode.NONE; + + if (REMOVE_DEAD_ENDS) { + diff.removeDeadEnds(); + } + return diff; + } finally { + } + } + + /** + * @param services + * @param filename + */ + private SolverSettings getSolverSettings(final IUltimateServiceProvider services, final String filename) { + + final IPreferenceProvider prefs = mServices.getPreferenceProvider(Activator.PLUGIN_ID); + + final SolverMode solverMode = prefs.getEnum(RcfgPreferenceInitializer.LABEL_SOLVER, SolverMode.class); + + final boolean fakeNonIncrementalScript = + prefs.getBoolean(RcfgPreferenceInitializer.LABEL_FAKE_NON_INCREMENTAL_SCRIPT); + + final boolean dumpSmtScriptToFile = prefs.getBoolean(RcfgPreferenceInitializer.LABEL_DUMP_TO_FILE); + final boolean compressSmtScript = prefs.getBoolean(RcfgPreferenceInitializer.LABEL_COMPRESS_SMT_DUMP_FILE); + final String pathOfDumpedScript = prefs.getString(RcfgPreferenceInitializer.LABEL_DUMP_PATH); + + final String commandExternalSolver = prefs.getString(RcfgPreferenceInitializer.LABEL_EXT_SOLVER_COMMAND); + + final boolean dumpUnsatCoreTrackBenchmark = + prefs.getBoolean(RcfgPreferenceInitializer.LABEL_DUMP_UNSAT_CORE_BENCHMARK); + + final boolean dumpMainTrackBenchmark = + prefs.getBoolean(RcfgPreferenceInitializer.LABEL_DUMP_MAIN_TRACK_BENCHMARK); + + final Map additionalSmtOptions = + prefs.getKeyValueMap(RcfgPreferenceInitializer.LABEL_ADDITIONAL_SMT_OPTIONS); + + final Logics logicForExternalSolver = + Logics.valueOf(prefs.getString(RcfgPreferenceInitializer.LABEL_EXT_SOLVER_LOGIC)); + final SolverSettings solverSettings = + SolverBuilder.constructSolverSettings().setUseFakeIncrementalScript(fakeNonIncrementalScript) + .setDumpSmtScriptToFile(dumpSmtScriptToFile, pathOfDumpedScript, filename, compressSmtScript) + .setDumpUnsatCoreTrackBenchmark(dumpUnsatCoreTrackBenchmark) + .setDumpMainTrackBenchmark(dumpMainTrackBenchmark) + .setUseExternalSolver(true, commandExternalSolver, logicForExternalSolver) + .setSolverMode(solverMode).setAdditionalOptions(additionalSmtOptions); + + return solverSettings; + } + + private void minimizeAbstractionIfEnabled(final PredicateFactoryRefinement stateFactoryForRefinement, + final PredicateFactoryResultChecking predicateFactoryResultChecking) + throws AutomataOperationCanceledException, AutomataLibraryException, AssertionError { + final Minimization minimization = mPref.getMinimization(); + switch (minimization) { + case NONE: + // do not apply minimization + break; + case DFA_HOPCROFT_LISTS: + case DFA_HOPCROFT_ARRAYS: + case MINIMIZE_SEVPA: + case SHRINK_NWA: + case NWA_MAX_SAT: + case NWA_MAX_SAT2: + case RAQ_DIRECT_SIMULATION: + case RAQ_DIRECT_SIMULATION_B: + case NWA_COMBINATOR_PATTERN: + case NWA_COMBINATOR_EVERY_KTH: + case NWA_OVERAPPROXIMATION: + case NWA_COMBINATOR_MULTI_DEFAULT: + case NWA_COMBINATOR_MULTI_SIMULATION: + // apply minimization + minimizeAbstraction(stateFactoryForRefinement, predicateFactoryResultChecking, minimization); + break; + default: + throw new AssertionError(); + } + } + + /** + * Automata theoretic minimization of the automaton stored in mAbstraction. Expects that mAbstraction does not have + * dead ends. + * + * @param predicateFactoryRefinement + * PredicateFactory for the construction of the new (minimized) abstraction. + * @param resultCheckPredFac + * PredicateFactory used for auxiliary automata used for checking correctness of the result (if + * assertions are enabled). + */ + @Override + protected void minimizeAbstraction(final PredicateFactoryRefinement predicateFactoryRefinement, + final PredicateFactoryResultChecking resultCheckPredFac, final Minimization minimization) + throws AutomataOperationCanceledException, AutomataLibraryException, AssertionError { + + final Function> lcsProvider = + x -> (x instanceof ISLPredicate ? Collections.singleton(((ISLPredicate) x).getProgramPoint()) + : new HashSet<>(Arrays.asList(((IMLPredicate) x).getProgramPoints()))); + AutomataMinimization, IPredicate, L> am; + try { + am = new AutomataMinimization<>(getServices(), mAbstraction, minimization, mComputeHoareAnnotation, + getIteration(), predicateFactoryRefinement, MINIMIZE_EVERY_KTH_ITERATION, + mStoredRawInterpolantAutomata, mInterpolAutomaton, MINIMIZATION_TIMEOUT, resultCheckPredFac, + lcsProvider, true); + } catch (final AutomataMinimizationTimeout e) { + mCegarLoopBenchmark.addAutomataMinimizationData(e.getStatistics()); + throw e.getAutomataOperationCanceledException(); + } + mCegarLoopBenchmark.addAutomataMinimizationData(am.getStatistics()); + final boolean newAutomatonWasBuilt = am.newAutomatonWasBuilt(); + + if (newAutomatonWasBuilt) { + // postprocessing after minimization + final IDoubleDeckerAutomaton newAbstraction = am.getMinimizedAutomaton(); + + // extract Hoare annotation + if (mComputeHoareAnnotation) { + final Map oldState2newState = am.getOldState2newStateMapping(); + if (oldState2newState == null) { + throw new AssertionError("Hoare annotation and " + minimization + " incompatible"); + } + } + + // statistics + final int oldSize = mAbstraction.size(); + final int newSize = newAbstraction.size(); + assert oldSize == 0 || oldSize >= newSize : "Minimization increased state space"; + + // use result + mAbstraction = newAbstraction; + } + } + + public PathProgramCache getCurrentProgramCache() { + return mProgramCache; + } + + public void reportFailedContinuesWorkerThread() { + final IcfgLocation currentErrorLoc = getErrorLocFromCounterexample(); + final IUltimateServiceProvider iterationServices = createIterationTimer(currentErrorLoc); + try { + setUpContinuesWorker(iterationServices, 0); + } catch (final InterruptedException e) { + e.printStackTrace(); + } + } + + public ManagedScript getManagedScript() { + return mCsToolkit.getManagedScript(); + } +} diff --git a/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/PathProgramCache.java b/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/PathProgramCache.java index 680d6347a0f..880217e6eb1 100644 --- a/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/PathProgramCache.java +++ b/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/PathProgramCache.java @@ -29,11 +29,11 @@ import java.util.ArrayList; import java.util.Arrays; import java.util.Collections; -import java.util.HashMap; import java.util.HashSet; import java.util.List; import java.util.Map; import java.util.Set; +import java.util.concurrent.ConcurrentHashMap; import de.uni_freiburg.informatik.ultimate.automata.Word; import de.uni_freiburg.informatik.ultimate.core.model.services.ILogger; @@ -53,8 +53,8 @@ public class PathProgramCache { public PathProgramCache(final ILogger logger) { mLogger = logger; - mKnownPathPrograms = new HashMap<>(); - mTraceHashes = new ArrayList<>(); + mKnownPathPrograms = new ConcurrentHashMap<>(); + mTraceHashes = Collections.synchronizedList(new ArrayList<>()); } /** diff --git a/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/TransferBetweenMainAndWorker.java b/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/TransferBetweenMainAndWorker.java new file mode 100644 index 00000000000..47b6bce6048 --- /dev/null +++ b/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/TransferBetweenMainAndWorker.java @@ -0,0 +1,547 @@ +/* + * Copyright (C) 2025 University of Freiburg + * Copyright (C) 2025 LMU Munich + * Copyright (C) 2025 Max Barth (Max.Barth@lmu.de) + * + * This file is part of the ULTIMATE Automata Library. + * + * The ULTIMATE Automata Library is free software: you can redistribute it and/or modify + * it under the terms of the GNU Lesser General Public License as published + * by the Free Software Foundation, either version 3 of the License, or + * (at your option) any later version. + * + * The ULTIMATE Automata Library is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU Lesser General Public License for more details. + * + * You should have received a copy of the GNU Lesser General Public License + * along with the ULTIMATE Automata Library. If not, see . + * + * Additional permission under GNU GPL version 3 section 7: + * If you modify the ULTIMATE Automata Library, or any covered work, by linking + * or combining it with Eclipse RCP (or a modified version of Eclipse RCP), + * containing parts covered by the terms of the Eclipse Public License, the + * licensors of the ULTIMATE Automata Library grant you additional permission + * to convey the resulting work. + */ +package de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction; + +import java.util.ArrayDeque; +import java.util.Collections; +import java.util.HashMap; +import java.util.HashSet; +import java.util.List; +import java.util.Map; +import java.util.Map.Entry; +import java.util.Set; +import java.util.stream.Collectors; + +import de.uni_freiburg.informatik.ultimate.automata.AutomataLibraryServices; +import de.uni_freiburg.informatik.ultimate.automata.IRun; +import de.uni_freiburg.informatik.ultimate.automata.nestedword.INwaOutgoingLetterAndTransitionProvider; +import de.uni_freiburg.informatik.ultimate.automata.nestedword.NestedRun; +import de.uni_freiburg.informatik.ultimate.automata.nestedword.NestedWord; +import de.uni_freiburg.informatik.ultimate.automata.nestedword.NestedWordAutomaton; +import de.uni_freiburg.informatik.ultimate.automata.nestedword.VpAlphabet; +import de.uni_freiburg.informatik.ultimate.automata.nestedword.transitions.OutgoingCallTransition; +import de.uni_freiburg.informatik.ultimate.automata.nestedword.transitions.OutgoingInternalTransition; +import de.uni_freiburg.informatik.ultimate.automata.nestedword.transitions.OutgoingReturnTransition; +import de.uni_freiburg.informatik.ultimate.automata.statefactory.IEmptyStackStateFactory; +import de.uni_freiburg.informatik.ultimate.core.model.services.ILogger; +import de.uni_freiburg.informatik.ultimate.core.model.services.IUltimateServiceProvider; +import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.CfgSmtToolkit; +import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.DefaultIcfgSymbolTable; +import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.IIcfgSymbolTable; +import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.ModifiableGlobalsTable; +import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.SmtFunctionsAndAxioms; +import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.transitions.TransFormulaBuilder; +import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.transitions.UnmodifiableTransFormula; +import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.variables.ILocalProgramVar; +import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.variables.IProgramConst; +import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.variables.IProgramFunction; +import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.variables.IProgramNonOldVar; +import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.variables.IProgramOldVar; +import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.variables.IProgramVar; +import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.variables.LocalProgramVar; +import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.variables.ProgramConst; +import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.variables.ProgramNonOldVar; +import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.variables.ProgramVarUtils; +import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.smt.predicates.BasicPredicate; +import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.smt.predicates.IPredicate; +import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.smt.scripttransfer.TermTransferrer; +import de.uni_freiburg.informatik.ultimate.lib.smtlibutils.ManagedScript; +import de.uni_freiburg.informatik.ultimate.lib.smtlibutils.solverbuilder.SolverBuilder.SolverSettings; +import de.uni_freiburg.informatik.ultimate.logic.ApplicationTerm; +import de.uni_freiburg.informatik.ultimate.logic.Term; +import de.uni_freiburg.informatik.ultimate.logic.TermVariable; +import de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder.cfg.BoogieIcfgLocation; +import de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder.cfg.Call; +import de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder.cfg.Return; +import de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder.cfg.StatementSequence; +import de.uni_freiburg.informatik.ultimate.util.ConstructionCache; +import de.uni_freiburg.informatik.ultimate.util.ConstructionCache.IValueConstruction; +import de.uni_freiburg.informatik.ultimate.util.datastructures.relation.HashRelation; + +public class TransferBetweenMainAndWorker { + + private final ILogger mLogger; + private final ManagedScript mMainScript; + private final ManagedScript mWorkerScript; + private final HashMap mEdgeCache = new HashMap<>(); // Bidirectional + private final HashMap mProgramVarBackTranslationCache = new HashMap<>(); // Maps worker -> + // main + private final AutomataLibraryServices mServices; + private final TermTransferrer mWorker2main; + private final TermTransferrer mMain2worker; + private VpAlphabet mMainVpAlphabet; + private final CfgSmtToolkit mMainCsToolkit; + private final VariableTransferrer mVarTransfer; + + enum Mode { + NONE, MAIN2WORKER, WORKER2MAIN + } + + private Mode mMode = Mode.NONE; + + /** + * A class used to transfer runs / cex and automata between worker and main scripts. Also used to create the worker + * CfgToolKit. Every creation of worker IProgramVars should run through this classes @VariableTransferrer + * + * On initialization this classes creates the workers ManagedScript. And the necessary TermTransferrer + * + * @param main + * @param worker + * @param mainCfgToolKit + * + * @author Max Barth (max.barth@lmu.de) + */ + public TransferBetweenMainAndWorker(final AutomataLibraryServices services, final ILogger logger, + final ManagedScript main, final IUltimateServiceProvider solverServices, + final SolverSettings solverSettings, final CfgSmtToolkit mainCfgToolKit) { + mLogger = logger; + mMainScript = main; + mWorkerScript = mainCfgToolKit.createFreshManagedScript(solverServices, solverSettings); + mServices = services; + mMainCsToolkit = mainCfgToolKit; + + mWorker2main = new TermTransferrer(mWorkerScript.getScript(), mMainScript.getScript()); + mMain2worker = new TermTransferrer(mMainScript.getScript(), mWorkerScript.getScript()); + mVarTransfer = new VariableTransferrer(mMain2worker, mWorkerScript); + } + + /* + * Gets a run / counterexample with Letters whose transformula comes from one script. Returns a new run with new + * letters, whose transformula comes from target script. The semantics of both runs are equal. + */ + public IRun transferRun(final NestedRun counterexample, final Mode mode) { + final NestedRun oldCounterexample = counterexample; + mMode = mode; + NestedWord currentWord = new NestedWord<>(); + for (int i = 0; i < oldCounterexample.getWord().length(); i++) { + final LETTER letter = oldCounterexample.getWord().asList().get(i); + int nestingOperation = NestedWord.INTERNAL_POSITION; + switch (letter) { + case final Call call -> nestingOperation = NestedWord.PLUS_INFINITY; + case final Return re -> nestingOperation = NestedWord.MINUS_INFINITY; + case final StatementSequence stmt -> nestingOperation = NestedWord.INTERNAL_POSITION; + default -> new AssertionError("Unexpected letter type: " + letter.getClass()); + } + final NestedWord singleWord = new NestedWord<>(transferEdge(letter), nestingOperation); + currentWord = currentWord.concatenate(singleWord); + + } + + final NestedRun workerCounterexample = + new NestedRun<>(currentWord, oldCounterexample.getStateSequence()); + return workerCounterexample; + } + + // Caches every transferred Edge bidirectional + private LETTER transferEdge(final LETTER letter) { + LETTER transferredLetter = null; + if (mEdgeCache.containsKey(letter)) { + transferredLetter = mEdgeCache.get(letter); + } else { + switch (letter) { + case final Call call -> transferredLetter = (LETTER) getTransferCall(call); + case final Return re -> transferredLetter = (LETTER) getTransferReturn(re); + case final StatementSequence stmt -> transferredLetter = (LETTER) getTransferStmtSequence(stmt); + default -> new AssertionError("Unexpected letter type: " + letter.getClass()); + } + } + assert transferredLetter != null; + mEdgeCache.put(letter, transferredLetter); + mEdgeCache.put(transferredLetter, letter); + return transferredLetter; + } + + private Call getTransferCall(final Call call) { + final Call newCall = new Call(call.getSerialNumber(), (BoogieIcfgLocation) call.getSource(), + (BoogieIcfgLocation) call.getTarget(), call.getCallStatement(), mLogger); + newCall.setTransitionFormula(transferTransFormulaWithMode(call.getTransformula())); + newCall.setPayload(call.getPayload()); // Payload is need for for example Overaprixmation Annotations + return newCall; + } + + private StatementSequence getTransferStmtSequence(final StatementSequence stmt) { + final StatementSequence newStmt = + new StatementSequence(stmt.getSerialNumber(), (BoogieIcfgLocation) stmt.getSource(), + (BoogieIcfgLocation) stmt.getTarget(), stmt.getStatements(), mLogger); + newStmt.setTransitionFormula(transferTransFormulaWithMode(stmt.getTransformula())); + newStmt.setPayload(stmt.getPayload()); + return newStmt; + + } + + private Return getTransferReturn(final Return re) { + final Return newReturn = new Return(re.getSerialNumber(), (BoogieIcfgLocation) re.getSource(), + (BoogieIcfgLocation) re.getTarget(), getTransferCall(re.getCorrespondingCall()), mLogger); + newReturn.setTransitionFormula(transferTransFormulaWithMode(re.getTransformula())); + newReturn.setPayload(re.getPayload()); + return newReturn; + + } + + private UnmodifiableTransFormula transferTransFormulaWithMode(final UnmodifiableTransFormula inTF) { + switch (mMode) { + case MAIN2WORKER: { + return transferTransformula(inTF, mMain2worker, mWorkerScript); + } + case WORKER2MAIN: { + return transferTransformula(inTF, mWorker2main, mMainScript); + } + default: { + throw new AssertionError("Unexpected transferrer mode: " + mMode); + } + } + } + + private UnmodifiableTransFormula transferTransformula(final UnmodifiableTransFormula inTF, + final TermTransferrer transferrer, final ManagedScript targetScript) { + + final TransFormulaBuilder transferredTF = new TransFormulaBuilder(transferMap(transferrer, inTF.getInVars()), + transferMap(transferrer, inTF.getOutVars()), inTF.getNonTheoryConsts().isEmpty(), + inTF.getNonTheoryConsts(), inTF.getBranchEncoders().isEmpty(), + transferSet(transferrer, inTF.getBranchEncoders()), inTF.getAuxVars().isEmpty()); + assert inTF.getNonTheoryConsts().isEmpty(); + transferredTF.setFormula(transferrer.transform(inTF.getFormula())); + + transferredTF.addAuxVarsButRenameToFreshCopies(transferSet(transferrer, inTF.getAuxVars()), targetScript); + + transferredTF.setInfeasibility(inTF.isInfeasible()); + return transferredTF.finishConstruction(targetScript); + + } + + private Map transferMap(final TermTransferrer transferrer, + final Map map) { + final Map transferredMap = new HashMap<>(); + for (final Entry entry : map.entrySet()) { + IProgramVar transferredProgramVar; + if (!mProgramVarBackTranslationCache.containsKey(entry.getKey())) { + assert mMode.equals(Mode.MAIN2WORKER); + switch (entry.getKey()) { + case final ProgramNonOldVar var -> { + transferredProgramVar = mVarTransfer.translateProgramVar(var); + break; + } + case final LocalProgramVar var -> { + transferredProgramVar = mVarTransfer.translateProgramVar(var); + break; + } + default -> throw new AssertionError("Unexpected type of BoogieVar: " + entry.getKey().getClass()); + } + mProgramVarBackTranslationCache.put(transferredProgramVar, entry.getKey()); + } else { + transferredProgramVar = mProgramVarBackTranslationCache.get(entry.getKey()); + } + assert transferredProgramVar != null; + transferredMap.put(transferredProgramVar, (TermVariable) transferrer.transform(entry.getValue())); + } + return transferredMap; + } + + public static Set transferSet(final TermTransferrer transferrer, final Set inputSet) { + final Set outSet = new HashSet<>(); + for (final TermVariable var : inputSet) { + outSet.add((TermVariable) transferrer.transform(var)); + } + return outSet; + } + + /** + * This method gets an @INwaOutgoingLetterAndTransitionProvider and returns + * an @INwaOutgoingLetterAndTransitionProvider + * + * Thereby, it explores the input automaton and creates the output automaton. States remain the same, Letters are + * transferred from one script to another depending on the @mode. The new automaton has a new Alphabet, and can have + * less transitions than the input automaton. TODO check if this can really be sound + */ + public INwaOutgoingLetterAndTransitionProvider transferAutomaton( + final INwaOutgoingLetterAndTransitionProvider automaton, + final IEmptyStackStateFactory emptyStateFactory, final Mode mode) { + + VpAlphabet alphabet; + Set internalAlphabet; + Set callAlphabet; + Set returnAlphabet; + mMode = mode; + switch (mMode) { + case MAIN2WORKER: { + internalAlphabet = new HashSet<>(); + callAlphabet = new HashSet<>(); + returnAlphabet = new HashSet<>(); + mMainVpAlphabet = automaton.getVpAlphabet(); + alphabet = new VpAlphabet<>(internalAlphabet, callAlphabet, returnAlphabet); + break; + } + case WORKER2MAIN: { + internalAlphabet = mMainVpAlphabet.getInternalAlphabet(); + callAlphabet = mMainVpAlphabet.getCallAlphabet(); + returnAlphabet = mMainVpAlphabet.getReturnAlphabet(); + alphabet = new VpAlphabet<>(internalAlphabet, callAlphabet, returnAlphabet); + break; + } + default: { + throw new AssertionError("Unexpected transferrer mode: " + mMode); + } + } + + final NestedWordAutomaton result = + new NestedWordAutomaton<>(mServices, alphabet, emptyStateFactory); + + final Set hierPredStates = new HashSet<>(); + hierPredStates.add(automaton.getEmptyStackState()); + final Set allStates = new HashSet<>(); + + final Set initialStates = new HashSet<>(); + automaton.getInitialStates().forEach(initialStates::add); + final ArrayDeque dequeue = new ArrayDeque<>(initialStates); + + final Set visited = new HashSet<>(); + while (!dequeue.isEmpty()) { + final STATE state = dequeue.pop(); + + if (!visited.add(state)) { + continue; + } + if (!result.contains(state)) { + allStates.add(state); + result.addState(automaton.isInitial(state), automaton.isFinal(state), state); + } + + for (final OutgoingCallTransition transition : automaton.callSuccessors(state)) { + final STATE succesor = transition.getSucc(); + if (!result.contains(succesor)) { + allStates.add(succesor); + result.addState(automaton.isInitial(succesor), automaton.isFinal(succesor), succesor); + } + final LETTER transferredLetter = transferEdge(transition.getLetter()); + callAlphabet.add(transferredLetter); + result.addCallTransition(state, transferredLetter, succesor); + hierPredStates.add(state); + dequeue.add(succesor); + } + for (final OutgoingInternalTransition transition : automaton.internalSuccessors(state)) { + final STATE succesor = transition.getSucc(); + if (!result.contains(succesor)) { + allStates.add(succesor); + result.addState(automaton.isInitial(succesor), automaton.isFinal(succesor), succesor); + } + final LETTER transferredLetter = transferEdge(transition.getLetter()); + internalAlphabet.add(transferredLetter); + result.addInternalTransition(state, transferredLetter, succesor); + dequeue.add(succesor); + } + final Set copyAllStates = new HashSet<>(allStates); + for (final STATE potentialhier : copyAllStates) { + for (final STATE hierPred : hierPredStates) { + for (final OutgoingReturnTransition returnTransition : automaton + .returnSuccessorsGivenHier(potentialhier, hierPred)) { + + final STATE succesor = returnTransition.getSucc(); + final STATE hier = returnTransition.getHierPred(); + if (!result.contains(succesor)) { + allStates.add(succesor); + result.addState(automaton.isInitial(succesor), automaton.isFinal(succesor), succesor); + } + if (!result.contains(hier)) { + allStates.add(hier); + result.addState(automaton.isInitial(hier), automaton.isFinal(hier), hier); + } + final LETTER transferredLetter = transferEdge(returnTransition.getLetter()); + returnAlphabet.add(transferredLetter); + result.addReturnTransition(potentialhier, hier, transferredLetter, succesor); + dequeue.add(succesor); + } + } + } + // TODO transfer summaries, so far they are ignored because i dont know how to detect a summary in the input + } + assert result.size() == automaton.size(); + return result; + + } + + public CfgSmtToolkit constructWorkerCfgSmtToolkit() { + final HashRelation proc2globals = + constructNewProc2Globals(mMainCsToolkit.getModifiableGlobalsTable().getProcToGlobals(), mVarTransfer); + final ModifiableGlobalsTable modifiableGlobalsTable = new ModifiableGlobalsTable(proc2globals); + final IIcfgSymbolTable symbolTable = + constructNewSymbolTable(mMainCsToolkit.getSymbolTable(), mMainCsToolkit.getProcedures(), mVarTransfer); + final Map> inParams = + constructNewParams(mMainCsToolkit.getInParams(), mVarTransfer); + final Map> outParams = + constructNewParams(mMainCsToolkit.getOutParams(), mVarTransfer); + + final IPredicate mainAxioms = mMainCsToolkit.getSmtFunctionsAndAxioms().getAxioms(); + final Set vars = new HashSet<>(); + for (final IProgramVar var : mainAxioms.getVars()) { + vars.add(mVarTransfer.translateProgramVar(var)); + } + final Set funs = new HashSet<>(); + for (final IProgramFunction fun : mainAxioms.getFuns()) { + // TODO what is a IProgramFunction? Does this do the trick? + funs.add(mVarTransfer.getOrConstruct((IProgramConst) fun)); + } + final IPredicate newAxiomsPred = new BasicPredicate(0, mMain2worker.transform(mainAxioms.getFormula()), vars, + funs, mMain2worker.transform(mainAxioms.getClosedFormula())); + final SmtFunctionsAndAxioms smtFunctionsAndAxioms = new SmtFunctionsAndAxioms(newAxiomsPred, mWorkerScript); + return new CfgSmtToolkit(modifiableGlobalsTable, mWorkerScript, symbolTable, mMainCsToolkit.getProcedures(), + inParams, outParams, mMainCsToolkit.getIcfgEdgeFactory(), mMainCsToolkit.getConcurrencyInformation(), + smtFunctionsAndAxioms); + } + + private static Map> constructNewParams( + final Map> inParams, final VariableTransferrer variableTranslation) { + final Map> result = new HashMap<>(); + for (final Entry> entry : inParams.entrySet()) { + final List newList = entry.getValue().stream() + .map(x -> variableTranslation.getOrConstruct(x)).collect(Collectors.toList()); + result.put(entry.getKey(), newList); + } + return result; + } + + private static IIcfgSymbolTable constructNewSymbolTable(final IIcfgSymbolTable symbolTable, + final Set procedures, final VariableTransferrer varTrans) { + final DefaultIcfgSymbolTable result = new DefaultIcfgSymbolTable(); + for (final IProgramConst c : symbolTable.getConstants()) { + result.add(varTrans.getOrConstruct(c)); + } + for (final IProgramNonOldVar g : symbolTable.getGlobals()) { + result.add(varTrans.getOrConstruct(g)); + } + for (final String proc : procedures) { + for (final ILocalProgramVar l : symbolTable.getLocals(proc)) { + result.add(varTrans.getOrConstruct(l)); + } + } + return result; + } + + private static HashRelation constructNewProc2Globals( + final HashRelation procToGlobals, + final VariableTransferrer variableTranslation) { + final HashRelation result = new HashRelation<>(); + for (final Entry> entry : procToGlobals.entrySet()) { + for (final IProgramNonOldVar old : entry.getValue()) { + final IProgramNonOldVar newVar = variableTranslation.getOrConstruct(old); + result.addPair(entry.getKey(), newVar); + } + } + return result; + } + +} + +class VariableTransferrer { + private final ConstructionCache mILocalProgramVarCC; + private final ConstructionCache mIProgramNonOldVarCC; + private final ConstructionCache mIProgramConstCC; + + public VariableTransferrer(final TermTransferrer transferrer, final ManagedScript targetScript) { + mILocalProgramVarCC = new ConstructionCache<>(new IValueConstruction() { + + @Override + public ILocalProgramVar constructValue(final ILocalProgramVar oldPv) { + targetScript.lock(this); + final ILocalProgramVar newPv = + (ILocalProgramVar) ProgramVarUtils.transferProgramVar(transferrer, oldPv); + targetScript.unlock(this); + return newPv; + } + }); + mIProgramNonOldVarCC = new ConstructionCache<>(new IValueConstruction() { + + @Override + public IProgramNonOldVar constructValue(final IProgramNonOldVar oldPv) { + targetScript.lock(this); + final IProgramNonOldVar newPv = + (IProgramNonOldVar) ProgramVarUtils.transferProgramVar(transferrer, oldPv); + targetScript.unlock(this); + return newPv; + } + + }); + mIProgramConstCC = new ConstructionCache<>(oldPv -> { + final String newIdentifier = oldPv.getIdentifier(); + final ApplicationTerm newSmtConstant = (ApplicationTerm) transferrer.transform(oldPv.getDefaultConstant()); + return new ProgramConst(newIdentifier, newSmtConstant, false); + }); + } + + public ILocalProgramVar getOrConstruct(final ILocalProgramVar key) { + return mILocalProgramVarCC.getOrConstruct(key); + } + + public IProgramNonOldVar getOrConstruct(final IProgramNonOldVar key) { + return mIProgramNonOldVarCC.getOrConstruct(key); + } + + public IProgramOldVar getOrConstruct(final IProgramOldVar key) { + return mIProgramNonOldVarCC.getOrConstruct(key.getNonOldVar()).getOldVar(); + } + + public IProgramConst getOrConstruct(final IProgramConst key) { + return mIProgramConstCC.getOrConstruct(key); + } + + public Map getILocalProgramVarMap() { + return Collections.unmodifiableMap(mILocalProgramVarCC); + } + + public Map getIProgramNonOldVarMap() { + return Collections.unmodifiableMap(mIProgramNonOldVarCC); + } + + public Map getIProgramConstMap() { + return Collections.unmodifiableMap(mIProgramConstCC); + } + + public Map getIProgramConstTermMap() { + return getIProgramConstMap().entrySet().stream().collect( + Collectors.toMap(x -> x.getKey().getDefaultConstant(), x -> x.getValue().getDefaultConstant())); + } + + public IProgramVar translateProgramVar(final IProgramVar pv) { + IProgramVar result; + if (pv instanceof ILocalProgramVar) { + result = getILocalProgramVarMap().get(pv); + } else if (pv instanceof IProgramNonOldVar) { + result = getIProgramNonOldVarMap().get(pv); + } else if (pv instanceof IProgramOldVar) { + result = getIProgramNonOldVarMap().get(((IProgramOldVar) pv).getNonOldVar()).getOldVar(); + } else { + throw new UnsupportedOperationException(pv.getClass().getSimpleName()); + } + assert result != null; + return result; + } + + public IProgramConst translateProgramConst(final IProgramConst pc) { + return getIProgramConstMap().get(pc); + } + +} \ No newline at end of file diff --git a/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/WorkerThreadResult.java b/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/WorkerThreadResult.java new file mode 100644 index 00000000000..d1b3075dc2b --- /dev/null +++ b/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/WorkerThreadResult.java @@ -0,0 +1,99 @@ +package de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction; + +import de.uni_freiburg.informatik.ultimate.automata.IAutomaton; +import de.uni_freiburg.informatik.ultimate.automata.IRun; +import de.uni_freiburg.informatik.ultimate.automata.nestedword.INwaOutgoingLetterAndTransitionProvider; +import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.structure.IIcfgTransition; +import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.smt.predicates.IPredicate; +import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.smt.predicates.IPredicateUnifier; +import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.smt.predicates.PredicateFactory; +import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.tracehandling.IIpTcStrategyModule; +import de.uni_freiburg.informatik.ultimate.lib.smtlibutils.ManagedScript; +import de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.NwaCegarLoop.AutomatonType; +import de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.preferences.TAPreferences.InterpolantAutomatonEnhancement; + +final class WorkerThreadResult, A extends IAutomaton> { + + private INwaOutgoingLetterAndTransitionProvider mSubtrahend; + private AutomatonType mAutomatonType; + private final boolean mUseErrorAutomaton; + private INwaOutgoingLetterAndTransitionProvider mSubtrahendBeforeEnhancement; + private InterpolantAutomatonEnhancement mEnhanceMode; + private final boolean mExploitSigmaStarConcatOfIa; + private ManagedScript mMgdScript; + private IRun mCounterexample; + PredicateFactory mPredicateFactory; + private final boolean mWorkerCrashed; + + /** + * The object returned by an @ICegarNwaWorkerThread + * + */ + WorkerThreadResult(final INwaOutgoingLetterAndTransitionProvider subtrahend, + final INwaOutgoingLetterAndTransitionProvider subtrahendBeforeEnhancement, + final IPredicateUnifier predicateUnifier, final boolean explointSigmaStarConcatOfIA, + final InterpolantAutomatonEnhancement enhanceMode, final boolean useErrorAutomaton, + final AutomatonType automatonType, final ManagedScript mgdScript, final IRun counterexample, + final PredicateFactory predicateFactory, final boolean workerCrashed) { + mSubtrahend = subtrahend; + mAutomatonType = automatonType; + mUseErrorAutomaton = useErrorAutomaton; + mEnhanceMode = enhanceMode; + mSubtrahendBeforeEnhancement = subtrahendBeforeEnhancement; + mExploitSigmaStarConcatOfIa = explointSigmaStarConcatOfIA; + mMgdScript = mgdScript; + mCounterexample = counterexample; + mPredicateFactory = predicateFactory; + mWorkerCrashed = workerCrashed; + } + + public boolean workerCrashed() { + return mWorkerCrashed; + } + + public PredicateFactory getPredicateFactory() { + return mPredicateFactory; + } + + public InterpolantAutomatonEnhancement getEnhanceMode() { + return mEnhanceMode; + } + + public INwaOutgoingLetterAndTransitionProvider getSubtrahend() { + return mSubtrahend; + } + + public AutomatonType getAutomatonType() { + return mAutomatonType; + } + + public boolean useErrorAutomaton() { + return mUseErrorAutomaton; + } + + public INwaOutgoingLetterAndTransitionProvider getSubtrahendBeforeEnhancement() { + return mSubtrahendBeforeEnhancement; + } + + public boolean exploitSigmaStarConcatOfIa() { + return mExploitSigmaStarConcatOfIa; + } + + public ManagedScript getWorkerMgdScript() { + return mMgdScript; + } + + public IRun getCounterexample() { + return mCounterexample; + } + + public void garbageCollect() { + mSubtrahend = null; + mAutomatonType = null; + mEnhanceMode = null; + mSubtrahendBeforeEnhancement = null; + mMgdScript = null; + mCounterexample = null; + mPredicateFactory = null; + } +} \ No newline at end of file diff --git a/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/preferences/TAPreferences.java b/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/preferences/TAPreferences.java index 1db45447d4d..5c54e95cb34 100644 --- a/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/preferences/TAPreferences.java +++ b/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/preferences/TAPreferences.java @@ -96,6 +96,13 @@ public final class TAPreferences { private final IndependenceSettings[] mPorIndependenceSettings; private final IndependenceSettings mLbeIndependenceSettings; + // Parallel Trace Abstraction Settings + private final int mThreadLimit; + private final boolean mParallelCegarLoop; + private final boolean mConsiderOnlyActiveCounterexamplesInIsEmptyParallel; + private final boolean mMinimizeAbstractionPerWorker; + private final int mSearchLoopBound; + public enum Artifact { ABSTRACTION, INTERPOLANT_AUTOMATON, NEG_INTERPOLANT_AUTOMATON, RCFG } @@ -198,6 +205,14 @@ public TAPreferences(final IUltimateServiceProvider services) { mPrefs.getBoolean(TraceAbstractionPreferenceInitializer.LABEL_SEMICOMM_PLBE), IndependenceSettings.DEFAULT_SOLVER /* currently ignored; not exposed as setting */, IndependenceSettings.DEFAULT_SOLVER_TIMEOUT /* currently ignored; not exposed as setting */); + + mParallelCegarLoop = mPrefs.getBoolean(TraceAbstractionPreferenceInitializer.LABEL_PARALLEL_CEGAR_LOOP); + mThreadLimit = mPrefs.getInt(TraceAbstractionPreferenceInitializer.LABEL_THREADLIMIT); + mConsiderOnlyActiveCounterexamplesInIsEmptyParallel = + mPrefs.getBoolean(TraceAbstractionPreferenceInitializer.LABEL_PARALLELSEARCH_ACTIVE_CEX_ONLY); + mMinimizeAbstractionPerWorker = + mPrefs.getBoolean(TraceAbstractionPreferenceInitializer.LABEL_MINIMIZE_ABSTRACTION_PER_WORKER); + mSearchLoopBound = mPrefs.getInt(TraceAbstractionPreferenceInitializer.LABEL_SEARCH_LOOP_BOUND); } /** @@ -566,4 +581,24 @@ public RefinementStrategy getConditionalCommutativityRefinementStrategy() { public HoareProofSettings getHoareSettings() { return new HoareProofSettings(getHoareAnnotationPositions(), getSimplificationTechnique()); } + + public int getThreadLimit() { + return mThreadLimit; + } + + public boolean isParallelCegarLoop() { + return mParallelCegarLoop; + } + + public boolean minimizeAbstractionPerWorker() { + return mMinimizeAbstractionPerWorker; + } + + public boolean considerOnlyActiveCounterexamplesInIsEmptyParallel() { + return mConsiderOnlyActiveCounterexamplesInIsEmptyParallel; + } + + public int getSearchLoopBound() { + return mSearchLoopBound; + } } diff --git a/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/preferences/TraceAbstractionPreferenceInitializer.java b/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/preferences/TraceAbstractionPreferenceInitializer.java index d495ab140c0..7446ffd6183 100644 --- a/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/preferences/TraceAbstractionPreferenceInitializer.java +++ b/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/preferences/TraceAbstractionPreferenceInitializer.java @@ -512,6 +512,24 @@ public enum CoinflipMode { private static final String DESC_ASSERT_CODEBLOCKS_HEURISTIC_SCORE_THRESHOLD = "If Assert CodeBlocks is set to SMT_FEATURE_HEURISTIC and partitioning strategy is THRESHOLD, two partitions are created, one partition contains all terms >= threshold and one all terms < threshold"; + // Parallel Trace Abstraction + // ======================================================================== + public static final String LABEL_PARALLEL_CEGAR_LOOP = "Use CEGAR loop for Parallel Trace Abstraction"; + private static final boolean DEF_PARALLEL_CEGAR_LOOP = false; + + public static final String LABEL_THREADLIMIT = "Threadlimit for Parallel CEGAR"; + private static final Integer DEF_THREADLIMIT = 1; + + public static final String LABEL_MINIMIZE_ABSTRACTION_PER_WORKER = + "Minimize Abstraction every time a worker is done"; + private static final boolean DEF_MINIMIZE_ABSTRACTION_PER_WORKER = true; + // Parallel CEGAR counterexample search stragies + // ======================================================================== + public static final String LABEL_PARALLELSEARCH_ACTIVE_CEX_ONLY = "Consider only active in Search Strategy"; + private static final boolean DEF_PARALLELSEARCH_ACTIVE_CEX_ONLY = false; + public static final String LABEL_SEARCH_LOOP_BOUND = "search loop bound"; + private static final int DEF_SEARCH_LOOP_BOUND = -1; + /** * Constructor. */ @@ -697,7 +715,7 @@ protected BaseUltimatePreferenceItem[] initDefaultPreferences() { new UltimatePreferenceItem<>(LABEL_DUMP_PATH_PROGRAM_IF_ANALYZED_TOO_OFTEN, 0, PreferenceType.Integer), new UltimatePreferenceItem<>(LABEL_DUMP_PATH_PROGRAM_STOP_MODE, PathProgramDumpStop.AFTER_FIRST_DUMP, PreferenceType.Combo, PathProgramDumpStop.values()), - getConcurrencySettings() }; + getConcurrencySettings(), getParallelCegarSettings() }; } private static UltimatePreferenceItemContainer getConcurrencySettings() { @@ -792,6 +810,21 @@ private static UltimatePreferenceItemGroup getIndependenceSettings(final int ind (int) IndependenceSettings.DEFAULT_SOLVER_TIMEOUT, PreferenceType.Integer)); } + public static UltimatePreferenceItemContainer getParallelCegarSettings() { + return new UltimatePreferenceItemContainer("Parallel Trace Abstraction", + new UltimatePreferenceItem<>(LABEL_PARALLEL_CEGAR_LOOP, DEF_PARALLEL_CEGAR_LOOP, + PreferenceType.Boolean), + new UltimatePreferenceItem<>(LABEL_THREADLIMIT, DEF_THREADLIMIT, PreferenceType.Integer, + new IUltimatePreferenceItemValidator.IntegerValidator(0, 1_0000_000)), + new UltimatePreferenceItem<>(LABEL_SEARCH_LOOP_BOUND, DEF_SEARCH_LOOP_BOUND, PreferenceType.Integer, + new IUltimatePreferenceItemValidator.IntegerValidator(-1, 1_0000_000)), + new UltimatePreferenceItem<>(LABEL_PARALLELSEARCH_ACTIVE_CEX_ONLY, DEF_PARALLELSEARCH_ACTIVE_CEX_ONLY, + PreferenceType.Boolean), + new UltimatePreferenceItem<>(LABEL_MINIMIZE_ABSTRACTION_PER_WORKER, DEF_MINIMIZE_ABSTRACTION_PER_WORKER, + PreferenceType.Boolean)); + + } + public static String getSuffixedLabel(final String label, final int index) { if (index == 0) { return label; diff --git a/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/tracehandling/StrategyFactory.java b/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/tracehandling/StrategyFactory.java index 53b143a3ce7..98563c9051a 100644 --- a/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/tracehandling/StrategyFactory.java +++ b/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/tracehandling/StrategyFactory.java @@ -102,7 +102,6 @@ public class StrategyFactory> { private final TAPreferences mTaPrefs; private final TaCheckAndRefinementPreferences mPrefs; private final ILogger mLogger; - private final IIcfg mInitialIcfg; private final PredicateFactory mPredicateFactory; private final PredicateFactoryForInterpolantAutomata mPredicateFactoryInterpolAut; private final PathProgramCache mPathProgramCache; @@ -113,14 +112,22 @@ public StrategyFactory(final ILogger logger, final TAPreferences taPrefsForInter final TaCheckAndRefinementPreferences prefs, final IIcfg initialIcfg, final PredicateFactory predicateFactory, final PredicateFactoryForInterpolantAutomata predicateFactoryInterpolAut, final Class transitionClazz) { + this(logger, taPrefsForInterpolantConsolidation, prefs, initialIcfg.getCfgSmtToolkit(), predicateFactory, + predicateFactoryInterpolAut, transitionClazz, new PathProgramCache<>(logger)); + } + + public StrategyFactory(final ILogger logger, final TAPreferences taPrefsForInterpolantConsolidation, + final TaCheckAndRefinementPreferences prefs, final CfgSmtToolkit cfgSmtTollkit, + final PredicateFactory predicateFactory, + final PredicateFactoryForInterpolantAutomata predicateFactoryInterpolAut, final Class transitionClazz, + final PathProgramCache programCache) { mLogger = logger; mTaPrefs = taPrefsForInterpolantConsolidation; mPrefs = prefs; - mInitialIcfg = initialIcfg; - mCfgSmtToolkit = initialIcfg.getCfgSmtToolkit(); + mCfgSmtToolkit = cfgSmtTollkit; mPredicateFactory = predicateFactory; mPredicateFactoryInterpolAut = predicateFactoryInterpolAut; - mPathProgramCache = new PathProgramCache<>(mLogger); + mPathProgramCache = programCache; mTransitionClazz = transitionClazz; } @@ -141,6 +148,7 @@ public PathProgramCache getPathProgramCache() { * @param abstraction * The initial abstraction representing the program. Various strategies require the initial abstraction, * e.g., to extract the complete alphabet, or to perform more complex generalizations. + * @param strategyType */ public ITARefinementStrategy constructStrategy(final IUltimateServiceProvider services, final Counterexample counterexample, final IAutomaton abstraction, @@ -153,6 +161,22 @@ public ITARefinementStrategy constructStrategy(final IUltimateServiceProvider predicateUnifier, precondition, postcondition, mPrefs.getRefinementStrategy()); } + /** + * Construct Strategy with a RefinementStrategy given as parameter. + * + */ + public ITARefinementStrategy constructStrategy(final IUltimateServiceProvider services, + final Counterexample counterexample, final IAutomaton abstraction, + final TaskIdentifier taskIdentifier, final IEmptyStackStateFactory emptyStackFactory, + final IPreconditionProvider preconditionProvider, final IPostconditionProvider postconditionProvider, + final RefinementStrategy strategyType) { + final IPredicateUnifier predicateUnifier = constructPredicateUnifier(services); + final IPredicate precondition = preconditionProvider.constructPrecondition(predicateUnifier); + final IPredicate postcondition = postconditionProvider.constructPostcondition(predicateUnifier); + return constructStrategy(services, counterexample, abstraction, taskIdentifier, emptyStackFactory, + predicateUnifier, precondition, postcondition, strategyType); + } + /** * Constructs a {@link IRefinementStrategy} that can be used in conjunction with a {@link IRefinementEngine}. * @@ -242,7 +266,7 @@ public ITARefinementStrategy constructStrategy(final IUltimateServiceProvider private IPredicateUnifier constructPredicateUnifier(final IUltimateServiceProvider services) { final ManagedScript managedScript = mPrefs.getCfgSmtToolkit().getManagedScript(); - final IIcfgSymbolTable symbolTable = mInitialIcfg.getCfgSmtToolkit().getSymbolTable(); + final IIcfgSymbolTable symbolTable = mPrefs.getCfgSmtToolkit().getSymbolTable(); if (mPrefs.usePredicateTrieBasedPredicateUnifier()) { return new BPredicateUnifier(services, mLogger, managedScript, mPredicateFactory, symbolTable); } diff --git a/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/tracehandling/TraceAbstractionRefinementEngine.java b/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/tracehandling/TraceAbstractionRefinementEngine.java index e38d4eda252..d728d0f6b41 100644 --- a/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/tracehandling/TraceAbstractionRefinementEngine.java +++ b/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/tracehandling/TraceAbstractionRefinementEngine.java @@ -47,6 +47,7 @@ import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.tracehandling.IRefinementEngineResult; import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.tracehandling.IRefinementEngineResult.BasicRefinementEngineResult; import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.tracehandling.IRefinementStrategy; +import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.tracehandling.ITraceCheckStrategyModule; import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.tracehandling.RefinementEngineStatisticsGenerator; import de.uni_freiburg.informatik.ultimate.logic.Script.LBool; import de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.BasicCegarLoop; @@ -138,6 +139,9 @@ public interface ITARefinementStrategy extends IRefinementStr * collected interpolant sequences. */ IIpAbStrategyModule getInterpolantAutomatonBuilder(); + + ITraceCheckStrategyModule[] getTraceCheckModules(); + } } diff --git a/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/tracehandling/strategy/BasicRefinementStrategy.java b/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/tracehandling/strategy/BasicRefinementStrategy.java index 543f0a13b4f..05513c8c65a 100644 --- a/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/tracehandling/strategy/BasicRefinementStrategy.java +++ b/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/tracehandling/strategy/BasicRefinementStrategy.java @@ -169,7 +169,8 @@ protected boolean needsMoreInterpolants(final List per return imperfectIpps.size() < DEFAULT_INTERPOLANT_THRESHOLD; } - protected ITraceCheckStrategyModule[] getTraceCheckModules() { + @Override + public ITraceCheckStrategyModule[] getTraceCheckModules() { return mTraceChecks; }