Tim Quatmann
6 years ago
59 changed files with 798 additions and 624 deletions
-
41CHANGELOG.md
-
54resources/doxygen/CMakeLists.txt
-
57src/storm-cli-utilities/model-handling.h
-
56src/storm-counterexamples/api/counterexamples.cpp
-
5src/storm-counterexamples/api/counterexamples.h
-
125src/storm-counterexamples/counterexamples/GuaranteedLabelSet.h
-
3src/storm-counterexamples/counterexamples/HighLevelCounterexample.h
-
22src/storm-counterexamples/counterexamples/MILPMinimalLabelSetGenerator.h
-
40src/storm-counterexamples/counterexamples/PathCounterexample.cpp
-
25src/storm-counterexamples/counterexamples/PathCounterexample.h
-
16src/storm-counterexamples/counterexamples/SMTMinimalLabelSetGenerator.h
-
45src/storm-counterexamples/settings/modules/CounterexampleGeneratorSettings.cpp
-
40src/storm-counterexamples/settings/modules/CounterexampleGeneratorSettings.h
-
97src/storm-dft-cli/storm-dft.cpp
-
75src/storm-dft/api/storm-dft.h
-
44src/storm-dft/modelchecker/dft/DFTModelChecker.cpp
-
17src/storm-dft/storage/dft/DFT.cpp
-
4src/storm-dft/storage/dft/DFT.h
-
1src/storm-dft/transformations/DftTransformator.cpp
-
2src/storm-dft/transformations/DftTransformator.h
-
58src/storm-dft/utility/FDEPConflictFinder.cpp
-
22src/storm-dft/utility/FDEPConflictFinder.h
-
4src/storm-parsers/parser/DeterministicSparseTransitionParser.cpp
-
3src/storm-parsers/parser/ImcaMarkovAutomatonParser.cpp
-
6src/storm-parsers/parser/MarkovAutomatonSparseTransitionParser.cpp
-
4src/storm-parsers/parser/NondeterministicSparseTransitionParser.cpp
-
4src/storm/api/export.h
-
45src/storm/api/transformation.h
-
4src/storm/builder/DdJaniModelBuilder.cpp
-
4src/storm/builder/DdPrismModelBuilder.cpp
-
3src/storm/builder/ExplicitModelBuilder.cpp
-
4src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp
-
4src/storm/builder/jit/ModelComponentsBuilder.cpp
-
17src/storm/models/sparse/DeterministicModel.cpp
-
2src/storm/models/sparse/DeterministicModel.h
-
30src/storm/models/sparse/Model.cpp
-
4src/storm/models/sparse/Model.h
-
22src/storm/models/sparse/NondeterministicModel.cpp
-
2src/storm/models/sparse/NondeterministicModel.h
-
8src/storm/settings/SettingsManager.cpp
-
19src/storm/settings/SettingsManager.h
-
12src/storm/settings/modules/BuildSettings.cpp
-
16src/storm/settings/modules/BuildSettings.h
-
19src/storm/settings/modules/CoreSettings.cpp
-
35src/storm/settings/modules/CoreSettings.h
-
11src/storm/settings/modules/IOSettings.cpp
-
8src/storm/settings/modules/IOSettings.h
-
27src/storm/transformer/NonMarkovianChainTransformer.h
-
128src/storm/utility/counterexamples.h
-
48src/storm/utility/export.h
-
4src/test/storm-dft/api/DftApproximationTest.cpp
-
2src/test/storm-dft/api/DftModelBuildingTest.cpp
-
4src/test/storm-dft/api/DftModelCheckerTest.cpp
-
4src/test/storm-dft/api/DftParserTest.cpp
-
22src/test/storm-dft/api/DftSmtTest.cpp
-
26src/test/storm-pars/analysis/AssumptionMakerTest.cpp
-
6src/test/storm/parser/DeterministicSparseTransitionParserTest.cpp
-
6src/test/storm/parser/MarkovAutomatonSparseTransitionParserTest.cpp
-
6src/test/storm/parser/NondeterministicSparseTransitionParserTest.cpp
@ -1,19 +1,65 @@ |
|||
#include "storm-counterexamples/api/counterexamples.h"
|
|||
|
|||
#include "storm/environment/Environment.h"
|
|||
#include "storm/utility/shortestPaths.h"
|
|||
|
|||
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) { |
|||
// 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."); |
|||
storm::logic::ProbabilityOperatorFormula const& probabilityOperator = formula->asProbabilityOperatorFormula(); |
|||
STORM_LOG_THROW(probabilityOperator.hasBound(), storm::exceptions::InvalidPropertyException, "Counterexample generation only supports bounded formulas."); |
|||
STORM_LOG_THROW(!storm::logic::isLowerBound(probabilityOperator.getComparisonType()), storm::exceptions::InvalidPropertyException, |
|||
"Counterexample generation only supports upper bounds."); |
|||
double threshold = probabilityOperator.getThresholdAs<double>(); |
|||
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); |
|||
|
|||
// Perform model checking to get target states
|
|||
Environment env; |
|||
storm::modelchecker::SparsePropositionalModelChecker<storm::models::sparse::Model<double>> modelchecker(*model); |
|||
|
|||
storm::logic::EventuallyFormula const& eventuallyFormula = subformula.asEventuallyFormula(); |
|||
std::unique_ptr<storm::modelchecker::CheckResult> subResult = modelchecker.check(env, eventuallyFormula.getSubformula()); |
|||
storm::modelchecker::ExplicitQualitativeCheckResult const& subQualitativeResult = subResult->asExplicitQualitativeCheckResult(); |
|||
|
|||
auto generator = storm::utility::ksp::ShortestPathsGenerator<double>(*model, subQualitativeResult.getTruthValuesVector()); |
|||
storm::counterexamples::PathCounterexample<double> cex(model); |
|||
double probability = 0; |
|||
bool thresholdExceeded = false; |
|||
for (size_t k = 1; k <= maxK; ++k) { |
|||
cex.addPath(generator.getPathAsList(k), k); |
|||
probability += generator.getDistance(k); |
|||
// Check if accumulated probability mass is already enough
|
|||
if ((probability >= threshold && !strictBound) || (probability > threshold)) { |
|||
thresholdExceeded = true; |
|||
break; |
|||
} |
|||
} |
|||
STORM_LOG_WARN_COND(thresholdExceeded, "Aborted computation because maximal number of paths was reached. Probability threshold is not yet exceeded."); |
|||
|
|||
return std::make_shared<storm::counterexamples::PathCounterexample<double>>(cex); |
|||
} |
|||
|
|||
} |
|||
} |
|||
@ -0,0 +1,125 @@ |
|||
#pragma once |
|||
|
|||
#include <queue> |
|||
#include <utility> |
|||
|
|||
#include "storm/exceptions/InvalidArgumentException.h" |
|||
#include "storm/models/sparse/Model.h" |
|||
#include "storm/storage/sparse/PrismChoiceOrigins.h" |
|||
|
|||
namespace storm { |
|||
namespace counterexamples { |
|||
|
|||
/*! |
|||
* Computes a set of labels that is executed along all paths from any state to a target state. |
|||
* |
|||
* @param labelSet the considered label sets (a label set is assigned to each choice) |
|||
* |
|||
* @return The set of labels that is visited on all paths from any state to a target state. |
|||
*/ |
|||
template<typename T> |
|||
std::vector<storm::storage::FlatSet<uint_fast64_t>> getGuaranteedLabelSets(storm::models::sparse::Model<T> const& model, std::vector<storm::storage::FlatSet<uint_fast64_t>> const& labelSets, storm::storage::BitVector const& psiStates, storm::storage::FlatSet<uint_fast64_t> const& relevantLabels) { |
|||
STORM_LOG_THROW(model.getNumberOfChoices() == labelSets.size(), storm::exceptions::InvalidArgumentException, "The given number of labels does not match the number of choices."); |
|||
|
|||
// Get some data from the model for convenient access. |
|||
storm::storage::SparseMatrix<T> const& transitionMatrix = model.getTransitionMatrix(); |
|||
std::vector<uint_fast64_t> const& nondeterministicChoiceIndices = transitionMatrix.getRowGroupIndices(); |
|||
storm::storage::SparseMatrix<T> backwardTransitions = model.getBackwardTransitions(); |
|||
|
|||
// Now we compute the set of labels that is present on all paths from the initial to the target states. |
|||
std::vector<storm::storage::FlatSet<uint_fast64_t>> analysisInformation(model.getNumberOfStates(), relevantLabels); |
|||
|
|||
std::queue<uint_fast64_t> worklist; |
|||
storm::storage::BitVector statesInWorkList(model.getNumberOfStates()); |
|||
storm::storage::BitVector markedStates(model.getNumberOfStates()); |
|||
|
|||
// Initially, put all predecessors of target states in the worklist and empty the analysis information them. |
|||
for (auto state : psiStates) { |
|||
analysisInformation[state] = storm::storage::FlatSet<uint_fast64_t>(); |
|||
for (auto const& predecessorEntry : backwardTransitions.getRow(state)) { |
|||
if (predecessorEntry.getColumn() != state && !statesInWorkList.get(predecessorEntry.getColumn()) && !psiStates.get(predecessorEntry.getColumn())) { |
|||
worklist.push(predecessorEntry.getColumn()); |
|||
statesInWorkList.set(predecessorEntry.getColumn()); |
|||
markedStates.set(state); |
|||
} |
|||
} |
|||
} |
|||
|
|||
uint_fast64_t iters = 0; |
|||
while (!worklist.empty()) { |
|||
++iters; |
|||
uint_fast64_t const& currentState = worklist.front(); |
|||
|
|||
size_t analysisInformationSizeBefore = analysisInformation[currentState].size(); |
|||
|
|||
// Iterate over the successor states for all choices and compute new analysis information. |
|||
for (uint_fast64_t currentChoice = nondeterministicChoiceIndices[currentState]; currentChoice < nondeterministicChoiceIndices[currentState + 1]; ++currentChoice) { |
|||
bool modifiedChoice = false; |
|||
|
|||
for (auto const& entry : transitionMatrix.getRow(currentChoice)) { |
|||
if (markedStates.get(entry.getColumn())) { |
|||
modifiedChoice = true; |
|||
break; |
|||
} |
|||
} |
|||
|
|||
// If we can reach the target state with this choice, we need to intersect the current |
|||
// analysis information with the union of the new analysis information of the target state |
|||
// and the choice labels. |
|||
if (modifiedChoice) { |
|||
for (auto const& entry : transitionMatrix.getRow(currentChoice)) { |
|||
if (markedStates.get(entry.getColumn())) { |
|||
storm::storage::FlatSet<uint_fast64_t> tmpIntersection; |
|||
std::set_intersection(analysisInformation[currentState].begin(), analysisInformation[currentState].end(), analysisInformation[entry.getColumn()].begin(), analysisInformation[entry.getColumn()].end(), std::inserter(tmpIntersection, tmpIntersection.begin())); |
|||
std::set_intersection(analysisInformation[currentState].begin(), analysisInformation[currentState].end(), labelSets[currentChoice].begin(), labelSets[currentChoice].end(), std::inserter(tmpIntersection, tmpIntersection.begin())); |
|||
analysisInformation[currentState] = std::move(tmpIntersection); |
|||
} |
|||
} |
|||
} |
|||
} |
|||
|
|||
// If the analysis information changed, we need to update it and put all the predecessors of this |
|||
// state in the worklist. |
|||
if (analysisInformation[currentState].size() != analysisInformationSizeBefore) { |
|||
for (auto const& predecessorEntry : backwardTransitions.getRow(currentState)) { |
|||
// Only put the predecessor in the worklist if it's not already a target state. |
|||
if (!psiStates.get(predecessorEntry.getColumn()) && !statesInWorkList.get(predecessorEntry.getColumn())) { |
|||
worklist.push(predecessorEntry.getColumn()); |
|||
statesInWorkList.set(predecessorEntry.getColumn()); |
|||
} |
|||
} |
|||
markedStates.set(currentState, true); |
|||
} else { |
|||
markedStates.set(currentState, false); |
|||
} |
|||
|
|||
worklist.pop(); |
|||
statesInWorkList.set(currentState, false); |
|||
} |
|||
|
|||
return analysisInformation; |
|||
} |
|||
|
|||
/*! |
|||
* Computes a set of labels that is executed along all paths from an initial state to a target state. |
|||
* |
|||
* @param labelSet the considered label sets (a label set is assigned to each choice) |
|||
* |
|||
* @return The set of labels that is executed on all paths from an initial state to a target state. |
|||
*/ |
|||
template <typename T> |
|||
storm::storage::FlatSet<uint_fast64_t> getGuaranteedLabelSet(storm::models::sparse::Model<T> const& model, std::vector<storm::storage::FlatSet<uint_fast64_t>> const& labelSets, storm::storage::BitVector const& psiStates, storm::storage::FlatSet<uint_fast64_t> const& relevantLabels) { |
|||
std::vector<storm::storage::FlatSet<uint_fast64_t>> guaranteedLabels = getGuaranteedLabelSets(model, labelSets, psiStates, relevantLabels); |
|||
|
|||
storm::storage::FlatSet<uint_fast64_t> knownLabels(relevantLabels); |
|||
storm::storage::FlatSet<uint_fast64_t> tempIntersection; |
|||
for (auto initialState : model.getInitialStates()) { |
|||
std::set_intersection(knownLabels.begin(), knownLabels.end(), guaranteedLabels[initialState].begin(), guaranteedLabels[initialState].end(), std::inserter(tempIntersection, tempIntersection.end())); |
|||
std::swap(knownLabels, tempIntersection); |
|||
} |
|||
|
|||
return knownLabels; |
|||
} |
|||
|
|||
} // namespace counterexample |
|||
} // namespace storm |
|||
@ -0,0 +1,40 @@ |
|||
#include "storm-counterexamples/counterexamples/PathCounterexample.h"
|
|||
|
|||
#include "storm/utility/export.h"
|
|||
|
|||
namespace storm { |
|||
namespace counterexamples { |
|||
|
|||
template<typename ValueType> |
|||
PathCounterexample<ValueType>::PathCounterexample(std::shared_ptr<storm::models::sparse::Model<ValueType>> model) : model(model) { |
|||
// Intentionally left empty.
|
|||
} |
|||
|
|||
template<typename ValueType> |
|||
void PathCounterexample<ValueType>::addPath(std::vector<storage::sparse::state_type> path, size_t k) { |
|||
if (k >= shortestPaths.size()) { |
|||
shortestPaths.resize(k); |
|||
} |
|||
shortestPaths[k-1] = path; |
|||
} |
|||
|
|||
template<typename ValueType> |
|||
void PathCounterexample<ValueType>::writeToStream(std::ostream& out) const { |
|||
out << "Shortest path counterexample with k = " << shortestPaths.size() << " paths: " << std::endl; |
|||
for (size_t i = 0; i < shortestPaths.size(); ++i) { |
|||
out << i+1 << "-shortest path: " << std::endl; |
|||
for (auto it = shortestPaths[i].rbegin(); it != shortestPaths[i].rend(); ++it) { |
|||
out << "\tstate " << *it; |
|||
if (model->hasStateValuations()) { |
|||
out << ": "<< model->getStateValuations().getStateInfo(*it); |
|||
} |
|||
out << ": {"; |
|||
storm::utility::outputFixedWidth(out, model->getLabelsOfState(*it), 0); |
|||
out << "}" << std::endl; |
|||
} |
|||
} |
|||
} |
|||
|
|||
template class PathCounterexample<double>; |
|||
} |
|||
} |
|||
@ -0,0 +1,25 @@ |
|||
#pragma once |
|||
|
|||
#include "storm-counterexamples/counterexamples/Counterexample.h" |
|||
|
|||
#include "storm/models/sparse/Model.h" |
|||
|
|||
namespace storm { |
|||
namespace counterexamples { |
|||
|
|||
template<typename ValueType> |
|||
class PathCounterexample : public Counterexample { |
|||
public: |
|||
PathCounterexample(std::shared_ptr<storm::models::sparse::Model<ValueType>> model); |
|||
|
|||
void addPath(std::vector<storage::sparse::state_type> path, size_t k); |
|||
|
|||
void writeToStream(std::ostream& out) const override; |
|||
|
|||
private: |
|||
std::shared_ptr<storm::models::sparse::Model<ValueType>> model; |
|||
std::vector<std::vector<storage::sparse::state_type>> shortestPaths; |
|||
}; |
|||
|
|||
} |
|||
} |
|||
@ -1,128 +0,0 @@ |
|||
#ifndef STORM_UTILITY_COUNTEREXAMPLE_H_ |
|||
#define STORM_UTILITY_COUNTEREXAMPLE_H_ |
|||
|
|||
#include <queue> |
|||
#include <utility> |
|||
|
|||
#include "storm/storage/sparse/PrismChoiceOrigins.h" |
|||
|
|||
namespace storm { |
|||
namespace utility { |
|||
namespace counterexamples { |
|||
|
|||
/*! |
|||
* Computes a set of labels that is executed along all paths from any state to a target state. |
|||
* |
|||
* @param labelSet the considered label sets (a label set is assigned to each choice) |
|||
* |
|||
* @return The set of labels that is visited on all paths from any state to a target state. |
|||
*/ |
|||
template <typename T> |
|||
std::vector<storm::storage::FlatSet<uint_fast64_t>> getGuaranteedLabelSets(storm::models::sparse::Model<T> const& model, std::vector<storm::storage::FlatSet<uint_fast64_t>> const& labelSets, storm::storage::BitVector const& psiStates, storm::storage::FlatSet<uint_fast64_t> const& relevantLabels) { |
|||
STORM_LOG_THROW(model.getNumberOfChoices() == labelSets.size(), storm::exceptions::InvalidArgumentException, "The given number of labels does not match the number of choices."); |
|||
|
|||
// Get some data from the model for convenient access. |
|||
storm::storage::SparseMatrix<T> const& transitionMatrix = model.getTransitionMatrix(); |
|||
std::vector<uint_fast64_t> const& nondeterministicChoiceIndices = transitionMatrix.getRowGroupIndices(); |
|||
storm::storage::SparseMatrix<T> backwardTransitions = model.getBackwardTransitions(); |
|||
|
|||
// Now we compute the set of labels that is present on all paths from the initial to the target states. |
|||
std::vector<storm::storage::FlatSet<uint_fast64_t>> analysisInformation(model.getNumberOfStates(), relevantLabels); |
|||
|
|||
std::queue<uint_fast64_t> worklist; |
|||
storm::storage::BitVector statesInWorkList(model.getNumberOfStates()); |
|||
storm::storage::BitVector markedStates(model.getNumberOfStates()); |
|||
|
|||
// Initially, put all predecessors of target states in the worklist and empty the analysis information them. |
|||
for (auto state : psiStates) { |
|||
analysisInformation[state] = storm::storage::FlatSet<uint_fast64_t>(); |
|||
for (auto const& predecessorEntry : backwardTransitions.getRow(state)) { |
|||
if (predecessorEntry.getColumn() != state && !statesInWorkList.get(predecessorEntry.getColumn()) && !psiStates.get(predecessorEntry.getColumn())) { |
|||
worklist.push(predecessorEntry.getColumn()); |
|||
statesInWorkList.set(predecessorEntry.getColumn()); |
|||
markedStates.set(state); |
|||
} |
|||
} |
|||
} |
|||
|
|||
uint_fast64_t iters = 0; |
|||
while (!worklist.empty()) { |
|||
++iters; |
|||
uint_fast64_t const& currentState = worklist.front(); |
|||
|
|||
size_t analysisInformationSizeBefore = analysisInformation[currentState].size(); |
|||
|
|||
// Iterate over the successor states for all choices and compute new analysis information. |
|||
for (uint_fast64_t currentChoice = nondeterministicChoiceIndices[currentState]; currentChoice < nondeterministicChoiceIndices[currentState + 1]; ++currentChoice) { |
|||
bool modifiedChoice = false; |
|||
|
|||
for (auto const& entry : transitionMatrix.getRow(currentChoice)) { |
|||
if (markedStates.get(entry.getColumn())) { |
|||
modifiedChoice = true; |
|||
break; |
|||
} |
|||
} |
|||
|
|||
// If we can reach the target state with this choice, we need to intersect the current |
|||
// analysis information with the union of the new analysis information of the target state |
|||
// and the choice labels. |
|||
if (modifiedChoice) { |
|||
for (auto const& entry : transitionMatrix.getRow(currentChoice)) { |
|||
if (markedStates.get(entry.getColumn())) { |
|||
storm::storage::FlatSet<uint_fast64_t> tmpIntersection; |
|||
std::set_intersection(analysisInformation[currentState].begin(), analysisInformation[currentState].end(), analysisInformation[entry.getColumn()].begin(), analysisInformation[entry.getColumn()].end(), std::inserter(tmpIntersection, tmpIntersection.begin())); |
|||
std::set_intersection(analysisInformation[currentState].begin(), analysisInformation[currentState].end(), labelSets[currentChoice].begin(), labelSets[currentChoice].end(), std::inserter(tmpIntersection, tmpIntersection.begin())); |
|||
analysisInformation[currentState] = std::move(tmpIntersection); |
|||
} |
|||
} |
|||
} |
|||
} |
|||
|
|||
// If the analysis information changed, we need to update it and put all the predecessors of this |
|||
// state in the worklist. |
|||
if (analysisInformation[currentState].size() != analysisInformationSizeBefore) { |
|||
for (auto const& predecessorEntry : backwardTransitions.getRow(currentState)) { |
|||
// Only put the predecessor in the worklist if it's not already a target state. |
|||
if (!psiStates.get(predecessorEntry.getColumn()) && !statesInWorkList.get(predecessorEntry.getColumn())) { |
|||
worklist.push(predecessorEntry.getColumn()); |
|||
statesInWorkList.set(predecessorEntry.getColumn()); |
|||
} |
|||
} |
|||
markedStates.set(currentState, true); |
|||
} else { |
|||
markedStates.set(currentState, false); |
|||
} |
|||
|
|||
worklist.pop(); |
|||
statesInWorkList.set(currentState, false); |
|||
} |
|||
|
|||
return analysisInformation; |
|||
} |
|||
|
|||
/*! |
|||
* Computes a set of labels that is executed along all paths from an initial state to a target state. |
|||
* |
|||
* @param labelSet the considered label sets (a label set is assigned to each choice) |
|||
* |
|||
* @return The set of labels that is executed on all paths from an initial state to a target state. |
|||
*/ |
|||
template <typename T> |
|||
storm::storage::FlatSet<uint_fast64_t> getGuaranteedLabelSet(storm::models::sparse::Model<T> const& model, std::vector<storm::storage::FlatSet<uint_fast64_t>> const& labelSets, storm::storage::BitVector const& psiStates, storm::storage::FlatSet<uint_fast64_t> const& relevantLabels) { |
|||
std::vector<storm::storage::FlatSet<uint_fast64_t>> guaranteedLabels = getGuaranteedLabelSets(model, labelSets, psiStates, relevantLabels); |
|||
|
|||
storm::storage::FlatSet<uint_fast64_t> knownLabels(relevantLabels); |
|||
storm::storage::FlatSet<uint_fast64_t> tempIntersection; |
|||
for (auto initialState : model.getInitialStates()) { |
|||
std::set_intersection(knownLabels.begin(), knownLabels.end(), guaranteedLabels[initialState].begin(), guaranteedLabels[initialState].end(), std::inserter(tempIntersection, tempIntersection.end())); |
|||
std::swap(knownLabels, tempIntersection); |
|||
} |
|||
|
|||
return knownLabels; |
|||
} |
|||
|
|||
} // namespace counterexample |
|||
} // namespace utility |
|||
} // namespace storm |
|||
|
|||
#endif /* STORM_UTILITY_COUNTEREXAMPLE_H_ */ |
|||
Write
Preview
Loading…
Cancel
Save
Reference in new issue