// Author: heizmann@informatik.uni-freiburg.de
// Date: November 2013

assert(!buchiIsEmpty(nwa));
assert(numberOfStates(removeNonLiveStates(nwa)) == 5);

NestedWordAutomaton nwa = (
    callAlphabet = {"a0" "a1" },
    internalAlphabet = {"a0" "a1" },
    returnAlphabet = {"a0" "a1" },
    states = {"q2" "q1" "q4" "q3" "q0" },
    initialStates = {"q0" },
    finalStates = {"q2" "q3" "q0" },
    callTransitions = {
         ("q2" "a1" "q4")
         ("q4" "a0" "q4")
         ("q4" "a0" "q3")
         ("q4" "a1" "q4")
         ("q3" "a0" "q4")
         ("q3" "a1" "q1")
    },
    internalTransitions = {
         ("q2" "a0" "q4")
         ("q1" "a0" "q2")
         ("q1" "a1" "q1")
         ("q4" "a1" "q2")
         ("q3" "a0" "q2")
         ("q0" "a0" "q3")
         ("q0" "a1" "q2")
         ("q0" "a1" "q1")
    },
    returnTransitions = {
         ("q2" "q1" "a1" "q3")
         ("q2" "q3" "a1" "q1")
         ("q1" "q1" "a0" "q4")
         ("q1" "q4" "a0" "q4")
         ("q1" "q4" "a0" "q3")
         ("q1" "q0" "a0" "q0")
         ("q4" "q2" "a1" "q3")
         ("q4" "q1" "a1" "q1")
         ("q4" "q3" "a1" "q4")
         ("q3" "q2" "a0" "q1")
         ("q3" "q1" "a0" "q0")
         ("q3" "q3" "a0" "q4")
         ("q3" "q0" "a0" "q3")
         ("q3" "q2" "a1" "q2")
         ("q3" "q2" "a1" "q1")
         ("q3" "q2" "a1" "q0")
         ("q3" "q0" "a1" "q4")
         ("q0" "q3" "a0" "q1")
         ("q0" "q0" "a0" "q1")
         ("q0" "q4" "a1" "q4")
    }
);