Call parse_prefix_ltl instead of parse_formula

src/storm/automata/LTL2DeterministicAutomaton.cpp

@@ -3,6 +3,7 @@
 
 #include "storm/logic/Formula.h"
 #include "storm/utility/macros.h"
+#include "storm/exceptions/ExpressionEvaluationException.h"
 
 #ifdef STORM_HAVE_SPOT
 #include "spot/tl/formula.hh"
@@ -16,15 +17,19 @@ namespace storm {
 
         std::shared_ptr<DeterministicAutomaton> LTL2DeterministicAutomaton::ltl2da(storm::logic::Formula const& f) {
 #ifdef STORM_HAVE_SPOT
-            spot::formula parsed_formula = spot::parse_formula(f.toPrefixString());
 
-            STORM_LOG_INFO("Construct deterministic automaton for "<< parsed_formula);
+            std::string prefixLtl = f.toPrefixString();
+            spot::parsed_formula spotPrefixLtl = spot::parse_prefix_ltl(prefixLtl);
+            STORM_LOG_THROW(!spotPrefixLtl.format_errors(std::cerr), storm::exceptions::ExpressionEvaluationException, "Spot could not parse formula: " << prefixLtl);
+            spot::formula spotFormula = spotPrefixLtl.f;
+
 
             // Request a deterministic, complete automaton with state-based acceptance
             spot::translator trans = spot::translator();
             trans.set_type(spot::postprocessor::Generic);
             trans.set_pref(spot::postprocessor::Deterministic | spot::postprocessor::SBAcc | spot::postprocessor::Complete);
-            auto aut = trans.run(parsed_formula);
+            STORM_LOG_INFO("Construct deterministic automaton for "<< spotFormula);
+            auto aut = trans.run(spotFormula);
 
             std::stringstream autStream;
             // Print reachable states in HOA format, implicit edges (i), state-based acceptance (s)