Previously, the formula parser only supported AND, OR and NOT over state formulas.
For LTL, we need those over path formulas.
We tweak the grammar, the AST types and visitors, to also handle
UnaryBooleanPathFormula and BinaryBooleanPathformula. During parsing,
we determine on-demand whether to generate the path or state formula
variant by looking at the subformulas - if they are state formulas,
the boolean operator will be a state formula as well.
Conflicts:
src/storm-parsers/parser/FormulaParserGrammar.cpp
src/storm-parsers/parser/FormulaParserGrammar.h
src/storm/logic/CloneVisitor.cpp
src/storm/logic/Formula.cpp
src/storm/logic/Formula.h
src/storm/logic/FragmentChecker.cpp
src/storm/logic/FragmentSpecification.cpp
src/storm/logic/FragmentSpecification.h
src/storm/logic/LiftableTransitionRewardsVisitor.cpp
src/storm/storage/jani/JSONExporter.cpp
Note: syntax of the HOA path formula will change!
We have added checks for boundedGloballyFormulae hence the conflicts
Conflicts:
src/storm/logic/CloneVisitor.cpp
src/storm/logic/Formula.cpp
src/storm/logic/Formula.h
src/storm/logic/FragmentSpecification.cpp
src/storm/logic/FragmentSpecification.h
src/storm/logic/LiftableTransitionRewardsVisitor.cpp
src/storm/storage/jani/JSONExporter.cpp
ConstantsComparator: The old code used `abs(x-y)/abs(x+y)<= epsilon` when comparing two numbers for equality (modulo relative precision). This is weird when x and y have different signs and potentially even causes a div by 0 whenever x=-y. Moreover the templating was awkward, causing a lot of code duplications and a Warning with clang.
Distribution[WithReward]: replaced forward declarations of ConstantsComparator by actual includes as the forward declarations caused some ambiguity regarding the template parameters.
hannah
Tim Quatmann
Stefan Pranger
Joachim Klein
Sebastian Junges
Johannes Lehmann