diff --git a/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.h b/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.h index 88727c504..8e4dd26eb 100644 --- a/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.h +++ b/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.h @@ -34,7 +34,7 @@ namespace storm { struct PreprocessorData { SparseModelType const& originalModel; - std::vector>> objectives; + std::vector>> objectives; std::vector>> tasks; std::shared_ptr memory; diff --git a/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessorReturnType.h b/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessorReturnType.h index f9f71231f..96de2956c 100644 --- a/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessorReturnType.h +++ b/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessorReturnType.h @@ -5,7 +5,7 @@ #include #include "storm/logic/Formulas.h" -#include "storm/modelchecker/multiobjective/constraintbased/CbObjective.h" +#include "storm/modelchecker/multiobjective/Objective.h" #include "storm/exceptions/UnexpectedException.h" @@ -14,7 +14,7 @@ namespace storm { namespace multiobjective { template - struct SparseCbPreprocessorReturnType { + struct SparseMultiObjectivePreprocessorReturnType { enum class QueryType { Achievability }; @@ -24,14 +24,14 @@ namespace storm { QueryType queryType; // The (preprocessed) objectives - std::vector> objectives; + std::vector> objectives; // The states for which there is a scheduler such that all objectives have value zero storm::storage::BitVector possibleBottomStates; // Overapproximation of the set of choices that are part of an end component. storm::storage::BitVector possibleECChoices; - SparseCbPreprocessorReturnType(storm::logic::MultiObjectiveFormula const& originalFormula, SparseModelType const& originalModel) : originalFormula(originalFormula), originalModel(originalModel) { + SparseMultiObjectivePreprocessorReturnType(storm::logic::MultiObjectiveFormula const& originalFormula, SparseModelType const& originalModel) : originalFormula(originalFormula), originalModel(originalModel) { // Intentionally left empty } @@ -56,12 +56,12 @@ namespace storm { originalModel.printModelInformationToStream(out); out << std::endl; out << "Preprocessed Model Information:" << std::endl; - preprocessedModel.printModelInformationToStream(out); + preprocessedModel->printModelInformationToStream(out); out << std::endl; out << "---------------------------------------------------------------------------------------------------------------------------------------" << std::endl; } - friend std::ostream& operator<<(std::ostream& out, SparseCbPreprocessorReturnType const& ret) { + friend std::ostream& operator<<(std::ostream& out, SparseMultiObjectivePreprocessorReturnType const& ret) { ret.printToStream(out); return out; } diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaPreprocessor.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaPreprocessor.cpp index 506bb1ee8..abc37571c 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaPreprocessor.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaPreprocessor.cpp @@ -82,6 +82,7 @@ namespace storm { auto backwardTransitions = result.preprocessedModel.getBackwardTransitions(); analyzeEndComponents(result, backwardTransitions); ensureRewardFiniteness(result, backwardTransitions); + break; } } return result;