Pdmc2

This push request is implementing some refactorings in the pushdown model checking algorithm (separated Post automaton generation from head reachability graph), as well as adding more functionality towards generating witnesses,  Currently it can compute a path to any reachable head. 

@dwightguth: please take a look at it.
@dlucanu: I will need your "conceptual" approval for merging this code.