search

moves-rwth / storm

A Modern Probabilistic Model Checker
https://www.stormchecker.org
GNU General Public License v3.0
135 stars 74 forks source link

Better treatment of Boolean literals in LTL formulas. #262

Open tquatmann opened 2 years ago

tquatmann commented 2 years ago

When checking LTL formulas like G (true U a), the true is somehow replaced by a fresh atomic proposition before feeding it into spot. This potentially yields unnecessarily large automata.

Obviously, this should be avoided.

kleinj commented 2 years ago

Should be quite easy, just add special casing/direct return for BooleanLiteralFormula at the start of https://github.com/moves-rwth/storm/blob/f37f477bc9995b9fa566dda20dd954e293497944/src/storm/logic/ExtractMaximalStateFormulasVisitor.cpp#L180

In PRISM, we have some additional logic that looks at the actual satisfying state sets for the maximal state subformulas and convert to true/false if the set covers all states of the model or is empty, respectively. In Storm, this info is not as easily available at that point of conversion...