spotProduct.h

Go to the documentation of this file.

#pragma once
 
#include "storm/automata/DeterministicAutomaton.h"
#include "storm/logic/ExtractMaximalStateFormulasVisitor.h"
#include "storm/logic/MultiObjectiveFormula.h"
 
namespace storm::modelchecker::helper::lexicographic::spothelper {
 
std::shared_ptr<storm::automata::DeterministicAutomaton> ltl2daSpotProduct(storm::logic::MultiObjectiveFormula const& formula,
                                                                           storm::logic::ExtractMaximalStateFormulasVisitor::ApToFormulaMap& extracted,
                                                                           std::vector<uint>& acceptanceConditions);
}  // namespace storm::modelchecker::helper::lexicographic::spothelper