Add specialized symbols/semantics for CTL/LTL interpretation of the X operator.
Specifically, (E)X is true in LTL in deadlocked states but not in CTL -- as defined in the MCC competition.
Instead of treating the semantics different, we should introduce two versions of the X quantifier; a deadlock sensitive one, and a deadlock insensitive.
Add specialized symbols/semantics for CTL/LTL interpretation of the X operator.
Specifically, (E)X is true in LTL in deadlocked states but not in CTL -- as defined in the MCC competition.
Instead of treating the semantics different, we should introduce two versions of the X quantifier; a deadlock sensitive one, and a deadlock insensitive.