From ca4ac3a16676edbdd94fa2bfec7cd4778a0e7f6f Mon Sep 17 00:00:00 2001 From: hannah Date: Sun, 6 Jun 2021 21:01:58 +0200 Subject: [PATCH] transform into generalized Rabin instead of DNF --- src/storm/automata/LTL2DeterministicAutomaton.cpp | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) diff --git a/src/storm/automata/LTL2DeterministicAutomaton.cpp b/src/storm/automata/LTL2DeterministicAutomaton.cpp index 06ceb5f03..2d30710bd 100644 --- a/src/storm/automata/LTL2DeterministicAutomaton.cpp +++ b/src/storm/automata/LTL2DeterministicAutomaton.cpp @@ -34,17 +34,21 @@ namespace storm { // Request a deterministic, complete automaton with state-based acceptance spot::translator trans = spot::translator(); - trans.set_type(spot::postprocessor::Generic); + trans.set_type(spot::postprocessor::Generic); //Generic trans.set_pref(spot::postprocessor::Deterministic | spot::postprocessor::SBAcc | spot::postprocessor::Complete); STORM_LOG_INFO("Construct deterministic automaton for "<< spotFormula); auto aut = trans.run(spotFormula); // TODO necessary for MDP LTL-MC if(!(aut->get_acceptance().is_dnf()) && dnf){ - STORM_LOG_INFO("Convert acceptance condition into DNF..."); - aut->set_acceptance(aut->get_acceptance().to_dnf()); + STORM_LOG_INFO("Convert acceptance condition "<< aut->get_acceptance() << " into DNF..."); + // Transform the acceptance condition in disjunctive normal form and merge all the Fin-sets of each clause + aut = to_generalized_rabin(aut,true); } + + STORM_LOG_INFO(aut->get_acceptance()); + std::stringstream autStream; // Print reachable states in HOA format, implicit edges (i), state-based acceptance (s) spot::print_hoa(autStream, aut, "is");