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

Check if counterexample exists for k-shortest path

tempestpy_adaptions
Matthias Volk 5 years ago
parent
013695a6ce
commit
4f36e7e431
1 changed files with 23 additions and 10 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. 33
      src/storm-counterexamples/api/counterexamples.cpp

33
src/storm-counterexamples/api/counterexamples.cpp
View File

@ -6,22 +6,22 @@
namespace storm {
namespace api {
std::shared_ptr<storm::counterexamples::Counterexample>
computeHighLevelCounterexampleMilp(storm::storage::SymbolicModelDescription const& symbolicModel, std::shared_ptr<storm::models::sparse::Mdp<double>> mdp,
std::shared_ptr<storm::logic::Formula const> const& formula) {
std::shared_ptr<storm::counterexamples::Counterexample> computeHighLevelCounterexampleMilp(storm::storage::SymbolicModelDescription const& symbolicModel,
std::shared_ptr<storm::models::sparse::Mdp<double>> mdp,
std::shared_ptr<storm::logic::Formula const> const& formula) {
Environment env;
return storm::counterexamples::MILPMinimalLabelSetGenerator<double>::computeCounterexample(env, symbolicModel, *mdp, formula);
}
std::shared_ptr<storm::counterexamples::Counterexample>
computeHighLevelCounterexampleMaxSmt(storm::storage::SymbolicModelDescription const& symbolicModel, std::shared_ptr<storm::models::sparse::Model<double>> model,
std::shared_ptr<storm::logic::Formula const> const& formula) {
std::shared_ptr<storm::counterexamples::Counterexample> computeHighLevelCounterexampleMaxSmt(storm::storage::SymbolicModelDescription const& symbolicModel,
std::shared_ptr <storm::models::sparse::Model<double>> model,
std::shared_ptr<storm::logic::Formula const> const& formula) {
Environment env;
return storm::counterexamples::SMTMinimalLabelSetGenerator<double>::computeCounterexample(env, symbolicModel, *model, formula);
}
std::shared_ptr<storm::counterexamples::Counterexample>
computeKShortestPathCounterexample(std::shared_ptr<storm::models::sparse::Model<double>> model, std::shared_ptr<storm::logic::Formula const> const& formula, size_t maxK) {
std::shared_ptr<storm::counterexamples::Counterexample> computeKShortestPathCounterexample(std::shared_ptr<storm::models::sparse::Model<double>> model,
std::shared_ptr<storm::logic::Formula const> const& formula, size_t maxK) {
// Only accept formulas of the form "P </<= x [F target]
STORM_LOG_THROW(formula->isProbabilityOperatorFormula(), storm::exceptions::InvalidPropertyException,
"Counterexample generation does not support this kind of formula. Expecting a probability operator as the outermost formula element.");
@ -33,7 +33,10 @@ namespace storm {
storm::logic::Formula const& subformula = formula->asOperatorFormula().getSubformula();
STORM_LOG_THROW(subformula.isEventuallyFormula(), storm::exceptions::InvalidPropertyException,
"Path formula is required to be of the form 'F psi' for counterexample generation.");
bool strictBound = (probabilityOperator.getComparisonType() == storm::logic::ComparisonType::Greater);
bool strictBound = (probabilityOperator.getComparisonType() == storm::logic::ComparisonType::Less);
STORM_LOG_THROW(model->getInitialStates().getNumberOfSetBits() == 1, storm::exceptions::NotSupportedException,
"k-shortest paths is only supported for models with a unique initial state.");
size_t initialState = *(model->getInitialStates().begin());
// Perform model checking to get target states
Environment env;
@ -43,6 +46,16 @@ namespace storm {
std::unique_ptr<storm::modelchecker::CheckResult> subResult = modelchecker.check(env, eventuallyFormula.getSubformula());
storm::modelchecker::ExplicitQualitativeCheckResult const& subQualitativeResult = subResult->asExplicitQualitativeCheckResult();
// Check if counterexample is even possible
storm::storage::BitVector phiStates(model->getNumberOfStates(), true);
auto results = storm::modelchecker::helper::SparseDtmcPrctlHelper<double>::computeUntilProbabilities(env, false, model->getTransitionMatrix(),
model->getBackwardTransitions(), phiStates,
subQualitativeResult.getTruthValuesVector(), true);
double reachProb = results.at(initialState);
STORM_LOG_THROW((reachProb > threshold) || (strictBound && reachProb >= threshold), storm::exceptions::InvalidArgumentException,
"Given probability threshold " << threshold << " cannot be " << (strictBound ? "achieved" : "exceeded")
<< " in model with maximal reachability probability of " << reachProb << ".");
auto generator = storm::utility::ksp::ShortestPathsGenerator<double>(*model, subQualitativeResult.getTruthValuesVector());
storm::counterexamples::PathCounterexample<double> cex(model);
double probability = 0;
@ -51,7 +64,7 @@ namespace storm {
cex.addPath(generator.getPathAsList(k), k);
probability += generator.getDistance(k);
// Check if accumulated probability mass is already enough
if ((probability >= threshold && !strictBound) || (probability > threshold)) {
if ((probability > threshold) || (strictBound && probability >= threshold && strictBound)) {
thresholdExceeded = true;
break;
}

Write Preview
Loading…
Cancel
Save