I found several possible reasons that make the current push down system runs slowly
No detection of computed control state
No detection of computed edges in dyck state graph
No detection of computed edges in epslang closure graph
Not the three reasons above. But worth noting!
No aggressive cut off: for a to-explore control state, the algo does not detect whether the control state is weaker than any seen states before. The right way should skip exploration of the weaker states.
No widening: per-point-widening, configuration-widening















