EpsilonNPDA and NPDA in automaton run
The run of NPDA uses rudimental checking of visited configurations. This obviously fails in case there is an epsilon loop (or cycle) that increases the pushdown store height. No such issue would be with NPDA that would not allow epsilon transitions at all.
The proposed change is to rename NPDA to EpsilonNPDA and introduce NPDA type that does not allow epsilon transitions.