Browse Source

more output

tempestpy_adaptions
TimQu 7 years ago
parent
commit
7fe24e912e
  1. 18
      src/storm-pomdp-cli/storm-pomdp.cpp

18
src/storm-pomdp-cli/storm-pomdp.cpp

@ -133,13 +133,21 @@ int main(const int argc, const char** argv) {
storm::analysis::QualitativeAnalysis<storm::RationalNumber> qualitativeAnalysis(*pomdp); storm::analysis::QualitativeAnalysis<storm::RationalNumber> qualitativeAnalysis(*pomdp);
STORM_PRINT_AND_LOG("Computing states with probability 0 ..."); STORM_PRINT_AND_LOG("Computing states with probability 0 ...");
std::cout << qualitativeAnalysis.analyseProb0(formula->asProbabilityOperatorFormula()) << std::endl; std::cout << qualitativeAnalysis.analyseProb0(formula->asProbabilityOperatorFormula()) << std::endl;
STORM_PRINT_AND_LOG(" done." << std::endl);
STORM_PRINT_AND_LOG("Computing states with probability 1 ..."); STORM_PRINT_AND_LOG("Computing states with probability 1 ...");
std::cout << qualitativeAnalysis.analyseProb1(formula->asProbabilityOperatorFormula()) << std::endl; std::cout << qualitativeAnalysis.analyseProb1(formula->asProbabilityOperatorFormula()) << std::endl;
STORM_PRINT_AND_LOG(" done." << std::endl);
std::cout << "actual reduction not yet implemented..." << std::endl; std::cout << "actual reduction not yet implemented..." << std::endl;
} }
}
if (pomdpSettings.getMemoryBound() > 1) { if (pomdpSettings.getMemoryBound() > 1) {
STORM_PRINT_AND_LOG("Computing the unfolding for memory bound " << pomdpSettings.getMemoryBound() << "...");
storm::transformer::PomdpMemoryUnfolder<storm::RationalNumber> memoryUnfolder(*pomdp, pomdpSettings.getMemoryBound()); storm::transformer::PomdpMemoryUnfolder<storm::RationalNumber> memoryUnfolder(*pomdp, pomdpSettings.getMemoryBound());
pomdp = memoryUnfolder.transform(); pomdp = memoryUnfolder.transform();
STORM_PRINT_AND_LOG(" done." << std::endl);
pomdp->printModelInformationToStream(std::cout);
} else {
STORM_PRINT_AND_LOG("Assumming memoryless schedulers.")
} }
// From now on the pomdp is considered memoryless // From now on the pomdp is considered memoryless
@ -150,14 +158,18 @@ int main(const int argc, const char** argv) {
uint64_t oldChoiceCount = pomdp->getNumberOfChoices(); uint64_t oldChoiceCount = pomdp->getNumberOfChoices();
storm::transformer::GlobalPomdpMecChoiceEliminator<storm::RationalNumber> mecChoiceEliminator(*pomdp); storm::transformer::GlobalPomdpMecChoiceEliminator<storm::RationalNumber> mecChoiceEliminator(*pomdp);
pomdp = mecChoiceEliminator.transform(*formula); pomdp = mecChoiceEliminator.transform(*formula);
STORM_PRINT_AND_LOG(" done." << std::endl);
STORM_PRINT_AND_LOG(oldChoiceCount - pomdp->getNumberOfChoices() << " choices eliminated through MEC choice elimination." << std::endl); STORM_PRINT_AND_LOG(oldChoiceCount - pomdp->getNumberOfChoices() << " choices eliminated through MEC choice elimination." << std::endl);
} }
if (pomdpSettings.isExportToParametricSet()) { if (pomdpSettings.isExportToParametricSet()) {
STORM_PRINT_AND_LOG("Transforming memoryless POMDP to pMC...");
storm::transformer::ApplyFiniteSchedulerToPomdp<storm::RationalNumber> toPMCTransformer(*pomdp); storm::transformer::ApplyFiniteSchedulerToPomdp<storm::RationalNumber> toPMCTransformer(*pomdp);
auto const &pmc = toPMCTransformer.transform();
storm::analysis::ConstraintCollector<storm::RationalFunction> constraints(*pmc);
auto pmc = toPMCTransformer.transform();
STORM_PRINT_AND_LOG(" done." << std::endl);
pmc->printModelInformationToStream(std::cout); pmc->printModelInformationToStream(std::cout);
STORM_PRINT_AND_LOG("Exporting pMC...");
storm::analysis::ConstraintCollector<storm::RationalFunction> constraints(*pmc);
auto const& parameterSet = constraints.getVariables(); auto const& parameterSet = constraints.getVariables();
std::vector<storm::RationalFunctionVariable> parameters(parameterSet.begin(), parameterSet.end()); std::vector<storm::RationalFunctionVariable> parameters(parameterSet.begin(), parameterSet.end());
std::vector<std::string> parameterNames; std::vector<std::string> parameterNames;
@ -165,10 +177,10 @@ int main(const int argc, const char** argv) {
parameterNames.push_back(parameter.getName()); parameterNames.push_back(parameter.getName());
} }
storm::api::exportSparseModelAsDrn(pmc, pomdpSettings.getExportToParametricFilename(), parameterNames); storm::api::exportSparseModelAsDrn(pmc, pomdpSettings.getExportToParametricFilename(), parameterNames);
STORM_PRINT_AND_LOG(" done." << std::endl);
} }
} }
}
// All operations have now been performed, so we clean up everything and terminate. // All operations have now been performed, so we clean up everything and terminate.
storm::utility::cleanUp(); storm::utility::cleanUp();

Loading…
Cancel
Save