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

fixed a bunch of unused variable warnings

main
dehnert 8 years ago
parent
05203792f2
commit
136cb194d1
41 changed files with 171 additions and 177 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 24
      src/storm/abstraction/ExpressionTranslator.cpp
  2. 4
      src/storm/abstraction/MenuGame.cpp
  3. 6
      src/storm/abstraction/MenuGameRefiner.cpp
  4. 2
      src/storm/abstraction/MenuGameRefiner.h
  5. 8
      src/storm/adapters/AddExpressionAdapter.cpp
  6. 8
      src/storm/adapters/MathsatExpressionAdapter.h
  7. 2
      src/storm/adapters/Smt2ExpressionAdapter.h
  8. 8
      src/storm/adapters/Z3ExpressionAdapter.cpp
  9. 4
      src/storm/builder/DdJaniModelBuilder.cpp
  10. 8
      src/storm/builder/DdPrismModelBuilder.cpp
  11. 4
      src/storm/builder/DdPrismModelBuilder.h
  12. 2
      src/storm/builder/RewardModelBuilder.cpp
  13. 2
      src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp
  14. 24
      src/storm/counterexamples/MILPMinimalLabelSetGenerator.h
  15. 4
      src/storm/counterexamples/SMTMinimalCommandSetGenerator.h
  16. 2
      src/storm/generator/JaniNextStateGenerator.cpp
  17. 2
      src/storm/generator/PrismNextStateGenerator.cpp
  18. 14
      src/storm/logic/CloneVisitor.cpp
  19. 6
      src/storm/logic/Formula.cpp
  20. 40
      src/storm/logic/FormulaInformationVisitor.cpp
  21. 14
      src/storm/logic/FragmentChecker.cpp
  22. 2
      src/storm/logic/LabelSubstitutionVisitor.cpp
  23. 34
      src/storm/logic/ToExpressionVisitor.cpp
  24. 2
      src/storm/logic/VariableSubstitutionVisitor.cpp
  25. 12
      src/storm/modelchecker/AbstractModelChecker.cpp
  26. 6
      src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp
  27. 2
      src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.h
  28. 6
      src/storm/modelchecker/csl/HybridCtmcCslModelChecker.cpp
  29. 12
      src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp
  30. 10
      src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp
  31. 12
      src/storm/modelchecker/csl/helper/HybridCtmcCslHelper.cpp
  32. 3
      src/storm/modelchecker/csl/helper/HybridCtmcCslHelper.h
  33. 20
      src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp
  34. 4
      src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.h
  35. 15
      src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp
  36. 8
      src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.h
  37. 2
      src/storm/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp
  38. 2
      src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp
  39. 4
      src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp
  40. 2
      src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h
  41. 2
      src/storm/utility/storm.h

24
src/storm/abstraction/ExpressionTranslator.cpp
View File

