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

Merge branch 'master' into chris_diss

main
dehnert 7 years ago
parent
cb89ab7509 54c0bbb7c3
commit
1adc1ce564
5 changed files with 57 additions and 53 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. 5
      CHANGELOG.md
  2. 5
      src/storm-cli-utilities/model-handling.h
  3. 94
      src/storm-counterexamples/counterexamples/SMTMinimalLabelSetGenerator.h
  4. 2
      src/storm-counterexamples/settings/modules/CounterexampleGeneratorSettings.cpp
  5. 4
      src/storm/api/export.cpp

5
CHANGELOG.md
View File

@ -13,7 +13,10 @@ Version 1.2.x
- Sound value iteration (SVI) for DTMCs and MDPs
- Topological solver for linear equation systems and MinMax equation systems.
- Added support for expected total rewards in the sparse engine
- `storm-parsers` extracted to reduce linking time
- `storm-counterexamples` extracted to reduce linking time
- Improved export for jani models
- Several extensions to high-level counterexamples
### Version 1.2.1 (2018/02)
- Multi-dimensional reward bounded reachability properties for DTMCs.

5
src/storm-cli-utilities/model-handling.h
View File

@ -420,7 +420,10 @@ namespace storm {
STORM_LOG_THROW(model->isSparseModel(), storm::exceptions::NotSupportedException, "Counterexample generation is currently only supported for sparse models.");
auto sparseModel = model->as<storm::models::sparse::Model<ValueType>>();
for (auto& rewModel : sparseModel->getRewardModels()) {
rewModel.second.reduceToStateBasedRewards(sparseModel->getTransitionMatrix(), true);
}
STORM_LOG_THROW(sparseModel->isOfType(storm::models::ModelType::Dtmc) || sparseModel->isOfType(storm::models::ModelType::Mdp), storm::exceptions::NotSupportedException, "Counterexample is currently only supported for discrete-time models.");
auto counterexampleSettings = storm::settings::getModule<storm::settings::modules::CounterexampleGeneratorSettings>();

94
src/storm-counterexamples/counterexamples/SMTMinimalLabelSetGenerator.h
View File

@ -59,10 +59,6 @@ namespace storm {
std::map<uint_fast64_t, std::list<uint_fast64_t>> relevantChoicesForRelevantStates;
};
struct GeneratorStats {
};
struct VariableInformation {
// The manager responsible for the constraints we are building.
std::shared_ptr<storm::expressions::ExpressionManager> manager;
@ -271,21 +267,6 @@ namespace storm {
return variableInformation;
}
/*!
* Asserts the constraints that are initially needed for the Fu-Malik procedure.
*
* @param solver The solver in which to assert the constraints.
* @param variableInformation A structure with information about the variables for the labels.
*/
static void assertFuMalikInitialConstraints(z3::solver& solver, VariableInformation const& variableInformation) {
// Assert that at least one of the labels must be taken.
z3::expr formula = variableInformation.labelVariables.at(0);
for (uint_fast64_t index = 1; index < variableInformation.labelVariables.size(); ++index) {
formula = formula || variableInformation.labelVariables.at(index);
}
solver.add(formula);
}
static storm::expressions::Expression getOtherSynchronizationEnabledFormula(boost::container::flat_set<uint_fast64_t> const& labelSet, std::map<uint_fast64_t, std::set<boost::container::flat_set<uint_fast64_t>>> const& synchronizingLabels, boost::container::flat_map<boost::container::flat_set<uint_fast64_t>, storm::expressions::Expression> const& labelSetToFormula, VariableInformation const& variableInformation, RelevancyInformation const& relevancyInformation) {
// Taking all commands of a combination does not necessarily mean that a following label set needs to be taken.
// This is because it could be that the commands are taken to enable other synchronizations. Therefore, we need
@ -338,7 +319,7 @@ namespace storm {
// * identify labels that can directly precede a given action
// * identify labels that directly reach a target state
// * identify labels that can directly follow a given action
boost::container::flat_set<uint_fast64_t> initialLabels;
std::set<boost::container::flat_set<uint_fast64_t>> initialCombinations;
boost::container::flat_set<uint_fast64_t> targetLabels;
@ -970,22 +951,7 @@ namespace storm {
}
solver.add(disjunction);
}
/*!
* Asserts that the conjunction of the given formulae holds. If the content of the conjunction is empty,
* this corresponds to asserting true.
*
* @param context The Z3 context in which to build the expressions.
* @param solver The solver to use for the satisfiability evaluation.
* @param formulaVector A vector of expressions that shall form the conjunction.
*/
static void assertConjunction(z3::context& context, z3::solver& solver, std::vector<z3::expr> const& formulaVector) {
z3::expr conjunction = context.bool_val(true);
for (auto expr : formulaVector) {
conjunction = conjunction && expr;
}
solver.add(conjunction);
}
/*!
* Creates a full-adder for the two inputs and returns the resulting bit as well as the carry bit.
@ -1387,7 +1353,10 @@ namespace storm {
std::vector<storm::expressions::Expression> formulae;
boost::container::flat_set<uint_fast64_t> unknownReachableLabels;
std::set_difference(reachableLabels.begin(), reachableLabels.end(), relevancyInformation.knownLabels.begin(), relevancyInformation.knownLabels.end(), std::inserter(unknownReachableLabels, unknownReachableLabels.end()));
for (auto label : unknownReachableLabels) {
boost::container::flat_set<uint64_t> unknownReachableMinimalityLabels;
std::set_intersection(unknownReachableLabels.begin(), unknownReachableLabels.end(), relevancyInformation.minimalityLabels.begin(), relevancyInformation.minimalityLabels.end(), std::inserter(unknownReachableMinimalityLabels, unknownReachableMinimalityLabels.end()));
for (auto label : unknownReachableMinimalityLabels) {
formulae.push_back(!variableInformation.labelVariables.at(variableInformation.labelToIndexMap.at(label)));
}
for (auto const& cutLabelSet : cutLabels) {
@ -1488,7 +1457,10 @@ namespace storm {
std::vector<storm::expressions::Expression> formulae;
boost::container::flat_set<uint_fast64_t> unknownReachableLabels;
std::set_difference(reachableLabels.begin(), reachableLabels.end(), relevancyInformation.knownLabels.begin(), relevancyInformation.knownLabels.end(), std::inserter(unknownReachableLabels, unknownReachableLabels.end()));
for (auto label : unknownReachableLabels) {
boost::container::flat_set<uint64_t> unknownReachableMinimalityLabels;
std::set_intersection(unknownReachableLabels.begin(), unknownReachableLabels.end(), relevancyInformation.minimalityLabels.begin(), relevancyInformation.minimalityLabels.end(), std::inserter(unknownReachableMinimalityLabels, unknownReachableMinimalityLabels.end()));
for (auto label : unknownReachableMinimalityLabels) {
formulae.push_back(!variableInformation.labelVariables.at(variableInformation.labelToIndexMap.at(label)));
}
for (auto const& cutLabelSet : cutLabels) {
@ -1510,7 +1482,7 @@ namespace storm {
* Returns the sub-model obtained from removing all choices that do not originate from the specified filterLabelSet.
* Also returns the Labelsets of the sub-model.
*/
static std::pair<std::shared_ptr<storm::models::sparse::Model<T>>, std::vector<boost::container::flat_set<uint_fast64_t>>> restrictModelToLabelSet(storm::models::sparse::Model<T> const& model, boost::container::flat_set<uint_fast64_t> const& filterLabelSet, boost::optional<uint64_t> absorbState = boost::none) {
static std::pair<std::shared_ptr<storm::models::sparse::Model<T>>, std::vector<boost::container::flat_set<uint_fast64_t>>> restrictModelToLabelSet(storm::models::sparse::Model<T> const& model, boost::container::flat_set<uint_fast64_t> const& filterLabelSet, boost::optional<std::string> const& rewardName = boost::none, boost::optional<uint64_t> absorbState = boost::none) {
bool customRowGrouping = model.isOfType(storm::models::ModelType::Mdp);
@ -1550,13 +1522,19 @@ namespace storm {
resultLabelSet.emplace_back();
++currentRow;
}
}
if (rewardName) {
auto const &origRewModel = model.getRewardModel(rewardName.get());
assert(origRewModel.hasOnlyStateRewards());
}
std::shared_ptr<storm::models::sparse::Model<T>> resultModel;
if (model.isOfType(storm::models::ModelType::Dtmc)) {
resultModel = std::make_shared<storm::models::sparse::Dtmc<T>>(transitionMatrixBuilder.build(), storm::models::sparse::StateLabeling(model.getStateLabeling()));
resultModel = std::make_shared<storm::models::sparse::Dtmc<T>>(transitionMatrixBuilder.build(), storm::models::sparse::StateLabeling(model.getStateLabeling()), model.getRewardModels());
} else {
resultModel = std::make_shared<storm::models::sparse::Mdp<T>>(transitionMatrixBuilder.build(), storm::models::sparse::StateLabeling(model.getStateLabeling()));
resultModel = std::make_shared<storm::models::sparse::Mdp<T>>(transitionMatrixBuilder.build(), storm::models::sparse::StateLabeling(model.getStateLabeling()), model.getRewardModels());
}
return std::make_pair(resultModel, std::move(resultLabelSet));
@ -1605,6 +1583,13 @@ namespace storm {
uint64_t maximumCounterexamples = 1;
uint64_t multipleCounterexampleSizeCap = 100000000;
};
struct GeneratorStats {
std::chrono::milliseconds setupTime;
std::chrono::milliseconds solverTime;
std::chrono::milliseconds modelCheckingTime;
std::chrono::milliseconds analysisTime;
};
/*!
* Computes the minimal command set that is needed in the given model to exceed the given probability threshold for satisfying phi until psi.
@ -1618,7 +1603,7 @@ namespace storm {
* @param strictBound Indicates whether the threshold needs to be achieved (true) or exceeded (false).
* @param options A set of options for customization.
*/
static std::vector<boost::container::flat_set<uint_fast64_t>> getMinimalLabelSet(Environment const& env, storm::storage::SymbolicModelDescription const& symbolicModel, storm::models::sparse::Model<T> const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, double propertyThreshold, boost::optional<std::string> const& rewardName, bool strictBound, boost::container::flat_set<uint_fast64_t> const& dontCareLabels = boost::container::flat_set<uint_fast64_t>(), Options const& options = Options()) {
static std::vector<boost::container::flat_set<uint_fast64_t>> getMinimalLabelSet(Environment const& env, GeneratorStats& stats, storm::storage::SymbolicModelDescription const& symbolicModel, storm::models::sparse::Model<T> const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, double propertyThreshold, boost::optional<std::string> const& rewardName, bool strictBound, boost::container::flat_set<uint_fast64_t> const& dontCareLabels = boost::container::flat_set<uint_fast64_t>(), Options const& options = Options()) {
#ifdef STORM_HAVE_Z3
std::vector<boost::container::flat_set<uint_fast64_t>> result;
// Set up all clocks used for time measurement.
@ -1742,7 +1727,7 @@ namespace storm {
}
auto subChoiceOrigins = restrictModelToLabelSet(model, commandSet, psiStates.getNextSetIndex(0));
auto subChoiceOrigins = restrictModelToLabelSet(model, commandSet, rewardName, psiStates.getNextSetIndex(0));
std::shared_ptr<storm::models::sparse::Model<T>> const& subModel = subChoiceOrigins.first;
std::vector<boost::container::flat_set<uint_fast64_t>> const& subLabelSets = subChoiceOrigins.second;
@ -1809,12 +1794,19 @@ namespace storm {
// Compute and emit the time measurements if the corresponding flag was set.
totalTime = std::chrono::high_resolution_clock::now() - totalClock;
stats.analysisTime = std::chrono::duration_cast<std::chrono::milliseconds>(totalAnalysisTime);
stats.setupTime = std::chrono::duration_cast<std::chrono::milliseconds>(totalSetupTime);
stats.modelCheckingTime = std::chrono::duration_cast<std::chrono::milliseconds>(totalModelCheckingTime);
stats.solverTime = std::chrono::duration_cast<std::chrono::milliseconds>(totalSolverTime);
if (storm::settings::getModule<storm::settings::modules::CoreSettings>().isShowStatisticsSet()) {
boost::container::flat_set<uint64_t> allLabels;
for (auto const& e : labelSets) {
allLabels.insert(e.begin(), e.end());
}
std::cout << "Metrics:" << std::endl;
std::cout << " * all labels: " << allLabels.size() << std::endl;
std::cout << " * known labels: " << relevancyInformation.knownLabels.size() << std::endl;
@ -1839,7 +1831,7 @@ namespace storm {
#endif
}
static void extendLabelSetLowerBound(storm::models::sparse::Model<T> const& model, boost::container::flat_set<uint_fast64_t>& commandSet, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool silent = false) {
static void extendLabelSetLowerBound(storm::models::sparse::Model<T> const& model, boost::container::flat_set<uint_fast64_t>& commandSet, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool silent = false) {
auto startTime = std::chrono::high_resolution_clock::now();
// Create sub-model that only contains the choices allowed by the given command set.
@ -1923,7 +1915,7 @@ namespace storm {
}
static std::vector<boost::container::flat_set<uint_fast64_t>> computeCounterexampleLabelSet(Environment const& env, storm::storage::SymbolicModelDescription const& symbolicModel, storm::models::sparse::Model<T> const& model, std::shared_ptr<storm::logic::Formula const> const& formula, boost::container::flat_set<uint_fast64_t> const& dontCareLabels = boost::container::flat_set<uint_fast64_t>(), Options const& options = Options(true)) {
static std::vector<boost::container::flat_set<uint_fast64_t>> computeCounterexampleLabelSet(Environment const& env, GeneratorStats& stats, storm::storage::SymbolicModelDescription const& symbolicModel, storm::models::sparse::Model<T> const& model, std::shared_ptr<storm::logic::Formula const> const& formula, boost::container::flat_set<uint_fast64_t> const& dontCareLabels = boost::container::flat_set<uint_fast64_t>(), Options const& options = Options(true)) {
STORM_LOG_THROW(model.isOfType(storm::models::ModelType::Dtmc) || model.isOfType(storm::models::ModelType::Mdp), storm::exceptions::NotSupportedException, "MaxSAT-based counterexample generation is supported only for discrete-time models.");
if (!options.silent) {
std::cout << std::endl << "Generating minimal label counterexample for formula " << *formula << std::endl;
@ -1952,7 +1944,8 @@ namespace storm {
rewardName = rewardOperator.getRewardModelName();
STORM_LOG_THROW(!storm::logic::isLowerBound(comparisonType), storm::exceptions::NotSupportedException, "Lower bounds in counterexamples are only supported for probability formulas.");
STORM_LOG_THROW(model.hasRewardModel(rewardName.get()), storm::exceptions::InvalidPropertyException, "Property refers to reward " << rewardName.get() << " but model does not contain such a reward model.");
STORM_LOG_THROW(model.getRewardModel(rewardName.get()).hasOnlyStateRewards(), storm::exceptions::NotSupportedException, "We only support state-based rewards at the moment.");
}
bool strictBound = comparisonType == storm::logic::ComparisonType::Less;
storm::logic::Formula const& subformula = formula->asOperatorFormula().getSubformula();
@ -2014,7 +2007,7 @@ namespace storm {
// Delegate the actual computation work to the function of equal name.
auto startTime = std::chrono::high_resolution_clock::now();
auto labelSets = getMinimalLabelSet(env, symbolicModel, model, phiStates, psiStates, threshold, rewardName, strictBound, dontCareLabels, options);
auto labelSets = getMinimalLabelSet(env, stats, symbolicModel, model, phiStates, psiStates, threshold, rewardName, strictBound, dontCareLabels, options);
auto endTime = std::chrono::high_resolution_clock::now();
if (!options.silent) {
for (auto const& labelSet : labelSets) {
@ -2036,7 +2029,8 @@ namespace storm {
static std::shared_ptr<HighLevelCounterexample> computeCounterexample(Environment const& env, storm::storage::SymbolicModelDescription const& symbolicModel, storm::models::sparse::Model<T> const& model, std::shared_ptr<storm::logic::Formula const> const& formula) {
#ifdef STORM_HAVE_Z3
auto labelSets = computeCounterexampleLabelSet(env, symbolicModel, model, formula);
GeneratorStats stats;
auto labelSets = computeCounterexampleLabelSet(env, stats, symbolicModel, model, formula);
if (symbolicModel.isPrismProgram()) {

2
src/storm-counterexamples/settings/modules/CounterexampleGeneratorSettings.cpp
View File

@ -1,4 +1,4 @@
#include "CounterexampleGeneratorSettings.h"
#include "storm-counterexamples/settings/modules/CounterexampleGeneratorSettings.h"
#include "storm/settings/SettingsManager.h"
#include "storm/exceptions/InvalidSettingsException.h"

4
src/storm/api/export.cpp
View File

@ -16,6 +16,10 @@ namespace storm {
}
}
if (janiSettings.isExportFlattenedSet()) {
exportModel = exportModel.flattenComposition();
}
if (janiSettings.isExportAsStandardJaniSet()) {
storm::jani::Model normalisedModel = exportModel;
normalisedModel.makeStandardJaniCompliant();

Write Preview
Loading…
Cancel
Save