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

NestedWordAutomaton result = removeNonLiveStates(nwa);
print(numberOfStates(result));
//assert(numberOfStates(result) == 4);

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