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

Initialize region before creating sample points

main
Jip Spel 6 years ago
parent
12e0ef537c
commit
b308f4e1d0
1 changed files with 28 additions and 26 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. 54
      src/storm-pars/analysis/MonotonicityChecker.cpp

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

@ -29,26 +29,10 @@ namespace storm {
this->formulas = formulas; this->formulas = formulas;
this->validate = validate; this->validate = validate;
this->precision = precision; this->precision = precision;
if (numberOfSamples > 0) {
// sampling
if (model->isOfType(storm::models::ModelType::Dtmc)) {
this->resultCheckOnSamples = std::map<typename utility::parametric::VariableType<ValueType>::type, std::pair<bool, bool>>(
checkOnSamples(model->as<storm::models::sparse::Dtmc<ValueType>>(), numberOfSamples));
} else if (model->isOfType(storm::models::ModelType::Mdp)) {
this->resultCheckOnSamples = std::map<typename utility::parametric::VariableType<ValueType>::type, std::pair<bool, bool>>(
checkOnSamples(model->as<storm::models::sparse::Mdp<ValueType>>(), numberOfSamples));
}
checkSamples= true;
} else {
checkSamples= false;
}
std::shared_ptr<storm::models::sparse::Model<ValueType>> sparseModel = model->as<storm::models::sparse::Model<ValueType>>(); std::shared_ptr<storm::models::sparse::Model<ValueType>> sparseModel = model->as<storm::models::sparse::Model<ValueType>>();
if (regions.size() == 1) { if (regions.size() == 1) {
region = *(regions.begin());
this->region = *(regions.begin());
} else { } else {
assert (regions.size() == 0); assert (regions.size() == 0);
typename storm::storage::ParameterRegion<ValueType>::Valuation lowerBoundaries; typename storm::storage::ParameterRegion<ValueType>::Valuation lowerBoundaries;
@ -61,7 +45,22 @@ namespace storm {
lowerBoundaries.insert(std::make_pair(var, lb)); lowerBoundaries.insert(std::make_pair(var, lb));
upperBoundaries.insert(std::make_pair(var, ub)); upperBoundaries.insert(std::make_pair(var, ub));
} }
region = storm::storage::ParameterRegion<ValueType>(std::move(lowerBoundaries), std::move(upperBoundaries));
this->region = storm::storage::ParameterRegion<ValueType>(std::move(lowerBoundaries), std::move(upperBoundaries));
}
if (numberOfSamples > 0) {
// sampling
if (model->isOfType(storm::models::ModelType::Dtmc)) {
this->resultCheckOnSamples = std::map<typename utility::parametric::VariableType<ValueType>::type, std::pair<bool, bool>>(
checkOnSamples(model->as<storm::models::sparse::Dtmc<ValueType>>(), numberOfSamples));
} else if (model->isOfType(storm::models::ModelType::Mdp)) {
this->resultCheckOnSamples = std::map<typename utility::parametric::VariableType<ValueType>::type, std::pair<bool, bool>>(
checkOnSamples(model->as<storm::models::sparse::Mdp<ValueType>>(), numberOfSamples));
}
checkSamples= true;
} else {
checkSamples= false;
} }
this->extender = new storm::analysis::OrderExtender<ValueType>(sparseModel); this->extender = new storm::analysis::OrderExtender<ValueType>(sparseModel);
@ -561,17 +560,20 @@ namespace storm {
for (auto itr2 = variables.begin(); itr2 != variables.end(); ++itr2) { for (auto itr2 = variables.begin(); itr2 != variables.end(); ++itr2) {
// Only change value for current variable // Only change value for current variable
if ((*itr) == (*itr2)) { if ((*itr) == (*itr2)) {
auto val = std::pair<typename utility::parametric::VariableType<ValueType>::type, typename utility::parametric::CoefficientType<ValueType>::type>(
(*itr2), storm::utility::convertNumber<typename utility::parametric::CoefficientType<ValueType>::type>(
boost::lexical_cast<std::string>((i + 1) / (double(numberOfSamples + 1)))));
auto lb = region.getLowerBoundary(itr->name());
auto ub = region.getUpperBoundary(itr->name());
// Creates samples between lb and ub, that is: lb, lb + (ub-lb)/(#samples -1), lb + 2* (ub-lb)/(#samples -1), ..., ub
auto val =
std::pair<typename utility::parametric::VariableType<ValueType>::type, typename utility::parametric::CoefficientType<ValueType>::type>
(*itr,utility::convertNumber<typename utility::parametric::CoefficientType<ValueType>::type>(lb + i*(ub-lb)/(numberOfSamples-1)));
valuation.insert(val); valuation.insert(val);
assert (0 < val.second && val.second < 1);
} else { } else {
auto val = std::pair<typename utility::parametric::VariableType<ValueType>::type, typename utility::parametric::CoefficientType<ValueType>::type>(
(*itr2), storm::utility::convertNumber<typename utility::parametric::CoefficientType<ValueType>::type>(
boost::lexical_cast<std::string>((1) / (double(numberOfSamples + 1)))));
auto lb = region.getLowerBoundary(itr->name());
auto val =
std::pair<typename utility::parametric::VariableType<ValueType>::type, typename utility::parametric::CoefficientType<ValueType>::type>
(*itr,utility::convertNumber<typename utility::parametric::CoefficientType<ValueType>::type>(lb));
valuation.insert(val); valuation.insert(val);
assert (0 < val.second && val.second < 1);
} }
} }
storm::models::sparse::Dtmc<double> sampleModel = instantiator.instantiate(valuation); storm::models::sparse::Dtmc<double> sampleModel = instantiator.instantiate(valuation);

Write Preview
Loading…
Cancel
Save