Week 04 · Sipser 2.2 · Part II
A PDA is a finite automaton that got one thing: a stack it can push to and pop from, and cannot read without popping. It is nondeterministic by definition — the branch is not a convenience, it is the answer. Every computation path is searched below.
One transition per line:
q1, a, eps -> q1, X means read a, pop nothing, push X.
Use eps anywhere you mean ε.
Read the stack without popping. There is no peek. If your design "checks the top and leaves it", it is not a PDA — pop it and push it back.
Test the stack for emptiness. That is why almost every machine here starts by pushing a marker $: seeing $ on top is the only way to know the real stack is empty.
A PDA has no single "current configuration" — after the first ε-move there are usually several. This page therefore does a breadth-first search over the whole configuration space (state, position in the input, stack) and reports the shortest accepting computation it finds. The step controls walk that one path; the other branches died.
Load i=j or j=k and run aabbcc, then aabbbb. The same machine accepts both, by committing to a different branch at the very first move. That commitment is what nondeterminism buys, and it is why no deterministic PDA for that language exists.
The search is bounded (30 000 configurations, stack depth 120). If it hits the bound the verdict says so rather than claiming a definite "no".