sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

Cleaned up some includes for the model checkers. 

Conflicts:
	src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.h
	src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp
tempestpy_adaptions
Tim Quatmann 3 years ago
committed by Stefan Pranger
parent
e92e32239b
commit
dffc04a280
7 changed files with 14 additions and 48 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 9
      src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp
  2. 14
      src/storm/modelchecker/helper/ltl/SparseLTLHelper.cpp
  3. 10
      src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp
  4. 3
      src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.h
  5. 21
      src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp
  6. 3
      src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.h
  7. 2
      src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp

9
src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp
View File

@ -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<typename SparseMarkovAutomatonModelType>

14
src/storm/modelchecker/helper/ltl/SparseLTLHelper.cpp
View File

@ -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 {

10
src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp
View File

@ -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 {

3
src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.h
View File

@ -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 {

21
src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp
View File

@ -1,7 +1,5 @@
#include "storm/modelchecker/prctl/SparseMdpPrctlModelChecker.h"
#include <sstream>
#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<typename SparseMdpModelType>
std::unique_ptr<CheckResult> SparseMdpPrctlModelChecker<SparseMdpModelType>::computeHOAPathProbabilities(Environment const& env, CheckTask<storm::logic::HOAPathFormula, ValueType> const& checkTask) {
storm::logic::HOAPathFormula const& pathFormula = checkTask.getFormula();
storm::modelchecker::helper::SparseLTLHelper<ValueType, false> 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<ValueType> numericResult = helper.computeDAProductProbabilities(env, *pathFormula.readAutomaton(), apSets);
std::unique_ptr<CheckResult> result(new ExplicitQuantitativeCheckResult<ValueType>(std::move(numericResult)));
if (checkTask.isProduceSchedulersSet()) {
result->asExplicitQuantitativeCheckResult<ValueType>().setScheduler(std::make_unique<storm::storage::Scheduler<ValueType>>(helper.extractScheduler(this->getModel())));
@ -183,7 +174,7 @@ namespace storm {
return result;
}
template<typename SparseMdpModelType>
std::unique_ptr<CheckResult> SparseMdpPrctlModelChecker<SparseMdpModelType>::computeLTLProbabilities(Environment const& env, CheckTask<storm::logic::PathFormula, ValueType> const& checkTask) {
storm::logic::PathFormula const& pathFormula = checkTask.getFormula();
@ -192,7 +183,7 @@ namespace storm {
storm::modelchecker::helper::SparseLTLHelper<ValueType, true> 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<ValueType> numericResult = helper.computeLTLProbabilities(env, pathFormula, formulaChecker);
@ -203,7 +194,7 @@ namespace storm {
return result;
}
template<typename SparseMdpModelType>
std::unique_ptr<CheckResult> SparseMdpPrctlModelChecker<SparseMdpModelType>::computeConditionalProbabilities(Environment const& env, CheckTask<storm::logic::ConditionalFormula, ValueType> const& checkTask) {
storm::logic::ConditionalFormula const& conditionalFormula = checkTask.getFormula();

3
src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.h
View File

@ -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<CheckResult> checkMultiObjectiveFormula(Environment const& env, CheckTask<storm::logic::MultiObjectiveFormula, ValueType> const& checkTask) override;
virtual std::unique_ptr<CheckResult> checkQuantileFormula(Environment const& env, CheckTask<storm::logic::QuantileFormula, ValueType> const& checkTask) override;
private:
//std::vector<ValueType> computeDAProductProbabilities(Environment const& env, storm::solver::SolveGoal<ValueType>&& goal, storm::automata::DeterministicAutomaton const& da, std::map<std::string, storm::storage::BitVector>& apSatSets, bool qualitative) const;
};
} // namespace modelchecker
} // namespace storm

2
src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp
View File

@ -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"

Write Preview
Loading…
Cancel
Save