From 466339059f917473c936b98b5677d30354ae9747 Mon Sep 17 00:00:00 2001 From: hannah Date: Wed, 21 Apr 2021 22:42:55 +0200 Subject: [PATCH] Call parse_prefix_ltl instead of parse_formula --- src/storm/automata/LTL2DeterministicAutomaton.cpp | 11 ++++++++--- 1 file changed, 8 insertions(+), 3 deletions(-) diff --git a/src/storm/automata/LTL2DeterministicAutomaton.cpp b/src/storm/automata/LTL2DeterministicAutomaton.cpp index ca4d0b5db..7f951135e 100644 --- a/src/storm/automata/LTL2DeterministicAutomaton.cpp +++ b/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 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)