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

better output

tempestpy_adaptions
Sebastian Junges 4 years ago
parent
1218991e6a
commit
85b676ff57
5 changed files with 40 additions and 35 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 36
      src/storm-pomdp-cli/storm-pomdp.cpp
  2. 26
      src/storm-pomdp/analysis/IterativePolicySearch.cpp
  3. 8
      src/storm-pomdp/analysis/JaniBeliefSupportMdpGenerator.cpp
  4. 1
      src/storm-pomdp/analysis/JaniBeliefSupportMdpGenerator.h
  5. 4
      src/storm-pomdp/analysis/OneShotPolicySearch.h

36
src/storm-pomdp-cli/storm-pomdp.cpp
View File

@ -155,7 +155,9 @@ namespace storm {
formula.asProbabilityOperatorFormula());
pomdp.getTransitionMatrix().makeRowGroupsAbsorbing(surelyNotAlmostSurelyReachTarget);
storm::storage::BitVector targetStates = qualitativeAnalysis.analyseProb1(formula.asProbabilityOperatorFormula());
bool computedSomething = false;
if (qualSettings.isMemlessSearchSet()) {
computedSomething = true;
storm::expressions::ExpressionManager expressionManager;
std::shared_ptr<storm::utility::solver::SmtSolverFactory> smtSolverFactory = std::make_shared<storm::utility::solver::Z3SmtSolverFactory>();
storm::pomdp::MemlessSearchOptions options = fillMemlessSearchOptionsFromSettings();
@ -168,7 +170,7 @@ namespace storm {
surelyNotAlmostSurelyReachTarget,
smtSolverFactory);
if (qualSettings.isWinningRegionSet()) {
STORM_LOG_ERROR("Computing winning regions is not supported by ccd-memless.");
STORM_LOG_ERROR("Computing winning regions is not supported by the one-shot method.");
} else {
memlessSearch.analyzeForInitialStates(lookahead);
}
@ -206,21 +208,28 @@ namespace storm {
++offset;
}
}
STORM_PRINT_AND_LOG("Initial state is safe: "
<< search.getLastWinningRegion().isWinning(initialObservation,
offset));
if (search.getLastWinningRegion().isWinning(initialObservation,
offset)) {
STORM_PRINT_AND_LOG("Initial state is safe!"
<< std::endl);
} else {
STORM_PRINT_AND_LOG("Initial state may not be safe."
<< std::endl);
}
} else {
STORM_LOG_WARN("Output for multiple initial states is incomplete");
}
std::cout << "Number of belief support states: "
<< search.getLastWinningRegion().beliefSupportStates() << std::endl;
if (coreSettings.isShowStatisticsSet() && qualSettings.computeExpensiveStats()) {
auto wbss = search.getLastWinningRegion().computeNrWinningBeliefs();
STORM_PRINT_AND_LOG(
"Number of winning belief support states: [" << wbss.first << "," << wbss.second
<< "]");
}
if (coreSettings.isShowStatisticsSet()) {
STORM_PRINT_AND_LOG("#STATS Number of belief support states: "
<< search.getLastWinningRegion().beliefSupportStates() << std::endl);
if (qualSettings.computeExpensiveStats()) {
auto wbss = search.getLastWinningRegion().computeNrWinningBeliefs();
STORM_PRINT_AND_LOG(
"#STATS Number of winning belief support states: [" << wbss.first << "," << wbss.second
<< "]");
}
search.getStatistics().print();
}
@ -229,12 +238,15 @@ namespace storm {
}
}
if (qualSettings.isComputeOnBeliefSupportSet()) {
computedSomething = true;
storm::pomdp::qualitative::JaniBeliefSupportMdpGenerator<ValueType> janicreator(pomdp);
janicreator.generate(targetStates, surelyNotAlmostSurelyReachTarget);
bool initialOnly = !qualSettings.isWinningRegionSet();
janicreator.verifySymbolic(initialOnly);
STORM_PRINT_AND_LOG("Initial state is safe: " << janicreator.isInitialWinning() << "\n");
}
STORM_LOG_THROW(computedSomething, storm::exceptions::InvalidSettingsException, "Nothing to be done, did you forget to set a method?");
}
template<typename ValueType, storm::dd::DdType DdType>

26
src/storm-pomdp/analysis/IterativePolicySearch.cpp
View File

