From e4bb2b1dce5f166e2acc4089322fe708f2cc565e Mon Sep 17 00:00:00 2001 From: Matthias Heizmann Date: Wed, 17 May 2017 03:42:59 +0200 Subject: [PATCH] refactoring automata library: do not store alphabet in three sets, but introduce an visibly pushdown alphabet object --- .../AutomataDefinitionInterpreter.java | 3 +- .../AutomataScriptInterpreterObserver.java | 10 ++- .../INestedWordAutomatonFactory.java | 8 +- .../factories/NestedWordAutomatonFactory.java | 5 +- .../shrinkers/UnusedLetterShrinker.java | 12 +-- .../buchiautomizer/BuchiCegarLoop.java | 6 +- .../generator/buchiautomizer/RefineBuchi.java | 7 +- .../emptinesscheck/NWAEmptinessCheck.java | 18 ++--- .../ltl2aut/never2nwa/Never2Automaton.java | 6 +- .../lassoranker/LassoAutomatonBuilder.java | 7 +- .../lassoranker/LassoExtractorBuchi.java | 4 +- .../alternating/AA_DeterminizeReversed.java | 5 +- .../nestedword/DoubleDeckerAutomaton.java | 5 +- .../INestedWordAutomatonSimple.java | 6 +- .../INwaOutgoingTransitionProvider.java | 30 +++----- .../nestedword/NestedWordAutomataUtils.java | 6 +- .../nestedword/NestedWordAutomaton.java | 6 +- .../nestedword/NestedWordAutomatonCache.java | 61 +++++---------- .../NestedWordAutomatonFilteredStates.java | 16 +--- ...edWordAutomatonOnDemandStateAndLetter.java | 28 ++----- .../TransitionConsistencyCheck.java | 2 +- .../{InCaReAlphabet.java => VpAlphabet.java} | 76 +++++++++++++++++-- .../nestedword/buchi/BuchiClosureNwa.java | 19 ++--- .../buchi/BuchiComplementAutomatonSVW.java | 63 +++++++-------- .../buchi/BuchiComplementDeterministic.java | 3 +- .../buchi/BuchiComplementFKVNwa.java | 30 +++----- .../buchi/BuchiComplementNCSBNwa.java | 19 +---- .../nestedword/buchi/BuchiIntersectNwa.java | 19 +---- .../nestedword/buchi/BuchiIsEmptyXW.java | 4 +- .../operations/AbstractAcceptance.java | 6 +- .../nestedword/operations/Analyze.java | 6 +- .../ComplementDeterministicNwa.java | 21 ++--- .../operations/ConcurrentProduct.java | 16 ++-- .../nestedword/operations/DeterminizeNwa.java | 29 ++----- .../nestedword/operations/GetRandomDfa.java | 3 +- .../operations/GetRandomNestedWord.java | 6 +- .../nestedword/operations/GetRandomNwa.java | 7 +- .../nestedword/operations/GetRandomNwaTv.java | 5 +- .../nestedword/operations/IntersectNwa.java | 19 +---- .../nestedword/operations/IsTotal.java | 6 +- .../nestedword/operations/LoopComplexity.java | 8 +- .../operations/SuperDifference.java | 3 +- .../nestedword/operations/TotalizeNwa.java | 27 +++---- .../IncrementalInclusionCheck2.java | 3 +- ...rementalInclusionCheck2DeadEndRemoval.java | 3 +- ...usionCheck2DeadEndRemovalAdvanceCover.java | 3 +- ...ck2DeadEndRemovalAdvanceCover_2Stacks.java | 3 +- ...2Stacks_multipleCounterExamplesAtOnce.java | 13 ++-- .../minimization/AbstractMinimizeNwa.java | 6 +- .../MinimizeDfaHopcroftArrays.java | 4 +- .../MinimizeDfaHopcroftLists.java | 6 +- .../minimization/MinimizeDfaHopcroftWiki.java | 8 +- .../minimization/MinimizeDfaSymbolic.java | 2 +- .../minimization/MinimizeDfaTable.java | 6 +- .../minimization/MinimizeNfaBrzozowski.java | 3 +- .../minimization/MinimizeNwaMaxSat2.java | 2 +- .../NwaApproximateBisimulation.java | 2 +- .../minimization/QuotientNwaConstructor.java | 6 +- .../operations/minimization/ShrinkNwa.java | 4 +- .../minimization/maxsat/arrays/Converter.java | 9 ++- .../NwaApproximateDelayedSimulation.java | 3 +- .../parallel/MinimizeDfaHopcroftParallel.java | 2 +- .../operations/oldapi/AbstractIntersect.java | 15 ++-- .../operations/oldapi/DeterminizeDD.java | 9 +-- .../operations/oldapi/DeterminizeSadd.java | 3 +- .../operations/oldapi/DifferenceDD.java | 22 +----- .../operations/oldapi/DifferenceSadd.java | 9 +-- .../oldapi/ReachableStatesCopy.java | 9 +-- .../operations/simulation/AGameGraph.java | 3 +- .../simulation/delayed/DelayedGameGraph.java | 6 +- .../simulation/direct/DirectGameGraph.java | 4 +- .../simulation/fair/FairGameGraph.java | 4 +- .../FullMultipebbleGameAutomaton.java | 28 ++----- .../CompareReduceBuchiSimulation.java | 3 +- .../nwa/graph/NwaGameGraphGeneration.java | 8 +- .../NestedWordAutomatonReachableStates.java | 32 ++------ .../nestedword/senwa/DifferenceSenwa.java | 3 +- .../automata/nestedword/senwa/Senwa.java | 6 +- .../nestedword/senwa/SenwaBuilder.java | 2 +- .../nestedword/senwa/SenwaWalker.java | 9 +-- .../CommonExternalFormatWriter.java | 2 +- .../visualization/GoalFormatWriter.java | 2 +- .../visualization/HanoiFormatWriter.java | 8 +- .../nestedword/visualization/NwaWriter.java | 6 +- .../petrinet/PetriNet2FiniteAutomaton.java | 4 +- .../julian/DifferenceBlackAndWhite.java | 2 +- .../petrinet/julian/PetriNetJulian.java | 2 +- .../petrinet/julian/PrefixProduct.java | 4 +- .../automata/statefactory/StringFactory.java | 4 +- .../traceabstraction/Converter.java | 6 +- .../CFG2NestedWordAutomaton.java | 5 +- .../CegarLoopSWBnonRecursive.java | 3 +- .../interactive/PreNestedWord.java | 15 ++-- ...sIntNonSmtInterpolantAutomatonBuilder.java | 3 +- ...raightLineInterpolantAutomatonBuilder.java | 9 +-- ...IntTotalInterpolationAutomatonBuilder.java | 3 +- .../CanonicalInterpolantAutomatonBuilder.java | 19 +++-- .../InterpolantAutomatonBuilderFactory.java | 6 +- ...MultiTrackInterpolantAutomatonBuilder.java | 20 +---- ...raightLineInterpolantAutomatonBuilder.java | 7 +- .../TotalInterpolationAutomatonBuilder.java | 4 +- .../TwoTrackInterpolantAutomatonBuilder.java | 18 +---- .../AbstractInterpolantAutomaton.java | 24 ++---- .../InterpolantConsolidation.java | 5 +- .../PathProgramAutomatonConstructor.java | 7 +- .../WitnessLocationMatcher.java | 12 +-- .../WitnessModelToAutomatonTransformer.java | 7 +- .../WitnessProductAutomaton.java | 15 +--- .../CFG2Automaton.java | 8 +- .../RAFA_Determination.java | 6 +- 110 files changed, 474 insertions(+), 671 deletions(-) rename trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/{InCaReAlphabet.java => VpAlphabet.java} (54%) diff --git a/trunk/source/AutomataScriptInterpreter/src/de/uni_freiburg/informatik/ultimate/plugins/generator/automatascriptinterpreter/AutomataDefinitionInterpreter.java b/trunk/source/AutomataScriptInterpreter/src/de/uni_freiburg/informatik/ultimate/plugins/generator/automatascriptinterpreter/AutomataDefinitionInterpreter.java index bdf862bbe3a..4c6ba655917 100644 --- a/trunk/source/AutomataScriptInterpreter/src/de/uni_freiburg/informatik/ultimate/plugins/generator/automatascriptinterpreter/AutomataDefinitionInterpreter.java +++ b/trunk/source/AutomataScriptInterpreter/src/de/uni_freiburg/informatik/ultimate/plugins/generator/automatascriptinterpreter/AutomataDefinitionInterpreter.java @@ -46,6 +46,7 @@ import de.uni_freiburg.informatik.ultimate.automata.AutomataLibraryServices; import de.uni_freiburg.informatik.ultimate.automata.alternating.AlternatingAutomaton; import de.uni_freiburg.informatik.ultimate.automata.alternating.BooleanExpression; +import de.uni_freiburg.informatik.ultimate.automata.nestedword.VpAlphabet; import de.uni_freiburg.informatik.ultimate.automata.nestedword.NestedWordAutomaton; import de.uni_freiburg.informatik.ultimate.automata.petrinet.Place; import de.uni_freiburg.informatik.ultimate.automata.petrinet.julian.PetriNetJulian; @@ -322,7 +323,7 @@ public void interpret(final NestedwordAutomatonAST nwa) { } final NestedWordAutomaton nw = new NestedWordAutomaton<>(new AutomataLibraryServices(mServices), - internalAlphabet, callAlphabet, returnAlphabet, new StringFactory()); + new VpAlphabet(internalAlphabet, callAlphabet, returnAlphabet), new StringFactory()); // add the states for (final String state : allStates) { diff --git a/trunk/source/AutomataScriptInterpreter/src/de/uni_freiburg/informatik/ultimate/plugins/generator/automatascriptinterpreter/AutomataScriptInterpreterObserver.java b/trunk/source/AutomataScriptInterpreter/src/de/uni_freiburg/informatik/ultimate/plugins/generator/automatascriptinterpreter/AutomataScriptInterpreterObserver.java index 392d4667634..9f7e33aa522 100644 --- a/trunk/source/AutomataScriptInterpreter/src/de/uni_freiburg/informatik/ultimate/plugins/generator/automatascriptinterpreter/AutomataScriptInterpreterObserver.java +++ b/trunk/source/AutomataScriptInterpreter/src/de/uni_freiburg/informatik/ultimate/plugins/generator/automatascriptinterpreter/AutomataScriptInterpreterObserver.java @@ -27,11 +27,12 @@ */ package de.uni_freiburg.informatik.ultimate.plugins.generator.automatascriptinterpreter; -import java.util.HashSet; +import java.util.Collections; 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.nestedword.VpAlphabet; import de.uni_freiburg.informatik.ultimate.automata.nestedword.NestedWordAutomaton; import de.uni_freiburg.informatik.ultimate.automata.statefactory.StringFactory; import de.uni_freiburg.informatik.ultimate.core.model.models.IElement; @@ -105,9 +106,10 @@ IElement getUltimateModelOfLastPrintedAutomaton() { public IAutomaton getDummyAutomatonWithMessage() { final NestedWordAutomaton dummyAutomaton = new NestedWordAutomaton<>( - new AutomataLibraryServices(mServices), new HashSet(0), null, null, new StringFactory()); - dummyAutomaton.addState(true, false, "Use the print keyword in .ats file to select an automaton" - + " for visualization"); + new AutomataLibraryServices(mServices), new VpAlphabet<>(Collections.emptySet()), + new StringFactory()); + dummyAutomaton.addState(true, false, + "Use the print keyword in .ats file to select an automaton" + " for visualization"); return dummyAutomaton; } } diff --git a/trunk/source/AutomatonDeltaDebugger/src/de/uni_freiburg/informatik/ultimate/plugins/analysis/automatondeltadebugger/factories/INestedWordAutomatonFactory.java b/trunk/source/AutomatonDeltaDebugger/src/de/uni_freiburg/informatik/ultimate/plugins/analysis/automatondeltadebugger/factories/INestedWordAutomatonFactory.java index 085df0ceba9..ae9402faaae 100644 --- a/trunk/source/AutomatonDeltaDebugger/src/de/uni_freiburg/informatik/ultimate/plugins/analysis/automatondeltadebugger/factories/INestedWordAutomatonFactory.java +++ b/trunk/source/AutomatonDeltaDebugger/src/de/uni_freiburg/informatik/ultimate/plugins/analysis/automatondeltadebugger/factories/INestedWordAutomatonFactory.java @@ -70,7 +70,7 @@ public INestedWordAutomatonFactory(final INestedWordAutomaton aut * @return new {@link INestedWordAutomaton} object */ public INestedWordAutomaton create(final INestedWordAutomaton automaton) { - return create(automaton.getInternalAlphabet(), automaton.getCallAlphabet(), automaton.getReturnAlphabet()); + return create(automaton.getVpAlphabet().getInternalAlphabet(), automaton.getVpAlphabet().getCallAlphabet(), automaton.getVpAlphabet().getReturnAlphabet()); } /** @@ -87,10 +87,10 @@ public INestedWordAutomaton create(final INestedWordAutomaton create(final Set internalAlphabet, final Set callAlphabet, final Set returnAlphabet) { final Set internalAlphabetRes = - (internalAlphabet == null) ? mAutomaton.getInternalAlphabet() : internalAlphabet; - final Set callAlphabetRes = (callAlphabet == null) ? mAutomaton.getCallAlphabet() : callAlphabet; + (internalAlphabet == null) ? mAutomaton.getVpAlphabet().getInternalAlphabet() : internalAlphabet; + final Set callAlphabetRes = (callAlphabet == null) ? mAutomaton.getVpAlphabet().getCallAlphabet() : callAlphabet; final Set returnAlphabetRes = - (returnAlphabet == null) ? mAutomaton.getReturnAlphabet() : returnAlphabet; + (returnAlphabet == null) ? mAutomaton.getVpAlphabet().getReturnAlphabet() : returnAlphabet; return createWithAlphabets(internalAlphabetRes, callAlphabetRes, returnAlphabetRes); } diff --git a/trunk/source/AutomatonDeltaDebugger/src/de/uni_freiburg/informatik/ultimate/plugins/analysis/automatondeltadebugger/factories/NestedWordAutomatonFactory.java b/trunk/source/AutomatonDeltaDebugger/src/de/uni_freiburg/informatik/ultimate/plugins/analysis/automatondeltadebugger/factories/NestedWordAutomatonFactory.java index 698191878fb..9328a2ab723 100644 --- a/trunk/source/AutomatonDeltaDebugger/src/de/uni_freiburg/informatik/ultimate/plugins/analysis/automatondeltadebugger/factories/NestedWordAutomatonFactory.java +++ b/trunk/source/AutomatonDeltaDebugger/src/de/uni_freiburg/informatik/ultimate/plugins/analysis/automatondeltadebugger/factories/NestedWordAutomatonFactory.java @@ -31,6 +31,7 @@ import de.uni_freiburg.informatik.ultimate.automata.AutomataLibraryServices; import de.uni_freiburg.informatik.ultimate.automata.nestedword.INestedWordAutomaton; +import de.uni_freiburg.informatik.ultimate.automata.nestedword.VpAlphabet; import de.uni_freiburg.informatik.ultimate.automata.nestedword.NestedWordAutomaton; import de.uni_freiburg.informatik.ultimate.core.model.services.IUltimateServiceProvider; @@ -72,8 +73,8 @@ private NestedWordAutomaton getNwa(final INestedWordAutomaton createWithAlphabets(final Set internalAlphabet, final Set callAlphabet, final Set returnAlphabet) { - return new NestedWordAutomaton<>(new AutomataLibraryServices(mServices), internalAlphabet, callAlphabet, - returnAlphabet, mAutomaton.getStateFactory()); + return new NestedWordAutomaton<>(new AutomataLibraryServices(mServices), new VpAlphabet<>(internalAlphabet, callAlphabet, + returnAlphabet), mAutomaton.getStateFactory()); } @Override diff --git a/trunk/source/AutomatonDeltaDebugger/src/de/uni_freiburg/informatik/ultimate/plugins/analysis/automatondeltadebugger/shrinkers/UnusedLetterShrinker.java b/trunk/source/AutomatonDeltaDebugger/src/de/uni_freiburg/informatik/ultimate/plugins/analysis/automatondeltadebugger/shrinkers/UnusedLetterShrinker.java index 9988299e7d9..bb1a218eb15 100644 --- a/trunk/source/AutomatonDeltaDebugger/src/de/uni_freiburg/informatik/ultimate/plugins/analysis/automatondeltadebugger/shrinkers/UnusedLetterShrinker.java +++ b/trunk/source/AutomatonDeltaDebugger/src/de/uni_freiburg/informatik/ultimate/plugins/analysis/automatondeltadebugger/shrinkers/UnusedLetterShrinker.java @@ -65,9 +65,9 @@ public UnusedLetterShrinker(final IUltimateServiceProvider services) { public INestedWordAutomaton createAutomaton(final List> list) { // create alphabets final ListIterator> lit = list.listIterator(); - final Set internalAlphabet = unwrapLetters(lit, mAutomaton.getInternalAlphabet(), LetterType.INTERNAL); - final Set callAlphabet = unwrapLetters(lit, mAutomaton.getCallAlphabet(), LetterType.CALL); - final Set returnAlphabet = unwrapLetters(lit, mAutomaton.getReturnAlphabet(), LetterType.RETURN); + final Set internalAlphabet = unwrapLetters(lit, mAutomaton.getVpAlphabet().getInternalAlphabet(), LetterType.INTERNAL); + final Set callAlphabet = unwrapLetters(lit, mAutomaton.getVpAlphabet().getCallAlphabet(), LetterType.CALL); + final Set returnAlphabet = unwrapLetters(lit, mAutomaton.getVpAlphabet().getReturnAlphabet(), LetterType.RETURN); // create fresh automaton final INestedWordAutomaton automaton = @@ -103,9 +103,9 @@ public List> extractList() { // wrap complement of present letters to include type information final ArrayList> unused = new ArrayList<>(); - addComplementLetters(internalsUsed, unused, LetterType.INTERNAL, mAutomaton.getInternalAlphabet()); - addComplementLetters(callsUsed, unused, LetterType.CALL, mAutomaton.getCallAlphabet()); - addComplementLetters(returnsUsed, unused, LetterType.RETURN, mAutomaton.getReturnAlphabet()); + addComplementLetters(internalsUsed, unused, LetterType.INTERNAL, mAutomaton.getVpAlphabet().getInternalAlphabet()); + addComplementLetters(callsUsed, unused, LetterType.CALL, mAutomaton.getVpAlphabet().getCallAlphabet()); + addComplementLetters(returnsUsed, unused, LetterType.RETURN, mAutomaton.getVpAlphabet().getReturnAlphabet()); return unused; } diff --git a/trunk/source/BuchiAutomizer/src/de/uni_freiburg/informatik/ultimate/plugins/generator/buchiautomizer/BuchiCegarLoop.java b/trunk/source/BuchiAutomizer/src/de/uni_freiburg/informatik/ultimate/plugins/generator/buchiautomizer/BuchiCegarLoop.java index eef8e3848c2..acd1ea6b6ee 100644 --- a/trunk/source/BuchiAutomizer/src/de/uni_freiburg/informatik/ultimate/plugins/generator/buchiautomizer/BuchiCegarLoop.java +++ b/trunk/source/BuchiAutomizer/src/de/uni_freiburg/informatik/ultimate/plugins/generator/buchiautomizer/BuchiCegarLoop.java @@ -45,7 +45,7 @@ import de.uni_freiburg.informatik.ultimate.automata.AutomatonDefinitionPrinter.Format; import de.uni_freiburg.informatik.ultimate.automata.IAutomaton; import de.uni_freiburg.informatik.ultimate.automata.nestedword.INestedWordAutomaton; -import de.uni_freiburg.informatik.ultimate.automata.nestedword.InCaReAlphabet; +import de.uni_freiburg.informatik.ultimate.automata.nestedword.VpAlphabet; 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; @@ -693,7 +693,7 @@ private void getInitialAbstraction() { acceptingNodes = allNodes; } mAbstraction = cFG2NestedWordAutomaton.getNestedWordAutomaton(mIcfg, mDefaultStateFactory, acceptingNodes); - if (!ALLOW_CALLS && !mAbstraction.getCallAlphabet().isEmpty()) { + if (!ALLOW_CALLS && !mAbstraction.getVpAlphabet().getCallAlphabet().isEmpty()) { throw new AssertionError("Calls are not allowed in this debugging mode"); } } @@ -772,7 +772,7 @@ protected void constructInterpolantAutomaton(final InterpolatingTraceChecker tra final NestedRun run) throws AutomataOperationCanceledException { final CanonicalInterpolantAutomatonBuilder iab = new CanonicalInterpolantAutomatonBuilder<>(mServices, traceChecker.getIpp(), run.getStateSequence(), - new InCaReAlphabet<>(mAbstraction), mCsToolkitWithRankVars, mAbstraction.getStateFactory(), + new VpAlphabet<>(mAbstraction), mCsToolkitWithRankVars, mAbstraction.getStateFactory(), mLogger, traceChecker.getPredicateUnifier(), run.getWord()); iab.analyze(); mInterpolAutomaton = iab.getResult(); diff --git a/trunk/source/BuchiAutomizer/src/de/uni_freiburg/informatik/ultimate/plugins/generator/buchiautomizer/RefineBuchi.java b/trunk/source/BuchiAutomizer/src/de/uni_freiburg/informatik/ultimate/plugins/generator/buchiautomizer/RefineBuchi.java index df41016d96f..3c4f4fe541d 100644 --- a/trunk/source/BuchiAutomizer/src/de/uni_freiburg/informatik/ultimate/plugins/generator/buchiautomizer/RefineBuchi.java +++ b/trunk/source/BuchiAutomizer/src/de/uni_freiburg/informatik/ultimate/plugins/generator/buchiautomizer/RefineBuchi.java @@ -313,7 +313,7 @@ INestedWordAutomaton refineBuchi( // : "no progress"; if (mDumpAutomata) { final String automatonString; - if (mInterpolAutomatonUsedInRefinement.getCallAlphabet().isEmpty()) { + if (mInterpolAutomatonUsedInRefinement.getVpAlphabet().getCallAlphabet().isEmpty()) { automatonString = "interpolBuchiAutomatonUsedInRefinement"; } else { automatonString = "interpolBuchiNestedWordAutomatonUsedInRefinement"; @@ -340,7 +340,7 @@ INestedWordAutomaton refineBuchi( determinicity = "nondeterministic"; } final String automatonString; - if (mInterpolAutomatonUsedInRefinement.getCallAlphabet().isEmpty()) { + if (mInterpolAutomatonUsedInRefinement.getVpAlphabet().getCallAlphabet().isEmpty()) { automatonString = "interpolBuchiAutomatonUsedInRefinement"; } else { automatonString = "interpolBuchiNestedWordAutomatonUsedInRefinement"; @@ -549,8 +549,7 @@ private NestedWordAutomaton constructBuchiInterpolantAutomat final NestedWord loop, final IPredicate[] loopInterpolants, final INestedWordAutomatonSimple abstraction) { final NestedWordAutomaton result = - new NestedWordAutomaton<>(new AutomataLibraryServices(mServices), abstraction.getInternalAlphabet(), - abstraction.getCallAlphabet(), abstraction.getReturnAlphabet(), abstraction.getStateFactory()); + new NestedWordAutomaton<>(new AutomataLibraryServices(mServices), abstraction.getVpAlphabet(), abstraction.getStateFactory()); final boolean emptyStem = stem.length() == 0; if (emptyStem) { result.addState(true, true, honda); diff --git a/trunk/source/CodeCheck/src/de/uni_freiburg/informatik/ultimate/plugins/generator/emptinesscheck/NWAEmptinessCheck.java b/trunk/source/CodeCheck/src/de/uni_freiburg/informatik/ultimate/plugins/generator/emptinesscheck/NWAEmptinessCheck.java index c50b22f5993..6c7f5bff545 100644 --- a/trunk/source/CodeCheck/src/de/uni_freiburg/informatik/ultimate/plugins/generator/emptinesscheck/NWAEmptinessCheck.java +++ b/trunk/source/CodeCheck/src/de/uni_freiburg/informatik/ultimate/plugins/generator/emptinesscheck/NWAEmptinessCheck.java @@ -39,6 +39,7 @@ import de.uni_freiburg.informatik.ultimate.automata.AutomataLibraryServices; import de.uni_freiburg.informatik.ultimate.automata.AutomataOperationCanceledException; import de.uni_freiburg.informatik.ultimate.automata.nestedword.INestedWordAutomatonSimple; +import de.uni_freiburg.informatik.ultimate.automata.nestedword.VpAlphabet; import de.uni_freiburg.informatik.ultimate.automata.nestedword.NestedRun; import de.uni_freiburg.informatik.ultimate.automata.nestedword.operations.IsEmpty; import de.uni_freiburg.informatik.ultimate.automata.nestedword.operations.RemoveUnreachable; @@ -83,6 +84,7 @@ private final class MyNWA implements INestedWordAutomatonSimple> mInternalAlphabet = new HashSet<>(); private final Set> mCallAlphabet = new HashSet<>(); private final Set> mReturnAlphabet = new HashSet<>(); + private final VpAlphabet> mVpAlphabet = new VpAlphabet>(mInternalAlphabet, mCallAlphabet, mReturnAlphabet); private final IStateFactory mStateFactory = new DummyStateFactory<>(); @@ -234,20 +236,10 @@ public Set> getAlphabet() { public String sizeInformation() { return "no size info available"; } - - @Override - public Set> getInternalAlphabet() { - return mInternalAlphabet; - } - - @Override - public Set> getCallAlphabet() { - return mCallAlphabet; - } - + @Override - public Set> getReturnAlphabet() { - return mReturnAlphabet; + public VpAlphabet> getVpAlphabet() { + return mVpAlphabet; } @Override diff --git a/trunk/source/LTL2aut/src/de/uni_freiburg/informatik/ultimate/ltl2aut/never2nwa/Never2Automaton.java b/trunk/source/LTL2aut/src/de/uni_freiburg/informatik/ultimate/ltl2aut/never2nwa/Never2Automaton.java index 79e5c6c500c..45cc20df85e 100644 --- a/trunk/source/LTL2aut/src/de/uni_freiburg/informatik/ultimate/ltl2aut/never2nwa/Never2Automaton.java +++ b/trunk/source/LTL2aut/src/de/uni_freiburg/informatik/ultimate/ltl2aut/never2nwa/Never2Automaton.java @@ -37,6 +37,7 @@ import de.uni_freiburg.informatik.ultimate.automata.AutomataLibraryServices; import de.uni_freiburg.informatik.ultimate.automata.nestedword.INestedWordAutomaton; +import de.uni_freiburg.informatik.ultimate.automata.nestedword.VpAlphabet; import de.uni_freiburg.informatik.ultimate.automata.nestedword.NestedWordAutomaton; import de.uni_freiburg.informatik.ultimate.automata.statefactory.DummyStateFactory; import de.uni_freiburg.informatik.ultimate.boogie.annotation.LTLPropertyCheck.CheckableExpression; @@ -114,8 +115,7 @@ public Never2Automaton(final AstNode ast, final BoogieSymbolTable boogieSymbolTa mRewriteAssumeDuringSBE = ups.getBoolean(PreferenceInitializer.LABEL_OPTIMIZE_REWRITEASSUME); mAutomaton = new NestedWordAutomaton<>(new AutomataLibraryServices(mServices), - collectAlphabet(), null, // call - null, // return + new VpAlphabet<>(collectAlphabet()), new DummyStateFactory()); collectStates(mNeverClaim, null); @@ -369,7 +369,7 @@ private List mergeStatements(final CheckableExpression... exprs) { } private void addTransition(final String predecessor, final CodeBlock letter, final String successor) { - mAutomaton.getInternalAlphabet().add(letter); + mAutomaton.getVpAlphabet().getInternalAlphabet().add(letter); mAutomaton.addInternalTransition(predecessor, letter, successor); } diff --git a/trunk/source/LassoRanker/src/de/uni_freiburg/informatik/ultimate/plugins/analysis/lassoranker/LassoAutomatonBuilder.java b/trunk/source/LassoRanker/src/de/uni_freiburg/informatik/ultimate/plugins/analysis/lassoranker/LassoAutomatonBuilder.java index 0b6d86ae9b8..f133070bf64 100644 --- a/trunk/source/LassoRanker/src/de/uni_freiburg/informatik/ultimate/plugins/analysis/lassoranker/LassoAutomatonBuilder.java +++ b/trunk/source/LassoRanker/src/de/uni_freiburg/informatik/ultimate/plugins/analysis/lassoranker/LassoAutomatonBuilder.java @@ -33,7 +33,7 @@ import de.uni_freiburg.informatik.ultimate.automata.AutomataLibraryServices; import de.uni_freiburg.informatik.ultimate.automata.AutomataOperationCanceledException; import de.uni_freiburg.informatik.ultimate.automata.nestedword.INestedWordAutomatonSimple; -import de.uni_freiburg.informatik.ultimate.automata.nestedword.InCaReAlphabet; +import de.uni_freiburg.informatik.ultimate.automata.nestedword.VpAlphabet; 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.buchi.BuchiAccepts; @@ -53,13 +53,12 @@ public final class LassoAutomatonBuilder { private final NestedWordAutomaton mResult; private final PredicateFactory mPredicateFactory; - public LassoAutomatonBuilder(final InCaReAlphabet alphabet, + public LassoAutomatonBuilder(final VpAlphabet alphabet, final IStateFactory predicateFactoryRc, final PredicateFactory predicateFactory, final NestedWord stem, final NestedWord loop, final IUltimateServiceProvider services) throws AutomataOperationCanceledException { mPredicateFactory = predicateFactory; - mResult = new NestedWordAutomaton<>(new AutomataLibraryServices(services), alphabet.getInternalAlphabet(), - alphabet.getCallAlphabet(), alphabet.getReturnAlphabet(), predicateFactoryRc); + mResult = new NestedWordAutomaton<>(new AutomataLibraryServices(services), alphabet, predicateFactoryRc); final List stemStates = constructListOfDontCarePredicates(stem.length()); final List loopStates = constructListOfDontCarePredicates(loop.length()); IPredicate initialState; diff --git a/trunk/source/LassoRanker/src/de/uni_freiburg/informatik/ultimate/plugins/analysis/lassoranker/LassoExtractorBuchi.java b/trunk/source/LassoRanker/src/de/uni_freiburg/informatik/ultimate/plugins/analysis/lassoranker/LassoExtractorBuchi.java index 6f952a8eb60..9317b6e65fd 100644 --- a/trunk/source/LassoRanker/src/de/uni_freiburg/informatik/ultimate/plugins/analysis/lassoranker/LassoExtractorBuchi.java +++ b/trunk/source/LassoRanker/src/de/uni_freiburg/informatik/ultimate/plugins/analysis/lassoranker/LassoExtractorBuchi.java @@ -34,7 +34,6 @@ import de.uni_freiburg.informatik.ultimate.automata.AutomataLibraryException; import de.uni_freiburg.informatik.ultimate.automata.AutomataLibraryServices; import de.uni_freiburg.informatik.ultimate.automata.nestedword.INestedWordAutomatonSimple; -import de.uni_freiburg.informatik.ultimate.automata.nestedword.InCaReAlphabet; import de.uni_freiburg.informatik.ultimate.automata.nestedword.buchi.BuchiDifferenceFKV; import de.uni_freiburg.informatik.ultimate.automata.nestedword.buchi.BuchiIsEmpty; import de.uni_freiburg.informatik.ultimate.automata.nestedword.buchi.NestedLassoRun; @@ -87,8 +86,7 @@ public LassoExtractorBuchi(final IUltimateServiceProvider services, final IIcfg< mSomeNoneForErrorReport = extractSomeNodeForErrorReport(rootNode); } else { final NestedLassoWord nlw = run.getNestedLassoWord(); - final InCaReAlphabet alphabet = new InCaReAlphabet<>(mCfgAutomaton); - mLassoAutomaton = new LassoAutomatonBuilder<>(alphabet, mPredicateFactoryRc, mPredicateFactory, + mLassoAutomaton = new LassoAutomatonBuilder<>(mCfgAutomaton.getVpAlphabet(), mPredicateFactoryRc, mPredicateFactory, nlw.getStem(), nlw.getLoop(), mServices).getResult(); final INestedWordAutomatonSimple difference = new BuchiDifferenceFKV<>(new AutomataLibraryServices(mServices), mPredicateFactoryRc, mCfgAutomaton, diff --git a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/alternating/AA_DeterminizeReversed.java b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/alternating/AA_DeterminizeReversed.java index bf77f7f062f..caeda24fa0e 100644 --- a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/alternating/AA_DeterminizeReversed.java +++ b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/alternating/AA_DeterminizeReversed.java @@ -35,6 +35,7 @@ import de.uni_freiburg.informatik.ultimate.automata.AutomataLibraryServices; import de.uni_freiburg.informatik.ultimate.automata.GeneralOperation; import de.uni_freiburg.informatik.ultimate.automata.nestedword.INestedWordAutomaton; +import de.uni_freiburg.informatik.ultimate.automata.nestedword.VpAlphabet; import de.uni_freiburg.informatik.ultimate.automata.nestedword.NestedWordAutomaton; import de.uni_freiburg.informatik.ultimate.automata.statefactory.IStateFactory; import de.uni_freiburg.informatik.ultimate.util.datastructures.relation.Pair; @@ -45,8 +46,8 @@ public class AA_DeterminizeReversed extends GeneralOperation alternatingAutomaton) { super(services); - mResultAutomaton = new NestedWordAutomaton<>(services, alternatingAutomaton.getAlphabet(), - Collections.emptySet(), Collections.emptySet(), alternatingAutomaton.getStateFactory()); + final VpAlphabet vpAlphabet = new VpAlphabet(alternatingAutomaton.getAlphabet(), Collections.emptySet(), Collections.emptySet()); + mResultAutomaton = new NestedWordAutomaton<>(services, vpAlphabet, alternatingAutomaton.getStateFactory()); final LinkedList newStates = new LinkedList<>(); newStates.add(alternatingAutomaton.getFinalStatesBitVector()); final List>> transitionsToAdd = new ArrayList<>(); diff --git a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/DoubleDeckerAutomaton.java b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/DoubleDeckerAutomaton.java index 9926e780af6..200ed0ef70a 100644 --- a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/DoubleDeckerAutomaton.java +++ b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/DoubleDeckerAutomaton.java @@ -62,9 +62,8 @@ public class DoubleDeckerAutomaton extends NestedWordAutomaton internalAlphabet, - final Set callAlphabet, final Set returnAlphabet, final IStateFactory stateFactory) { - super(services, internalAlphabet, callAlphabet, returnAlphabet, stateFactory); + public DoubleDeckerAutomaton(final AutomataLibraryServices services, final VpAlphabet vpAlphabet, final IStateFactory stateFactory) { + super(services, vpAlphabet, stateFactory); mUp2Down = null; } diff --git a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/INestedWordAutomatonSimple.java b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/INestedWordAutomatonSimple.java index d09cc46c2bc..404ecaeaa65 100644 --- a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/INestedWordAutomatonSimple.java +++ b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/INestedWordAutomatonSimple.java @@ -79,7 +79,7 @@ public interface INestedWordAutomatonSimple extends INwaOutgoingT * with letter a. */ default Set lettersInternal(final STATE state) { - return getInternalAlphabet(); + return getVpAlphabet().getInternalAlphabet(); } /** @@ -89,7 +89,7 @@ default Set lettersInternal(final STATE state) { * letter a. */ default Set lettersCall(final STATE state) { - return getCallAlphabet(); + return getVpAlphabet().getCallAlphabet(); } /** @@ -99,7 +99,7 @@ default Set lettersCall(final STATE state) { * hierarchical predecessor is hier and that is labeled with letter a */ default Set lettersReturn(final STATE state, final STATE hier) { - return getReturnAlphabet(); + return getVpAlphabet().getReturnAlphabet(); } /** diff --git a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/INwaOutgoingTransitionProvider.java b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/INwaOutgoingTransitionProvider.java index 5df4d1776f1..c5d7fe36584 100644 --- a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/INwaOutgoingTransitionProvider.java +++ b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/INwaOutgoingTransitionProvider.java @@ -46,32 +46,22 @@ * Type of objects which can be used as states. */ public interface INwaOutgoingTransitionProvider extends IAutomaton { - /** - * @return Set of all letters that can occur as label of an internal transition. - *

