- DONE Implement Weak until?
- DONE (test it!) Allow underscores in CTL DONE; everywhere -Victor
- Check whether states and variables can share names
- HACKED Implement state specification in CTL; preferably with macros (ie, names for states set at runtime at prompt)
- Check a property for Marsha (when everything works):
    W -- weak until
- FIXED CDTW: Witness for EX -- fix (problem KEGTest)
    eg. thirdmergedphone.xml 
        EX (!connected)
	(Problem was that we oculd only go down one path; now we have depth first traversal, at the option of the user. Would breadth-first be more intuitive?)

