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

Fix TODOs

tempestpy_adaptions
Jip Spel 5 years ago
parent
a39f297b8c
commit
ed3fa3f82b
5 changed files with 58 additions and 118 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Unified View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 110
      src/storm-pars-cli/storm-pars.cpp
  2. 2
      src/storm-pars/analysis/AssumptionChecker.cpp
  3. 5
      src/storm-pars/analysis/MonotonicityChecker.cpp
  4. 29
      src/storm-pars/analysis/OrderExtender.cpp
  5. 30
      src/storm-pars/api/region.h

110
src/storm-pars-cli/storm-pars.cpp
View File

@ -668,66 +668,72 @@ namespace storm {
if (model && monSettings.isSccEliminationSet()) { if (model && monSettings.isSccEliminationSet()) {
storm::utility::Stopwatch eliminationWatch(true); storm::utility::Stopwatch eliminationWatch(true);
// TODO: check for correct Model type
STORM_PRINT("Applying scc elimination" << std::endl);
auto sparseModel = model->as<storm::models::sparse::Model<ValueType>>();
auto matrix = sparseModel->getTransitionMatrix();
auto backwardsTransitionMatrix = matrix.transpose();
storm::storage::StronglyConnectedComponentDecompositionOptions const options;
auto decomposition = storm::storage::StronglyConnectedComponentDecomposition<ValueType>(matrix, options);
storm::storage::BitVector selectedStates(matrix.getRowCount());
storm::storage::BitVector selfLoopStates(matrix.getRowCount());
for (auto i = 0; i < decomposition.size(); ++i) {
auto scc = decomposition.getBlock(i);
if (scc.size() > 1) {
auto nrInitial = 0;
auto statesScc = scc.getStates();
std::vector<uint_fast64_t> entryStates;
for (auto state : statesScc) {
auto row = backwardsTransitionMatrix.getRow(state);
bool found = false;
for (auto backState : row) {
if (!scc.containsState(backState.getColumn())) {
found = true;
if (model->isOfType(storm::models::ModelType::Dtmc)) {
STORM_PRINT("Applying scc elimination" << std::endl);
auto sparseModel = model->as<storm::models::sparse::Model<ValueType>>();
auto matrix = sparseModel->getTransitionMatrix();
auto backwardsTransitionMatrix = matrix.transpose();
storm::storage::StronglyConnectedComponentDecompositionOptions const options;
auto decomposition = storm::storage::StronglyConnectedComponentDecomposition<ValueType>(matrix, options);
storm::storage::BitVector selectedStates(matrix.getRowCount());
storm::storage::BitVector selfLoopStates(matrix.getRowCount());
for (auto i = 0; i < decomposition.size(); ++i) {
auto scc = decomposition.getBlock(i);
if (scc.size() > 1) {
auto nrInitial = 0;
auto statesScc = scc.getStates();
std::vector<uint_fast64_t> entryStates;
for (auto state : statesScc) {
auto row = backwardsTransitionMatrix.getRow(state);
bool found = false;
for (auto backState : row) {
if (!scc.containsState(backState.getColumn())) {
found = true;
}
}
if (found) {
entryStates.push_back(state);
selfLoopStates.set(state);
} else {
selectedStates.set(state);
} }
} }
if (found) {
entryStates.push_back(state);
selfLoopStates.set(state);
} else {
selectedStates.set(state);
if (entryStates.size() != 1) {
STORM_LOG_THROW(entryStates.size() > 1, storm::exceptions::NotImplementedException,
"state elimination not implemented for scc with more than 1 entry points");
} }
} }
}
if (entryStates.size() != 1) {
STORM_LOG_THROW(entryStates.size() > 1, storm::exceptions::NotImplementedException,
"state elimination not implemented for scc with more than 1 entry points");
}
storm::storage::FlexibleSparseMatrix<ValueType> flexibleMatrix(matrix);
storm::storage::FlexibleSparseMatrix<ValueType> flexibleBackwardTransitions(backwardsTransitionMatrix, true);
auto actionRewards = std::vector<ValueType>(matrix.getRowCount(), storm::utility::zero<ValueType>());
storm::solver::stateelimination::NondeterministicModelStateEliminator<ValueType> stateEliminator(flexibleMatrix, flexibleBackwardTransitions, actionRewards);
for(auto state : selectedStates) {
stateEliminator.eliminateState(state, true);
}
for (auto state : selfLoopStates) {
auto row = flexibleMatrix.getRow(state);
stateEliminator.eliminateLoop(state);
} }
selectedStates.complement();
auto keptRows = matrix.getRowFilter(selectedStates);
storm::storage::SparseMatrix<ValueType> newTransitionMatrix = flexibleMatrix.createSparseMatrix(keptRows, selectedStates);
// TODO: note that rewards get lost
model = std::make_shared<storm::models::sparse::Dtmc<ValueType>>(std::move(newTransitionMatrix), sparseModel->getStateLabeling().getSubLabeling(selectedStates));
eliminationWatch.stop();
STORM_PRINT(std::endl << "Time for scc elimination: " << eliminationWatch << "." << std::endl << std::endl);
model->printModelInformationToStream(std::cout);
} else if (model->isOfType(storm::models::ModelType::Mdp)) {
STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Unable to perform SCC elimination for monotonicity analysis on MDP: Not mplemented");
} else {
STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Unable to perform monotonicity analysis on the provided model type.");
} }
storm::storage::FlexibleSparseMatrix<ValueType> flexibleMatrix(matrix);
storm::storage::FlexibleSparseMatrix<ValueType> flexibleBackwardTransitions(backwardsTransitionMatrix, true);
auto actionRewards = std::vector<ValueType>(matrix.getRowCount(), storm::utility::zero<ValueType>());
storm::solver::stateelimination::NondeterministicModelStateEliminator<ValueType> stateEliminator(flexibleMatrix, flexibleBackwardTransitions, actionRewards);
for(auto state : selectedStates) {
stateEliminator.eliminateState(state, true);
}
for (auto state : selfLoopStates) {
auto row = flexibleMatrix.getRow(state);
stateEliminator.eliminateLoop(state);
}
selectedStates.complement();
auto keptRows = matrix.getRowFilter(selectedStates);
storm::storage::SparseMatrix<ValueType> newTransitionMatrix = flexibleMatrix.createSparseMatrix(keptRows, selectedStates);
// TODO: rewards get lost
model = std::make_shared<storm::models::sparse::Dtmc<ValueType>>(std::move(newTransitionMatrix), sparseModel->getStateLabeling().getSubLabeling(selectedStates));
eliminationWatch.stop();
STORM_PRINT(std::endl << "Time for scc elimination: " << eliminationWatch << "." << std::endl << std::endl);
model->printModelInformationToStream(std::cout);
} }
std::vector<storm::storage::ParameterRegion<ValueType>> regions = parseRegions<ValueType>(model); std::vector<storm::storage::ParameterRegion<ValueType>> regions = parseRegions<ValueType>(model);

2
src/storm-pars/analysis/AssumptionChecker.cpp
View File

@ -32,9 +32,7 @@ namespace storm {
for (auto i = 0; i < numberOfSamples; ++i) { for (auto i = 0; i < numberOfSamples; ++i) {
auto valuation = utility::parametric::Valuation<ValueType>(); auto valuation = utility::parametric::Valuation<ValueType>();
// TODO: samplen over de region
for (auto var: variables) { for (auto var: variables) {
auto lb = region.getLowerBoundary(var.name()); auto lb = region.getLowerBoundary(var.name());
auto ub = region.getUpperBoundary(var.name()); auto ub = region.getUpperBoundary(var.name());
// Creates samples between lb and ub, that is: lb, lb + (ub-lb)/(#samples -1), lb + 2* (ub-lb)/(#samples -1), ..., ub // Creates samples between lb and ub, that is: lb, lb + (ub-lb)/(#samples -1), lb + 2* (ub-lb)/(#samples -1), ..., ub

5
src/storm-pars/analysis/MonotonicityChecker.cpp
View File

@ -194,13 +194,8 @@ namespace storm {
std::vector<double> minValues = minRes.getValueVector(); std::vector<double> minValues = minRes.getValueVector();
std::vector<double> maxValues = maxRes.getValueVector(); std::vector<double> maxValues = maxRes.getValueVector();
// TODO: zijn de value vectors nu precies omgedraaid?
// Create initial order // Create initial order
std::tuple<storm::analysis::Order*, uint_fast64_t, uint_fast64_t> criticalTuple = extender->toOrder(formulas, minValues, maxValues); std::tuple<storm::analysis::Order*, uint_fast64_t, uint_fast64_t> criticalTuple = extender->toOrder(formulas, minValues, maxValues);
// std::tuple<storm::analysis::Order*, uint_fast64_t, uint_fast64_t> criticalTuple = extender->toOrder(formulas);
// Continue based on not (yet) sorted states // Continue based on not (yet) sorted states
std::map<storm::analysis::Order*, std::vector<std::shared_ptr<storm::expressions::BinaryRelationExpression>>> result; std::map<storm::analysis::Order*, std::vector<std::shared_ptr<storm::expressions::BinaryRelationExpression>>> result;

29
src/storm-pars/analysis/OrderExtender.cpp
View File

@ -38,10 +38,8 @@ namespace storm {
uint_fast64_t numberOfStates = this->model->getNumberOfStates(); uint_fast64_t numberOfStates = this->model->getNumberOfStates();
// Build stateMap // Build stateMap
// TODO: is dit wel nodig
for (uint_fast64_t i = 0; i < numberOfStates; ++i) { for (uint_fast64_t i = 0; i < numberOfStates; ++i) {
stateMap[i] = new storm::storage::BitVector(numberOfStates, false); stateMap[i] = new storm::storage::BitVector(numberOfStates, false);
auto row = matrix.getRow(i); auto row = matrix.getRow(i);
for (auto rowItr = row.begin(); rowItr != row.end(); ++rowItr) { for (auto rowItr = row.begin(); rowItr != row.end(); ++rowItr) {
// ignore self-loops when there are more transitions // ignore self-loops when there are more transitions
@ -129,33 +127,6 @@ namespace storm {
template <typename ValueType> template <typename ValueType>
std::tuple<Order*, uint_fast64_t, uint_fast64_t> OrderExtender<ValueType>::toOrder(std::vector<std::shared_ptr<storm::logic::Formula const>> formulas, std::vector<double> minValues, std::vector<double> maxValues) { std::tuple<Order*, uint_fast64_t, uint_fast64_t> OrderExtender<ValueType>::toOrder(std::vector<std::shared_ptr<storm::logic::Formula const>> formulas, std::vector<double> minValues, std::vector<double> maxValues) {
uint_fast64_t numberOfStates = this->model->getNumberOfStates(); uint_fast64_t numberOfStates = this->model->getNumberOfStates();
//
// // Compare min/max for all states
// STORM_LOG_THROW((++formulas.begin()) == formulas.end(), storm::exceptions::NotSupportedException, "Only one formula allowed for monotonicity analysis");
// STORM_LOG_THROW((*(formulas[0])).isProbabilityOperatorFormula()
// && ((*(formulas[0])).asProbabilityOperatorFormula().getSubformula().isUntilFormula()
// || (*(formulas[0])).asProbabilityOperatorFormula().getSubformula().isEventuallyFormula()), storm::exceptions::NotSupportedException, "Expecting until or eventually formula");
//
// // TODO: dit moet anders kunnen
// storm::modelchecker::SparsePropositionalModelChecker<storm::models::sparse::Model<ValueType>> propositionalChecker(*model);
// storm::storage::BitVector phiStates;
// storm::storage::BitVector psiStates;
// if ((*(formulas[0])).asProbabilityOperatorFormula().getSubformula().isUntilFormula()) {
// phiStates = propositionalChecker.check((*(formulas[0])).asProbabilityOperatorFormula().getSubformula().asUntilFormula().getLeftSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector();
// psiStates = propositionalChecker.check((*(formulas[0])).asProbabilityOperatorFormula().getSubformula().asUntilFormula().getRightSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector();
// } else {
// phiStates = storm::storage::BitVector(numberOfStates, true);
// psiStates = propositionalChecker.check((*(formulas[0])).asProbabilityOperatorFormula().getSubformula().asEventuallyFormula().getSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector();
// }
//
// // Get the maybeStates
// std::pair<storm::storage::BitVector, storm::storage::BitVector> statesWithProbability01 = storm::utility::graph::performProb01(this->model->getBackwardTransitions(), phiStates, psiStates);
// storm::storage::BitVector topStates = statesWithProbability01.second;
// storm::storage::BitVector bottomStates = statesWithProbability01.first;
//
// STORM_LOG_THROW(topStates.begin() != topStates.end(), storm::exceptions::NotImplementedException, "Formula yields to no 1 states");
// STORM_LOG_THROW(bottomStates.begin() != bottomStates.end(), storm::exceptions::NotImplementedException, "Formula yields to no zero states");
//
uint_fast64_t bottom = numberOfStates; uint_fast64_t bottom = numberOfStates;
uint_fast64_t top = numberOfStates; uint_fast64_t top = numberOfStates;
std::vector<uint_fast64_t> statesSorted = storm::utility::graph::getTopologicalSort(matrix); std::vector<uint_fast64_t> statesSorted = storm::utility::graph::getTopologicalSort(matrix);

30
src/storm-pars/api/region.h
View File

@ -110,36 +110,6 @@ namespace storm {
return checker; return checker;
} }
// TODO: make more generic
template <typename ParametricType, typename ConstantType>
std::shared_ptr<storm::modelchecker::SparseDtmcParameterLiftingModelChecker<storm::models::sparse::Dtmc<ParametricType>, ConstantType>> initializeParameterLiftingDtmcModelChecker(Environment const& env, std::shared_ptr<storm::models::sparse::Model<ParametricType>> const& model, storm::modelchecker::CheckTask<storm::logic::Formula, ParametricType> const& task, bool generateSplitEstimates = false, bool allowModelSimplification = true) {
STORM_LOG_WARN_COND(storm::utility::parameterlifting::validateParameterLiftingSound(*model, task.getFormula()), "Could not validate whether parameter lifting is applicable. Please validate manually...");
std::shared_ptr<storm::models::sparse::Model<ParametricType>> consideredModel = model;
// Treat continuous time models
if (consideredModel->isOfType(storm::models::ModelType::Ctmc) || consideredModel->isOfType(storm::models::ModelType::MarkovAutomaton)) {
STORM_LOG_WARN("Parameter lifting not supported for continuous time models. Transforming continuous model to discrete model...");
std::vector<std::shared_ptr<storm::logic::Formula const>> taskFormulaAsVector { task.getFormula().asSharedPointer() };
consideredModel = storm::api::transformContinuousToDiscreteTimeSparseModel(consideredModel, taskFormulaAsVector).first;
STORM_LOG_THROW(consideredModel->isOfType(storm::models::ModelType::Dtmc) || consideredModel->isOfType(storm::models::ModelType::Mdp), storm::exceptions::UnexpectedException, "Transformation to discrete time model has failed.");
}
// Obtain the region model checker
std::shared_ptr<storm::modelchecker::SparseDtmcParameterLiftingModelChecker<storm::models::sparse::Dtmc<ParametricType>, ConstantType>> checker;
if (consideredModel->isOfType(storm::models::ModelType::Dtmc)) {
checker = std::make_shared<storm::modelchecker::SparseDtmcParameterLiftingModelChecker<storm::models::sparse::Dtmc<ParametricType>, ConstantType>>();
} else {
STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Unable to perform parameterLifting on the provided model type.");
}
checker->specify(env, consideredModel, task, generateSplitEstimates, allowModelSimplification);
return checker;
}
template <typename ParametricType, typename ImpreciseType, typename PreciseType> template <typename ParametricType, typename ImpreciseType, typename PreciseType>
std::shared_ptr<storm::modelchecker::RegionModelChecker<ParametricType>> initializeValidatingRegionModelChecker(Environment const& env, std::shared_ptr<storm::models::sparse::Model<ParametricType>> const& model, storm::modelchecker::CheckTask<storm::logic::Formula, ParametricType> const& task, bool generateSplitEstimates = false, bool allowModelSimplification = true) { std::shared_ptr<storm::modelchecker::RegionModelChecker<ParametricType>> initializeValidatingRegionModelChecker(Environment const& env, std::shared_ptr<storm::models::sparse::Model<ParametricType>> const& model, storm::modelchecker::CheckTask<storm::logic::Formula, ParametricType> const& task, bool generateSplitEstimates = false, bool allowModelSimplification = true) {

Write Preview
Loading…
Cancel
Save