Tool for translating PDAs to CFGs We know that all push down automata are representable using context-free grammars. Furthermore, there is an algorithm to construct a CFG from any PDA (e.g. Sipser's proof in intro to theory of computation). 

Are there any tools which do this translation? I.e. I can put in a set of transition functions and it will return an equivalent CFG.
jflap is pretty nice and can do this. See here: http://www.cs.duke.edu/csed/jflap/.