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

added some convenience functions for reward model building 

Former-commit-id: 796963aee3
main
dehnert 10 years ago
parent
5b77d827dc
commit
1a07b24682
14 changed files with 360 additions and 232 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. 32
      src/builder/DdPrismModelBuilder.cpp
  2. 10
      src/builder/DdPrismModelBuilder.h
  3. 71
      src/builder/ExplicitPrismModelBuilder.cpp
  4. 10
      src/builder/ExplicitPrismModelBuilder.h
  5. 2
      src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp
  6. 2
      src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h
  7. 17
      src/models/sparse/Model.cpp
  8. 16
      src/models/symbolic/Model.cpp
  9. 17
      src/parser/PrismParser.cpp
  10. 42
      src/storage/DeterministicModelBisimulationDecomposition.cpp
  11. 23
      src/storage/DeterministicModelBisimulationDecomposition.h
  12. 58
      src/utility/cli.cpp
  13. 86
      src/utility/cli.h
  14. 8
      src/utility/vector.h

32
src/builder/DdPrismModelBuilder.cpp
View File

@ -174,18 +174,28 @@ namespace storm {
}
};
template <storm::dd::DdType Type>
DdPrismModelBuilder<Type>::Options::Options() : buildAllRewardModels(false), rewardModelsToBuild(), constantDefinitions() {
DdPrismModelBuilder<Type>::Options::Options() : buildAllRewardModels(true), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(true), labelsToBuild(), expressionLabels() {
// Intentionally left empty.
}
template <storm::dd::DdType Type>
DdPrismModelBuilder<Type>::Options::Options(storm::logic::Formula const& formula) : buildAllRewardModels(false), rewardModelsToBuild(), constantDefinitions(), labelsToBuild(std::set<std::string>()), expressionLabels(std::vector<storm::expressions::Expression>()) {
DdPrismModelBuilder<Type>::Options::Options(storm::logic::Formula const& formula) : buildAllRewardModels(false), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(false), labelsToBuild(std::set<std::string>()), expressionLabels(std::vector<storm::expressions::Expression>()) {
this->preserveFormula(formula);
}
template <storm::dd::DdType Type>
DdPrismModelBuilder<Type>::Options::Options(std::vector<std::shared_ptr<storm::logic::Formula>> const& formulas) : buildAllRewardModels(false), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(false), labelsToBuild(), expressionLabels() {
if (formulas.empty()) {
this->buildAllRewardModels = true;
this->buildAllLabels = true;
} else {
for (auto const& formula : formulas) {
this->preserveFormula(*formula);
}
}
}
template <storm::dd::DdType Type>
void DdPrismModelBuilder<Type>::Options::preserveFormula(storm::logic::Formula const& formula) {
// If we are not required to build all reward models, we determine the reward models we need to build.
@ -844,6 +854,8 @@ namespace storm {
preparedProgram = preparedProgram.substituteConstants();
STORM_LOG_DEBUG("Building representation of program :" << std::endl << preparedProgram << std::endl);
// Start by initializing the structure used for storing all information needed during the model generation.
// In particular, this creates the meta variables used to encode the model.
GenerationInformation generationInfo(preparedProgram);
@ -857,12 +869,22 @@ namespace storm {
// the reward computation might divide by the transition probabilities, which must therefore never be 0.
// However, cutting it to the reachable fragment, there might be zero probability transitions.
std::vector<std::reference_wrapper<storm::prism::RewardModel const>> selectedRewardModels;
// First, we make sure that all selected reward models actually exist.
for (auto const& rewardModelName : options.rewardModelsToBuild) {
STORM_LOG_THROW(rewardModelName.empty() || preparedProgram.hasRewardModel(rewardModelName), storm::exceptions::InvalidArgumentException, "Model does not possess a reward model with the name '" << rewardModelName << "'.");
}
for (auto const& rewardModel : preparedProgram.getRewardModels()) {
if (options.buildAllRewardModels || options.rewardModelsToBuild.find(rewardModel.getName()) != options.rewardModelsToBuild.end()) {
selectedRewardModels.push_back(rewardModel);
}
}
// If no reward model was selected until now and a referenced reward model appears to be unique, we build
// the only existing reward model (given that no explicit name was given for the referenced reward model).
if (selectedRewardModels.empty() && preparedProgram.getNumberOfRewardModels() == 1 && options.rewardModelsToBuild.size() == 1 && *options.rewardModelsToBuild.begin() == "") {
selectedRewardModels.push_back(preparedProgram.getRewardModel(0));
}
std::unordered_map<std::string, storm::models::symbolic::StandardRewardModel<Type, double>> rewardModels;
if (options.buildAllRewardModels || !options.rewardModelsToBuild.empty()) {
for (auto const& rewardModel : preparedProgram.getRewardModels()) {

10
src/builder/DdPrismModelBuilder.h
View File

@ -46,6 +46,13 @@ namespace storm {
*/
Options(storm::logic::Formula const& formula);
/*! Creates an object representing the suggested building options assuming that the given formulas are
* the only ones to check. Additional formulas may be preserved by calling <code>preserveFormula</code>.
*
* @param formula Thes formula based on which to choose the building options.
*/
Options(std::vector<std::shared_ptr<storm::logic::Formula>> const& formulas);
/*!
* Sets the constants definitions from the given string. The string must be of the form 'X=a,Y=b,Z=c',
* etc. where X,Y,Z are the variable names and a,b,c are the values of the constants.
@ -73,6 +80,9 @@ namespace storm {
// An optional mapping that, if given, contains defining expressions for undefined constants.
boost::optional<std::map<storm::expressions::Variable, storm::expressions::Expression>> constantDefinitions;
// A flag indicating whether all labels are to be build.
bool buildAllLabels;
// An optional set of labels that, if given, restricts the labels that are built.
boost::optional<std::set<std::string>> labelsToBuild;

71
src/builder/ExplicitPrismModelBuilder.cpp
View File

@ -104,15 +104,27 @@ namespace storm {
}
template <typename ValueType, typename IndexType>
ExplicitPrismModelBuilder<ValueType, IndexType>::Options::Options() : buildCommandLabels(false), buildAllRewardModels(false), rewardModelsToBuild(), constantDefinitions() {
ExplicitPrismModelBuilder<ValueType, IndexType>::Options::Options() : buildCommandLabels(false), buildAllRewardModels(true), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(true), labelsToBuild(), expressionLabels() {
// Intentionally left empty.
}
template <typename ValueType, typename IndexType>
ExplicitPrismModelBuilder<ValueType, IndexType>::Options::Options(storm::logic::Formula const& formula) : buildCommandLabels(false), buildAllRewardModels(false), rewardModelsToBuild(), constantDefinitions(), labelsToBuild(std::set<std::string>()), expressionLabels(std::vector<storm::expressions::Expression>()) {
ExplicitPrismModelBuilder<ValueType, IndexType>::Options::Options(storm::logic::Formula const& formula) : buildCommandLabels(false), buildAllRewardModels(false), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(false), labelsToBuild(std::set<std::string>()), expressionLabels(std::vector<storm::expressions::Expression>()) {
this->preserveFormula(formula);
}
template <typename ValueType, typename IndexType>
ExplicitPrismModelBuilder<ValueType, IndexType>::Options::Options(std::vector<std::shared_ptr<storm::logic::Formula>> const& formulas) : buildCommandLabels(false), buildAllRewardModels(false), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(false), labelsToBuild(), expressionLabels() {
if (formulas.empty()) {
this->buildAllRewardModels = true;
this->buildAllLabels = true;
} else {
for (auto const& formula : formulas) {
this->preserveFormula(*formula);
}
}
}
template <typename ValueType, typename IndexType>
void ExplicitPrismModelBuilder<ValueType, IndexType>::Options::preserveFormula(storm::logic::Formula const& formula) {
// If we are not required to build all reward models, we determine the reward models we need to build.
@ -124,10 +136,16 @@ namespace storm {
}
// Extract all the labels used in the formula.
if (!buildAllLabels) {
if (!labelsToBuild) {
labelsToBuild = std::set<std::string>();
}
std::vector<std::shared_ptr<storm::logic::AtomicLabelFormula const>> atomicLabelFormulas = formula.getAtomicLabelFormulas();
for (auto const& formula : atomicLabelFormulas) {
labelsToBuild.get().insert(formula.get()->getLabel());
}
}
// Extract all the expressions used in the formula.
std::vector<std::shared_ptr<storm::logic::AtomicExpressionFormula const>> atomicExpressionFormulas = formula.getAtomicExpressionFormulas();
@ -191,8 +209,10 @@ namespace storm {
// If the set of labels we are supposed to built is restricted, we need to remove the other labels from the program.
if (options.labelsToBuild) {
if (!options.buildAllLabels) {
preparedProgram.filterLabels(options.labelsToBuild.get());
}
}
// If we need to build labels for expressions that may appear in some formula, we need to add appropriate
// labels to the program.
@ -210,15 +230,26 @@ namespace storm {
// Now that the program is fixed, we we need to substitute all constants with their concrete value.
preparedProgram = preparedProgram.substituteConstants();
std::cout << preparedProgram << std::endl;
STORM_LOG_DEBUG("Building representation of program :" << std::endl << preparedProgram << std::endl);
// Select the appropriate reward models (after the constants have been substituted).
std::vector<std::reference_wrapper<storm::prism::RewardModel const>> selectedRewardModels;
// First, we make sure that all selected reward models actually exist.
for (auto const& rewardModelName : options.rewardModelsToBuild) {
STORM_LOG_THROW(rewardModelName.empty() || preparedProgram.hasRewardModel(rewardModelName), storm::exceptions::InvalidArgumentException, "Model does not possess a reward model with the name '" << rewardModelName << "'.");
}
for (auto const& rewardModel : preparedProgram.getRewardModels()) {
if (options.buildAllRewardModels || options.rewardModelsToBuild.find(rewardModel.getName()) != options.rewardModelsToBuild.end()) {
selectedRewardModels.push_back(rewardModel);
}
}
// If no reward model was selected until now and a referenced reward model appears to be unique, we build
// the only existing reward model (given that no explicit name was given for the referenced reward model).
if (selectedRewardModels.empty() && preparedProgram.getNumberOfRewardModels() == 1 && options.rewardModelsToBuild.size() == 1 && *options.rewardModelsToBuild.begin() == "") {
selectedRewardModels.push_back(preparedProgram.getRewardModel(0));
}
ModelComponents modelComponents = buildModelComponents(preparedProgram, selectedRewardModels, options);
@ -554,6 +585,18 @@ namespace storm {
}
transitionMatrixBuilder.addNextValue(currentRow, stateIndex, storm::utility::one<ValueType>());
auto builderIt = rewardModelBuilders.begin();
for (auto rewardModelIt = selectedRewardModels.begin(), rewardModelIte = selectedRewardModels.end(); rewardModelIt != rewardModelIte; ++rewardModelIt, ++builderIt) {
if (rewardModelIt->get().hasStateRewards()) {
builderIt->stateRewardVector.push_back(storm::utility::zero<ValueType>());
}
if (rewardModelIt->get().hasStateActionRewards()) {
builderIt->stateActionRewardVector.push_back(storm::utility::zero<ValueType>());
}
}
++currentRow;
} else {
STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Error while creating sparse matrix from probabilistic program: found deadlock state. For fixing these, please provide the appropriate option.");
@ -616,20 +659,20 @@ namespace storm {
auto builderIt = rewardModelBuilders.begin();
for (auto rewardModelIt = selectedRewardModels.begin(), rewardModelIte = selectedRewardModels.end(); rewardModelIt != rewardModelIte; ++rewardModelIt, ++builderIt) {
if (rewardModelIt->get().hasStateRewards()) {
builderIt->stateRewardVector.resize(currentRow + 1);
builderIt->stateRewardVector.push_back(storm::utility::zero<ValueType>());
for (auto const& stateReward : rewardModelIt->get().getStateRewards()) {
if (evaluator.asBool(stateReward.getStatePredicateExpression())) {
builderIt->stateRewardVector[currentRow] += ValueType(evaluator.asRational(stateReward.getRewardValueExpression()));
builderIt->stateRewardVector.back() += ValueType(evaluator.asRational(stateReward.getRewardValueExpression()));
}
}
}
if (rewardModelIt->get().hasStateActionRewards()) {
builderIt->stateActionRewardVector.resize(currentRow + 1);
builderIt->stateActionRewardVector.push_back(storm::utility::zero<ValueType>());
for (auto const& stateActionReward : rewardModelIt->get().getStateActionRewards()) {
if (!stateActionReward.isLabeled()) {
if (evaluator.asBool(stateActionReward.getStatePredicateExpression())) {
builderIt->stateActionRewardVector[currentRow] += ValueType(evaluator.asRational(stateActionReward.getRewardValueExpression())) / totalNumberOfChoices;
builderIt->stateActionRewardVector.back() += ValueType(evaluator.asRational(stateActionReward.getRewardValueExpression())) / totalNumberOfChoices;
}
}
}
@ -652,20 +695,18 @@ namespace storm {
auto builderIt = rewardModelBuilders.begin();
for (auto rewardModelIt = selectedRewardModels.begin(), rewardModelIte = selectedRewardModels.end(); rewardModelIt != rewardModelIte; ++rewardModelIt, ++builderIt) {
if (rewardModelIt->get().hasStateRewards()) {
builderIt->stateRewardVector.resize(currentRow + 1);
for (auto const& stateReward : rewardModelIt->get().getStateRewards()) {
if (evaluator.asBool(stateReward.getStatePredicateExpression())) {
builderIt->stateRewardVector[currentRow] += ValueType(evaluator.asRational(stateReward.getRewardValueExpression()));
builderIt->stateRewardVector.back() += ValueType(evaluator.asRational(stateReward.getRewardValueExpression()));
}
}
}
if (rewardModelIt->get().hasStateActionRewards()) {
builderIt->stateActionRewardVector.resize(currentRow + 1);
for (auto const& stateActionReward : rewardModelIt->get().getStateActionRewards()) {
if (stateActionReward.isLabeled() && stateActionReward.getActionIndex() == choice.getActionIndex()) {
if (evaluator.asBool(stateActionReward.getStatePredicateExpression())) {
builderIt->stateActionRewardVector[currentRow] += ValueType(evaluator.asRational(stateActionReward.getRewardValueExpression())) / totalNumberOfChoices;
builderIt->stateActionRewardVector.back() += ValueType(evaluator.asRational(stateActionReward.getRewardValueExpression())) / totalNumberOfChoices;
}
}
}
@ -719,11 +760,11 @@ namespace storm {
auto builderIt = rewardModelBuilders.begin();
for (auto rewardModelIt = selectedRewardModels.begin(), rewardModelIte = selectedRewardModels.end(); rewardModelIt != rewardModelIte; ++rewardModelIt, ++builderIt) {
if (rewardModelIt->get().hasStateActionRewards()) {
builderIt->stateActionRewardVector.resize(currentRow + 1);
builderIt->stateActionRewardVector.push_back(storm::utility::zero<ValueType>());
for (auto const& stateActionReward : rewardModelIt->get().getStateActionRewards()) {
if (!stateActionReward.isLabeled()) {
if (evaluator.asBool(stateActionReward.getStatePredicateExpression())) {
builderIt->stateActionRewardVector[currentRow] += ValueType(evaluator.asRational(stateActionReward.getRewardValueExpression()));
builderIt->stateActionRewardVector.back() += ValueType(evaluator.asRational(stateActionReward.getRewardValueExpression()));
}
}
}
@ -747,11 +788,11 @@ namespace storm {
auto builderIt = rewardModelBuilders.begin();
for (auto rewardModelIt = selectedRewardModels.begin(), rewardModelIte = selectedRewardModels.end(); rewardModelIt != rewardModelIte; ++rewardModelIt, ++builderIt) {
if (rewardModelIt->get().hasStateActionRewards()) {
builderIt->stateActionRewardVector.resize(currentRow + 1);
builderIt->stateActionRewardVector.push_back(storm::utility::zero<ValueType>());
for (auto const& stateActionReward : rewardModelIt->get().getStateActionRewards()) {
if (stateActionReward.isLabeled() && stateActionReward.getActionIndex() == choice.getActionIndex()) {
if (evaluator.asBool(stateActionReward.getStatePredicateExpression())) {
builderIt->stateActionRewardVector[currentRow] += ValueType(evaluator.asRational(stateActionReward.getRewardValueExpression()));
builderIt->stateActionRewardVector.back() += ValueType(evaluator.asRational(stateActionReward.getRewardValueExpression()));
}
}
}

10
src/builder/ExplicitPrismModelBuilder.h
View File

@ -133,6 +133,13 @@ namespace storm {
*/
Options(storm::logic::Formula const& formula);
/*! Creates an object representing the suggested building options assuming that the given formulas are
* the only ones to check. Additional formulas may be preserved by calling <code>preserveFormula</code>.
*
* @param formula Thes formula based on which to choose the building options.
*/
Options(std::vector<std::shared_ptr<storm::logic::Formula>> const& formulas);
/*!
* Sets the constants definitions from the given string. The string must be of the form 'X=a,Y=b,Z=c',
* etc. where X,Y,Z are the variable names and a,b,c are the values of the constants.
@ -163,6 +170,9 @@ namespace storm {
// An optional mapping that, if given, contains defining expressions for undefined constants.
boost::optional<std::map<storm::expressions::Variable, storm::expressions::Expression>> constantDefinitions;
// A flag that indicates whether all labels are to be build.
bool buildAllLabels;
// An optional set of labels that, if given, restricts the labels that are built.
boost::optional<std::set<std::string>> labelsToBuild;

2
src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp
View File

@ -159,7 +159,7 @@ namespace storm {
}
template<typename ValueType, typename RewardModelType>
std::vector<ValueType> SparseDtmcPrctlHelper<ValueType, RewardModelType>::computeReachabilityRewards(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, std::function<std::vector<ValueType> const&(uint_fast64_t, storm::storage::SparseMatrix<ValueType> const&, storm::storage::BitVector const&)> const& totalStateRewardVectorGetter, storm::storage::BitVector const& targetStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory) {
std::vector<ValueType> SparseDtmcPrctlHelper<ValueType, RewardModelType>::computeReachabilityRewards(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, std::function<std::vector<ValueType>(uint_fast64_t, storm::storage::SparseMatrix<ValueType> const&, storm::storage::BitVector const&)> const& totalStateRewardVectorGetter, storm::storage::BitVector const& targetStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory) {
// Determine which states have a reward of infinity by definition.
storm::storage::BitVector trueStates(transitionMatrix.getRowCount(), true);

2
src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h
View File

@ -34,7 +34,7 @@ namespace storm {
static std::vector<ValueType> computeLongRunAverage(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::BitVector const& psiStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory);
private:
static std::vector<ValueType> computeReachabilityRewards(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, std::function<std::vector<ValueType> const&(uint_fast64_t, storm::storage::SparseMatrix<ValueType> const&, storm::storage::BitVector const&)> const& totalStateRewardVectorGetter, storm::storage::BitVector const& targetStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory);
static std::vector<ValueType> computeReachabilityRewards(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, std::function<std::vector<ValueType>(uint_fast64_t, storm::storage::SparseMatrix<ValueType> const&, storm::storage::BitVector const&)> const& totalStateRewardVectorGetter, storm::storage::BitVector const& targetStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory);
};
}

17
src/models/sparse/Model.cpp
View File

@ -90,7 +90,17 @@ namespace storm {
template<typename ValueType, typename RewardModelType>
RewardModelType const& Model<ValueType, RewardModelType>::getRewardModel(std::string const& rewardModelName) const {
auto it = this->rewardModels.find(rewardModelName);
STORM_LOG_THROW(it != this->rewardModels.end(), storm::exceptions::IllegalArgumentException, "The requested reward model '" << rewardModelName << "' does not exist.");
if (it == this->rewardModels.end()) {
if (rewardModelName.empty()) {
if (this->hasUniqueRewardModel()) {
return this->getUniqueRewardModel()->second;
} else {
STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentException, "Unable to refer to default reward model, because there is no default model or it is not unique.");
}
} else {
STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentException, "The requested reward model '" << rewardModelName << "' does not exist.");
}
}
return it->second;
}
@ -178,7 +188,10 @@ namespace storm {
void Model<ValueType, RewardModelType>::printRewardModelsInformationToStream(std::ostream& out) const {
if (this->rewardModels.size()) {
std::vector<std::string> rewardModelNames;
std::for_each(this->rewardModels.cbegin(), this->rewardModels.cend(), [&rewardModelNames] (typename std::pair<std::string, RewardModelType> const& nameRewardModelPair) { rewardModelNames.push_back(nameRewardModelPair.first); });
std::for_each(this->rewardModels.cbegin(), this->rewardModels.cend(),
[&rewardModelNames] (typename std::pair<std::string, RewardModelType> const& nameRewardModelPair) {
if (nameRewardModelPair.first.empty()) { rewardModelNames.push_back("(default)"); } else { rewardModelNames.push_back(nameRewardModelPair.first); }
});
out << "Reward Models: " << boost::join(rewardModelNames, ", ") << std::endl;
} else {
out << "Reward Models: none" << std::endl;

16
src/models/symbolic/Model.cpp
View File

@ -1,6 +1,6 @@
#include "src/models/symbolic/Model.h"
#include "src/exceptions/InvalidArgumentException.h"
#include "src/exceptions/IllegalArgumentException.h"
#include "src/adapters/AddExpressionAdapter.h"
@ -60,7 +60,7 @@ namespace storm {
template<storm::dd::DdType Type>
storm::dd::Bdd<Type> Model<Type>::getStates(std::string const& label) const {
STORM_LOG_THROW(labelToExpressionMap.find(label) != labelToExpressionMap.end(), storm::exceptions::InvalidArgumentException, "The label " << label << " is invalid for the labeling of the model.");
STORM_LOG_THROW(labelToExpressionMap.find(label) != labelToExpressionMap.end(), storm::exceptions::IllegalArgumentException, "The label " << label << " is invalid for the labeling of the model.");
return rowExpressionAdapter->translateExpression(labelToExpressionMap.at(label)).toBdd() && this->reachableStates;
}
@ -132,7 +132,17 @@ namespace storm {
template<storm::dd::DdType Type>
typename Model<Type>::RewardModelType const& Model<Type>::getRewardModel(std::string const& rewardModelName) const {
auto it = this->rewardModels.find(rewardModelName);
STORM_LOG_THROW(it != this->rewardModels.end(), storm::exceptions::InvalidArgumentException, "The requested reward model '" << rewardModelName << "' does not exist.");
if (it == this->rewardModels.end()) {
if (rewardModelName.empty()) {
if (this->hasUniqueRewardModel()) {
return this->getUniqueRewardModel()->second;
} else {
STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentException, "Unable to refer to default reward model, because there is no default model or it is not unique.");
}
} else {
STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentException, "The requested reward model '" << rewardModelName << "' does not exist.");
}
}
return it->second;
}

17
src/parser/PrismParser.cpp
View File

@ -406,14 +406,12 @@ namespace storm {
STORM_LOG_ASSERT(!this->secondRun, "Dummy procedure must not be called in second run.");
std::string realActionName = actionName ? actionName.get() : "";
if (!actionName) {
// Register the action name if it has not appeared earlier.
auto nameIndexPair = globalProgramInformation.actionIndices.find(realActionName);
if (nameIndexPair == globalProgramInformation.actionIndices.end()) {
std::size_t nextIndex = globalProgramInformation.actionIndices.size();
globalProgramInformation.actionIndices.emplace(realActionName, nextIndex);
}
}
return storm::prism::Command();
}
@ -476,6 +474,21 @@ namespace storm {
this->identifiers_.add(renamingPair->second, renamedVariable.getExpression());
}
for (auto const& command : moduleToRename.getCommands()) {
std::string newActionName = command.getActionName();
auto const& renamingPair = renaming.find(command.getActionName());
if (renamingPair != renaming.end()) {
newActionName = renamingPair->second;
}
// Record any newly occurring action names/indices.
auto nameIndexPair = globalProgramInformation.actionIndices.find(newActionName);
if (nameIndexPair == globalProgramInformation.actionIndices.end()) {
std::size_t nextIndex = globalProgramInformation.actionIndices.size();
globalProgramInformation.actionIndices.emplace(newActionName, nextIndex);
}
}
// Return a dummy module in the first pass.
return storm::prism::Module();
} else {

42
src/storage/DeterministicModelBisimulationDecomposition.cpp
View File

@ -602,6 +602,43 @@ namespace storm {
template<typename ValueType>
DeterministicModelBisimulationDecomposition<ValueType>::Options::Options(storm::models::sparse::Model<ValueType> const& model, storm::logic::Formula const& formula) : Options() {
this->preserveSingleFormula(model, formula);
}
template<typename ValueType>
DeterministicModelBisimulationDecomposition<ValueType>::Options::Options(storm::models::sparse::Model<ValueType> const& model, std::vector<std::shared_ptr<storm::logic::Formula>> const& formulas) : Options() {
if (formulas.size() == 1) {
this->preserveSingleFormula(model, *formulas.front());
} else {
for (auto const& formula : formulas) {
std::vector<std::shared_ptr<storm::logic::AtomicExpressionFormula const>> atomicExpressionFormulas = formula->getAtomicExpressionFormulas();
std::vector<std::shared_ptr<storm::logic::AtomicLabelFormula const>> atomicLabelFormulas = formula->getAtomicLabelFormulas();
std::set<std::string> labelsToRespect;
for (auto const& labelFormula : atomicLabelFormulas) {
labelsToRespect.insert(labelFormula->getLabel());
}
for (auto const& expressionFormula : atomicExpressionFormulas) {
std::stringstream stream;
stream << *expressionFormula;
labelsToRespect.insert(stream.str());
}
if (!respectedAtomicPropositions) {
respectedAtomicPropositions = labelsToRespect;
} else {
respectedAtomicPropositions.get().insert(labelsToRespect.begin(), labelsToRespect.end());
}
}
}
}
template<typename ValueType>
DeterministicModelBisimulationDecomposition<ValueType>::Options::Options() : measureDrivenInitialPartition(false), phiStates(), psiStates(), respectedAtomicPropositions(), keepRewards(true), weak(false), bounded(true), buildQuotient(true) {
// Intentionally left empty.
}
template<typename ValueType>
void DeterministicModelBisimulationDecomposition<ValueType>::Options::preserveSingleFormula(storm::models::sparse::Model<ValueType> const& model, storm::logic::Formula const& formula) {
if (!formula.containsRewardOperator()) {
this->keepRewards = false;
}
@ -664,11 +701,6 @@ namespace storm {
}
}
template<typename ValueType>
DeterministicModelBisimulationDecomposition<ValueType>::Options::Options() : measureDrivenInitialPartition(false), phiStates(), psiStates(), respectedAtomicPropositions(), keepRewards(true), weak(false), bounded(true), buildQuotient(true) {
// Intentionally left empty.
}
template<typename ValueType>
DeterministicModelBisimulationDecomposition<ValueType>::DeterministicModelBisimulationDecomposition(storm::models::sparse::Dtmc<ValueType> const& model, Options const& options) {
STORM_LOG_THROW(!model.hasRewardModel() || model.hasUniqueRewardModel(), storm::exceptions::IllegalFunctionCallException, "Bisimulation currently only supports models with at most one reward model.");

23
src/storage/DeterministicModelBisimulationDecomposition.h
View File

@ -29,8 +29,8 @@ namespace storm {
Options();
/*!
* Creates an object representing the options necessary to obtain the smallest quotient while still
* preserving the given formula.
* Creates an object representing the options necessary to obtain the quotient while still preserving
* the given formula.
*
* @param The model for which the quotient model shall be computed. This needs to be given in order to
* derive a suitable initial partition.
@ -38,6 +38,16 @@ namespace storm {
*/
Options(storm::models::sparse::Model<ValueType> const& model, storm::logic::Formula const& formula);
/*!
* Creates an object representing the options necessary to obtain the smallest quotient while still
* preserving the given formula.
*
* @param The model for which the quotient model shall be computed. This needs to be given in order to
* derive a suitable initial partition.
* @param formulas The formula that is to be preserved.
*/
Options(storm::models::sparse::Model<ValueType> const& model, std::vector<std::shared_ptr<storm::logic::Formula>> const& formulas);
// A flag that indicates whether a measure driven initial partition is to be used. If this flag is set
// to true, the two optional pairs phiStatesAndLabel and psiStatesAndLabel must be set. Then, the
// measure driven initial partition wrt. to the states phi and psi is taken.
@ -62,6 +72,15 @@ namespace storm {
// A flag that governs whether the quotient model is actually built or only the decomposition is computed.
bool buildQuotient;
private:
/*!
* Sets the options under the assumption that the given formula is the only one that is to be checked.
*
* @param model The model for which to preserve the formula.
* @param formula The only formula to check.
*/
void preserveSingleFormula(storm::models::sparse::Model<ValueType> const& model, storm::logic::Formula const& formula);
};
/*!

58
src/utility/cli.cpp
View File

@ -218,9 +218,9 @@ namespace storm {
}
// Then proceed to parsing the property (if given), since the model we are building may depend on the property.
std::vector<boost::optional<std::shared_ptr<storm::logic::Formula>>> formulas;
std::vector<std::shared_ptr<storm::logic::Formula>> formulas;
if (settings.isPropertySet()) {
boost::optional<std::shared_ptr<storm::logic::Formula>> formula;
std::shared_ptr<storm::logic::Formula> formula;
if (program) {
storm::parser::FormulaParser formulaParser(program.get().getManager().getSharedPointer());
formula = formulaParser.parseFromString(settings.getProperty());
@ -229,70 +229,26 @@ namespace storm {
formula = formulaParser.parseFromString(settings.getProperty());
}
formulas.push_back(formula);
} else if (settings.isPropertyFileSet()) {
// FIXME: asap.
}
else if (settings.isPropertyFileSet()) {
std::cout << "Reading properties from " << settings.getPropertiesFilename() << std::endl;
std::ifstream inputFileStream(settings.getPropertiesFilename(), std::ios::in);
std::vector<std::string> properties;
if (inputFileStream.good()) {
try {
while (inputFileStream.good()) {
std::string prop;
std::getline(inputFileStream, prop);
if (!prop.empty()) {
properties.push_back(prop);
}
}
}
catch (std::exception& e) {
inputFileStream.close();
throw e;
}
inputFileStream.close();
} else {
STORM_LOG_ERROR("Unable to read property file.");
}
for (std::string prop : properties) {
boost::optional<std::shared_ptr<storm::logic::Formula>> formula;
try {
if (program) {
storm::parser::FormulaParser formulaParser(program.get().getManager().getSharedPointer());
formula = formulaParser.parseFromString(prop);
} else {
storm::parser::FormulaParser formulaParser;
formula = formulaParser.parseFromString(prop);
}
formulas.push_back(formula);
}
catch (storm::exceptions::WrongFormatException &e) {
STORM_LOG_WARN("Unable to parse line as formula: " << prop);
}
}
std::cout << "Parsed " << formulas.size() << " properties from file " << settings.getPropertiesFilename() << std::endl;
}
for (boost::optional<std::shared_ptr<storm::logic::Formula>> formula : formulas) {
if (settings.isSymbolicSet()) {
#ifdef STORM_HAVE_CARL
if (settings.isParametricSet()) {
buildAndCheckSymbolicModel<storm::RationalFunction>(program.get(), formula);
buildAndCheckSymbolicModel<storm::RationalFunction>(program.get(), formulas);
} else {
#endif
buildAndCheckSymbolicModel<double>(program.get(), formula);
buildAndCheckSymbolicModel<double>(program.get(), formulas);
#ifdef STORM_HAVE_CARL
}
#endif
} else if (settings.isExplicitSet()) {
buildAndCheckExplicitModel<double>(formula);
buildAndCheckExplicitModel<double>(formulas);
} else {
STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "No input model.");
}
}
}
}
}

86
src/utility/cli.h
View File

@ -93,7 +93,7 @@ namespace storm {
}
template<typename ValueType>
std::shared_ptr<storm::models::ModelBase> buildSymbolicModel(storm::prism::Program const& program, boost::optional<std::shared_ptr<storm::logic::Formula>> const& formula) {
std::shared_ptr<storm::models::ModelBase> buildSymbolicModel(storm::prism::Program const& program, std::vector<std::shared_ptr<storm::logic::Formula>> const& formulas) {
std::shared_ptr<storm::models::ModelBase> result(nullptr);
storm::settings::modules::GeneralSettings settings = storm::settings::generalSettings();
@ -104,9 +104,7 @@ namespace storm {
// Customize and perform model-building.
if (settings.getEngine() == storm::settings::modules::GeneralSettings::Engine::Sparse) {
typename storm::builder::ExplicitPrismModelBuilder<ValueType>::Options options;
if (formula) {
options = typename storm::builder::ExplicitPrismModelBuilder<ValueType>::Options(*formula.get());
}
options = typename storm::builder::ExplicitPrismModelBuilder<ValueType>::Options(formulas);
options.addConstantDefinitionsFromString(program, settings.getConstantDefinitionString());
// Generate command labels if we are going to build a counterexample later.
@ -117,9 +115,7 @@ namespace storm {
result = storm::builder::ExplicitPrismModelBuilder<ValueType>::translateProgram(program, options);
} else if (settings.getEngine() == storm::settings::modules::GeneralSettings::Engine::Dd || settings.getEngine() == storm::settings::modules::GeneralSettings::Engine::Hybrid) {
typename storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::Options options;
if (formula) {
options = typename storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::Options(*formula.get());
}
options = typename storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::Options(formulas);
options.addConstantDefinitionsFromString(program, settings.getConstantDefinitionString());
result = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::translateProgram(program, options);
@ -130,7 +126,7 @@ namespace storm {
}
template<typename ValueType>
std::shared_ptr<storm::models::ModelBase> preprocessModel(std::shared_ptr<storm::models::ModelBase> model, boost::optional<std::shared_ptr<storm::logic::Formula>> const& formula) {
std::shared_ptr<storm::models::ModelBase> preprocessModel(std::shared_ptr<storm::models::ModelBase> model, std::vector<std::shared_ptr<storm::logic::Formula>> const& formulas) {
if (storm::settings::generalSettings().isBisimulationSet()) {
STORM_LOG_THROW(model->isSparseModel(), storm::exceptions::InvalidSettingsException, "Bisimulation minimization is currently only available for sparse models.");
std::shared_ptr<storm::models::sparse::Model<ValueType>> sparseModel = model->template as<storm::models::sparse::Model<ValueType>>();
@ -141,8 +137,8 @@ namespace storm {
std::cout << "Performing bisimulation minimization... ";
typename storm::storage::DeterministicModelBisimulationDecomposition<ValueType>::Options options;
if (formula) {
options = typename storm::storage::DeterministicModelBisimulationDecomposition<ValueType>::Options(*sparseModel, *formula.get());
if (!formulas.empty()) {
options = typename storm::storage::DeterministicModelBisimulationDecomposition<ValueType>::Options(*sparseModel, formulas);
}
if (storm::settings::bisimulationSettings().isWeakBisimulationSet()) {
options.weak = true;
@ -157,7 +153,7 @@ namespace storm {
}
template<typename ValueType>
void generateCounterexample(storm::prism::Program const& program, std::shared_ptr<storm::models::sparse::Model<ValueType>> model, std::shared_ptr<storm::logic::Formula> formula) {
void generateCounterexample(storm::prism::Program const& program, std::shared_ptr<storm::models::sparse::Model<ValueType>> model, std::shared_ptr<storm::logic::Formula> const& formula) {
if (storm::settings::counterexampleGeneratorSettings().isMinimalCommandSetGenerationSet()) {
STORM_LOG_THROW(model->getType() == storm::models::ModelType::Mdp, storm::exceptions::InvalidTypeException, "Minimal command set generation is only available for MDPs.");
STORM_LOG_THROW(storm::settings::generalSettings().isSymbolicSet(), storm::exceptions::InvalidSettingsException, "Minimal command set generation is only available for symbolic models.");
@ -180,15 +176,16 @@ namespace storm {
#ifdef STORM_HAVE_CARL
template<>
inline void generateCounterexample(storm::prism::Program const& program, std::shared_ptr<storm::models::sparse::Model<storm::RationalFunction>> model, std::shared_ptr<storm::logic::Formula> formula) {
inline void generateCounterexample(storm::prism::Program const& program, std::shared_ptr<storm::models::sparse::Model<storm::RationalFunction>> model, std::shared_ptr<storm::logic::Formula> const& formula) {
STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Unable to generate counterexample for parametric model.");
}
#endif
template<typename ValueType>
void verifySparseModel(boost::optional<storm::prism::Program> const& program, std::shared_ptr<storm::models::sparse::Model<ValueType>> model, std::shared_ptr<storm::logic::Formula> formula) {
void verifySparseModel(boost::optional<storm::prism::Program> const& program, std::shared_ptr<storm::models::sparse::Model<ValueType>> model, std::vector<std::shared_ptr<storm::logic::Formula>> const& formulas) {
storm::settings::modules::GeneralSettings const& settings = storm::settings::generalSettings();
for (auto const& formula : formulas) {
// If we were requested to generate a counterexample, we now do so.
if (settings.isCounterexampleSet()) {
STORM_LOG_THROW(program, storm::exceptions::InvalidSettingsException, "Unable to generate counterexample for non-symbolic model.");
@ -199,12 +196,12 @@ namespace storm {
if (model->getType() == storm::models::ModelType::Dtmc) {
std::shared_ptr<storm::models::sparse::Dtmc<ValueType>> dtmc = model->template as<storm::models::sparse::Dtmc<ValueType>>();
storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<ValueType>> modelchecker(*dtmc);
if (modelchecker.canHandle(*formula.get())) {
result = modelchecker.check(*formula.get());
if (modelchecker.canHandle(*formula)) {
result = modelchecker.check(*formula);
} else {
storm::modelchecker::SparseDtmcEliminationModelChecker<storm::models::sparse::Dtmc<ValueType>> modelchecker2(*dtmc);
if (modelchecker2.canHandle(*formula.get())) {
result = modelchecker2.check(*formula.get());
if (modelchecker2.canHandle(*formula)) {
result = modelchecker2.check(*formula);
}
}
} else if (model->getType() == storm::models::ModelType::Mdp) {
@ -212,20 +209,20 @@ namespace storm {
#ifdef STORM_HAVE_CUDA
if (settings.isCudaSet()) {
storm::modelchecker::TopologicalValueIterationMdpPrctlModelChecker<ValueType> modelchecker(*mdp);
result = modelchecker.check(*formula.get());
result = modelchecker.check(*formula);
} else {
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<ValueType>> modelchecker(*mdp);
result = modelchecker.check(*formula.get());
result = modelchecker.check(*formula);
}
#else
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<ValueType>> modelchecker(*mdp);
result = modelchecker.check(*formula.get());
result = modelchecker.check(*formula);
#endif
} else if (model->getType() == storm::models::ModelType::Ctmc) {
std::shared_ptr<storm::models::sparse::Ctmc<ValueType>> ctmc = model->template as<storm::models::sparse::Ctmc<ValueType>>();
storm::modelchecker::SparseCtmcCslModelChecker<storm::models::sparse::Ctmc<ValueType>> modelchecker(*ctmc);
result = modelchecker.check(*formula.get());
result = modelchecker.check(*formula);
}
if (result) {
@ -236,7 +233,7 @@ namespace storm {
} else {
std::cout << " skipped, because the modelling formalism is currently unsupported." << std::endl;
}
}
}
}
@ -258,8 +255,9 @@ namespace storm {
}
template<>
inline void verifySparseModel(boost::optional<storm::prism::Program> const& program, std::shared_ptr<storm::models::sparse::Model<storm::RationalFunction>> model, std::shared_ptr<storm::logic::Formula> formula) {
inline void verifySparseModel(boost::optional<storm::prism::Program> const& program, std::shared_ptr<storm::models::sparse::Model<storm::RationalFunction>> model, std::vector<std::shared_ptr<storm::logic::Formula>> const& formulas) {
for (auto const& formula : formulas) {
STORM_LOG_THROW(model->getType() == storm::models::ModelType::Dtmc, storm::exceptions::InvalidSettingsException, "Currently parametric verification is only available for DTMCs.");
std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> dtmc = model->template as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
@ -267,8 +265,8 @@ namespace storm {
std::unique_ptr<storm::modelchecker::CheckResult> result;
storm::modelchecker::SparseDtmcEliminationModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>> modelchecker(*dtmc);
if (modelchecker.canHandle(*formula.get())) {
result = modelchecker.check(*formula.get());
if (modelchecker.canHandle(*formula)) {
result = modelchecker.check(*formula);
} else {
STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "The parametric engine currently does not support this property.");
}
@ -287,30 +285,31 @@ namespace storm {
exportParametricResultToFile(result->asExplicitQuantitativeCheckResult<storm::RationalFunction>()[*dtmc->getInitialStates().begin()], storm::models::sparse::Dtmc<storm::RationalFunction>::ConstraintCollector(*dtmc), parametricSettings.exportResultPath());
}
}
}
#endif
template<storm::dd::DdType DdType>
void verifySymbolicModel(boost::optional<storm::prism::Program> const& program, std::shared_ptr<storm::models::symbolic::Model<DdType>> model, std::shared_ptr<storm::logic::Formula> formula) {
void verifySymbolicModel(boost::optional<storm::prism::Program> const& program, std::shared_ptr<storm::models::symbolic::Model<DdType>> model, std::vector<std::shared_ptr<storm::logic::Formula>> const& formulas) {
for (auto const& formula : formulas) {
std::cout << std::endl << "Model checking property: " << *formula << " ...";
std::unique_ptr<storm::modelchecker::CheckResult> result;
if (model->getType() == storm::models::ModelType::Dtmc) {
std::shared_ptr<storm::models::symbolic::Dtmc<DdType>> dtmc = model->template as<storm::models::symbolic::Dtmc<DdType>>();
storm::modelchecker::HybridDtmcPrctlModelChecker<DdType, double> modelchecker(*dtmc);
if (modelchecker.canHandle(*formula.get())) {
result = modelchecker.check(*formula.get());
if (modelchecker.canHandle(*formula)) {
result = modelchecker.check(*formula);
}
} else if (model->getType() == storm::models::ModelType::Ctmc) {
std::shared_ptr<storm::models::symbolic::Ctmc<DdType>> ctmc = model->template as<storm::models::symbolic::Ctmc<DdType>>();
storm::modelchecker::HybridCtmcCslModelChecker<DdType, double> modelchecker(*ctmc);
if (modelchecker.canHandle(*formula.get())) {
result = modelchecker.check(*formula.get());
if (modelchecker.canHandle(*formula)) {
result = modelchecker.check(*formula);
}
} else if (model->getType() == storm::models::ModelType::Mdp) {
std::shared_ptr<storm::models::symbolic::Mdp<DdType>> mdp = model->template as<storm::models::symbolic::Mdp<DdType>>();
storm::modelchecker::HybridMdpPrctlModelChecker<DdType, double> modelchecker(*mdp);
if (modelchecker.canHandle(*formula.get())) {
result = modelchecker.check(*formula.get());
if (modelchecker.canHandle(*formula)) {
result = modelchecker.check(*formula);
}
} else {
STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This functionality is not yet implemented.");
@ -325,28 +324,29 @@ namespace storm {
std::cout << " skipped, because the modelling formalism is currently unsupported." << std::endl;
}
}
}
template<typename ValueType>
void buildAndCheckSymbolicModel(boost::optional<storm::prism::Program> const& program, boost::optional<std::shared_ptr<storm::logic::Formula>> formula) {
void buildAndCheckSymbolicModel(boost::optional<storm::prism::Program> const& program, std::vector<std::shared_ptr<storm::logic::Formula>> const& formulas) {
// Now we are ready to actually build the model.
STORM_LOG_THROW(program, storm::exceptions::InvalidStateException, "Program has not been successfully parsed.");
std::shared_ptr<storm::models::ModelBase> model = buildSymbolicModel<ValueType>(program.get(), formula);
std::shared_ptr<storm::models::ModelBase> model = buildSymbolicModel<ValueType>(program.get(), formulas);
STORM_LOG_THROW(model != nullptr, storm::exceptions::InvalidStateException, "Model could not be constructed for an unknown reason.");
// Preprocess the model if needed.
model = preprocessModel<ValueType>(model, formula);
model = preprocessModel<ValueType>(model, formulas);
// Print some information about the model.
model->printModelInformationToStream(std::cout);
// Verify the model, if a formula was given.
if (formula) {
if (!formulas.empty()) {
if (model->isSparseModel()) {
verifySparseModel<ValueType>(program, model->as<storm::models::sparse::Model<ValueType>>(), formula.get());
verifySparseModel<ValueType>(program, model->as<storm::models::sparse::Model<ValueType>>(), formulas);
} else if (model->isSymbolicModel()) {
if (storm::settings::generalSettings().getEngine() == storm::settings::modules::GeneralSettings::Engine::Hybrid) {
verifySymbolicModel(program, model->as<storm::models::symbolic::Model<storm::dd::DdType::CUDD>>(), formula.get());
verifySymbolicModel(program, model->as<storm::models::symbolic::Model<storm::dd::DdType::CUDD>>(), formulas);
} else {
// Not handled yet.
STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This functionality is not yet implemented.");
@ -358,22 +358,22 @@ namespace storm {
}
template<typename ValueType>
void buildAndCheckExplicitModel(boost::optional<std::shared_ptr<storm::logic::Formula>> formula) {
void buildAndCheckExplicitModel(std::vector<std::shared_ptr<storm::logic::Formula>> const& formulas) {
storm::settings::modules::GeneralSettings const& settings = storm::settings::generalSettings();
STORM_LOG_THROW(settings.isExplicitSet(), storm::exceptions::InvalidStateException, "Unable to build explicit model without model files.");
std::shared_ptr<storm::models::ModelBase> model = buildExplicitModel<ValueType>(settings.getTransitionFilename(), settings.getLabelingFilename(), settings.isStateRewardsSet() ? settings.getStateRewardsFilename() : boost::optional<std::string>(), settings.isTransitionRewardsSet() ? settings.getTransitionRewardsFilename() : boost::optional<std::string>());
// Preprocess the model if needed.
model = preprocessModel<ValueType>(model, formula);
model = preprocessModel<ValueType>(model, formulas);
// Print some information about the model.
model->printModelInformationToStream(std::cout);
// Verify the model, if a formula was given.
if (formula) {
if (!formulas.empty()) {
STORM_LOG_THROW(model->isSparseModel(), storm::exceptions::InvalidStateException, "Expected sparse model.");
verifySparseModel<ValueType>(boost::optional<storm::prism::Program>(), model->as<storm::models::sparse::Model<ValueType>>(), formula.get());
verifySparseModel<ValueType>(boost::optional<storm::prism::Program>(), model->as<storm::models::sparse::Model<ValueType>>(), formulas);
}
}

8
src/utility/vector.h
View File

@ -136,7 +136,8 @@ namespace storm {
auto it = source.cbegin() + rowGroupIndices[group];
auto ite = source.cbegin() + rowGroupIndices[group + 1];
while (it != ite) {
target[currentPosition] = *it;
target[currentPosition] += *it;
++currentPosition;
++it;
}
}
@ -162,7 +163,7 @@ namespace storm {
++rowGroupIt;
uint_fast64_t next = *rowGroupIt;
while (current < next) {
*targetIt = *sourceIt;
*targetIt += *sourceIt;
++targetIt;
}
}
@ -183,8 +184,9 @@ namespace storm {
uint_fast64_t current = rowGroupIndices[group];
uint_fast64_t next = rowGroupIndices[group + 1];
while (current < next) {
target[currentPosition] = source[group];
target[currentPosition] += source[group];
++currentPosition;
++current;
}
}
}

Write Preview
Loading…
Cancel
Save