@ -26,7 +26,7 @@ namespace storm {
}
template <storm::dd::DdType DdType>
boost::any ExpressionTranslator<DdType>::visit(IfThenElseExpression const& expression, boost::any const& data) {
boost::any ExpressionTranslator<DdType>::visit(IfThenElseExpression const&, boost::any const&) {
STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Expressions of this kind are currently not supported by the abstraction expression translator.");
}
@ -57,8 +57,8 @@ namespace storm {
// At this point, none of the predicates was found to be equivalent, so we split the expression.
}
storm::dd::Bdd<DdType> left = boost::any_cast<storm::dd::Bdd<DdType>>(expression.getFirstOperand()->accept(*this, boost::none));
storm::dd::Bdd<DdType> right = boost::any_cast<storm::dd::Bdd<DdType>>(expression.getSecondOperand()->accept(*this, boost::none));
storm::dd::Bdd<DdType> left = boost::any_cast<storm::dd::Bdd<DdType>>(expression.getFirstOperand()->accept(*this, data));
storm::dd::Bdd<DdType> right = boost::any_cast<storm::dd::Bdd<DdType>>(expression.getSecondOperand()->accept(*this, data));
switch (expression.getOperatorType()) {
case BinaryBooleanFunctionExpression::OperatorType::And: return left && right;
case BinaryBooleanFunctionExpression::OperatorType::Or: return left || right;
@ -69,7 +69,7 @@ namespace storm {
}
template <storm::dd::DdType DdType>
boost::any ExpressionTranslator<DdType>::visit(BinaryNumericalFunctionExpression const& expression, boost::any const& data) {
boost::any ExpressionTranslator<DdType>::visit(BinaryNumericalFunctionExpression const&, boost::any const&) {
STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Expressions of this kind are currently not supported by the abstraction expression translator.");
}
@ -92,8 +92,8 @@ namespace storm {
STORM_LOG_THROW(!hasLocationVariables || !hasAbstractedVariables, storm::exceptions::NotSupportedException, "Expressions with two types (location variables and abstracted variables) of variables are currently not supported by the abstraction expression translator.");
if (hasLocationVariables) {
storm::dd::Add<DdType, double> left = boost::any_cast<storm::dd::Add<DdType, double>>(expression.getFirstOperand()->accept(*this, boost::none));
storm::dd::Add<DdType, double> right = boost::any_cast<storm::dd::Add<DdType, double>>(expression.getSecondOperand()->accept(*this, boost::none));
storm::dd::Add<DdType, double> left = boost::any_cast<storm::dd::Add<DdType, double>>(expression.getFirstOperand()->accept(*this, data));
storm::dd::Add<DdType, double> right = boost::any_cast<storm::dd::Add<DdType, double>>(expression.getSecondOperand()->accept(*this, data));
switch (expression.getRelationType()) {
case BinaryRelationExpression::RelationType::Equal: return left.equals(right);
@ -117,7 +117,7 @@ namespace storm {
}
template <storm::dd::DdType DdType>
boost::any ExpressionTranslator<DdType>::visit(VariableExpression const& expression, boost::any const& data) {
boost::any ExpressionTranslator<DdType>::visit(VariableExpression const& expression, boost::any const&) {
if (abstractedVariables.find(expression.getVariable()) != abstractedVariables.end()) {
for (uint64_t predicateIndex = 0; predicateIndex < abstractionInformation.get().getNumberOfPredicates(); ++predicateIndex) {
if (equivalenceChecker.areEquivalent(abstractionInformation.get().getPredicateByIndex(predicateIndex), expression.toExpression())) {
@ -158,19 +158,19 @@ namespace storm {
// At this point, none of the predicates was found to be equivalent, so we split the expression.
}
storm::dd::Bdd<DdType> sub = boost::any_cast<storm::dd::Bdd<DdType>>(expression.getOperand()->accept(*this, boost::none));
storm::dd::Bdd<DdType> sub = boost::any_cast<storm::dd::Bdd<DdType>>(expression.getOperand()->accept(*this, data));
switch (expression.getOperatorType()) {
case UnaryBooleanFunctionExpression::OperatorType::Not: return !sub;
}
}
template <storm::dd::DdType DdType>
boost::any ExpressionTranslator<DdType>::visit(UnaryNumericalFunctionExpression const& expression, boost::any const& data) {
boost::any ExpressionTranslator<DdType>::visit(UnaryNumericalFunctionExpression const&, boost::any const&) {
STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Expressions of this kind are currently not supported by the abstraction expression translator.");
}
template <storm::dd::DdType DdType>
boost::any ExpressionTranslator<DdType>::visit(BooleanLiteralExpression const& expression, boost::any const& data) {
boost::any ExpressionTranslator<DdType>::visit(BooleanLiteralExpression const& expression, boost::any const&) {
if (expression.isTrue()) {
return abstractionInformation.get().getDdManager().getBddOne();
} else {
@ -179,12 +179,12 @@ namespace storm {
}
template <storm::dd::DdType DdType>
boost::any ExpressionTranslator<DdType>::visit(IntegerLiteralExpression const& expression, boost::any const& data) {
boost::any ExpressionTranslator<DdType>::visit(IntegerLiteralExpression const& expression, boost::any const&) {
return abstractionInformation.get().getDdManager().template getConstant<double>(expression.getValue());
}
template <storm::dd::DdType DdType>
boost::any ExpressionTranslator<DdType>::visit(RationalLiteralExpression const& expression, boost::any const& data) {
boost::any ExpressionTranslator<DdType>::visit(RationalLiteralExpression const&, boost::any const&) {
STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Expressions of this kind are currently not supported by the abstraction expression translator.");
}

4
src/storm/abstraction/MenuGame.cpp
View File

@ -34,7 +34,7 @@ namespace storm {
}
template<storm::dd::DdType Type, typename ValueType>
storm::dd::Bdd<Type> MenuGame<Type, ValueType>::getStates(std::string const& label) const {
storm::dd::Bdd<Type> MenuGame<Type, ValueType>::getStates(std::string const&) const {
STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Menu games do not provide labels.");
}
@ -75,7 +75,7 @@ namespace storm {
}
template<storm::dd::DdType Type, typename ValueType>
bool MenuGame<Type, ValueType>::hasLabel(std::string const& label) const {
bool MenuGame<Type, ValueType>::hasLabel(std::string const&) const {
return false;
}

6
src/storm/abstraction/MenuGameRefiner.cpp
View File

@ -231,7 +231,7 @@ namespace storm {
}
template <storm::dd::DdType Type, typename ValueType>
RefinementPredicates MenuGameRefiner<Type, ValueType>::derivePredicatesFromDifferingChoices(storm::dd::Bdd<Type> const& pivotState, storm::dd::Bdd<Type> const& player1Choice, storm::dd::Bdd<Type> const& lowerChoice, storm::dd::Bdd<Type> const& upperChoice) const {
RefinementPredicates MenuGameRefiner<Type, ValueType>::derivePredicatesFromDifferingChoices(storm::dd::Bdd<Type> const& player1Choice, storm::dd::Bdd<Type> const& lowerChoice, storm::dd::Bdd<Type> const& upperChoice) const {
// Prepare result.
storm::expressions::Expression newPredicate;
bool fromGuard = false;
@ -389,7 +389,7 @@ namespace storm {
bool lowerChoicesDifferent = !lowerChoice1.exclusiveOr(lowerChoice2).isZero();
if (lowerChoicesDifferent) {
STORM_LOG_TRACE("Deriving predicate based on lower choice.");
predicates = derivePredicatesFromDifferingChoices(pivotState, (pivotState && minPlayer1Strategy).existsAbstract(game.getRowVariables()), lowerChoice1, lowerChoice2);
predicates = derivePredicatesFromDifferingChoices((pivotState && minPlayer1Strategy).existsAbstract(game.getRowVariables()), lowerChoice1, lowerChoice2);
}
if (predicates && (!player1ChoicesDifferent || predicates.get().getSource() == RefinementPredicates::Source::Guard)) {
@ -404,7 +404,7 @@ namespace storm {
bool upperChoicesDifferent = !upperChoice1.exclusiveOr(upperChoice2).isZero();
if (upperChoicesDifferent) {
STORM_LOG_TRACE("Deriving predicate based on upper choice.");
additionalPredicates = derivePredicatesFromDifferingChoices(pivotState, (pivotState && maxPlayer1Strategy).existsAbstract(game.getRowVariables()), upperChoice1, upperChoice2);
additionalPredicates = derivePredicatesFromDifferingChoices((pivotState && maxPlayer1Strategy).existsAbstract(game.getRowVariables()), upperChoice1, upperChoice2);
}
if (additionalPredicates) {

2
src/storm/abstraction/MenuGameRefiner.h
View File

@ -100,7 +100,7 @@ namespace storm {
bool addedAllGuards() const;
private:
RefinementPredicates derivePredicatesFromDifferingChoices(storm::dd::Bdd<Type> const& pivotState, storm::dd::Bdd<Type> const& player1Choice, storm::dd::Bdd<Type> const& lowerChoice, storm::dd::Bdd<Type> const& upperChoice) const;
RefinementPredicates derivePredicatesFromDifferingChoices(storm::dd::Bdd<Type> const& player1Choice, storm::dd::Bdd<Type> const& lowerChoice, storm::dd::Bdd<Type> const& upperChoice) const;
RefinementPredicates derivePredicatesFromPivotState(storm::abstraction::MenuGame<Type, ValueType> const& game, storm::dd::Bdd<Type> const& pivotState, storm::dd::Bdd<Type> const& minPlayer1Strategy, storm::dd::Bdd<Type> const& minPlayer2Strategy, storm::dd::Bdd<Type> const& maxPlayer1Strategy, storm::dd::Bdd<Type> const& maxPlayer2Strategy) const;
/*!

8
src/storm/adapters/AddExpressionAdapter.cpp
View File

@ -142,7 +142,7 @@ namespace storm {
}
template<storm::dd::DdType Type, typename ValueType>
boost::any AddExpressionAdapter<Type, ValueType>::visit(storm::expressions::VariableExpression const& expression, boost::any const& data) {
boost::any AddExpressionAdapter<Type, ValueType>::visit(storm::expressions::VariableExpression const& expression, boost::any const&) {
auto const& variablePair = variableMapping->find(expression.getVariable());
STORM_LOG_THROW(variablePair != variableMapping->end(), storm::exceptions::InvalidArgumentException, "Cannot translate the given expression, because it contains the variable '" << expression.getVariableName() << "' for which no DD counterpart is known.");
if (expression.hasBooleanType()) {
@ -187,17 +187,17 @@ namespace storm {
}
template<storm::dd::DdType Type, typename ValueType>
boost::any AddExpressionAdapter<Type, ValueType>::visit(storm::expressions::BooleanLiteralExpression const& expression, boost::any const& data) {
boost::any AddExpressionAdapter<Type, ValueType>::visit(storm::expressions::BooleanLiteralExpression const& expression, boost::any const&) {
return expression.getValue() ? ddManager->getBddOne() : ddManager->getBddZero();
}
template<storm::dd::DdType Type, typename ValueType>
boost::any AddExpressionAdapter<Type, ValueType>::visit(storm::expressions::IntegerLiteralExpression const& expression, boost::any const& data) {
boost::any AddExpressionAdapter<Type, ValueType>::visit(storm::expressions::IntegerLiteralExpression const& expression, boost::any const&) {
return ddManager->getConstant(static_cast<ValueType>(expression.getValue()));
}
template<storm::dd::DdType Type, typename ValueType>
boost::any AddExpressionAdapter<Type, ValueType>::visit(storm::expressions::RationalLiteralExpression const& expression, boost::any const& data) {
boost::any AddExpressionAdapter<Type, ValueType>::visit(storm::expressions::RationalLiteralExpression const& expression, boost::any const&) {
return ddManager->getConstant(static_cast<ValueType>(expression.getValueAsDouble()));
}

8
src/storm/adapters/MathsatExpressionAdapter.h
View File

@ -176,15 +176,15 @@ namespace storm {
}
}
virtual boost::any visit(storm::expressions::BooleanLiteralExpression const& expression, boost::any const& data) override {
virtual boost::any visit(storm::expressions::BooleanLiteralExpression const& expression, boost::any const&) override {
return expression.getValue() ? msat_make_true(env) : msat_make_false(env);
}
virtual boost::any visit(storm::expressions::RationalLiteralExpression const& expression, boost::any const& data) override {
virtual boost::any visit(storm::expressions::RationalLiteralExpression const& expression, boost::any const&) override {
return msat_make_number(env, std::to_string(expression.getValueAsDouble()).c_str());
}
virtual boost::any visit(storm::expressions::IntegerLiteralExpression const& expression, boost::any const& data) override {
virtual boost::any visit(storm::expressions::IntegerLiteralExpression const& expression, boost::any const&) override {
return msat_make_number(env, std::to_string(static_cast<int>(expression.getValue())).c_str());
}
@ -218,7 +218,7 @@ namespace storm {
}
}
virtual boost::any visit(storm::expressions::VariableExpression const& expression, boost::any const& data) override {
virtual boost::any visit(storm::expressions::VariableExpression const& expression, boost::any const&) override {
return translateExpression(expression.getVariable());
}

2
src/storm/adapters/Smt2ExpressionAdapter.h
View File

@ -24,7 +24,7 @@ namespace storm {
* @param manager The manager that can be used to build expressions.
* @param useReadableVarNames sets whether the expressions should use human readable names for the variables or the internal representation
*/
Smt2ExpressionAdapter(storm::expressions::ExpressionManager& manager, bool useReadableVarNames)
Smt2ExpressionAdapter(storm::expressions::ExpressionManager&, bool useReadableVarNames)
: useReadableVarNames(useReadableVarNames) {
declaredVariables.emplace_back(std::set<std::string>());
}

8
src/storm/adapters/Z3ExpressionAdapter.cpp
View File

@ -207,17 +207,17 @@ namespace storm {
}
}
boost::any Z3ExpressionAdapter::visit(storm::expressions::BooleanLiteralExpression const& expression, boost::any const& data) {
boost::any Z3ExpressionAdapter::visit(storm::expressions::BooleanLiteralExpression const& expression, boost::any const&) {
return context.bool_val(expression.getValue());
}
boost::any Z3ExpressionAdapter::visit(storm::expressions::RationalLiteralExpression const& expression, boost::any const& data) {
boost::any Z3ExpressionAdapter::visit(storm::expressions::RationalLiteralExpression const& expression, boost::any const&) {
std::stringstream fractionStream;
fractionStream << expression.getValue();
return context.real_val(fractionStream.str().c_str());
}
boost::any Z3ExpressionAdapter::visit(storm::expressions::IntegerLiteralExpression const& expression, boost::any const& data) {
boost::any Z3ExpressionAdapter::visit(storm::expressions::IntegerLiteralExpression const& expression, boost::any const&) {
return context.int_val(static_cast<int>(expression.getValue()));
}
@ -261,7 +261,7 @@ namespace storm {
return z3::expr(context, Z3_mk_ite(context, conditionResult, thenResult, elseResult));
}
boost::any Z3ExpressionAdapter::visit(storm::expressions::VariableExpression const& expression, boost::any const& data) {
boost::any Z3ExpressionAdapter::visit(storm::expressions::VariableExpression const& expression, boost::any const&) {
return this->translateExpression(expression.getVariable());
}

4
src/storm/builder/DdJaniModelBuilder.cpp
View File

@ -222,7 +222,7 @@ namespace storm {
return createVariables();
}
boost::any visit(storm::jani::AutomatonComposition const& composition, boost::any const& data) override {
boost::any visit(storm::jani::AutomatonComposition const& composition, boost::any const&) override {
auto it = automata.find(composition.getAutomatonName());
STORM_LOG_THROW(it == automata.end(), storm::exceptions::InvalidArgumentException, "Cannot build symbolic model from JANI model whose system composition that refers to the automaton '" << composition.getAutomatonName() << "' multiple times.");
automata.insert(it, composition.getAutomatonName());
@ -231,7 +231,7 @@ namespace storm {
boost::any visit(storm::jani::ParallelComposition const& composition, boost::any const& data) override {
for (auto const& subcomposition : composition.getSubcompositions()) {
subcomposition->accept(*this, boost::none);
subcomposition->accept(*this, data);
}
return boost::none;
}

8
src/storm/builder/DdPrismModelBuilder.cpp
View File

@ -424,7 +424,7 @@ namespace storm {
action.second = emptyAction;
} else {
// Otherwise, the actions of the modules are synchronized.
action.second = DdPrismModelBuilder<Type, ValueType>::combineSynchronizingActions(generationInfo, action.second, right.synchronizingActionToDecisionDiagramMap[action.first]);
action.second = DdPrismModelBuilder<Type, ValueType>::combineSynchronizingActions(action.second, right.synchronizingActionToDecisionDiagramMap[action.first]);
}
} else {
// If we don't synchronize over this action, we need to construct the interleaving.
@ -893,7 +893,7 @@ namespace storm {
}
template <storm::dd::DdType Type, typename ValueType>
typename DdPrismModelBuilder<Type, ValueType>::ActionDecisionDiagram DdPrismModelBuilder<Type, ValueType>::combineSynchronizingActions(GenerationInformation const& generationInfo, ActionDecisionDiagram const& action1, ActionDecisionDiagram const& action2) {
typename DdPrismModelBuilder<Type, ValueType>::ActionDecisionDiagram DdPrismModelBuilder<Type, ValueType>::combineSynchronizingActions(ActionDecisionDiagram const& action1, ActionDecisionDiagram const& action2) {
std::set<storm::expressions::Variable> assignedGlobalVariables;
std::set_union(action1.assignedGlobalVariables.begin(), action1.assignedGlobalVariables.end(), action2.assignedGlobalVariables.begin(), action2.assignedGlobalVariables.end(), std::inserter(assignedGlobalVariables, assignedGlobalVariables.begin()));
return ActionDecisionDiagram(action1.guardDd * action2.guardDd, action1.transitionsDd * action2.transitionsDd, assignedGlobalVariables, std::max(action1.numberOfUsedNondeterminismVariables, action2.numberOfUsedNondeterminismVariables));
@ -1107,7 +1107,7 @@ namespace storm {
}
template <storm::dd::DdType Type, typename ValueType>
storm::models::symbolic::StandardRewardModel<Type, ValueType> DdPrismModelBuilder<Type, ValueType>::createRewardModelDecisionDiagrams(GenerationInformation& generationInfo, storm::prism::RewardModel const& rewardModel, ModuleDecisionDiagram const& globalModule, storm::dd::Add<Type, ValueType> const& transitionMatrix, storm::dd::Add<Type, ValueType> const& reachableStatesAdd, storm::dd::Add<Type, ValueType> const& stateActionDd) {
storm::models::symbolic::StandardRewardModel<Type, ValueType> DdPrismModelBuilder<Type, ValueType>::createRewardModelDecisionDiagrams(GenerationInformation& generationInfo, storm::prism::RewardModel const& rewardModel, ModuleDecisionDiagram const& globalModule, storm::dd::Add<Type, ValueType> const& reachableStatesAdd, storm::dd::Add<Type, ValueType> const& stateActionDd) {
// Start by creating the state reward vector.
boost::optional<storm::dd::Add<Type, ValueType>> stateRewards;
@ -1384,7 +1384,7 @@ namespace storm {
std::unordered_map<std::string, storm::models::symbolic::StandardRewardModel<Type, ValueType>> rewardModels;
for (auto const& rewardModel : selectedRewardModels) {
rewardModels.emplace(rewardModel.get().getName(), createRewardModelDecisionDiagrams(generationInfo, rewardModel.get(), globalModule, transitionMatrix, reachableStatesAdd, stateActionDd));
rewardModels.emplace(rewardModel.get().getName(), createRewardModelDecisionDiagrams(generationInfo, rewardModel.get(), globalModule, reachableStatesAdd, stateActionDd));
}
// Build the labels that can be accessed as a shortcut.

4
src/storm/builder/DdPrismModelBuilder.h
View File

@ -218,7 +218,7 @@ namespace storm {
static ActionDecisionDiagram combineCommandsToActionMDP(GenerationInformation& generationInfo, std::vector<ActionDecisionDiagram>& commandDds, uint_fast64_t nondeterminismVariableOffset);
static ActionDecisionDiagram combineSynchronizingActions(GenerationInformation const& generationInfo, ActionDecisionDiagram const& action1, ActionDecisionDiagram const& action2);
static ActionDecisionDiagram combineSynchronizingActions(ActionDecisionDiagram const& action1, ActionDecisionDiagram const& action2);
static ActionDecisionDiagram combineUnsynchronizedActions(GenerationInformation const& generationInfo, ActionDecisionDiagram& action1, ActionDecisionDiagram& action2, storm::dd::Add<Type, ValueType> const& identityDd1, storm::dd::Add<Type, ValueType> const& identityDd2);
@ -230,7 +230,7 @@ namespace storm {
static storm::dd::Add<Type, ValueType> createSystemFromModule(GenerationInformation& generationInfo, ModuleDecisionDiagram const& module);
static storm::models::symbolic::StandardRewardModel<Type, ValueType> createRewardModelDecisionDiagrams(GenerationInformation& generationInfo, storm::prism::RewardModel const& rewardModel, ModuleDecisionDiagram const& globalModule, storm::dd::Add<Type, ValueType> const& transitionMatrix, storm::dd::Add<Type, ValueType> const& reachableStatesAdd, storm::dd::Add<Type, ValueType> const& stateActionDd);
static storm::models::symbolic::StandardRewardModel<Type, ValueType> createRewardModelDecisionDiagrams(GenerationInformation& generationInfo, storm::prism::RewardModel const& rewardModel, ModuleDecisionDiagram const& globalModule, storm::dd::Add<Type, ValueType> const& reachableStatesAdd, storm::dd::Add<Type, ValueType> const& stateActionDd);
static SystemResult createSystemDecisionDiagram(GenerationInformation& generationInfo);

2
src/storm/builder/RewardModelBuilder.cpp
View File

@ -16,7 +16,7 @@ namespace storm {
}
template <typename ValueType>
storm::models::sparse::StandardRewardModel<ValueType> RewardModelBuilder<ValueType>::build(uint_fast64_t rowCount, uint_fast64_t columnCount, uint_fast64_t rowGroupCount) {
storm::models::sparse::StandardRewardModel<ValueType> RewardModelBuilder<ValueType>::build(uint_fast64_t rowCount, uint_fast64_t, uint_fast64_t rowGroupCount) {
boost::optional<std::vector<ValueType>> optionalStateRewardVector;
if (hasStateRewards()) {
stateRewardVector.resize(rowGroupCount);

2
src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp
View File

@ -2405,7 +2405,7 @@ namespace storm {
}
template<typename ValueType>
std::vector<storm::RationalFunction> getParameters(storm::jani::Model const& model, std::shared_ptr<carl::Cache<carl::PolynomialFactorizationPair<RawPolynomial>>> cache) {
std::vector<storm::RationalFunction> getParameters(storm::jani::Model const&, std::shared_ptr<carl::Cache<carl::PolynomialFactorizationPair<RawPolynomial>>> cache) {
STORM_LOG_THROW(false, storm::exceptions::InvalidStateException, "This function must not be called for this type.");
}

24
src/storm/counterexamples/MILPMinimalLabelSetGenerator.h
View File

@ -262,11 +262,9 @@ namespace storm {
* Creates the variable for the probability of the virtual initial state.
*
* @param solver The MILP solver.
* @param maximizeProbability If set to true, the objective function is constructed in a way that a
* label-minimal subsystem of maximal probability is computed.
* @return The index of the variable for the probability of the virtual initial state.
*/
static std::pair<storm::expressions::Variable, uint_fast64_t> createVirtualInitialStateVariable(storm::solver::LpSolver& solver, bool maximizeProbability = false) {
static std::pair<storm::expressions::Variable, uint_fast64_t> createVirtualInitialStateVariable(storm::solver::LpSolver& solver) {
std::stringstream variableNameBuffer;
variableNameBuffer << "pinit";
storm::expressions::Variable variable = solver.addBoundedContinuousVariable(variableNameBuffer.str(), 0, 1);
@ -415,13 +413,12 @@ namespace storm {
* exceeds the given threshold.
*
* @param solver The MILP solver.
* @param labeledMdp The labeled MDP.
* @param variableInformation A struct with information about the variables of the model.
* @param probabilityThreshold The probability that the subsystem must exceed.
* @param strictBound A flag indicating whether the threshold must be exceeded or only matched.
* @return The total number of constraints that were created.
*/
static uint_fast64_t assertProbabilityGreaterThanThreshold(storm::solver::LpSolver& solver, storm::models::sparse::Mdp<T> const& labeledMdp, VariableInformation const& variableInformation, double probabilityThreshold, bool strictBound) {
static uint_fast64_t assertProbabilityGreaterThanThreshold(storm::solver::LpSolver& solver, VariableInformation const& variableInformation, double probabilityThreshold, bool strictBound) {
storm::expressions::Expression constraint;
if (strictBound) {
constraint = variableInformation.virtualInitialStateVariable > solver.getConstant(probabilityThreshold);
@ -506,11 +503,10 @@ namespace storm {
*
* @param solver The MILP solver.
* @param stateInformation The information about the states in the model.
* @param choiceInformation The information about the choices in the model.
* @param variableInformation A struct with information about the variables of the model.
* @return The total number of constraints that were created.
*/
static uint_fast64_t assertZeroProbabilityWithoutChoice(storm::solver::LpSolver& solver, StateInformation const& stateInformation, ChoiceInformation const& choiceInformation, VariableInformation const& variableInformation) {
static uint_fast64_t assertZeroProbabilityWithoutChoice(storm::solver::LpSolver& solver, StateInformation const& stateInformation, VariableInformation const& variableInformation) {
uint_fast64_t numberOfConstraintsCreated = 0;
for (auto state : stateInformation.relevantStates) {
storm::expressions::Expression constraint = variableInformation.stateToProbabilityVariableMap.at(state);
@ -624,13 +620,11 @@ namespace storm {
* Asserts that labels that are on all paths from initial to target states are definitely taken.
*
* @param solver The MILP solver.
* @param labeledMdp The labeled MDP.
* @param psiStates A bit vector characterizing the psi states in the model.
* @param choiceInformation The information about the choices in the model.
* @param variableInformation A struct with information about the variables of the model.
* @return The total number of constraints that were created.
*/
static uint_fast64_t assertKnownLabels(storm::solver::LpSolver& solver, storm::models::sparse::Mdp<T> const& labeledMdp, storm::storage::BitVector const& psiStates, ChoiceInformation const& choiceInformation, VariableInformation const& variableInformation) {
static uint_fast64_t assertKnownLabels(storm::solver::LpSolver& solver, ChoiceInformation const& choiceInformation, VariableInformation const& variableInformation) {
uint_fast64_t numberOfConstraintsCreated = 0;
for (auto label : choiceInformation.knownLabels) {
@ -815,7 +809,7 @@ namespace storm {
*/
static void buildConstraintSystem(storm::solver::LpSolver& solver, storm::models::sparse::Mdp<T> const& labeledMdp, storm::storage::BitVector const& psiStates, StateInformation const& stateInformation, ChoiceInformation const& choiceInformation, VariableInformation const& variableInformation, double probabilityThreshold, bool strictBound, bool includeSchedulerCuts = false) {
// Assert that the reachability probability in the subsystem exceeds the given threshold.
uint_fast64_t numberOfConstraints = assertProbabilityGreaterThanThreshold(solver, labeledMdp, variableInformation, probabilityThreshold, strictBound);
uint_fast64_t numberOfConstraints = assertProbabilityGreaterThanThreshold(solver, variableInformation, probabilityThreshold, strictBound);
STORM_LOG_DEBUG("Asserted that reachability probability exceeds threshold.");
// Add constraints that assert the policy takes at most one action in each state.
@ -828,7 +822,7 @@ namespace storm {
// Add constraints that encode that the reachability probability from states which do not pick any action
// is zero.
numberOfConstraints += assertZeroProbabilityWithoutChoice(solver, stateInformation, choiceInformation, variableInformation);
numberOfConstraints += assertZeroProbabilityWithoutChoice(solver, stateInformation, variableInformation);
STORM_LOG_DEBUG("Asserted that reachability probability is zero if no choice is taken.");
// Add constraints that encode the reachability probabilities for states.
@ -840,7 +834,7 @@ namespace storm {
STORM_LOG_DEBUG("Asserted that unproblematic state reachable from problematic states.");
// Add constraints that express that certain labels are already known to be taken.
numberOfConstraints += assertKnownLabels(solver, labeledMdp, psiStates, choiceInformation, variableInformation);
numberOfConstraints += assertKnownLabels(solver, choiceInformation, variableInformation);
STORM_LOG_DEBUG("Asserted known labels are taken.");
// If required, assert additional constraints that reduce the number of possible policies.
@ -923,7 +917,7 @@ namespace storm {
}
public:
static boost::container::flat_set<uint_fast64_t> getMinimalLabelSet(storm::logic::Formula const& pathFormula, storm::models::sparse::Mdp<T> const& labeledMdp, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, double probabilityThreshold, bool strictBound, bool checkThresholdFeasible = false, bool includeSchedulerCuts = false) {
static boost::container::flat_set<uint_fast64_t> getMinimalLabelSet(storm::models::sparse::Mdp<T> const& labeledMdp, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, double probabilityThreshold, bool strictBound, bool checkThresholdFeasible = false, bool includeSchedulerCuts = false) {
// (0) Check whether the MDP is indeed labeled.
if (!labeledMdp.hasChoiceLabeling()) {
throw storm::exceptions::InvalidArgumentException() << "Minimal label set generation is impossible for unlabeled model.";
@ -1015,7 +1009,7 @@ namespace storm {
// Delegate the actual computation work to the function of equal name.
auto startTime = std::chrono::high_resolution_clock::now();
boost::container::flat_set<uint_fast64_t> usedLabelSet = getMinimalLabelSet(probabilityOperator.getSubformula(), labeledMdp, phiStates, psiStates, threshold, strictBound, true, storm::settings::getModule<storm::settings::modules::CounterexampleGeneratorSettings>().isUseSchedulerCutsSet());
boost::container::flat_set<uint_fast64_t> usedLabelSet = getMinimalLabelSet(labeledMdp, phiStates, psiStates, threshold, strictBound, true, storm::settings::getModule<storm::settings::modules::CounterexampleGeneratorSettings>().isUseSchedulerCutsSet());
auto endTime = std::chrono::high_resolution_clock::now();
std::cout << std::endl << "Computed minimal label set of size " << usedLabelSet.size() << " in " << std::chrono::duration_cast<std::chrono::milliseconds>(endTime - startTime).count() << "ms." << std::endl;

4
src/storm/counterexamples/SMTMinimalCommandSetGenerator.h
View File

@ -1593,7 +1593,7 @@ namespace storm {
* @param checkThresholdFeasible If set, it is verified that the model can actually achieve/exceed the given probability value. If this check
* is made and fails, an exception is thrown.
*/
static boost::container::flat_set<uint_fast64_t> getMinimalCommandSet(storm::logic::Formula const& pathFormula, storm::prism::Program program, std::string const& constantDefinitionString, storm::models::sparse::Mdp<T> const& labeledMdp, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, double probabilityThreshold, bool strictBound, bool checkThresholdFeasible = false, bool includeReachabilityEncoding = false) {
static boost::container::flat_set<uint_fast64_t> getMinimalCommandSet(storm::prism::Program program, std::string const& constantDefinitionString, storm::models::sparse::Mdp<T> const& labeledMdp, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, double probabilityThreshold, bool strictBound, bool checkThresholdFeasible = false, bool includeReachabilityEncoding = false) {
#ifdef STORM_HAVE_Z3
// Set up all clocks used for time measurement.
auto totalClock = std::chrono::high_resolution_clock::now();
@ -1791,7 +1791,7 @@ namespace storm {
// Delegate the actual computation work to the function of equal name.
auto startTime = std::chrono::high_resolution_clock::now();
auto labelSet = getMinimalCommandSet(probabilityOperator.getSubformula(), program, constantDefinitionString, labeledMdp, phiStates, psiStates, threshold, strictBound, true, storm::settings::getModule<storm::settings::modules::CounterexampleGeneratorSettings>().isEncodeReachabilitySet());
auto labelSet = getMinimalCommandSet(program, constantDefinitionString, labeledMdp, phiStates, psiStates, threshold, strictBound, true, storm::settings::getModule<storm::settings::modules::CounterexampleGeneratorSettings>().isEncodeReachabilitySet());
auto endTime = std::chrono::high_resolution_clock::now();
std::cout << std::endl << "Computed minimal label set of size " << labelSet.size() << " in " << std::chrono::duration_cast<std::chrono::milliseconds>(endTime - startTime).count() << "ms." << std::endl;

2
src/storm/generator/JaniNextStateGenerator.cpp
View File

@ -23,7 +23,7 @@ namespace storm {
}
template<typename ValueType, typename StateType>
JaniNextStateGenerator<ValueType, StateType>::JaniNextStateGenerator(storm::jani::Model const& model, NextStateGeneratorOptions const& options, bool flag) : NextStateGenerator<ValueType, StateType>(model.getExpressionManager(), options), model(model), rewardVariables(), hasStateActionRewards(false) {
JaniNextStateGenerator<ValueType, StateType>::JaniNextStateGenerator(storm::jani::Model const& model, NextStateGeneratorOptions const& options, bool) : NextStateGenerator<ValueType, StateType>(model.getExpressionManager(), options), model(model), rewardVariables(), hasStateActionRewards(false) {
STORM_LOG_THROW(model.hasStandardComposition(), storm::exceptions::WrongFormatException, "The explicit next-state generator currently does not support custom system compositions.");
STORM_LOG_THROW(!model.hasNonGlobalTransientVariable(), storm::exceptions::InvalidSettingsException, "The explicit next-state generator currently does not support automata-local transient variables.");
STORM_LOG_THROW(!model.usesAssignmentLevels(), storm::exceptions::InvalidSettingsException, "The explicit next-state generator currently does not support assignment levels.");

2
src/storm/generator/PrismNextStateGenerator.cpp
View File

@ -22,7 +22,7 @@ namespace storm {
}
template<typename ValueType, typename StateType>
PrismNextStateGenerator<ValueType, StateType>::PrismNextStateGenerator(storm::prism::Program const& program, NextStateGeneratorOptions const& options, bool flag) : NextStateGenerator<ValueType, StateType>(program.getManager(), options), program(program), rewardModels() {
PrismNextStateGenerator<ValueType, StateType>::PrismNextStateGenerator(storm::prism::Program const& program, NextStateGeneratorOptions const& options, bool) : NextStateGenerator<ValueType, StateType>(program.getManager(), options), program(program), rewardModels() {
STORM_LOG_TRACE("Creating next-state generator for PRISM program: " << program);
STORM_LOG_THROW(!this->program.specifiesSystemComposition(), storm::exceptions::WrongFormatException, "The explicit next-state generator currently does not support custom system compositions.");

14
src/storm/logic/CloneVisitor.cpp
View File

@ -10,11 +10,11 @@ namespace storm {
return boost::any_cast<std::shared_ptr<Formula>>(result);
}
boost::any CloneVisitor::visit(AtomicExpressionFormula const& f, boost::any const& data) const {
boost::any CloneVisitor::visit(AtomicExpressionFormula const& f, boost::any const&) const {
return std::static_pointer_cast<Formula>(std::make_shared<AtomicExpressionFormula>(f));
}
boost::any CloneVisitor::visit(AtomicLabelFormula const& f, boost::any const& data) const {
boost::any CloneVisitor::visit(AtomicLabelFormula const& f, boost::any const&) const {
return std::static_pointer_cast<Formula>(std::make_shared<AtomicLabelFormula>(f));
}
@ -24,7 +24,7 @@ namespace storm {
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 {
boost::any CloneVisitor::visit(BooleanLiteralFormula const& f, boost::any const&) const {
return std::static_pointer_cast<Formula>(std::make_shared<BooleanLiteralFormula>(f));
}
@ -44,7 +44,7 @@ namespace storm {
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 {
boost::any CloneVisitor::visit(CumulativeRewardFormula const& f, boost::any const&) const {
return std::static_pointer_cast<Formula>(std::make_shared<CumulativeRewardFormula>(f));
}
@ -63,7 +63,7 @@ namespace storm {
return std::static_pointer_cast<Formula>(std::make_shared<GloballyFormula>(subformula));
}
boost::any CloneVisitor::visit(InstantaneousRewardFormula const& f, boost::any const& data) const {
boost::any CloneVisitor::visit(InstantaneousRewardFormula const& f, boost::any const&) const {
return std::static_pointer_cast<Formula>(std::make_shared<InstantaneousRewardFormula>(f));
}
@ -72,7 +72,7 @@ namespace storm {
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 {
boost::any CloneVisitor::visit(LongRunAverageRewardFormula const& f, boost::any const&) const {
return std::static_pointer_cast<Formula>(std::make_shared<LongRunAverageRewardFormula>(f));
}
@ -99,7 +99,7 @@ namespace storm {
return std::static_pointer_cast<Formula>(std::make_shared<RewardOperatorFormula>(subformula, f.getOptionalRewardModelName(), f.getOperatorInformation()));
}
boost::any CloneVisitor::visit(TotalRewardFormula const& f, boost::any const& data) const {
boost::any CloneVisitor::visit(TotalRewardFormula const& f, boost::any const&) const {
return std::static_pointer_cast<Formula>(std::make_shared<TotalRewardFormula>());
}

6
src/storm/logic/Formula.cpp
View File

@ -460,15 +460,15 @@ namespace storm {
return this->shared_from_this();
}
void Formula::gatherAtomicExpressionFormulas(std::vector<std::shared_ptr<AtomicExpressionFormula const>>& atomicExpressionFormulas) const {
void Formula::gatherAtomicExpressionFormulas(std::vector<std::shared_ptr<AtomicExpressionFormula const>>&) const {
return;
}
void Formula::gatherAtomicLabelFormulas(std::vector<std::shared_ptr<AtomicLabelFormula const>>& atomicLabelFormulas) const {
void Formula::gatherAtomicLabelFormulas(std::vector<std::shared_ptr<AtomicLabelFormula const>>&) const {
return;
}
void Formula::gatherReferencedRewardModels(std::set<std::string>& referencedRewardModels) const {
void Formula::gatherReferencedRewardModels(std::set<std::string>&) const {
return;
}

40
src/storm/logic/FormulaInformationVisitor.cpp
View File

@ -9,88 +9,88 @@ namespace storm {
return boost::any_cast<FormulaInformation>(result);
}
boost::any FormulaInformationVisitor::visit(AtomicExpressionFormula const& f, boost::any const& data) const {
boost::any FormulaInformationVisitor::visit(AtomicExpressionFormula const& f, boost::any const&) const {
return FormulaInformation();
}
boost::any FormulaInformationVisitor::visit(AtomicLabelFormula const& f, boost::any const& data) const {
boost::any FormulaInformationVisitor::visit(AtomicLabelFormula const& f, boost::any const&) const {
return FormulaInformation();
}
boost::any FormulaInformationVisitor::visit(BinaryBooleanStateFormula const& f, boost::any const& data) const {
boost::any FormulaInformationVisitor::visit(BinaryBooleanStateFormula const& f, boost::any const&) const {
return FormulaInformation();
}
boost::any FormulaInformationVisitor::visit(BooleanLiteralFormula const& f, boost::any const& data) const {
boost::any FormulaInformationVisitor::visit(BooleanLiteralFormula const& f, boost::any const&) const {
return FormulaInformation();
}
boost::any FormulaInformationVisitor::visit(BoundedUntilFormula const& f, boost::any const& data) const {
return boost::any_cast<FormulaInformation>(f.getLeftSubformula().accept(*this)).join(boost::any_cast<FormulaInformation>(f.getRightSubformula().accept(*this))).setContainsBoundedUntilFormula();
return boost::any_cast<FormulaInformation>(f.getLeftSubformula().accept(*this, data)).join(boost::any_cast<FormulaInformation>(f.getRightSubformula().accept(*this))).setContainsBoundedUntilFormula();
}
boost::any FormulaInformationVisitor::visit(ConditionalFormula const& f, boost::any const& data) const {
return boost::any_cast<FormulaInformation>(f.getSubformula().accept(*this)).join(boost::any_cast<FormulaInformation>(f.getConditionFormula().accept(*this)));
return boost::any_cast<FormulaInformation>(f.getSubformula().accept(*this, data)).join(boost::any_cast<FormulaInformation>(f.getConditionFormula().accept(*this)));
}
boost::any FormulaInformationVisitor::visit(CumulativeRewardFormula const& f, boost::any const& data) const {
boost::any FormulaInformationVisitor::visit(CumulativeRewardFormula const& f, boost::any const&) const {
return FormulaInformation();
}
boost::any FormulaInformationVisitor::visit(EventuallyFormula const& f, boost::any const& data) const {
return f.getSubformula().accept(*this);
return f.getSubformula().accept(*this, data);
}
boost::any FormulaInformationVisitor::visit(TimeOperatorFormula const& f, boost::any const& data) const {
return f.getSubformula().accept(*this);
return f.getSubformula().accept(*this, data);
}
boost::any FormulaInformationVisitor::visit(GloballyFormula const& f, boost::any const& data) const {
return f.getSubformula().accept(*this);
return f.getSubformula().accept(*this, data);
}
boost::any FormulaInformationVisitor::visit(InstantaneousRewardFormula const& f, boost::any const& data) const {
boost::any FormulaInformationVisitor::visit(InstantaneousRewardFormula const& f, boost::any const&) const {
return FormulaInformation();
}
boost::any FormulaInformationVisitor::visit(LongRunAverageOperatorFormula const& f, boost::any const& data) const {
return f.getSubformula().accept(*this);
return f.getSubformula().accept(*this, data);
}
boost::any FormulaInformationVisitor::visit(LongRunAverageRewardFormula const& f, boost::any const& data) const {
boost::any FormulaInformationVisitor::visit(LongRunAverageRewardFormula const& f, boost::any const&) const {
return FormulaInformation();
}
boost::any FormulaInformationVisitor::visit(MultiObjectiveFormula const& f, boost::any const& data) const {
FormulaInformation result;
for(auto const& subF : f.getSubformulas()){
result.join(boost::any_cast<FormulaInformation>(subF->accept(*this)));
result.join(boost::any_cast<FormulaInformation>(subF->accept(*this, data)));
}
return result;
}
boost::any FormulaInformationVisitor::visit(NextFormula const& f, boost::any const& data) const {
return boost::any_cast<FormulaInformation>(f.getSubformula().accept(*this)).setContainsNextFormula();
return boost::any_cast<FormulaInformation>(f.getSubformula().accept(*this, data)).setContainsNextFormula();
}
boost::any FormulaInformationVisitor::visit(ProbabilityOperatorFormula const& f, boost::any const& data) const {
return f.getSubformula().accept(*this);
return f.getSubformula().accept(*this, data);
}
boost::any FormulaInformationVisitor::visit(RewardOperatorFormula const& f, boost::any const& data) const {
return boost::any_cast<FormulaInformation>(f.getSubformula().accept(*this)).setContainsRewardOperator();
return boost::any_cast<FormulaInformation>(f.getSubformula().accept(*this, data)).setContainsRewardOperator();
}
boost::any FormulaInformationVisitor::visit(TotalRewardFormula const& f, boost::any const& data) const {
boost::any FormulaInformationVisitor::visit(TotalRewardFormula const& f, boost::any const&) const {
return FormulaInformation();
}
boost::any FormulaInformationVisitor::visit(UnaryBooleanStateFormula const& f, boost::any const& data) const {
return f.getSubformula().accept(*this);
return f.getSubformula().accept(*this, data);
}
boost::any FormulaInformationVisitor::visit(UntilFormula const& f, boost::any const& data) const {
return boost::any_cast<FormulaInformation>(f.getLeftSubformula().accept(*this)).join(boost::any_cast<FormulaInformation>(f.getRightSubformula().accept(*this)));
return boost::any_cast<FormulaInformation>(f.getLeftSubformula().accept(*this, data)).join(boost::any_cast<FormulaInformation>(f.getRightSubformula().accept(*this)));
}
}

14
src/storm/logic/FragmentChecker.cpp
View File

@ -28,12 +28,12 @@ namespace storm {
return result;
}
boost::any FragmentChecker::visit(AtomicExpressionFormula const& f, boost::any const& data) const {
boost::any FragmentChecker::visit(AtomicExpressionFormula const&, boost::any const& data) const {
InheritedInformation const& inherited = boost::any_cast<InheritedInformation const&>(data);
return inherited.getSpecification().areAtomicExpressionFormulasAllowed();
}
boost::any FragmentChecker::visit(AtomicLabelFormula const& f, boost::any const& data) const {
boost::any FragmentChecker::visit(AtomicLabelFormula const&, boost::any const& data) const {
InheritedInformation const& inherited = boost::any_cast<InheritedInformation const&>(data);
return inherited.getSpecification().areAtomicLabelFormulasAllowed();
}
@ -46,7 +46,7 @@ namespace storm {
return result;
}
boost::any FragmentChecker::visit(BooleanLiteralFormula const& f, boost::any const& data) const {
boost::any FragmentChecker::visit(BooleanLiteralFormula const&, boost::any const& data) const {
InheritedInformation const& inherited = boost::any_cast<InheritedInformation const&>(data);
return inherited.getSpecification().areBooleanLiteralFormulasAllowed();
}
@ -88,7 +88,7 @@ namespace storm {
return result;
}
boost::any FragmentChecker::visit(CumulativeRewardFormula const& f, boost::any const& data) const {
boost::any FragmentChecker::visit(CumulativeRewardFormula const&, boost::any const& data) const {
InheritedInformation const& inherited = boost::any_cast<InheritedInformation const&>(data);
return inherited.getSpecification().areCumulativeRewardFormulasAllowed();
}
@ -137,7 +137,7 @@ namespace storm {
return result;
}
boost::any FragmentChecker::visit(InstantaneousRewardFormula const& f, boost::any const& data) const {
boost::any FragmentChecker::visit(InstantaneousRewardFormula const&, boost::any const& data) const {
InheritedInformation const& inherited = boost::any_cast<InheritedInformation const&>(data);
return inherited.getSpecification().areInstantaneousRewardFormulasAllowed();
}
@ -154,7 +154,7 @@ namespace storm {
return result;
}
boost::any FragmentChecker::visit(LongRunAverageRewardFormula const& f, boost::any const& data) const {
boost::any FragmentChecker::visit(LongRunAverageRewardFormula const&, boost::any const& data) const {
InheritedInformation const& inherited = boost::any_cast<InheritedInformation const&>(data);
return inherited.getSpecification().areLongRunAverageRewardFormulasAllowed();
}
@ -219,7 +219,7 @@ namespace storm {
return result;
}
boost::any FragmentChecker::visit(TotalRewardFormula const& f, boost::any const& data) const {
boost::any FragmentChecker::visit(TotalRewardFormula const&, boost::any const& data) const {
InheritedInformation const& inherited = boost::any_cast<InheritedInformation const&>(data);
return inherited.getSpecification().areTotalRewardFormulasAllowed();
}

2
src/storm/logic/LabelSubstitutionVisitor.cpp
View File

@ -14,7 +14,7 @@ namespace storm {
return boost::any_cast<std::shared_ptr<Formula>>(result);
}
boost::any LabelSubstitutionVisitor::visit(AtomicLabelFormula const& f, boost::any const& data) const {
boost::any LabelSubstitutionVisitor::visit(AtomicLabelFormula const& f, boost::any const&) const {
auto it = labelToExpressionMapping.find(f.getLabel());
if (it != labelToExpressionMapping.end()) {
return std::static_pointer_cast<Formula>(std::make_shared<AtomicExpressionFormula>(it->second));

34
src/storm/logic/ToExpressionVisitor.cpp
View File

@ -15,11 +15,11 @@ namespace storm {
return boost::any_cast<storm::expressions::Expression>(result);
}
boost::any ToExpressionVisitor::visit(AtomicExpressionFormula const& f, boost::any const& data) const {
boost::any ToExpressionVisitor::visit(AtomicExpressionFormula const& f, boost::any const&) const {
return f.getExpression();
}
boost::any ToExpressionVisitor::visit(AtomicLabelFormula const& f, boost::any const& data) const {
boost::any ToExpressionVisitor::visit(AtomicLabelFormula const& f, boost::any const&) const {
STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Cannot assemble expression, because the undefined atomic label '" << f.getLabel() << "' appears in the formula.");
}
@ -46,59 +46,59 @@ namespace storm {
return result;
}
boost::any ToExpressionVisitor::visit(BoundedUntilFormula const& f, boost::any const& data) const {
boost::any ToExpressionVisitor::visit(BoundedUntilFormula const&, boost::any const&) 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 {
boost::any ToExpressionVisitor::visit(ConditionalFormula const&, boost::any const&) 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 {
boost::any ToExpressionVisitor::visit(CumulativeRewardFormula const&, boost::any const&) 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 {
boost::any ToExpressionVisitor::visit(EventuallyFormula const&, boost::any const&) 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 {
boost::any ToExpressionVisitor::visit(TimeOperatorFormula const&, boost::any const&) 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 {
boost::any ToExpressionVisitor::visit(GloballyFormula const&, boost::any const&) 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 {
boost::any ToExpressionVisitor::visit(InstantaneousRewardFormula const&, boost::any const&) 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 {
boost::any ToExpressionVisitor::visit(LongRunAverageOperatorFormula const&, boost::any const&) 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 {
boost::any ToExpressionVisitor::visit(LongRunAverageRewardFormula const&, boost::any const&) const {
STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Cannot assemble expression from formula that contains illegal elements.");
}
boost::any ToExpressionVisitor::visit(MultiObjectiveFormula const& f, boost::any const& data) const {
boost::any ToExpressionVisitor::visit(MultiObjectiveFormula const&, boost::any const&) 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 {
boost::any ToExpressionVisitor::visit(NextFormula const&, boost::any const&) 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 {
boost::any ToExpressionVisitor::visit(ProbabilityOperatorFormula const&, boost::any const&) 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 {
boost::any ToExpressionVisitor::visit(RewardOperatorFormula const&, boost::any const&) const {
STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Cannot assemble expression from formula that contains illegal elements.");
}
boost::any ToExpressionVisitor::visit(TotalRewardFormula const& f, boost::any const& data) const {
boost::any ToExpressionVisitor::visit(TotalRewardFormula const&, boost::any const&) const {
STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Cannot assemble expression from formula that contains illegal elements.");
}
@ -111,7 +111,7 @@ namespace storm {
}
}
boost::any ToExpressionVisitor::visit(UntilFormula const& f, boost::any const& data) const {
boost::any ToExpressionVisitor::visit(UntilFormula const&, boost::any const&) const {
STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Cannot assemble expression from formula that contains illegal elements.");
}

2
src/storm/logic/VariableSubstitutionVisitor.cpp
View File

@ -14,7 +14,7 @@ namespace storm {
return boost::any_cast<std::shared_ptr<Formula>>(result);
}
boost::any VariableSubstitutionVisitor::visit(AtomicExpressionFormula const& f, boost::any const& data) const {
boost::any VariableSubstitutionVisitor::visit(AtomicExpressionFormula const& f, boost::any const&) const {
return std::static_pointer_cast<Formula>(std::make_shared<AtomicExpressionFormula>(f.getExpression().substitute(substitution)));
}
}

12
src/storm/modelchecker/AbstractModelChecker.cpp
View File

@ -105,27 +105,27 @@ namespace storm {
}
template<typename ModelType>
std::unique_ptr<CheckResult> AbstractModelChecker<ModelType>::computeConditionalRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::ConditionalFormula, ValueType> const& checkTask) {
std::unique_ptr<CheckResult> AbstractModelChecker<ModelType>::computeConditionalRewards(storm::logic::RewardMeasureType, CheckTask<storm::logic::ConditionalFormula, ValueType> const& checkTask) {
STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the formula: " << checkTask.getFormula() << ".");
}
template<typename ModelType>
std::unique_ptr<CheckResult> AbstractModelChecker<ModelType>::computeCumulativeRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::CumulativeRewardFormula, ValueType> const& checkTask) {
std::unique_ptr<CheckResult> AbstractModelChecker<ModelType>::computeCumulativeRewards(storm::logic::RewardMeasureType, CheckTask<storm::logic::CumulativeRewardFormula, ValueType> const& checkTask) {
STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the formula: " << checkTask.getFormula() << ".");
}
template<typename ModelType>
std::unique_ptr<CheckResult> AbstractModelChecker<ModelType>::computeInstantaneousRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::InstantaneousRewardFormula, ValueType> const& checkTask) {
std::unique_ptr<CheckResult> AbstractModelChecker<ModelType>::computeInstantaneousRewards(storm::logic::RewardMeasureType, CheckTask<storm::logic::InstantaneousRewardFormula, ValueType> const& checkTask) {
STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the formula: " << checkTask.getFormula() << ".");
}
template<typename ModelType>
std::unique_ptr<CheckResult> AbstractModelChecker<ModelType>::computeReachabilityRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::EventuallyFormula, ValueType> const& checkTask) {
std::unique_ptr<CheckResult> AbstractModelChecker<ModelType>::computeReachabilityRewards(storm::logic::RewardMeasureType, CheckTask<storm::logic::EventuallyFormula, ValueType> const& checkTask) {
STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the formula: " << checkTask.getFormula() << ".");
}
template<typename ModelType>
std::unique_ptr<CheckResult> AbstractModelChecker<ModelType>::computeLongRunAverageRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::LongRunAverageRewardFormula, ValueType> const& checkTask) {
std::unique_ptr<CheckResult> AbstractModelChecker<ModelType>::computeLongRunAverageRewards(storm::logic::RewardMeasureType, CheckTask<storm::logic::LongRunAverageRewardFormula, ValueType> const& checkTask) {
STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the formula: " << checkTask.getFormula() << ".");
}
@ -144,7 +144,7 @@ namespace storm {
}
template<typename ModelType>
std::unique_ptr<CheckResult> AbstractModelChecker<ModelType>::computeReachabilityTimes(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::EventuallyFormula, ValueType> const& checkTask) {
std::unique_ptr<CheckResult> AbstractModelChecker<ModelType>::computeReachabilityTimes(storm::logic::RewardMeasureType, CheckTask<storm::logic::EventuallyFormula, ValueType> const& checkTask) {
STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the formula: " << checkTask.getFormula() << ".");
}

6
src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp
View File

@ -368,12 +368,12 @@ namespace storm {
}
// #ifdef LOCAL_DEBUG
abstractor->exportToDot("game" + std::to_string(iterations) + ".dot", targetStates, game.getManager().getBddOne());
// abstractor->exportToDot("game" + std::to_string(iterations) + ".dot", targetStates, game.getManager().getBddOne());
// #endif
// (3) compute all states with probability 0/1 wrt. to the two different player 2 goals (min/max).
auto qualitativeStart = std::chrono::high_resolution_clock::now();
QualitativeResultMinMax<Type> qualitativeResult = computeProb01States(checkTask, previousQualitativeResult, game, player1Direction, transitionMatrixBdd, initialStates, constraintStates, targetStates);
QualitativeResultMinMax<Type> qualitativeResult = computeProb01States(previousQualitativeResult, game, player1Direction, transitionMatrixBdd, constraintStates, targetStates);
std::unique_ptr<CheckResult> result = checkForResultAfterQualitativeCheck<Type, ValueType>(checkTask, initialStates, qualitativeResult);
if (result) {
printStatistics(*abstractor, game);
@ -527,7 +527,7 @@ namespace storm {
}
template<storm::dd::DdType Type, typename ModelType>
QualitativeResultMinMax<Type> GameBasedMdpModelChecker<Type, ModelType>::computeProb01States(CheckTask<storm::logic::Formula> const& checkTask, boost::optional<QualitativeResultMinMax<Type>> const& previousQualitativeResult, storm::abstraction::MenuGame<Type, ValueType> const& game, storm::OptimizationDirection player1Direction, storm::dd::Bdd<Type> const& transitionMatrixBdd, storm::dd::Bdd<Type> const& initialStates, storm::dd::Bdd<Type> const& constraintStates, storm::dd::Bdd<Type> const& targetStates) {
QualitativeResultMinMax<Type> GameBasedMdpModelChecker<Type, ModelType>::computeProb01States(boost::optional<QualitativeResultMinMax<Type>> const& previousQualitativeResult, storm::abstraction::MenuGame<Type, ValueType> const& game, storm::OptimizationDirection player1Direction, storm::dd::Bdd<Type> const& transitionMatrixBdd, storm::dd::Bdd<Type> const& constraintStates, storm::dd::Bdd<Type> const& targetStates) {
QualitativeResultMinMax<Type> result;

2
src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.h
View File

@ -71,7 +71,7 @@ namespace storm {
* Performs a qualitative check on the the given game to compute the (player 1) states that have probability
* 0 or 1, respectively, to reach a target state and only visiting constraint states before.
*/
QualitativeResultMinMax<Type> computeProb01States(CheckTask<storm::logic::Formula> const& checkTask, boost::optional<QualitativeResultMinMax<Type>> const& previousQualitativeResult, storm::abstraction::MenuGame<Type, ValueType> const& game, storm::OptimizationDirection player1Direction, storm::dd::Bdd<Type> const& transitionMatrixBdd, storm::dd::Bdd<Type> const& initialStates, storm::dd::Bdd<Type> const& constraintStates, storm::dd::Bdd<Type> const& targetStates);
QualitativeResultMinMax<Type> computeProb01States(boost::optional<QualitativeResultMinMax<Type>> const& previousQualitativeResult, storm::abstraction::MenuGame<Type, ValueType> const& game, storm::OptimizationDirection player1Direction, storm::dd::Bdd<Type> const& transitionMatrixBdd, storm::dd::Bdd<Type> const& constraintStates, storm::dd::Bdd<Type> const& targetStates);
void printStatistics(storm::abstraction::MenuGameAbstractor<Type, ValueType> const& abstractor, storm::abstraction::MenuGame<Type, ValueType> const& game) const;

6
src/storm/modelchecker/csl/HybridCtmcCslModelChecker.cpp
View File

@ -52,7 +52,7 @@ namespace storm {
template<typename ModelType>
std::unique_ptr<CheckResult> HybridCtmcCslModelChecker<ModelType>::computeReachabilityRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::EventuallyFormula, ValueType> const& checkTask) {
std::unique_ptr<CheckResult> HybridCtmcCslModelChecker<ModelType>::computeReachabilityRewards(storm::logic::RewardMeasureType, CheckTask<storm::logic::EventuallyFormula, ValueType> const& checkTask) {
storm::logic::EventuallyFormula const& eventuallyFormula = checkTask.getFormula();
std::unique_ptr<CheckResult> subResultPointer = this->check(eventuallyFormula.getSubformula());
SymbolicQualitativeCheckResult<DdType> const& subResult = subResultPointer->asSymbolicQualitativeCheckResult<DdType>();
@ -81,13 +81,13 @@ namespace storm {
}
template<typename ModelType>
std::unique_ptr<CheckResult> HybridCtmcCslModelChecker<ModelType>::computeInstantaneousRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::InstantaneousRewardFormula, ValueType> const& checkTask) {
std::unique_ptr<CheckResult> HybridCtmcCslModelChecker<ModelType>::computeInstantaneousRewards(storm::logic::RewardMeasureType, CheckTask<storm::logic::InstantaneousRewardFormula, ValueType> const& checkTask) {
storm::logic::InstantaneousRewardFormula const& rewardPathFormula = checkTask.getFormula();
return storm::modelchecker::helper::HybridCtmcCslHelper<DdType, ValueType>::computeInstantaneousRewards(this->getModel(), this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getContinuousTimeBound(), *linearEquationSolverFactory);
}
template<typename ModelType>
std::unique_ptr<CheckResult> HybridCtmcCslModelChecker<ModelType>::computeCumulativeRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::CumulativeRewardFormula, ValueType> const& checkTask) {
std::unique_ptr<CheckResult> HybridCtmcCslModelChecker<ModelType>::computeCumulativeRewards(storm::logic::RewardMeasureType, CheckTask<storm::logic::CumulativeRewardFormula, ValueType> const& checkTask) {
storm::logic::CumulativeRewardFormula const& rewardPathFormula = checkTask.getFormula();
return storm::modelchecker::helper::HybridCtmcCslHelper<DdType, ValueType>::computeCumulativeRewards(this->getModel(), this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getContinuousTimeBound(), *linearEquationSolverFactory);
}

12
src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp
View File

@ -94,21 +94,21 @@ namespace storm {
}
template <typename SparseCtmcModelType>
std::unique_ptr<CheckResult> SparseCtmcCslModelChecker<SparseCtmcModelType>::computeInstantaneousRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::InstantaneousRewardFormula, ValueType> const& checkTask) {
std::unique_ptr<CheckResult> SparseCtmcCslModelChecker<SparseCtmcModelType>::computeInstantaneousRewards(storm::logic::RewardMeasureType, CheckTask<storm::logic::InstantaneousRewardFormula, ValueType> const& checkTask) {
storm::logic::InstantaneousRewardFormula const& rewardPathFormula = checkTask.getFormula();
std::vector<ValueType> numericResult = storm::modelchecker::helper::SparseCtmcCslHelper::computeInstantaneousRewards(this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getContinuousTimeBound(), *linearEquationSolverFactory);
return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(std::move(numericResult)));
}
template <typename SparseCtmcModelType>
std::unique_ptr<CheckResult> SparseCtmcCslModelChecker<SparseCtmcModelType>::computeCumulativeRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::CumulativeRewardFormula, ValueType> const& checkTask) {
std::unique_ptr<CheckResult> SparseCtmcCslModelChecker<SparseCtmcModelType>::computeCumulativeRewards(storm::logic::RewardMeasureType, CheckTask<storm::logic::CumulativeRewardFormula, ValueType> const& checkTask) {
storm::logic::CumulativeRewardFormula const& rewardPathFormula = checkTask.getFormula();
std::vector<ValueType> numericResult = storm::modelchecker::helper::SparseCtmcCslHelper::computeCumulativeRewards(this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getContinuousTimeBound(), *linearEquationSolverFactory);
return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(std::move(numericResult)));
}
template <typename SparseCtmcModelType>
std::unique_ptr<CheckResult> SparseCtmcCslModelChecker<SparseCtmcModelType>::computeReachabilityRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::EventuallyFormula, ValueType> const& checkTask) {
std::unique_ptr<CheckResult> SparseCtmcCslModelChecker<SparseCtmcModelType>::computeReachabilityRewards(storm::logic::RewardMeasureType, CheckTask<storm::logic::EventuallyFormula, ValueType> const& checkTask) {
storm::logic::EventuallyFormula const& eventuallyFormula = checkTask.getFormula();
std::unique_ptr<CheckResult> subResultPointer = this->check(eventuallyFormula.getSubformula());
ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult();
@ -124,17 +124,17 @@ namespace storm {
ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult();
storm::storage::SparseMatrix<ValueType> probabilityMatrix = storm::modelchecker::helper::SparseCtmcCslHelper::computeProbabilityMatrix(this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector());
std::vector<ValueType> numericResult = storm::modelchecker::helper::SparseCtmcCslHelper::computeLongRunAverageProbabilities(probabilityMatrix, subResult.getTruthValuesVector(), &this->getModel().getExitRateVector(), checkTask.isQualitativeSet(), *linearEquationSolverFactory);
std::vector<ValueType> numericResult = storm::modelchecker::helper::SparseCtmcCslHelper::computeLongRunAverageProbabilities(probabilityMatrix, subResult.getTruthValuesVector(), &this->getModel().getExitRateVector(), *linearEquationSolverFactory);
return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(std::move(numericResult)));
}
template <typename SparseCtmcModelType>
std::unique_ptr<CheckResult> SparseCtmcCslModelChecker<SparseCtmcModelType>::computeReachabilityTimes(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::EventuallyFormula, ValueType> const& checkTask) {
std::unique_ptr<CheckResult> SparseCtmcCslModelChecker<SparseCtmcModelType>::computeReachabilityTimes(storm::logic::RewardMeasureType, CheckTask<storm::logic::EventuallyFormula, ValueType> const& checkTask) {
storm::logic::EventuallyFormula const& eventuallyFormula = checkTask.getFormula();
std::unique_ptr<CheckResult> subResultPointer = this->check(eventuallyFormula.getSubformula());
ExplicitQualitativeCheckResult& subResult = subResultPointer->asExplicitQualitativeCheckResult();
std::vector<ValueType> numericResult = storm::modelchecker::helper::SparseCtmcCslHelper::computeReachabilityTimes(this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), this->getModel().getExitRateVector(), this->getModel().getInitialStates(), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *linearEquationSolverFactory);
std::vector<ValueType> numericResult = storm::modelchecker::helper::SparseCtmcCslHelper::computeReachabilityTimes(this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), this->getModel().getExitRateVector(), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *linearEquationSolverFactory);
return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(std::move(numericResult)));
}

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

@ -80,14 +80,14 @@ namespace storm {
}
template<typename SparseMarkovAutomatonModelType>
std::unique_ptr<CheckResult> SparseMarkovAutomatonCslModelChecker<SparseMarkovAutomatonModelType>::computeReachabilityRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::EventuallyFormula, ValueType> const& checkTask) {
std::unique_ptr<CheckResult> SparseMarkovAutomatonCslModelChecker<SparseMarkovAutomatonModelType>::computeReachabilityRewards(storm::logic::RewardMeasureType, CheckTask<storm::logic::EventuallyFormula, ValueType> const& checkTask) {
storm::logic::EventuallyFormula const& eventuallyFormula = checkTask.getFormula();
STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model.");
STORM_LOG_THROW(this->getModel().isClosed(), storm::exceptions::InvalidPropertyException, "Unable to compute reachability rewards in non-closed Markov automaton.");
std::unique_ptr<CheckResult> subResultPointer = this->check(eventuallyFormula.getSubformula());
ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult();
std::vector<ValueType> result = storm::modelchecker::helper::SparseMarkovAutomatonCslHelper<ValueType>::computeReachabilityRewards(checkTask.getOptimizationDirection(), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), this->getModel().getExitRates(), this->getModel().getMarkovianStates(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *minMaxLinearEquationSolverFactory);
std::vector<ValueType> result = storm::modelchecker::helper::SparseMarkovAutomatonCslHelper<ValueType>::computeReachabilityRewards(checkTask.getOptimizationDirection(), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), this->getModel().getExitRates(), this->getModel().getMarkovianStates(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), subResult.getTruthValuesVector(), *minMaxLinearEquationSolverFactory);
return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(std::move(result)));
}
@ -100,19 +100,19 @@ namespace storm {
std::unique_ptr<CheckResult> subResultPointer = this->check(stateFormula);
ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult();
std::vector<ValueType> result = storm::modelchecker::helper::SparseMarkovAutomatonCslHelper<ValueType>::computeLongRunAverageProbabilities(checkTask.getOptimizationDirection(), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), this->getModel().getExitRates(), this->getModel().getMarkovianStates(), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *minMaxLinearEquationSolverFactory);
std::vector<ValueType> result = storm::modelchecker::helper::SparseMarkovAutomatonCslHelper<ValueType>::computeLongRunAverageProbabilities(checkTask.getOptimizationDirection(), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), this->getModel().getExitRates(), this->getModel().getMarkovianStates(), subResult.getTruthValuesVector(), *minMaxLinearEquationSolverFactory);
return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(std::move(result)));
}
template<typename SparseMarkovAutomatonModelType>
std::unique_ptr<CheckResult> SparseMarkovAutomatonCslModelChecker<SparseMarkovAutomatonModelType>::computeReachabilityTimes(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::EventuallyFormula, ValueType> const& checkTask) {
std::unique_ptr<CheckResult> SparseMarkovAutomatonCslModelChecker<SparseMarkovAutomatonModelType>::computeReachabilityTimes(storm::logic::RewardMeasureType, CheckTask<storm::logic::EventuallyFormula, ValueType> const& checkTask) {
storm::logic::EventuallyFormula const& eventuallyFormula = checkTask.getFormula();
STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model.");
STORM_LOG_THROW(this->getModel().isClosed(), storm::exceptions::InvalidPropertyException, "Unable to compute expected times in non-closed Markov automaton.");
std::unique_ptr<CheckResult> subResultPointer = this->check(eventuallyFormula.getSubformula());
ExplicitQualitativeCheckResult& subResult = subResultPointer->asExplicitQualitativeCheckResult();
std::vector<ValueType> result = storm::modelchecker::helper::SparseMarkovAutomatonCslHelper<ValueType>::computeTimes(checkTask.getOptimizationDirection(), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), this->getModel().getExitRates(), this->getModel().getMarkovianStates(), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *minMaxLinearEquationSolverFactory);
std::vector<ValueType> result = storm::modelchecker::helper::SparseMarkovAutomatonCslHelper<ValueType>::computeTimes(checkTask.getOptimizationDirection(), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), this->getModel().getExitRates(), this->getModel().getMarkovianStates(), subResult.getTruthValuesVector(), *minMaxLinearEquationSolverFactory);
return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(std::move(result)));
}

12
src/storm/modelchecker/csl/helper/HybridCtmcCslHelper.cpp
View File

@ -28,17 +28,17 @@ namespace storm {
template<storm::dd::DdType DdType, class ValueType>
std::unique_ptr<CheckResult> HybridCtmcCslHelper<DdType, ValueType>::computeReachabilityRewards(storm::models::symbolic::Ctmc<DdType, ValueType> const& model, storm::dd::Add<DdType, ValueType> const& rateMatrix, storm::dd::Add<DdType, ValueType> const& exitRateVector, RewardModelType const& rewardModel, storm::dd::Bdd<DdType> const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory) {
return HybridDtmcPrctlHelper<DdType, ValueType>::computeReachabilityRewards(model, computeProbabilityMatrix(model, rateMatrix, exitRateVector), rewardModel.divideStateRewardVector(exitRateVector), targetStates, qualitative, linearEquationSolverFactory);
return HybridDtmcPrctlHelper<DdType, ValueType>::computeReachabilityRewards(model, computeProbabilityMatrix(rateMatrix, exitRateVector), rewardModel.divideStateRewardVector(exitRateVector), targetStates, qualitative, linearEquationSolverFactory);
}
template<storm::dd::DdType DdType, class ValueType>
std::unique_ptr<CheckResult> HybridCtmcCslHelper<DdType, ValueType>::computeNextProbabilities(storm::models::symbolic::Ctmc<DdType, ValueType> const& model, storm::dd::Add<DdType, ValueType> const& rateMatrix, storm::dd::Add<DdType, ValueType> const& exitRateVector, storm::dd::Bdd<DdType> const& nextStates) {
return HybridDtmcPrctlHelper<DdType, ValueType>::computeNextProbabilities(model, computeProbabilityMatrix(model, rateMatrix, exitRateVector), nextStates);
return HybridDtmcPrctlHelper<DdType, ValueType>::computeNextProbabilities(model, computeProbabilityMatrix(rateMatrix, exitRateVector), nextStates);
}
template<storm::dd::DdType DdType, class ValueType>
std::unique_ptr<CheckResult> HybridCtmcCslHelper<DdType, ValueType>::computeUntilProbabilities(storm::models::symbolic::Ctmc<DdType, ValueType> const& model, storm::dd::Add<DdType, ValueType> const& rateMatrix, storm::dd::Add<DdType, ValueType> const& exitRateVector, storm::dd::Bdd<DdType> const& phiStates, storm::dd::Bdd<DdType> const& psiStates, bool qualitative, storm::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory) {
return HybridDtmcPrctlHelper<DdType, ValueType>::computeUntilProbabilities(model, computeProbabilityMatrix(model, rateMatrix, exitRateVector), phiStates, psiStates, qualitative, linearEquationSolverFactory);
return HybridDtmcPrctlHelper<DdType, ValueType>::computeUntilProbabilities(model, computeProbabilityMatrix(rateMatrix, exitRateVector), phiStates, psiStates, qualitative, linearEquationSolverFactory);
}
template<storm::dd::DdType DdType, class ValueType>
@ -277,7 +277,7 @@ namespace storm {
template<storm::dd::DdType DdType, class ValueType>
std::unique_ptr<CheckResult> HybridCtmcCslHelper<DdType, ValueType>::computeLongRunAverageProbabilities(storm::models::symbolic::Ctmc<DdType, ValueType> const& model, storm::dd::Add<DdType, ValueType> const& rateMatrix, storm::dd::Add<DdType, ValueType> const& exitRateVector, storm::dd::Bdd<DdType> const& psiStates, bool qualitative, storm::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory) {
storm::dd::Add<DdType, ValueType> probabilityMatrix = computeProbabilityMatrix(model, rateMatrix, exitRateVector);
storm::dd::Add<DdType, ValueType> probabilityMatrix = computeProbabilityMatrix(rateMatrix, exitRateVector);
// Create ODD for the translation.
storm::dd::Odd odd = model.getReachableStates().createOdd();
@ -285,7 +285,7 @@ namespace storm {
storm::storage::SparseMatrix<ValueType> explicitProbabilityMatrix = probabilityMatrix.toMatrix(odd, odd);
std::vector<ValueType> explicitExitRateVector = exitRateVector.toVector(odd);
std::vector<ValueType> result = storm::modelchecker::helper::SparseCtmcCslHelper::computeLongRunAverageProbabilities(explicitProbabilityMatrix, psiStates.toVector(odd), &explicitExitRateVector, qualitative, linearEquationSolverFactory);
std::vector<ValueType> result = storm::modelchecker::helper::SparseCtmcCslHelper::computeLongRunAverageProbabilities(explicitProbabilityMatrix, psiStates.toVector(odd), &explicitExitRateVector, linearEquationSolverFactory);
return std::unique_ptr<CheckResult>(new HybridQuantitativeCheckResult<DdType>(model.getReachableStates(), model.getManager().getBddZero(), model.getManager().template getAddZero<ValueType>(), model.getReachableStates(), std::move(odd), std::move(result)));
}
@ -309,7 +309,7 @@ namespace storm {
}
template<storm::dd::DdType DdType, class ValueType>
storm::dd::Add<DdType, ValueType> HybridCtmcCslHelper<DdType, ValueType>::computeProbabilityMatrix(storm::models::symbolic::Ctmc<DdType, ValueType> const& model, storm::dd::Add<DdType, ValueType> const& rateMatrix, storm::dd::Add<DdType, ValueType> const& exitRateVector) {
storm::dd::Add<DdType, ValueType> HybridCtmcCslHelper<DdType, ValueType>::computeProbabilityMatrix(storm::dd::Add<DdType, ValueType> const& rateMatrix, storm::dd::Add<DdType, ValueType> const& exitRateVector) {
return rateMatrix / exitRateVector;
}

3
src/storm/modelchecker/csl/helper/HybridCtmcCslHelper.h
View File

@ -40,12 +40,11 @@ namespace storm {
* @param exitRateVector The exit rate vector of the model.
* @return The probability matrix.
*/
static storm::dd::Add<DdType, ValueType> computeProbabilityMatrix(storm::models::symbolic::Ctmc<DdType, ValueType> const& model, storm::dd::Add<DdType, ValueType> const& rateMatrix, storm::dd::Add<DdType, ValueType> const& exitRateVector);
static storm::dd::Add<DdType, ValueType> computeProbabilityMatrix(storm::dd::Add<DdType, ValueType> const& rateMatrix, storm::dd::Add<DdType, ValueType> const& exitRateVector);
/*!
* Computes the matrix representing the transitions of the uniformized CTMC.
*
* @param model The symbolic model.
* @param transitionMatrix The matrix to uniformize.
* @param exitRateVector The exit rate vector.
* @param maybeStates The states that need to be considered.

20
src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp
View File

@ -192,7 +192,7 @@ namespace storm {
}
template <typename ValueType, typename std::enable_if<!storm::NumberTraits<ValueType>::SupportsExponential, int>::type>
std::vector<ValueType> SparseCtmcCslHelper::computeBoundedUntilProbabilities(storm::storage::SparseMatrix<ValueType> const& rateMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, std::vector<ValueType> const& exitRates, bool qualitative, double lowerBound, double upperBound, storm::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory) {
std::vector<ValueType> SparseCtmcCslHelper::computeBoundedUntilProbabilities(storm::storage::SparseMatrix<ValueType> const&, storm::storage::SparseMatrix<ValueType> const&, storm::storage::BitVector const&, storm::storage::BitVector const&, std::vector<ValueType> const&, bool, double, double, storm::solver::LinearEquationSolverFactory<ValueType> const&) {
STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Computing bounded until probabilities is unsupported for this value type.");
}
@ -233,7 +233,7 @@ namespace storm {
}
template <typename ValueType, typename RewardModelType, typename std::enable_if<!storm::NumberTraits<ValueType>::SupportsExponential, int>::type>
std::vector<ValueType> SparseCtmcCslHelper::computeInstantaneousRewards(storm::storage::SparseMatrix<ValueType> const& rateMatrix, std::vector<ValueType> const& exitRateVector, RewardModelType const& rewardModel, double timeBound, storm::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory) {
std::vector<ValueType> SparseCtmcCslHelper::computeInstantaneousRewards(storm::storage::SparseMatrix<ValueType> const&, std::vector<ValueType> const&, RewardModelType const&, double, storm::solver::LinearEquationSolverFactory<ValueType> const&) {
STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Computing instantaneous rewards is unsupported for this value type.");
}
@ -274,7 +274,7 @@ namespace storm {
}
template <typename ValueType>
std::vector<ValueType> SparseCtmcCslHelper::computeReachabilityTimes(storm::storage::SparseMatrix<ValueType> const& rateMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, std::vector<ValueType> const& exitRateVector, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory) {
std::vector<ValueType> SparseCtmcCslHelper::computeReachabilityTimes(storm::storage::SparseMatrix<ValueType> const& rateMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, std::vector<ValueType> const& exitRateVector, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory) {
// Compute expected time on CTMC by reduction to DTMC with rewards.
storm::storage::SparseMatrix<ValueType> probabilityMatrix = computeProbabilityMatrix(rateMatrix, exitRateVector);
@ -330,7 +330,7 @@ namespace storm {
}
template <typename ValueType>
std::vector<ValueType> SparseCtmcCslHelper::computeLongRunAverageProbabilities(storm::storage::SparseMatrix<ValueType> const& probabilityMatrix, storm::storage::BitVector const& psiStates, std::vector<ValueType> const* exitRateVector, bool qualitative, storm::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory) {
std::vector<ValueType> SparseCtmcCslHelper::computeLongRunAverageProbabilities(storm::storage::SparseMatrix<ValueType> const& probabilityMatrix, storm::storage::BitVector const& psiStates, std::vector<ValueType> const* exitRateVector, storm::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory) {
// If there are no goal states, we avoid the computation and directly return zero.
uint_fast64_t numberOfStates = probabilityMatrix.getRowCount();
if (psiStates.empty()) {
@ -695,11 +695,11 @@ namespace storm {
template std::vector<double> SparseCtmcCslHelper::computeInstantaneousRewards(storm::storage::SparseMatrix<double> const& rateMatrix, std::vector<double> const& exitRateVector, storm::models::sparse::StandardRewardModel<double> const& rewardModel, double timeBound, storm::solver::LinearEquationSolverFactory<double> const& linearEquationSolverFactory);
template std::vector<double> SparseCtmcCslHelper::computeReachabilityTimes(storm::storage::SparseMatrix<double> const& rateMatrix, storm::storage::SparseMatrix<double> const& backwardTransitions, std::vector<double> const& exitRateVector, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory<double> const& linearEquationSolverFactory);
template std::vector<double> SparseCtmcCslHelper::computeReachabilityTimes(storm::storage::SparseMatrix<double> const& rateMatrix, storm::storage::SparseMatrix<double> const& backwardTransitions, std::vector<double> const& exitRateVector, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory<double> const& linearEquationSolverFactory);
template std::vector<double> SparseCtmcCslHelper::computeReachabilityRewards(storm::storage::SparseMatrix<double> const& rateMatrix, storm::storage::SparseMatrix<double> const& backwardTransitions, std::vector<double> const& exitRateVector, storm::models::sparse::StandardRewardModel<double> const& rewardModel, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory<double> const& linearEquationSolverFactory);
template std::vector<double> SparseCtmcCslHelper::computeLongRunAverageProbabilities(storm::storage::SparseMatrix<double> const& probabilityMatrix, storm::storage::BitVector const& psiStates, std::vector<double> const* exitRateVector, bool qualitative, storm::solver::LinearEquationSolverFactory<double> const& linearEquationSolverFactory);
template std::vector<double> SparseCtmcCslHelper::computeLongRunAverageProbabilities(storm::storage::SparseMatrix<double> const& probabilityMatrix, storm::storage::BitVector const& psiStates, std::vector<double> const* exitRateVector, storm::solver::LinearEquationSolverFactory<double> const& linearEquationSolverFactory);
template std::vector<double> SparseCtmcCslHelper::computeCumulativeRewards(storm::storage::SparseMatrix<double> const& rateMatrix, std::vector<double> const& exitRateVector, storm::models::sparse::StandardRewardModel<double> const& rewardModel, double timeBound, storm::solver::LinearEquationSolverFactory<double> const& linearEquationSolverFactory);
@ -720,14 +720,14 @@ namespace storm {
template std::vector<storm::RationalNumber> SparseCtmcCslHelper::computeInstantaneousRewards(storm::storage::SparseMatrix<storm::RationalNumber> const& rateMatrix, std::vector<storm::RationalNumber> const& exitRateVector, storm::models::sparse::StandardRewardModel<storm::RationalNumber> const& rewardModel, double timeBound, storm::solver::LinearEquationSolverFactory<storm::RationalNumber> const& linearEquationSolverFactory);
template std::vector<storm::RationalFunction> SparseCtmcCslHelper::computeInstantaneousRewards(storm::storage::SparseMatrix<storm::RationalFunction> const& rateMatrix, std::vector<storm::RationalFunction> const& exitRateVector, storm::models::sparse::StandardRewardModel<storm::RationalFunction> const& rewardModel, double timeBound, storm::solver::LinearEquationSolverFactory<storm::RationalFunction> const& linearEquationSolverFactory);
template std::vector<storm::RationalNumber> SparseCtmcCslHelper::computeReachabilityTimes(storm::storage::SparseMatrix<storm::RationalNumber> const& rateMatrix, storm::storage::SparseMatrix<storm::RationalNumber> const& backwardTransitions, std::vector<storm::RationalNumber> const& exitRateVector, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory<storm::RationalNumber> const& linearEquationSolverFactory);
template std::vector<storm::RationalFunction> SparseCtmcCslHelper::computeReachabilityTimes(storm::storage::SparseMatrix<storm::RationalFunction> const& rateMatrix, storm::storage::SparseMatrix<storm::RationalFunction> const& backwardTransitions, std::vector<storm::RationalFunction> const& exitRateVector, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory<storm::RationalFunction> const& linearEquationSolverFactory);
template std::vector<storm::RationalNumber> SparseCtmcCslHelper::computeReachabilityTimes(storm::storage::SparseMatrix<storm::RationalNumber> const& rateMatrix, storm::storage::SparseMatrix<storm::RationalNumber> const& backwardTransitions, std::vector<storm::RationalNumber> const& exitRateVector, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory<storm::RationalNumber> const& linearEquationSolverFactory);
template std::vector<storm::RationalFunction> SparseCtmcCslHelper::computeReachabilityTimes(storm::storage::SparseMatrix<storm::RationalFunction> const& rateMatrix, storm::storage::SparseMatrix<storm::RationalFunction> const& backwardTransitions, std::vector<storm::RationalFunction> const& exitRateVector, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory<storm::RationalFunction> const& linearEquationSolverFactory);
template std::vector<storm::RationalNumber> SparseCtmcCslHelper::computeReachabilityRewards(storm::storage::SparseMatrix<storm::RationalNumber> const& rateMatrix, storm::storage::SparseMatrix<storm::RationalNumber> const& backwardTransitions, std::vector<storm::RationalNumber> const& exitRateVector, storm::models::sparse::StandardRewardModel<storm::RationalNumber> const& rewardModel, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory<storm::RationalNumber> const& linearEquationSolverFactory);
template std::vector<storm::RationalFunction> SparseCtmcCslHelper::computeReachabilityRewards(storm::storage::SparseMatrix<storm::RationalFunction> const& rateMatrix, storm::storage::SparseMatrix<storm::RationalFunction> const& backwardTransitions, std::vector<storm::RationalFunction> const& exitRateVector, storm::models::sparse::StandardRewardModel<storm::RationalFunction> const& rewardModel, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory<storm::RationalFunction> const& linearEquationSolverFactory);
template std::vector<storm::RationalNumber> SparseCtmcCslHelper::computeLongRunAverageProbabilities(storm::storage::SparseMatrix<storm::RationalNumber> const& probabilityMatrix, storm::storage::BitVector const& psiStates, std::vector<storm::RationalNumber> const* exitRateVector, bool qualitative, storm::solver::LinearEquationSolverFactory<storm::RationalNumber> const& linearEquationSolverFactory);
template std::vector<storm::RationalFunction> SparseCtmcCslHelper::computeLongRunAverageProbabilities(storm::storage::SparseMatrix<storm::RationalFunction> const& probabilityMatrix, storm::storage::BitVector const& psiStates, std::vector<storm::RationalFunction> const* exitRateVector, bool qualitative, storm::solver::LinearEquationSolverFactory<storm::RationalFunction> const& linearEquationSolverFactory);
template std::vector<storm::RationalNumber> SparseCtmcCslHelper::computeLongRunAverageProbabilities(storm::storage::SparseMatrix<storm::RationalNumber> const& probabilityMatrix, storm::storage::BitVector const& psiStates, std::vector<storm::RationalNumber> const* exitRateVector, storm::solver::LinearEquationSolverFactory<storm::RationalNumber> const& linearEquationSolverFactory);
template std::vector<storm::RationalFunction> SparseCtmcCslHelper::computeLongRunAverageProbabilities(storm::storage::SparseMatrix<storm::RationalFunction> const& probabilityMatrix, storm::storage::BitVector const& psiStates, std::vector<storm::RationalFunction> const* exitRateVector, storm::solver::LinearEquationSolverFactory<storm::RationalFunction> const& linearEquationSolverFactory);
template std::vector<storm::RationalNumber> SparseCtmcCslHelper::computeCumulativeRewards(storm::storage::SparseMatrix<storm::RationalNumber> const& rateMatrix, std::vector<storm::RationalNumber> const& exitRateVector, storm::models::sparse::StandardRewardModel<storm::RationalNumber> const& rewardModel, double timeBound, storm::solver::LinearEquationSolverFactory<storm::RationalNumber> const& linearEquationSolverFactory);
template std::vector<storm::RationalFunction> SparseCtmcCslHelper::computeCumulativeRewards(storm::storage::SparseMatrix<storm::RationalFunction> const& rateMatrix, std::vector<storm::RationalFunction> const& exitRateVector, storm::models::sparse::StandardRewardModel<storm::RationalFunction> const& rewardModel, double timeBound, storm::solver::LinearEquationSolverFactory<storm::RationalFunction> const& linearEquationSolverFactory);

4
src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.h
View File

@ -43,10 +43,10 @@ namespace storm {
static std::vector<ValueType> computeReachabilityRewards(storm::storage::SparseMatrix<ValueType> const& rateMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, std::vector<ValueType> const& exitRateVector, RewardModelType const& rewardModel, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory);
template <typename ValueType>
static std::vector<ValueType> computeLongRunAverageProbabilities(storm::storage::SparseMatrix<ValueType> const& probabilityMatrix, storm::storage::BitVector const& psiStates, std::vector<ValueType> const* exitRateVector, bool qualitative, storm::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory);
static std::vector<ValueType> computeLongRunAverageProbabilities(storm::storage::SparseMatrix<ValueType> const& probabilityMatrix, storm::storage::BitVector const& psiStates, std::vector<ValueType> const* exitRateVector, storm::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory);
template <typename ValueType>
static std::vector<ValueType> computeReachabilityTimes(storm::storage::SparseMatrix<ValueType> const& rateMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, std::vector<ValueType> const& exitRateVector, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory);
static std::vector<ValueType> computeReachabilityTimes(storm::storage::SparseMatrix<ValueType> const& rateMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, std::vector<ValueType> const& exitRateVector, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory);
/*!
* Computes the matrix representing the transitions of the uniformized CTMC.

15
src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp
View File

@ -31,7 +31,7 @@ namespace storm {
namespace helper {
template<typename ValueType>
void SparseMarkovAutomatonCslHelper<ValueType>::computeBoundedReachabilityProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, std::vector<ValueType> const& exitRates, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& goalStates, storm::storage::BitVector const& markovianNonGoalStates, storm::storage::BitVector const& probabilisticNonGoalStates, std::vector<ValueType>& markovianNonGoalValues, std::vector<ValueType>& probabilisticNonGoalValues, ValueType delta, uint_fast64_t numberOfSteps, storm::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory) {
void SparseMarkovAutomatonCslHelper<ValueType>::computeBoundedReachabilityProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, std::vector<ValueType> const& exitRates, storm::storage::BitVector const& goalStates, storm::storage::BitVector const& markovianNonGoalStates, storm::storage::BitVector const& probabilisticNonGoalStates, std::vector<ValueType>& markovianNonGoalValues, std::vector<ValueType>& probabilisticNonGoalValues, ValueType delta, uint_fast64_t numberOfSteps, storm::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory) {
// Start by computing four sparse matrices:
// * a matrix aMarkovian with all (discretized) transitions from Markovian non-goal states to all Markovian non-goal states.
@ -145,7 +145,7 @@ namespace storm {
std::vector<ValueType> vProbabilistic(probabilisticNonGoalStates.getNumberOfSetBits());
std::vector<ValueType> vMarkovian(markovianNonGoalStates.getNumberOfSetBits());
computeBoundedReachabilityProbabilities(dir, transitionMatrix, exitRateVector, markovianStates, psiStates, markovianNonGoalStates, probabilisticNonGoalStates, vMarkovian, vProbabilistic, delta, numberOfSteps, minMaxLinearEquationSolverFactory);
computeBoundedReachabilityProbabilities(dir, transitionMatrix, exitRateVector, psiStates, markovianNonGoalStates, probabilisticNonGoalStates, vMarkovian, vProbabilistic, delta, numberOfSteps, minMaxLinearEquationSolverFactory);
// (4) If the lower bound of interval was non-zero, we need to take the current values as the starting values for a subsequent value iteration.
if (lowerBound != storm::utility::zero<ValueType>()) {
@ -163,7 +163,7 @@ namespace storm {
STORM_LOG_INFO("Performing " << numberOfSteps << " iterations (delta=" << delta << ") for interval [0, " << lowerBound << "]." << std::endl);
// Compute the bounded reachability for interval [0, b-a].
computeBoundedReachabilityProbabilities(dir, transitionMatrix, exitRateVector, markovianStates, storm::storage::BitVector(numberOfStates), markovianStates, ~markovianStates, vAllMarkovian, vAllProbabilistic, delta, numberOfSteps, minMaxLinearEquationSolverFactory);
computeBoundedReachabilityProbabilities(dir, transitionMatrix, exitRateVector, storm::storage::BitVector(numberOfStates), markovianStates, ~markovianStates, vAllMarkovian, vAllProbabilistic, delta, numberOfSteps, minMaxLinearEquationSolverFactory);
// Create the result vector out of vAllProbabilistic and vAllMarkovian and return it.
std::vector<ValueType> result(numberOfStates, storm::utility::zero<ValueType>());
@ -189,12 +189,13 @@ namespace storm {
template <typename ValueType>
template <typename RewardModelType>
std::vector<ValueType> SparseMarkovAutomatonCslHelper<ValueType>::computeReachabilityRewards(OptimizationDirection dir, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, std::vector<ValueType> const& exitRateVector, storm::storage::BitVector const& markovianStates, RewardModelType const& rewardModel, storm::storage::BitVector const& psiStates, bool qualitative, storm::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory) {
std::vector<ValueType> SparseMarkovAutomatonCslHelper<ValueType>::computeReachabilityRewards(OptimizationDirection dir, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, std::vector<ValueType> const& exitRateVector, storm::storage::BitVector const& markovianStates, RewardModelType const& rewardModel, storm::storage::BitVector const& psiStates, storm::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory) {
std::vector<ValueType> totalRewardVector = rewardModel.getTotalRewardVector(transitionMatrix.getRowCount(), transitionMatrix, storm::storage::BitVector(transitionMatrix.getRowGroupCount(), true));
return computeExpectedRewards(dir, transitionMatrix, backwardTransitions, exitRateVector, markovianStates, psiStates, totalRewardVector, minMaxLinearEquationSolverFactory);
}
template<typename ValueType>
std::vector<ValueType> SparseMarkovAutomatonCslHelper<ValueType>::computeLongRunAverageProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, std::vector<ValueType> const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory) {
std::vector<ValueType> SparseMarkovAutomatonCslHelper<ValueType>::computeLongRunAverageProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, std::vector<ValueType> const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates, storm::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory) {
uint_fast64_t numberOfStates = transitionMatrix.getRowGroupCount();
// If there are no goal states, we avoid the computation and directly return zero.
@ -349,7 +350,7 @@ namespace storm {
}
template <typename ValueType>
std::vector<ValueType> SparseMarkovAutomatonCslHelper<ValueType>::computeTimes(OptimizationDirection dir, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, std::vector<ValueType> const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory) {
std::vector<ValueType> SparseMarkovAutomatonCslHelper<ValueType>::computeTimes(OptimizationDirection dir, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, std::vector<ValueType> const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates, storm::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory) {
uint_fast64_t numberOfStates = transitionMatrix.getRowGroupCount();
std::vector<ValueType> rewardValues(numberOfStates, storm::utility::zero<ValueType>());
storm::utility::vector::setVectorValues(rewardValues, markovianStates, storm::utility::one<ValueType>());
@ -505,7 +506,7 @@ namespace storm {
}
template class SparseMarkovAutomatonCslHelper<double>;
template std::vector<double> SparseMarkovAutomatonCslHelper<double>::computeReachabilityRewards(OptimizationDirection dir, storm::storage::SparseMatrix<double> const& transitionMatrix, storm::storage::SparseMatrix<double> const& backwardTransitions, std::vector<double> const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::models::sparse::StandardRewardModel<double> const& rewardModel, storm::storage::BitVector const& psiStates, bool qualitative, storm::solver::MinMaxLinearEquationSolverFactory<double> const& minMaxLinearEquationSolverFactory);
template std::vector<double> SparseMarkovAutomatonCslHelper<double>::computeReachabilityRewards(OptimizationDirection dir, storm::storage::SparseMatrix<double> const& transitionMatrix, storm::storage::SparseMatrix<double> const& backwardTransitions, std::vector<double> const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::models::sparse::StandardRewardModel<double> const& rewardModel, storm::storage::BitVector const& psiStates, storm::solver::MinMaxLinearEquationSolverFactory<double> const& minMaxLinearEquationSolverFactory);
}
}

8
src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.h
View File

@ -19,15 +19,15 @@ namespace storm {
static std::vector<ValueType> computeUntilProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory);
template <typename RewardModelType>
static std::vector<ValueType> computeReachabilityRewards(OptimizationDirection dir, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, std::vector<ValueType> const& exitRateVector, storm::storage::BitVector const& markovianStates, RewardModelType const& rewardModel, storm::storage::BitVector const& psiStates, bool qualitative, storm::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory);
static std::vector<ValueType> computeReachabilityRewards(OptimizationDirection dir, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, std::vector<ValueType> const& exitRateVector, storm::storage::BitVector const& markovianStates, RewardModelType const& rewardModel, storm::storage::BitVector const& psiStates, storm::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory);
static std::vector<ValueType> computeLongRunAverageProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, std::vector<ValueType> const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory);
static std::vector<ValueType> computeLongRunAverageProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, std::vector<ValueType> const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates, storm::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory);
static std::vector<ValueType> computeTimes(OptimizationDirection dir, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, std::vector<ValueType> const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory);
static std::vector<ValueType> computeTimes(OptimizationDirection dir, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, std::vector<ValueType> const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates, storm::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory);
private:
static void computeBoundedReachabilityProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, std::vector<ValueType> const& exitRates, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& goalStates, storm::storage::BitVector const& markovianNonGoalStates, storm::storage::BitVector const& probabilisticNonGoalStates, std::vector<ValueType>& markovianNonGoalValues, std::vector<ValueType>& probabilisticNonGoalValues, ValueType delta, uint_fast64_t numberOfSteps, storm::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory);
static void computeBoundedReachabilityProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, std::vector<ValueType> const& exitRates, storm::storage::BitVector const& goalStates, storm::storage::BitVector const& markovianNonGoalStates, storm::storage::BitVector const& probabilisticNonGoalStates, std::vector<ValueType>& markovianNonGoalValues, std::vector<ValueType>& probabilisticNonGoalValues, ValueType delta, uint_fast64_t numberOfSteps, storm::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory);
/*!
* Computes the long-run average value for the given maximal end component of a Markov automaton.

2
src/storm/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp
View File

@ -112,7 +112,7 @@ namespace storm {
storm::storage::SparseMatrix<ValueType> explicitProbabilityMatrix = this->getModel().getTransitionMatrix().toMatrix(odd, odd);
std::vector<ValueType> result = storm::modelchecker::helper::SparseDtmcPrctlHelper<ValueType>::computeLongRunAverageProbabilities(explicitProbabilityMatrix, subResult.getTruthValuesVector().toVector(odd), checkTask.isQualitativeSet(), *this->linearEquationSolverFactory);
std::vector<ValueType> result = storm::modelchecker::helper::SparseDtmcPrctlHelper<ValueType>::computeLongRunAverageProbabilities(explicitProbabilityMatrix, subResult.getTruthValuesVector().toVector(odd), *this->linearEquationSolverFactory);
return std::unique_ptr<CheckResult>(new HybridQuantitativeCheckResult<DdType>(this->getModel().getReachableStates(), this->getModel().getManager().getBddZero(), this->getModel().getManager().template getAddZero<ValueType>(), this->getModel().getReachableStates(), std::move(odd), std::move(result)));
}

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

@ -111,7 +111,7 @@ namespace storm {
storm::logic::StateFormula const& stateFormula = checkTask.getFormula();
std::unique_ptr<CheckResult> subResultPointer = this->check(stateFormula);
ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult();
std::vector<ValueType> numericResult = storm::modelchecker::helper::SparseCtmcCslHelper::computeLongRunAverageProbabilities<ValueType>(this->getModel().getTransitionMatrix(), subResult.getTruthValuesVector(), nullptr, checkTask.isQualitativeSet(), *linearEquationSolverFactory);
std::vector<ValueType> numericResult = storm::modelchecker::helper::SparseCtmcCslHelper::computeLongRunAverageProbabilities<ValueType>(this->getModel().getTransitionMatrix(), subResult.getTruthValuesVector(), nullptr, *linearEquationSolverFactory);
return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(std::move(numericResult)));
}

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

@ -232,8 +232,8 @@ namespace storm {
}
template<typename ValueType, typename RewardModelType>
std::vector<ValueType> SparseDtmcPrctlHelper<ValueType, RewardModelType>::computeLongRunAverageProbabilities(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::BitVector const& psiStates, bool qualitative, storm::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory) {
return SparseCtmcCslHelper::computeLongRunAverageProbabilities<ValueType>(transitionMatrix, psiStates, nullptr, qualitative, linearEquationSolverFactory);
std::vector<ValueType> SparseDtmcPrctlHelper<ValueType, RewardModelType>::computeLongRunAverageProbabilities(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::BitVector const& psiStates, storm::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory) {
return SparseCtmcCslHelper::computeLongRunAverageProbabilities<ValueType>(transitionMatrix, psiStates, nullptr, linearEquationSolverFactory);
}
template<typename ValueType, typename RewardModelType>

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

@ -38,7 +38,7 @@ namespace storm {
static std::vector<ValueType> computeReachabilityRewards(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, std::vector<ValueType> const& totalStateRewardVector, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory, boost::optional<std::vector<ValueType>> resultHint = boost::none);
static std::vector<ValueType> computeLongRunAverageProbabilities(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::BitVector const& psiStates, bool qualitative, storm::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory);
static std::vector<ValueType> computeLongRunAverageProbabilities(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::BitVector const& psiStates, storm::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory);
static std::vector<ValueType> computeConditionalProbabilities(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& targetStates, storm::storage::BitVector const& conditionStates, bool qualitative, storm::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory);

2
src/storm/utility/storm.h
View File

@ -113,7 +113,7 @@ namespace storm {
std::vector<std::shared_ptr<storm::logic::Formula const>> parseFormulasForJaniModel(std::string const& inputString, storm::jani::Model const& model);
template<typename ValueType>
std::shared_ptr<storm::models::sparse::Model<ValueType>> buildSparseModel(storm::storage::SymbolicModelDescription const& model, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, bool onlyInitialStatesRelevant = false) {
std::shared_ptr<storm::models::sparse::Model<ValueType>> buildSparseModel(storm::storage::SymbolicModelDescription const& model, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas) {
storm::builder::BuilderOptions options(formulas);
if (storm::settings::getModule<storm::settings::modules::IOSettings>().isBuildFullModelSet()) {

Write Preview
Loading…
Cancel
Save