Browse Source

fixed compiling storm-pars cli and improved output a little

tempestpy_adaptions
TimQu 8 years ago
parent
commit
f2294fadb0
  1. 4
      src/storm-pars-cli/storm-pars.cpp
  2. 2
      src/storm-pars/modelchecker/region/ValidatingSparseParameterLiftingModelChecker.cpp
  3. 13
      src/storm-pars/modelchecker/results/RegionCheckResult.cpp

4
src/storm-pars-cli/storm-pars.cpp

@ -137,7 +137,7 @@ namespace storm {
template<typename ValueType>
void printInitialStatesResult(std::unique_ptr<storm::modelchecker::CheckResult> const& result, storm::jani::Property const& property, storm::utility::Stopwatch* watch = nullptr) {
if (result) {
STORM_PRINT_AND_LOG("Result (initial states): ");
STORM_PRINT_AND_LOG("Result (initial states): " << std::endl);
auto const* regionCheckResult = dynamic_cast<storm::modelchecker::RegionCheckResult<ValueType> const*>(result.get());
if (regionCheckResult != nullptr) {
@ -184,7 +184,7 @@ namespace storm {
verifyProperties<ValueType>(input.properties,
[&model] (std::shared_ptr<storm::logic::Formula const> const& formula) {
std::unique_ptr<storm::modelchecker::CheckResult> result = storm::api::verifyWithSparseEngine<ValueType>(model, storm::api::createTask<ValueType>(formula, true));
result->filter(storm::modelchecker::ExplicitQualitativeCheckResult(simplificationResult.first->getInitialStates()));
result->filter(storm::modelchecker::ExplicitQualitativeCheckResult(model->getInitialStates()));
return result;
},
[&model] (std::unique_ptr<storm::modelchecker::CheckResult> const& result) {

2
src/storm-pars/modelchecker/region/ValidatingSparseParameterLiftingModelChecker.cpp

@ -18,7 +18,7 @@ namespace storm {
template <typename SparseModelType, typename ImpreciseType, typename PreciseType>
ValidatingSparseParameterLiftingModelChecker<SparseModelType, ImpreciseType, PreciseType>::~ValidatingSparseParameterLiftingModelChecker() {
if (storm::settings::getModule<storm::settings::modules::CoreSettings>().isShowStatisticsSet()) {
STORM_PRINT_AND_LOG("Validating Parameter Lifting Model Checker detected " << numOfWrongRegions << " regions where the imprecise method was wrong.");
STORM_PRINT_AND_LOG("Validating Parameter Lifting Model Checker detected " << numOfWrongRegions << " regions where the imprecise method was wrong." << std::endl);
}
}

13
src/storm-pars/modelchecker/results/RegionCheckResult.cpp

@ -59,16 +59,19 @@ namespace storm {
for (auto const& res : this->regionResults) {
out << res.first.toString() << ": \t" << res.second << std::endl;
}
return out;
}
template<typename ValueType>
std::ostream& RegionCheckResult<ValueType>::writeCondensedToStream(std::ostream& out) const {
double satPercent = storm::utility::convertNumber<double>(satFraction) * 100.0;
double unsatPercent = storm::utility::convertNumber<double>(unsatFraction) * 100.0;
auto oneHundred = storm::utility::convertNumber<typename storm::storage::ParameterRegion<ValueType>::CoefficientType>(100.0);
auto one = storm::utility::convertNumber<typename storm::storage::ParameterRegion<ValueType>::CoefficientType>(1.0);
out << "Fraction of satisfied area: " << (satFraction * oneHundred) << std::endl;
out << "Fraction of unsatisfied area: " << (unsatFraction * oneHundred) << std::endl;
out << "Unknown fraction: " << ((one - satFraction - unsatFraction) * oneHundred) << std::endl;
out << "Total Number of regions: " << regionResults.size() << std::endl;
out << " Fraction of satisfied area: " << satPercent << "%" << std::endl;
out << "Fraction of unsatisfied area: " << unsatPercent << "%" << std::endl;
out << " Unknown fraction: " << (100.0 - satPercent - unsatPercent) << "%" << std::endl;
out << " Total number of regions: " << regionResults.size() << std::endl;
std::map<storm::modelchecker::RegionResult, uint_fast64_t> counters;
for (auto const& res : this->regionResults) {
++counters[res.second];
@ -76,11 +79,13 @@ namespace storm {
for (auto const& counter : counters) {
out << std::setw(28) << counter.first << ": " << counter.second << std::endl;
}
return out;
}
template<typename ValueType>
std::ostream& RegionCheckResult<ValueType>::writeIllustrationToStream(std::ostream& out) const {
STORM_LOG_WARN("Writing illustration of region check result to a stream is not implemented.");
return out;
}
template<typename ValueType>

Loading…
Cancel
Save