dehnert
9 years ago
107 changed files with 2837 additions and 583 deletions
-
0SparseLearningModelChecker.cpp
-
2src/CMakeLists.txt
-
132src/builder/ExplicitPrismModelBuilder.cpp
-
53src/builder/ExplicitPrismModelBuilder.h
-
35src/cli/entrypoints.h
-
15src/generator/CompressedState.cpp
-
15src/generator/CompressedState.h
-
7src/generator/NextStateGenerator.h
-
26src/generator/PrismNextStateGenerator.cpp
-
9src/generator/PrismNextStateGenerator.h
-
5src/generator/StateBehavior.cpp
-
5src/generator/StateBehavior.h
-
4src/logic/AtomicExpressionFormula.cpp
-
2src/logic/AtomicExpressionFormula.h
-
5src/logic/AtomicLabelFormula.cpp
-
4src/logic/AtomicLabelFormula.h
-
6src/logic/BinaryBooleanStateFormula.cpp
-
2src/logic/BinaryBooleanStateFormula.h
-
4src/logic/BooleanLiteralFormula.cpp
-
2src/logic/BooleanLiteralFormula.h
-
4src/logic/BoundedUntilFormula.cpp
-
2src/logic/BoundedUntilFormula.h
-
106src/logic/CloneVisitor.cpp
-
37src/logic/CloneVisitor.h
-
10src/logic/ConditionalFormula.cpp
-
7src/logic/ConditionalFormula.h
-
4src/logic/CumulativeRewardFormula.cpp
-
2src/logic/CumulativeRewardFormula.h
-
10src/logic/EventuallyFormula.cpp
-
4src/logic/EventuallyFormula.h
-
22src/logic/Formula.cpp
-
14src/logic/Formula.h
-
9src/logic/FragmentChecker.cpp
-
30src/logic/FragmentSpecification.cpp
-
10src/logic/FragmentSpecification.h
-
4src/logic/GloballyFormula.cpp
-
2src/logic/GloballyFormula.h
-
6src/logic/InstantaneousRewardFormula.cpp
-
4src/logic/InstantaneousRewardFormula.h
-
26src/logic/LabelSubstitutionVisitor.cpp
-
29src/logic/LabelSubstitutionVisitor.h
-
6src/logic/LongRunAverageOperatorFormula.cpp
-
2src/logic/LongRunAverageOperatorFormula.h
-
4src/logic/LongRunAverageRewardFormula.cpp
-
2src/logic/LongRunAverageRewardFormula.h
-
6src/logic/NextFormula.cpp
-
4src/logic/NextFormula.h
-
4src/logic/OperatorFormula.cpp
-
4src/logic/OperatorFormula.h
-
6src/logic/ProbabilityOperatorFormula.cpp
-
4src/logic/ProbabilityOperatorFormula.h
-
4src/logic/RewardOperatorFormula.cpp
-
4src/logic/RewardOperatorFormula.h
-
6src/logic/TimeOperatorFormula.cpp
-
4src/logic/TimeOperatorFormula.h
-
111src/logic/ToExpressionVisitor.cpp
-
39src/logic/ToExpressionVisitor.h
-
6src/logic/UnaryBooleanStateFormula.cpp
-
2src/logic/UnaryBooleanStateFormula.h
-
4src/logic/UntilFormula.cpp
-
4src/logic/UntilFormula.h
-
21src/logic/VariableSubstitutionVisitor.cpp
-
29src/logic/VariableSubstitutionVisitor.h
-
2src/modelchecker/AbstractModelChecker.cpp
-
2src/modelchecker/CheckTask.h
-
149src/modelchecker/exploration/Bounds.cpp
-
74src/modelchecker/exploration/Bounds.h
-
227src/modelchecker/exploration/ExplorationInformation.cpp
-
128src/modelchecker/exploration/ExplorationInformation.h
-
687src/modelchecker/exploration/SparseExplorationModelChecker.cpp
-
89src/modelchecker/exploration/SparseExplorationModelChecker.h
-
69src/modelchecker/exploration/StateGeneration.cpp
-
56src/modelchecker/exploration/StateGeneration.h
-
46src/modelchecker/exploration/Statistics.cpp
-
44src/modelchecker/exploration/Statistics.h
-
13src/models/sparse/StateAnnotation.h
-
2src/parser/DeterministicModelParser.cpp
-
2src/parser/NondeterministicModelParser.cpp
-
6src/settings/SettingsManager.cpp
-
7src/settings/SettingsManager.h
-
96src/settings/modules/ExplorationSettings.cpp
-
102src/settings/modules/ExplorationSettings.h
-
6src/settings/modules/GeneralSettings.cpp
-
2src/settings/modules/GeneralSettings.h
-
7src/storage/MaximalEndComponentDecomposition.cpp
-
35src/storage/SparseMatrix.cpp
-
2src/storage/SparseMatrix.h
-
2src/storage/expressions/ToExprtkStringVisitor.cpp
-
8src/storage/prism/Program.cpp
-
7src/storage/prism/Program.h
-
20src/storage/sparse/StateStorage.cpp
-
35src/storage/sparse/StateStorage.h
-
17src/storage/sparse/StateValuations.cpp
-
33src/storage/sparse/StateValuations.h
-
66src/utility/prism.cpp
-
190src/utility/prism.h
-
3src/utility/storm.h
-
2src/utility/vector.h
-
8test/functional/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp
-
16test/functional/modelchecker/NativeDtmcPrctlModelCheckerTest.cpp
@ -0,0 +1,106 @@ |
|||
#include "src/logic/CloneVisitor.h"
|
|||
|
|||
#include "src/logic/Formulas.h"
|
|||
|
|||
namespace storm { |
|||
namespace logic { |
|||
|
|||
std::shared_ptr<Formula> CloneVisitor::clone(Formula const& f) const { |
|||
boost::any result = f.accept(*this, boost::any()); |
|||
return boost::any_cast<std::shared_ptr<Formula>>(result); |
|||
} |
|||
|
|||
boost::any CloneVisitor::visit(AtomicExpressionFormula const& f, boost::any const& data) const { |
|||
return std::static_pointer_cast<Formula>(std::make_shared<AtomicExpressionFormula>(f)); |
|||
} |
|||
|
|||
boost::any CloneVisitor::visit(AtomicLabelFormula const& f, boost::any const& data) const { |
|||
return std::static_pointer_cast<Formula>(std::make_shared<AtomicLabelFormula>(f)); |
|||
} |
|||
|
|||
boost::any CloneVisitor::visit(BinaryBooleanStateFormula const& f, boost::any const& data) const { |
|||
std::shared_ptr<Formula> left = boost::any_cast<std::shared_ptr<Formula>>(f.getLeftSubformula().accept(*this, data)); |
|||
std::shared_ptr<Formula> right = boost::any_cast<std::shared_ptr<Formula>>(f.getRightSubformula().accept(*this, data)); |
|||
return std::static_pointer_cast<Formula>(std::make_shared<BinaryBooleanStateFormula>(f.getOperator(), left, right)); |
|||
} |
|||
|
|||
boost::any CloneVisitor::visit(BooleanLiteralFormula const& f, boost::any const& data) const { |
|||
return std::static_pointer_cast<Formula>(std::make_shared<BooleanLiteralFormula>(f)); |
|||
} |
|||
|
|||
boost::any CloneVisitor::visit(BoundedUntilFormula const& f, boost::any const& data) const { |
|||
std::shared_ptr<Formula> left = boost::any_cast<std::shared_ptr<Formula>>(f.getLeftSubformula().accept(*this, data)); |
|||
std::shared_ptr<Formula> right = boost::any_cast<std::shared_ptr<Formula>>(f.getRightSubformula().accept(*this, data)); |
|||
if (f.hasDiscreteTimeBound()) { |
|||
return std::static_pointer_cast<Formula>(std::make_shared<BoundedUntilFormula>(left, right, f.getDiscreteTimeBound())); |
|||
} else { |
|||
return std::static_pointer_cast<Formula>(std::make_shared<BoundedUntilFormula>(left, right, f.getIntervalBounds())); |
|||
} |
|||
} |
|||
|
|||
boost::any CloneVisitor::visit(ConditionalFormula const& f, boost::any const& data) const { |
|||
std::shared_ptr<Formula> subformula = boost::any_cast<std::shared_ptr<Formula>>(f.getSubformula().accept(*this, data)); |
|||
std::shared_ptr<Formula> conditionFormula = boost::any_cast<std::shared_ptr<Formula>>(f.getConditionFormula().accept(*this, data)); |
|||
return std::static_pointer_cast<Formula>(std::make_shared<ConditionalFormula>(subformula, conditionFormula, f.getContext())); |
|||
} |
|||
|
|||
boost::any CloneVisitor::visit(CumulativeRewardFormula const& f, boost::any const& data) const { |
|||
return std::static_pointer_cast<Formula>(std::make_shared<CumulativeRewardFormula>(f)); |
|||
} |
|||
|
|||
boost::any CloneVisitor::visit(EventuallyFormula const& f, boost::any const& data) const { |
|||
std::shared_ptr<Formula> subformula = boost::any_cast<std::shared_ptr<Formula>>(f.getSubformula().accept(*this, data)); |
|||
return std::static_pointer_cast<Formula>(std::make_shared<EventuallyFormula>(subformula, f.getContext())); |
|||
} |
|||
|
|||
boost::any CloneVisitor::visit(TimeOperatorFormula const& f, boost::any const& data) const { |
|||
std::shared_ptr<Formula> subformula = boost::any_cast<std::shared_ptr<Formula>>(f.getSubformula().accept(*this, data)); |
|||
return std::static_pointer_cast<Formula>(std::make_shared<TimeOperatorFormula>(subformula, f.getOperatorInformation())); |
|||
} |
|||
|
|||
boost::any CloneVisitor::visit(GloballyFormula const& f, boost::any const& data) const { |
|||
std::shared_ptr<Formula> subformula = boost::any_cast<std::shared_ptr<Formula>>(f.getSubformula().accept(*this, data)); |
|||
return std::static_pointer_cast<Formula>(std::make_shared<GloballyFormula>(subformula)); |
|||
} |
|||
|
|||
boost::any CloneVisitor::visit(InstantaneousRewardFormula const& f, boost::any const& data) const { |
|||
return std::static_pointer_cast<Formula>(std::make_shared<InstantaneousRewardFormula>(f)); |
|||
} |
|||
|
|||
boost::any CloneVisitor::visit(LongRunAverageOperatorFormula const& f, boost::any const& data) const { |
|||
std::shared_ptr<Formula> subformula = boost::any_cast<std::shared_ptr<Formula>>(f.getSubformula().accept(*this, data)); |
|||
return std::static_pointer_cast<Formula>(std::make_shared<LongRunAverageOperatorFormula>(subformula, f.getOperatorInformation())); |
|||
} |
|||
|
|||
boost::any CloneVisitor::visit(LongRunAverageRewardFormula const& f, boost::any const& data) const { |
|||
return std::static_pointer_cast<Formula>(std::make_shared<LongRunAverageRewardFormula>(f)); |
|||
} |
|||
|
|||
boost::any CloneVisitor::visit(NextFormula const& f, boost::any const& data) const { |
|||
std::shared_ptr<Formula> subformula = boost::any_cast<std::shared_ptr<Formula>>(f.getSubformula().accept(*this, data)); |
|||
return std::static_pointer_cast<Formula>(std::make_shared<NextFormula>(subformula)); |
|||
} |
|||
|
|||
boost::any CloneVisitor::visit(ProbabilityOperatorFormula const& f, boost::any const& data) const { |
|||
std::shared_ptr<Formula> subformula = boost::any_cast<std::shared_ptr<Formula>>(f.getSubformula().accept(*this, data)); |
|||
return std::static_pointer_cast<Formula>(std::make_shared<ProbabilityOperatorFormula>(subformula, f.getOperatorInformation())); |
|||
} |
|||
|
|||
boost::any CloneVisitor::visit(RewardOperatorFormula const& f, boost::any const& data) const { |
|||
std::shared_ptr<Formula> subformula = boost::any_cast<std::shared_ptr<Formula>>(f.getSubformula().accept(*this, data)); |
|||
return std::static_pointer_cast<Formula>(std::make_shared<RewardOperatorFormula>(subformula, f.getOptionalRewardModelName(), f.getOperatorInformation())); |
|||
} |
|||
|
|||
boost::any CloneVisitor::visit(UnaryBooleanStateFormula const& f, boost::any const& data) const { |
|||
std::shared_ptr<Formula> subformula = boost::any_cast<std::shared_ptr<Formula>>(f.getSubformula().accept(*this, data)); |
|||
return std::static_pointer_cast<Formula>(std::make_shared<UnaryBooleanStateFormula>(f.getOperator(), subformula)); |
|||
} |
|||
|
|||
boost::any CloneVisitor::visit(UntilFormula const& f, boost::any const& data) const { |
|||
std::shared_ptr<Formula> left = boost::any_cast<std::shared_ptr<Formula>>(f.getLeftSubformula().accept(*this, data)); |
|||
std::shared_ptr<Formula> right = boost::any_cast<std::shared_ptr<Formula>>(f.getRightSubformula().accept(*this, data)); |
|||
return std::static_pointer_cast<Formula>(std::make_shared<UntilFormula>(left, right)); |
|||
} |
|||
|
|||
} |
|||
} |
|||
@ -0,0 +1,37 @@ |
|||
#ifndef STORM_LOGIC_CLONEVISITOR_H_ |
|||
#define STORM_LOGIC_CLONEVISITOR_H_ |
|||
|
|||
#include "src/logic/FormulaVisitor.h" |
|||
|
|||
namespace storm { |
|||
namespace logic { |
|||
|
|||
class CloneVisitor : public FormulaVisitor { |
|||
public: |
|||
std::shared_ptr<Formula> clone(Formula const& f) const; |
|||
|
|||
virtual boost::any visit(AtomicExpressionFormula const& f, boost::any const& data) const override; |
|||
virtual boost::any visit(AtomicLabelFormula const& f, boost::any const& data) const override; |
|||
virtual boost::any visit(BinaryBooleanStateFormula const& f, boost::any const& data) const override; |
|||
virtual boost::any visit(BooleanLiteralFormula const& f, boost::any const& data) const override; |
|||
virtual boost::any visit(BoundedUntilFormula const& f, boost::any const& data) const override; |
|||
virtual boost::any visit(ConditionalFormula const& f, boost::any const& data) const override; |
|||
virtual boost::any visit(CumulativeRewardFormula const& f, boost::any const& data) const override; |
|||
virtual boost::any visit(EventuallyFormula const& f, boost::any const& data) const override; |
|||
virtual boost::any visit(TimeOperatorFormula const& f, boost::any const& data) const override; |
|||
virtual boost::any visit(GloballyFormula const& f, boost::any const& data) const override; |
|||
virtual boost::any visit(InstantaneousRewardFormula const& f, boost::any const& data) const override; |
|||
virtual boost::any visit(LongRunAverageOperatorFormula const& f, boost::any const& data) const override; |
|||
virtual boost::any visit(LongRunAverageRewardFormula const& f, boost::any const& data) const override; |
|||
virtual boost::any visit(NextFormula const& f, boost::any const& data) const override; |
|||
virtual boost::any visit(ProbabilityOperatorFormula const& f, boost::any const& data) const override; |
|||
virtual boost::any visit(RewardOperatorFormula const& f, boost::any const& data) const override; |
|||
virtual boost::any visit(UnaryBooleanStateFormula const& f, boost::any const& data) const override; |
|||
virtual boost::any visit(UntilFormula const& f, boost::any const& data) const override; |
|||
}; |
|||
|
|||
} |
|||
} |
|||
|
|||
|
|||
#endif /* STORM_LOGIC_CLONEVISITOR_H_ */ |
|||
@ -0,0 +1,26 @@ |
|||
#include "src/logic/LabelSubstitutionVisitor.h"
|
|||
|
|||
#include "src/logic/Formulas.h"
|
|||
|
|||
namespace storm { |
|||
namespace logic { |
|||
|
|||
LabelSubstitutionVisitor::LabelSubstitutionVisitor(std::map<std::string, storm::expressions::Expression> const& labelToExpressionMapping) : labelToExpressionMapping(labelToExpressionMapping) { |
|||
// Intentionally left empty.
|
|||
} |
|||
|
|||
std::shared_ptr<Formula> LabelSubstitutionVisitor::substitute(Formula const& f) const { |
|||
boost::any result = f.accept(*this, boost::any()); |
|||
return boost::any_cast<std::shared_ptr<Formula>>(result); |
|||
} |
|||
|
|||
boost::any LabelSubstitutionVisitor::visit(AtomicLabelFormula const& f, boost::any const& data) const { |
|||
auto it = labelToExpressionMapping.find(f.getLabel()); |
|||
if (it != labelToExpressionMapping.end()) { |
|||
return std::static_pointer_cast<Formula>(std::make_shared<AtomicExpressionFormula>(it->second)); |
|||
} else { |
|||
return std::static_pointer_cast<Formula>(std::make_shared<AtomicLabelFormula>(f)); |
|||
} |
|||
} |
|||
} |
|||
} |
|||
@ -0,0 +1,29 @@ |
|||
#ifndef STORM_LOGIC_LABELSUBSTITUTIONVISITOR_H_ |
|||
#define STORM_LOGIC_LABELSUBSTITUTIONVISITOR_H_ |
|||
|
|||
#include <map> |
|||
|
|||
#include "src/logic/CloneVisitor.h" |
|||
|
|||
#include "src/storage/expressions/Expression.h" |
|||
|
|||
namespace storm { |
|||
namespace logic { |
|||
|
|||
class LabelSubstitutionVisitor : public CloneVisitor { |
|||
public: |
|||
LabelSubstitutionVisitor(std::map<std::string, storm::expressions::Expression> const& labelToExpressionMapping); |
|||
|
|||
std::shared_ptr<Formula> substitute(Formula const& f) const; |
|||
|
|||
virtual boost::any visit(AtomicLabelFormula const& f, boost::any const& data) const override; |
|||
|
|||
private: |
|||
std::map<std::string, storm::expressions::Expression> const& labelToExpressionMapping; |
|||
}; |
|||
|
|||
} |
|||
} |
|||
|
|||
|
|||
#endif /* STORM_LOGIC_FORMULAINFORMATIONVISITOR_H_ */ |
|||
@ -0,0 +1,111 @@ |
|||
#include "src/logic/ToExpressionVisitor.h"
|
|||
|
|||
#include "src/logic/Formulas.h"
|
|||
|
|||
#include "src/storage/expressions/ExpressionManager.h"
|
|||
|
|||
#include "src/utility/macros.h"
|
|||
#include "src/exceptions/InvalidOperationException.h"
|
|||
|
|||
namespace storm { |
|||
namespace logic { |
|||
|
|||
storm::expressions::Expression ToExpressionVisitor::toExpression(Formula const& f, storm::expressions::ExpressionManager const& manager) const { |
|||
boost::any result = f.accept(*this, std::ref(manager)); |
|||
return boost::any_cast<storm::expressions::Expression>(result); |
|||
} |
|||
|
|||
boost::any ToExpressionVisitor::visit(AtomicExpressionFormula const& f, boost::any const& data) const { |
|||
return f.getExpression(); |
|||
} |
|||
|
|||
boost::any ToExpressionVisitor::visit(AtomicLabelFormula const& f, boost::any const& data) const { |
|||
STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Cannot assemble expression, because the undefined atomic label '" << f.getLabel() << "' appears in the formula."); |
|||
} |
|||
|
|||
boost::any ToExpressionVisitor::visit(BinaryBooleanStateFormula const& f, boost::any const& data) const { |
|||
storm::expressions::Expression left = boost::any_cast<storm::expressions::Expression>(f.getLeftSubformula().accept(*this, data)); |
|||
storm::expressions::Expression right = boost::any_cast<storm::expressions::Expression>(f.getRightSubformula().accept(*this, data)); |
|||
switch (f.getOperator()) { |
|||
case BinaryBooleanStateFormula::OperatorType::And: |
|||
return left && right; |
|||
break; |
|||
case BinaryBooleanStateFormula::OperatorType::Or: |
|||
return left || right; |
|||
break; |
|||
} |
|||
} |
|||
|
|||
boost::any ToExpressionVisitor::visit(BooleanLiteralFormula const& f, boost::any const& data) const { |
|||
storm::expressions::Expression result; |
|||
if (f.isTrueFormula()) { |
|||
result = boost::any_cast<std::reference_wrapper<storm::expressions::ExpressionManager const>>(data).get().boolean(true); |
|||
} else { |
|||
result = boost::any_cast<std::reference_wrapper<storm::expressions::ExpressionManager const>>(data).get().boolean(false); |
|||
} |
|||
return result; |
|||
} |
|||
|
|||
boost::any ToExpressionVisitor::visit(BoundedUntilFormula const& f, boost::any const& data) const { |
|||
STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Cannot assemble expression from formula that contains illegal elements."); |
|||
} |
|||
|
|||
boost::any ToExpressionVisitor::visit(ConditionalFormula const& f, boost::any const& data) const { |
|||
STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Cannot assemble expression from formula that contains illegal elements."); |
|||
} |
|||
|
|||
boost::any ToExpressionVisitor::visit(CumulativeRewardFormula const& f, boost::any const& data) const { |
|||
STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Cannot assemble expression from formula that contains illegal elements."); |
|||
} |
|||
|
|||
boost::any ToExpressionVisitor::visit(EventuallyFormula const& f, boost::any const& data) const { |
|||
STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Cannot assemble expression from formula that contains illegal elements."); |
|||
} |
|||
|
|||
boost::any ToExpressionVisitor::visit(TimeOperatorFormula const& f, boost::any const& data) const { |
|||
STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Cannot assemble expression from formula that contains illegal elements."); |
|||
} |
|||
|
|||
boost::any ToExpressionVisitor::visit(GloballyFormula const& f, boost::any const& data) const { |
|||
STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Cannot assemble expression from formula that contains illegal elements."); |
|||
} |
|||
|
|||
boost::any ToExpressionVisitor::visit(InstantaneousRewardFormula const& f, boost::any const& data) const { |
|||
STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Cannot assemble expression from formula that contains illegal elements."); |
|||
} |
|||
|
|||
boost::any ToExpressionVisitor::visit(LongRunAverageOperatorFormula const& f, boost::any const& data) const { |
|||
STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Cannot assemble expression from formula that contains illegal elements."); |
|||
} |
|||
|
|||
boost::any ToExpressionVisitor::visit(LongRunAverageRewardFormula const& f, boost::any const& data) const { |
|||
STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Cannot assemble expression from formula that contains illegal elements."); |
|||
} |
|||
|
|||
boost::any ToExpressionVisitor::visit(NextFormula const& f, boost::any const& data) const { |
|||
STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Cannot assemble expression from formula that contains illegal elements."); |
|||
} |
|||
|
|||
boost::any ToExpressionVisitor::visit(ProbabilityOperatorFormula const& f, boost::any const& data) const { |
|||
STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Cannot assemble expression from formula that contains illegal elements."); |
|||
} |
|||
|
|||
boost::any ToExpressionVisitor::visit(RewardOperatorFormula const& f, boost::any const& data) const { |
|||
STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Cannot assemble expression from formula that contains illegal elements."); |
|||
} |
|||
|
|||
boost::any ToExpressionVisitor::visit(UnaryBooleanStateFormula const& f, boost::any const& data) const { |
|||
storm::expressions::Expression subexpression = boost::any_cast<storm::expressions::Expression>(f.getSubformula().accept(*this, data)); |
|||
switch (f.getOperator()) { |
|||
case UnaryBooleanStateFormula::OperatorType::Not: |
|||
return !subexpression; |
|||
break; |
|||
} |
|||
} |
|||
|
|||
boost::any ToExpressionVisitor::visit(UntilFormula const& f, boost::any const& data) const { |
|||
STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Cannot assemble expression from formula that contains illegal elements."); |
|||
} |
|||
|
|||
} |
|||
} |
|||
@ -0,0 +1,39 @@ |
|||
#ifndef STORM_LOGIC_TOEXPRESSIONVISITOR_H_ |
|||
#define STORM_LOGIC_TOEXPRESSIONVISITOR_H_ |
|||
|
|||
#include "src/logic/FormulaVisitor.h" |
|||
|
|||
#include "src/storage/expressions/Expression.h" |
|||
|
|||
namespace storm { |
|||
namespace logic { |
|||
|
|||
class ToExpressionVisitor : public FormulaVisitor { |
|||
public: |
|||
storm::expressions::Expression toExpression(Formula const& f, storm::expressions::ExpressionManager const& manager) const; |
|||
|
|||
virtual boost::any visit(AtomicExpressionFormula const& f, boost::any const& data) const override; |
|||
virtual boost::any visit(AtomicLabelFormula const& f, boost::any const& data) const override; |
|||
virtual boost::any visit(BinaryBooleanStateFormula const& f, boost::any const& data) const override; |
|||
virtual boost::any visit(BooleanLiteralFormula const& f, boost::any const& data) const override; |
|||
virtual boost::any visit(BoundedUntilFormula const& f, boost::any const& data) const override; |
|||
virtual boost::any visit(ConditionalFormula const& f, boost::any const& data) const override; |
|||
virtual boost::any visit(CumulativeRewardFormula const& f, boost::any const& data) const override; |
|||
virtual boost::any visit(EventuallyFormula const& f, boost::any const& data) const override; |
|||
virtual boost::any visit(TimeOperatorFormula const& f, boost::any const& data) const override; |
|||
virtual boost::any visit(GloballyFormula const& f, boost::any const& data) const override; |
|||
virtual boost::any visit(InstantaneousRewardFormula const& f, boost::any const& data) const override; |
|||
virtual boost::any visit(LongRunAverageOperatorFormula const& f, boost::any const& data) const override; |
|||
virtual boost::any visit(LongRunAverageRewardFormula const& f, boost::any const& data) const override; |
|||
virtual boost::any visit(NextFormula const& f, boost::any const& data) const override; |
|||
virtual boost::any visit(ProbabilityOperatorFormula const& f, boost::any const& data) const override; |
|||
virtual boost::any visit(RewardOperatorFormula const& f, boost::any const& data) const override; |
|||
virtual boost::any visit(UnaryBooleanStateFormula const& f, boost::any const& data) const override; |
|||
virtual boost::any visit(UntilFormula const& f, boost::any const& data) const override; |
|||
}; |
|||
|
|||
} |
|||
} |
|||
|
|||
|
|||
#endif /* STORM_LOGIC_TOEXPRESSIONVISITOR_H_ */ |
|||
@ -0,0 +1,21 @@ |
|||
#include "src/logic/VariableSubstitutionVisitor.h"
|
|||
|
|||
#include "src/logic/Formulas.h"
|
|||
|
|||
namespace storm { |
|||
namespace logic { |
|||
|
|||
VariableSubstitutionVisitor::VariableSubstitutionVisitor(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) : substitution(substitution) { |
|||
// Intentionally left empty.
|
|||
} |
|||
|
|||
std::shared_ptr<Formula> VariableSubstitutionVisitor::substitute(Formula const& f) const { |
|||
boost::any result = f.accept(*this, boost::any()); |
|||
return boost::any_cast<std::shared_ptr<Formula>>(result); |
|||
} |
|||
|
|||
boost::any VariableSubstitutionVisitor::visit(AtomicExpressionFormula const& f, boost::any const& data) const { |
|||
return std::static_pointer_cast<Formula>(std::make_shared<AtomicExpressionFormula>(f.getExpression().substitute(substitution))); |
|||
} |
|||
} |
|||
} |
|||
@ -0,0 +1,29 @@ |
|||
#ifndef STORM_LOGIC_VARIABLESUBSTITUTIONVISITOR_H_ |
|||
#define STORM_LOGIC_VARIABLESUBSTITUTIONVISITOR_H_ |
|||
|
|||
#include <map> |
|||
|
|||
#include "src/logic/CloneVisitor.h" |
|||
|
|||
#include "src/storage/expressions/Expression.h" |
|||
|
|||
namespace storm { |
|||
namespace logic { |
|||
|
|||
class VariableSubstitutionVisitor : public CloneVisitor { |
|||
public: |
|||
VariableSubstitutionVisitor(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution); |
|||
|
|||
std::shared_ptr<Formula> substitute(Formula const& f) const; |
|||
|
|||
virtual boost::any visit(AtomicExpressionFormula const& f, boost::any const& data) const override; |
|||
|
|||
private: |
|||
std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution; |
|||
}; |
|||
|
|||
} |
|||
} |
|||
|
|||
|
|||
#endif /* STORM_LOGIC_VARIABLESUBSTITUTIONVISITOR_H_ */ |
|||
@ -0,0 +1,149 @@ |
|||
#include "src/modelchecker/exploration/Bounds.h"
|
|||
|
|||
#include "src/modelchecker/exploration/ExplorationInformation.h"
|
|||
|
|||
namespace storm { |
|||
namespace modelchecker { |
|||
namespace exploration_detail { |
|||
|
|||
template<typename StateType, typename ValueType> |
|||
std::pair<ValueType, ValueType> Bounds<StateType, ValueType>::getBoundsForState(StateType const& state, ExplorationInformation<StateType, ValueType> const& explorationInformation) const { |
|||
ActionType index = explorationInformation.getRowGroup(state); |
|||
if (index == explorationInformation.getUnexploredMarker()) { |
|||
return std::make_pair(storm::utility::zero<ValueType>(), storm::utility::one<ValueType>()); |
|||
} else { |
|||
return boundsPerState[index]; |
|||
} |
|||
} |
|||
|
|||
template<typename StateType, typename ValueType> |
|||
ValueType Bounds<StateType, ValueType>::getLowerBoundForState(StateType const& state, ExplorationInformation<StateType, ValueType> const& explorationInformation) const { |
|||
ActionType index = explorationInformation.getRowGroup(state); |
|||
if (index == explorationInformation.getUnexploredMarker()) { |
|||
return storm::utility::zero<ValueType>(); |
|||
} else { |
|||
return getLowerBoundForRowGroup(index); |
|||
} |
|||
} |
|||
|
|||
template<typename StateType, typename ValueType> |
|||
ValueType const& Bounds<StateType, ValueType>::getLowerBoundForRowGroup(StateType const& rowGroup) const { |
|||
return boundsPerState[rowGroup].first; |
|||
} |
|||
|
|||
template<typename StateType, typename ValueType> |
|||
ValueType Bounds<StateType, ValueType>::getUpperBoundForState(StateType const& state, ExplorationInformation<StateType, ValueType> const& explorationInformation) const { |
|||
ActionType index = explorationInformation.getRowGroup(state); |
|||
if (index == explorationInformation.getUnexploredMarker()) { |
|||
return storm::utility::one<ValueType>(); |
|||
} else { |
|||
return getUpperBoundForRowGroup(index); |
|||
} |
|||
} |
|||
|
|||
template<typename StateType, typename ValueType> |
|||
ValueType const& Bounds<StateType, ValueType>::getUpperBoundForRowGroup(StateType const& rowGroup) const { |
|||
return boundsPerState[rowGroup].second; |
|||
} |
|||
|
|||
template<typename StateType, typename ValueType> |
|||
std::pair<ValueType, ValueType> const& Bounds<StateType, ValueType>::getBoundsForAction(ActionType const& action) const { |
|||
return boundsPerAction[action]; |
|||
} |
|||
|
|||
template<typename StateType, typename ValueType> |
|||
ValueType const& Bounds<StateType, ValueType>::getLowerBoundForAction(ActionType const& action) const { |
|||
return boundsPerAction[action].first; |
|||
} |
|||
|
|||
template<typename StateType, typename ValueType> |
|||
ValueType const& Bounds<StateType, ValueType>::getUpperBoundForAction(ActionType const& action) const { |
|||
return boundsPerAction[action].second; |
|||
} |
|||
|
|||
template<typename StateType, typename ValueType> |
|||
ValueType const& Bounds<StateType, ValueType>::getBoundForAction(storm::OptimizationDirection const& direction, ActionType const& action) const { |
|||
if (direction == storm::OptimizationDirection::Maximize) { |
|||
return getUpperBoundForAction(action); |
|||
} else { |
|||
return getLowerBoundForAction(action); |
|||
} |
|||
} |
|||
|
|||
template<typename StateType, typename ValueType> |
|||
ValueType Bounds<StateType, ValueType>::getDifferenceOfStateBounds(StateType const& state, ExplorationInformation<StateType, ValueType> const& explorationInformation) const { |
|||
std::pair<ValueType, ValueType> bounds = getBoundsForState(state, explorationInformation); |
|||
return bounds.second - bounds.first; |
|||
} |
|||
|
|||
template<typename StateType, typename ValueType> |
|||
void Bounds<StateType, ValueType>::initializeBoundsForNextState(std::pair<ValueType, ValueType> const& vals) { |
|||
boundsPerState.push_back(vals); |
|||
} |
|||
|
|||
template<typename StateType, typename ValueType> |
|||
void Bounds<StateType, ValueType>::initializeBoundsForNextAction(std::pair<ValueType, ValueType> const& vals) { |
|||
boundsPerAction.push_back(vals); |
|||
} |
|||
|
|||
template<typename StateType, typename ValueType> |
|||
void Bounds<StateType, ValueType>::setLowerBoundForState(StateType const& state, ExplorationInformation<StateType, ValueType> const& explorationInformation, ValueType const& value) { |
|||
setLowerBoundForRowGroup(explorationInformation.getRowGroup(state), value); |
|||
} |
|||
|
|||
template<typename StateType, typename ValueType> |
|||
void Bounds<StateType, ValueType>::setLowerBoundForRowGroup(StateType const& group, ValueType const& value) { |
|||
boundsPerState[group].first = value; |
|||
} |
|||
|
|||
template<typename StateType, typename ValueType> |
|||
void Bounds<StateType, ValueType>::setUpperBoundForState(StateType const& state, ExplorationInformation<StateType, ValueType> const& explorationInformation, ValueType const& value) { |
|||
setUpperBoundForRowGroup(explorationInformation.getRowGroup(state), value); |
|||
} |
|||
|
|||
template<typename StateType, typename ValueType> |
|||
void Bounds<StateType, ValueType>::setUpperBoundForRowGroup(StateType const& group, ValueType const& value) { |
|||
boundsPerState[group].second = value; |
|||
} |
|||
|
|||
template<typename StateType, typename ValueType> |
|||
void Bounds<StateType, ValueType>::setBoundsForAction(ActionType const& action, std::pair<ValueType, ValueType> const& values) { |
|||
boundsPerAction[action] = values; |
|||
} |
|||
|
|||
template<typename StateType, typename ValueType> |
|||
void Bounds<StateType, ValueType>::setBoundsForState(StateType const& state, ExplorationInformation<StateType, ValueType> const& explorationInformation, std::pair<ValueType, ValueType> const& values) { |
|||
StateType const& rowGroup = explorationInformation.getRowGroup(state); |
|||
setBoundsForRowGroup(rowGroup, values); |
|||
} |
|||
|
|||
template<typename StateType, typename ValueType> |
|||
void Bounds<StateType, ValueType>::setBoundsForRowGroup(StateType const& rowGroup, std::pair<ValueType, ValueType> const& values) { |
|||
boundsPerState[rowGroup] = values; |
|||
} |
|||
|
|||
template<typename StateType, typename ValueType> |
|||
bool Bounds<StateType, ValueType>::setLowerBoundOfStateIfGreaterThanOld(StateType const& state, ExplorationInformation<StateType, ValueType> const& explorationInformation, ValueType const& newLowerValue) { |
|||
StateType const& rowGroup = explorationInformation.getRowGroup(state); |
|||
if (boundsPerState[rowGroup].first < newLowerValue) { |
|||
boundsPerState[rowGroup].first = newLowerValue; |
|||
return true; |
|||
} |
|||
return false; |
|||
} |
|||
|
|||
template<typename StateType, typename ValueType> |
|||
bool Bounds<StateType, ValueType>::setUpperBoundOfStateIfLessThanOld(StateType const& state, ExplorationInformation<StateType, ValueType> const& explorationInformation, ValueType const& newUpperValue) { |
|||
StateType const& rowGroup = explorationInformation.getRowGroup(state); |
|||
if (newUpperValue < boundsPerState[rowGroup].second) { |
|||
boundsPerState[rowGroup].second = newUpperValue; |
|||
return true; |
|||
} |
|||
return false; |
|||
} |
|||
|
|||
template class Bounds<uint32_t, double>; |
|||
|
|||
} |
|||
} |
|||
} |
|||
@ -0,0 +1,74 @@ |
|||
#ifndef STORM_MODELCHECKER_EXPLORATION_EXPLORATION_DETAIL_BOUNDS_H_ |
|||
#define STORM_MODELCHECKER_EXPLORATION_EXPLORATION_DETAIL_BOUNDS_H_ |
|||
|
|||
#include <vector> |
|||
#include <utility> |
|||
|
|||
#include "src/solver/OptimizationDirection.h" |
|||
|
|||
#include "src/utility/constants.h" |
|||
|
|||
namespace storm { |
|||
namespace modelchecker { |
|||
namespace exploration_detail { |
|||
|
|||
template<typename StateType, typename ValueType> |
|||
class ExplorationInformation; |
|||
|
|||
template<typename StateType, typename ValueType> |
|||
class Bounds { |
|||
public: |
|||
typedef StateType ActionType; |
|||
|
|||
std::pair<ValueType, ValueType> getBoundsForState(StateType const& state, ExplorationInformation<StateType, ValueType> const& explorationInformation) const; |
|||
|
|||
ValueType getLowerBoundForState(StateType const& state, ExplorationInformation<StateType, ValueType> const& explorationInformation) const; |
|||
|
|||
ValueType const& getLowerBoundForRowGroup(StateType const& rowGroup) const; |
|||
|
|||
ValueType getUpperBoundForState(StateType const& state, ExplorationInformation<StateType, ValueType> const& explorationInformation) const; |
|||
|
|||
ValueType const& getUpperBoundForRowGroup(StateType const& rowGroup) const; |
|||
|
|||
std::pair<ValueType, ValueType> const& getBoundsForAction(ActionType const& action) const; |
|||
|
|||
ValueType const& getLowerBoundForAction(ActionType const& action) const; |
|||
|
|||
ValueType const& getUpperBoundForAction(ActionType const& action) const; |
|||
|
|||
ValueType const& getBoundForAction(storm::OptimizationDirection const& direction, ActionType const& action) const; |
|||
|
|||
ValueType getDifferenceOfStateBounds(StateType const& state, ExplorationInformation<StateType, ValueType> const& explorationInformation) const; |
|||
|
|||
void initializeBoundsForNextState(std::pair<ValueType, ValueType> const& vals = std::pair<ValueType, ValueType>(storm::utility::zero<ValueType>(), storm::utility::one<ValueType>())); |
|||
|
|||
void initializeBoundsForNextAction(std::pair<ValueType, ValueType> const& vals = std::pair<ValueType, ValueType>(storm::utility::zero<ValueType>(), storm::utility::one<ValueType>())); |
|||
|
|||
void setLowerBoundForState(StateType const& state, ExplorationInformation<StateType, ValueType> const& explorationInformation, ValueType const& value); |
|||
|
|||
void setLowerBoundForRowGroup(StateType const& group, ValueType const& value); |
|||
|
|||
void setUpperBoundForState(StateType const& state, ExplorationInformation<StateType, ValueType> const& explorationInformation, ValueType const& value); |
|||
|
|||
void setUpperBoundForRowGroup(StateType const& group, ValueType const& value); |
|||
|
|||
void setBoundsForAction(ActionType const& action, std::pair<ValueType, ValueType> const& values); |
|||
|
|||
void setBoundsForState(StateType const& state, ExplorationInformation<StateType, ValueType> const& explorationInformation, std::pair<ValueType, ValueType> const& values); |
|||
|
|||
void setBoundsForRowGroup(StateType const& rowGroup, std::pair<ValueType, ValueType> const& values); |
|||
|
|||
bool setLowerBoundOfStateIfGreaterThanOld(StateType const& state, ExplorationInformation<StateType, ValueType> const& explorationInformation, ValueType const& newLowerValue); |
|||
|
|||
bool setUpperBoundOfStateIfLessThanOld(StateType const& state, ExplorationInformation<StateType, ValueType> const& explorationInformation, ValueType const& newUpperValue); |
|||
|
|||
private: |
|||
std::vector<std::pair<ValueType, ValueType>> boundsPerState; |
|||
std::vector<std::pair<ValueType, ValueType>> boundsPerAction; |
|||
}; |
|||
|
|||
} |
|||
} |
|||
} |
|||
|
|||
#endif /* STORM_MODELCHECKER_EXPLORATION_EXPLORATION_DETAIL_BOUNDS_H_ */ |
|||
@ -0,0 +1,227 @@ |
|||
#include "src/modelchecker/exploration/ExplorationInformation.h"
|
|||
|
|||
#include "src/settings/SettingsManager.h"
|
|||
#include "src/settings/modules/ExplorationSettings.h"
|
|||
|
|||
#include "src/utility/macros.h"
|
|||
|
|||
namespace storm { |
|||
namespace modelchecker { |
|||
namespace exploration_detail { |
|||
|
|||
template<typename StateType, typename ValueType> |
|||
ExplorationInformation<StateType, ValueType>::ExplorationInformation(storm::OptimizationDirection const& direction, ActionType const& unexploredMarker) : unexploredMarker(unexploredMarker), optimizationDirection(direction), localPrecomputation(false), numberOfExplorationStepsUntilPrecomputation(100000), numberOfSampledPathsUntilPrecomputation(), nextStateHeuristic(storm::settings::modules::ExplorationSettings::NextStateHeuristic::DifferenceProbabilitySum) { |
|||
|
|||
storm::settings::modules::ExplorationSettings const& settings = storm::settings::explorationSettings(); |
|||
localPrecomputation = settings.isLocalPrecomputationSet(); |
|||
numberOfExplorationStepsUntilPrecomputation = settings.getNumberOfExplorationStepsUntilPrecomputation(); |
|||
if (settings.isNumberOfSampledPathsUntilPrecomputationSet()) { |
|||
numberOfSampledPathsUntilPrecomputation = settings.getNumberOfSampledPathsUntilPrecomputation(); |
|||
} |
|||
|
|||
nextStateHeuristic = settings.getNextStateHeuristic(); |
|||
} |
|||
|
|||
template<typename StateType, typename ValueType> |
|||
typename ExplorationInformation<StateType, ValueType>::const_iterator ExplorationInformation<StateType, ValueType>::findUnexploredState(StateType const& state) const { |
|||
return unexploredStates.find(state); |
|||
} |
|||
|
|||
template<typename StateType, typename ValueType> |
|||
typename ExplorationInformation<StateType, ValueType>::const_iterator ExplorationInformation<StateType, ValueType>::unexploredStatesEnd() const { |
|||
return unexploredStates.end(); |
|||
} |
|||
|
|||
template<typename StateType, typename ValueType> |
|||
void ExplorationInformation<StateType, ValueType>::removeUnexploredState(const_iterator it) { |
|||
unexploredStates.erase(it); |
|||
} |
|||
|
|||
template<typename StateType, typename ValueType> |
|||
void ExplorationInformation<StateType, ValueType>::addUnexploredState(StateType const& stateId, storm::generator::CompressedState const& compressedState) { |
|||
stateToRowGroupMapping.push_back(unexploredMarker); |
|||
unexploredStates[stateId] = compressedState; |
|||
} |
|||
|
|||
template<typename StateType, typename ValueType> |
|||
void ExplorationInformation<StateType, ValueType>::assignStateToRowGroup(StateType const& state, ActionType const& rowGroup) { |
|||
stateToRowGroupMapping[state] = rowGroup; |
|||
} |
|||
|
|||
template<typename StateType, typename ValueType> |
|||
StateType ExplorationInformation<StateType, ValueType>::assignStateToNextRowGroup(StateType const& state) { |
|||
stateToRowGroupMapping[state] = rowGroupIndices.size() - 1; |
|||
return stateToRowGroupMapping[state]; |
|||
} |
|||
|
|||
template<typename StateType, typename ValueType> |
|||
StateType ExplorationInformation<StateType, ValueType>::getNextRowGroup() const { |
|||
return rowGroupIndices.size() - 1; |
|||
} |
|||
|
|||
template<typename StateType, typename ValueType> |
|||
void ExplorationInformation<StateType, ValueType>::newRowGroup(ActionType const& action) { |
|||
rowGroupIndices.push_back(action); |
|||
} |
|||
|
|||
template<typename StateType, typename ValueType> |
|||
void ExplorationInformation<StateType, ValueType>::newRowGroup() { |
|||
newRowGroup(matrix.size()); |
|||
} |
|||
|
|||
template<typename StateType, typename ValueType> |
|||
void ExplorationInformation<StateType, ValueType>::terminateCurrentRowGroup() { |
|||
rowGroupIndices.push_back(matrix.size()); |
|||
} |
|||
|
|||
template<typename StateType, typename ValueType> |
|||
void ExplorationInformation<StateType, ValueType>::moveActionToBackOfMatrix(ActionType const& action) { |
|||
matrix.emplace_back(std::move(matrix[action])); |
|||
} |
|||
|
|||
template<typename StateType, typename ValueType> |
|||
StateType ExplorationInformation<StateType, ValueType>::getActionCount() const { |
|||
return matrix.size(); |
|||
} |
|||
|
|||
template<typename StateType, typename ValueType> |
|||
std::size_t ExplorationInformation<StateType, ValueType>::getNumberOfUnexploredStates() const { |
|||
return unexploredStates.size(); |
|||
} |
|||
|
|||
template<typename StateType, typename ValueType> |
|||
std::size_t ExplorationInformation<StateType, ValueType>::getNumberOfDiscoveredStates() const { |
|||
return stateToRowGroupMapping.size(); |
|||
} |
|||
|
|||
template<typename StateType, typename ValueType> |
|||
StateType const& ExplorationInformation<StateType, ValueType>::getRowGroup(StateType const& state) const { |
|||
return stateToRowGroupMapping[state]; |
|||
} |
|||
|
|||
template<typename StateType, typename ValueType> |
|||
StateType const& ExplorationInformation<StateType, ValueType>::getUnexploredMarker() const { |
|||
return unexploredMarker; |
|||
} |
|||
|
|||
template<typename StateType, typename ValueType> |
|||
bool ExplorationInformation<StateType, ValueType>::isUnexplored(StateType const& state) const { |
|||
return stateToRowGroupMapping[state] == unexploredMarker; |
|||
} |
|||
|
|||
template<typename StateType, typename ValueType> |
|||
bool ExplorationInformation<StateType, ValueType>::isTerminal(StateType const& state) const { |
|||
return terminalStates.find(state) != terminalStates.end(); |
|||
} |
|||
|
|||
template<typename StateType, typename ValueType> |
|||
typename ExplorationInformation<StateType, ValueType>::ActionType const& ExplorationInformation<StateType, ValueType>::getStartRowOfGroup(StateType const& group) const { |
|||
return rowGroupIndices[group]; |
|||
} |
|||
|
|||
template<typename StateType, typename ValueType> |
|||
std::size_t ExplorationInformation<StateType, ValueType>::getRowGroupSize(StateType const& group) const { |
|||
return rowGroupIndices[group + 1] - rowGroupIndices[group]; |
|||
} |
|||
|
|||
template<typename StateType, typename ValueType> |
|||
bool ExplorationInformation<StateType, ValueType>::onlyOneActionAvailable(StateType const& group) const { |
|||
return getRowGroupSize(group) == 1; |
|||
} |
|||
|
|||
template<typename StateType, typename ValueType> |
|||
void ExplorationInformation<StateType, ValueType>::addTerminalState(StateType const& state) { |
|||
terminalStates.insert(state); |
|||
} |
|||
|
|||
template<typename StateType, typename ValueType> |
|||
std::vector<storm::storage::MatrixEntry<StateType, ValueType>>& ExplorationInformation<StateType, ValueType>::getRowOfMatrix(ActionType const& row) { |
|||
return matrix[row]; |
|||
} |
|||
|
|||
template<typename StateType, typename ValueType> |
|||
std::vector<storm::storage::MatrixEntry<StateType, ValueType>> const& ExplorationInformation<StateType, ValueType>::getRowOfMatrix(ActionType const& row) const { |
|||
return matrix[row]; |
|||
} |
|||
|
|||
template<typename StateType, typename ValueType> |
|||
void ExplorationInformation<StateType, ValueType>::addActionsToMatrix(std::size_t const& count) { |
|||
matrix.resize(matrix.size() + count); |
|||
} |
|||
|
|||
template<typename StateType, typename ValueType> |
|||
bool ExplorationInformation<StateType, ValueType>::maximize() const { |
|||
return optimizationDirection == storm::OptimizationDirection::Maximize; |
|||
} |
|||
|
|||
template<typename StateType, typename ValueType> |
|||
bool ExplorationInformation<StateType, ValueType>::minimize() const { |
|||
return !maximize(); |
|||
} |
|||
|
|||
template<typename StateType, typename ValueType> |
|||
bool ExplorationInformation<StateType, ValueType>::performPrecomputationExcessiveExplorationSteps(std::size_t& numberExplorationStepsSinceLastPrecomputation) const { |
|||
bool result = numberExplorationStepsSinceLastPrecomputation > numberOfExplorationStepsUntilPrecomputation; |
|||
if (result) { |
|||
numberExplorationStepsSinceLastPrecomputation = 0; |
|||
} |
|||
return result; |
|||
} |
|||
|
|||
template<typename StateType, typename ValueType> |
|||
bool ExplorationInformation<StateType, ValueType>::performPrecomputationExcessiveSampledPaths(std::size_t& numberOfSampledPathsSinceLastPrecomputation) const { |
|||
if (!numberOfSampledPathsUntilPrecomputation) { |
|||
return false; |
|||
} else { |
|||
bool result = numberOfSampledPathsSinceLastPrecomputation > numberOfSampledPathsUntilPrecomputation.get(); |
|||
if (result) { |
|||
numberOfSampledPathsSinceLastPrecomputation = 0; |
|||
} |
|||
return result; |
|||
} |
|||
} |
|||
|
|||
template<typename StateType, typename ValueType> |
|||
bool ExplorationInformation<StateType, ValueType>::useLocalPrecomputation() const { |
|||
return localPrecomputation; |
|||
} |
|||
|
|||
template<typename StateType, typename ValueType> |
|||
bool ExplorationInformation<StateType, ValueType>::useGlobalPrecomputation() const { |
|||
return !useLocalPrecomputation(); |
|||
} |
|||
|
|||
template<typename StateType, typename ValueType> |
|||
storm::settings::modules::ExplorationSettings::NextStateHeuristic const& ExplorationInformation<StateType, ValueType>::getNextStateHeuristic() const { |
|||
return nextStateHeuristic; |
|||
} |
|||
|
|||
template<typename StateType, typename ValueType> |
|||
bool ExplorationInformation<StateType, ValueType>::useDifferenceProbabilitySumHeuristic() const { |
|||
return nextStateHeuristic == storm::settings::modules::ExplorationSettings::NextStateHeuristic::DifferenceProbabilitySum; |
|||
} |
|||
|
|||
template<typename StateType, typename ValueType> |
|||
bool ExplorationInformation<StateType, ValueType>::useProbabilityHeuristic() const { |
|||
return nextStateHeuristic == storm::settings::modules::ExplorationSettings::NextStateHeuristic::Probability; |
|||
} |
|||
|
|||
template<typename StateType, typename ValueType> |
|||
bool ExplorationInformation<StateType, ValueType>::useUniformHeuristic() const { |
|||
return nextStateHeuristic == storm::settings::modules::ExplorationSettings::NextStateHeuristic::Uniform; |
|||
} |
|||
|
|||
template<typename StateType, typename ValueType> |
|||
storm::OptimizationDirection const& ExplorationInformation<StateType, ValueType>::getOptimizationDirection() const { |
|||
return optimizationDirection; |
|||
} |
|||
|
|||
template<typename StateType, typename ValueType> |
|||
void ExplorationInformation<StateType, ValueType>::setOptimizationDirection(storm::OptimizationDirection const& direction) { |
|||
optimizationDirection = direction; |
|||
} |
|||
|
|||
template class ExplorationInformation<uint32_t, double>; |
|||
} |
|||
} |
|||
} |
|||
@ -0,0 +1,128 @@ |
|||
#ifndef STORM_MODELCHECKER_EXPLORATION_EXPLORATION_DETAIL_EXPLORATIONINFORMATION_H_ |
|||
#define STORM_MODELCHECKER_EXPLORATION_EXPLORATION_DETAIL_EXPLORATIONINFORMATION_H_ |
|||
|
|||
#include <vector> |
|||
#include <limits> |
|||
#include <unordered_map> |
|||
|
|||
#include <boost/optional.hpp> |
|||
#include <boost/container/flat_set.hpp> |
|||
|
|||
#include "src/solver/OptimizationDirection.h" |
|||
|
|||
#include "src/generator/CompressedState.h" |
|||
|
|||
#include "src/storage/SparseMatrix.h" |
|||
|
|||
#include "src/settings/modules/ExplorationSettings.h" |
|||
|
|||
namespace storm { |
|||
namespace modelchecker { |
|||
namespace exploration_detail { |
|||
template<typename StateType, typename ValueType> |
|||
class ExplorationInformation { |
|||
public: |
|||
typedef StateType ActionType; |
|||
typedef boost::container::flat_set<StateType> StateSet; |
|||
typedef std::unordered_map<StateType, storm::generator::CompressedState> IdToStateMap; |
|||
typedef typename IdToStateMap::const_iterator const_iterator; |
|||
typedef std::vector<std::vector<storm::storage::MatrixEntry<StateType, ValueType>>> MatrixType; |
|||
|
|||
ExplorationInformation(storm::OptimizationDirection const& direction, ActionType const& unexploredMarker = std::numeric_limits<ActionType>::max()); |
|||
|
|||
const_iterator findUnexploredState(StateType const& state) const; |
|||
|
|||
const_iterator unexploredStatesEnd() const; |
|||
|
|||
void removeUnexploredState(const_iterator it); |
|||
|
|||
void addUnexploredState(StateType const& stateId, storm::generator::CompressedState const& compressedState); |
|||
|
|||
void assignStateToRowGroup(StateType const& state, ActionType const& rowGroup); |
|||
|
|||
StateType assignStateToNextRowGroup(StateType const& state); |
|||
|
|||
StateType getNextRowGroup() const; |
|||
|
|||
void newRowGroup(ActionType const& action); |
|||
|
|||
void newRowGroup(); |
|||
|
|||
void terminateCurrentRowGroup(); |
|||
|
|||
void moveActionToBackOfMatrix(ActionType const& action); |
|||
|
|||
StateType getActionCount() const; |
|||
|
|||
std::size_t getNumberOfUnexploredStates() const; |
|||
|
|||
std::size_t getNumberOfDiscoveredStates() const; |
|||
|
|||
StateType const& getRowGroup(StateType const& state) const; |
|||
|
|||
StateType const& getUnexploredMarker() const; |
|||
|
|||
bool isUnexplored(StateType const& state) const; |
|||
|
|||
bool isTerminal(StateType const& state) const; |
|||
|
|||
ActionType const& getStartRowOfGroup(StateType const& group) const; |
|||
|
|||
std::size_t getRowGroupSize(StateType const& group) const; |
|||
|
|||
bool onlyOneActionAvailable(StateType const& group) const; |
|||
|
|||
void addTerminalState(StateType const& state); |
|||
|
|||
std::vector<storm::storage::MatrixEntry<StateType, ValueType>>& getRowOfMatrix(ActionType const& row); |
|||
|
|||
std::vector<storm::storage::MatrixEntry<StateType, ValueType>> const& getRowOfMatrix(ActionType const& row) const; |
|||
|
|||
void addActionsToMatrix(std::size_t const& count); |
|||
|
|||
bool maximize() const; |
|||
|
|||
bool minimize() const; |
|||
|
|||
bool performPrecomputationExcessiveExplorationSteps(std::size_t& numberExplorationStepsSinceLastPrecomputation) const; |
|||
|
|||
bool performPrecomputationExcessiveSampledPaths(std::size_t& numberOfSampledPathsSinceLastPrecomputation) const; |
|||
|
|||
bool useLocalPrecomputation() const; |
|||
|
|||
bool useGlobalPrecomputation() const; |
|||
|
|||
storm::settings::modules::ExplorationSettings::NextStateHeuristic const& getNextStateHeuristic() const; |
|||
|
|||
bool useDifferenceProbabilitySumHeuristic() const; |
|||
|
|||
bool useProbabilityHeuristic() const; |
|||
|
|||
bool useUniformHeuristic() const; |
|||
|
|||
storm::OptimizationDirection const& getOptimizationDirection() const; |
|||
|
|||
void setOptimizationDirection(storm::OptimizationDirection const& direction); |
|||
|
|||
private: |
|||
MatrixType matrix; |
|||
std::vector<StateType> rowGroupIndices; |
|||
|
|||
std::vector<StateType> stateToRowGroupMapping; |
|||
StateType unexploredMarker; |
|||
IdToStateMap unexploredStates; |
|||
|
|||
storm::OptimizationDirection optimizationDirection; |
|||
StateSet terminalStates; |
|||
|
|||
bool localPrecomputation; |
|||
std::size_t numberOfExplorationStepsUntilPrecomputation; |
|||
boost::optional<std::size_t> numberOfSampledPathsUntilPrecomputation; |
|||
|
|||
storm::settings::modules::ExplorationSettings::NextStateHeuristic nextStateHeuristic; |
|||
}; |
|||
} |
|||
} |
|||
} |
|||
|
|||
#endif /* STORM_MODELCHECKER_EXPLORATION_EXPLORATION_DETAIL_EXPLORATIONINFORMATION_H_ */ |
|||
@ -0,0 +1,687 @@ |
|||
#include "src/modelchecker/exploration/SparseExplorationModelChecker.h"
|
|||
|
|||
#include "src/modelchecker/exploration/ExplorationInformation.h"
|
|||
#include "src/modelchecker/exploration/StateGeneration.h"
|
|||
#include "src/modelchecker/exploration/Bounds.h"
|
|||
#include "src/modelchecker/exploration/Statistics.h"
|
|||
|
|||
#include "src/generator/CompressedState.h"
|
|||
|
|||
#include "src/storage/SparseMatrix.h"
|
|||
#include "src/storage/MaximalEndComponentDecomposition.h"
|
|||
|
|||
#include "src/storage/prism/Program.h"
|
|||
|
|||
#include "src/logic/FragmentSpecification.h"
|
|||
|
|||
#include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h"
|
|||
|
|||
#include "src/models/sparse/StandardRewardModel.h"
|
|||
|
|||
#include "src/settings/SettingsManager.h"
|
|||
#include "src/settings/modules/GeneralSettings.h"
|
|||
|
|||
#include "src/utility/macros.h"
|
|||
#include "src/utility/constants.h"
|
|||
#include "src/utility/graph.h"
|
|||
#include "src/utility/prism.h"
|
|||
|
|||
#include "src/exceptions/InvalidOperationException.h"
|
|||
#include "src/exceptions/InvalidPropertyException.h"
|
|||
#include "src/exceptions/NotSupportedException.h"
|
|||
|
|||
namespace storm { |
|||
namespace modelchecker { |
|||
|
|||
template<typename ValueType, typename StateType> |
|||
SparseExplorationModelChecker<ValueType, StateType>::SparseExplorationModelChecker(storm::prism::Program const& program, boost::optional<std::map<storm::expressions::Variable, storm::expressions::Expression>> const& constantDefinitions) : program(storm::utility::prism::preprocessProgram<ValueType>(program, constantDefinitions)), variableInformation(this->program), randomGenerator(std::chrono::system_clock::now().time_since_epoch().count()), comparator(storm::settings::explorationSettings().getPrecision()) { |
|||
// Intentionally left empty.
|
|||
} |
|||
|
|||
template<typename ValueType, typename StateType> |
|||
bool SparseExplorationModelChecker<ValueType, StateType>::canHandle(CheckTask<storm::logic::Formula> const& checkTask) const { |
|||
storm::logic::Formula const& formula = checkTask.getFormula(); |
|||
storm::logic::FragmentSpecification fragment = storm::logic::reachability(); |
|||
return formula.isInFragment(fragment) && checkTask.isOnlyInitialStatesRelevantSet(); |
|||
} |
|||
|
|||
template<typename ValueType, typename StateType> |
|||
std::unique_ptr<CheckResult> SparseExplorationModelChecker<ValueType, StateType>::computeUntilProbabilities(CheckTask<storm::logic::UntilFormula> const& checkTask) { |
|||
storm::logic::UntilFormula const& untilFormula = checkTask.getFormula(); |
|||
storm::logic::Formula const& conditionFormula = untilFormula.getLeftSubformula(); |
|||
storm::logic::Formula const& targetFormula = untilFormula.getRightSubformula(); |
|||
STORM_LOG_THROW(program.isDeterministicModel() || checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException, "For nondeterministic systems, an optimization direction (min/max) must be given in the property."); |
|||
|
|||
ExplorationInformation<StateType, ValueType> explorationInformation(checkTask.isOptimizationDirectionSet() ? checkTask.getOptimizationDirection() : storm::OptimizationDirection::Maximize); |
|||
|
|||
// The first row group starts at action 0.
|
|||
explorationInformation.newRowGroup(0); |
|||
|
|||
std::map<std::string, storm::expressions::Expression> labelToExpressionMapping = program.getLabelToExpressionMapping(); |
|||
StateGeneration<StateType, ValueType> stateGeneration(program, variableInformation, explorationInformation, conditionFormula.toExpression(program.getManager(), labelToExpressionMapping), targetFormula.toExpression(program.getManager(), labelToExpressionMapping)); |
|||
|
|||
|
|||
// Compute and return result.
|
|||
std::tuple<StateType, ValueType, ValueType> boundsForInitialState = performExploration(stateGeneration, explorationInformation); |
|||
return std::make_unique<ExplicitQuantitativeCheckResult<ValueType>>(std::get<0>(boundsForInitialState), std::get<1>(boundsForInitialState)); |
|||
} |
|||
|
|||
template<typename ValueType, typename StateType> |
|||
std::tuple<StateType, ValueType, ValueType> SparseExplorationModelChecker<ValueType, StateType>::performExploration(StateGeneration<StateType, ValueType>& stateGeneration, ExplorationInformation<StateType, ValueType>& explorationInformation) const { |
|||
// Generate the initial state so we know where to start the simulation.
|
|||
stateGeneration.computeInitialStates(); |
|||
STORM_LOG_THROW(stateGeneration.getNumberOfInitialStates() == 1, storm::exceptions::NotSupportedException, "Currently only models with one initial state are supported by the exploration engine."); |
|||
StateType initialStateIndex = stateGeneration.getFirstInitialState(); |
|||
|
|||
// Create a structure that holds the bounds for the states and actions.
|
|||
Bounds<StateType, ValueType> bounds; |
|||
|
|||
// Create a stack that is used to track the path we sampled.
|
|||
StateActionStack stack; |
|||
|
|||
// Now perform the actual sampling.
|
|||
Statistics<StateType, ValueType> stats; |
|||
bool convergenceCriterionMet = false; |
|||
while (!convergenceCriterionMet) { |
|||
bool result = samplePathFromInitialState(stateGeneration, explorationInformation, stack, bounds, stats); |
|||
|
|||
stats.sampledPath(); |
|||
stats.updateMaxPathLength(stack.size()); |
|||
|
|||
// If a terminal state was found, we update the probabilities along the path contained in the stack.
|
|||
if (result) { |
|||
// Update the bounds along the path to the terminal state.
|
|||
STORM_LOG_TRACE("Found terminal state, updating probabilities along path."); |
|||
updateProbabilityBoundsAlongSampledPath(stack, explorationInformation, bounds); |
|||
} else { |
|||
// If not terminal state was found, the search aborted, possibly because of an EC-detection. In this
|
|||
// case, we cannot update the probabilities.
|
|||
STORM_LOG_TRACE("Did not find terminal state."); |
|||
} |
|||
|
|||
STORM_LOG_DEBUG("Discovered states: " << explorationInformation.getNumberOfDiscoveredStates() << " (" << stats.numberOfExploredStates << " explored, " << explorationInformation.getNumberOfUnexploredStates() << " unexplored)."); |
|||
STORM_LOG_DEBUG("Value of initial state is in [" << bounds.getLowerBoundForState(initialStateIndex, explorationInformation) << ", " << bounds.getUpperBoundForState(initialStateIndex, explorationInformation) << "]."); |
|||
ValueType difference = bounds.getDifferenceOfStateBounds(initialStateIndex, explorationInformation); |
|||
STORM_LOG_DEBUG("Difference after iteration " << stats.pathsSampled << " is " << difference << "."); |
|||
convergenceCriterionMet = comparator.isZero(difference); |
|||
|
|||
// If the number of sampled paths exceeds a certain threshold, do a precomputation.
|
|||
if (!convergenceCriterionMet && explorationInformation.performPrecomputationExcessiveSampledPaths(stats.pathsSampledSinceLastPrecomputation)) { |
|||
performPrecomputation(stack, explorationInformation, bounds, stats); |
|||
} |
|||
} |
|||
|
|||
// Show statistics if required.
|
|||
if (storm::settings::generalSettings().isShowStatisticsSet()) { |
|||
stats.printToStream(std::cout, explorationInformation); |
|||
} |
|||
|
|||
return std::make_tuple(initialStateIndex, bounds.getLowerBoundForState(initialStateIndex, explorationInformation), bounds.getUpperBoundForState(initialStateIndex, explorationInformation)); |
|||
} |
|||
|
|||
template<typename ValueType, typename StateType> |
|||
bool SparseExplorationModelChecker<ValueType, StateType>::samplePathFromInitialState(StateGeneration<StateType, ValueType>& stateGeneration, ExplorationInformation<StateType, ValueType>& explorationInformation, StateActionStack& stack, Bounds<StateType, ValueType>& bounds, Statistics<StateType, ValueType>& stats) const { |
|||
// Start the search from the initial state.
|
|||
stack.push_back(std::make_pair(stateGeneration.getFirstInitialState(), 0)); |
|||
|
|||
// As long as we didn't find a terminal (accepting or rejecting) state in the search, sample a new successor.
|
|||
bool foundTerminalState = false; |
|||
while (!foundTerminalState) { |
|||
StateType const& currentStateId = stack.back().first; |
|||
STORM_LOG_TRACE("State on top of stack is: " << currentStateId << "."); |
|||
|
|||
// If the state is not yet explored, we need to retrieve its behaviors.
|
|||
auto unexploredIt = explorationInformation.findUnexploredState(currentStateId); |
|||
if (unexploredIt != explorationInformation.unexploredStatesEnd()) { |
|||
STORM_LOG_TRACE("State was not yet explored."); |
|||
|
|||
// Explore the previously unexplored state.
|
|||
storm::generator::CompressedState const& compressedState = unexploredIt->second; |
|||
foundTerminalState = exploreState(stateGeneration, currentStateId, compressedState, explorationInformation, bounds, stats); |
|||
if (foundTerminalState) { |
|||
STORM_LOG_TRACE("Aborting sampling of path, because a terminal state was reached."); |
|||
} |
|||
explorationInformation.removeUnexploredState(unexploredIt); |
|||
} else { |
|||
// If the state was already explored, we check whether it is a terminal state or not.
|
|||
if (explorationInformation.isTerminal(currentStateId)) { |
|||
STORM_LOG_TRACE("Found already explored terminal state: " << currentStateId << "."); |
|||
foundTerminalState = true; |
|||
} |
|||
} |
|||
|
|||
// Notify the stats about the performed exploration step.
|
|||
stats.explorationStep(); |
|||
|
|||
// If the state was not a terminal state, we continue the path search and sample the next state.
|
|||
if (!foundTerminalState) { |
|||
// At this point, we can be sure that the state was expanded and that we can sample according to the
|
|||
// probabilities in the matrix.
|
|||
uint32_t chosenAction = sampleActionOfState(currentStateId, explorationInformation, bounds); |
|||
stack.back().second = chosenAction; |
|||
STORM_LOG_TRACE("Sampled action " << chosenAction << " in state " << currentStateId << "."); |
|||
|
|||
StateType successor = sampleSuccessorFromAction(chosenAction, explorationInformation, bounds); |
|||
STORM_LOG_TRACE("Sampled successor " << successor << " according to action " << chosenAction << " of state " << currentStateId << "."); |
|||
|
|||
// Put the successor state and a dummy action on top of the stack.
|
|||
stack.emplace_back(successor, 0); |
|||
|
|||
// If the number of exploration steps exceeds a certain threshold, do a precomputation.
|
|||
if (explorationInformation.performPrecomputationExcessiveExplorationSteps(stats.explorationStepsSinceLastPrecomputation)) { |
|||
performPrecomputation(stack, explorationInformation, bounds, stats); |
|||
|
|||
STORM_LOG_TRACE("Aborting the search after precomputation."); |
|||
stack.clear(); |
|||
break; |
|||
} |
|||
} |
|||
} |
|||
|
|||
return foundTerminalState; |
|||
} |
|||
|
|||
template<typename ValueType, typename StateType> |
|||
bool SparseExplorationModelChecker<ValueType, StateType>::exploreState(StateGeneration<StateType, ValueType>& stateGeneration, StateType const& currentStateId, storm::generator::CompressedState const& currentState, ExplorationInformation<StateType, ValueType>& explorationInformation, Bounds<StateType, ValueType>& bounds, Statistics<StateType, ValueType>& stats) const { |
|||
bool isTerminalState = false; |
|||
bool isTargetState = false; |
|||
|
|||
++stats.numberOfExploredStates; |
|||
|
|||
// Finally, map the unexplored state to the row group.
|
|||
explorationInformation.assignStateToNextRowGroup(currentStateId); |
|||
STORM_LOG_TRACE("Assigning row group " << explorationInformation.getRowGroup(currentStateId) << " to state " << currentStateId << "."); |
|||
|
|||
// Initialize the bounds, because some of the following computations depend on the values to be available for
|
|||
// all states that have been assigned to a row-group.
|
|||
bounds.initializeBoundsForNextState(); |
|||
|
|||
// Before generating the behavior of the state, we need to determine whether it's a target state that
|
|||
// does not need to be expanded.
|
|||
stateGeneration.load(currentState); |
|||
if (stateGeneration.isTargetState()) { |
|||
++stats.numberOfTargetStates; |
|||
isTargetState = true; |
|||
isTerminalState = true; |
|||
} else if (stateGeneration.isConditionState()) { |
|||
STORM_LOG_TRACE("Exploring state."); |
|||
|
|||
// If it needs to be expanded, we use the generator to retrieve the behavior of the new state.
|
|||
storm::generator::StateBehavior<ValueType, StateType> behavior = stateGeneration.expand(); |
|||
STORM_LOG_TRACE("State has " << behavior.getNumberOfChoices() << " choices."); |
|||
|
|||
// Clumsily check whether we have found a state that forms a trivial BMEC.
|
|||
bool otherSuccessor = false; |
|||
for (auto const& choice : behavior) { |
|||
for (auto const& entry : choice) { |
|||
if (entry.first != currentStateId) { |
|||
otherSuccessor = true; |
|||
break; |
|||
} |
|||
} |
|||
} |
|||
isTerminalState = !otherSuccessor; |
|||
|
|||
// If the state was neither a trivial (non-accepting) terminal state nor a target state, we
|
|||
// need to store its behavior.
|
|||
if (!isTerminalState) { |
|||
// Next, we insert the behavior into our matrix structure.
|
|||
StateType startAction = explorationInformation.getActionCount(); |
|||
explorationInformation.addActionsToMatrix(behavior.getNumberOfChoices()); |
|||
|
|||
ActionType localAction = 0; |
|||
|
|||
// Retrieve the lowest state bounds (wrt. to the current optimization direction).
|
|||
std::pair<ValueType, ValueType> stateBounds = getLowestBounds(explorationInformation.getOptimizationDirection()); |
|||
|
|||
for (auto const& choice : behavior) { |
|||
for (auto const& entry : choice) { |
|||
explorationInformation.getRowOfMatrix(startAction + localAction).emplace_back(entry.first, entry.second); |
|||
STORM_LOG_TRACE("Found transition " << currentStateId << "-[" << (startAction + localAction) << ", " << entry.second << "]-> " << entry.first << "."); |
|||
} |
|||
|
|||
std::pair<ValueType, ValueType> actionBounds = computeBoundsOfAction(startAction + localAction, explorationInformation, bounds); |
|||
bounds.initializeBoundsForNextAction(actionBounds); |
|||
stateBounds = combineBounds(explorationInformation.getOptimizationDirection(), stateBounds, actionBounds); |
|||
|
|||
STORM_LOG_TRACE("Initializing bounds of action " << (startAction + localAction) << " to " << bounds.getLowerBoundForAction(startAction + localAction) << " and " << bounds.getUpperBoundForAction(startAction + localAction) << "."); |
|||
|
|||
++localAction; |
|||
} |
|||
|
|||
// Terminate the row group.
|
|||
explorationInformation.terminateCurrentRowGroup(); |
|||
|
|||
bounds.setBoundsForState(currentStateId, explorationInformation, stateBounds); |
|||
STORM_LOG_TRACE("Initializing bounds of state " << currentStateId << " to " << bounds.getLowerBoundForState(currentStateId, explorationInformation) << " and " << bounds.getUpperBoundForState(currentStateId, explorationInformation) << "."); |
|||
} |
|||
} else { |
|||
// In this case, the state is neither a target state nor a condition state and therefore a rejecting
|
|||
// terminal state.
|
|||
isTerminalState = true; |
|||
} |
|||
|
|||
if (isTerminalState) { |
|||
STORM_LOG_TRACE("State does not need to be explored, because it is " << (isTargetState ? "a target state" : "a rejecting terminal state") << "."); |
|||
explorationInformation.addTerminalState(currentStateId); |
|||
|
|||
if (isTargetState) { |
|||
bounds.setBoundsForState(currentStateId, explorationInformation, std::make_pair(storm::utility::one<ValueType>(), storm::utility::one<ValueType>())); |
|||
bounds.initializeBoundsForNextAction(std::make_pair(storm::utility::one<ValueType>(), storm::utility::one<ValueType>())); |
|||
} else { |
|||
bounds.setBoundsForState(currentStateId, explorationInformation, std::make_pair(storm::utility::zero<ValueType>(), storm::utility::zero<ValueType>())); |
|||
bounds.initializeBoundsForNextAction(std::make_pair(storm::utility::zero<ValueType>(), storm::utility::zero<ValueType>())); |
|||
} |
|||
|
|||
// Increase the size of the matrix, but leave the row empty.
|
|||
explorationInformation.addActionsToMatrix(1); |
|||
|
|||
// Terminate the row group.
|
|||
explorationInformation.newRowGroup(); |
|||
} |
|||
|
|||
return isTerminalState; |
|||
} |
|||
|
|||
template<typename ValueType, typename StateType> |
|||
typename SparseExplorationModelChecker<ValueType, StateType>::ActionType SparseExplorationModelChecker<ValueType, StateType>::sampleActionOfState(StateType const& currentStateId, ExplorationInformation<StateType, ValueType> const& explorationInformation, Bounds<StateType, ValueType>& bounds) const { |
|||
// Determine the values of all available actions.
|
|||
std::vector<std::pair<ActionType, ValueType>> actionValues; |
|||
StateType rowGroup = explorationInformation.getRowGroup(currentStateId); |
|||
|
|||
// Check for cases in which we do not need to perform more work.
|
|||
if (explorationInformation.onlyOneActionAvailable(rowGroup)) { |
|||
return explorationInformation.getStartRowOfGroup(rowGroup); |
|||
} |
|||
|
|||
// If there are more choices to consider, start by gathering the values of relevant actions.
|
|||
STORM_LOG_TRACE("Sampling from actions leaving the state."); |
|||
|
|||
for (uint32_t row = explorationInformation.getStartRowOfGroup(rowGroup); row < explorationInformation.getStartRowOfGroup(rowGroup + 1); ++row) { |
|||
actionValues.push_back(std::make_pair(row, bounds.getBoundForAction(explorationInformation.getOptimizationDirection(), row))); |
|||
} |
|||
|
|||
STORM_LOG_ASSERT(!actionValues.empty(), "Values for actions must not be empty."); |
|||
|
|||
// Sort the actions wrt. to the optimization direction.
|
|||
if (explorationInformation.maximize()) { |
|||
std::sort(actionValues.begin(), actionValues.end(), [] (std::pair<ActionType, ValueType> const& a, std::pair<ActionType, ValueType> const& b) { return a.second > b.second; } ); |
|||
} else { |
|||
std::sort(actionValues.begin(), actionValues.end(), [] (std::pair<ActionType, ValueType> const& a, std::pair<ActionType, ValueType> const& b) { return a.second < b.second; } ); |
|||
} |
|||
|
|||
// Determine the first elements of the sorted range that agree on their value.
|
|||
auto end = ++actionValues.begin(); |
|||
while (end != actionValues.end() && comparator.isEqual(actionValues.begin()->second, end->second)) { |
|||
++end; |
|||
} |
|||
|
|||
// Now sample from all maximizing actions.
|
|||
std::uniform_int_distribution<ActionType> distribution(0, std::distance(actionValues.begin(), end) - 1); |
|||
return actionValues[distribution(randomGenerator)].first; |
|||
} |
|||
|
|||
template<typename ValueType, typename StateType> |
|||
StateType SparseExplorationModelChecker<ValueType, StateType>::sampleSuccessorFromAction(ActionType const& chosenAction, ExplorationInformation<StateType, ValueType> const& explorationInformation, Bounds<StateType, ValueType> const& bounds) const { |
|||
std::vector<storm::storage::MatrixEntry<StateType, ValueType>> const& row = explorationInformation.getRowOfMatrix(chosenAction); |
|||
if (row.size() == 1) { |
|||
return row.front().getColumn(); |
|||
} |
|||
|
|||
// Depending on the selected next-state heuristic, we give the states other likelihoods of getting chosen.
|
|||
if (explorationInformation.useDifferenceProbabilitySumHeuristic() || explorationInformation.useProbabilityHeuristic()) { |
|||
std::vector<ValueType> probabilities(row.size()); |
|||
if (explorationInformation.useDifferenceProbabilitySumHeuristic()) { |
|||
std::transform(row.begin(), row.end(), probabilities.begin(), |
|||
[&bounds, &explorationInformation] (storm::storage::MatrixEntry<StateType, ValueType> const& entry) { |
|||
return entry.getValue() + bounds.getDifferenceOfStateBounds(entry.getColumn(), explorationInformation); |
|||
}); |
|||
} else if (explorationInformation.useProbabilityHeuristic()) { |
|||
std::transform(row.begin(), row.end(), probabilities.begin(), |
|||
[&bounds, &explorationInformation] (storm::storage::MatrixEntry<StateType, ValueType> const& entry) { |
|||
return entry.getValue(); |
|||
}); |
|||
} |
|||
|
|||
// Now sample according to the probabilities.
|
|||
std::discrete_distribution<StateType> distribution(probabilities.begin(), probabilities.end()); |
|||
return row[distribution(randomGenerator)].getColumn(); |
|||
} else { |
|||
STORM_LOG_ASSERT(explorationInformation.useUniformHeuristic(), "Illegal next-state heuristic."); |
|||
std::uniform_int_distribution<ActionType> distribution(0, row.size() - 1); |
|||
return row[distribution(randomGenerator)].getColumn(); |
|||
} |
|||
} |
|||
|
|||
template<typename ValueType, typename StateType> |
|||
bool SparseExplorationModelChecker<ValueType, StateType>::performPrecomputation(StateActionStack const& stack, ExplorationInformation<StateType, ValueType>& explorationInformation, Bounds<StateType, ValueType>& bounds, Statistics<StateType, ValueType>& stats) const { |
|||
++stats.numberOfPrecomputations; |
|||
|
|||
// Outline:
|
|||
// 1. construct a sparse transition matrix of the relevant part of the state space.
|
|||
// 2. use this matrix to compute states with probability 0/1 and an MEC decomposition (in the max case).
|
|||
// 3. use MEC decomposition to collapse MECs.
|
|||
STORM_LOG_TRACE("Starting " << (explorationInformation.useLocalPrecomputation() ? "local" : "global") << " precomputation."); |
|||
|
|||
// Construct the matrix that represents the fragment of the system contained in the currently sampled path.
|
|||
storm::storage::SparseMatrixBuilder<ValueType> builder(0, 0, 0, false, true, 0); |
|||
|
|||
// Determine the set of states that was expanded.
|
|||
std::vector<StateType> relevantStates; |
|||
if (explorationInformation.useLocalPrecomputation()) { |
|||
for (auto const& stateActionPair : stack) { |
|||
if (explorationInformation.maximize() || !storm::utility::isOne(bounds.getLowerBoundForState(stateActionPair.first, explorationInformation))) { |
|||
relevantStates.push_back(stateActionPair.first); |
|||
} |
|||
} |
|||
std::sort(relevantStates.begin(), relevantStates.end()); |
|||
auto newEnd = std::unique(relevantStates.begin(), relevantStates.end()); |
|||
relevantStates.resize(std::distance(relevantStates.begin(), newEnd)); |
|||
} else { |
|||
for (StateType state = 0; state < explorationInformation.getNumberOfDiscoveredStates(); ++state) { |
|||
// Add the state to the relevant states if they are not unexplored.
|
|||
if (!explorationInformation.isUnexplored(state)) { |
|||
relevantStates.push_back(state); |
|||
} |
|||
} |
|||
} |
|||
StateType sink = relevantStates.size(); |
|||
|
|||
// Create a mapping for faster look-up during the translation of flexible matrix to the real sparse matrix.
|
|||
// While doing so, record all target states.
|
|||
std::unordered_map<StateType, StateType> relevantStateToNewRowGroupMapping; |
|||
storm::storage::BitVector targetStates(sink + 1); |
|||
for (StateType index = 0; index < relevantStates.size(); ++index) { |
|||
relevantStateToNewRowGroupMapping.emplace(relevantStates[index], index); |
|||
if (storm::utility::isOne(bounds.getLowerBoundForState(relevantStates[index], explorationInformation))) { |
|||
targetStates.set(index); |
|||
} |
|||
} |
|||
|
|||
// Do the actual translation.
|
|||
StateType currentRow = 0; |
|||
for (auto const& state : relevantStates) { |
|||
builder.newRowGroup(currentRow); |
|||
StateType rowGroup = explorationInformation.getRowGroup(state); |
|||
for (auto row = explorationInformation.getStartRowOfGroup(rowGroup); row < explorationInformation.getStartRowOfGroup(rowGroup + 1); ++row) { |
|||
ValueType unexpandedProbability = storm::utility::zero<ValueType>(); |
|||
for (auto const& entry : explorationInformation.getRowOfMatrix(row)) { |
|||
auto it = relevantStateToNewRowGroupMapping.find(entry.getColumn()); |
|||
if (it != relevantStateToNewRowGroupMapping.end()) { |
|||
// If the entry is a relevant state, we copy it over (and compensate for the offset change).
|
|||
builder.addNextValue(currentRow, it->second, entry.getValue()); |
|||
} else { |
|||
// If the entry is an unexpanded state, we gather the probability to later redirect it to an unexpanded sink.
|
|||
unexpandedProbability += entry.getValue(); |
|||
} |
|||
} |
|||
if (unexpandedProbability != storm::utility::zero<ValueType>()) { |
|||
builder.addNextValue(currentRow, sink, unexpandedProbability); |
|||
} |
|||
++currentRow; |
|||
} |
|||
} |
|||
// Then, make the unexpanded state absorbing.
|
|||
builder.newRowGroup(currentRow); |
|||
builder.addNextValue(currentRow, sink, storm::utility::one<ValueType>()); |
|||
storm::storage::SparseMatrix<ValueType> relevantStatesMatrix = builder.build(); |
|||
storm::storage::SparseMatrix<ValueType> transposedMatrix = relevantStatesMatrix.transpose(true); |
|||
STORM_LOG_TRACE("Successfully built matrix for precomputation."); |
|||
|
|||
storm::storage::BitVector allStates(sink + 1, true); |
|||
storm::storage::BitVector statesWithProbability0; |
|||
storm::storage::BitVector statesWithProbability1; |
|||
if (explorationInformation.maximize()) { |
|||
// If we are computing maximal probabilities, we first perform a detection of states that have
|
|||
// probability 01 and then additionally perform an MEC decomposition. The reason for this somewhat
|
|||
// duplicate work is the following. Optimally, we would only do the MEC decomposition, because we need
|
|||
// it anyway. However, when only detecting (accepting) MECs, we do not infer which of the other states
|
|||
// (not contained in MECs) also have probability 0/1.
|
|||
statesWithProbability0 = storm::utility::graph::performProb0A(relevantStatesMatrix, relevantStatesMatrix.getRowGroupIndices(), transposedMatrix, allStates, targetStates); |
|||
targetStates.set(sink, true); |
|||
statesWithProbability1 = storm::utility::graph::performProb1E(relevantStatesMatrix, relevantStatesMatrix.getRowGroupIndices(), transposedMatrix, allStates, targetStates); |
|||
|
|||
storm::storage::MaximalEndComponentDecomposition<ValueType> mecDecomposition(relevantStatesMatrix, relevantStatesMatrix.transpose(true)); |
|||
++stats.ecDetections; |
|||
STORM_LOG_TRACE("Successfully computed MEC decomposition. Found " << (mecDecomposition.size() > 1 ? (mecDecomposition.size() - 1) : 0) << " MEC(s)."); |
|||
|
|||
// If the decomposition contains only the MEC consisting of the sink state, we count it as 'failed'.
|
|||
if (mecDecomposition.size() > 1) { |
|||
++stats.failedEcDetections; |
|||
} else { |
|||
stats.totalNumberOfEcDetected += mecDecomposition.size() - 1; |
|||
|
|||
// 3. Analyze the MEC decomposition.
|
|||
for (auto const& mec : mecDecomposition) { |
|||
// Ignore the (expected) MEC of the sink state.
|
|||
if (mec.containsState(sink)) { |
|||
continue; |
|||
} |
|||
|
|||
collapseMec(mec, relevantStates, relevantStatesMatrix, explorationInformation, bounds); |
|||
} |
|||
} |
|||
} else { |
|||
// If we are computing minimal probabilities, we do not need to perform an EC-detection. We rather
|
|||
// compute all states (of the considered fragment) that have probability 0/1. For states with
|
|||
// probability 0, we have to mark the sink as being a target. For states with probability 1, however,
|
|||
// we must treat the sink as being rejecting.
|
|||
targetStates.set(sink, true); |
|||
statesWithProbability0 = storm::utility::graph::performProb0E(relevantStatesMatrix, relevantStatesMatrix.getRowGroupIndices(), transposedMatrix, allStates, targetStates); |
|||
targetStates.set(sink, false); |
|||
statesWithProbability1 = storm::utility::graph::performProb1A(relevantStatesMatrix, relevantStatesMatrix.getRowGroupIndices(), transposedMatrix, allStates, targetStates); |
|||
} |
|||
|
|||
// Set the bounds of the identified states.
|
|||
for (auto state : statesWithProbability0) { |
|||
StateType originalState = relevantStates[state]; |
|||
bounds.setUpperBoundForState(originalState, explorationInformation, storm::utility::zero<ValueType>()); |
|||
explorationInformation.addTerminalState(originalState); |
|||
} |
|||
for (auto state : statesWithProbability1) { |
|||
StateType originalState = relevantStates[state]; |
|||
bounds.setLowerBoundForState(originalState, explorationInformation, storm::utility::one<ValueType>()); |
|||
explorationInformation.addTerminalState(originalState); |
|||
} |
|||
return true; |
|||
} |
|||
|
|||
template<typename ValueType, typename StateType> |
|||
void SparseExplorationModelChecker<ValueType, StateType>::collapseMec(storm::storage::MaximalEndComponent const& mec, std::vector<StateType> const& relevantStates, storm::storage::SparseMatrix<ValueType> const& relevantStatesMatrix, ExplorationInformation<StateType, ValueType>& explorationInformation, Bounds<StateType, ValueType>& bounds) const { |
|||
bool containsTargetState = false; |
|||
|
|||
// Now we record all actions leaving the EC.
|
|||
std::vector<ActionType> leavingActions; |
|||
for (auto const& stateAndChoices : mec) { |
|||
// Compute the state of the original model that corresponds to the current state.
|
|||
StateType originalState = relevantStates[stateAndChoices.first]; |
|||
StateType originalRowGroup = explorationInformation.getRowGroup(originalState); |
|||
|
|||
// Check whether a target state is contained in the MEC.
|
|||
if (!containsTargetState && storm::utility::isOne(bounds.getLowerBoundForRowGroup(originalRowGroup))) { |
|||
containsTargetState = true; |
|||
} |
|||
|
|||
// For each state, compute the actions that leave the MEC.
|
|||
auto includedChoicesIt = stateAndChoices.second.begin(); |
|||
auto includedChoicesIte = stateAndChoices.second.end(); |
|||
for (auto action = explorationInformation.getStartRowOfGroup(originalRowGroup); action < explorationInformation.getStartRowOfGroup(originalRowGroup + 1); ++action) { |
|||
if (includedChoicesIt != includedChoicesIte) { |
|||
STORM_LOG_TRACE("Next (local) choice contained in MEC is " << (*includedChoicesIt - relevantStatesMatrix.getRowGroupIndices()[stateAndChoices.first])); |
|||
STORM_LOG_TRACE("Current (local) choice iterated is " << (action - explorationInformation.getStartRowOfGroup(originalRowGroup))); |
|||
if (action - explorationInformation.getStartRowOfGroup(originalRowGroup) != *includedChoicesIt - relevantStatesMatrix.getRowGroupIndices()[stateAndChoices.first]) { |
|||
STORM_LOG_TRACE("Choice leaves the EC."); |
|||
leavingActions.push_back(action); |
|||
} else { |
|||
STORM_LOG_TRACE("Choice stays in the EC."); |
|||
++includedChoicesIt; |
|||
} |
|||
} else { |
|||
STORM_LOG_TRACE("Choice leaves the EC, because there is no more choice staying in the EC."); |
|||
leavingActions.push_back(action); |
|||
} |
|||
} |
|||
} |
|||
|
|||
// Now, we need to collapse the EC only if it does not contain a target state and the leaving actions are
|
|||
// non-empty, because only then have the states a (potentially) non-zero, non-one probability.
|
|||
if (!containsTargetState && !leavingActions.empty()) { |
|||
// In this case, no target state is contained in the MEC, but there are actions leaving the MEC. To
|
|||
// prevent the simulation getting stuck in this MEC again, we replace all states in the MEC by a new
|
|||
// state whose outgoing actions are the ones leaving the MEC. We do this, by assigning all states in the
|
|||
// MEC to a new row group, which will then hold all the outgoing choices.
|
|||
|
|||
// Remap all contained states to the new row group.
|
|||
StateType nextRowGroup = explorationInformation.getNextRowGroup(); |
|||
for (auto const& stateAndChoices : mec) { |
|||
explorationInformation.assignStateToRowGroup(stateAndChoices.first, nextRowGroup); |
|||
} |
|||
|
|||
bounds.initializeBoundsForNextState(); |
|||
|
|||
// Add to the new row group all leaving actions of contained states and set the appropriate bounds for
|
|||
// the actions and the new state.
|
|||
std::pair<ValueType, ValueType> stateBounds = getLowestBounds(explorationInformation.getOptimizationDirection()); |
|||
for (auto const& action : leavingActions) { |
|||
explorationInformation.moveActionToBackOfMatrix(action); |
|||
std::pair<ValueType, ValueType> const& actionBounds = bounds.getBoundsForAction(action); |
|||
bounds.initializeBoundsForNextAction(actionBounds); |
|||
stateBounds = combineBounds(explorationInformation.getOptimizationDirection(), stateBounds, actionBounds); |
|||
} |
|||
bounds.setBoundsForRowGroup(nextRowGroup, stateBounds); |
|||
|
|||
// Terminate the row group of the newly introduced state.
|
|||
explorationInformation.terminateCurrentRowGroup(); |
|||
} |
|||
} |
|||
|
|||
template<typename ValueType, typename StateType> |
|||
ValueType SparseExplorationModelChecker<ValueType, StateType>::computeLowerBoundOfAction(ActionType const& action, ExplorationInformation<StateType, ValueType> const& explorationInformation, Bounds<StateType, ValueType> const& bounds) const { |
|||
ValueType result = storm::utility::zero<ValueType>(); |
|||
for (auto const& element : explorationInformation.getRowOfMatrix(action)) { |
|||
result += element.getValue() * bounds.getLowerBoundForState(element.getColumn(), explorationInformation); |
|||
} |
|||
return result; |
|||
} |
|||
|
|||
template<typename ValueType, typename StateType> |
|||
ValueType SparseExplorationModelChecker<ValueType, StateType>::computeUpperBoundOfAction(ActionType const& action, ExplorationInformation<StateType, ValueType> const& explorationInformation, Bounds<StateType, ValueType> const& bounds) const { |
|||
ValueType result = storm::utility::zero<ValueType>(); |
|||
for (auto const& element : explorationInformation.getRowOfMatrix(action)) { |
|||
result += element.getValue() * bounds.getUpperBoundForState(element.getColumn(), explorationInformation); |
|||
} |
|||
return result; |
|||
} |
|||
|
|||
template<typename ValueType, typename StateType> |
|||
std::pair<ValueType, ValueType> SparseExplorationModelChecker<ValueType, StateType>::computeBoundsOfAction(ActionType const& action, ExplorationInformation<StateType, ValueType> const& explorationInformation, Bounds<StateType, ValueType> const& bounds) const { |
|||
// TODO: take into account self-loops?
|
|||
std::pair<ValueType, ValueType> result = std::make_pair(storm::utility::zero<ValueType>(), storm::utility::zero<ValueType>()); |
|||
for (auto const& element : explorationInformation.getRowOfMatrix(action)) { |
|||
result.first += element.getValue() * bounds.getLowerBoundForState(element.getColumn(), explorationInformation); |
|||
result.second += element.getValue() * bounds.getUpperBoundForState(element.getColumn(), explorationInformation); |
|||
} |
|||
return result; |
|||
} |
|||
|
|||
template<typename ValueType, typename StateType> |
|||
std::pair<ValueType, ValueType> SparseExplorationModelChecker<ValueType, StateType>::computeBoundsOfState(StateType const& currentStateId, ExplorationInformation<StateType, ValueType> const& explorationInformation, Bounds<StateType, ValueType> const& bounds) const { |
|||
StateType group = explorationInformation.getRowGroup(currentStateId); |
|||
std::pair<ValueType, ValueType> result = getLowestBounds(explorationInformation.getOptimizationDirection()); |
|||
for (ActionType action = explorationInformation.getStartRowOfGroup(group); action < explorationInformation.getStartRowOfGroup(group + 1); ++action) { |
|||
std::pair<ValueType, ValueType> actionValues = computeBoundsOfAction(action, explorationInformation, bounds); |
|||
result = combineBounds(explorationInformation.getOptimizationDirection(), result, actionValues); |
|||
} |
|||
return result; |
|||
} |
|||
|
|||
template<typename ValueType, typename StateType> |
|||
void SparseExplorationModelChecker<ValueType, StateType>::updateProbabilityBoundsAlongSampledPath(StateActionStack& stack, ExplorationInformation<StateType, ValueType> const& explorationInformation, Bounds<StateType, ValueType>& bounds) const { |
|||
stack.pop_back(); |
|||
while (!stack.empty()) { |
|||
updateProbabilityOfAction(stack.back().first, stack.back().second, explorationInformation, bounds); |
|||
stack.pop_back(); |
|||
} |
|||
} |
|||
|
|||
template<typename ValueType, typename StateType> |
|||
void SparseExplorationModelChecker<ValueType, StateType>::updateProbabilityOfAction(StateType const& state, ActionType const& action, ExplorationInformation<StateType, ValueType> const& explorationInformation, Bounds<StateType, ValueType>& bounds) const { |
|||
// Compute the new lower/upper values of the action.
|
|||
std::pair<ValueType, ValueType> newBoundsForAction = computeBoundsOfAction(action, explorationInformation, bounds); |
|||
|
|||
// And set them as the current value.
|
|||
bounds.setBoundsForAction(action, newBoundsForAction); |
|||
|
|||
// Check if we need to update the values for the states.
|
|||
if (explorationInformation.maximize()) { |
|||
bounds.setLowerBoundOfStateIfGreaterThanOld(state, explorationInformation, newBoundsForAction.first); |
|||
|
|||
StateType rowGroup = explorationInformation.getRowGroup(state); |
|||
if (newBoundsForAction.second < bounds.getUpperBoundForRowGroup(rowGroup)) { |
|||
if (explorationInformation.getRowGroupSize(rowGroup) > 1) { |
|||
newBoundsForAction.second = std::max(newBoundsForAction.second, computeBoundOverAllOtherActions(storm::OptimizationDirection::Maximize, state, action, explorationInformation, bounds)); |
|||
} |
|||
|
|||
bounds.setUpperBoundForRowGroup(rowGroup, newBoundsForAction.second); |
|||
} |
|||
} else { |
|||
bounds.setUpperBoundOfStateIfLessThanOld(state, explorationInformation, newBoundsForAction.second); |
|||
|
|||
StateType rowGroup = explorationInformation.getRowGroup(state); |
|||
if (bounds.getLowerBoundForRowGroup(rowGroup) < newBoundsForAction.first) { |
|||
if (explorationInformation.getRowGroupSize(rowGroup) > 1) { |
|||
ValueType min = computeBoundOverAllOtherActions(storm::OptimizationDirection::Minimize, state, action, explorationInformation, bounds); |
|||
newBoundsForAction.first = std::min(newBoundsForAction.first, min); |
|||
} |
|||
|
|||
bounds.setLowerBoundForRowGroup(rowGroup, newBoundsForAction.first); |
|||
} |
|||
} |
|||
} |
|||
|
|||
template<typename ValueType, typename StateType> |
|||
ValueType SparseExplorationModelChecker<ValueType, StateType>::computeBoundOverAllOtherActions(storm::OptimizationDirection const& direction, StateType const& state, ActionType const& action, ExplorationInformation<StateType, ValueType> const& explorationInformation, Bounds<StateType, ValueType> const& bounds) const { |
|||
ValueType bound = getLowestBound(explorationInformation.getOptimizationDirection()); |
|||
|
|||
ActionType group = explorationInformation.getRowGroup(state); |
|||
for (auto currentAction = explorationInformation.getStartRowOfGroup(group); currentAction < explorationInformation.getStartRowOfGroup(group + 1); ++currentAction) { |
|||
if (currentAction == action) { |
|||
continue; |
|||
} |
|||
|
|||
if (direction == storm::OptimizationDirection::Maximize) { |
|||
bound = std::max(bound, computeUpperBoundOfAction(currentAction, explorationInformation, bounds)); |
|||
} else { |
|||
bound = std::min(bound, computeLowerBoundOfAction(currentAction, explorationInformation, bounds)); |
|||
} |
|||
} |
|||
return bound; |
|||
} |
|||
|
|||
template<typename ValueType, typename StateType> |
|||
std::pair<ValueType, ValueType> SparseExplorationModelChecker<ValueType, StateType>::getLowestBounds(storm::OptimizationDirection const& direction) const { |
|||
ValueType val = getLowestBound(direction); |
|||
return std::make_pair(val, val); |
|||
} |
|||
|
|||
template<typename ValueType, typename StateType> |
|||
ValueType SparseExplorationModelChecker<ValueType, StateType>::getLowestBound(storm::OptimizationDirection const& direction) const { |
|||
if (direction == storm::OptimizationDirection::Maximize) { |
|||
return storm::utility::zero<ValueType>(); |
|||
} else { |
|||
return storm::utility::one<ValueType>(); |
|||
} |
|||
} |
|||
|
|||
template<typename ValueType, typename StateType> |
|||
std::pair<ValueType, ValueType> SparseExplorationModelChecker<ValueType, StateType>::combineBounds(storm::OptimizationDirection const& direction, std::pair<ValueType, ValueType> const& bounds1, std::pair<ValueType, ValueType> const& bounds2) const { |
|||
if (direction == storm::OptimizationDirection::Maximize) { |
|||
return std::make_pair(std::max(bounds1.first, bounds2.first), std::max(bounds1.second, bounds2.second)); |
|||
} else { |
|||
return std::make_pair(std::min(bounds1.first, bounds2.first), std::min(bounds1.second, bounds2.second)); |
|||
} |
|||
} |
|||
|
|||
template class SparseExplorationModelChecker<double, uint32_t>; |
|||
} |
|||
} |
|||
@ -0,0 +1,89 @@ |
|||
#ifndef STORM_MODELCHECKER_EXPLORATION_SPARSEEXPLORATIONMODELCHECKER_H_ |
|||
#define STORM_MODELCHECKER_EXPLORATION_SPARSEEXPLORATIONMODELCHECKER_H_ |
|||
|
|||
#include <random> |
|||
|
|||
#include "src/modelchecker/AbstractModelChecker.h" |
|||
|
|||
#include "src/storage/prism/Program.h" |
|||
|
|||
#include "src/generator/CompressedState.h" |
|||
#include "src/generator/VariableInformation.h" |
|||
|
|||
#include "src/utility/ConstantsComparator.h" |
|||
|
|||
namespace storm { |
|||
namespace storage { |
|||
class MaximalEndComponent; |
|||
} |
|||
namespace prism { |
|||
class Program; |
|||
} |
|||
|
|||
namespace modelchecker { |
|||
namespace exploration_detail { |
|||
template <typename StateType, typename ValueType> class StateGeneration; |
|||
template <typename StateType, typename ValueType> class ExplorationInformation; |
|||
template <typename StateType, typename ValueType> class Bounds; |
|||
template <typename StateType, typename ValueType> class Statistics; |
|||
} |
|||
|
|||
using namespace exploration_detail; |
|||
|
|||
template<typename ValueType, typename StateType = uint32_t> |
|||
class SparseExplorationModelChecker : public AbstractModelChecker { |
|||
public: |
|||
typedef StateType ActionType; |
|||
typedef std::vector<std::pair<StateType, ActionType>> StateActionStack; |
|||
|
|||
SparseExplorationModelChecker(storm::prism::Program const& program, boost::optional<std::map<storm::expressions::Variable, storm::expressions::Expression>> const& constantDefinitions = boost::none); |
|||
|
|||
virtual bool canHandle(CheckTask<storm::logic::Formula> const& checkTask) const override; |
|||
|
|||
virtual std::unique_ptr<CheckResult> computeUntilProbabilities(CheckTask<storm::logic::UntilFormula> const& checkTask) override; |
|||
|
|||
private: |
|||
std::tuple<StateType, ValueType, ValueType> performExploration(StateGeneration<StateType, ValueType>& stateGeneration, ExplorationInformation<StateType, ValueType>& explorationInformation) const; |
|||
|
|||
bool samplePathFromInitialState(StateGeneration<StateType, ValueType>& stateGeneration, ExplorationInformation<StateType, ValueType>& explorationInformation, StateActionStack& stack, Bounds<StateType, ValueType>& bounds, Statistics<StateType, ValueType>& stats) const; |
|||
|
|||
bool exploreState(StateGeneration<StateType, ValueType>& stateGeneration, StateType const& currentStateId, storm::generator::CompressedState const& currentState, ExplorationInformation<StateType, ValueType>& explorationInformation, Bounds<StateType, ValueType>& bounds, Statistics<StateType, ValueType>& stats) const; |
|||
|
|||
ActionType sampleActionOfState(StateType const& currentStateId, ExplorationInformation<StateType, ValueType> const& explorationInformation, Bounds<StateType, ValueType>& bounds) const; |
|||
|
|||
StateType sampleSuccessorFromAction(ActionType const& chosenAction, ExplorationInformation<StateType, ValueType> const& explorationInformation, Bounds<StateType, ValueType> const& bounds) const; |
|||
|
|||
bool performPrecomputation(StateActionStack const& stack, ExplorationInformation<StateType, ValueType>& explorationInformation, Bounds<StateType, ValueType>& bounds, Statistics<StateType, ValueType>& stats) const; |
|||
|
|||
void collapseMec(storm::storage::MaximalEndComponent const& mec, std::vector<StateType> const& relevantStates, storm::storage::SparseMatrix<ValueType> const& relevantStatesMatrix, ExplorationInformation<StateType, ValueType>& explorationInformation, Bounds<StateType, ValueType>& bounds) const; |
|||
|
|||
void updateProbabilityBoundsAlongSampledPath(StateActionStack& stack, ExplorationInformation<StateType, ValueType> const& explorationInformation, Bounds<StateType, ValueType>& bounds) const; |
|||
|
|||
void updateProbabilityOfAction(StateType const& state, ActionType const& action, ExplorationInformation<StateType, ValueType> const& explorationInformation, Bounds<StateType, ValueType>& bounds) const; |
|||
|
|||
std::pair<ValueType, ValueType> computeBoundsOfAction(ActionType const& action, ExplorationInformation<StateType, ValueType> const& explorationInformation, Bounds<StateType, ValueType> const& bounds) const; |
|||
ValueType computeBoundOverAllOtherActions(storm::OptimizationDirection const& direction, StateType const& state, ActionType const& action, ExplorationInformation<StateType, ValueType> const& explorationInformation, Bounds<StateType, ValueType> const& bounds) const; |
|||
std::pair<ValueType, ValueType> computeBoundsOfState(StateType const& currentStateId, ExplorationInformation<StateType, ValueType> const& explorationInformation, Bounds<StateType, ValueType> const& bounds) const; |
|||
ValueType computeLowerBoundOfAction(ActionType const& action, ExplorationInformation<StateType, ValueType> const& explorationInformation, Bounds<StateType, ValueType> const& bounds) const; |
|||
ValueType computeUpperBoundOfAction(ActionType const& action, ExplorationInformation<StateType, ValueType> const& explorationInformation, Bounds<StateType, ValueType> const& bounds) const; |
|||
|
|||
std::pair<ValueType, ValueType> getLowestBounds(storm::OptimizationDirection const& direction) const; |
|||
ValueType getLowestBound(storm::OptimizationDirection const& direction) const; |
|||
std::pair<ValueType, ValueType> combineBounds(storm::OptimizationDirection const& direction, std::pair<ValueType, ValueType> const& bounds1, std::pair<ValueType, ValueType> const& bounds2) const; |
|||
|
|||
// The program that defines the model to check. |
|||
storm::prism::Program program; |
|||
|
|||
// The variable information. |
|||
storm::generator::VariableInformation variableInformation; |
|||
|
|||
// The random number generator. |
|||
mutable std::default_random_engine randomGenerator; |
|||
|
|||
// A comparator used to determine whether values are equal. |
|||
storm::utility::ConstantsComparator<ValueType> comparator; |
|||
}; |
|||
} |
|||
} |
|||
|
|||
#endif /* STORM_MODELCHECKER_EXPLORATION_SPARSEEXPLORATIONMODELCHECKER_H_ */ |
|||
@ -0,0 +1,69 @@ |
|||
#include "src/modelchecker/exploration/StateGeneration.h"
|
|||
|
|||
#include "src/modelchecker/exploration/ExplorationInformation.h"
|
|||
|
|||
namespace storm { |
|||
namespace modelchecker { |
|||
namespace exploration_detail { |
|||
|
|||
template <typename StateType, typename ValueType> |
|||
StateGeneration<StateType, ValueType>::StateGeneration(storm::prism::Program const& program, storm::generator::VariableInformation const& variableInformation, ExplorationInformation<StateType, ValueType>& explorationInformation, storm::expressions::Expression const& conditionStateExpression, storm::expressions::Expression const& targetStateExpression) : generator(program, variableInformation, false), stateStorage(variableInformation.getTotalBitOffset(true)), conditionStateExpression(conditionStateExpression), targetStateExpression(targetStateExpression) { |
|||
|
|||
stateToIdCallback = [&explorationInformation, this] (storm::generator::CompressedState const& state) -> StateType { |
|||
StateType newIndex = stateStorage.getNumberOfStates(); |
|||
|
|||
// Check, if the state was already registered.
|
|||
std::pair<StateType, std::size_t> actualIndexBucketPair = stateStorage.stateToId.findOrAddAndGetBucket(state, newIndex); |
|||
|
|||
if (actualIndexBucketPair.first == newIndex) { |
|||
explorationInformation.addUnexploredState(newIndex, state); |
|||
} |
|||
|
|||
return actualIndexBucketPair.first; |
|||
}; |
|||
} |
|||
|
|||
template <typename StateType, typename ValueType> |
|||
void StateGeneration<StateType, ValueType>::load(storm::generator::CompressedState const& state) { |
|||
generator.load(state); |
|||
} |
|||
|
|||
template <typename StateType, typename ValueType> |
|||
std::vector<StateType> StateGeneration<StateType, ValueType>::getInitialStates() { |
|||
return stateStorage.initialStateIndices; |
|||
} |
|||
|
|||
template <typename StateType, typename ValueType> |
|||
storm::generator::StateBehavior<ValueType, StateType> StateGeneration<StateType, ValueType>::expand() { |
|||
return generator.expand(stateToIdCallback); |
|||
} |
|||
|
|||
template <typename StateType, typename ValueType> |
|||
bool StateGeneration<StateType, ValueType>::isConditionState() const { |
|||
return generator.satisfies(conditionStateExpression); |
|||
} |
|||
|
|||
template <typename StateType, typename ValueType> |
|||
bool StateGeneration<StateType, ValueType>::isTargetState() const { |
|||
return generator.satisfies(targetStateExpression); |
|||
} |
|||
|
|||
template<typename StateType, typename ValueType> |
|||
void StateGeneration<StateType, ValueType>::computeInitialStates() { |
|||
stateStorage.initialStateIndices = generator.getInitialStates(stateToIdCallback); |
|||
} |
|||
|
|||
template<typename StateType, typename ValueType> |
|||
StateType StateGeneration<StateType, ValueType>::getFirstInitialState() const { |
|||
return stateStorage.initialStateIndices.front(); |
|||
} |
|||
|
|||
template<typename StateType, typename ValueType> |
|||
std::size_t StateGeneration<StateType, ValueType>::getNumberOfInitialStates() const { |
|||
return stateStorage.initialStateIndices.size(); |
|||
} |
|||
|
|||
template class StateGeneration<uint32_t, double>; |
|||
} |
|||
} |
|||
} |
|||
@ -0,0 +1,56 @@ |
|||
#ifndef STORM_MODELCHECKER_EXPLORATION_EXPLORATION_DETAIL_STATEGENERATION_H_ |
|||
#define STORM_MODELCHECKER_EXPLORATION_EXPLORATION_DETAIL_STATEGENERATION_H_ |
|||
|
|||
#include "src/generator/CompressedState.h" |
|||
#include "src/generator/PrismNextStateGenerator.h" |
|||
|
|||
#include "src/storage/sparse/StateStorage.h" |
|||
|
|||
namespace storm { |
|||
namespace generator { |
|||
template<typename ValueType, typename StateType> |
|||
class PrismNextStateGenerator; |
|||
} |
|||
|
|||
namespace modelchecker { |
|||
namespace exploration_detail { |
|||
|
|||
template <typename StateType, typename ValueType> |
|||
class ExplorationInformation; |
|||
|
|||
template <typename StateType, typename ValueType> |
|||
class StateGeneration { |
|||
public: |
|||
StateGeneration(storm::prism::Program const& program, storm::generator::VariableInformation const& variableInformation, ExplorationInformation<StateType, ValueType>& explorationInformation, storm::expressions::Expression const& conditionStateExpression, storm::expressions::Expression const& targetStateExpression); |
|||
|
|||
void load(storm::generator::CompressedState const& state); |
|||
|
|||
std::vector<StateType> getInitialStates(); |
|||
|
|||
storm::generator::StateBehavior<ValueType, StateType> expand(); |
|||
|
|||
void computeInitialStates(); |
|||
|
|||
StateType getFirstInitialState() const; |
|||
|
|||
std::size_t getNumberOfInitialStates() const; |
|||
|
|||
bool isConditionState() const; |
|||
|
|||
bool isTargetState() const; |
|||
|
|||
private: |
|||
storm::generator::PrismNextStateGenerator<ValueType, StateType> generator; |
|||
std::function<StateType (storm::generator::CompressedState const&)> stateToIdCallback; |
|||
|
|||
storm::storage::sparse::StateStorage<StateType> stateStorage; |
|||
|
|||
storm::expressions::Expression conditionStateExpression; |
|||
storm::expressions::Expression targetStateExpression; |
|||
}; |
|||
|
|||
} |
|||
} |
|||
} |
|||
|
|||
#endif /* STORM_MODELCHECKER_EXPLORATION_EXPLORATION_DETAIL_STATEGENERATION_H_ */ |
|||
@ -0,0 +1,46 @@ |
|||
#include "src/modelchecker/exploration/Statistics.h"
|
|||
|
|||
#include "src/modelchecker/exploration/ExplorationInformation.h"
|
|||
|
|||
namespace storm { |
|||
namespace modelchecker { |
|||
namespace exploration_detail { |
|||
|
|||
template<typename StateType, typename ValueType> |
|||
Statistics<StateType, ValueType>::Statistics() : pathsSampled(0), pathsSampledSinceLastPrecomputation(0), explorationSteps(0), explorationStepsSinceLastPrecomputation(0), maxPathLength(0), numberOfTargetStates(0), numberOfExploredStates(0), numberOfPrecomputations(0), ecDetections(0), failedEcDetections(0), totalNumberOfEcDetected(0) { |
|||
// Intentionally left empty.
|
|||
} |
|||
|
|||
template<typename StateType, typename ValueType> |
|||
void Statistics<StateType, ValueType>::explorationStep() { |
|||
++explorationSteps; |
|||
++explorationStepsSinceLastPrecomputation; |
|||
} |
|||
|
|||
template<typename StateType, typename ValueType> |
|||
void Statistics<StateType, ValueType>::sampledPath() { |
|||
++pathsSampled; |
|||
++pathsSampledSinceLastPrecomputation; |
|||
} |
|||
|
|||
template<typename StateType, typename ValueType> |
|||
void Statistics<StateType, ValueType>::updateMaxPathLength(std::size_t const& currentPathLength) { |
|||
maxPathLength = std::max(maxPathLength, currentPathLength); |
|||
} |
|||
|
|||
template<typename StateType, typename ValueType> |
|||
void Statistics<StateType, ValueType>::printToStream(std::ostream& out, ExplorationInformation<StateType, ValueType> const& explorationInformation) const { |
|||
out << std::endl << "Exploration statistics:" << std::endl; |
|||
out << "Discovered states: " << explorationInformation.getNumberOfDiscoveredStates() << " (" << numberOfExploredStates << " explored, " << explorationInformation.getNumberOfUnexploredStates() << " unexplored, " << numberOfTargetStates << " target)" << std::endl; |
|||
out << "Exploration steps: " << explorationSteps << std::endl; |
|||
out << "Sampled paths: " << pathsSampled << std::endl; |
|||
out << "Maximal path length: " << maxPathLength << std::endl; |
|||
out << "Precomputations: " << numberOfPrecomputations << std::endl; |
|||
out << "EC detections: " << ecDetections << " (" << failedEcDetections << " failed, " << totalNumberOfEcDetected << " EC(s) detected)" << std::endl; |
|||
} |
|||
|
|||
template class Statistics<uint32_t, double>; |
|||
|
|||
} |
|||
} |
|||
} |
|||
@ -0,0 +1,44 @@ |
|||
#ifndef STORM_MODELCHECKER_EXPLORATION_EXPLORATION_DETAIL_STATISTICS_H_ |
|||
#define STORM_MODELCHECKER_EXPLORATION_EXPLORATION_DETAIL_STATISTICS_H_ |
|||
|
|||
#include <cstddef> |
|||
#include <iostream> |
|||
|
|||
namespace storm { |
|||
namespace modelchecker { |
|||
namespace exploration_detail { |
|||
|
|||
template<typename StateType, typename ValueType> |
|||
class ExplorationInformation; |
|||
|
|||
// A struct that keeps track of certain statistics during the exploration. |
|||
template<typename StateType, typename ValueType> |
|||
struct Statistics { |
|||
Statistics(); |
|||
|
|||
void explorationStep(); |
|||
|
|||
void sampledPath(); |
|||
|
|||
void updateMaxPathLength(std::size_t const& currentPathLength); |
|||
|
|||
void printToStream(std::ostream& out, ExplorationInformation<StateType, ValueType> const& explorationInformation) const; |
|||
|
|||
std::size_t pathsSampled; |
|||
std::size_t pathsSampledSinceLastPrecomputation; |
|||
std::size_t explorationSteps; |
|||
std::size_t explorationStepsSinceLastPrecomputation; |
|||
std::size_t maxPathLength; |
|||
std::size_t numberOfTargetStates; |
|||
std::size_t numberOfExploredStates; |
|||
std::size_t numberOfPrecomputations; |
|||
std::size_t ecDetections; |
|||
std::size_t failedEcDetections; |
|||
std::size_t totalNumberOfEcDetected; |
|||
}; |
|||
|
|||
} |
|||
} |
|||
} |
|||
|
|||
#endif /* STORM_MODELCHECKER_EXPLORATION_EXPLORATION_DETAIL_STATISTICS_H_ */ |
|||
@ -1,16 +1,19 @@ |
|||
#ifndef STORM_STATEANNOTATION_H |
|||
#define STORM_STATEANNOTATION_H |
|||
#ifndef STORM_MODELS_SPARSE_STATEANNOTATION_H_ |
|||
#define STORM_MODELS_SPARSE_STATEANNOTATION_H_ |
|||
|
|||
#include "src/storage/sparse/StateType.h" |
|||
|
|||
namespace storm { |
|||
namespace models { |
|||
namespace sparse { |
|||
|
|||
class StateAnnotation { |
|||
public: |
|||
virtual std::string stateInfo(uint_fast64_t s) const = 0; |
|||
virtual std::string stateInfo(storm::storage::sparse::state_type const& state) const = 0; |
|||
}; |
|||
|
|||
} |
|||
} |
|||
|
|||
} |
|||
|
|||
#endif //STORM_STATEANNOTATION_H |
|||
#endif /* STORM_MODELS_SPARSE_STATEANNOTATION_H_ */ |
|||
@ -0,0 +1,96 @@ |
|||
#include "src/settings/modules/ExplorationSettings.h"
|
|||
#include "src/settings/modules/GeneralSettings.h"
|
|||
#include "src/settings/Option.h"
|
|||
#include "src/settings/OptionBuilder.h"
|
|||
#include "src/settings/ArgumentBuilder.h"
|
|||
#include "src/settings/Argument.h"
|
|||
#include "src/settings/SettingsManager.h"
|
|||
|
|||
namespace storm { |
|||
namespace settings { |
|||
namespace modules { |
|||
|
|||
const std::string ExplorationSettings::moduleName = "exploration"; |
|||
const std::string ExplorationSettings::precomputationTypeOptionName = "precomp"; |
|||
const std::string ExplorationSettings::numberOfExplorationStepsUntilPrecomputationOptionName = "stepsprecomp"; |
|||
const std::string ExplorationSettings::numberOfSampledPathsUntilPrecomputationOptionName = "pathsprecomp"; |
|||
const std::string ExplorationSettings::nextStateHeuristicOptionName = "nextstate"; |
|||
const std::string ExplorationSettings::precisionOptionName = "precision"; |
|||
const std::string ExplorationSettings::precisionOptionShortName = "eps"; |
|||
|
|||
ExplorationSettings::ExplorationSettings(storm::settings::SettingsManager& settingsManager) : ModuleSettings(settingsManager, moduleName) { |
|||
std::vector<std::string> types = { "local", "global" }; |
|||
this->addOption(storm::settings::OptionBuilder(moduleName, precomputationTypeOptionName, true, "Sets the kind of precomputation used. Available are: { local, global }.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the type to use.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(types)).setDefaultValueString("global").build()).build()); |
|||
this->addOption(storm::settings::OptionBuilder(moduleName, numberOfExplorationStepsUntilPrecomputationOptionName, true, "Sets the number of exploration steps to perform until a precomputation is triggered.").addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("count", "The number of exploration steps to perform.").setDefaultValueUnsignedInteger(100000).build()).build()); |
|||
this->addOption(storm::settings::OptionBuilder(moduleName, numberOfSampledPathsUntilPrecomputationOptionName, true, "If set, a precomputation is perfomed periodically after the given number of paths has been sampled.").addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("count", "The number of paths to sample until a precomputation is triggered.").setDefaultValueUnsignedInteger(100000).build()).build()); |
|||
|
|||
std::vector<std::string> nextStateHeuristics = { "probdiffs", "prob", "unif" }; |
|||
this->addOption(storm::settings::OptionBuilder(moduleName, nextStateHeuristicOptionName, true, "Sets the next-state heuristic to use. Available are: { probdiffs, prob, unif } where 'prob' samples according to the probabilities in the system, 'probdiffs' takes into account probabilities and the differences between the current bounds and 'unif' samples uniformly.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the heuristic to use.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(nextStateHeuristics)).setDefaultValueString("probdiffs").build()).build()); |
|||
|
|||
this->addOption(storm::settings::OptionBuilder(moduleName, precisionOptionName, false, "The internally used precision.").setShortName(precisionOptionShortName) |
|||
.addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("value", "The precision to use.").setDefaultValueDouble(1e-06).addValidationFunctionDouble(storm::settings::ArgumentValidators::doubleRangeValidatorExcluding(0.0, 1.0)).build()).build()); |
|||
} |
|||
|
|||
bool ExplorationSettings::isLocalPrecomputationSet() const { |
|||
if (this->getOption(precomputationTypeOptionName).getArgumentByName("name").getValueAsString() == "local") { |
|||
return true; |
|||
} |
|||
return false; |
|||
} |
|||
|
|||
bool ExplorationSettings::isGlobalPrecomputationSet() const { |
|||
if (this->getOption(precomputationTypeOptionName).getArgumentByName("name").getValueAsString() == "global") { |
|||
return true; |
|||
} |
|||
return false; |
|||
} |
|||
|
|||
ExplorationSettings::PrecomputationType ExplorationSettings::getPrecomputationType() const { |
|||
std::string typeAsString = this->getOption(precomputationTypeOptionName).getArgumentByName("name").getValueAsString(); |
|||
if (typeAsString == "local") { |
|||
return ExplorationSettings::PrecomputationType::Local; |
|||
} else if (typeAsString == "global") { |
|||
return ExplorationSettings::PrecomputationType::Global; |
|||
} |
|||
STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown precomputation type '" << typeAsString << "'."); |
|||
} |
|||
|
|||
uint_fast64_t ExplorationSettings::getNumberOfExplorationStepsUntilPrecomputation() const { |
|||
return this->getOption(numberOfExplorationStepsUntilPrecomputationOptionName).getArgumentByName("count").getValueAsUnsignedInteger(); |
|||
} |
|||
|
|||
bool ExplorationSettings::isNumberOfSampledPathsUntilPrecomputationSet() const { |
|||
return this->getOption(numberOfSampledPathsUntilPrecomputationOptionName).getHasOptionBeenSet(); |
|||
} |
|||
|
|||
uint_fast64_t ExplorationSettings::getNumberOfSampledPathsUntilPrecomputation() const { |
|||
return this->getOption(numberOfSampledPathsUntilPrecomputationOptionName).getArgumentByName("count").getValueAsUnsignedInteger(); |
|||
} |
|||
|
|||
ExplorationSettings::NextStateHeuristic ExplorationSettings::getNextStateHeuristic() const { |
|||
std::string nextStateHeuristicAsString = this->getOption(nextStateHeuristicOptionName).getArgumentByName("name").getValueAsString(); |
|||
if (nextStateHeuristicAsString == "probdiffs") { |
|||
return ExplorationSettings::NextStateHeuristic::DifferenceProbabilitySum; |
|||
} else if (nextStateHeuristicAsString == "prob") { |
|||
return ExplorationSettings::NextStateHeuristic::Probability; |
|||
} else if (nextStateHeuristicAsString == "unif") { |
|||
return ExplorationSettings::NextStateHeuristic::Uniform; |
|||
} |
|||
STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown next-state heuristic '" << nextStateHeuristicAsString << "'."); |
|||
} |
|||
|
|||
double ExplorationSettings::getPrecision() const { |
|||
return this->getOption(precisionOptionName).getArgumentByName("value").getValueAsDouble(); |
|||
} |
|||
|
|||
bool ExplorationSettings::check() const { |
|||
bool optionsSet = this->getOption(precomputationTypeOptionName).getHasOptionBeenSet() || |
|||
this->getOption(numberOfExplorationStepsUntilPrecomputationOptionName).getHasOptionBeenSet() || |
|||
this->getOption(numberOfSampledPathsUntilPrecomputationOptionName).getHasOptionBeenSet() || |
|||
this->getOption(nextStateHeuristicOptionName).getHasOptionBeenSet(); |
|||
STORM_LOG_WARN_COND(storm::settings::generalSettings().getEngine() == storm::settings::modules::GeneralSettings::Engine::Exploration || !optionsSet, "Exploration engine is not selected, so setting options for it has no effect."); |
|||
return true; |
|||
} |
|||
} // namespace modules
|
|||
} // namespace settings
|
|||
} // namespace storm
|
|||
@ -0,0 +1,102 @@ |
|||
#ifndef STORM_SETTINGS_MODULES_EXPLORATIONSETTINGS_H_ |
|||
#define STORM_SETTINGS_MODULES_EXPLORATIONSETTINGS_H_ |
|||
|
|||
#include "src/settings/modules/ModuleSettings.h" |
|||
|
|||
namespace storm { |
|||
namespace settings { |
|||
namespace modules { |
|||
|
|||
/*! |
|||
* This class represents the exploration settings. |
|||
*/ |
|||
class ExplorationSettings : public ModuleSettings { |
|||
public: |
|||
// An enumeration of all available precomputation types. |
|||
enum class PrecomputationType { Local, Global }; |
|||
|
|||
// The available heuristics to choose the next state. |
|||
enum class NextStateHeuristic { DifferenceProbabilitySum, Probability, Uniform }; |
|||
|
|||
/*! |
|||
* Creates a new set of exploration settings that is managed by the given manager. |
|||
* |
|||
* @param settingsManager The responsible manager. |
|||
*/ |
|||
ExplorationSettings(storm::settings::SettingsManager& settingsManager); |
|||
|
|||
/*! |
|||
* Retrieves whether local precomputation is to be used. |
|||
* |
|||
* @return True iff local precomputation is to be used. |
|||
*/ |
|||
bool isLocalPrecomputationSet() const; |
|||
|
|||
/*! |
|||
* Retrieves whether global precomputation is to be used. |
|||
* |
|||
* @return True iff global precomputation is to be used. |
|||
*/ |
|||
bool isGlobalPrecomputationSet() const; |
|||
|
|||
/*! |
|||
* Retrieves the selected precomputation type. |
|||
* |
|||
* @return The selected precomputation type. |
|||
*/ |
|||
PrecomputationType getPrecomputationType() const; |
|||
|
|||
/*! |
|||
* Retrieves the number of exploration steps to perform until a precomputation is triggered. |
|||
* |
|||
* @return The number of exploration steps to perform until a precomputation is triggered. |
|||
*/ |
|||
uint_fast64_t getNumberOfExplorationStepsUntilPrecomputation() const; |
|||
|
|||
/* |
|||
* Retrieves whether the option to perform a precomputation after a given number of sampled paths was set. |
|||
* |
|||
* @return True iff a precomputation after a given number of sampled paths is to be performed. |
|||
*/ |
|||
bool isNumberOfSampledPathsUntilPrecomputationSet() const; |
|||
|
|||
/*! |
|||
* Retrieves the number of paths to sample until a precomputation is triggered. |
|||
* |
|||
* @return The the number of paths to sample until a precomputation is triggered. |
|||
*/ |
|||
uint_fast64_t getNumberOfSampledPathsUntilPrecomputation() const; |
|||
|
|||
/*! |
|||
* Retrieves the selected next-state heuristic. |
|||
* |
|||
* @return The selected next-state heuristic. |
|||
*/ |
|||
NextStateHeuristic getNextStateHeuristic() const; |
|||
|
|||
/*! |
|||
* Retrieves the precision to use for numerical operations. |
|||
* |
|||
* @return The precision to use for numerical operations. |
|||
*/ |
|||
double getPrecision() const; |
|||
|
|||
virtual bool check() const override; |
|||
|
|||
// The name of the module. |
|||
static const std::string moduleName; |
|||
|
|||
private: |
|||
// Define the string names of the options as constants. |
|||
static const std::string precomputationTypeOptionName; |
|||
static const std::string numberOfExplorationStepsUntilPrecomputationOptionName; |
|||
static const std::string numberOfSampledPathsUntilPrecomputationOptionName; |
|||
static const std::string nextStateHeuristicOptionName; |
|||
static const std::string precisionOptionName; |
|||
static const std::string precisionOptionShortName; |
|||
}; |
|||
} // namespace modules |
|||
} // namespace settings |
|||
} // namespace storm |
|||
|
|||
#endif /* STORM_SETTINGS_MODULES_EXPLORATIONSETTINGS_H_ */ |
|||
@ -0,0 +1,20 @@ |
|||
#include "src/storage/sparse/StateStorage.h"
|
|||
|
|||
namespace storm { |
|||
namespace storage { |
|||
namespace sparse { |
|||
|
|||
template <typename StateType> |
|||
StateStorage<StateType>::StateStorage(uint64_t bitsPerState) : stateToId(bitsPerState, 10000000), initialStateIndices(), bitsPerState(bitsPerState) { |
|||
// Intentionally left empty.
|
|||
} |
|||
|
|||
template <typename StateType> |
|||
uint_fast64_t StateStorage<StateType>::getNumberOfStates() const { |
|||
return stateToId.size(); |
|||
} |
|||
|
|||
template class StateStorage<uint32_t>; |
|||
} |
|||
} |
|||
} |
|||
@ -0,0 +1,35 @@ |
|||
#ifndef STORM_STORAGE_SPARSE_STATESTORAGE_H_ |
|||
#define STORM_STORAGE_SPARSE_STATESTORAGE_H_ |
|||
|
|||
#include <cstdint> |
|||
|
|||
#include "src/storage/BitVectorHashMap.h" |
|||
|
|||
namespace storm { |
|||
namespace storage { |
|||
namespace sparse { |
|||
|
|||
// A structure holding information about the reachable state space while building it. |
|||
template <typename StateType> |
|||
struct StateStorage { |
|||
// Creates an empty state storage structure for storing states of the given bit width. |
|||
StateStorage(uint64_t bitsPerState); |
|||
|
|||
// This member stores all the states and maps them to their unique indices. |
|||
storm::storage::BitVectorHashMap<StateType> stateToId; |
|||
|
|||
// A list of initial states in terms of their global indices. |
|||
std::vector<StateType> initialStateIndices; |
|||
|
|||
// The number of bits of each state. |
|||
uint64_t bitsPerState; |
|||
|
|||
// The number of states that were found in the exploration so far. |
|||
uint_fast64_t getNumberOfStates() const; |
|||
}; |
|||
|
|||
} |
|||
} |
|||
} |
|||
|
|||
#endif /* STORM_STORAGE_SPARSE_STATESTORAGE_H_ */ |
|||
@ -0,0 +1,17 @@ |
|||
#include "src/storage/sparse/StateValuations.h"
|
|||
|
|||
namespace storm { |
|||
namespace storage { |
|||
namespace sparse { |
|||
|
|||
StateValuations::StateValuations(state_type const& numberOfStates) : valuations(numberOfStates) { |
|||
// Intentionally left empty.
|
|||
} |
|||
|
|||
std::string StateValuations::stateInfo(state_type const& state) const { |
|||
return valuations[state].toString(); |
|||
} |
|||
|
|||
} |
|||
} |
|||
} |
|||
@ -0,0 +1,33 @@ |
|||
#ifndef STORM_STORAGE_SPARSE_STATEVALUATIONS_H_ |
|||
#define STORM_STORAGE_SPARSE_STATEVALUATIONS_H_ |
|||
|
|||
#include <cstdint> |
|||
#include <string> |
|||
|
|||
#include "src/storage/sparse/StateType.h" |
|||
#include "src/storage/expressions/SimpleValuation.h" |
|||
|
|||
#include "src/models/sparse/StateAnnotation.h" |
|||
|
|||
namespace storm { |
|||
namespace storage { |
|||
namespace sparse { |
|||
|
|||
// A structure holding information about the reachable state space that can be retrieved from the outside. |
|||
struct StateValuations : public storm::models::sparse::StateAnnotation { |
|||
/*! |
|||
* Constructs a state information object for the given number of states. |
|||
*/ |
|||
StateValuations(state_type const& numberOfStates); |
|||
|
|||
// A mapping from state indices to their variable valuations. |
|||
std::vector<storm::expressions::SimpleValuation> valuations; |
|||
|
|||
virtual std::string stateInfo(state_type const& state) const override; |
|||
}; |
|||
|
|||
} |
|||
} |
|||
} |
|||
|
|||
#endif /* STORM_STORAGE_SPARSE_STATEVALUATIONS_H_ */ |
|||
Some files were not shown because too many files changed in this diff
Write
Preview
Loading…
Cancel
Save
Reference in new issue