@ -35,16 +35,16 @@ namespace storm {
template <typename ValueType>
void IterativePolicySearch<ValueType>::Statistics::print() const {
STORM_PRINT_AND_LOG("Total time: " << totalTimer);
STORM_PRINT_AND_LOG("SAT Calls " << satCalls);
STORM_PRINT_AND_LOG("SAT Calls time: " << smtCheckTimer);
STORM_PRINT_AND_LOG("Outer iterations: " << outerIterations);
STORM_PRINT_AND_LOG("Solver initialization time: " << initializeSolverTimer);
STORM_PRINT_AND_LOG("Obtain partial scheduler time: " << evaluateExtensionSolverTime);
STORM_PRINT_AND_LOG("Update solver to extend partial scheduler time: " << encodeExtensionSolverTime);
STORM_PRINT_AND_LOG("Update solver with new scheduler time: " << updateNewStrategySolverTime);
STORM_PRINT_AND_LOG("Winning regions update time: " << winningRegionUpdatesTimer);
STORM_PRINT_AND_LOG("Graph search time: " << graphSearchTime);
STORM_PRINT_AND_LOG("#STATS Total time: " << totalTimer << std::endl);
STORM_PRINT_AND_LOG("#STATS SAT Calls: " << satCalls << std::endl);
STORM_PRINT_AND_LOG("#STATS SAT Calls time: " << smtCheckTimer << std::endl);
STORM_PRINT_AND_LOG("#STATS Outer iterations: " << outerIterations << std::endl);
STORM_PRINT_AND_LOG("#STATS Solver initialization time: " << initializeSolverTimer << std::endl);
STORM_PRINT_AND_LOG("#STATS Obtain partial scheduler time: " << evaluateExtensionSolverTime << std::endl );
STORM_PRINT_AND_LOG("#STATS Update solver to extend partial scheduler time: " << encodeExtensionSolverTime << std::endl);
STORM_PRINT_AND_LOG("#STATS Update solver with new scheduler time: " << updateNewStrategySolverTime << std::endl);
STORM_PRINT_AND_LOG("#STATS Winning regions update time: " << winningRegionUpdatesTimer << std::endl);
STORM_PRINT_AND_LOG("#STATS Graph search time: " << graphSearchTime << std::endl);
}
template <typename ValueType>
@ -203,8 +203,6 @@ namespace storm {
++obs;
}
// Update at least one observation.
// PAPER COMMENT: 2
smtSolver->add(storm::expressions::disjunction(observationUpdatedExpressions));
@ -265,8 +263,6 @@ namespace storm {
}
}
rowindex = 0;
for (uint64_t state = 0; state < pomdp.getNumberOfStates(); ++state) {
// PAPER COMMENT 5
@ -334,7 +330,6 @@ namespace storm {
actPathDisjunction.push_back(storm::expressions::disjunction(pathDisjunction) && actionSelectionVarExpressions.at(pomdp.getObservation(state)).at(action));
rowindex++;
}
// TODO reconsider if this next add is sound
actPathDisjunction.push_back(switchVarExpressions.at(pomdp.getObservation(state)));
actPathDisjunction.push_back(followVarExpressions[pomdp.getObservation(state)]);
actPathDisjunction.push_back(!reachVarExpressions[state]);
@ -349,7 +344,6 @@ namespace storm {
}
} else {
smtSolver->add(pathVarExpressions[state][0] == expressionManager->integer(0));
//assert(false);
}
}
smtSolver->add(reachVars[state]);

8
src/storm-pomdp/analysis/JaniBeliefSupportMdpGenerator.cpp
View File

@ -200,16 +200,14 @@ namespace storm {
}
if(result && !onlyInitial) {
std::cout << "count: " << result->asQualitativeCheckResult().count() << std::endl;
auto vars = result->asSymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>().getTruthValuesVector().getContainedMetaVariables();
} else if (result) {
initialIsWinning = result->asQualitativeCheckResult().existsTrue();
}
}
template <typename ValueType>
template <typename ValueType>
bool JaniBeliefSupportMdpGenerator<ValueType>::isInitialWinning() const {
return initialIsWinning;
}

1
src/storm-pomdp/analysis/JaniBeliefSupportMdpGenerator.h
View File

@ -16,6 +16,7 @@ namespace storm {
void generate(storm::storage::BitVector const& targetStates, storm::storage::BitVector const& badStates);
void verifySymbolic(bool onlyInitial = true);
bool isInitialWinning() const;
private:
storm::models::sparse::Pomdp<ValueType> const& pomdp;
jani::Model model;

4
src/storm-pomdp/analysis/OneShotPolicySearch.h
View File

@ -55,9 +55,9 @@ namespace storm {
STORM_LOG_TRACE("Questionmark states: " << (~surelyReachSinkStates & ~targetStates));
bool result = analyze(k, ~surelyReachSinkStates & ~targetStates, pomdp.getInitialStates());
if (result) {
STORM_PRINT_AND_LOG("From initial state, one can almost-surely reach the target.");
STORM_PRINT_AND_LOG("From initial state, one can almost-surely reach the target." << std::endl);
} else {
STORM_PRINT_AND_LOG("From initial state, one may not almost-surely reach the target .");
STORM_PRINT_AND_LOG("From initial state, one may not almost-surely reach the target ." << std::endl);
}
}

Write Preview
Loading…
Cancel
Save