diff --git a/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp b/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp index 358945d14..1874a1384 100644 --- a/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp +++ b/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp @@ -13,25 +13,16 @@ #include "storm/utility/FilteredRewardModel.h" #include "storm/utility/macros.h" -#include "storm/settings/SettingsManager.h" -#include "storm/settings/modules/GeneralSettings.h" -#include "storm/settings/modules/DebugSettings.h" - #include "storm/solver/SolveGoal.h" -#include "storm/transformer/ContinuousToDiscreteTimeModelTransformer.h" - #include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h" #include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h" #include "storm/logic/FragmentSpecification.h" -#include "storm/logic/ExtractMaximalStateFormulasVisitor.h" #include "storm/exceptions/InvalidPropertyException.h" #include "storm/exceptions/NotImplementedException.h" -#include "storm/api/storm.h" - namespace storm { namespace modelchecker { template diff --git a/src/storm/modelchecker/helper/ltl/SparseLTLHelper.cpp b/src/storm/modelchecker/helper/ltl/SparseLTLHelper.cpp index 46627e714..151e3892e 100644 --- a/src/storm/modelchecker/helper/ltl/SparseLTLHelper.cpp +++ b/src/storm/modelchecker/helper/ltl/SparseLTLHelper.cpp @@ -3,24 +3,22 @@ #include "storm/automata/LTL2DeterministicAutomaton.h" #include "storm/automata/DeterministicAutomaton.h" -#include "storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h" -#include "storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.h" +#include "storm/environment/modelchecker/ModelCheckerEnvironment.h" #include "storm/logic/ExtractMaximalStateFormulasVisitor.h" -#include "storm/solver/SolveGoal.h" + +#include "storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h" +#include "storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.h" #include "storm/storage/StronglyConnectedComponentDecomposition.h" #include "storm/storage/MaximalEndComponentDecomposition.h" #include "storm/storage/memorystructure/MemoryStructure.h" #include "storm/storage/memorystructure/MemoryStructureBuilder.h" +#include "storm/solver/SolveGoal.h" +#include "storm/utility/graph.h" -#include "storm/settings/SettingsManager.h" -#include "storm/settings/modules/DebugSettings.h" #include "storm/exceptions/InvalidPropertyException.h" -#include "storm/environment/modelchecker/ModelCheckerEnvironment.h" - -#include "storm/utility/graph.h" namespace storm { namespace modelchecker { diff --git a/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp b/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp index 4fb9802de..838caf03d 100644 --- a/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp +++ b/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp @@ -19,18 +19,12 @@ #include "storm/modelchecker/helper/utility/SetInformationFromCheckTask.h" #include "storm/logic/FragmentSpecification.h" -#include "storm/logic/ExtractMaximalStateFormulasVisitor.h" -#include "storm/automata/AcceptanceCondition.h" + #include "storm/solver/SolveGoal.h" +#include "storm/models/sparse/Dtmc.h" #include "storm/models/sparse/StandardRewardModel.h" -#include "storm/settings/SettingsManager.h" -#include "storm/settings/modules/GeneralSettings.h" -#include "storm/settings/modules/DebugSettings.h" - -#include "storm/exceptions/InvalidStateException.h" - #include "storm/exceptions/InvalidPropertyException.h" namespace storm { diff --git a/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.h b/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.h index e5ff0d5f4..7ab10210f 100644 --- a/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.h +++ b/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.h @@ -3,9 +3,6 @@ #include "storm/modelchecker/propositional/SparsePropositionalModelChecker.h" #include "storm/models/sparse/Dtmc.h" -#include "storm/utility/solver.h" -#include "storm/solver/LinearEquationSolver.h" -#include "storm/storage/StronglyConnectedComponent.h" namespace storm { namespace modelchecker { diff --git a/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp b/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp index 874bb1c84..7ce739537 100644 --- a/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp +++ b/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp @@ -1,7 +1,5 @@ #include "storm/modelchecker/prctl/SparseMdpPrctlModelChecker.h" -#include - #include "storm/utility/constants.h" #include "storm/utility/macros.h" #include "storm/utility/vector.h" @@ -30,17 +28,10 @@ #include "storm/shields/ShieldHandling.h" -#include "storm/settings/SettingsManager.h" - -#include "storm/settings/modules/GeneralSettings.h" -#include "storm/settings/modules/DebugSettings.h" - #include "storm/exceptions/InvalidStateException.h" #include "storm/exceptions/InvalidPropertyException.h" #include "storm/storage/expressions/Expressions.h" -#include "storm/storage/MaximalEndComponentDecomposition.h" - #include "storm/exceptions/InvalidPropertyException.h" namespace storm { @@ -168,14 +159,14 @@ namespace storm { template std::unique_ptr SparseMdpPrctlModelChecker::computeHOAPathProbabilities(Environment const& env, CheckTask const& checkTask) { storm::logic::HOAPathFormula const& pathFormula = checkTask.getFormula(); - + storm::modelchecker::helper::SparseLTLHelper helper(this->getModel().getTransitionMatrix()); storm::modelchecker::helper::setInformationFromCheckTaskDeterministic(helper, checkTask, this->getModel()); - + auto formulaChecker = [&] (storm::logic::Formula const& formula) { return this->check(env, formula)->asExplicitQualitativeCheckResult().getTruthValuesVector(); }; auto apSets = helper.computeApSets(pathFormula.getAPMapping(), formulaChecker); std::vector numericResult = helper.computeDAProductProbabilities(env, *pathFormula.readAutomaton(), apSets); - + std::unique_ptr result(new ExplicitQuantitativeCheckResult(std::move(numericResult))); if (checkTask.isProduceSchedulersSet()) { result->asExplicitQuantitativeCheckResult().setScheduler(std::make_unique>(helper.extractScheduler(this->getModel()))); @@ -183,7 +174,7 @@ namespace storm { return result; } - + template std::unique_ptr SparseMdpPrctlModelChecker::computeLTLProbabilities(Environment const& env, CheckTask const& checkTask) { storm::logic::PathFormula const& pathFormula = checkTask.getFormula(); @@ -192,7 +183,7 @@ namespace storm { storm::modelchecker::helper::SparseLTLHelper helper(this->getModel().getTransitionMatrix()); storm::modelchecker::helper::setInformationFromCheckTaskNondeterministic(helper, checkTask, this->getModel()); - + auto formulaChecker = [&] (storm::logic::Formula const& formula) { return this->check(env, formula)->asExplicitQualitativeCheckResult().getTruthValuesVector(); }; std::vector numericResult = helper.computeLTLProbabilities(env, pathFormula, formulaChecker); @@ -203,7 +194,7 @@ namespace storm { return result; } - + template std::unique_ptr SparseMdpPrctlModelChecker::computeConditionalProbabilities(Environment const& env, CheckTask const& checkTask) { storm::logic::ConditionalFormula const& conditionalFormula = checkTask.getFormula(); diff --git a/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.h b/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.h index 74358d334..3feb0802d 100644 --- a/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.h +++ b/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.h @@ -4,7 +4,6 @@ #include "storm/modelchecker/propositional/SparsePropositionalModelChecker.h" #include "storm/models/sparse/Mdp.h" #include "storm/solver/MinMaxLinearEquationSolver.h" -#include "storm/solver/SolveGoal.h" namespace storm { @@ -45,8 +44,6 @@ namespace storm { virtual std::unique_ptr checkMultiObjectiveFormula(Environment const& env, CheckTask const& checkTask) override; virtual std::unique_ptr checkQuantileFormula(Environment const& env, CheckTask const& checkTask) override; - private: - //std::vector computeDAProductProbabilities(Environment const& env, storm::solver::SolveGoal&& goal, storm::automata::DeterministicAutomaton const& da, std::map& apSatSets, bool qualitative) const; }; } // namespace modelchecker } // namespace storm diff --git a/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp index 30619d8f0..4ebfb4821 100644 --- a/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp @@ -6,8 +6,6 @@ #include "storm/utility/vector.h" #include "storm/utility/graph.h" -#include "storm/models/sparse/Dtmc.h" - #include "storm/storage/StronglyConnectedComponentDecomposition.h" #include "storm/storage/DynamicPriorityQueue.h" #include "storm/storage/ConsecutiveUint64DynamicPriorityQueue.h"