Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

iMC changes outside of storm-pars #627

Open
wants to merge 7 commits into
base: master
Choose a base branch
from
Open

iMC changes outside of storm-pars #627

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
7 commits
Select commit Hold shift + click to select a range
e6e6fdd
iMC changes outside of storm-pars
glatteis Nov 1, 2024
c1a741a
Remove commented out code
glatteis Nov 1, 2024
217c5a8
Fix iMDPs
glatteis Nov 12, 2024
b32ec4c
Format
glatteis Nov 12, 2024
2d7239c
Fix POMDP test segfault
glatteis Nov 18, 2024
0ee405b
Fix other POMDP test
glatteis Nov 18, 2024
76c1eeb
Move viCallback out of if
glatteis Dec 17, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
3 changes: 3 additions & 0 deletions src/storm/adapters/Z3ExpressionAdapter.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -166,6 +166,9 @@ storm::expressions::Expression Z3ExpressionAdapter::translateExpression(z3::expr
return manager.rational(storm::utility::convertNumber<storm::RationalNumber>(std::string(Z3_get_numeral_string(expr.ctx(), expr))));
}
}
case Z3_OP_AGNUM:
return manager.rational(storm::utility::convertNumber<storm::RationalNumber>(
std::string(Z3_get_numeral_string(expr.ctx(), Z3_get_algebraic_number_lower(expr.ctx(), expr, 16)))));
case Z3_OP_UNINTERPRETED:
// Currently, we only support uninterpreted constant functions.
STORM_LOG_THROW(expr.is_const(), storm::exceptions::ExpressionEvaluationException,
Expand Down
31 changes: 23 additions & 8 deletions src/storm/api/bisimulation.h
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,5 +1,6 @@
#pragma once

#include <any>
#include "storm/models/sparse/Ctmc.h"
#include "storm/models/sparse/Dtmc.h"
#include "storm/models/sparse/Mdp.h"
Expand All @@ -19,11 +20,18 @@ namespace api {
template<typename ModelType>
std::shared_ptr<ModelType> performDeterministicSparseBisimulationMinimization(std::shared_ptr<ModelType> model,
std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas,
storm::storage::BisimulationType type) {
storm::storage::BisimulationType type, bool graphPreserving = true) {
typename storm::storage::DeterministicModelBisimulationDecomposition<ModelType>::Options options;
if (!formulas.empty()) {
if (!formulas.empty() && graphPreserving) {
options = typename storm::storage::DeterministicModelBisimulationDecomposition<ModelType>::Options(*model, formulas);
}
// If we cannot use formula-based decomposition because of
// non-graph-preserving regions but there are reward models, we need to
// preserve those
if (!graphPreserving &&
std::any_of(formulas.begin(), formulas.end(), [](auto const& formula) { return formula->getReferencedRewardModels().size() > 0; })) {
options.setKeepRewards(true);
}
options.setType(type);

storm::storage::DeterministicModelBisimulationDecomposition<ModelType> bisimulationDecomposition(*model, options);
Expand All @@ -34,11 +42,18 @@ std::shared_ptr<ModelType> performDeterministicSparseBisimulationMinimization(st
template<typename ModelType>
std::shared_ptr<ModelType> performNondeterministicSparseBisimulationMinimization(std::shared_ptr<ModelType> model,
std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas,
storm::storage::BisimulationType type) {
storm::storage::BisimulationType type, bool graphPreserving = true) {
typename storm::storage::NondeterministicModelBisimulationDecomposition<ModelType>::Options options;
if (!formulas.empty()) {
if (!formulas.empty() && graphPreserving) {
options = typename storm::storage::NondeterministicModelBisimulationDecomposition<ModelType>::Options(*model, formulas);
}
// If we cannot use formula-based decomposition because of
// non-graph-preserving regions but there are reward models, we need to
// preserve those
if (!graphPreserving &&
std::any_of(formulas.begin(), formulas.end(), [](auto const& formula) { return formula->getReferencedRewardModels().size() > 0; })) {
options.setKeepRewards(true);
}
options.setType(type);

storm::storage::NondeterministicModelBisimulationDecomposition<ModelType> bisimulationDecomposition(*model, options);
Expand All @@ -49,7 +64,7 @@ std::shared_ptr<ModelType> performNondeterministicSparseBisimulationMinimization
template<typename ValueType>
std::shared_ptr<storm::models::sparse::Model<ValueType>> performBisimulationMinimization(
std::shared_ptr<storm::models::sparse::Model<ValueType>> const& model, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas,
storm::storage::BisimulationType type = storm::storage::BisimulationType::Strong) {
storm::storage::BisimulationType type = storm::storage::BisimulationType::Strong, bool graphPreserving = true) {
STORM_LOG_THROW(
model->isOfType(storm::models::ModelType::Dtmc) || model->isOfType(storm::models::ModelType::Ctmc) || model->isOfType(storm::models::ModelType::Mdp),
storm::exceptions::NotSupportedException, "Bisimulation minimization is currently only available for DTMCs, CTMCs and MDPs.");
Expand All @@ -59,13 +74,13 @@ std::shared_ptr<storm::models::sparse::Model<ValueType>> performBisimulationMini

if (model->isOfType(storm::models::ModelType::Dtmc)) {
return performDeterministicSparseBisimulationMinimization<storm::models::sparse::Dtmc<ValueType>>(
model->template as<storm::models::sparse::Dtmc<ValueType>>(), formulas, type);
model->template as<storm::models::sparse::Dtmc<ValueType>>(), formulas, type, graphPreserving);
} else if (model->isOfType(storm::models::ModelType::Ctmc)) {
return performDeterministicSparseBisimulationMinimization<storm::models::sparse::Ctmc<ValueType>>(
model->template as<storm::models::sparse::Ctmc<ValueType>>(), formulas, type);
model->template as<storm::models::sparse::Ctmc<ValueType>>(), formulas, type, graphPreserving);
} else {
return performNondeterministicSparseBisimulationMinimization<storm::models::sparse::Mdp<ValueType>>(
model->template as<storm::models::sparse::Mdp<ValueType>>(), formulas, type);
model->template as<storm::models::sparse::Mdp<ValueType>>(), formulas, type, graphPreserving);
}
}

Expand Down
10 changes: 8 additions & 2 deletions src/storm/logic/Bound.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -29,9 +29,15 @@ ValueType Bound::evaluateThresholdAs() const {
}

template bool Bound::isSatisfied(double const& compareValue) const;
template bool Bound::isSatisfied(storm::RationalNumber const& compareValue) const;
#if defined(STORM_HAVE_CLN)
template bool Bound::isSatisfied(storm::ClnRationalNumber const& compareValue) const;
template storm::ClnRationalNumber Bound::evaluateThresholdAs() const;
#endif
#if defined(STORM_HAVE_GMP)
template bool Bound::isSatisfied(storm::GmpRationalNumber const& compareValue) const;
template storm::GmpRationalNumber Bound::evaluateThresholdAs() const;
#endif
template double Bound::evaluateThresholdAs() const;
template storm::RationalNumber Bound::evaluateThresholdAs() const;
template storm::RationalFunction Bound::evaluateThresholdAs() const;

} // namespace storm::logic
Loading
Loading