- * The default definition of nested word automata does not allow separate alphabets for internal, call, and - * return symbols. The default definition of visibly pushdown automata requires that all three alphabets are - * disjoint. We deviate from both definitions. We allow separate alphabets but do not require that they are - * disjoint. - */ - Set getInternalAlphabet(); + +// Set getInternalAlphabet(); +// +// Set getCallAlphabet(); +// +// Set getReturnAlphabet(); + + VpAlphabet getVpAlphabet(); + @Override default Set getAlphabet() { - return getInternalAlphabet(); + return getVpAlphabet().getInternalAlphabet(); } - /** - * @return Set of all letters that can occur as label of a call transition. - * @see #getInternalAlphabet() - */ - Set getCallAlphabet(); - /** - * @return Set of all letters that can occur as label of a return transition. - * @see #getInternalAlphabet() - */ - Set getReturnAlphabet(); /** * @return Auxiliary state used to model the hierarchical predecessor of a pending return in some operations.
diff --git a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/NestedWordAutomataUtils.java b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/NestedWordAutomataUtils.java index cceffafb2ab..449e65565a0 100644 --- a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/NestedWordAutomataUtils.java +++ b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/NestedWordAutomataUtils.java @@ -286,7 +286,7 @@ public static Set constructReturnSuccessors( * @return {@code true} iff both the call alphabet and the return alphabet is empty. */ public static boolean isFiniteAutomaton(final INestedWordAutomatonSimple nwa) { - return nwa.getCallAlphabet().isEmpty() && nwa.getReturnAlphabet().isEmpty(); + return nwa.getVpAlphabet().getCallAlphabet().isEmpty() && nwa.getVpAlphabet().getReturnAlphabet().isEmpty(); } /** @@ -305,9 +305,7 @@ public static boolean isFiniteAutomaton(final INestedWordAutomat public static boolean sameAlphabet(final INestedWordAutomatonSimple fstOperand, final INestedWordAutomatonSimple sndOperand) { boolean result; - result = fstOperand.getInternalAlphabet().equals(sndOperand.getInternalAlphabet()); - result = result && fstOperand.getCallAlphabet().equals(sndOperand.getCallAlphabet()); - result = result && fstOperand.getReturnAlphabet().equals(sndOperand.getReturnAlphabet()); + result = fstOperand.getVpAlphabet().equals(sndOperand.getVpAlphabet()); return result; } diff --git a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/NestedWordAutomaton.java b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/NestedWordAutomaton.java index 2148e63cd1a..7d1fe16a82f 100644 --- a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/NestedWordAutomaton.java +++ b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/NestedWordAutomaton.java @@ -111,9 +111,9 @@ public class NestedWordAutomaton extends NestedWordAutomatonCache * @param stateFactory * state factory */ - public NestedWordAutomaton(final AutomataLibraryServices services, final Set internalAlphabet, - final Set callAlphabet, final Set returnAlphabet, final IStateFactory stateFactory) { - super(services, internalAlphabet, callAlphabet, returnAlphabet, stateFactory); + public NestedWordAutomaton(final AutomataLibraryServices services, final VpAlphabet vpAlphabet, + final IStateFactory stateFactory) { + super(services, vpAlphabet, stateFactory); } diff --git a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/NestedWordAutomatonCache.java b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/NestedWordAutomatonCache.java index a6209844c15..96f1cc996ac 100644 --- a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/NestedWordAutomatonCache.java +++ b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/NestedWordAutomatonCache.java @@ -72,9 +72,7 @@ public class NestedWordAutomatonCache implements INestedWordAutom protected final AutomataLibraryServices mServices; protected final ILogger mLogger; - private final Set mInternalAlphabet; - private final Set mCallAlphabet; - private final Set mReturnAlphabet; + private final VpAlphabet mVpAlphabet; /** * Set of internal transitions PREs x LETTERs x SUCCs stored as map PREs -> LETTERs -> SUCCs. @@ -108,36 +106,22 @@ public class NestedWordAutomatonCache implements INestedWordAutom * @param stateFactory * state factory */ - public NestedWordAutomatonCache(final AutomataLibraryServices services, final Set internalAlphabet, - final Set callAlphabet, final Set returnAlphabet, final IStateFactory stateFactory) { + public NestedWordAutomatonCache(final AutomataLibraryServices services, + final VpAlphabet vpAlphabet, + final IStateFactory stateFactory) { mServices = services; mLogger = mServices.getLoggingService().getLogger(LibraryIdentifiers.PLUGIN_ID); - if (internalAlphabet == null) { - throw new IllegalArgumentException("nwa must have internal alphabet"); - } + mVpAlphabet = vpAlphabet; if (stateFactory == null) { throw new IllegalArgumentException("nwa must have stateFactory"); } - mInternalAlphabet = internalAlphabet; - mCallAlphabet = callAlphabet; - mReturnAlphabet = returnAlphabet; mStateFactory = stateFactory; mEmptyStackState = mStateFactory.createEmptyStackState(); } - - @Override - public final Set getInternalAlphabet() { - return mInternalAlphabet; - } - - @Override - public final Set getCallAlphabet() { - return mCallAlphabet == null ? Collections.emptySet() : mCallAlphabet; - } - + @Override - public final Set getReturnAlphabet() { - return mReturnAlphabet == null ? Collections.emptySet() : mReturnAlphabet; + public VpAlphabet getVpAlphabet() { + return mVpAlphabet; } public final Set getStates() { @@ -172,11 +156,6 @@ public final int size() { return mSetOfStates.getStates().size(); } - @Override - public final Set getAlphabet() { - return getInternalAlphabet(); - } - @Override public final Set getInitialStates() { return mSetOfStates.getInitialStates(); @@ -478,7 +457,7 @@ public void addInternalTransition(final STATE pred, final LETTER letter, final S } assert contains(pred) : STATE + pred + NOT_IN_AUTOMATON; assert contains(succ) : STATE + succ + NOT_IN_AUTOMATON; - assert getInternalAlphabet().contains(letter); + assert getVpAlphabet().getInternalAlphabet().contains(letter); mInternalOut.put(pred, letter, succ, IsContained.IsContained); } @@ -491,7 +470,7 @@ public void addInternalTransition(final STATE pred, final LETTER letter, final S * successor states */ public void addInternalTransitions(final STATE pred, final LETTER letter, final Collection succs) { - if (!mInternalAlphabet.contains(letter)) { + if (!getVpAlphabet().getInternalAlphabet().contains(letter)) { throw new IllegalArgumentException("letter" + letter + " not in internal alphabet"); } if (!contains(pred)) { @@ -499,7 +478,7 @@ public void addInternalTransitions(final STATE pred, final LETTER letter, final } assert contains(pred) : STATE + pred + NOT_IN_AUTOMATON; assert assertThatAllStatesAreInAutomaton(succs); - assert getInternalAlphabet().contains(letter); + assert getVpAlphabet().getInternalAlphabet().contains(letter); for (final STATE succ : succs) { addInternalTransition(pred, letter, succ); } @@ -514,13 +493,13 @@ public void addInternalTransitions(final STATE pred, final LETTER letter, final * successor state */ public void addCallTransition(final STATE pred, final LETTER letter, final STATE succ) { - if (!mCallAlphabet.contains(letter)) { + if (!getVpAlphabet().getCallAlphabet().contains(letter)) { throw new IllegalArgumentException("letter" + letter + " not in call alphabet"); } assert contains(pred) : STATE + pred + NOT_IN_AUTOMATON; assert contains(succ) : STATE + succ + NOT_IN_AUTOMATON; - assert getCallAlphabet().contains(letter); + assert getVpAlphabet().getCallAlphabet().contains(letter); mCallOut.put(pred, letter, succ, IsContained.IsContained); } @@ -535,7 +514,7 @@ public void addCallTransition(final STATE pred, final LETTER letter, final STATE public void addCallTransitions(final STATE pred, final LETTER letter, final Collection succs) { assert contains(pred) : STATE + pred + NOT_IN_AUTOMATON; assert assertThatAllStatesAreInAutomaton(succs); - assert getCallAlphabet().contains(letter); + assert getVpAlphabet().getCallAlphabet().contains(letter); for (final STATE succ : succs) { addCallTransition(pred, letter, succ); } @@ -552,14 +531,14 @@ public void addCallTransitions(final STATE pred, final LETTER letter, final Coll * successor state */ public void addReturnTransition(final STATE pred, final STATE hier, final LETTER letter, final STATE succ) { - if (!mReturnAlphabet.contains(letter)) { + if (!getVpAlphabet().getReturnAlphabet().contains(letter)) { throw new IllegalArgumentException("letter" + letter + " not in return alphabet"); } assert contains(pred) : STATE + pred + NOT_IN_AUTOMATON; assert contains(succ) : STATE + succ + NOT_IN_AUTOMATON; assert contains(hier) : STATE + hier + NOT_IN_AUTOMATON; - assert getReturnAlphabet().contains(letter); + assert getVpAlphabet().getReturnAlphabet().contains(letter); mReturnOut.put(pred, hier, letter, succ, IsContained.IsContained); } @@ -578,7 +557,7 @@ public void addReturnTransitions(final STATE pred, final STATE hier, final LETTE assert contains(pred) : STATE + pred + NOT_IN_AUTOMATON; assert assertThatAllStatesAreInAutomaton(succs); assert contains(hier) : STATE + hier + NOT_IN_AUTOMATON; - assert getReturnAlphabet().contains(letter); + assert getVpAlphabet().getReturnAlphabet().contains(letter); for (final STATE succ : succs) { addReturnTransition(pred, hier, letter, succ); } @@ -661,17 +640,17 @@ public final boolean isTotal() { } private boolean isTotal(final STATE state) { - for (final LETTER symbol : getInternalAlphabet()) { + for (final LETTER symbol : getVpAlphabet().getInternalAlphabet()) { if (succInternal(state, symbol).isEmpty()) { return false; } } - for (final LETTER symbol : getCallAlphabet()) { + for (final LETTER symbol : getVpAlphabet().getCallAlphabet()) { if (succCall(state, symbol).isEmpty()) { return false; } } - for (final LETTER symbol : getReturnAlphabet()) { + for (final LETTER symbol : getVpAlphabet().getReturnAlphabet()) { for (final STATE hier : getStates()) { if (succReturn(state, hier, symbol).isEmpty()) { return false; diff --git a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/NestedWordAutomatonFilteredStates.java b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/NestedWordAutomatonFilteredStates.java index 87d405e6b63..09a575789cc 100644 --- a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/NestedWordAutomatonFilteredStates.java +++ b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/NestedWordAutomatonFilteredStates.java @@ -155,20 +155,10 @@ public Set getAlphabet() { public String sizeInformation() { return mRemainingStates.size() + " states."; } - - @Override - public Set getInternalAlphabet() { - return mNwa.getInternalAlphabet(); - } - - @Override - public Set getCallAlphabet() { - return mNwa.getCallAlphabet(); - } - + @Override - public Set getReturnAlphabet() { - return mNwa.getReturnAlphabet(); + public VpAlphabet getVpAlphabet() { + return mNwa.getVpAlphabet(); } @Override diff --git a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/NestedWordAutomatonOnDemandStateAndLetter.java b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/NestedWordAutomatonOnDemandStateAndLetter.java index 5fe33f5a6d2..a01999d75c8 100644 --- a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/NestedWordAutomatonOnDemandStateAndLetter.java +++ b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/NestedWordAutomatonOnDemandStateAndLetter.java @@ -60,6 +60,7 @@ public abstract class NestedWordAutomatonOnDemandStateAndLetter protected final Set mInternalAlphabet; protected final Set mCallAlphabet; protected final Set mReturnAlphabet; + private final VpAlphabet mVpAlphabet; protected boolean mInitialStateHaveBeenConstructed; @@ -84,8 +85,8 @@ public NestedWordAutomatonOnDemandStateAndLetter(final AutomataLibraryServices s mInternalAlphabet = new HashSet<>(); mCallAlphabet = new HashSet<>(); mReturnAlphabet = new HashSet<>(); - mCache = new NestedWordAutomatonCache<>(mServices, mInternalAlphabet, mCallAlphabet, mReturnAlphabet, - stateFactory); + mVpAlphabet = new VpAlphabet<>(mInternalAlphabet, mCallAlphabet, mReturnAlphabet); + mCache = new NestedWordAutomatonCache<>(mServices, mVpAlphabet, stateFactory); } protected abstract void constructInitialStates() throws AutomataOperationCanceledException; @@ -96,28 +97,9 @@ public NestedWordAutomatonOnDemandStateAndLetter(final AutomataLibraryServices s protected abstract void constructReturnSuccessors(STATE lin, STATE hier); - /** - * @see de.uni_freiburg.informatik.ultimate.automata.nestedword.NestedWordAutomatonCache#getInternalAlphabet() - */ - @Override - public Set getInternalAlphabet() { - return mCache.getInternalAlphabet(); - } - - /** - * @see de.uni_freiburg.informatik.ultimate.automata.nestedword.NestedWordAutomatonCache#getCallAlphabet() - */ - @Override - public Set getCallAlphabet() { - return mCache.getCallAlphabet(); - } - - /** - * @see de.uni_freiburg.informatik.ultimate.automata.nestedword.NestedWordAutomatonCache#getReturnAlphabet() - */ @Override - public Set getReturnAlphabet() { - return mCache.getReturnAlphabet(); + public VpAlphabet getVpAlphabet() { + return mVpAlphabet; } /** diff --git a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/TransitionConsistencyCheck.java b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/TransitionConsistencyCheck.java index d416491f288..1939e6de625 100644 --- a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/TransitionConsistencyCheck.java +++ b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/TransitionConsistencyCheck.java @@ -116,7 +116,7 @@ private boolean consistentForState(final STATE state) { result = result && returnSummary(trans.getLinPred(), trans.getHierPred(), trans.getLetter(), state); assert result; } - for (final LETTER letter : mNwa.getReturnAlphabet()) { + for (final LETTER letter : mNwa.getVpAlphabet().getReturnAlphabet()) { for (final SummaryReturnTransition trans : mNwa.summarySuccessors(state, letter)) { result = result && returnIn(trans.getLinPred(), state, trans.getLetter(), trans.getSucc()); assert result; diff --git a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/InCaReAlphabet.java b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/VpAlphabet.java similarity index 54% rename from trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/InCaReAlphabet.java rename to trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/VpAlphabet.java index 18176c1e71e..6ff97018b95 100644 --- a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/InCaReAlphabet.java +++ b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/VpAlphabet.java @@ -32,6 +32,7 @@ import de.uni_freiburg.informatik.ultimate.automata.IAutomaton; /** + * Visibly pushdown Alphabet. * Alphabet consisting of three not necessarily disjoint sets. For visibly pushdown automata a (disjoint) partition into * internal, call, and return alphabets is necessary. For our NestedWordAutomata this segmentation can increase the * performance of operations but is not necessary. @@ -40,7 +41,7 @@ * @param * Type of the Objects that can be used as letters. */ -public class InCaReAlphabet { +public class VpAlphabet { private final Set mInternalAlphabet; private final Set mCallAlphabet; private final Set mReturnAlphabet; @@ -55,12 +56,18 @@ public class InCaReAlphabet { * @param returnAlphabet * return alphabet */ - public InCaReAlphabet(final Set internalAlphabet, final Set callAlphabet, + public VpAlphabet(final Set internalAlphabet, final Set callAlphabet, final Set returnAlphabet) { mInternalAlphabet = internalAlphabet; mCallAlphabet = callAlphabet; mReturnAlphabet = returnAlphabet; } + + public VpAlphabet(final Set internalAlphabet) { + mInternalAlphabet = internalAlphabet; + mCallAlphabet = Collections.emptySet(); + mReturnAlphabet = Collections.emptySet(); + } /** * Constructor which takes the alphabets from an automaton. @@ -68,12 +75,12 @@ public InCaReAlphabet(final Set internalAlphabet, final Set call * @param automaton * automaton */ - public InCaReAlphabet(final IAutomaton automaton) { + public VpAlphabet(final IAutomaton automaton) { if (automaton instanceof INestedWordAutomatonSimple) { final INestedWordAutomatonSimple nwa = (INestedWordAutomatonSimple) automaton; - mInternalAlphabet = nwa.getInternalAlphabet(); - mCallAlphabet = nwa.getCallAlphabet(); - mReturnAlphabet = nwa.getReturnAlphabet(); + mInternalAlphabet = nwa.getVpAlphabet().getInternalAlphabet(); + mCallAlphabet = nwa.getVpAlphabet().getCallAlphabet(); + mReturnAlphabet = nwa.getVpAlphabet().getReturnAlphabet(); } else { mInternalAlphabet = automaton.getAlphabet(); mCallAlphabet = Collections.emptySet(); @@ -81,15 +88,72 @@ public InCaReAlphabet(final IAutomaton automaton) { } } + /** + * @return Set of all letters that can occur as label of an internal transition. + *

+ * The default definition of nested word automata does not allow separate alphabets for internal, call, and + * return symbols. The default definition of visibly pushdown automata requires that all three alphabets are + * disjoint. We deviate from both definitions. We allow separate alphabets but do not require that they are + * disjoint. + */ public Set getInternalAlphabet() { return mInternalAlphabet; } + + /** + * @return Set of all letters that can occur as label of a call transition. + * @see #getInternalAlphabet() + */ public Set getCallAlphabet() { return mCallAlphabet; } + + /** + * @return Set of all letters that can occur as label of a return transition. + * @see #getInternalAlphabet() + */ public Set getReturnAlphabet() { return mReturnAlphabet; } + + @Override + public int hashCode() { + final int prime = 31; + int result = 1; + result = prime * result + ((mCallAlphabet == null) ? 0 : mCallAlphabet.hashCode()); + result = prime * result + ((mInternalAlphabet == null) ? 0 : mInternalAlphabet.hashCode()); + result = prime * result + ((mReturnAlphabet == null) ? 0 : mReturnAlphabet.hashCode()); + return result; + } + + @Override + public boolean equals(final Object obj) { + if (this == obj) + return true; + if (obj == null) + return false; + if (getClass() != obj.getClass()) + return false; + final VpAlphabet other = (VpAlphabet) obj; + if (mCallAlphabet == null) { + if (other.mCallAlphabet != null) + return false; + } else if (!mCallAlphabet.equals(other.mCallAlphabet)) + return false; + if (mInternalAlphabet == null) { + if (other.mInternalAlphabet != null) + return false; + } else if (!mInternalAlphabet.equals(other.mInternalAlphabet)) + return false; + if (mReturnAlphabet == null) { + if (other.mReturnAlphabet != null) + return false; + } else if (!mReturnAlphabet.equals(other.mReturnAlphabet)) + return false; + return true; + } + + } diff --git a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/buchi/BuchiClosureNwa.java b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/buchi/BuchiClosureNwa.java index ea3710bdfc2..ed89448ade6 100644 --- a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/buchi/BuchiClosureNwa.java +++ b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/buchi/BuchiClosureNwa.java @@ -35,6 +35,7 @@ import de.uni_freiburg.informatik.ultimate.automata.LibraryIdentifiers; 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.VpAlphabet; import de.uni_freiburg.informatik.ultimate.automata.nestedword.transitions.IncomingCallTransition; import de.uni_freiburg.informatik.ultimate.automata.nestedword.transitions.IncomingInternalTransition; import de.uni_freiburg.informatik.ultimate.automata.nestedword.transitions.IncomingReturnTransition; @@ -158,20 +159,10 @@ private boolean allSuccessorsAccepting(final STATE state, final Set newFi public Set getInitialStates() { return mOperand.getInitialStates(); } - - @Override - public Set getInternalAlphabet() { - return mOperand.getInternalAlphabet(); - } - - @Override - public Set getCallAlphabet() { - return mOperand.getCallAlphabet(); - } - + @Override - public Set getReturnAlphabet() { - return mOperand.getReturnAlphabet(); + public VpAlphabet getVpAlphabet() { + return mOperand.getVpAlphabet(); } @Override @@ -206,7 +197,7 @@ public Set lettersCall(final STATE state) { @Override public Set lettersReturn(final STATE state, final STATE hier) { - return mOperand.getReturnAlphabet(); + return mOperand.lettersReturn(state, hier); } @Override diff --git a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/buchi/BuchiComplementAutomatonSVW.java b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/buchi/BuchiComplementAutomatonSVW.java index 90efb874814..93c2a6ddb35 100644 --- a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/buchi/BuchiComplementAutomatonSVW.java +++ b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/buchi/BuchiComplementAutomatonSVW.java @@ -43,6 +43,8 @@ import de.uni_freiburg.informatik.ultimate.automata.AutomataOperationCanceledException; import de.uni_freiburg.informatik.ultimate.automata.LibraryIdentifiers; import de.uni_freiburg.informatik.ultimate.automata.nestedword.INestedWordAutomaton; +import de.uni_freiburg.informatik.ultimate.automata.nestedword.VpAlphabet; +import de.uni_freiburg.informatik.ultimate.automata.nestedword.NestedWordAutomataUtils; import de.uni_freiburg.informatik.ultimate.automata.nestedword.NestedWordAutomaton; import de.uni_freiburg.informatik.ultimate.automata.nestedword.transitions.IncomingCallTransition; import de.uni_freiburg.informatik.ultimate.automata.nestedword.transitions.IncomingInternalTransition; @@ -54,6 +56,7 @@ import de.uni_freiburg.informatik.ultimate.automata.statefactory.IBuchiComplementSvwStateFactory; import de.uni_freiburg.informatik.ultimate.automata.statefactory.IEmptyStackStateFactory; import de.uni_freiburg.informatik.ultimate.automata.statefactory.IStateFactory; +import de.uni_freiburg.informatik.ultimate.core.model.models.IElement; import de.uni_freiburg.informatik.ultimate.core.model.services.ILogger; /** @@ -77,7 +80,7 @@ public class BuchiComplementAutomatonSVW implements INestedWordAu protected final STATE mEmptyStackState; protected final AutomataLibraryServices mServices; private final TransitionMonoidAutomaton mTma; - private final Set mAlphabet; + private final VpAlphabet mVpAlphabet; private SizeInfoContainer mSizeInfo; // not all transitions have been computed private boolean mBuildCompleted; @@ -107,8 +110,8 @@ public & IEmptyStackStat mServices = services; mLogger = mServices.getLoggingService().getLogger(LibraryIdentifiers.PLUGIN_ID); mTma = new TransitionMonoidAutomaton(operand); - mAlphabet = operand.getInternalAlphabet(); - if (!operand.getCallAlphabet().isEmpty() || !operand.getReturnAlphabet().isEmpty()) { + mVpAlphabet = operand.getVpAlphabet(); + if (!NestedWordAutomataUtils.isFiniteAutomaton(operand)) { throw new IllegalArgumentException("only applicable to Buchi automata (not BuchiNWA)"); } mStateFactory = stateFactory; @@ -126,7 +129,7 @@ public & IEmptyStackStat */ public INestedWordAutomaton toNestedWordAutomaton() throws AutomataOperationCanceledException { final NestedWordAutomaton result = - new NestedWordAutomaton<>(mServices, mAlphabet, null, null, mStateFactory); + new NestedWordAutomaton<>(mServices, mVpAlphabet, mStateFactory); final int size = getSizeInfo().mTotalSize; // Breadth-first traversal of the state space. final Set alreadySeen = new HashSet<>(size); @@ -136,7 +139,7 @@ public INestedWordAutomaton toNestedWordAutomaton() throws Automa result.addState(true, false, mInitialState); while (!queue.isEmpty()) { final STATE state = queue.remove(); - for (final LETTER letter : mAlphabet) { + for (final LETTER letter : getAlphabet()) { final Collection succSet = succInternal(state, letter); for (final STATE succState : succSet) { addIfNotContained1(result, alreadySeen, queue, succState); @@ -157,11 +160,6 @@ public int size() { return getSizeInfo().mTotalSize; } - @Override - public Set getAlphabet() { - return mAlphabet; - } - @Override public String sizeInformation() { final SizeInfoContainer sizeInfo = getSizeInfo(); @@ -178,11 +176,6 @@ public String sizeInformation() { return sb.toString(); } - @Override - public Set getInternalAlphabet() { - return mAlphabet; - } - @Override public IStateFactory getStateFactory() { return mStateFactory; @@ -201,7 +194,7 @@ public Set getStates() { queue.add(mInitialState); while (!queue.isEmpty()) { final STATE state = queue.remove(); - for (final LETTER letter : mAlphabet) { + for (final LETTER letter : getAlphabet()) { final Collection succSet = succInternal(state, letter); for (final STATE succState : succSet) { addIfNotContained2(alreadySeen, queue, succState); @@ -267,7 +260,7 @@ public Set lettersInternal(final STATE state) { if (!knows(state)) { throw new IllegalArgumentException(STATE_STRING + state + IS_NOT_YET_KNOWN); } - return mAlphabet; + return getAlphabet(); } @Override @@ -276,7 +269,7 @@ public Set lettersInternalIncoming(final STATE state) { throw new IllegalArgumentException(STATE_STRING + state + IS_NOT_YET_KNOWN); } final Set result = new HashSet<>(); - for (final LETTER letter : mAlphabet) { + for (final LETTER letter : getAlphabet()) { final Collection predStateSet = predInternal(state, letter); if (!predStateSet.isEmpty()) { result.add(letter); @@ -294,7 +287,7 @@ private Collection succInternal(final STATE state, final LETTER letter) { Set result = map.get(letter); // If the result is not in the map, compute it. if (result == null) { - if (!mAlphabet.contains(letter)) { + if (!getAlphabet().contains(letter)) { throw new IllegalArgumentException("Letter " + letter + " is not in the alphabet."); } final MetaState mState = getMetaState2(state); @@ -341,7 +334,7 @@ private Collection predInternal(final STATE state, final LETTER letter) { if (result != null) { return result; } - if (!mAlphabet.contains(letter)) { + if (!getAlphabet().contains(letter)) { throw new IllegalArgumentException("Letter " + letter + " is not in the alphabet."); } final MetaState mState = getMetaState2(state); @@ -428,22 +421,6 @@ private static boolean isTotal() { // --------------------------------------------------------------------- } - @Override - public Set getCallAlphabet() { - if (mLogger.isWarnEnabled()) { - mLogger.warn("No nwa. Has no call alphabet."); - } - return Collections.emptySet(); - } - - @Override - public Set getReturnAlphabet() { - if (mLogger.isWarnEnabled()) { - mLogger.warn("No nwa. Has no return alphabet."); - } - return Collections.emptySet(); - } - @Override public Set lettersCall(final STATE state) { // mLogger.warn("No nwa. Has no call alphabet."); @@ -748,7 +725,7 @@ private class TransitionMonoidAutomaton { public TransitionMonoidAutomaton(final INestedWordAutomaton origAutomaton) throws AutomataOperationCanceledException { mOrigAutomaton = origAutomaton; - final Collection alphabet = origAutomaton.getInternalAlphabet(); + final Collection alphabet = origAutomaton.getVpAlphabet().getInternalAlphabet(); // Map from numbers to corresponding transition profiles final Map mapNum2Tp = new HashMap<>(); @@ -1094,4 +1071,16 @@ public boolean equals(final Object obj) { } } } + + @Override + public VpAlphabet getVpAlphabet() { + return mVpAlphabet; + } + + @Override + public IElement transformToUltimateModel(final AutomataLibraryServices services) + throws AutomataOperationCanceledException { + // TODO Auto-generated method stub + return null; + } } diff --git a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/buchi/BuchiComplementDeterministic.java b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/buchi/BuchiComplementDeterministic.java index 18a105e62f0..4bb549acf8b 100644 --- a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/buchi/BuchiComplementDeterministic.java +++ b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/buchi/BuchiComplementDeterministic.java @@ -99,8 +99,7 @@ public BuchiComplementDeterministic(final AutomataLibraryServices services, } else { mTotalizedOperand = new ReachableStatesCopy<>(mServices, operand, true, false, false, false).getResult(); } - mTraversedNwa = new NestedWordAutomaton<>(mServices, operand.getInternalAlphabet(), operand.getCallAlphabet(), - operand.getReturnAlphabet(), operand.getStateFactory()); + mTraversedNwa = new NestedWordAutomaton<>(mServices, operand.getVpAlphabet(), operand.getStateFactory()); traverseDoubleDeckerGraph(); if (mLogger.isInfoEnabled()) { diff --git a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/buchi/BuchiComplementFKVNwa.java b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/buchi/BuchiComplementFKVNwa.java index abc18074300..68897fda76f 100644 --- a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/buchi/BuchiComplementFKVNwa.java +++ b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/buchi/BuchiComplementFKVNwa.java @@ -36,6 +36,7 @@ import de.uni_freiburg.informatik.ultimate.automata.AutomataOperationCanceledException; import de.uni_freiburg.informatik.ultimate.automata.LibraryIdentifiers; import de.uni_freiburg.informatik.ultimate.automata.nestedword.INestedWordAutomatonSimple; +import de.uni_freiburg.informatik.ultimate.automata.nestedword.VpAlphabet; import de.uni_freiburg.informatik.ultimate.automata.nestedword.NestedWordAutomatonCache; import de.uni_freiburg.informatik.ultimate.automata.nestedword.buchi.MultiOptimizationLevelRankingGenerator.FkvOptimization; import de.uni_freiburg.informatik.ultimate.automata.nestedword.operations.IStateDeterminizer; @@ -139,8 +140,7 @@ public BuchiComplementFKVNwa(final AutomataLibraryServices services, mLogger = mServices.getLoggingService().getLogger(LibraryIdentifiers.PLUGIN_ID); mOperand = operand; mStateFactory = stateFactory; - mCache = new NestedWordAutomatonCache<>(mServices, operand.getInternalAlphabet(), operand.getCallAlphabet(), - operand.getReturnAlphabet(), mStateFactory); + mCache = new NestedWordAutomatonCache<>(mServices, operand.getVpAlphabet(), mStateFactory); mStateDeterminizer = stateDeterminizer; mUserDefinedMaxRank = userDefinedMaxRank; mLevelRankingGenerator = @@ -221,18 +221,8 @@ public Iterable getInitialStates() { } @Override - public Set getInternalAlphabet() { - return mOperand.getInternalAlphabet(); - } - - @Override - public Set getCallAlphabet() { - return mOperand.getCallAlphabet(); - } - - @Override - public Set getReturnAlphabet() { - return mOperand.getReturnAlphabet(); + public VpAlphabet getVpAlphabet() { + return mOperand.getVpAlphabet(); } @Override @@ -257,17 +247,17 @@ public STATE getEmptyStackState() { @Override public Set lettersInternal(final STATE state) { - return mOperand.getInternalAlphabet(); + return mOperand.getVpAlphabet().getInternalAlphabet(); } @Override public Set lettersCall(final STATE state) { - return mOperand.getCallAlphabet(); + return mOperand.getVpAlphabet().getCallAlphabet(); } @Override public Set lettersReturn(final STATE state, final STATE hier) { - return mOperand.getReturnAlphabet(); + return mOperand.getVpAlphabet().getReturnAlphabet(); } @Override @@ -297,7 +287,7 @@ public Iterable> internalSuccessors(fi @Override public Iterable> internalSuccessors(final STATE state) { - for (final LETTER letter : getInternalAlphabet()) { + for (final LETTER letter : getVpAlphabet().getInternalAlphabet()) { internalSuccessors(state, letter); } return mCache.internalSuccessors(state); @@ -350,7 +340,7 @@ public Iterable> callSuccessors(final STAT @Override public Iterable> callSuccessors(final STATE state) { - for (final LETTER letter : getCallAlphabet()) { + for (final LETTER letter : getVpAlphabet().getCallAlphabet()) { callSuccessors(state, letter); } return mCache.callSuccessors(state); @@ -430,7 +420,7 @@ private LevelRankingConstraint getLevelRankingConstraintDrdCheck( @Override public Iterable> returnSuccessorsGivenHier(final STATE state, final STATE hier) { - for (final LETTER letter : getReturnAlphabet()) { + for (final LETTER letter : getVpAlphabet().getReturnAlphabet()) { returnSuccessors(state, hier, letter); } return mCache.returnSuccessorsGivenHier(state, hier); diff --git a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/buchi/BuchiComplementNCSBNwa.java b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/buchi/BuchiComplementNCSBNwa.java index 03a97b8bfdb..6211e28661c 100644 --- a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/buchi/BuchiComplementNCSBNwa.java +++ b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/buchi/BuchiComplementNCSBNwa.java @@ -32,11 +32,11 @@ import java.util.HashMap; import java.util.List; import java.util.Map; -import java.util.Set; import de.uni_freiburg.informatik.ultimate.automata.AutomataLibraryServices; import de.uni_freiburg.informatik.ultimate.automata.AutomataOperationCanceledException; import de.uni_freiburg.informatik.ultimate.automata.nestedword.INestedWordAutomatonSimple; +import de.uni_freiburg.informatik.ultimate.automata.nestedword.VpAlphabet; import de.uni_freiburg.informatik.ultimate.automata.nestedword.NestedWordAutomatonCache; import de.uni_freiburg.informatik.ultimate.automata.nestedword.transitions.OutgoingCallTransition; import de.uni_freiburg.informatik.ultimate.automata.nestedword.transitions.OutgoingInternalTransition; @@ -106,8 +106,7 @@ public BuchiComplementNCSBNwa(final AutomataLibraryServices services, mServices = services; mOperand = operand; mStateFactory = stateFactory; - mCache = new NestedWordAutomatonCache<>(mServices, operand.getInternalAlphabet(), operand.getCallAlphabet(), - operand.getReturnAlphabet(), mStateFactory); + mCache = new NestedWordAutomatonCache<>(mServices, operand.getVpAlphabet(), mStateFactory); mEmptyStackStateWri = new StateWithRankInfo<>(getEmptyStackState()); mBclrg = new BarelyCoveredLevelRankingsGenerator<>(mServices, mOperand, BARELY_COVERED_MAX_RANK, false, true, false, false, false); @@ -149,18 +148,8 @@ public Iterable getInitialStates() { } @Override - public Set getInternalAlphabet() { - return mOperand.getInternalAlphabet(); - } - - @Override - public Set getCallAlphabet() { - return mOperand.getCallAlphabet(); - } - - @Override - public Set getReturnAlphabet() { - return mOperand.getReturnAlphabet(); + public VpAlphabet getVpAlphabet() { + return mOperand.getVpAlphabet(); } @Override diff --git a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/buchi/BuchiIntersectNwa.java b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/buchi/BuchiIntersectNwa.java index b697dd15925..62549f43e9a 100644 --- a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/buchi/BuchiIntersectNwa.java +++ b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/buchi/BuchiIntersectNwa.java @@ -35,6 +35,7 @@ import de.uni_freiburg.informatik.ultimate.automata.AutomataLibraryException; import de.uni_freiburg.informatik.ultimate.automata.nestedword.INestedWordAutomatonSimple; +import de.uni_freiburg.informatik.ultimate.automata.nestedword.VpAlphabet; import de.uni_freiburg.informatik.ultimate.automata.nestedword.NestedWordAutomataUtils; import de.uni_freiburg.informatik.ultimate.automata.nestedword.transitions.OutgoingCallTransition; import de.uni_freiburg.informatik.ultimate.automata.nestedword.transitions.OutgoingInternalTransition; @@ -163,18 +164,8 @@ public Iterable getInitialStates() { } @Override - public Set getInternalAlphabet() { - return mFstOperand.getInternalAlphabet(); - } - - @Override - public Set getCallAlphabet() { - return mFstOperand.getCallAlphabet(); - } - - @Override - public Set getReturnAlphabet() { - return mFstOperand.getReturnAlphabet(); + public VpAlphabet getVpAlphabet() { + return mFstOperand.getVpAlphabet(); } @Override @@ -341,10 +332,6 @@ public int size() { return 0; } - @Override - public Set getAlphabet() { - return getInternalAlphabet(); - } @Override public String sizeInformation() { diff --git a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/buchi/BuchiIsEmptyXW.java b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/buchi/BuchiIsEmptyXW.java index 8b988a37ea6..bcfbb9204b6 100644 --- a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/buchi/BuchiIsEmptyXW.java +++ b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/buchi/BuchiIsEmptyXW.java @@ -161,8 +161,8 @@ public boolean checkEmptiness() throws AutomataOperationCanceledException { final Set allStates = new HashSet<>(); final Set acceptingStates = new HashSet<>(); final Set initialStates = new HashSet<>(); - final Collection callAlphabet = mOperand.getCallAlphabet(); - final Collection returnAlphabet = mOperand.getReturnAlphabet(); + final Collection callAlphabet = mOperand.getVpAlphabet().getCallAlphabet(); + final Collection returnAlphabet = mOperand.getVpAlphabet().getReturnAlphabet(); // Get all states and accepting states // TODO: xw: check the consequence of casting diff --git a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/AbstractAcceptance.java b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/AbstractAcceptance.java index 01317737917..fc8c9720e56 100644 --- a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/AbstractAcceptance.java +++ b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/AbstractAcceptance.java @@ -148,7 +148,7 @@ protected Set> successorConfigurations(final Set nwa, final Set> succConfigs, final ArrayDeque config, final STATE state, final LETTER symbol) throws AutomataLibraryException { - if (!nwa.getInternalAlphabet().contains(symbol)) { + if (!nwa.getVpAlphabet().getInternalAlphabet().contains(symbol)) { throw new AutomataLibraryException(this.getClass(), UNABLE_TO_CHECK_ACCEPTANCE_LETTER + symbol + AT_POSITION + position + " not in internal alphabet of automaton."); } @@ -165,7 +165,7 @@ private void successorConfigurationsInternal(final int position, private void successorConfigurationsCall(final int position, final INestedWordAutomatonSimple nwa, final Set> succConfigs, final ArrayDeque config, final STATE state, final LETTER symbol) throws AutomataLibraryException { - if (!nwa.getCallAlphabet().contains(symbol)) { + if (!nwa.getVpAlphabet().getCallAlphabet().contains(symbol)) { throw new AutomataLibraryException(this.getClass(), UNABLE_TO_CHECK_ACCEPTANCE_LETTER + symbol + AT_POSITION + position + " not in call alphabet of automaton."); } @@ -182,7 +182,7 @@ private void successorConfigurationsCall(final int position, final INestedWordAu private void successorConfigurationsReturn(final int position, final INestedWordAutomatonSimple nwa, final Set> succConfigs, final ArrayDeque config, final STATE state, final LETTER symbol) throws AutomataLibraryException { - if (!nwa.getReturnAlphabet().contains(symbol)) { + if (!nwa.getVpAlphabet().getReturnAlphabet().contains(symbol)) { throw new AutomataLibraryException(this.getClass(), UNABLE_TO_CHECK_ACCEPTANCE_LETTER + symbol + AT_POSITION + position + " not in return alphabet of automaton."); } diff --git a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/Analyze.java b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/Analyze.java index 3b84dd17a16..dc1b467d67e 100644 --- a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/Analyze.java +++ b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/Analyze.java @@ -316,9 +316,9 @@ private final void computeNumberOfStates() { } private final void computeNumberOfSymbols() { - mNumberOfInternalSymbols = mOperand.getInternalAlphabet().size(); - mNumberOfCallSymbols = mOperand.getCallAlphabet().size(); - mNumberOfReturnSymbols = mOperand.getReturnAlphabet().size(); + mNumberOfInternalSymbols = mOperand.getVpAlphabet().getInternalAlphabet().size(); + mNumberOfCallSymbols = mOperand.getVpAlphabet().getCallAlphabet().size(); + mNumberOfReturnSymbols = mOperand.getVpAlphabet().getReturnAlphabet().size(); mNumberOfSymbolsComputed = true; } diff --git a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/ComplementDeterministicNwa.java b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/ComplementDeterministicNwa.java index ac07851e365..b26896fac35 100644 --- a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/ComplementDeterministicNwa.java +++ b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/ComplementDeterministicNwa.java @@ -29,6 +29,7 @@ import java.util.Set; import de.uni_freiburg.informatik.ultimate.automata.nestedword.INestedWordAutomatonSimple; +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; @@ -75,18 +76,8 @@ public Iterable getInitialStates() { } @Override - public Set getInternalAlphabet() { - return mOperand.getInternalAlphabet(); - } - - @Override - public Set getCallAlphabet() { - return mOperand.getCallAlphabet(); - } - - @Override - public Set getReturnAlphabet() { - return mOperand.getReturnAlphabet(); + public VpAlphabet getVpAlphabet() { + return mOperand.getVpAlphabet(); } @Override @@ -111,17 +102,17 @@ public STATE getEmptyStackState() { @Override public Set lettersInternal(final STATE state) { - return mOperand.getInternalAlphabet(); + return mOperand.getVpAlphabet().getInternalAlphabet(); } @Override public Set lettersCall(final STATE state) { - return mOperand.getCallAlphabet(); + return mOperand.getVpAlphabet().getCallAlphabet(); } @Override public Set lettersReturn(final STATE state, final STATE hier) { - return mOperand.getReturnAlphabet(); + return mOperand.getVpAlphabet().getReturnAlphabet(); } @Override diff --git a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/ConcurrentProduct.java b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/ConcurrentProduct.java index fa2fe0135bb..4d26d5553cf 100644 --- a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/ConcurrentProduct.java +++ b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/ConcurrentProduct.java @@ -36,6 +36,8 @@ import de.uni_freiburg.informatik.ultimate.automata.nestedword.BinaryNwaOperation; import de.uni_freiburg.informatik.ultimate.automata.nestedword.INestedWordAutomaton; import de.uni_freiburg.informatik.ultimate.automata.nestedword.INestedWordAutomatonSimple; +import de.uni_freiburg.informatik.ultimate.automata.nestedword.VpAlphabet; +import de.uni_freiburg.informatik.ultimate.automata.nestedword.NestedWordAutomataUtils; import de.uni_freiburg.informatik.ultimate.automata.nestedword.NestedWordAutomaton; import de.uni_freiburg.informatik.ultimate.automata.nestedword.transitions.OutgoingInternalTransition; import de.uni_freiburg.informatik.ultimate.automata.statefactory.IConcurrentProductStateFactory; @@ -114,16 +116,16 @@ public ConcurrentProduct(final AutomataLibraryServices services, */ if (mLogger.isWarnEnabled() - && (!fstOperand.getCallAlphabet().isEmpty() || !fstOperand.getReturnAlphabet().isEmpty() - || !sndOperand.getCallAlphabet().isEmpty() || !sndOperand.getReturnAlphabet().isEmpty())) { + && (!NestedWordAutomataUtils.isFiniteAutomaton(fstOperand) + || !NestedWordAutomataUtils.isFiniteAutomaton(sndOperand))) { mLogger.warn("Call alphabet and return alphabet are ignored."); } - mSynchronizationAlphabet = new HashSet<>(fstOperand.getInternalAlphabet()); - mSynchronizationAlphabet.retainAll(sndOperand.getInternalAlphabet()); - final Set commonAlphabet = new HashSet<>(fstOperand.getInternalAlphabet()); - commonAlphabet.addAll(sndOperand.getInternalAlphabet()); + mSynchronizationAlphabet = new HashSet<>(fstOperand.getAlphabet()); + mSynchronizationAlphabet.retainAll(sndOperand.getAlphabet()); + final Set commonAlphabet = new HashSet<>(fstOperand.getAlphabet()); + commonAlphabet.addAll(sndOperand.getAlphabet()); // TODO Christian 2016-09-04: Use Collections.emptySet() or is it intended that a user modifies the result? - mResult = new NestedWordAutomaton<>(mServices, commonAlphabet, new HashSet(0), new HashSet(0), + mResult = new NestedWordAutomaton<>(mServices, new VpAlphabet<>(commonAlphabet), mContentFactory); constructInitialStates(); while (!mWorklist.isEmpty()) { diff --git a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/DeterminizeNwa.java b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/DeterminizeNwa.java index b79a5f55d8d..2e4713bc619 100644 --- a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/DeterminizeNwa.java +++ b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/DeterminizeNwa.java @@ -34,6 +34,7 @@ import de.uni_freiburg.informatik.ultimate.automata.AutomataLibraryServices; import de.uni_freiburg.informatik.ultimate.automata.nestedword.INestedWordAutomatonSimple; +import de.uni_freiburg.informatik.ultimate.automata.nestedword.VpAlphabet; import de.uni_freiburg.informatik.ultimate.automata.nestedword.NestedWordAutomaton; import de.uni_freiburg.informatik.ultimate.automata.nestedword.operations.oldapi.DeterminizedState; import de.uni_freiburg.informatik.ultimate.automata.nestedword.transitions.OutgoingCallTransition; @@ -102,8 +103,7 @@ public DeterminizeNwa(final AutomataLibraryServices services, mOperand = operand; mStateDeterminizer = stateDeterminizer; mStateFactory = stateFactory; - mCache = new NestedWordAutomaton<>(services, operand.getInternalAlphabet(), operand.getCallAlphabet(), - operand.getReturnAlphabet(), stateFactory); + mCache = new NestedWordAutomaton<>(services, operand.getVpAlphabet(), stateFactory); mPredefinedInitials = predefinedInitials; mMakeAutomatonTotal = makeAutomatonTotal; } @@ -152,23 +152,8 @@ public Iterable getInitialStates() { } @Override - public Set getAlphabet() { - return getInternalAlphabet(); - } - - @Override - public Set getInternalAlphabet() { - return mCache.getInternalAlphabet(); - } - - @Override - public Set getCallAlphabet() { - return mCache.getCallAlphabet(); - } - - @Override - public Set getReturnAlphabet() { - return mCache.getReturnAlphabet(); + public VpAlphabet getVpAlphabet() { + return mCache.getVpAlphabet(); } @Override @@ -194,7 +179,7 @@ public STATE getEmptyStackState() { @Override public Set lettersInternal(final STATE state) { if (mMakeAutomatonTotal) { - return getInternalAlphabet(); + return getVpAlphabet().getInternalAlphabet(); } final Set result = new HashSet<>(); final DeterminizedState detState = mRes2det.get(state); @@ -209,7 +194,7 @@ public Set lettersInternal(final STATE state) { @Override public Set lettersCall(final STATE state) { if (mMakeAutomatonTotal) { - return getCallAlphabet(); + return getVpAlphabet().getCallAlphabet(); } final Set result = new HashSet<>(); final DeterminizedState detState = mRes2det.get(state); @@ -224,7 +209,7 @@ public Set lettersCall(final STATE state) { @Override public Set lettersReturn(final STATE state, final STATE hier) { if (mMakeAutomatonTotal) { - return getReturnAlphabet(); + return getVpAlphabet().getReturnAlphabet(); } final Set result = new HashSet<>(); final DeterminizedState detState = mRes2det.get(state); diff --git a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/GetRandomDfa.java b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/GetRandomDfa.java index b5650d9daa1..697b0d68b11 100644 --- a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/GetRandomDfa.java +++ b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/GetRandomDfa.java @@ -42,6 +42,7 @@ import de.uni_freiburg.informatik.ultimate.automata.AutomataLibraryServices; import de.uni_freiburg.informatik.ultimate.automata.GeneralOperation; import de.uni_freiburg.informatik.ultimate.automata.nestedword.INestedWordAutomaton; +import de.uni_freiburg.informatik.ultimate.automata.nestedword.VpAlphabet; import de.uni_freiburg.informatik.ultimate.automata.nestedword.NestedWordAutomaton; import de.uni_freiburg.informatik.ultimate.automata.statefactory.IStateFactory; import de.uni_freiburg.informatik.ultimate.automata.statefactory.StringFactory; @@ -684,7 +685,7 @@ private INestedWordAutomaton extractPackedDfa(final int[] dfa, f } final NestedWordAutomaton result = - new NestedWordAutomaton<>(mServices, new HashSet<>(num2Letter), null, null, new StringFactory()); + new NestedWordAutomaton<>(mServices, new VpAlphabet(new HashSet<>(num2Letter)), new StringFactory()); // Create states for (int i = 0; i < mSize; ++i) { diff --git a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/GetRandomNestedWord.java b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/GetRandomNestedWord.java index 7070d17e68e..cd043a870c7 100644 --- a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/GetRandomNestedWord.java +++ b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/GetRandomNestedWord.java @@ -72,9 +72,9 @@ public class GetRandomNestedWord implements IOperation nwa, final int length, final long seed) { - mInternalAlphabet = new ArrayList<>(nwa.getInternalAlphabet()); - mCallAlphabet = new ArrayList<>(nwa.getCallAlphabet()); - mReturnAlphabet = new ArrayList<>(nwa.getReturnAlphabet()); + mInternalAlphabet = new ArrayList<>(nwa.getVpAlphabet().getInternalAlphabet()); + mCallAlphabet = new ArrayList<>(nwa.getVpAlphabet().getCallAlphabet()); + mReturnAlphabet = new ArrayList<>(nwa.getVpAlphabet().getReturnAlphabet()); mRandom = new Random(seed); final int sum = mInternalAlphabet.size() + mCallAlphabet.size() + mReturnAlphabet.size(); diff --git a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/GetRandomNwa.java b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/GetRandomNwa.java index bf0f5e06864..03250ee3c87 100644 --- a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/GetRandomNwa.java +++ b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/GetRandomNwa.java @@ -38,6 +38,7 @@ import de.uni_freiburg.informatik.ultimate.automata.AutomataLibraryServices; import de.uni_freiburg.informatik.ultimate.automata.GeneralOperation; import de.uni_freiburg.informatik.ultimate.automata.nestedword.INestedWordAutomaton; +import de.uni_freiburg.informatik.ultimate.automata.nestedword.VpAlphabet; import de.uni_freiburg.informatik.ultimate.automata.nestedword.NestedWordAutomaton; import de.uni_freiburg.informatik.ultimate.automata.statefactory.IStateFactory; import de.uni_freiburg.informatik.ultimate.automata.statefactory.StringFactory; @@ -212,10 +213,10 @@ private INestedWordAutomaton generateAutomaton() { @SuppressWarnings("squid:S1244") final boolean isFiniteAutomaton = mCallTransitionDensity == 0D && mReturnTransitionDensity == 0D; if (isFiniteAutomaton) { - result = new NestedWordAutomaton<>(mServices, new HashSet<>(num2Letter), null, null, new StringFactory()); + result = new NestedWordAutomaton<>(mServices, new VpAlphabet<>(new HashSet<>(num2Letter)), new StringFactory()); } else { - result = new NestedWordAutomaton<>(mServices, new HashSet<>(num2Letter), new HashSet<>(num2Letter), - new HashSet<>(num2Letter), new StringFactory()); + result = new NestedWordAutomaton<>(mServices, new VpAlphabet<>(new HashSet<>(num2Letter), new HashSet<>(num2Letter), + new HashSet<>(num2Letter)), new StringFactory()); } // -------------------------------------------------------------------- diff --git a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/GetRandomNwaTv.java b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/GetRandomNwaTv.java index fbf6ff8d69f..a299a6f6fc8 100644 --- a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/GetRandomNwaTv.java +++ b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/GetRandomNwaTv.java @@ -34,6 +34,7 @@ import de.uni_freiburg.informatik.ultimate.automata.AutomataLibraryServices; import de.uni_freiburg.informatik.ultimate.automata.GeneralOperation; import de.uni_freiburg.informatik.ultimate.automata.nestedword.INestedWordAutomaton; +import de.uni_freiburg.informatik.ultimate.automata.nestedword.VpAlphabet; import de.uni_freiburg.informatik.ultimate.automata.nestedword.NestedWordAutomaton; import de.uni_freiburg.informatik.ultimate.automata.statefactory.IStateFactory; import de.uni_freiburg.informatik.ultimate.automata.statefactory.StringFactory; @@ -393,8 +394,8 @@ private NestedWordAutomaton generateAutomaton(final long seed) { final Set returnAlphabet = new HashSet<>(mNumberOfInternalLetters); // create raw automaton - final NestedWordAutomaton result = new NestedWordAutomaton<>(mServices, internalAlphabet, - callAlphabet, returnAlphabet, new StringFactory()); + final NestedWordAutomaton result = new NestedWordAutomaton<>(mServices, new VpAlphabet<>(internalAlphabet, + callAlphabet, returnAlphabet), new StringFactory()); if (mNumberOfStates == 0) { // empty automaton diff --git a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/IntersectNwa.java b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/IntersectNwa.java index 43317c9fe96..8f4d724424c 100644 --- a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/IntersectNwa.java +++ b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/IntersectNwa.java @@ -35,6 +35,7 @@ import de.uni_freiburg.informatik.ultimate.automata.AutomataLibraryException; import de.uni_freiburg.informatik.ultimate.automata.nestedword.INestedWordAutomatonSimple; +import de.uni_freiburg.informatik.ultimate.automata.nestedword.VpAlphabet; import de.uni_freiburg.informatik.ultimate.automata.nestedword.NestedWordAutomataUtils; import de.uni_freiburg.informatik.ultimate.automata.nestedword.transitions.OutgoingCallTransition; import de.uni_freiburg.informatik.ultimate.automata.nestedword.transitions.OutgoingInternalTransition; @@ -138,18 +139,8 @@ public Iterable getInitialStates() { } @Override - public Set getInternalAlphabet() { - return mFstOperand.getInternalAlphabet(); - } - - @Override - public Set getCallAlphabet() { - return mFstOperand.getCallAlphabet(); - } - - @Override - public Set getReturnAlphabet() { - return mFstOperand.getReturnAlphabet(); + public VpAlphabet getVpAlphabet() { + return mFstOperand.getVpAlphabet(); } @Override @@ -316,10 +307,6 @@ public int size() { return mRes2prod.size(); } - @Override - public Set getAlphabet() { - return getInternalAlphabet(); - } @Override public String sizeInformation() { diff --git a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/IsTotal.java b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/IsTotal.java index 17cd699490b..10ab21d5658 100644 --- a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/IsTotal.java +++ b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/IsTotal.java @@ -87,7 +87,7 @@ private boolean computeIsTotal() { */ private boolean isTotal(final STATE state) { // internals - for (final LETTER symbol : mOperand.getInternalAlphabet()) { + for (final LETTER symbol : mOperand.getVpAlphabet().getInternalAlphabet()) { final Iterable> it = mOperand.internalSuccessors(state, symbol); if (!it.iterator().hasNext()) { return false; @@ -95,7 +95,7 @@ private boolean isTotal(final STATE state) { } // calls - for (final LETTER symbol : mOperand.getCallAlphabet()) { + for (final LETTER symbol : mOperand.getVpAlphabet().getCallAlphabet()) { final Iterable> it = mOperand.callSuccessors(state, symbol); if (!it.iterator().hasNext()) { return false; @@ -103,7 +103,7 @@ private boolean isTotal(final STATE state) { } // returns - for (final LETTER symbol : mOperand.getReturnAlphabet()) { + for (final LETTER symbol : mOperand.getVpAlphabet().getReturnAlphabet()) { for (final STATE hier : mOperand.getStates()) { // TODO Christian 2016-09-18: Is this what we want? How can we check that 'hier' is a valid candidate? final Iterable> it = diff --git a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/LoopComplexity.java b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/LoopComplexity.java index a04098043c7..1ac89275a95 100644 --- a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/LoopComplexity.java +++ b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/LoopComplexity.java @@ -39,6 +39,7 @@ import de.uni_freiburg.informatik.ultimate.automata.nestedword.AutomatonSccComputation; import de.uni_freiburg.informatik.ultimate.automata.nestedword.INestedWordAutomaton; import de.uni_freiburg.informatik.ultimate.automata.nestedword.INestedWordAutomatonSimple; +import de.uni_freiburg.informatik.ultimate.automata.nestedword.VpAlphabet; import de.uni_freiburg.informatik.ultimate.automata.nestedword.NestedWordAutomaton; import de.uni_freiburg.informatik.ultimate.automata.nestedword.UnaryNwaOperation; import de.uni_freiburg.informatik.ultimate.automata.nestedword.reachablestates.NestedWordAutomatonReachableStates; @@ -110,10 +111,11 @@ public LoopComplexity(final AutomataLibraryServices services, final INestedWordA */ private NestedWordAutomatonReachableStates constructGraph() throws AutomataOperationCanceledException { - final LETTER letter = mOperand.getInternalAlphabet().iterator().next(); + final LETTER letter = mOperand.getVpAlphabet().getInternalAlphabet().iterator().next(); final Set singletonAlphabet = Collections.singleton(letter); - final NestedWordAutomaton graph = new NestedWordAutomaton<>(mServices, singletonAlphabet, - singletonAlphabet, singletonAlphabet, mOperand.getStateFactory()); + final NestedWordAutomaton graph = new NestedWordAutomaton<>(mServices, + new VpAlphabet<>(singletonAlphabet, singletonAlphabet, singletonAlphabet), + mOperand.getStateFactory()); for (final STATE state : mOperand.getStates()) { graph.addState(true, true, state); diff --git a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/SuperDifference.java b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/SuperDifference.java index 02b8e373c2f..190c0ce0fd9 100644 --- a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/SuperDifference.java +++ b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/SuperDifference.java @@ -113,8 +113,7 @@ public SuperDifference(final AutomataLibraryServices services, final INestedWord } // initialize the result with the empty automaton - mResult = new NestedWordAutomaton<>(mServices, minuend.getInternalAlphabet(), minuend.getCallAlphabet(), - minuend.getReturnAlphabet(), mStateFactory); + mResult = new NestedWordAutomaton<>(mServices, minuend.getVpAlphabet(), mStateFactory); mSinkState = sinkStateFactory.createSinkStateContent(); if (mLogger.isDebugEnabled()) { mLogger.debug("Created Sink-State: " + mSinkState.toString()); diff --git a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/TotalizeNwa.java b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/TotalizeNwa.java index ab2ce4a4780..13308a6d317 100644 --- a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/TotalizeNwa.java +++ b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/TotalizeNwa.java @@ -34,6 +34,7 @@ import de.uni_freiburg.informatik.ultimate.automata.nestedword.INestedWordAutomaton; import de.uni_freiburg.informatik.ultimate.automata.nestedword.INestedWordAutomatonSimple; +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; @@ -141,18 +142,8 @@ public Iterable getInitialStates() { } @Override - public Set getInternalAlphabet() { - return mOperand.getInternalAlphabet(); - } - - @Override - public Set getCallAlphabet() { - return mOperand.getCallAlphabet(); - } - - @Override - public Set getReturnAlphabet() { - return mOperand.getReturnAlphabet(); + public VpAlphabet getVpAlphabet() { + return mOperand.getVpAlphabet(); } @Override @@ -192,17 +183,17 @@ public STATE getEmptyStackState() { @Override public Set lettersInternal(final STATE state) { - return mOperand.getInternalAlphabet(); + return mOperand.getVpAlphabet().getInternalAlphabet(); } @Override public Set lettersCall(final STATE state) { - return mOperand.getCallAlphabet(); + return mOperand.getVpAlphabet().getCallAlphabet(); } @Override public Set lettersReturn(final STATE state, final STATE hier) { - return mOperand.getReturnAlphabet(); + return mOperand.getVpAlphabet().getReturnAlphabet(); } @Override @@ -234,7 +225,7 @@ public Iterable> internalSuccessors(fi if (mNondeterministicTransitionsDetected) { return Collections.emptySet(); } - final Set alphabet = getInternalAlphabet(); + final Set alphabet = getVpAlphabet().getInternalAlphabet(); final ArrayList> result = new ArrayList<>(alphabet.size()); for (final LETTER letter : alphabet) { final Iterator> it = internalSuccessors(state, letter).iterator(); @@ -275,7 +266,7 @@ public Iterable> callSuccessors(final STAT if (mNondeterministicTransitionsDetected) { return Collections.emptySet(); } - final Set alphabet = getCallAlphabet(); + final Set alphabet = getVpAlphabet().getCallAlphabet(); final ArrayList> result = new ArrayList<>(alphabet.size()); for (final LETTER letter : alphabet) { final Iterator> it = callSuccessors(state, letter).iterator(); @@ -318,7 +309,7 @@ public Iterable> returnSuccessorsGivenHi if (mNondeterministicTransitionsDetected) { return Collections.emptySet(); } - final Set alphabet = getReturnAlphabet(); + final Set alphabet = getVpAlphabet().getReturnAlphabet(); final ArrayList> result = new ArrayList<>(alphabet.size()); for (final LETTER letter : alphabet) { final Iterator> it = diff --git a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/incrementalinclusion/IncrementalInclusionCheck2.java b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/incrementalinclusion/IncrementalInclusionCheck2.java index 9a560b430fc..34f76c65a6b 100755 --- a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/incrementalinclusion/IncrementalInclusionCheck2.java +++ b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/incrementalinclusion/IncrementalInclusionCheck2.java @@ -40,6 +40,7 @@ import de.uni_freiburg.informatik.ultimate.automata.nestedword.INestedWordAutomatonSimple; 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.NestedWordAutomataUtils; import de.uni_freiburg.informatik.ultimate.automata.nestedword.transitions.OutgoingInternalTransition; import de.uni_freiburg.informatik.ultimate.automata.statefactory.IDeterminizeStateFactory; @@ -606,7 +607,7 @@ private void addBStates(final INestedWordAutomatonSimple nwa) { } public static void abortIfContainsCallOrReturn(final INestedWordAutomatonSimple a) { - if (!a.getCallAlphabet().isEmpty() || !a.getReturnAlphabet().isEmpty()) { + if (!NestedWordAutomataUtils.isFiniteAutomaton(a)) { throw new UnsupportedOperationException("Operation does not support call or return"); } } diff --git a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/incrementalinclusion/IncrementalInclusionCheck2DeadEndRemoval.java b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/incrementalinclusion/IncrementalInclusionCheck2DeadEndRemoval.java index 5a8f97ee00a..56aeb8d9163 100755 --- a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/incrementalinclusion/IncrementalInclusionCheck2DeadEndRemoval.java +++ b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/incrementalinclusion/IncrementalInclusionCheck2DeadEndRemoval.java @@ -41,6 +41,7 @@ import de.uni_freiburg.informatik.ultimate.automata.nestedword.INestedWordAutomatonSimple; 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.NestedWordAutomataUtils; import de.uni_freiburg.informatik.ultimate.automata.nestedword.operations.RemoveDeadEnds; import de.uni_freiburg.informatik.ultimate.automata.nestedword.transitions.OutgoingInternalTransition; import de.uni_freiburg.informatik.ultimate.automata.statefactory.IDeterminizeStateFactory; @@ -554,7 +555,7 @@ private void checkErrorNodesAfterAddingB() { } public static void abortIfContainsCallOrReturn(final INestedWordAutomatonSimple a) { - if (!a.getCallAlphabet().isEmpty() || !a.getReturnAlphabet().isEmpty()) { + if (!NestedWordAutomataUtils.isFiniteAutomaton(a)) { throw new UnsupportedOperationException("Operation does not support call or return"); } } diff --git a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/incrementalinclusion/IncrementalInclusionCheck2DeadEndRemovalAdvanceCover.java b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/incrementalinclusion/IncrementalInclusionCheck2DeadEndRemovalAdvanceCover.java index 440f53185e2..2a862629498 100755 --- a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/incrementalinclusion/IncrementalInclusionCheck2DeadEndRemovalAdvanceCover.java +++ b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/incrementalinclusion/IncrementalInclusionCheck2DeadEndRemovalAdvanceCover.java @@ -40,6 +40,7 @@ import de.uni_freiburg.informatik.ultimate.automata.nestedword.INestedWordAutomatonSimple; 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.NestedWordAutomataUtils; import de.uni_freiburg.informatik.ultimate.automata.nestedword.transitions.ITransitionlet; import de.uni_freiburg.informatik.ultimate.automata.nestedword.transitions.OutgoingInternalTransition; import de.uni_freiburg.informatik.ultimate.automata.statefactory.IDeterminizeStateFactory; @@ -812,7 +813,7 @@ public static boolean compareInclusionCheckResult(final Automata } public static void abortIfContainsCallOrReturn(final INestedWordAutomatonSimple a) { - if (!a.getCallAlphabet().isEmpty() || !a.getReturnAlphabet().isEmpty()) { + if (!NestedWordAutomataUtils.isFiniteAutomaton(a)) { throw new UnsupportedOperationException("Operation does not support call or return"); } } diff --git a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/incrementalinclusion/IncrementalInclusionCheck2DeadEndRemovalAdvanceCover_2Stacks.java b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/incrementalinclusion/IncrementalInclusionCheck2DeadEndRemovalAdvanceCover_2Stacks.java index 3d8e2fea857..870f27b463d 100755 --- a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/incrementalinclusion/IncrementalInclusionCheck2DeadEndRemovalAdvanceCover_2Stacks.java +++ b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/incrementalinclusion/IncrementalInclusionCheck2DeadEndRemovalAdvanceCover_2Stacks.java @@ -41,6 +41,7 @@ import de.uni_freiburg.informatik.ultimate.automata.nestedword.INestedWordAutomatonSimple; 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.NestedWordAutomataUtils; import de.uni_freiburg.informatik.ultimate.automata.nestedword.transitions.ITransitionlet; import de.uni_freiburg.informatik.ultimate.automata.nestedword.transitions.OutgoingInternalTransition; import de.uni_freiburg.informatik.ultimate.automata.statefactory.IDeterminizeStateFactory; @@ -1026,7 +1027,7 @@ public static boolean compareInclusionCheckResult(final Automata } public static void abortIfContainsCallOrReturn(final INestedWordAutomatonSimple a) { - if (!a.getCallAlphabet().isEmpty() || !a.getReturnAlphabet().isEmpty()) { + if (!NestedWordAutomataUtils.isFiniteAutomaton(a)) { throw new UnsupportedOperationException("Operation does not support call or return"); } } diff --git a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/incrementalinclusion/IncrementalInclusionCheck2DeadEndRemovalAdvanceCover_2Stacks_multipleCounterExamplesAtOnce.java b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/incrementalinclusion/IncrementalInclusionCheck2DeadEndRemovalAdvanceCover_2Stacks_multipleCounterExamplesAtOnce.java index 03d2c6a7b95..be60128486a 100755 --- a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/incrementalinclusion/IncrementalInclusionCheck2DeadEndRemovalAdvanceCover_2Stacks_multipleCounterExamplesAtOnce.java +++ b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/incrementalinclusion/IncrementalInclusionCheck2DeadEndRemovalAdvanceCover_2Stacks_multipleCounterExamplesAtOnce.java @@ -40,8 +40,10 @@ import de.uni_freiburg.informatik.ultimate.automata.IOperation; import de.uni_freiburg.informatik.ultimate.automata.nestedword.INestedWordAutomaton; import de.uni_freiburg.informatik.ultimate.automata.nestedword.INestedWordAutomatonSimple; +import de.uni_freiburg.informatik.ultimate.automata.nestedword.VpAlphabet; 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.NestedWordAutomataUtils; import de.uni_freiburg.informatik.ultimate.automata.nestedword.NestedWordAutomaton; import de.uni_freiburg.informatik.ultimate.automata.nestedword.transitions.ITransitionlet; import de.uni_freiburg.informatik.ultimate.automata.nestedword.transitions.OutgoingInternalTransition; @@ -81,7 +83,8 @@ class NfaUnion implements IOperation> { INestedWordAutomatonSimple orgin, target; NestedWordAutomaton result; Collection state1, state2; - Collection letter1, letter2, newLetterSet; + Collection letter1, letter2; + Set newLetterSet; private final AutomataLibraryServices mServices; public NfaUnion(final AutomataLibraryServices services, final IStateFactory sf, @@ -92,8 +95,8 @@ public NfaUnion(final AutomataLibraryServices services, final IStateFactory(); newLetterSet.addAll(letter1); newLetterSet.addAll(letter2); @@ -102,7 +105,7 @@ public NfaUnion(final AutomataLibraryServices services, final IStateFactory(mServices, (Set) newLetterSet, null, null, stateFactory); + result = new NestedWordAutomaton(mServices, new VpAlphabet(newLetterSet), stateFactory); final HashSet currentStates = new HashSet<>(); final HashSet nextRoundStates = new HashSet<>(); final HashSet finishedStates = new HashSet<>(); @@ -1119,7 +1122,7 @@ public static boolean compareInclusionCheckResult(final Automata } public static void abortIfContainsCallOrReturn(final INestedWordAutomatonSimple a) { - if (!a.getCallAlphabet().isEmpty() || !a.getReturnAlphabet().isEmpty()) { + if (!NestedWordAutomataUtils.isFiniteAutomaton(a)) { throw new UnsupportedOperationException("Operation does not support call or return"); } } diff --git a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/minimization/AbstractMinimizeNwa.java b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/minimization/AbstractMinimizeNwa.java index a41a801ed72..14f0016c83d 100644 --- a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/minimization/AbstractMinimizeNwa.java +++ b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/minimization/AbstractMinimizeNwa.java @@ -43,6 +43,7 @@ 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.INwaInclusionStateFactory; +import de.uni_freiburg.informatik.ultimate.automata.nestedword.NestedWordAutomataUtils; import de.uni_freiburg.informatik.ultimate.automata.nestedword.NestedWordAutomaton; import de.uni_freiburg.informatik.ultimate.automata.nestedword.UnaryNwaOperation; import de.uni_freiburg.informatik.ultimate.automata.nestedword.buchi.BuchiIsEquivalent; @@ -300,8 +301,7 @@ protected final void startResultConstruction() { if (mResult != null) { throw new AssertionError("The result has already been constructed."); } - mTemporaryResult = new DoubleDeckerAutomaton<>(mServices, getOperand().getInternalAlphabet(), - getOperand().getCallAlphabet(), getOperand().getReturnAlphabet(), mStateFactory); + mTemporaryResult = new DoubleDeckerAutomaton<>(mServices, getOperand().getVpAlphabet(), mStateFactory); } /** @@ -503,7 +503,7 @@ protected final boolean isDeterministic() throws AutomataOperationCanceledExcept * @return true iff automaton contains no call and return letters */ protected final boolean isFiniteAutomaton() { - return (getOperand().getCallAlphabet().isEmpty()) && (getOperand().getReturnAlphabet().isEmpty()); + return (NestedWordAutomataUtils.isFiniteAutomaton(getOperand())); } /** diff --git a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/minimization/MinimizeDfaHopcroftArrays.java b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/minimization/MinimizeDfaHopcroftArrays.java index 56e8648cfe6..233ec398c58 100644 --- a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/minimization/MinimizeDfaHopcroftArrays.java +++ b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/minimization/MinimizeDfaHopcroftArrays.java @@ -211,7 +211,7 @@ private void preprocessingData() { mNumberOfFinalStates = mOperand.getFinalStates().size(); mFinalStates = new int[mNumberOfFinalStates]; mNumberOfStates = mOperand.size(); - mNumberOfLetters = mOperand.getInternalAlphabet().size(); + mNumberOfLetters = mOperand.getVpAlphabet().getInternalAlphabet().size(); initializeMappings(); initializeLables(); @@ -241,7 +241,7 @@ private void initializeMappings() { mState2int.put(state, ++index); } index = -1; - for (final LETTER letter : mOperand.getInternalAlphabet()) { + for (final LETTER letter : mOperand.getVpAlphabet().getInternalAlphabet()) { mInt2letter.add(letter); mLetter2int.put(letter, ++index); } diff --git a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/minimization/MinimizeDfaHopcroftLists.java b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/minimization/MinimizeDfaHopcroftLists.java index d7f408daed1..2428e9ddfe5 100644 --- a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/minimization/MinimizeDfaHopcroftLists.java +++ b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/minimization/MinimizeDfaHopcroftLists.java @@ -140,7 +140,7 @@ public MinimizeDfaHopcroftLists(final AutomataLibraryServices services, // stateToOutgoingEdges = new HashMap>>( // stateAmount); - final int letterAmount = operand.getInternalAlphabet().size(); + final int letterAmount = operand.getVpAlphabet().getInternalAlphabet().size(); mLetterToId = new HashMap<>(letterAmount); init(stateAmount, letterAmount); @@ -309,7 +309,7 @@ private void init(final int stateAmount, final int letterAmount) { maxAmount = letterAmount; } final Iterator states = mOperand.getStates().iterator(); - final Iterator letters = mOperand.getInternalAlphabet().iterator(); + final Iterator letters = mOperand.getVpAlphabet().getInternalAlphabet().iterator(); for (int i = 0; i < maxAmount; i++) { if (states.hasNext()) { @@ -443,7 +443,7 @@ private void minimizeIcdfa(final PartitionBackedSetOfPairs initialPartiti splitCandidates.remove(splitter); final LinkedList> splitCandidatesToAppend = - split(splitter, mOperand.getInternalAlphabet().size()); + split(splitter, mOperand.getVpAlphabet().getInternalAlphabet().size()); splitCandidates.addAll(splitCandidatesToAppend); } diff --git a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/minimization/MinimizeDfaHopcroftWiki.java b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/minimization/MinimizeDfaHopcroftWiki.java index 7be7b4938c7..66c81299f0b 100644 --- a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/minimization/MinimizeDfaHopcroftWiki.java +++ b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/minimization/MinimizeDfaHopcroftWiki.java @@ -116,7 +116,7 @@ private Partition createInitialPartition() { */ private void initializeData() { final int nOfStates = mOperand.size(); - final int nOfLables = mOperand.getInternalAlphabet().size(); + final int nOfLables = mOperand.getVpAlphabet().getInternalAlphabet().size(); initializeMappings(nOfStates, nOfLables); initializeLables(); } @@ -137,7 +137,7 @@ private void initializeMappings(final int numberOfStates, final int numberOfLabl mState2int.put(state, ++index); } index = -1; - for (final LETTER letter : mOperand.getInternalAlphabet()) { + for (final LETTER letter : mOperand.getVpAlphabet().getInternalAlphabet()) { mInt2letter.add(letter); mLetter2int.put(letter, ++index); } @@ -150,7 +150,7 @@ private void initializeMappings(final int numberOfStates, final int numberOfLabl */ private void initializeLables() { final int capacity = (int) Math.min(Integer.MAX_VALUE, - (double) mOperand.size() * mOperand.size() * mOperand.getInternalAlphabet().size()); + (double) mOperand.size() * mOperand.size() * mOperand.getVpAlphabet().getInternalAlphabet().size()); mLabels = new int[capacity]; mLabelTails = new int[capacity]; mLabelHeads = new int[capacity]; @@ -188,7 +188,7 @@ private void minimizeDfaHopcroft() { final Worklist worklist = mPartition.getWorklist(); while (!worklist.isEmpty()) { final int[] elem = worklist.popFromWorklist(); - for (final LETTER letter : mOperand.getInternalAlphabet()) { + for (final LETTER letter : mOperand.getVpAlphabet().getInternalAlphabet()) { // This is far from optimal (hopefully): Find X, set of all // states for which a transition on letter leads to a state in // elem. diff --git a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/minimization/MinimizeDfaSymbolic.java b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/minimization/MinimizeDfaSymbolic.java index 1d717251b6e..a0d4addeda6 100644 --- a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/minimization/MinimizeDfaSymbolic.java +++ b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/minimization/MinimizeDfaSymbolic.java @@ -148,7 +148,7 @@ private void preprocessingData() { mInitialState = mOperand.getInitialStates().iterator().next(); // get internal alphabet of moperand. - final Collection alphabet = mOperand.getInternalAlphabet(); + final Collection alphabet = mOperand.getVpAlphabet().getInternalAlphabet(); // iterate over whole alphabet and construct letter --> atom mapping. final Iterator alphabetIt = alphabet.iterator(); diff --git a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/minimization/MinimizeDfaTable.java b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/minimization/MinimizeDfaTable.java index 007aed9304e..d36832c5cb3 100644 --- a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/minimization/MinimizeDfaTable.java +++ b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/minimization/MinimizeDfaTable.java @@ -137,7 +137,7 @@ private void calculateTable(final ArrayList states, final boolean[][] tab for (int j = 0; j < i; j++) { // if (i, j) not marked if (!table[i][j]) { - for (final LETTER s : mOperand.getInternalAlphabet()) { + for (final LETTER s : mOperand.getVpAlphabet().getInternalAlphabet()) { final ArrayList first = getSuccessors(states, s, i); final ArrayList second = getSuccessors(states, s, j); // if either i or j has no successors, for k mark @@ -268,7 +268,7 @@ private void generateResultAutomaton(final ArrayList states, final boolea // add edges for (final STATE c : mOperand.getStates()) { - for (final LETTER s : mOperand.getInternalAlphabet()) { + for (final LETTER s : mOperand.getVpAlphabet().getInternalAlphabet()) { for (final OutgoingInternalTransition trans : mOperand.internalSuccessors(c, s)) { final STATE newPred = oldSNames2newSNames.get(c); final STATE newSucc = oldSNames2newSNames.get(trans.getSucc()); @@ -314,7 +314,7 @@ private void printTable(final ArrayList st, final boolean[][] t) { private void printTransitions(final INestedWordAutomaton nwa) { StringBuilder msg; for (final STATE c : nwa.getStates()) { - for (final LETTER s : nwa.getInternalAlphabet()) { + for (final LETTER s : nwa.getVpAlphabet().getInternalAlphabet()) { for (final OutgoingInternalTransition trans : nwa.internalSuccessors(c, s)) { msg = new StringBuilder(c.toString()); msg.append(" ").append(s).append(" ").append(trans.getSucc()); diff --git a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/minimization/MinimizeNfaBrzozowski.java b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/minimization/MinimizeNfaBrzozowski.java index 7e666723f20..f050f1eace7 100644 --- a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/minimization/MinimizeNfaBrzozowski.java +++ b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/minimization/MinimizeNfaBrzozowski.java @@ -127,8 +127,7 @@ private void minimize(final IDeterminizeStateFactory determinizeStateFact @SuppressWarnings("squid:S3047") private INestedWordAutomaton reverse(final INestedWordAutomaton automaton) { final NestedWordAutomaton reversed = - new NestedWordAutomaton<>(mServices, automaton.getInternalAlphabet(), automaton.getCallAlphabet(), - automaton.getReturnAlphabet(), automaton.getStateFactory()); + new NestedWordAutomaton<>(mServices, automaton.getVpAlphabet(), automaton.getStateFactory()); // add states for (final STATE state : automaton.getStates()) { diff --git a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/minimization/MinimizeNwaMaxSat2.java b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/minimization/MinimizeNwaMaxSat2.java index 64793b3f944..1a7e840967d 100644 --- a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/minimization/MinimizeNwaMaxSat2.java +++ b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/minimization/MinimizeNwaMaxSat2.java @@ -749,7 +749,7 @@ private static boolean isVoidOfNull(final T[] positiveAtoms) { } private static boolean hasNoReturnTransitions(final IDoubleDeckerAutomaton operand) { - return operand.getReturnAlphabet().isEmpty(); + return operand.getVpAlphabet().getReturnAlphabet().isEmpty(); } protected final void checkTimeout(final String currentTask) throws AutomataOperationCanceledException { diff --git a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/minimization/NwaApproximateBisimulation.java b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/minimization/NwaApproximateBisimulation.java index 4153998c233..42565f42efb 100644 --- a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/minimization/NwaApproximateBisimulation.java +++ b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/minimization/NwaApproximateBisimulation.java @@ -196,7 +196,7 @@ protected void separateByDifferentSymbols() throws AutomataOperationCanceledExce for (final Set block : mPartition) { queue.add(block); } - final boolean hasCalls = !mOperand.getCallAlphabet().isEmpty(); + final boolean hasCalls = !mOperand.getVpAlphabet().getCallAlphabet().isEmpty(); while (!queue.isEmpty()) { final Set block = queue.poll(); diff --git a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/minimization/QuotientNwaConstructor.java b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/minimization/QuotientNwaConstructor.java index 1f14079f23f..b4c3df6f87e 100644 --- a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/minimization/QuotientNwaConstructor.java +++ b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/minimization/QuotientNwaConstructor.java @@ -99,14 +99,12 @@ public QuotientNwaConstructor(final AutomataLibraryServices services, if (operand instanceof IDoubleDeckerAutomaton) { // create a DoubleDeckerAutomaton - mResult = new DoubleDeckerAutomaton<>(mServices, mOperand.getInternalAlphabet(), mOperand.getCallAlphabet(), - mOperand.getReturnAlphabet(), mStateFactory); + mResult = new DoubleDeckerAutomaton<>(mServices, mOperand.getVpAlphabet(), mStateFactory); mUp2Down = new HashMap<>(partition.size()); ((DoubleDeckerAutomaton) mResult).setUp2Down(mUp2Down); } else { // create a NestedWordAutomaton - mResult = new NestedWordAutomaton<>(mServices, mOperand.getInternalAlphabet(), mOperand.getCallAlphabet(), - mOperand.getReturnAlphabet(), mStateFactory); + mResult = new NestedWordAutomaton<>(mServices, mOperand.getVpAlphabet(), mStateFactory); mUp2Down = null; } diff --git a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/minimization/ShrinkNwa.java b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/minimization/ShrinkNwa.java index 717f6b5bca1..3385f831477 100644 --- a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/minimization/ShrinkNwa.java +++ b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/minimization/ShrinkNwa.java @@ -2645,7 +2645,7 @@ private interface IOutgoingHelper { private class OutgoingHelperInternal implements IOutgoingHelper { @Override public int size() { - return mOperand.getInternalAlphabet().size(); + return mOperand.getVpAlphabet().getInternalAlphabet().size(); } @Override @@ -2690,7 +2690,7 @@ public boolean assertLetters(final STATE state) { private class OutgoingHelperCall implements IOutgoingHelper { @Override public int size() { - return mOperand.getCallAlphabet().size(); + return mOperand.getVpAlphabet().getCallAlphabet().size(); } @Override diff --git a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/minimization/maxsat/arrays/Converter.java b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/minimization/maxsat/arrays/Converter.java index 1ac5b968e60..28b89d8d636 100644 --- a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/minimization/maxsat/arrays/Converter.java +++ b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/minimization/maxsat/arrays/Converter.java @@ -37,6 +37,7 @@ import de.uni_freiburg.informatik.ultimate.automata.AutomataLibraryServices; 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.VpAlphabet; import de.uni_freiburg.informatik.ultimate.automata.nestedword.NestedWordAutomaton; import de.uni_freiburg.informatik.ultimate.automata.nestedword.transitions.OutgoingCallTransition; import de.uni_freiburg.informatik.ultimate.automata.nestedword.transitions.OutgoingInternalTransition; @@ -110,9 +111,9 @@ final class Converter { mOldInitialStates = automaton.getInitialStates(); mOldFinalStates = automaton.getFinalStates(); - mIAlphabet = automaton.getInternalAlphabet(); - mCAlphabet = automaton.getCallAlphabet(); - mRAlphabet = automaton.getReturnAlphabet(); + mIAlphabet = automaton.getVpAlphabet().getInternalAlphabet(); + mCAlphabet = automaton.getVpAlphabet().getCallAlphabet(); + mRAlphabet = automaton.getVpAlphabet().getReturnAlphabet(); mOldStateIndex = new HashMap<>(); mOldState = new ArrayList<>(); @@ -280,7 +281,7 @@ INestedWordAutomaton constructMerged(final Partition partition) { */ NestedWordAutomaton nwa; - nwa = new NestedWordAutomaton(mServices, mIAlphabet, mCAlphabet, mRAlphabet, mFactory); + nwa = new NestedWordAutomaton(mServices, new VpAlphabet<>(mIAlphabet, mCAlphabet, mRAlphabet), mFactory); for (final STATE st : newState) { nwa.addState(newInitialStates.contains(st), newFinalStates.contains(st), st); diff --git a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/minimization/maxsat/collections/NwaApproximateDelayedSimulation.java b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/minimization/maxsat/collections/NwaApproximateDelayedSimulation.java index 74940fc89c2..434a4b57490 100644 --- a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/minimization/maxsat/collections/NwaApproximateDelayedSimulation.java +++ b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/minimization/maxsat/collections/NwaApproximateDelayedSimulation.java @@ -38,6 +38,7 @@ import de.uni_freiburg.informatik.ultimate.automata.AutomataOperationCanceledException; import de.uni_freiburg.informatik.ultimate.automata.LibraryIdentifiers; import de.uni_freiburg.informatik.ultimate.automata.nestedword.INestedWordAutomaton; +import de.uni_freiburg.informatik.ultimate.automata.nestedword.NestedWordAutomataUtils; import de.uni_freiburg.informatik.ultimate.automata.nestedword.operations.minimization.NwaApproximateSimulation; import de.uni_freiburg.informatik.ultimate.automata.nestedword.operations.minimization.NwaApproximateXsimulation.SimulationType; import de.uni_freiburg.informatik.ultimate.automata.nestedword.transitions.IncomingInternalTransition; @@ -96,7 +97,7 @@ public NwaApproximateDelayedSimulation(final AutomataLibraryServices services, mOperand = operand; // FIXME: Currently this operation only works for finite automata, in which case it is exact. - if (!mOperand.getCallAlphabet().isEmpty() || !mOperand.getReturnAlphabet().isEmpty()) { + if (!NestedWordAutomataUtils.isFiniteAutomaton(operand)) { throw new IllegalArgumentException("Currently this operation only supports finite automata"); } diff --git a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/minimization/parallel/MinimizeDfaHopcroftParallel.java b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/minimization/parallel/MinimizeDfaHopcroftParallel.java index 1fc9749e59f..b72c82a0ccc 100644 --- a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/minimization/parallel/MinimizeDfaHopcroftParallel.java +++ b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/minimization/parallel/MinimizeDfaHopcroftParallel.java @@ -340,7 +340,7 @@ private void minimizeDfaHopcroft() { final HashSet elem = currentBlock.getStates(); - for (final LETTER letter : mOperand.getInternalAlphabet()) { + for (final LETTER letter : mOperand.getVpAlphabet().getInternalAlphabet()) { // Initialize Predecessors on letter. final Set x = new HashSet<>(); for (final int state : elem) { diff --git a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/oldapi/AbstractIntersect.java b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/oldapi/AbstractIntersect.java index 63e68219e9f..fbd0ae9db38 100644 --- a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/oldapi/AbstractIntersect.java +++ b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/oldapi/AbstractIntersect.java @@ -39,6 +39,7 @@ import de.uni_freiburg.informatik.ultimate.automata.IOperation; import de.uni_freiburg.informatik.ultimate.automata.nestedword.DoubleDecker; import de.uni_freiburg.informatik.ultimate.automata.nestedword.INestedWordAutomatonSimple; +import de.uni_freiburg.informatik.ultimate.automata.nestedword.VpAlphabet; import de.uni_freiburg.informatik.ultimate.automata.nestedword.NestedWordAutomataUtils; import de.uni_freiburg.informatik.ultimate.automata.nestedword.NestedWordAutomaton; import de.uni_freiburg.informatik.ultimate.automata.nestedword.transitions.IOutgoingTransitionlet; @@ -99,16 +100,16 @@ public AbstractIntersect(final AutomataLibraryServices services, final IStateFac } final Set newInternals = new HashSet<>(); - newInternals.addAll(mFstNwa.getInternalAlphabet()); - newInternals.retainAll(mSndNwa.getInternalAlphabet()); + newInternals.addAll(mFstNwa.getVpAlphabet().getInternalAlphabet()); + newInternals.retainAll(mSndNwa.getVpAlphabet().getInternalAlphabet()); final Set newCalls = new HashSet<>(); - newCalls.addAll(mFstNwa.getCallAlphabet()); - newCalls.retainAll(mSndNwa.getCallAlphabet()); + newCalls.addAll(mFstNwa.getVpAlphabet().getCallAlphabet()); + newCalls.retainAll(mSndNwa.getVpAlphabet().getCallAlphabet()); final Set newReturns = new HashSet<>(); - newReturns.addAll(mFstNwa.getReturnAlphabet()); - newReturns.retainAll(mSndNwa.getReturnAlphabet()); + newReturns.addAll(mFstNwa.getVpAlphabet().getReturnAlphabet()); + newReturns.retainAll(mSndNwa.getVpAlphabet().getReturnAlphabet()); - mResultNwa = new NestedWordAutomaton<>(mServices, newInternals, newCalls, newReturns, stateFactory); + mResultNwa = new NestedWordAutomaton<>(mServices, new VpAlphabet<>(newInternals, newCalls, newReturns), stateFactory); } @Override diff --git a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/oldapi/DeterminizeDD.java b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/oldapi/DeterminizeDD.java index 1f8cb1fdd13..8a2d332a2f8 100644 --- a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/oldapi/DeterminizeDD.java +++ b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/oldapi/DeterminizeDD.java @@ -112,8 +112,7 @@ public DeterminizeDD(final AutomataLibraryServices services, } mStateDeterminizer = stateDeterminizer; - super.mTraversedNwa = new NestedWordAutomaton<>(mServices, operand.getInternalAlphabet(), - operand.getCallAlphabet(), operand.getReturnAlphabet(), operand.getStateFactory()); + super.mTraversedNwa = new NestedWordAutomaton<>(mServices, operand.getVpAlphabet(), operand.getStateFactory()); mRemoveDeadEnds = false; traverseDoubleDeckerGraph(); assert new IsDeterministic<>(mServices, mTraversedNwa).getResult(); @@ -159,7 +158,7 @@ protected Collection buildInternalSuccessors(final DoubleDecker do final DeterminizedState detState = mRes2det.get(resState); - for (final LETTER symbol : mOperand.getInternalAlphabet()) { + for (final LETTER symbol : mOperand.getVpAlphabet().getInternalAlphabet()) { final DeterminizedState detSucc = mStateDeterminizer.internalSuccessor(detState, symbol); final STATE resSucc = getResState(detSucc); ((NestedWordAutomaton) mTraversedNwa).addInternalTransition(resState, symbol, resSucc); @@ -175,7 +174,7 @@ protected Collection buildCallSuccessors(final DoubleDecker double final DeterminizedState detState = mRes2det.get(resState); - for (final LETTER symbol : mOperand.getCallAlphabet()) { + for (final LETTER symbol : mOperand.getVpAlphabet().getCallAlphabet()) { final DeterminizedState detSucc = mStateDeterminizer.callSuccessor(detState, symbol); final STATE resSucc = getResState(detSucc); ((NestedWordAutomaton) mTraversedNwa).addCallTransition(resState, symbol, resSucc); @@ -197,7 +196,7 @@ protected Collection buildReturnSuccessors(final DoubleDecker doub final STATE resState = doubleDecker.getUp(); final DeterminizedState detLinPred = mRes2det.get(resLinPred); final DeterminizedState detState = mRes2det.get(resState); - for (final LETTER symbol : mOperand.getReturnAlphabet()) { + for (final LETTER symbol : mOperand.getVpAlphabet().getReturnAlphabet()) { final DeterminizedState detSucc = mStateDeterminizer.returnSuccessor(detState, detLinPred, symbol); final STATE resSucc = getResState(detSucc); diff --git a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/oldapi/DeterminizeSadd.java b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/oldapi/DeterminizeSadd.java index c53039371c4..9f857be6287 100644 --- a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/oldapi/DeterminizeSadd.java +++ b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/oldapi/DeterminizeSadd.java @@ -90,8 +90,7 @@ public DeterminizeSadd(final AutomataLibraryServices services, final IDeterminiz mLogger.info(startMessage()); } - mResult = new NestedWordAutomaton<>(mServices, mOperand.getInternalAlphabet(), mOperand.getCallAlphabet(), - mOperand.getReturnAlphabet(), mOperand.getStateFactory()); + mResult = new NestedWordAutomaton<>(mServices, mOperand.getVpAlphabet(), mOperand.getStateFactory()); mAuxiliaryEmptyStackState = mOperand.getEmptyStackState(); determinize(); diff --git a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/oldapi/DifferenceDD.java b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/oldapi/DifferenceDD.java index 4f728fc8161..e65108aaee3 100644 --- a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/oldapi/DifferenceDD.java +++ b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/oldapi/DifferenceDD.java @@ -29,11 +29,9 @@ import java.util.ArrayList; import java.util.Collection; import java.util.HashMap; -import java.util.HashSet; import java.util.LinkedList; import java.util.List; import java.util.Map; -import java.util.Set; import de.uni_freiburg.informatik.ultimate.automata.AutomataLibraryException; import de.uni_freiburg.informatik.ultimate.automata.AutomataLibraryServices; @@ -187,17 +185,6 @@ public & IIntersectionStateFactory(subtrahend, true, stateFactory), false, false, false); - // TODO Christian 2016-10-05: These sets are never used - a bug? - final Set newInternals = new HashSet<>(); - newInternals.addAll(minuend.getInternalAlphabet()); - newInternals.retainAll(subtrahend.getInternalAlphabet()); - final Set newCalls = new HashSet<>(); - newCalls.addAll(minuend.getCallAlphabet()); - newCalls.retainAll(subtrahend.getCallAlphabet()); - final Set newReturns = new HashSet<>(); - newReturns.addAll(minuend.getReturnAlphabet()); - newReturns.retainAll(subtrahend.getReturnAlphabet()); - runConstruction(); if (mLogger.isInfoEnabled()) { @@ -230,8 +217,7 @@ private DifferenceDD(final AutomataLibraryServices services, mLogger.info(startMessage()); } - super.mTraversedNwa = new DoubleDeckerAutomaton<>(mServices, minuend.getInternalAlphabet(), - minuend.getCallAlphabet(), minuend.getReturnAlphabet(), mStateFactoryForIntersection); + super.mTraversedNwa = new DoubleDeckerAutomaton<>(mServices, minuend.getVpAlphabet(), mStateFactoryForIntersection); /* mDeterminizedSubtrahend = @@ -360,7 +346,7 @@ protected Collection buildInternalSuccessors(final DoubleDecker do final DeterminizedState detState = diffState.getSubtrahendDeterminizedState(); for (final LETTER symbol : mMinuend.lettersInternal(minuState)) { - if (!mSubtrahend.getInternalAlphabet().contains(symbol)) { + if (!mSubtrahend.getVpAlphabet().getInternalAlphabet().contains(symbol)) { continue; } DeterminizedState detSucc = internalSuccessorCache(detState, symbol); @@ -401,7 +387,7 @@ protected Collection buildCallSuccessors(final DoubleDecker double final DeterminizedState detState = diffState.getSubtrahendDeterminizedState(); for (final LETTER symbol : mMinuend.lettersCall(minuState)) { - if (!mSubtrahend.getCallAlphabet().contains(symbol)) { + if (!mSubtrahend.getVpAlphabet().getCallAlphabet().contains(symbol)) { continue; } DeterminizedState detSucc = callSuccessorCache(detState, symbol); @@ -465,7 +451,7 @@ protected Collection buildReturnSuccessors(final DoubleDecker doub continue; } - if (!mSubtrahend.getReturnAlphabet().contains(symbol)) { + if (!mSubtrahend.getVpAlphabet().getReturnAlphabet().contains(symbol)) { continue; } diff --git a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/oldapi/DifferenceSadd.java b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/oldapi/DifferenceSadd.java index 7ee2081f6e1..39d4873fdf0 100644 --- a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/oldapi/DifferenceSadd.java +++ b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/oldapi/DifferenceSadd.java @@ -160,8 +160,7 @@ public DifferenceSadd(final AutomataLibraryServices services, final IIntersectio mLogger.info(startMessage()); } - mDifference = new NestedWordAutomaton<>(mServices, minuend.getInternalAlphabet(), minuend.getCallAlphabet(), - minuend.getReturnAlphabet(), minuend.getStateFactory()); + mDifference = new NestedWordAutomaton<>(mServices, minuend.getVpAlphabet(), minuend.getStateFactory()); mAuxiliaryEmptyStackState = mDifference.getEmptyStackState(); computeDifference(); @@ -312,7 +311,7 @@ private void processSummaryState(final SummaryState resSummaryState) { final DeterminizedState detState = diffState.getSubtrahendDeterminizedState(); for (final LETTER symbol : mMinuend.lettersInternal(minuState)) { - if (!mSubtrahend.getInternalAlphabet().contains(symbol)) { + if (!mSubtrahend.getVpAlphabet().getInternalAlphabet().contains(symbol)) { continue; } final DeterminizedState detSucc = mStateDeterminizer.internalSuccessor(detState, symbol); @@ -327,7 +326,7 @@ private void processSummaryState(final SummaryState resSummaryState) { } for (final LETTER symbol : mMinuend.lettersCall(minuState)) { - if (!mSubtrahend.getCallAlphabet().contains(symbol)) { + if (!mSubtrahend.getVpAlphabet().getCallAlphabet().contains(symbol)) { continue; } final DeterminizedState detSucc = mStateDeterminizer.callSuccessor(detState, symbol); @@ -341,7 +340,7 @@ private void processSummaryState(final SummaryState resSummaryState) { } for (final LETTER symbol : mMinuend.lettersReturn(minuState)) { - if (!mSubtrahend.getReturnAlphabet().contains(symbol)) { + if (!mSubtrahend.getVpAlphabet().getReturnAlphabet().contains(symbol)) { continue; } final STATE resLinPred = resSummaryState.getCallerState(); diff --git a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/oldapi/ReachableStatesCopy.java b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/oldapi/ReachableStatesCopy.java index b13e2a61b46..666161fa449 100644 --- a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/oldapi/ReachableStatesCopy.java +++ b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/oldapi/ReachableStatesCopy.java @@ -114,8 +114,7 @@ public ReachableStatesCopy(final AutomataLibraryServices services, mComplement = complement; mOperand = operand; mLogger.info(startMessage()); - mTraversedNwa = new DoubleDeckerAutomaton<>(mServices, operand.getInternalAlphabet(), operand.getCallAlphabet(), - operand.getReturnAlphabet(), operand.getStateFactory()); + mTraversedNwa = new DoubleDeckerAutomaton<>(mServices, operand.getVpAlphabet(), operand.getStateFactory()); super.mRemoveDeadEnds = removeDeadEnds; super.mRemoveNonLiveStates = removeNonLiveStates; final boolean operandHasInitialStates = mOperand.getInitialStates().iterator().hasNext(); @@ -140,13 +139,13 @@ private void makeAutomatonTotal(final STATE sinkState) throws AutomataOperationC throw new AutomataOperationCanceledException(this.getClass()); } - for (final LETTER letter : mTraversedNwa.getInternalAlphabet()) { + for (final LETTER letter : mTraversedNwa.getVpAlphabet().getInternalAlphabet()) { if (!mTraversedNwa.internalSuccessors(state, letter).iterator().hasNext()) { ((NestedWordAutomaton) mTraversedNwa).addInternalTransition(state, letter, sinkState); } } - for (final LETTER letter : mTraversedNwa.getCallAlphabet()) { + for (final LETTER letter : mTraversedNwa.getVpAlphabet().getCallAlphabet()) { if (!mTraversedNwa.callSuccessors(state, letter).iterator().hasNext()) { ((NestedWordAutomaton) mTraversedNwa).addCallTransition(state, letter, sinkState); } @@ -156,7 +155,7 @@ private void makeAutomatonTotal(final STATE sinkState) throws AutomataOperationC } private void makeAutomatonTotalReturn(final STATE sinkState, final STATE state) { - for (final LETTER symbol : mTraversedNwa.getReturnAlphabet()) { + for (final LETTER symbol : mTraversedNwa.getVpAlphabet().getReturnAlphabet()) { for (final STATE hier : mTraversedNwa.getStates()) { if (!mTraversedNwa.returnSuccessors(state, hier, symbol).iterator().hasNext()) { ((NestedWordAutomaton) mTraversedNwa).addReturnTransition(state, hier, symbol, diff --git a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/simulation/AGameGraph.java b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/simulation/AGameGraph.java index 06308a337b8..8628ba96328 100644 --- a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/simulation/AGameGraph.java +++ b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/simulation/AGameGraph.java @@ -35,6 +35,7 @@ import de.uni_freiburg.informatik.ultimate.automata.AutomataLibraryServices; import de.uni_freiburg.informatik.ultimate.automata.AutomataOperationCanceledException; import de.uni_freiburg.informatik.ultimate.automata.nestedword.INestedWordAutomaton; +import de.uni_freiburg.informatik.ultimate.automata.nestedword.NestedWordAutomataUtils; import de.uni_freiburg.informatik.ultimate.automata.nestedword.operations.simulation.performance.SimulationPerformance; import de.uni_freiburg.informatik.ultimate.automata.nestedword.operations.simulation.util.DuplicatorVertex; import de.uni_freiburg.informatik.ultimate.automata.nestedword.operations.simulation.util.SpoilerVertex; @@ -849,7 +850,7 @@ public void undoChanges(final GameGraphChanges changes) { * Automaton to verify validity */ public void verifyAutomatonValidity(final INestedWordAutomaton automaton) { - if (!automaton.getCallAlphabet().isEmpty() || !automaton.getReturnAlphabet().isEmpty()) { + if (!NestedWordAutomataUtils.isFiniteAutomaton(automaton)) { throw new IllegalArgumentException( "The inputed automaton is no Buechi-automaton. It must have an empty call and return alphabet."); } diff --git a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/simulation/delayed/DelayedGameGraph.java b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/simulation/delayed/DelayedGameGraph.java index 521a5e576f2..f96b096f342 100644 --- a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/simulation/delayed/DelayedGameGraph.java +++ b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/simulation/delayed/DelayedGameGraph.java @@ -39,8 +39,8 @@ import de.uni_freiburg.informatik.ultimate.automata.nestedword.INestedWordAutomaton; import de.uni_freiburg.informatik.ultimate.automata.nestedword.NestedWordAutomaton; import de.uni_freiburg.informatik.ultimate.automata.nestedword.operations.simulation.AGameGraph; -import de.uni_freiburg.informatik.ultimate.automata.nestedword.operations.simulation.performance.TimeMeasure; import de.uni_freiburg.informatik.ultimate.automata.nestedword.operations.simulation.performance.SimulationPerformance; +import de.uni_freiburg.informatik.ultimate.automata.nestedword.operations.simulation.performance.TimeMeasure; import de.uni_freiburg.informatik.ultimate.automata.nestedword.operations.simulation.util.DuplicatorVertex; import de.uni_freiburg.informatik.ultimate.automata.nestedword.operations.simulation.util.SpoilerVertex; import de.uni_freiburg.informatik.ultimate.automata.nestedword.transitions.IncomingInternalTransition; @@ -164,7 +164,7 @@ public INestedWordAutomaton generateAutomatonFromGraph() throws A final Set temp = new HashSet<>(); final HashMap oldSNames2newSNames = new HashMap<>(); final NestedWordAutomaton result = - new NestedWordAutomaton<>(mServices, mBuechi.getInternalAlphabet(), null, null, getStateFactory()); + new NestedWordAutomaton<>(mServices, mBuechi.getVpAlphabet(), getStateFactory()); for (int i = 0; i < states.size(); i++) { if (marker[i]) { @@ -202,7 +202,7 @@ public INestedWordAutomaton generateAutomatonFromGraph() throws A // Add edges for (final STATE c : mBuechi.getStates()) { - for (final LETTER s : mBuechi.getInternalAlphabet()) { + for (final LETTER s : mBuechi.getVpAlphabet().getInternalAlphabet()) { for (final OutgoingInternalTransition trans : mBuechi.internalSuccessors(c, s)) { final STATE newPred = oldSNames2newSNames.get(c); final STATE newSucc = oldSNames2newSNames.get(trans.getSucc()); diff --git a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/simulation/direct/DirectGameGraph.java b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/simulation/direct/DirectGameGraph.java index 6b3b5009356..faa746c84a5 100644 --- a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/simulation/direct/DirectGameGraph.java +++ b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/simulation/direct/DirectGameGraph.java @@ -37,8 +37,8 @@ import de.uni_freiburg.informatik.ultimate.automata.nestedword.INestedWordAutomaton; import de.uni_freiburg.informatik.ultimate.automata.nestedword.NestedWordAutomaton; import de.uni_freiburg.informatik.ultimate.automata.nestedword.operations.simulation.AGameGraph; -import de.uni_freiburg.informatik.ultimate.automata.nestedword.operations.simulation.performance.TimeMeasure; import de.uni_freiburg.informatik.ultimate.automata.nestedword.operations.simulation.performance.SimulationPerformance; +import de.uni_freiburg.informatik.ultimate.automata.nestedword.operations.simulation.performance.TimeMeasure; import de.uni_freiburg.informatik.ultimate.automata.nestedword.operations.simulation.util.DuplicatorVertex; import de.uni_freiburg.informatik.ultimate.automata.nestedword.operations.simulation.util.SpoilerVertex; import de.uni_freiburg.informatik.ultimate.automata.nestedword.transitions.IncomingInternalTransition; @@ -165,7 +165,7 @@ public INestedWordAutomaton generateAutomatonFromGraph() throws A // Merge states final NestedWordAutomaton result = - new NestedWordAutomaton<>(mServices, mBuechi.getInternalAlphabet(), null, null, mStateFactory); + new NestedWordAutomaton<>(mServices, mBuechi.getVpAlphabet(), mStateFactory); final Set representativesOfInitials = new HashSet<>(); for (final STATE initial : mBuechi.getInitialStates()) { representativesOfInitials.add(uf.find(initial)); diff --git a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/simulation/fair/FairGameGraph.java b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/simulation/fair/FairGameGraph.java index 73e6ed02ea5..f4e8ea842de 100644 --- a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/simulation/fair/FairGameGraph.java +++ b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/simulation/fair/FairGameGraph.java @@ -43,8 +43,8 @@ import de.uni_freiburg.informatik.ultimate.automata.nestedword.operations.simulation.AGameGraph; import de.uni_freiburg.informatik.ultimate.automata.nestedword.operations.simulation.GameGraphChangeType; import de.uni_freiburg.informatik.ultimate.automata.nestedword.operations.simulation.GameGraphChanges; -import de.uni_freiburg.informatik.ultimate.automata.nestedword.operations.simulation.performance.TimeMeasure; import de.uni_freiburg.informatik.ultimate.automata.nestedword.operations.simulation.performance.SimulationPerformance; +import de.uni_freiburg.informatik.ultimate.automata.nestedword.operations.simulation.performance.TimeMeasure; import de.uni_freiburg.informatik.ultimate.automata.nestedword.operations.simulation.util.DuplicatorVertex; import de.uni_freiburg.informatik.ultimate.automata.nestedword.operations.simulation.util.SpoilerVertex; import de.uni_freiburg.informatik.ultimate.automata.nestedword.operations.simulation.util.Vertex; @@ -177,7 +177,7 @@ public INestedWordAutomaton generateAutomatonFromGraph() throws A Map input2result = null; final NestedWordAutomaton result = - new NestedWordAutomaton<>(mServices, mBuechi.getInternalAlphabet(), null, null, getStateFactory()); + new NestedWordAutomaton<>(mServices, mBuechi.getVpAlphabet(), getStateFactory()); // Merge states if (areThereMergeableStates) { diff --git a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/simulation/multipebble/FullMultipebbleGameAutomaton.java b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/simulation/multipebble/FullMultipebbleGameAutomaton.java index d9329122c33..0f28f9eff30 100644 --- a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/simulation/multipebble/FullMultipebbleGameAutomaton.java +++ b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/simulation/multipebble/FullMultipebbleGameAutomaton.java @@ -35,6 +35,7 @@ import de.uni_freiburg.informatik.ultimate.automata.AutomataLibraryServices; import de.uni_freiburg.informatik.ultimate.automata.nestedword.IDoubleDeckerAutomaton; import de.uni_freiburg.informatik.ultimate.automata.nestedword.INestedWordAutomatonSimple; +import de.uni_freiburg.informatik.ultimate.automata.nestedword.VpAlphabet; import de.uni_freiburg.informatik.ultimate.automata.nestedword.NestedWordAutomatonForLetterBasedOnDemandConstruction; import de.uni_freiburg.informatik.ultimate.automata.nestedword.transitions.OutgoingCallTransition; import de.uni_freiburg.informatik.ultimate.automata.nestedword.transitions.OutgoingInternalTransition; @@ -71,14 +72,14 @@ public FullMultipebbleGameAutomaton(final AutomataLibraryServices services, mEmptyStackState = gameFactory.createEmptyStackState(); mInitialStates = new HashSet<>(); mGameStateMapping = new NestedMap2<>(); - if (mOperand.getInternalAlphabet().isEmpty()) { + if (mOperand.getVpAlphabet().getInternalAlphabet().isEmpty()) { mInternalLetterForSpoilerWinningSink = null; - if (mOperand.getCallAlphabet().isEmpty()) { + if (mOperand.getVpAlphabet().getCallAlphabet().isEmpty()) { throw new UnsupportedOperationException("Unsupported: automata where internal alphabet and call alphabet are empty."); } - mCallLetterForSpoilerWinningSink = mOperand.getCallAlphabet().iterator().next(); + mCallLetterForSpoilerWinningSink = mOperand.getVpAlphabet().getCallAlphabet().iterator().next(); } else { - mInternalLetterForSpoilerWinningSink = mOperand.getInternalAlphabet().iterator().next(); + mInternalLetterForSpoilerWinningSink = mOperand.getVpAlphabet().getInternalAlphabet().iterator().next(); mCallLetterForSpoilerWinningSink = null; } constructInitialStates(initialPairs); @@ -106,23 +107,8 @@ public NestedMap2 getGameStateMapping() { } @Override - public Set getAlphabet() { - return mOperand.getAlphabet(); - } - - @Override - public Set getInternalAlphabet() { - return mOperand.getInternalAlphabet(); - } - - @Override - public Set getCallAlphabet() { - return mOperand.getCallAlphabet(); - } - - @Override - public Set getReturnAlphabet() { - return mOperand.getReturnAlphabet(); + public VpAlphabet getVpAlphabet() { + return mOperand.getVpAlphabet(); } @Override diff --git a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/simulation/performance/CompareReduceBuchiSimulation.java b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/simulation/performance/CompareReduceBuchiSimulation.java index fdcc806b739..46ce3ee700d 100644 --- a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/simulation/performance/CompareReduceBuchiSimulation.java +++ b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/simulation/performance/CompareReduceBuchiSimulation.java @@ -46,6 +46,7 @@ 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.INestedWordAutomatonSimple; +import de.uni_freiburg.informatik.ultimate.automata.nestedword.NestedWordAutomataUtils; import de.uni_freiburg.informatik.ultimate.automata.nestedword.UnaryNwaOperation; import de.uni_freiburg.informatik.ultimate.automata.nestedword.operations.Analyze; import de.uni_freiburg.informatik.ultimate.automata.nestedword.operations.Analyze.SymbolType; @@ -294,7 +295,7 @@ public String operationName() { * Automaton to verify validity */ public void verifyAutomatonValidity(final INestedWordAutomatonSimple automaton) { - if (!automaton.getCallAlphabet().isEmpty() || !automaton.getReturnAlphabet().isEmpty()) { + if (!NestedWordAutomataUtils.isFiniteAutomaton(automaton)) { throw new IllegalArgumentException( "The inputed automaton is no Buechi-automaton. It must have an empty call and return alphabet."); } diff --git a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/simulation/util/nwa/graph/NwaGameGraphGeneration.java b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/simulation/util/nwa/graph/NwaGameGraphGeneration.java index b6032fba6b5..46c76a92440 100644 --- a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/simulation/util/nwa/graph/NwaGameGraphGeneration.java +++ b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/operations/simulation/util/nwa/graph/NwaGameGraphGeneration.java @@ -43,6 +43,7 @@ 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.INestedWordAutomatonSimple; +import de.uni_freiburg.informatik.ultimate.automata.nestedword.VpAlphabet; import de.uni_freiburg.informatik.ultimate.automata.nestedword.NestedWordAutomaton; import de.uni_freiburg.informatik.ultimate.automata.nestedword.NestedWordAutomatonFilteredStates; import de.uni_freiburg.informatik.ultimate.automata.nestedword.operations.Determinize; @@ -736,7 +737,7 @@ public INestedWordAutomaton generateAutomatonFromGraph(final bool // If there are no merge-able states simply // copy the inputed automaton final NestedWordAutomaton resultAsChangeableAutomaton = new NestedWordAutomaton<>(mServices, - mNwa.getInternalAlphabet(), mNwa.getCallAlphabet(), mNwa.getReturnAlphabet(), stateFactory); + mNwa.getVpAlphabet(), stateFactory); for (final STATE state : mNwa.getStates()) { // Copy states final boolean isInitial = mNwa.isInitial(state); @@ -2438,9 +2439,12 @@ private INestedWordAutomatonSimple, IGameState> creat final Set> internalGameAlphabet = new HashSet<>(); final Set> callGameAlphabet = new HashSet<>(); final Set> returnGameAlphabet = new HashSet<>(); + + final VpAlphabet> gameVpAlphabet = new VpAlphabet<>(internalGameAlphabet, callGameAlphabet, returnGameAlphabet); + final NestedWordAutomaton, IGameState> gameAutomaton = new NestedWordAutomaton<>( - mServices, internalGameAlphabet, callGameAlphabet, returnGameAlphabet, new GameFactory()); + mServices, gameVpAlphabet, new GameFactory()); // Collect all data by using // (spoilerVertex -> duplicatorSucc -> spoilerSucc) diff --git a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/reachablestates/NestedWordAutomatonReachableStates.java b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/reachablestates/NestedWordAutomatonReachableStates.java index cb82ffda2f7..a630588ebb6 100644 --- a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/reachablestates/NestedWordAutomatonReachableStates.java +++ b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/reachablestates/NestedWordAutomatonReachableStates.java @@ -50,6 +50,7 @@ import de.uni_freiburg.informatik.ultimate.automata.nestedword.DownStateConsistencyCheck; import de.uni_freiburg.informatik.ultimate.automata.nestedword.IDoubleDeckerAutomaton; import de.uni_freiburg.informatik.ultimate.automata.nestedword.INwaOutgoingTransitionProvider; +import de.uni_freiburg.informatik.ultimate.automata.nestedword.VpAlphabet; import de.uni_freiburg.informatik.ultimate.automata.nestedword.NestedRun; import de.uni_freiburg.informatik.ultimate.automata.nestedword.buchi.BuchiAccepts; import de.uni_freiburg.informatik.ultimate.automata.nestedword.buchi.NestedLassoRun; @@ -103,9 +104,7 @@ public class NestedWordAutomatonReachableStates private final INwaOutgoingTransitionProvider mOperand; - private final Set mInternalAlphabet; - private final Set mCallAlphabet; - private final Set mReturnAlphabet; + private final VpAlphabet mVpAlphabet; private final Set mInitialStates = new HashSet<>(); private final Set mFinalStates = new HashSet<>(); @@ -180,9 +179,7 @@ public NestedWordAutomatonReachableStates(final AutomataLibraryServices services mServices = services; mLogger = mServices.getLoggingService().getLogger(LibraryIdentifiers.PLUGIN_ID); mOperand = operand; - mInternalAlphabet = operand.getInternalAlphabet(); - mCallAlphabet = operand.getCallAlphabet(); - mReturnAlphabet = operand.getReturnAlphabet(); + mVpAlphabet = operand.getVpAlphabet(); mStateFactory = operand.getStateFactory(); try { new ReachableStatesComputation(); @@ -318,11 +315,6 @@ public int size() { return mStates.size(); } - @Override - public Set getAlphabet() { - return mInternalAlphabet; - } - @Override public String sizeInformation() { final int states = mStates.size(); @@ -340,20 +332,10 @@ private static int computeCyclomaticComplexity(final int numberOfTransitions, fi final int numberOfSccs) { return numberOfTransitions - numberOfStates + numberOfSccs; } - - @Override - public Set getInternalAlphabet() { - return mInternalAlphabet; - } - - @Override - public Set getCallAlphabet() { - return mCallAlphabet; - } - + @Override - public Set getReturnAlphabet() { - return mReturnAlphabet; + public VpAlphabet getVpAlphabet() { + return mVpAlphabet; } @Override @@ -1061,7 +1043,7 @@ private boolean candidateForOutgoingReturn(final STATE state) { if (mOperand.hasModifiableAlphabet()) { return true; } - if (getReturnAlphabet().isEmpty()) { + if (getVpAlphabet().getReturnAlphabet().isEmpty()) { return false; } return true; diff --git a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/senwa/DifferenceSenwa.java b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/senwa/DifferenceSenwa.java index 32e02346bc2..f1c628d57c2 100644 --- a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/senwa/DifferenceSenwa.java +++ b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/senwa/DifferenceSenwa.java @@ -148,8 +148,7 @@ public & IIntersectionStateFactory> mStateDeterminizer = new StateDeterminizerCache<>(stateDeterminizer); - mSenwa = new Senwa<>(mServices, minuend.getInternalAlphabet(), minuend.getCallAlphabet(), - minuend.getReturnAlphabet(), minuend.getStateFactory()); + mSenwa = new Senwa<>(mServices, minuend.getVpAlphabet(), minuend.getStateFactory()); mSenwaWalker = new SenwaWalker<>(mServices, mSenwa, this, removeDeadEndsImmediately); mLogger.info(exitMessage()); } diff --git a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/senwa/Senwa.java b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/senwa/Senwa.java index 6ae2d3662b9..1220429312e 100644 --- a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/senwa/Senwa.java +++ b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/senwa/Senwa.java @@ -34,6 +34,7 @@ import de.uni_freiburg.informatik.ultimate.automata.AutomataLibraryServices; import de.uni_freiburg.informatik.ultimate.automata.nestedword.DoubleDeckerAutomaton; import de.uni_freiburg.informatik.ultimate.automata.nestedword.INestedWordAutomatonSimple; +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.statefactory.IStateFactory; @@ -77,9 +78,8 @@ public final class Senwa extends DoubleDeckerAutomaton internalAlphabet, - final Set callAlphabet, final Set returnAlphabet, final IStateFactory stateFactory) { - super(services, internalAlphabet, callAlphabet, returnAlphabet, stateFactory); + public Senwa(final AutomataLibraryServices services, final VpAlphabet vpAlphabet, final IStateFactory stateFactory) { + super(services, vpAlphabet, stateFactory); assert isModuleInformationConsistent(); } diff --git a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/senwa/SenwaBuilder.java b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/senwa/SenwaBuilder.java index e63c736bd48..9ca735d8293 100644 --- a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/senwa/SenwaBuilder.java +++ b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/senwa/SenwaBuilder.java @@ -84,7 +84,7 @@ public SenwaBuilder(final AutomataLibraryServices services, final ISenwaStateFac mStateFactory = stateFactory; mNwa = nwa; mLogger.info(startMessage()); - mSenwa = new Senwa<>(mServices, mNwa.getInternalAlphabet(), mNwa.getCallAlphabet(), mNwa.getReturnAlphabet(), + mSenwa = new Senwa<>(mServices, mNwa.getVpAlphabet(), mNwa.getStateFactory()); new SenwaWalker<>(mServices, mSenwa, this, true); mLogger.info(exitMessage()); diff --git a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/senwa/SenwaWalker.java b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/senwa/SenwaWalker.java index 74a6cbf137a..0eed8fe4e41 100644 --- a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/senwa/SenwaWalker.java +++ b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/senwa/SenwaWalker.java @@ -304,8 +304,7 @@ private void processNextWorkListState(final STATE state) throws AutomataOperatio protected Senwa getTotalizedEmptyAutomaton() { final Senwa emptyAutomaton = - new Senwa<>(mServices, mTraversedSenwa.getInternalAlphabet(), mTraversedSenwa.getCallAlphabet(), - mTraversedSenwa.getReturnAlphabet(), mTraversedSenwa.getStateFactory()); + new Senwa<>(mServices, mTraversedSenwa.getVpAlphabet(), mTraversedSenwa.getStateFactory()); // TODO Christian 2017-02-15 Temporary workaround, make state factory a parameter final STATE sinkState = ((ISinkStateFactory) emptyAutomaton.getStateFactory()).createSinkStateContent(); emptyAutomaton.addState(sinkState, true, false, sinkState); @@ -319,17 +318,17 @@ protected Senwa getTotalizedEmptyAutomaton() { private void getTotalizedEmptyAutomatonHelper(final Senwa emptyAutomaton, final STATE sinkState, final STATE state) { - for (final LETTER letter : emptyAutomaton.getInternalAlphabet()) { + for (final LETTER letter : emptyAutomaton.getVpAlphabet().getInternalAlphabet()) { if (!emptyAutomaton.internalSuccessors(state, letter).iterator().hasNext()) { emptyAutomaton.addInternalTransition(state, letter, sinkState); } } - for (final LETTER letter : emptyAutomaton.getCallAlphabet()) { + for (final LETTER letter : emptyAutomaton.getVpAlphabet().getCallAlphabet()) { if (!emptyAutomaton.callSuccessors(state, letter).iterator().hasNext()) { emptyAutomaton.addCallTransition(state, letter, sinkState); } } - for (final LETTER letter : emptyAutomaton.getReturnAlphabet()) { + for (final LETTER letter : emptyAutomaton.getVpAlphabet().getReturnAlphabet()) { for (final STATE hier : emptyAutomaton.getStates()) { if (!emptyAutomaton.returnSuccessors(state, hier, letter).iterator().hasNext()) { emptyAutomaton.addReturnTransition(state, hier, letter, sinkState); diff --git a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/visualization/CommonExternalFormatWriter.java b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/visualization/CommonExternalFormatWriter.java index 4e6c4309aa1..9009d179465 100644 --- a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/visualization/CommonExternalFormatWriter.java +++ b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/visualization/CommonExternalFormatWriter.java @@ -59,7 +59,7 @@ public abstract class CommonExternalFormatWriter extends GeneralA */ public CommonExternalFormatWriter(final PrintWriter writer, final INestedWordAutomaton nwa) { super(writer); - mAlphabetMapping = getAlphabetMapping(nwa.getInternalAlphabet()); + mAlphabetMapping = getAlphabetMapping(nwa.getVpAlphabet().getInternalAlphabet()); mStateMapping = getStateMapping(nwa.getStates()); mNwa = nwa; } diff --git a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/visualization/GoalFormatWriter.java b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/visualization/GoalFormatWriter.java index 42d5e4b44f4..3b761938e06 100644 --- a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/visualization/GoalFormatWriter.java +++ b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/visualization/GoalFormatWriter.java @@ -90,7 +90,7 @@ private void constructAlphabetSection(final StringBuilder builder) { builder.append(TAB) .append("") .append(NEW_LINE); - for (final LETTER letter : mNwa.getInternalAlphabet()) { + for (final LETTER letter : mNwa.getVpAlphabet().getInternalAlphabet()) { builder.append(TAB) .append(TAB) .append("") diff --git a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/visualization/HanoiFormatWriter.java b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/visualization/HanoiFormatWriter.java index ea1b6965e6c..cb1ae0362a1 100644 --- a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/visualization/HanoiFormatWriter.java +++ b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/visualization/HanoiFormatWriter.java @@ -92,18 +92,18 @@ private StringBuilder constructHeader() { } builder.append("AP: ") - .append(mNwa.getInternalAlphabet().size()); - for (final LETTER letter : mNwa.getInternalAlphabet()) { + .append(mNwa.getVpAlphabet().getInternalAlphabet().size()); + for (final LETTER letter : mNwa.getVpAlphabet().getInternalAlphabet()) { builder.append(" \"p") .append(mLetterConverter.convert(letter) + QUOTE); } builder.append(NEW_LINE); - for (final LETTER letter : mNwa.getInternalAlphabet()) { + for (final LETTER letter : mNwa.getVpAlphabet().getInternalAlphabet()) { builder.append("Alias: @") .append(mAlphabetMapping.get(letter)); boolean firstOther = true; - for (final LETTER otherLetter : mNwa.getInternalAlphabet()) { + for (final LETTER otherLetter : mNwa.getVpAlphabet().getInternalAlphabet()) { if (firstOther) { firstOther = false; } else { diff --git a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/visualization/NwaWriter.java b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/visualization/NwaWriter.java index 832897027d4..6965f09f32b 100644 --- a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/visualization/NwaWriter.java +++ b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/visualization/NwaWriter.java @@ -66,9 +66,9 @@ public abstract class NwaWriter extends GeneralAutomatonPrinter { public NwaWriter(final PrintWriter writer, final String name, final INestedWordAutomaton nwa) { super(writer); mNwa = nwa; - mInternalAlphabet = getAlphabetMapping(mNwa.getInternalAlphabet(), 'a'); - mCallAlphabet = getAlphabetMapping(mNwa.getCallAlphabet(), 'c'); - mReturnAlphabet = getAlphabetMapping(mNwa.getReturnAlphabet(), 'r'); + mInternalAlphabet = getAlphabetMapping(mNwa.getVpAlphabet().getInternalAlphabet(), 'a'); + mCallAlphabet = getAlphabetMapping(mNwa.getVpAlphabet().getCallAlphabet(), 'c'); + mReturnAlphabet = getAlphabetMapping(mNwa.getVpAlphabet().getReturnAlphabet(), 'r'); mStateMapping = getStateMapping(mNwa.getStates()); final boolean isFiniteAutomaton = mCallAlphabet.isEmpty() && mReturnAlphabet.isEmpty(); diff --git a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/petrinet/PetriNet2FiniteAutomaton.java b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/petrinet/PetriNet2FiniteAutomaton.java index adbce124466..9fddce18ac1 100644 --- a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/petrinet/PetriNet2FiniteAutomaton.java +++ b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/petrinet/PetriNet2FiniteAutomaton.java @@ -39,6 +39,7 @@ import de.uni_freiburg.informatik.ultimate.automata.AutomataLibraryException; import de.uni_freiburg.informatik.ultimate.automata.AutomataLibraryServices; import de.uni_freiburg.informatik.ultimate.automata.nestedword.INestedWordAutomaton; +import de.uni_freiburg.informatik.ultimate.automata.nestedword.VpAlphabet; import de.uni_freiburg.informatik.ultimate.automata.nestedword.NestedWordAutomaton; import de.uni_freiburg.informatik.ultimate.automata.statefactory.IPetriNet2FiniteAutomatonStateFactory; import de.uni_freiburg.informatik.ultimate.automata.statefactory.IStateFactory; @@ -91,7 +92,8 @@ public PetriNet2FiniteAutomaton(final AutomataLibraryServices services, mContentFactory = factory; final Set alphabet = new HashSet<>(operand.getAlphabet()); - mResult = new NestedWordAutomaton<>(mServices, alphabet, Collections.emptySet(), Collections.emptySet(), + final VpAlphabet vpAlphabet = new VpAlphabet(alphabet, Collections.emptySet(), Collections.emptySet()); + mResult = new NestedWordAutomaton<>(mServices, vpAlphabet, operand.getStateFactory()); getState(operand.getInitialMarking(), true); while (!mWorklist.isEmpty()) { diff --git a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/petrinet/julian/DifferenceBlackAndWhite.java b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/petrinet/julian/DifferenceBlackAndWhite.java index 0d49f12c7dd..7dfb53532d8 100644 --- a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/petrinet/julian/DifferenceBlackAndWhite.java +++ b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/petrinet/julian/DifferenceBlackAndWhite.java @@ -152,7 +152,7 @@ public String exitMessage() { } private void classifySymbols() { - for (final S symbol : mNwa.getInternalAlphabet()) { + for (final S symbol : mNwa.getVpAlphabet().getInternalAlphabet()) { final HashSet selfloopStates = new HashSet<>(); final HashSet changerStates = new HashSet<>(); for (final C state : mNwa.getStates()) { diff --git a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/petrinet/julian/PetriNetJulian.java b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/petrinet/julian/PetriNetJulian.java index aeda638cce1..05b9e30d9f4 100644 --- a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/petrinet/julian/PetriNetJulian.java +++ b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/petrinet/julian/PetriNetJulian.java @@ -138,7 +138,7 @@ public PetriNetJulian(final AutomataLibraryServices services, final Set alpha */ public PetriNetJulian(final AutomataLibraryServices services, final INestedWordAutomaton nwa) throws AutomataLibraryException { - this(services, nwa.getInternalAlphabet(), nwa.getStateFactory(), true, false); + this(services, nwa.getVpAlphabet().getInternalAlphabet(), nwa.getStateFactory(), true, false); final Map> state2place = new HashMap<>(); for (final C content : nwa.getStates()) { // C content = state.getContent(); diff --git a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/petrinet/julian/PrefixProduct.java b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/petrinet/julian/PrefixProduct.java index aca4bf8ed38..07f5202295e 100644 --- a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/petrinet/julian/PrefixProduct.java +++ b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/petrinet/julian/PrefixProduct.java @@ -148,10 +148,10 @@ private void updateSymbol2nwaTransitions(final S symbol, final AutomatonTransiti private PetriNetJulian computeResult() { final HashSet netOnlyAlphabet = new HashSet<>(mOperand.getAlphabet()); - netOnlyAlphabet.removeAll(mNwa.getInternalAlphabet()); + netOnlyAlphabet.removeAll(mNwa.getVpAlphabet().getInternalAlphabet()); final HashSet sharedAlphabet = new HashSet<>(mOperand.getAlphabet()); sharedAlphabet.removeAll(netOnlyAlphabet); - final HashSet nwaOnlyAlphabet = new HashSet<>(mNwa.getInternalAlphabet()); + final HashSet nwaOnlyAlphabet = new HashSet<>(mNwa.getVpAlphabet().getInternalAlphabet()); nwaOnlyAlphabet.removeAll(sharedAlphabet); final HashSet unionAlphabet = new HashSet<>(mOperand.getAlphabet()); unionAlphabet.addAll(nwaOnlyAlphabet); diff --git a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/statefactory/StringFactory.java b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/statefactory/StringFactory.java index fef34d542eb..0f92b40bcc6 100644 --- a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/statefactory/StringFactory.java +++ b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/statefactory/StringFactory.java @@ -179,7 +179,7 @@ public String buchiComplementFkv(final LevelRankingState complementSt return complementState.toString(); } - final boolean isNestedWordAutomaton = !complementState.getOperand().getCallAlphabet().isEmpty(); + final boolean isNestedWordAutomaton = !complementState.getOperand().getVpAlphabet().getCallAlphabet().isEmpty(); final StringBuilder builder = new StringBuilder(); builder.append(OPEN_BRACE); for (final StateWithRankInfo downState : complementState.getDownStates()) { @@ -228,7 +228,7 @@ public String buchiComplementNcsb(final LevelRankingState complementS } } } - final boolean isNestedWordAutomaton = !complementState.getOperand().getCallAlphabet().isEmpty(); + final boolean isNestedWordAutomaton = !complementState.getOperand().getVpAlphabet().getCallAlphabet().isEmpty(); final StringBuilder builder = new StringBuilder(listN.size() + listC.size() + listS.size() + listB.size()); builder.append(OPEN_PARENTHESIS); prettyprintCollectionOfStates(builder, listN, isNestedWordAutomaton); diff --git a/trunk/source/Library-InteractiveTA/src/de/uni_freiburg/informatik/ultimate/interactive/traceabstraction/Converter.java b/trunk/source/Library-InteractiveTA/src/de/uni_freiburg/informatik/ultimate/interactive/traceabstraction/Converter.java index a51efef8fc0..c4414feb638 100644 --- a/trunk/source/Library-InteractiveTA/src/de/uni_freiburg/informatik/ultimate/interactive/traceabstraction/Converter.java +++ b/trunk/source/Library-InteractiveTA/src/de/uni_freiburg/informatik/ultimate/interactive/traceabstraction/Converter.java @@ -344,9 +344,9 @@ else if (nestingRelation.getInternalNestingOrThrow(word.getCallPosition(i)) != i private static void copyAlphabets(final INestedWordAutomatonSimple fromNwa, final List callAlphabet, final List internalAlphabet, final List returnAlphabet, final TraceAbstractionProtos.NestedWordAutomaton.Builder toNwa) { - fromNwa.getCallAlphabet().forEach(callAlphabet::add); - fromNwa.getInternalAlphabet().forEach(internalAlphabet::add); - fromNwa.getReturnAlphabet().forEach(returnAlphabet::add); + fromNwa.getVpAlphabet().getCallAlphabet().forEach(callAlphabet::add); + fromNwa.getVpAlphabet().getInternalAlphabet().forEach(internalAlphabet::add); + fromNwa.getVpAlphabet().getReturnAlphabet().forEach(returnAlphabet::add); toNwa.setCall(fromAlphabet(callAlphabet)).setInternal(fromAlphabet(internalAlphabet)) .setReturn(fromAlphabet(returnAlphabet)); } diff --git a/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/CFG2NestedWordAutomaton.java b/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/CFG2NestedWordAutomaton.java index 6b7f61c9161..dca100a7af2 100644 --- a/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/CFG2NestedWordAutomaton.java +++ b/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/CFG2NestedWordAutomaton.java @@ -36,6 +36,7 @@ import de.uni_freiburg.informatik.ultimate.automata.AutomataLibraryServices; import de.uni_freiburg.informatik.ultimate.automata.nestedword.INestedWordAutomaton; +import de.uni_freiburg.informatik.ultimate.automata.nestedword.VpAlphabet; import de.uni_freiburg.informatik.ultimate.automata.nestedword.NestedWordAutomaton; import de.uni_freiburg.informatik.ultimate.automata.statefactory.IStateFactory; import de.uni_freiburg.informatik.ultimate.core.model.services.ILogger; @@ -133,8 +134,8 @@ public INestedWordAutomaton getNestedWordAutomaton(final IIc mLogger.debug("Step: construct the automaton"); // construct the automaton final NestedWordAutomaton nwa = - new NestedWordAutomaton<>(new AutomataLibraryServices(mServices), internalAlphabet, callAlphabet, - returnAlphabet, tAContentFactory); + new NestedWordAutomaton<>(new AutomataLibraryServices(mServices), + new VpAlphabet<>(internalAlphabet, callAlphabet, returnAlphabet), tAContentFactory); mLogger.debug("Step: add states"); // add states diff --git a/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/CegarLoopSWBnonRecursive.java b/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/CegarLoopSWBnonRecursive.java index ecdc5d15969..d6748b3fc28 100644 --- a/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/CegarLoopSWBnonRecursive.java +++ b/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/CegarLoopSWBnonRecursive.java @@ -206,8 +206,7 @@ protected void constructInterpolantAutomaton() throws AutomataOperationCanceledE // create an new interpolant automaton mInterpolAutomaton = new NestedWordAutomaton<>(new AutomataLibraryServices(mServices), - mNestedAbstraction.getAlphabet(), mNestedAbstraction.getCallAlphabet(), - mNestedAbstraction.getReturnAlphabet(), mNestedAbstraction.getStateFactory()); + mNestedAbstraction.getVpAlphabet(), mNestedAbstraction.getStateFactory()); // remember some of its properties mAbstractionInitialState = mInterpolantGenerator.getPrecondition(); diff --git a/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/interactive/PreNestedWord.java b/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/interactive/PreNestedWord.java index 280ea35bada..457f3bc8d7d 100644 --- a/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/interactive/PreNestedWord.java +++ b/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/interactive/PreNestedWord.java @@ -79,9 +79,9 @@ public INestedWordAutomatonSimple getAutomaton(fina final IStateFactory taContentFactory, final PredicateFactory predicateFactory, final ManagedScript script) { - final Set internalAlphabet = automaton.getAlphabet(); - final Set callAlphabet = automaton.getCallAlphabet(); - final Set returnAlphabet = automaton.getReturnAlphabet(); + final Set internalAlphabet = automaton.getVpAlphabet().getInternalAlphabet(); + final Set callAlphabet = automaton.getVpAlphabet().getCallAlphabet(); + final Set returnAlphabet = automaton.getVpAlphabet().getReturnAlphabet(); final Map internalAlphabetMap = internalAlphabet.stream().collect(Collectors.toMap(Object::hashCode, x -> x)); final Map callAlphabetMap = @@ -93,8 +93,7 @@ public INestedWordAutomatonSimple getAutomaton(fina // allAlphabetMap.putAll(callAlphabetMap); // allAlphabetMap.putAll(returnAlphabetMap); final NestedWordAutomaton nwa = - new NestedWordAutomaton<>(new AutomataLibraryServices(services), automaton.getAlphabet(), - automaton.getCallAlphabet(), automaton.getReturnAlphabet(), taContentFactory); + new NestedWordAutomaton<>(new AutomataLibraryServices(services), automaton.getVpAlphabet(), taContentFactory); IPredicate previousState = newTruePredicate(predicateFactory, script); IPredicate previousHierarchyState = null; @@ -142,9 +141,9 @@ public INestedWordAutomatonSimple getAutomaton(fina } public LETTER[] getWord(final INestedWordAutomatonSimple automaton) { - final Set internalAlphabet = automaton.getAlphabet(); - final Set callAlphabet = automaton.getCallAlphabet(); - final Set returnAlphabet = automaton.getReturnAlphabet(); + final Set internalAlphabet = automaton.getVpAlphabet().getInternalAlphabet(); + final Set callAlphabet = automaton.getVpAlphabet().getCallAlphabet(); + final Set returnAlphabet = automaton.getVpAlphabet().getReturnAlphabet(); final Map internalAlphabetMap = internalAlphabet.stream().collect(Collectors.toMap(Object::hashCode, x -> x)); final Map callAlphabetMap = diff --git a/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/interpolantautomata/builders/AbsIntNonSmtInterpolantAutomatonBuilder.java b/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/interpolantautomata/builders/AbsIntNonSmtInterpolantAutomatonBuilder.java index b92de689557..4b89bef3807 100644 --- a/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/interpolantautomata/builders/AbsIntNonSmtInterpolantAutomatonBuilder.java +++ b/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/interpolantautomata/builders/AbsIntNonSmtInterpolantAutomatonBuilder.java @@ -106,8 +106,7 @@ private NestedWordAutomaton getPathProgramAutomatonNew( } final NestedWordAutomaton result = new NestedWordAutomaton<>( - new AutomataLibraryServices(mServices), oldAbstraction.getInternalAlphabet(), - oldAbstraction.getCallAlphabet(), oldAbstraction.getReturnAlphabet(), oldAbstraction.getStateFactory()); + new AutomataLibraryServices(mServices), oldAbstraction.getVpAlphabet(), oldAbstraction.getStateFactory()); final Map newStates = new HashMap<>(); final Map callHierPreds = new HashMap<>(); diff --git a/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/interpolantautomata/builders/AbsIntStraightLineInterpolantAutomatonBuilder.java b/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/interpolantautomata/builders/AbsIntStraightLineInterpolantAutomatonBuilder.java index 02d31910018..9e42d16fe80 100644 --- a/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/interpolantautomata/builders/AbsIntStraightLineInterpolantAutomatonBuilder.java +++ b/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/interpolantautomata/builders/AbsIntStraightLineInterpolantAutomatonBuilder.java @@ -112,8 +112,7 @@ public NestedWordAutomaton getResult() { mLogger.info("Creating interpolant automaton from AI predicates (straight)"); final NestedWordAutomaton result = new NestedWordAutomaton<>( - new AutomataLibraryServices(mServices), oldAbstraction.getInternalAlphabet(), - oldAbstraction.getCallAlphabet(), oldAbstraction.getReturnAlphabet(), oldAbstraction.getStateFactory()); + new AutomataLibraryServices(mServices), oldAbstraction.getVpAlphabet(), oldAbstraction.getStateFactory()); final NestedRun cex = (NestedRun) mCurrentCounterExample; final Word word = cex.getWord(); @@ -211,10 +210,10 @@ private > void addSelfLoops( final NestedWordAutomaton result, final TripleStack callStack) { if (!result.getFinalStates().isEmpty()) { for (final IPredicate finalState : result.getFinalStates()) { - oldAbstraction.getInternalAlphabet() + oldAbstraction.getVpAlphabet().getInternalAlphabet() .forEach(l -> result.addInternalTransition(finalState, l, finalState)); - oldAbstraction.getCallAlphabet().forEach(l -> result.addCallTransition(finalState, l, finalState)); - for (final LETTER returnSymbol : oldAbstraction.getReturnAlphabet()) { + oldAbstraction.getVpAlphabet().getCallAlphabet().forEach(l -> result.addCallTransition(finalState, l, finalState)); + for (final LETTER returnSymbol : oldAbstraction.getVpAlphabet().getReturnAlphabet()) { final IIcfgReturnTransition ret = (IIcfgReturnTransition) returnSymbol; result.addReturnTransition(finalState, finalState, returnSymbol, finalState); for (final Triple> openCall : callStack) { diff --git a/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/interpolantautomata/builders/AbsIntTotalInterpolationAutomatonBuilder.java b/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/interpolantautomata/builders/AbsIntTotalInterpolationAutomatonBuilder.java index 72193017449..08e37c74248 100644 --- a/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/interpolantautomata/builders/AbsIntTotalInterpolationAutomatonBuilder.java +++ b/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/interpolantautomata/builders/AbsIntTotalInterpolationAutomatonBuilder.java @@ -137,8 +137,7 @@ private NestedWordAutomaton constructAutomaton( mLogger.info("Creating interpolant automaton from AI predicates (total)"); final NestedWordAutomaton result = new NestedWordAutomaton<>( - new AutomataLibraryServices(mServices), oldAbstraction.getInternalAlphabet(), - oldAbstraction.getCallAlphabet(), oldAbstraction.getReturnAlphabet(), oldAbstraction.getStateFactory()); + new AutomataLibraryServices(mServices), oldAbstraction.getVpAlphabet(), oldAbstraction.getStateFactory()); final NestedRun counterExample = (NestedRun) mCurrentCounterExample; final Word word = counterExample.getWord(); diff --git a/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/interpolantautomata/builders/CanonicalInterpolantAutomatonBuilder.java b/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/interpolantautomata/builders/CanonicalInterpolantAutomatonBuilder.java index 48364dacac7..dc292b4fbdd 100644 --- a/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/interpolantautomata/builders/CanonicalInterpolantAutomatonBuilder.java +++ b/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/interpolantautomata/builders/CanonicalInterpolantAutomatonBuilder.java @@ -34,7 +34,7 @@ import java.util.Set; import de.uni_freiburg.informatik.ultimate.automata.AutomataLibraryServices; -import de.uni_freiburg.informatik.ultimate.automata.nestedword.InCaReAlphabet; +import de.uni_freiburg.informatik.ultimate.automata.nestedword.VpAlphabet; 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.statefactory.IStateFactory; @@ -65,13 +65,12 @@ public class CanonicalInterpolantAutomatonBuilder extends CoverageAn public CanonicalInterpolantAutomatonBuilder(final IUltimateServiceProvider services, final InterpolantsPreconditionPostcondition ipp, final List programPointSequence, - final InCaReAlphabet alphabet, final CfgSmtToolkit csToolkit, + final VpAlphabet alphabet, final CfgSmtToolkit csToolkit, final IStateFactory predicateFactory, final ILogger logger, final IPredicateUnifier predicateUnifier, final NestedWord nestedWord) { super(services, ipp, programPointSequence, logger, predicateUnifier); mNestedWord = nestedWord; - mIA = new NestedWordAutomaton<>(new AutomataLibraryServices(mServices), alphabet.getInternalAlphabet(), - alphabet.getCallAlphabet(), alphabet.getReturnAlphabet(), predicateFactory); + mIA = new NestedWordAutomaton<>(new AutomataLibraryServices(mServices), alphabet, predicateFactory); } @Override @@ -96,13 +95,13 @@ protected void processCoveringResult(final int currentPosition, final int previo protected void postprocess() { if (mSelfloopAtInitial) { final IPredicate precond = mIpp.getPrecondition(); - for (final LETTER symbol : mIA.getInternalAlphabet()) { + for (final LETTER symbol : mIA.getVpAlphabet().getInternalAlphabet()) { mIA.addInternalTransition(precond, symbol, precond); } - for (final LETTER symbol : mIA.getCallAlphabet()) { + for (final LETTER symbol : mIA.getVpAlphabet().getCallAlphabet()) { mIA.addCallTransition(precond, symbol, precond); } - for (final LETTER symbol : mIA.getReturnAlphabet()) { + for (final LETTER symbol : mIA.getVpAlphabet().getReturnAlphabet()) { mIA.addReturnTransition(precond, precond, symbol, precond); for (final Integer pos : mAlternativeCallPredecessors.keySet()) { for (final IPredicate hier : mAlternativeCallPredecessors.get(pos)) { @@ -114,13 +113,13 @@ protected void postprocess() { if (mSelfloopAtFinal) { final IPredicate postcond = mIpp.getPostcondition(); - for (final LETTER symbol : mIA.getInternalAlphabet()) { + for (final LETTER symbol : mIA.getVpAlphabet().getInternalAlphabet()) { mIA.addInternalTransition(postcond, symbol, postcond); } - for (final LETTER symbol : mIA.getCallAlphabet()) { + for (final LETTER symbol : mIA.getVpAlphabet().getCallAlphabet()) { mIA.addCallTransition(postcond, symbol, postcond); } - for (final LETTER symbol : mIA.getReturnAlphabet()) { + for (final LETTER symbol : mIA.getVpAlphabet().getReturnAlphabet()) { mIA.addReturnTransition(postcond, postcond, symbol, postcond); for (final Integer pos : mAlternativeCallPredecessors.keySet()) { for (final IPredicate hier : mAlternativeCallPredecessors.get(pos)) { diff --git a/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/interpolantautomata/builders/InterpolantAutomatonBuilderFactory.java b/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/interpolantautomata/builders/InterpolantAutomatonBuilderFactory.java index 1ef068f8f3b..121f03dd178 100644 --- a/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/interpolantautomata/builders/InterpolantAutomatonBuilderFactory.java +++ b/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/interpolantautomata/builders/InterpolantAutomatonBuilderFactory.java @@ -32,7 +32,7 @@ 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.InCaReAlphabet; +import de.uni_freiburg.informatik.ultimate.automata.nestedword.VpAlphabet; 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; @@ -176,7 +176,7 @@ private IInterpolantAutomatonBuilder createBuilderCanonical( @SuppressWarnings("unchecked") final CanonicalInterpolantAutomatonBuilder iab = new CanonicalInterpolantAutomatonBuilder<>(mServices, ipp, counterexample.getStateSequence(), - new InCaReAlphabet<>(abstraction), mCsToolkit, mPredicateFactory, mLogger, + new VpAlphabet<>(abstraction), mCsToolkit, mPredicateFactory, mLogger, interpolGenerator.getPredicateUnifier(), (NestedWord) interpolGenerator.getTrace()); iab.analyze(); mLogger.info("Interpolants " + iab.getResult().getStates()); @@ -191,7 +191,7 @@ private IInterpolantAutomatonBuilder createBuilderSingleTrac final IAutomaton abstraction, final IInterpolantGenerator interpolGenerator, final IRun counterexample, final List ipps) { final StraightLineInterpolantAutomatonBuilder iab = new StraightLineInterpolantAutomatonBuilder<>( - mServices, new InCaReAlphabet<>(abstraction), interpolGenerator, mPredicateFactory); + mServices, new VpAlphabet<>(abstraction), interpolGenerator, mPredicateFactory); return iab; } diff --git a/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/interpolantautomata/builders/MultiTrackInterpolantAutomatonBuilder.java b/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/interpolantautomata/builders/MultiTrackInterpolantAutomatonBuilder.java index fc132b3257d..d638467c938 100644 --- a/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/interpolantautomata/builders/MultiTrackInterpolantAutomatonBuilder.java +++ b/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/interpolantautomata/builders/MultiTrackInterpolantAutomatonBuilder.java @@ -26,15 +26,13 @@ */ package de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.interpolantautomata.builders; -import java.util.Collections; import java.util.Iterator; import java.util.List; -import java.util.Set; import de.uni_freiburg.informatik.ultimate.automata.AutomataLibraryServices; import de.uni_freiburg.informatik.ultimate.automata.IAutomaton; import de.uni_freiburg.informatik.ultimate.automata.IRun; -import de.uni_freiburg.informatik.ultimate.automata.nestedword.INestedWordAutomatonSimple; +import de.uni_freiburg.informatik.ultimate.automata.nestedword.VpAlphabet; 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.statefactory.IStateFactory; @@ -89,23 +87,9 @@ private NestedWordAutomaton constructInterpolantAutomaton( final IUltimateServiceProvider services, final IAutomaton abstraction, final List interpolantSequences, final NestedWord nestedWord, final IStateFactory taContentFactory) { - final Set internalAlphabet = abstraction.getAlphabet(); - final Set callAlphabet; - final Set returnAlphabet; - - if (abstraction instanceof INestedWordAutomatonSimple) { - final INestedWordAutomatonSimple abstractionAsNwa = - (INestedWordAutomatonSimple) abstraction; - callAlphabet = abstractionAsNwa.getCallAlphabet(); - returnAlphabet = abstractionAsNwa.getReturnAlphabet(); - } else { - callAlphabet = Collections.emptySet(); - returnAlphabet = Collections.emptySet(); - } final NestedWordAutomaton nwa = - new NestedWordAutomaton<>(new AutomataLibraryServices(services), internalAlphabet, callAlphabet, - returnAlphabet, taContentFactory); + new NestedWordAutomaton<>(new AutomataLibraryServices(services), new VpAlphabet<>(abstraction), taContentFactory); addStatesAccordingToPredicates(nwa, interpolantSequences, nestedWord); addBasicTransitions(nwa, interpolantSequences, nestedWord); diff --git a/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/interpolantautomata/builders/StraightLineInterpolantAutomatonBuilder.java b/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/interpolantautomata/builders/StraightLineInterpolantAutomatonBuilder.java index e83bb9ee8e1..83766eab460 100644 --- a/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/interpolantautomata/builders/StraightLineInterpolantAutomatonBuilder.java +++ b/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/interpolantautomata/builders/StraightLineInterpolantAutomatonBuilder.java @@ -27,7 +27,7 @@ package de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.interpolantautomata.builders; import de.uni_freiburg.informatik.ultimate.automata.AutomataLibraryServices; -import de.uni_freiburg.informatik.ultimate.automata.nestedword.InCaReAlphabet; +import de.uni_freiburg.informatik.ultimate.automata.nestedword.VpAlphabet; import de.uni_freiburg.informatik.ultimate.automata.nestedword.NestedWord; import de.uni_freiburg.informatik.ultimate.automata.nestedword.NestedWordAutomaton; import de.uni_freiburg.informatik.ultimate.core.model.services.IUltimateServiceProvider; @@ -55,13 +55,12 @@ public class StraightLineInterpolantAutomatonBuilder private final NestedWordAutomaton mResult; public StraightLineInterpolantAutomatonBuilder(final IUltimateServiceProvider services, - final InCaReAlphabet alphabet, final IInterpolantGenerator interpolantGenerator, + final VpAlphabet alphabet, final IInterpolantGenerator interpolantGenerator, final PredicateFactoryForInterpolantAutomata predicateFactory) { mServices = services; final InterpolantsPreconditionPostcondition ipp = new InterpolantsPreconditionPostcondition(interpolantGenerator); - mResult = new NestedWordAutomaton<>(new AutomataLibraryServices(mServices), alphabet.getInternalAlphabet(), - alphabet.getCallAlphabet(), alphabet.getReturnAlphabet(), predicateFactory); + mResult = new NestedWordAutomaton<>(new AutomataLibraryServices(mServices), alphabet, predicateFactory); addStatesAndTransitions(interpolantGenerator, predicateFactory, ipp); } diff --git a/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/interpolantautomata/builders/TotalInterpolationAutomatonBuilder.java b/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/interpolantautomata/builders/TotalInterpolationAutomatonBuilder.java index e070f30435f..ddfa9f7ad5a 100644 --- a/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/interpolantautomata/builders/TotalInterpolationAutomatonBuilder.java +++ b/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/interpolantautomata/builders/TotalInterpolationAutomatonBuilder.java @@ -42,7 +42,7 @@ import de.uni_freiburg.informatik.ultimate.automata.AutomataOperationCanceledException; import de.uni_freiburg.informatik.ultimate.automata.AutomatonEpimorphism; import de.uni_freiburg.informatik.ultimate.automata.nestedword.INestedWordAutomaton; -import de.uni_freiburg.informatik.ultimate.automata.nestedword.InCaReAlphabet; +import de.uni_freiburg.informatik.ultimate.automata.nestedword.VpAlphabet; 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.NestedWordAutomataUtils; @@ -129,7 +129,7 @@ public TotalInterpolationAutomatonBuilder(final INestedWordAutomaton alphabet = new InCaReAlphabet<>(abstraction); + final VpAlphabet alphabet = new VpAlphabet<>(abstraction); mIA = new StraightLineInterpolantAutomatonBuilder<>(mServices, alphabet, interpolantGenerator, predicateFactory) .getResult(); mModifiedGlobals = modifiableGlobalsTable; diff --git a/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/interpolantautomata/builders/TwoTrackInterpolantAutomatonBuilder.java b/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/interpolantautomata/builders/TwoTrackInterpolantAutomatonBuilder.java index ba632a7389b..2fe009aad23 100644 --- a/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/interpolantautomata/builders/TwoTrackInterpolantAutomatonBuilder.java +++ b/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/interpolantautomata/builders/TwoTrackInterpolantAutomatonBuilder.java @@ -27,14 +27,12 @@ */ package de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.interpolantautomata.builders; -import java.util.HashSet; import java.util.List; -import java.util.Set; import de.uni_freiburg.informatik.ultimate.automata.AutomataLibraryServices; import de.uni_freiburg.informatik.ultimate.automata.IAutomaton; import de.uni_freiburg.informatik.ultimate.automata.IRun; -import de.uni_freiburg.informatik.ultimate.automata.nestedword.INestedWordAutomatonSimple; +import de.uni_freiburg.informatik.ultimate.automata.nestedword.VpAlphabet; 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.statefactory.IStateFactory; @@ -93,20 +91,8 @@ public TwoTrackInterpolantAutomatonBuilder(final IUltimateServiceProvider servic private NestedWordAutomaton buildTwoTrackInterpolantAutomaton( final IAutomaton abstraction, final IStateFactory tAContentFactory) { - final Set internalAlphabet = abstraction.getAlphabet(); - Set callAlphabet = new HashSet<>(0); - Set returnAlphabet = new HashSet<>(0); - - if (abstraction instanceof INestedWordAutomatonSimple) { - final INestedWordAutomatonSimple abstractionAsNwa = - (INestedWordAutomatonSimple) abstraction; - callAlphabet = abstractionAsNwa.getCallAlphabet(); - returnAlphabet = abstractionAsNwa.getReturnAlphabet(); - } - final NestedWordAutomaton nwa = - new NestedWordAutomaton<>(new AutomataLibraryServices(mServices), internalAlphabet, callAlphabet, - returnAlphabet, tAContentFactory); + new NestedWordAutomaton<>(new AutomataLibraryServices(mServices), new VpAlphabet<>(abstraction), tAContentFactory); // Add states, which contains the predicates computed via SP, WP. addStatesAccordingToPredicates(nwa); diff --git a/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/interpolantautomata/transitionappender/AbstractInterpolantAutomaton.java b/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/interpolantautomata/transitionappender/AbstractInterpolantAutomaton.java index 3278d7fe5b8..cb1441d3408 100644 --- a/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/interpolantautomata/transitionappender/AbstractInterpolantAutomaton.java +++ b/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/interpolantautomata/transitionappender/AbstractInterpolantAutomaton.java @@ -35,6 +35,7 @@ import de.uni_freiburg.informatik.ultimate.automata.AutomatonDefinitionPrinter.Format; import de.uni_freiburg.informatik.ultimate.automata.nestedword.INestedWordAutomaton; import de.uni_freiburg.informatik.ultimate.automata.nestedword.INestedWordAutomatonSimple; +import de.uni_freiburg.informatik.ultimate.automata.nestedword.VpAlphabet; import de.uni_freiburg.informatik.ultimate.automata.nestedword.NestedWordAutomataUtils; import de.uni_freiburg.informatik.ultimate.automata.nestedword.NestedWordAutomatonCache; import de.uni_freiburg.informatik.ultimate.automata.nestedword.NwaCacheBookkeeping; @@ -118,8 +119,7 @@ public AbstractInterpolantAutomaton(final IUltimateServiceProvider services, fin mCaSucComp = new CallSuccessorComputationHelper(); mReSucComp = new ReturnSuccessorComputationHelper(); mAlreadyConstrucedAutomaton = new NestedWordAutomatonCache<>(new AutomataLibraryServices(mServices), - inputInterpolantAutomaton.getInternalAlphabet(), inputInterpolantAutomaton.getCallAlphabet(), - inputInterpolantAutomaton.getReturnAlphabet(), inputInterpolantAutomaton.getStateFactory()); + inputInterpolantAutomaton.getVpAlphabet(), inputInterpolantAutomaton.getStateFactory()); if (useEfficientTotalAutomatonBookkeeping) { mSuccessorComputationBookkeeping = new SuccessorComputationBookkeepingForTotalAutomata(); } else { @@ -180,18 +180,8 @@ public final String sizeInformation() { } @Override - public final Set getInternalAlphabet() { - return mAlreadyConstrucedAutomaton.getInternalAlphabet(); - } - - @Override - public final Set getCallAlphabet() { - return mAlreadyConstrucedAutomaton.getCallAlphabet(); - } - - @Override - public final Set getReturnAlphabet() { - return mAlreadyConstrucedAutomaton.getReturnAlphabet(); + public VpAlphabet getVpAlphabet() { + return mAlreadyConstrucedAutomaton.getVpAlphabet(); } @Override @@ -221,17 +211,17 @@ public final boolean isFinal(final IPredicate state) { @Override public final Set lettersInternal(final IPredicate state) { - return getInternalAlphabet(); + return getVpAlphabet().getInternalAlphabet(); } @Override public final Set lettersCall(final IPredicate state) { - return getCallAlphabet(); + return getVpAlphabet().getCallAlphabet(); } @Override public final Set lettersReturn(final IPredicate state, final IPredicate hier) { - return getReturnAlphabet(); + return getVpAlphabet().getReturnAlphabet(); } @Override diff --git a/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/singletracecheck/InterpolantConsolidation.java b/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/singletracecheck/InterpolantConsolidation.java index 13183914bca..86005d22741 100644 --- a/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/singletracecheck/InterpolantConsolidation.java +++ b/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/singletracecheck/InterpolantConsolidation.java @@ -45,6 +45,7 @@ import de.uni_freiburg.informatik.ultimate.automata.Word; import de.uni_freiburg.informatik.ultimate.automata.nestedword.INestedWordAutomaton; import de.uni_freiburg.informatik.ultimate.automata.nestedword.INestedWordAutomatonSimple; +import de.uni_freiburg.informatik.ultimate.automata.nestedword.VpAlphabet; 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.operations.Difference; @@ -538,8 +539,8 @@ private NestedWordAutomaton constructInterpolantAutomaton(fi csToolkit.getManagedScript(), predicateFactor, taPrefs.computeHoareAnnotation()); final NestedWordAutomaton nwa = - new NestedWordAutomaton<>(new AutomataLibraryServices(services), internalAlphabet, callAlphabet, - returnAlphabet, predicateFactoryFia); + new NestedWordAutomaton<>(new AutomataLibraryServices(services), new VpAlphabet<>(internalAlphabet, callAlphabet, + returnAlphabet), predicateFactoryFia); // Set the initial and the final state of the automaton nwa.addState(true, false, traceChecker.getPrecondition()); nwa.addState(false, true, traceChecker.getPostcondition()); diff --git a/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/singletracecheck/PathProgramAutomatonConstructor.java b/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/singletracecheck/PathProgramAutomatonConstructor.java index ec39be6f6b9..7d5d7db7e7c 100644 --- a/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/singletracecheck/PathProgramAutomatonConstructor.java +++ b/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/singletracecheck/PathProgramAutomatonConstructor.java @@ -35,6 +35,7 @@ import de.uni_freiburg.informatik.ultimate.automata.AutomataLibraryServices; import de.uni_freiburg.informatik.ultimate.automata.nestedword.INestedWordAutomaton; +import de.uni_freiburg.informatik.ultimate.automata.nestedword.VpAlphabet; 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.statefactory.IStateFactory; @@ -91,9 +92,9 @@ public INestedWordAutomaton constructAutomatonFromGivenPath( final IStateFactory predicateFactoryFia = new PredicateFactoryForInterpolantAutomata( csToolkit.getManagedScript(), predicateFactory, taPrefs.computeHoareAnnotation()); // Create the automaton - final NestedWordAutomaton pathPA = - new NestedWordAutomaton<>(new AutomataLibraryServices(services), internalAlphabet, callAlphabet, - returnAlphabet, predicateFactoryFia); + final NestedWordAutomaton pathPA = new NestedWordAutomaton<>( + new AutomataLibraryServices(services), + new VpAlphabet<>(internalAlphabet, callAlphabet, returnAlphabet), predicateFactoryFia); // We need this list to create the transitions of the automaton. mPositionsToStates = new ArrayList<>(path.length() + 1); diff --git a/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/witnesschecking/WitnessLocationMatcher.java b/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/witnesschecking/WitnessLocationMatcher.java index fb7f67b85ae..f5714eb8f17 100644 --- a/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/witnesschecking/WitnessLocationMatcher.java +++ b/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/witnesschecking/WitnessLocationMatcher.java @@ -66,16 +66,16 @@ public WitnessLocationMatcher(final IUltimateServiceProvider services, final INestedWordAutomatonSimple witnessAutomaton) { mServices = services; mLogger = mServices.getLoggingService().getLogger(Activator.PLUGIN_ID); - partitionEdges(witnessAutomaton.getInternalAlphabet()); - matchLocations(controlFlowAutomaton.getInternalAlphabet()); - matchLocations(controlFlowAutomaton.getCallAlphabet()); - matchLocations(controlFlowAutomaton.getReturnAlphabet()); - mUnmatchedWitnessLetters = new ArrayList<>(witnessAutomaton.getInternalAlphabet()); + partitionEdges(witnessAutomaton.getVpAlphabet().getInternalAlphabet()); + matchLocations(controlFlowAutomaton.getVpAlphabet().getInternalAlphabet()); + matchLocations(controlFlowAutomaton.getVpAlphabet().getCallAlphabet()); + matchLocations(controlFlowAutomaton.getVpAlphabet().getReturnAlphabet()); + mUnmatchedWitnessLetters = new ArrayList<>(witnessAutomaton.getVpAlphabet().getInternalAlphabet()); mUnmatchedWitnessLetters.removeAll(mWitnessLetters2SingleLineLocations.getDomain()); // for (WitnessEdge witnessLetter : mUnmatchedWitnessLetters) { // mLogger.info("Unmatched witness edge: " + witnessLetter); // } - mLogger.info(witnessAutomaton.getInternalAlphabet().size() + " witness edges"); + mLogger.info(witnessAutomaton.getVpAlphabet().getInternalAlphabet().size() + " witness edges"); mLogger.info(mPureAnnotationEdges.size() + " pure annotation edges"); mLogger.info(mUnmatchedWitnessLetters.size() + " unmatched witness edges"); mLogger.info(mWitnessLetters2SingleLineLocations.getDomain().size() + " matched witness edges"); diff --git a/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/witnesschecking/WitnessModelToAutomatonTransformer.java b/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/witnesschecking/WitnessModelToAutomatonTransformer.java index 33735fa5764..ed420e7f95d 100644 --- a/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/witnesschecking/WitnessModelToAutomatonTransformer.java +++ b/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/witnesschecking/WitnessModelToAutomatonTransformer.java @@ -27,12 +27,12 @@ package de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.witnesschecking; import java.util.ArrayDeque; -import java.util.Collections; import java.util.LinkedHashSet; import java.util.Set; import de.uni_freiburg.informatik.ultimate.automata.AutomataLibraryServices; import de.uni_freiburg.informatik.ultimate.automata.nestedword.INestedWordAutomaton; +import de.uni_freiburg.informatik.ultimate.automata.nestedword.VpAlphabet; import de.uni_freiburg.informatik.ultimate.automata.nestedword.NestedWordAutomaton; import de.uni_freiburg.informatik.ultimate.automata.statefactory.IStateFactory; import de.uni_freiburg.informatik.ultimate.core.model.services.IUltimateServiceProvider; @@ -49,12 +49,9 @@ public WitnessModelToAutomatonTransformer(final WitnessNode witnessRoot, final I super(); mWitnessRoot = witnessRoot; final Set internalAlphabet = new LinkedHashSet<>(); - final Set callAlphabet = Collections.emptySet(); - final Set returnAlphabet = Collections.emptySet(); final IStateFactory stateFactory = new IStateFactory() { }; - mResult = new NestedWordAutomaton<>(new AutomataLibraryServices(services), internalAlphabet, callAlphabet, - returnAlphabet, stateFactory); + mResult = new NestedWordAutomaton<>(new AutomataLibraryServices(services), new VpAlphabet<>(internalAlphabet), stateFactory); constructAutomaton(internalAlphabet); } diff --git a/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/witnesschecking/WitnessProductAutomaton.java b/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/witnesschecking/WitnessProductAutomaton.java index 325ca222522..34bbdb33c58 100644 --- a/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/witnesschecking/WitnessProductAutomaton.java +++ b/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/witnesschecking/WitnessProductAutomaton.java @@ -36,6 +36,7 @@ import java.util.Set; import de.uni_freiburg.informatik.ultimate.automata.nestedword.INestedWordAutomatonSimple; +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; @@ -168,18 +169,8 @@ public String sizeInformation() { } @Override - public Set getInternalAlphabet() { - return mControlFlowAutomaton.getInternalAlphabet(); - } - - @Override - public Set getCallAlphabet() { - return mControlFlowAutomaton.getCallAlphabet(); - } - - @Override - public Set getReturnAlphabet() { - return mControlFlowAutomaton.getReturnAlphabet(); + public VpAlphabet getVpAlphabet() { + return mControlFlowAutomaton.getVpAlphabet(); } @Override diff --git a/trunk/source/TraceAbstractionConcurrent/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstractionconcurrent/CFG2Automaton.java b/trunk/source/TraceAbstractionConcurrent/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstractionconcurrent/CFG2Automaton.java index 25f55abfb73..f7adf5ea7f2 100644 --- a/trunk/source/TraceAbstractionConcurrent/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstractionconcurrent/CFG2Automaton.java +++ b/trunk/source/TraceAbstractionConcurrent/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstractionconcurrent/CFG2Automaton.java @@ -37,6 +37,7 @@ import de.uni_freiburg.informatik.ultimate.automata.AutomataLibraryServices; import de.uni_freiburg.informatik.ultimate.automata.nestedword.INestedWordAutomaton; +import de.uni_freiburg.informatik.ultimate.automata.nestedword.VpAlphabet; import de.uni_freiburg.informatik.ultimate.automata.nestedword.NestedWordAutomaton; import de.uni_freiburg.informatik.ultimate.automata.statefactory.IStateFactory; import de.uni_freiburg.informatik.ultimate.core.model.services.ILogger; @@ -163,8 +164,6 @@ private INestedWordAutomaton getNestedWordAutomaton(final Ic mLogger.debug("Step: determine the alphabet"); // determine the alphabet final Set internalAlphabet = new HashSet<>(); - final Set callAlphabet = new HashSet<>(0); - final Set returnAlphabet = new HashSet<>(0); // add transAnnot from sharedVars initialization internalAlphabet.add(mSharedVarsInit); @@ -179,9 +178,8 @@ private INestedWordAutomaton getNestedWordAutomaton(final Ic mLogger.debug("Step: construct the automaton"); // construct the automaton - final NestedWordAutomaton nwa = - new NestedWordAutomaton<>(new AutomataLibraryServices(mServices), internalAlphabet, callAlphabet, - returnAlphabet, mContentFactory); + final NestedWordAutomaton nwa = new NestedWordAutomaton<>( + new AutomataLibraryServices(mServices), new VpAlphabet(internalAlphabet), mContentFactory); IPredicate procedureInitialState = null; diff --git a/trunk/source/TraceAbstractionWithAFAs/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstractionwithafas/RAFA_Determination.java b/trunk/source/TraceAbstractionWithAFAs/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstractionwithafas/RAFA_Determination.java index b93b6396019..76f77c365c6 100644 --- a/trunk/source/TraceAbstractionWithAFAs/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstractionwithafas/RAFA_Determination.java +++ b/trunk/source/TraceAbstractionWithAFAs/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstractionwithafas/RAFA_Determination.java @@ -27,13 +27,13 @@ package de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstractionwithafas; import java.util.BitSet; -import java.util.Collections; import java.util.LinkedList; import de.uni_freiburg.informatik.ultimate.automata.AutomataLibraryException; import de.uni_freiburg.informatik.ultimate.automata.AutomataLibraryServices; import de.uni_freiburg.informatik.ultimate.automata.GeneralOperation; import de.uni_freiburg.informatik.ultimate.automata.alternating.AlternatingAutomaton; +import de.uni_freiburg.informatik.ultimate.automata.nestedword.VpAlphabet; import de.uni_freiburg.informatik.ultimate.automata.nestedword.NestedWordAutomaton; import de.uni_freiburg.informatik.ultimate.automata.statefactory.IStateFactory; import de.uni_freiburg.informatik.ultimate.modelcheckerutils.cfg.CfgSmtToolkit; @@ -55,9 +55,7 @@ public RAFA_Determination(final AutomataLibraryServices services, mCsToolkit = csToolkit; mPredicateUnifier = predicateUnifier; mResultAutomaton = new NestedWordAutomaton<>(services, - alternatingAutomaton.getAlphabet(), - Collections. emptySet(), - Collections. emptySet(), + new VpAlphabet<>(alternatingAutomaton.getAlphabet()), alternatingAutomaton.getStateFactory()); final LinkedList newStates = new LinkedList<>(); newStates.add(alternatingAutomaton.getFinalStatesBitVector());