refactoring automata library: do not store alphabet in three sets, bu…

…t introduce an visibly pushdown alphabet object
ultimate-pa · May 17, 2017 · e4bb2b1 · e4bb2b1
1 parent a3be1a3
commit e4bb2b1
Show file tree

Hide file tree

Showing 110 changed files with 474 additions and 671 deletions.
diff --git a/...k/ultimate/plugins/generator/automatascriptinterpreter/AutomataDefinitionInterpreter.java b/...k/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<String, String> nw = new NestedWordAutomaton<>(new AutomataLibraryServices(mServices),
-				internalAlphabet, callAlphabet, returnAlphabet, new StringFactory());
+				new VpAlphabet<String>(internalAlphabet, callAlphabet, returnAlphabet), new StringFactory());
 
 		// add the states
 		for (final String state : allStates) {

diff --git a/...timate/plugins/generator/automatascriptinterpreter/AutomataScriptInterpreterObserver.java b/...timate/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<String, String> getDummyAutomatonWithMessage() {
 		final NestedWordAutomaton<String, String> dummyAutomaton = new NestedWordAutomaton<>(
-				new AutomataLibraryServices(mServices), new HashSet<String>(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/...timate/plugins/analysis/automatondeltadebugger/factories/INestedWordAutomatonFactory.java b/...timate/plugins/analysis/automatondeltadebugger/factories/INestedWordAutomatonFactory.java
@@ -70,7 +70,7 @@ public INestedWordAutomatonFactory(final INestedWordAutomaton<LETTER, STATE> aut
 	 * @return new {@link INestedWordAutomaton} object
 	 */
 	public INestedWordAutomaton<LETTER, STATE> create(final INestedWordAutomaton<LETTER, STATE> 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<LETTER, STATE> create(final INestedWordAutomaton<LET
 	public INestedWordAutomaton<LETTER, STATE> create(final Set<LETTER> internalAlphabet,
 			final Set<LETTER> callAlphabet, final Set<LETTER> returnAlphabet) {
 		final Set<LETTER> internalAlphabetRes =
-				(internalAlphabet == null) ? mAutomaton.getInternalAlphabet() : internalAlphabet;
-		final Set<LETTER> callAlphabetRes = (callAlphabet == null) ? mAutomaton.getCallAlphabet() : callAlphabet;
+				(internalAlphabet == null) ? mAutomaton.getVpAlphabet().getInternalAlphabet() : internalAlphabet;
+		final Set<LETTER> callAlphabetRes = (callAlphabet == null) ? mAutomaton.getVpAlphabet().getCallAlphabet() : callAlphabet;
 		final Set<LETTER> returnAlphabetRes =
-				(returnAlphabet == null) ? mAutomaton.getReturnAlphabet() : returnAlphabet;
+				(returnAlphabet == null) ? mAutomaton.getVpAlphabet().getReturnAlphabet() : returnAlphabet;
 
 		return createWithAlphabets(internalAlphabetRes, callAlphabetRes, returnAlphabetRes);
 	}

diff --git a/...ltimate/plugins/analysis/automatondeltadebugger/factories/NestedWordAutomatonFactory.java b/...ltimate/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<LETTER, STATE> getNwa(final INestedWordAutomaton<LET
 	@Override
 	protected INestedWordAutomaton<LETTER, STATE> createWithAlphabets(final Set<LETTER> internalAlphabet,
 			final Set<LETTER> callAlphabet, final Set<LETTER> 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/...atik/ultimate/plugins/analysis/automatondeltadebugger/shrinkers/UnusedLetterShrinker.java b/...atik/ultimate/plugins/analysis/automatondeltadebugger/shrinkers/UnusedLetterShrinker.java
@@ -65,9 +65,9 @@ public UnusedLetterShrinker(final IUltimateServiceProvider services) {
 	public INestedWordAutomaton<LETTER, STATE> createAutomaton(final List<TypedLetter<LETTER>> list) {
 		// create alphabets
 		final ListIterator<TypedLetter<LETTER>> lit = list.listIterator();
-		final Set<LETTER> internalAlphabet = unwrapLetters(lit, mAutomaton.getInternalAlphabet(), LetterType.INTERNAL);
-		final Set<LETTER> callAlphabet = unwrapLetters(lit, mAutomaton.getCallAlphabet(), LetterType.CALL);
-		final Set<LETTER> returnAlphabet = unwrapLetters(lit, mAutomaton.getReturnAlphabet(), LetterType.RETURN);
+		final Set<LETTER> internalAlphabet = unwrapLetters(lit, mAutomaton.getVpAlphabet().getInternalAlphabet(), LetterType.INTERNAL);
+		final Set<LETTER> callAlphabet = unwrapLetters(lit, mAutomaton.getVpAlphabet().getCallAlphabet(), LetterType.CALL);
+		final Set<LETTER> returnAlphabet = unwrapLetters(lit, mAutomaton.getVpAlphabet().getReturnAlphabet(), LetterType.RETURN);
 
 		// create fresh automaton
 		final INestedWordAutomaton<LETTER, STATE> automaton =
@@ -103,9 +103,9 @@ public List<TypedLetter<LETTER>> extractList() {
 
 		// wrap complement of present letters to include type information
 		final ArrayList<TypedLetter<LETTER>> 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/.../de/uni_freiburg/informatik/ultimate/plugins/generator/buchiautomizer/BuchiCegarLoop.java b/.../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<LETTER, IPredicate> run) throws AutomataOperationCanceledException {
 		final CanonicalInterpolantAutomatonBuilder<? extends Object, LETTER> 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/...src/de/uni_freiburg/informatik/ultimate/plugins/generator/buchiautomizer/RefineBuchi.java b/...src/de/uni_freiburg/informatik/ultimate/plugins/generator/buchiautomizer/RefineBuchi.java
@@ -313,7 +313,7 @@ INestedWordAutomaton<LETTER, IPredicate> 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<LETTER, IPredicate> 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<LETTER, IPredicate> constructBuchiInterpolantAutomat
 			final NestedWord<LETTER> loop, final IPredicate[] loopInterpolants,
 			final INestedWordAutomatonSimple<LETTER, IPredicate> abstraction) {
 		final NestedWordAutomaton<LETTER, IPredicate> 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/.../uni_freiburg/informatik/ultimate/plugins/generator/emptinesscheck/NWAEmptinessCheck.java b/.../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<IIcfgTransition<
 		private final Set<IIcfgTransition<?>> mInternalAlphabet = new HashSet<>();
 		private final Set<IIcfgTransition<?>> mCallAlphabet = new HashSet<>();
 		private final Set<IIcfgTransition<?>> mReturnAlphabet = new HashSet<>();
+		private final VpAlphabet<IIcfgTransition<?>> mVpAlphabet = new VpAlphabet<IIcfgTransition<?>>(mInternalAlphabet, mCallAlphabet, mReturnAlphabet);
 
 		private final IStateFactory<AnnotatedProgramPoint> mStateFactory = new DummyStateFactory<>();
 
@@ -234,20 +236,10 @@ public Set<IIcfgTransition<?>> getAlphabet() {
 		public String sizeInformation() {
 			return "no size info available";
 		}
-
-		@Override
-		public Set<IIcfgTransition<?>> getInternalAlphabet() {
-			return mInternalAlphabet;
-		}
-
-		@Override
-		public Set<IIcfgTransition<?>> getCallAlphabet() {
-			return mCallAlphabet;
-		}
-
+
 		@Override
-		public Set<IIcfgTransition<?>> getReturnAlphabet() {
-			return mReturnAlphabet;
+		public VpAlphabet<IIcfgTransition<?>> getVpAlphabet() {
+			return mVpAlphabet;
 		}
 
 		@Override

diff --git a/...ce/LTL2aut/src/de/uni_freiburg/informatik/ultimate/ltl2aut/never2nwa/Never2Automaton.java b/...ce/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<String>());
 
 		collectStates(mNeverClaim, null);
@@ -369,7 +369,7 @@ private List<Statement> 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/.../uni_freiburg/informatik/ultimate/plugins/analysis/lassoranker/LassoAutomatonBuilder.java b/.../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<LETTER> {
 	private final NestedWordAutomaton<LETTER, IPredicate> mResult;
 	private final PredicateFactory mPredicateFactory;
 
-	public LassoAutomatonBuilder(final InCaReAlphabet<LETTER> alphabet,
+	public LassoAutomatonBuilder(final VpAlphabet<LETTER> alphabet,
 			final IStateFactory<IPredicate> predicateFactoryRc, final PredicateFactory predicateFactory,
 			final NestedWord<LETTER> stem, final NestedWord<LETTER> 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<IPredicate> stemStates = constructListOfDontCarePredicates(stem.length());
 		final List<IPredicate> loopStates = constructListOfDontCarePredicates(loop.length());
 		IPredicate initialState;

diff --git a/...de/uni_freiburg/informatik/ultimate/plugins/analysis/lassoranker/LassoExtractorBuchi.java b/...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<LETTER> nlw = run.getNestedLassoWord();
-			final InCaReAlphabet<LETTER> 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<LETTER, IPredicate> difference =
 					new BuchiDifferenceFKV<>(new AutomataLibraryServices(mServices), mPredicateFactoryRc, mCfgAutomaton,

diff --git a/.../src/de/uni_freiburg/informatik/ultimate/automata/alternating/AA_DeterminizeReversed.java b/.../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<LETTER> extends GeneralOperation<LETTER, Bit
 	public AA_DeterminizeReversed(final AutomataLibraryServices services,
 			final AlternatingAutomaton<LETTER, BitSet> alternatingAutomaton) {
 		super(services);
-		mResultAutomaton = new NestedWordAutomaton<>(services, alternatingAutomaton.getAlphabet(),
-				Collections.emptySet(), Collections.emptySet(), alternatingAutomaton.getStateFactory());
+		final VpAlphabet<LETTER> vpAlphabet = new VpAlphabet<LETTER>(alternatingAutomaton.getAlphabet(), Collections.emptySet(), Collections.emptySet());
+		mResultAutomaton = new NestedWordAutomaton<>(services, vpAlphabet, alternatingAutomaton.getStateFactory());
 		final LinkedList<BitSet> newStates = new LinkedList<>();
 		newStates.add(alternatingAutomaton.getFinalStatesBitVector());
 		final List<Pair<BitSet, Pair<LETTER, BitSet>>> transitionsToAdd = new ArrayList<>();

diff --git a/...ta/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/DoubleDeckerAutomaton.java b/...ta/src/de/uni_freiburg/informatik/ultimate/automata/nestedword/DoubleDeckerAutomaton.java
@@ -62,9 +62,8 @@ public class DoubleDeckerAutomaton<LETTER, STATE> extends NestedWordAutomaton<LE
 	 * @param stateFactory
 	 *            state factory
 	 */
-	public DoubleDeckerAutomaton(final AutomataLibraryServices services, final Set<LETTER> internalAlphabet,
-			final Set<LETTER> callAlphabet, final Set<LETTER> returnAlphabet, final IStateFactory<STATE> stateFactory) {
-		super(services, internalAlphabet, callAlphabet, returnAlphabet, stateFactory);
+	public DoubleDeckerAutomaton(final AutomataLibraryServices services, final VpAlphabet<LETTER> vpAlphabet, final IStateFactory<STATE> stateFactory) {
+		super(services, vpAlphabet, stateFactory);
 		mUp2Down = null;
 	}
 

diff --git a/...c/de/uni_freiburg/informatik/ultimate/automata/nestedword/INestedWordAutomatonSimple.java b/...c/de/uni_freiburg/informatik/ultimate/automata/nestedword/INestedWordAutomatonSimple.java
@@ -79,7 +79,7 @@ public interface INestedWordAutomatonSimple<LETTER, STATE> extends INwaOutgoingT
 	 *         with letter <tt>a</tt>.
 	 */
 	default Set<LETTER> lettersInternal(final STATE state) {
-		return getInternalAlphabet();
+		return getVpAlphabet().getInternalAlphabet();
 	}
 
 	/**
@@ -89,7 +89,7 @@ default Set<LETTER> lettersInternal(final STATE state) {
 	 *         letter <tt>a</tt>.
 	 */
 	default Set<LETTER> lettersCall(final STATE state) {
-		return getCallAlphabet();
+		return getVpAlphabet().getCallAlphabet();
 	}
 
 	/**
@@ -99,7 +99,7 @@ default Set<LETTER> lettersCall(final STATE state) {
 	 * hierarchical predecessor is hier and that is labeled with letter <tt>a</tt> 
 	 */
 	default Set<LETTER> lettersReturn(final STATE state, final STATE hier) {
-		return getReturnAlphabet();
+		return getVpAlphabet().getReturnAlphabet();
 	}
 
 	/**