[Feature Request] Improve CTL model checking

[axel-habermaier]

I'm trying to use pins2lts-sym for CTL model checking and encountered two significant shortcomings:

1. Apparently, only state slots can be referenced in a CTL formula. Ideally, I'd like to be able to reference state labels as well. I have a workaround for that (encoding state labels in the state vector, which increases the state vector size and consequently increases model checking times by 2 to 20%, depending on the model and the formula), but ideally I'd rather not special case CTL model checking compared to LTL model checking.

2. No counter examples are generated for invalid CTL formulas, like NuSMV does, for example; which makes model checking a lot less useful than it could be.

Ideally, I'd like to be able to us pins2lts-sym with CTL model checking in the same way that I can use pins2lts-seq (or -mc) with LTL model checking.

Note that I don't really care about CTL* or mu-calculus, if that makes things any easier.