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

added special label 'deadlock' to models and builders 

Former-commit-id: 4edc57216e
tempestpy_adaptions
dehnert 9 years ago
parent
74ee726e35
commit
512a1ec558
25 changed files with 152 additions and 64 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/DdJaniModelBuilder.cpp
  2. 63
      src/builder/DdPrismModelBuilder.cpp
  3. 7
      src/builder/ExplicitModelBuilder.cpp
  4. 6
      src/generator/JaniNextStateGenerator.cpp
  5. 2
      src/generator/JaniNextStateGenerator.h
  6. 18
      src/generator/NextStateGenerator.cpp
  7. 4
      src/generator/NextStateGenerator.h
  8. 19
      src/generator/PrismNextStateGenerator.cpp
  9. 2
      src/generator/PrismNextStateGenerator.h
  10. 3
      src/models/symbolic/Ctmc.cpp
  11. 2
      src/models/symbolic/Ctmc.h
  12. 3
      src/models/symbolic/DeterministicModel.cpp
  13. 2
      src/models/symbolic/DeterministicModel.h
  14. 3
      src/models/symbolic/Dtmc.cpp
  15. 2
      src/models/symbolic/Dtmc.h
  16. 3
      src/models/symbolic/Mdp.cpp
  17. 2
      src/models/symbolic/Mdp.h
  18. 23
      src/models/symbolic/Model.cpp
  19. 5
      src/models/symbolic/Model.h
  20. 3
      src/models/symbolic/NondeterministicModel.cpp
  21. 2
      src/models/symbolic/NondeterministicModel.h
  22. 3
      src/models/symbolic/StochasticTwoPlayerGame.cpp
  23. 2
      src/models/symbolic/StochasticTwoPlayerGame.h
  24. 2
      src/storage/sparse/StateStorage.cpp
  25. 3
      src/storage/sparse/StateStorage.h

32
src/builder/DdJaniModelBuilder.cpp
View File

@ -1585,6 +1585,7 @@ namespace storm {
struct ModelComponents {
storm::dd::Bdd<Type> reachableStates;
storm::dd::Bdd<Type> initialStates;
storm::dd::Bdd<Type> deadlockStates;
storm::dd::Add<Type, ValueType> transitionMatrix;
std::unordered_map<std::string, storm::models::symbolic::StandardRewardModel<Type, ValueType>> rewardModels;
};
@ -1592,11 +1593,11 @@ namespace storm {
template <storm::dd::DdType Type, typename ValueType>
std::shared_ptr<storm::models::symbolic::Model<Type, ValueType>> createModel(storm::jani::ModelType const& modelType, CompositionVariables<Type, ValueType> const& variables, ModelComponents<Type, ValueType> const& modelComponents) {
if (modelType == storm::jani::ModelType::DTMC) {
return std::shared_ptr<storm::models::symbolic::Model<Type, ValueType>>(new storm::models::symbolic::Dtmc<Type, ValueType>(variables.manager, modelComponents.reachableStates, modelComponents.initialStates, modelComponents.transitionMatrix, variables.rowMetaVariables, variables.rowExpressionAdapter, variables.columnMetaVariables, variables.columnExpressionAdapter, variables.rowColumnMetaVariablePairs, std::map<std::string, storm::expressions::Expression>(), modelComponents.rewardModels));
return std::shared_ptr<storm::models::symbolic::Model<Type, ValueType>>(new storm::models::symbolic::Dtmc<Type, ValueType>(variables.manager, modelComponents.reachableStates, modelComponents.initialStates, modelComponents.deadlockStates, modelComponents.transitionMatrix, variables.rowMetaVariables, variables.rowExpressionAdapter, variables.columnMetaVariables, variables.columnExpressionAdapter, variables.rowColumnMetaVariablePairs, std::map<std::string, storm::expressions::Expression>(), modelComponents.rewardModels));
} else if (modelType == storm::jani::ModelType::CTMC) {
return std::shared_ptr<storm::models::symbolic::Model<Type, ValueType>>(new storm::models::symbolic::Ctmc<Type, ValueType>(variables.manager, modelComponents.reachableStates, modelComponents.initialStates, modelComponents.transitionMatrix, variables.rowMetaVariables, variables.rowExpressionAdapter, variables.columnMetaVariables, variables.columnExpressionAdapter, variables.rowColumnMetaVariablePairs, std::map<std::string, storm::expressions::Expression>(), modelComponents.rewardModels));
return std::shared_ptr<storm::models::symbolic::Model<Type, ValueType>>(new storm::models::symbolic::Ctmc<Type, ValueType>(variables.manager, modelComponents.reachableStates, modelComponents.initialStates, modelComponents.deadlockStates, modelComponents.transitionMatrix, variables.rowMetaVariables, variables.rowExpressionAdapter, variables.columnMetaVariables, variables.columnExpressionAdapter, variables.rowColumnMetaVariablePairs, std::map<std::string, storm::expressions::Expression>(), modelComponents.rewardModels));
} else if (modelType == storm::jani::ModelType::MDP) {
return std::shared_ptr<storm::models::symbolic::Model<Type, ValueType>>(new storm::models::symbolic::Mdp<Type, ValueType>(variables.manager, modelComponents.reachableStates, modelComponents.initialStates, modelComponents.transitionMatrix, variables.rowMetaVariables, variables.rowExpressionAdapter, variables.columnMetaVariables, variables.columnExpressionAdapter, variables.rowColumnMetaVariablePairs, variables.allNondeterminismVariables, std::map<std::string, storm::expressions::Expression>(), modelComponents.rewardModels));
return std::shared_ptr<storm::models::symbolic::Model<Type, ValueType>>(new storm::models::symbolic::Mdp<Type, ValueType>(variables.manager, modelComponents.reachableStates, modelComponents.initialStates, modelComponents.deadlockStates, modelComponents.transitionMatrix, variables.rowMetaVariables, variables.rowExpressionAdapter, variables.columnMetaVariables, variables.columnExpressionAdapter, variables.rowColumnMetaVariablePairs, variables.allNondeterminismVariables, std::map<std::string, storm::expressions::Expression>(), modelComponents.rewardModels));
} else {
STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Invalid model type.");
}
@ -1624,7 +1625,7 @@ namespace storm {
}
template <storm::dd::DdType Type, typename ValueType>
void postprocessSystem(storm::jani::Model const& model, ComposerResult<Type, ValueType>& system, CompositionVariables<Type, ValueType> const& variables, typename DdJaniModelBuilder<Type, ValueType>::Options const& options) {
storm::dd::Bdd<Type> postprocessSystem(storm::jani::Model const& model, ComposerResult<Type, ValueType>& system, CompositionVariables<Type, ValueType> const& variables, typename DdJaniModelBuilder<Type, ValueType>::Options const& options) {
// For DTMCs, we normalize each row to 1 (to account for non-determinism).
if (model.getModelType() == storm::jani::ModelType::DTMC) {
system.transitions = system.transitions / system.transitions.sumAbstract(variables.columnMetaVariables);
@ -1647,7 +1648,9 @@ namespace storm {
}
system.transitions *= (!terminalStatesBdd).template toAdd<ValueType>();
return terminalStatesBdd;
}
return variables.manager->getBddZero();
}
template <storm::dd::DdType Type, typename ValueType>
@ -1667,18 +1670,19 @@ namespace storm {
}
template <storm::dd::DdType Type, typename ValueType>
void fixDeadlocks(storm::jani::ModelType const& modelType, storm::dd::Add<Type, ValueType>& transitionMatrix, storm::dd::Bdd<Type> const& transitionMatrixBdd, storm::dd::Bdd<Type> const& reachableStates, CompositionVariables<Type, ValueType> const& variables) {
storm::dd::Bdd<Type> fixDeadlocks(storm::jani::ModelType const& modelType, storm::dd::Add<Type, ValueType>& transitionMatrix, storm::dd::Bdd<Type> const& transitionMatrixBdd, storm::dd::Bdd<Type> const& reachableStates, CompositionVariables<Type, ValueType> const& variables) {
// Detect deadlocks and 1) fix them if requested 2) throw an error otherwise.
storm::dd::Bdd<Type> statesWithTransition = transitionMatrixBdd.existsAbstract(variables.columnMetaVariables);
storm::dd::Add<Type, ValueType> deadlockStates = (reachableStates && !statesWithTransition).template toAdd<ValueType>();
storm::dd::Bdd<Type> deadlockStates = reachableStates && !statesWithTransition;
if (!deadlockStates.isZero()) {
// If we need to fix deadlocks, we do so now.
if (!storm::settings::getModule<storm::settings::modules::MarkovChainSettings>().isDontFixDeadlocksSet()) {
STORM_LOG_INFO("Fixing deadlocks in " << deadlockStates.getNonZeroCount() << " states. The first three of these states are: ");
storm::dd::Add<Type, ValueType> deadlockStatesAdd = deadlockStates.template toAdd<ValueType>();
uint_fast64_t count = 0;
for (auto it = deadlockStates.begin(), ite = deadlockStates.end(); it != ite && count < 3; ++it, ++count) {
for (auto it = deadlockStatesAdd.begin(), ite = deadlockStatesAdd.end(); it != ite && count < 3; ++it, ++count) {
STORM_LOG_INFO((*it).first.toPrettyString(variables.rowMetaVariables) << std::endl);
}
@ -1693,7 +1697,7 @@ namespace storm {
if (modelType == storm::jani::ModelType::DTMC || modelType == storm::jani::ModelType::CTMC) {
// For DTMCs, we can simply add the identity of the global module for all deadlock states.
transitionMatrix += deadlockStates * globalIdentity;
transitionMatrix += deadlockStatesAdd * globalIdentity;
} else if (modelType == storm::jani::ModelType::MDP) {
// For MDPs, however, we need to select an action associated with the self-loop, if we do not
// want to attach a lot of self-loops to the deadlock states.
@ -1704,12 +1708,13 @@ namespace storm {
for (auto const& variable : variables.localNondeterminismVariables) {
action *= variables.manager->template getIdentity<ValueType>(variable);
}
transitionMatrix += deadlockStates * globalIdentity * action;
transitionMatrix += deadlockStatesAdd * globalIdentity * action;
}
} else {
STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The model contains " << deadlockStates.getNonZeroCount() << " deadlock states. Please unset the option to not fix deadlocks, if you want to fix them automatically.");
}
}
return deadlockStates;
}
template <storm::dd::DdType Type, typename ValueType>
@ -1726,8 +1731,8 @@ namespace storm {
// Postprocess the variables in place.
postprocessVariables(this->model->getModelType(), system, variables);
// Postprocess the system in place.
postprocessSystem(*this->model, system, variables, options);
// Postprocess the system in place and get the states that were terminal (i.e. whose transitions were cut off).
storm::dd::Bdd<Type> terminalStates = postprocessSystem(*this->model, system, variables, options);
// Start creating the model components.
ModelComponents<Type, ValueType> modelComponents;
@ -1751,7 +1756,10 @@ namespace storm {
modelComponents.transitionMatrix = system.transitions * reachableStatesAdd;
// Fix deadlocks if existing.
fixDeadlocks(this->model->getModelType(), modelComponents.transitionMatrix, transitionMatrixBdd, modelComponents.reachableStates, variables);
modelComponents.deadlockStates = fixDeadlocks(this->model->getModelType(), modelComponents.transitionMatrix, transitionMatrixBdd, modelComponents.reachableStates, variables);
// Cut the deadlock states by removing all states that we 'converted' to deadlock states by making them terminal.
modelComponents.deadlockStates = modelComponents.deadlockStates && !terminalStates;
// Finally, create the model.
return createModel(this->model->getModelType(), variables, modelComponents);

63
src/builder/DdPrismModelBuilder.cpp
View File

@ -1265,39 +1265,51 @@ namespace storm {
storm::dd::Add<Type, ValueType> stateActionDd = system.stateActionDd;
// If we were asked to treat some states as terminal states, we cut away their transitions now.
storm::dd::Bdd<Type> terminalStatesBdd = generationInfo.manager->getBddZero();
if (options.terminalStates || options.negatedTerminalStates) {
std::map<storm::expressions::Variable, storm::expressions::Expression> constantsSubstitution = preparedProgram->getConstantsSubstitution();
storm::dd::Bdd<Type> terminalStatesBdd = generationInfo.manager->getBddZero();
if (options.terminalStates) {
storm::expressions::Expression terminalExpression;
if (options.terminalStates.get().type() == typeid(storm::expressions::Expression)) {
terminalExpression = boost::get<storm::expressions::Expression>(options.terminalStates.get());
} else {
std::string const& labelName = boost::get<std::string>(options.terminalStates.get());
terminalExpression = preparedProgram->getLabelExpression(labelName);
}
// If the expression refers to constants of the model, we need to substitute them.
terminalExpression = terminalExpression.substitute(constantsSubstitution);
if (program.hasLabel(labelName)) {
terminalExpression = preparedProgram->getLabelExpression(labelName);
} else {
STORM_LOG_THROW(labelName == "init" || labelName == "deadlock", storm::exceptions::InvalidArgumentException, "Terminal states refer to illegal label '" << labelName << "'.");
}
}
STORM_LOG_TRACE("Making the states satisfying " << terminalExpression << " terminal.");
terminalStatesBdd = generationInfo.rowExpressionAdapter->translateExpression(terminalExpression).toBdd();
if (terminalExpression.isInitialized()) {
// If the expression refers to constants of the model, we need to substitute them.
terminalExpression = terminalExpression.substitute(constantsSubstitution);
STORM_LOG_TRACE("Making the states satisfying " << terminalExpression << " terminal.");
terminalStatesBdd = generationInfo.rowExpressionAdapter->translateExpression(terminalExpression).toBdd();
}
}
if (options.negatedTerminalStates) {
storm::expressions::Expression negatedTerminalExpression;
if (options.negatedTerminalStates.get().type() == typeid(storm::expressions::Expression)) {
negatedTerminalExpression = boost::get<storm::expressions::Expression>(options.negatedTerminalStates.get());
} else {
std::string const& labelName = boost::get<std::string>(options.terminalStates.get());
negatedTerminalExpression = preparedProgram->getLabelExpression(labelName);
std::string const& labelName = boost::get<std::string>(options.negatedTerminalStates.get());
if (program.hasLabel(labelName)) {
negatedTerminalExpression = preparedProgram->getLabelExpression(labelName);
} else {
STORM_LOG_THROW(labelName == "init" || labelName == "deadlock", storm::exceptions::InvalidArgumentException, "Terminal states refer to illegal label '" << labelName << "'.");
}
}
// If the expression refers to constants of the model, we need to substitute them.
negatedTerminalExpression = negatedTerminalExpression.substitute(constantsSubstitution);
STORM_LOG_TRACE("Making the states *not* satisfying " << negatedTerminalExpression << " terminal.");
terminalStatesBdd |= !generationInfo.rowExpressionAdapter->translateExpression(negatedTerminalExpression).toBdd();
if (negatedTerminalExpression.isInitialized()) {
// If the expression refers to constants of the model, we need to substitute them.
negatedTerminalExpression = negatedTerminalExpression.substitute(constantsSubstitution);
STORM_LOG_TRACE("Making the states *not* satisfying " << negatedTerminalExpression << " terminal.");
terminalStatesBdd |= !generationInfo.rowExpressionAdapter->translateExpression(negatedTerminalExpression).toBdd();
}
}
transitionMatrix *= (!terminalStatesBdd).template toAdd<ValueType>();
@ -1318,15 +1330,17 @@ namespace storm {
// Detect deadlocks and 1) fix them if requested 2) throw an error otherwise.
storm::dd::Bdd<Type> statesWithTransition = transitionMatrixBdd.existsAbstract(generationInfo.columnMetaVariables);
storm::dd::Add<Type, ValueType> deadlockStates = (reachableStates && !statesWithTransition).template toAdd<ValueType>();
storm::dd::Bdd<Type> deadlockStates = reachableStates && !statesWithTransition;
// If there are deadlocks, either fix them or raise an error.
if (!deadlockStates.isZero()) {
// If we need to fix deadlocks, we do so now.
if (!storm::settings::getModule<storm::settings::modules::MarkovChainSettings>().isDontFixDeadlocksSet()) {
STORM_LOG_INFO("Fixing deadlocks in " << deadlockStates.getNonZeroCount() << " states. The first three of these states are: ");
storm::dd::Add<Type, ValueType> deadlockStatesAdd = deadlockStates.template toAdd<ValueType>();
uint_fast64_t count = 0;
for (auto it = deadlockStates.begin(), ite = deadlockStates.end(); it != ite && count < 3; ++it, ++count) {
for (auto it = deadlockStatesAdd.begin(), ite = deadlockStatesAdd.end(); it != ite && count < 3; ++it, ++count) {
STORM_LOG_INFO((*it).first.toPrettyString(generationInfo.rowMetaVariables) << std::endl);
}
@ -1339,7 +1353,7 @@ namespace storm {
}
// For DTMCs, we can simply add the identity of the global module for all deadlock states.
transitionMatrix += deadlockStates * identity;
transitionMatrix += deadlockStatesAdd * identity;
} else if (program.getModelType() == storm::prism::Program::ModelType::MDP) {
// For MDPs, however, we need to select an action associated with the self-loop, if we do not
// want to attach a lot of self-loops to the deadlock states.
@ -1351,13 +1365,16 @@ namespace storm {
for (auto const& var : generationInfo.allGlobalVariables) {
action *= generationInfo.variableToIdentityMap.at(var);
}
transitionMatrix += deadlockStates * globalModule.identity * action;
transitionMatrix += deadlockStatesAdd * globalModule.identity * action;
}
} else {
STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The model contains " << deadlockStates.getNonZeroCount() << " deadlock states. Please unset the option to not fix deadlocks, if you want to fix them automatically.");
}
}
// Reduce the deadlock states by the states that we did simply not explore.
deadlockStates = deadlockStates && !terminalStatesBdd;
// Now build the reward models.
std::vector<std::reference_wrapper<storm::prism::RewardModel const>> selectedRewardModels;
@ -1389,11 +1406,11 @@ namespace storm {
}
if (program.getModelType() == storm::prism::Program::ModelType::DTMC) {
return std::shared_ptr<storm::models::symbolic::Model<Type>>(new storm::models::symbolic::Dtmc<Type>(generationInfo.manager, reachableStates, initialStates, transitionMatrix, generationInfo.rowMetaVariables, generationInfo.rowExpressionAdapter, generationInfo.columnMetaVariables, generationInfo.columnExpressionAdapter, generationInfo.rowColumnMetaVariablePairs, labelToExpressionMapping, rewardModels));
return std::shared_ptr<storm::models::symbolic::Model<Type>>(new storm::models::symbolic::Dtmc<Type>(generationInfo.manager, reachableStates, initialStates, deadlockStates, transitionMatrix, generationInfo.rowMetaVariables, generationInfo.rowExpressionAdapter, generationInfo.columnMetaVariables, generationInfo.columnExpressionAdapter, generationInfo.rowColumnMetaVariablePairs, labelToExpressionMapping, rewardModels));
} else if (program.getModelType() == storm::prism::Program::ModelType::CTMC) {
return std::shared_ptr<storm::models::symbolic::Model<Type>>(new storm::models::symbolic::Ctmc<Type>(generationInfo.manager, reachableStates, initialStates, transitionMatrix, generationInfo.rowMetaVariables, generationInfo.rowExpressionAdapter, generationInfo.columnMetaVariables, generationInfo.columnExpressionAdapter, generationInfo.rowColumnMetaVariablePairs, labelToExpressionMapping, rewardModels));
return std::shared_ptr<storm::models::symbolic::Model<Type>>(new storm::models::symbolic::Ctmc<Type>(generationInfo.manager, reachableStates, initialStates, deadlockStates, transitionMatrix, generationInfo.rowMetaVariables, generationInfo.rowExpressionAdapter, generationInfo.columnMetaVariables, generationInfo.columnExpressionAdapter, generationInfo.rowColumnMetaVariablePairs, labelToExpressionMapping, rewardModels));
} else if (program.getModelType() == storm::prism::Program::ModelType::MDP) {
return std::shared_ptr<storm::models::symbolic::Model<Type>>(new storm::models::symbolic::Mdp<Type>(generationInfo.manager, reachableStates, initialStates, transitionMatrix, generationInfo.rowMetaVariables, generationInfo.rowExpressionAdapter, generationInfo.columnMetaVariables, generationInfo.columnExpressionAdapter, generationInfo.rowColumnMetaVariablePairs, generationInfo.allNondeterminismVariables, labelToExpressionMapping, rewardModels));
return std::shared_ptr<storm::models::symbolic::Model<Type>>(new storm::models::symbolic::Mdp<Type>(generationInfo.manager, reachableStates, initialStates, deadlockStates, transitionMatrix, generationInfo.rowMetaVariables, generationInfo.rowExpressionAdapter, generationInfo.columnMetaVariables, generationInfo.columnExpressionAdapter, generationInfo.rowColumnMetaVariablePairs, generationInfo.allNondeterminismVariables, labelToExpressionMapping, rewardModels));
} else {
STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Invalid model type.");
}

7
src/builder/ExplicitModelBuilder.cpp
View File

@ -210,6 +210,11 @@ namespace storm {
// If there is no behavior, we might have to introduce a self-loop.
if (behavior.empty()) {
if (!storm::settings::getModule<storm::settings::modules::MarkovChainSettings>().isDontFixDeadlocksSet() || !behavior.wasExpanded()) {
// If the behavior was actually expanded and yet there are no transitions, then we have a deadlock state.
if (behavior.wasExpanded()) {
this->stateStorage.deadlockStateIndices.push_back(currentIndex);
}
if (generator->getOptions().isBuildChoiceLabelsSet()) {
// Insert empty choice labeling for added self-loop transitions.
choiceLabels.get().push_back(boost::container::flat_set<uint_fast64_t>());
@ -342,7 +347,7 @@ namespace storm {
template <typename ValueType, typename RewardModelType, typename StateType>
storm::models::sparse::StateLabeling ExplicitModelBuilder<ValueType, RewardModelType, StateType>::buildStateLabeling() {
return generator->label(stateStorage.stateToId, stateStorage.initialStateIndices);
return generator->label(stateStorage.stateToId, stateStorage.initialStateIndices, stateStorage.deadlockStateIndices);
}
// Explicitly instantiate the class.

6
src/generator/JaniNextStateGenerator.cpp
View File

@ -32,7 +32,7 @@ namespace storm {
if (expressionOrLabelAndBool.first.isExpression()) {
this->terminalStates.push_back(std::make_pair(expressionOrLabelAndBool.first.getExpression(), expressionOrLabelAndBool.second));
} else {
STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Cannot make label terminal for JANI models.");
STORM_LOG_THROW(expressionOrLabelAndBool.first.getLabel() == "init" || expressionOrLabelAndBool.first.getLabel() == "deadlock", storm::exceptions::InvalidSettingsException, "Terminal states refer to illegal label '" << expressionOrLabelAndBool.first.getLabel() << "'.");
}
}
}
@ -487,8 +487,8 @@ namespace storm {
}
template<typename ValueType, typename StateType>
storm::models::sparse::StateLabeling JaniNextStateGenerator<ValueType, StateType>::label(storm::storage::BitVectorHashMap<StateType> const& states, std::vector<StateType> const& initialStateIndices) {
return NextStateGenerator<ValueType, StateType>::label(states, initialStateIndices, {});
storm::models::sparse::StateLabeling JaniNextStateGenerator<ValueType, StateType>::label(storm::storage::BitVectorHashMap<StateType> const& states, std::vector<StateType> const& initialStateIndices, std::vector<StateType> const& deadlockStateIndices) {
return NextStateGenerator<ValueType, StateType>::label(states, initialStateIndices, deadlockStateIndices, {});
}
template class JaniNextStateGenerator<double>;

2
src/generator/JaniNextStateGenerator.h
View File

@ -24,7 +24,7 @@ namespace storm {
virtual std::size_t getNumberOfRewardModels() const override;
virtual RewardModelInformation getRewardModelInformation(uint64_t const& index) const override;
virtual storm::models::sparse::StateLabeling label(storm::storage::BitVectorHashMap<StateType> const& states, std::vector<StateType> const& initialStateIndices = {}) override;
virtual storm::models::sparse::StateLabeling label(storm::storage::BitVectorHashMap<StateType> const& states, std::vector<StateType> const& initialStateIndices = {}, std::vector<StateType> const& deadlockStateIndices = {}) override;
private:
/*!

18
src/generator/NextStateGenerator.cpp
View File

@ -244,7 +244,7 @@ namespace storm {
}
template<typename ValueType, typename StateType>
storm::models::sparse::StateLabeling NextStateGenerator<ValueType, StateType>::label(storm::storage::BitVectorHashMap<StateType> const& states, std::vector<StateType> const& initialStateIndices, std::vector<std::pair<std::string, storm::expressions::Expression>> labelsAndExpressions) {
storm::models::sparse::StateLabeling NextStateGenerator<ValueType, StateType>::label(storm::storage::BitVectorHashMap<StateType> const& states, std::vector<StateType> const& initialStateIndices, std::vector<StateType> const& deadlockStateIndices, std::vector<std::pair<std::string, storm::expressions::Expression>> labelsAndExpressions) {
// Make the labels unique.
std::sort(labelsAndExpressions.begin(), labelsAndExpressions.end(), [] (std::pair<std::string, storm::expressions::Expression> const& a, std::pair<std::string, storm::expressions::Expression> const& b) { return a.first < b.first; } );
auto it = std::unique(labelsAndExpressions.begin(), labelsAndExpressions.end(), [] (std::pair<std::string, storm::expressions::Expression> const& a, std::pair<std::string, storm::expressions::Expression> const& b) { return a.first == b.first; } );
@ -274,10 +274,18 @@ namespace storm {
}
}
// Also label the initial state with the special label "init".
result.addLabel("init");
for (auto index : initialStateIndices) {
result.addLabelToState("init", index);
if (!result.containsLabel("init")) {
// Also label the initial state with the special label "init".
result.addLabel("init");
for (auto index : initialStateIndices) {
result.addLabelToState("init", index);
}
}
if (!result.containsLabel("deadlock")) {
result.addLabel("deadlock");
for (auto index : deadlockStateIndices) {
result.addLabelToState("deadlock", index);
}
}
return result;

4
src/generator/NextStateGenerator.h
View File

@ -177,7 +177,7 @@ namespace storm {
storm::expressions::SimpleValuation toValuation(CompressedState const& state) const;
virtual storm::models::sparse::StateLabeling label(storm::storage::BitVectorHashMap<StateType> const& states, std::vector<StateType> const& initialStateIndices = {}) = 0;
virtual storm::models::sparse::StateLabeling label(storm::storage::BitVectorHashMap<StateType> const& states, std::vector<StateType> const& initialStateIndices = {}, std::vector<StateType> const& deadlockStateIndices = {}) = 0;
NextStateGeneratorOptions const& getOptions() const;
@ -185,7 +185,7 @@ namespace storm {
/*!
* Creates the state labeling for the given states using the provided labels and expressions.
*/
storm::models::sparse::StateLabeling label(storm::storage::BitVectorHashMap<StateType> const& states, std::vector<StateType> const& initialStateIndices, std::vector<std::pair<std::string, storm::expressions::Expression>> labelsAndExpressions);
storm::models::sparse::StateLabeling label(storm::storage::BitVectorHashMap<StateType> const& states, std::vector<StateType> const& initialStateIndices, std::vector<StateType> const& deadlockStateIndices, std::vector<std::pair<std::string, storm::expressions::Expression>> labelsAndExpressions);
/// The options to be used for next-state generation.
NextStateGeneratorOptions options;

19
src/generator/PrismNextStateGenerator.cpp
View File

@ -59,7 +59,12 @@ namespace storm {
if (expressionOrLabelAndBool.first.isExpression()) {
this->terminalStates.push_back(std::make_pair(expressionOrLabelAndBool.first.getExpression(), expressionOrLabelAndBool.second));
} else {
this->terminalStates.push_back(std::make_pair(this->program.getLabelExpression(expressionOrLabelAndBool.first.getLabel()), expressionOrLabelAndBool.second));
if (program.hasLabel(expressionOrLabelAndBool.first.getLabel())) {
this->terminalStates.push_back(std::make_pair(this->program.getLabelExpression(expressionOrLabelAndBool.first.getLabel()), expressionOrLabelAndBool.second));
} else {
// If the label is not present in the program and is not a special one, we raise an error.
STORM_LOG_THROW(expressionOrLabelAndBool.first.getLabel() == "init" || expressionOrLabelAndBool.first.getLabel() == "deadlock", storm::exceptions::InvalidArgumentException, "Terminal states refer to illegal label '" << expressionOrLabelAndBool.first.getLabel() << "'.");
}
}
}
}
@ -162,6 +167,7 @@ namespace storm {
}
// Get all choices for the state.
result.setExpanded();
std::vector<Choice<ValueType>> allChoices = getUnlabeledChoices(*this->state, stateToIdCallback);
std::vector<Choice<ValueType>> allLabeledChoices = getLabeledChoices(*this->state, stateToIdCallback);
for (auto& choice : allLabeledChoices) {
@ -229,7 +235,6 @@ namespace storm {
result.addChoice(std::move(choice));
}
result.setExpanded();
return result;
}
@ -498,7 +503,7 @@ namespace storm {
}
template<typename ValueType, typename StateType>
storm::models::sparse::StateLabeling PrismNextStateGenerator<ValueType, StateType>::label(storm::storage::BitVectorHashMap<StateType> const& states, std::vector<StateType> const& initialStateIndices) {
storm::models::sparse::StateLabeling PrismNextStateGenerator<ValueType, StateType>::label(storm::storage::BitVectorHashMap<StateType> const& states, std::vector<StateType> const& initialStateIndices, std::vector<StateType> const& deadlockStateIndices) {
// Gather a vector of labels and their expressions.
std::vector<std::pair<std::string, storm::expressions::Expression>> labels;
if (this->options.isBuildAllLabelsSet()) {
@ -507,11 +512,15 @@ namespace storm {
}
} else {
for (auto const& labelName : this->options.getLabelNames()) {
labels.push_back(std::make_pair(labelName, program.getLabelExpression(labelName)));
if (program.hasLabel(labelName)) {
labels.push_back(std::make_pair(labelName, program.getLabelExpression(labelName)));
} else {
STORM_LOG_THROW(labelName == "init" || labelName == "deadlock", storm::exceptions::InvalidArgumentException, "Cannot build labeling for unknown label '" << labelName << "'.");
}
}
}
return NextStateGenerator<ValueType, StateType>::label(states, initialStateIndices, labels);
return NextStateGenerator<ValueType, StateType>::label(states, initialStateIndices, deadlockStateIndices, labels);
}
template<typename ValueType, typename StateType>

2
src/generator/PrismNextStateGenerator.h
View File

@ -25,7 +25,7 @@ namespace storm {
virtual std::size_t getNumberOfRewardModels() const override;
virtual RewardModelInformation getRewardModelInformation(uint64_t const& index) const override;
virtual storm::models::sparse::StateLabeling label(storm::storage::BitVectorHashMap<StateType> const& states, std::vector<StateType> const& initialStateIndices = {}) override;
virtual storm::models::sparse::StateLabeling label(storm::storage::BitVectorHashMap<StateType> const& states, std::vector<StateType> const& initialStateIndices = {}, std::vector<StateType> const& deadlockStateIndices = {}) override;
private:
/*!

3
src/models/symbolic/Ctmc.cpp
View File

@ -14,6 +14,7 @@ namespace storm {
Ctmc<Type, ValueType>::Ctmc(std::shared_ptr<storm::dd::DdManager<Type>> manager,
storm::dd::Bdd<Type> reachableStates,
storm::dd::Bdd<Type> initialStates,
storm::dd::Bdd<Type> deadlockStates,
storm::dd::Add<Type, ValueType> transitionMatrix,
std::set<storm::expressions::Variable> const& rowVariables,
std::shared_ptr<storm::adapters::AddExpressionAdapter<Type, ValueType>> rowExpressionAdapter,
@ -22,7 +23,7 @@ namespace storm {
std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& rowColumnMetaVariablePairs,
std::map<std::string, storm::expressions::Expression> labelToExpressionMap,
std::unordered_map<std::string, RewardModelType> const& rewardModels)
: DeterministicModel<Type>(storm::models::ModelType::Ctmc, manager, reachableStates, initialStates, transitionMatrix, rowVariables, rowExpressionAdapter, columnVariables, columnExpressionAdapter, rowColumnMetaVariablePairs, labelToExpressionMap, rewardModels) {
: DeterministicModel<Type>(storm::models::ModelType::Ctmc, manager, reachableStates, initialStates, deadlockStates, transitionMatrix, rowVariables, rowExpressionAdapter, columnVariables, columnExpressionAdapter, rowColumnMetaVariablePairs, labelToExpressionMap, rewardModels) {
exitRates = this->getTransitionMatrix().sumAbstract(this->getColumnVariables());
}

2
src/models/symbolic/Ctmc.h
View File

@ -30,6 +30,7 @@ namespace storm {
* @param manager The manager responsible for the decision diagrams.
* @param reachableStates A DD representing the reachable states.
* @param initialStates A DD representing the initial states of the model.
* @param deadlockStates A DD representing the deadlock states of the model.
* @param transitionMatrix The matrix representing the transitions in the model.
* @param rowVariables The set of row meta variables used in the DDs.
* @param rowExpressionAdapter An object that can be used to translate expressions in terms of the row
@ -44,6 +45,7 @@ namespace storm {
Ctmc(std::shared_ptr<storm::dd::DdManager<Type>> manager,
storm::dd::Bdd<Type> reachableStates,
storm::dd::Bdd<Type> initialStates,
storm::dd::Bdd<Type> deadlockStates,
storm::dd::Add<Type, ValueType> transitionMatrix,
std::set<storm::expressions::Variable> const& rowVariables,
std::shared_ptr<storm::adapters::AddExpressionAdapter<Type, ValueType>> rowExpressionAdapter,

3
src/models/symbolic/DeterministicModel.cpp
View File

@ -15,6 +15,7 @@ namespace storm {
std::shared_ptr<storm::dd::DdManager<Type>> manager,
storm::dd::Bdd<Type> reachableStates,
storm::dd::Bdd<Type> initialStates,
storm::dd::Bdd<Type> deadlockStates,
storm::dd::Add<Type, ValueType> transitionMatrix,
std::set<storm::expressions::Variable> const& rowVariables,
std::shared_ptr<storm::adapters::AddExpressionAdapter<Type, ValueType>> rowExpressionAdapter,
@ -23,7 +24,7 @@ namespace storm {
std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& rowColumnMetaVariablePairs,
std::map<std::string, storm::expressions::Expression> labelToExpressionMap,
std::unordered_map<std::string, RewardModelType> const& rewardModels)
: Model<Type>(modelType, manager, reachableStates, initialStates, transitionMatrix, rowVariables, rowExpressionAdapter, columnVariables, columnExpressionAdapter, rowColumnMetaVariablePairs, labelToExpressionMap, rewardModels) {
: Model<Type>(modelType, manager, reachableStates, initialStates, deadlockStates, transitionMatrix, rowVariables, rowExpressionAdapter, columnVariables, columnExpressionAdapter, rowColumnMetaVariablePairs, labelToExpressionMap, rewardModels) {
// Intentionally left empty.
}

2
src/models/symbolic/DeterministicModel.h
View File

@ -31,6 +31,7 @@ namespace storm {
* @param manager The manager responsible for the decision diagrams.
* @param reachableStates A DD representing the reachable states.
* @param initialStates A DD representing the initial states of the model.
* @param deadlockStates A DD representing the deadlock states of the model.
* @param transitionMatrix The matrix representing the transitions in the model.
* @param rowVariables The set of row meta variables used in the DDs.
* @param rowExpressionAdapter An object that can be used to translate expressions in terms of the row
@ -46,6 +47,7 @@ namespace storm {
std::shared_ptr<storm::dd::DdManager<Type>> manager,
storm::dd::Bdd<Type> reachableStates,
storm::dd::Bdd<Type> initialStates,
storm::dd::Bdd<Type> deadlockStates,
storm::dd::Add<Type, ValueType> transitionMatrix,
std::set<storm::expressions::Variable> const& rowVariables,
std::shared_ptr<storm::adapters::AddExpressionAdapter<Type, ValueType>> rowExpressionAdapter,

3
src/models/symbolic/Dtmc.cpp
View File

@ -14,6 +14,7 @@ namespace storm {
Dtmc<Type, ValueType>::Dtmc(std::shared_ptr<storm::dd::DdManager<Type>> manager,
storm::dd::Bdd<Type> reachableStates,
storm::dd::Bdd<Type> initialStates,
storm::dd::Bdd<Type> deadlockStates,
storm::dd::Add<Type, ValueType> transitionMatrix,
std::set<storm::expressions::Variable> const& rowVariables,
std::shared_ptr<storm::adapters::AddExpressionAdapter<Type, ValueType>> rowExpressionAdapter,
@ -22,7 +23,7 @@ namespace storm {
std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& rowColumnMetaVariablePairs,
std::map<std::string, storm::expressions::Expression> labelToExpressionMap,
std::unordered_map<std::string, RewardModelType> const& rewardModels)
: DeterministicModel<Type, ValueType>(storm::models::ModelType::Dtmc, manager, reachableStates, initialStates, transitionMatrix, rowVariables, rowExpressionAdapter, columnVariables, columnExpressionAdapter, rowColumnMetaVariablePairs, labelToExpressionMap, rewardModels) {
: DeterministicModel<Type, ValueType>(storm::models::ModelType::Dtmc, manager, reachableStates, initialStates, deadlockStates, transitionMatrix, rowVariables, rowExpressionAdapter, columnVariables, columnExpressionAdapter, rowColumnMetaVariablePairs, labelToExpressionMap, rewardModels) {
// Intentionally left empty.
}

2
src/models/symbolic/Dtmc.h
View File

@ -30,6 +30,7 @@ namespace storm {
* @param manager The manager responsible for the decision diagrams.
* @param reachableStates A DD representing the reachable states.
* @param initialStates A DD representing the initial states of the model.
* @param deadlockStates A DD representing the deadlock states of the model.
* @param transitionMatrix The matrix representing the transitions in the model.
* @param rowVariables The set of row meta variables used in the DDs.
* @param rowExpressionAdapter An object that can be used to translate expressions in terms of the row
@ -44,6 +45,7 @@ namespace storm {
Dtmc(std::shared_ptr<storm::dd::DdManager<Type>> manager,
storm::dd::Bdd<Type> reachableStates,
storm::dd::Bdd<Type> initialStates,
storm::dd::Bdd<Type> deadlockStates,
storm::dd::Add<Type, ValueType> transitionMatrix,
std::set<storm::expressions::Variable> const& rowVariables,
std::shared_ptr<storm::adapters::AddExpressionAdapter<Type, ValueType>> rowExpressionAdapter,

3
src/models/symbolic/Mdp.cpp
View File

@ -14,6 +14,7 @@ namespace storm {
Mdp<Type, ValueType>::Mdp(std::shared_ptr<storm::dd::DdManager<Type>> manager,
storm::dd::Bdd<Type> reachableStates,
storm::dd::Bdd<Type> initialStates,
storm::dd::Bdd<Type> deadlockStates,
storm::dd::Add<Type, ValueType> transitionMatrix,
std::set<storm::expressions::Variable> const& rowVariables,
std::shared_ptr<storm::adapters::AddExpressionAdapter<Type, ValueType>> rowExpressionAdapter,
@ -23,7 +24,7 @@ namespace storm {
std::set<storm::expressions::Variable> const& nondeterminismVariables,
std::map<std::string, storm::expressions::Expression> labelToExpressionMap,
std::unordered_map<std::string, RewardModelType> const& rewardModels)
: NondeterministicModel<Type, ValueType>(storm::models::ModelType::Mdp, manager, reachableStates, initialStates, transitionMatrix, rowVariables, rowExpressionAdapter, columnVariables, columnExpressionAdapter, rowColumnMetaVariablePairs, nondeterminismVariables, labelToExpressionMap, rewardModels) {
: NondeterministicModel<Type, ValueType>(storm::models::ModelType::Mdp, manager, reachableStates, initialStates, deadlockStates, transitionMatrix, rowVariables, rowExpressionAdapter, columnVariables, columnExpressionAdapter, rowColumnMetaVariablePairs, nondeterminismVariables, labelToExpressionMap, rewardModels) {
// Intentionally left empty.
}

2
src/models/symbolic/Mdp.h
View File

@ -31,6 +31,7 @@ namespace storm {
* @param manager The manager responsible for the decision diagrams.
* @param reachableStates A DD representing the reachable states.
* @param initialStates A DD representing the initial states of the model.
* @param deadlockStates A DD representing the deadlock states of the model.
* @param transitionMatrix The matrix representing the transitions in the model.
* @param rowVariables The set of row meta variables used in the DDs.
* @param rowExpressionAdapter An object that can be used to translate expressions in terms of the row
@ -46,6 +47,7 @@ namespace storm {
Mdp(std::shared_ptr<storm::dd::DdManager<Type>> manager,
storm::dd::Bdd<Type> reachableStates,
storm::dd::Bdd<Type> initialStates,
storm::dd::Bdd<Type> deadlockStates,
storm::dd::Add<Type, ValueType> transitionMatrix,
std::set<storm::expressions::Variable> const& rowVariables,
std::shared_ptr<storm::adapters::AddExpressionAdapter<Type, ValueType>> rowExpressionAdapter,

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

@ -21,6 +21,7 @@ namespace storm {
std::shared_ptr<storm::dd::DdManager<Type>> manager,
storm::dd::Bdd<Type> reachableStates,
storm::dd::Bdd<Type> initialStates,
storm::dd::Bdd<Type> deadlockStates,
storm::dd::Add<Type, ValueType> transitionMatrix,
std::set<storm::expressions::Variable> const& rowVariables,
std::shared_ptr<storm::adapters::AddExpressionAdapter<Type, ValueType>> rowExpressionAdapter,
@ -29,7 +30,7 @@ namespace storm {
std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& rowColumnMetaVariablePairs,
std::map<std::string, storm::expressions::Expression> labelToExpressionMap,
std::unordered_map<std::string, RewardModelType> const& rewardModels)
: ModelBase(modelType), manager(manager), reachableStates(reachableStates), initialStates(initialStates), transitionMatrix(transitionMatrix), rowVariables(rowVariables), rowExpressionAdapter(rowExpressionAdapter), columnVariables(columnVariables), columnExpressionAdapter(columnExpressionAdapter), rowColumnMetaVariablePairs(rowColumnMetaVariablePairs), labelToExpressionMap(labelToExpressionMap), rewardModels(rewardModels) {
: ModelBase(modelType), manager(manager), reachableStates(reachableStates), initialStates(initialStates), deadlockStates(deadlockStates), transitionMatrix(transitionMatrix), rowVariables(rowVariables), rowExpressionAdapter(rowExpressionAdapter), columnVariables(columnVariables), columnExpressionAdapter(columnExpressionAdapter), rowColumnMetaVariablePairs(rowColumnMetaVariablePairs), labelToExpressionMap(labelToExpressionMap), rewardModels(rewardModels) {
// Intentionally left empty.
}
@ -65,8 +66,17 @@ namespace storm {
template<storm::dd::DdType Type, typename ValueType>
storm::dd::Bdd<Type> Model<Type, ValueType>::getStates(std::string const& label) const {
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;
auto labelIt = labelToExpressionMap.find(label);
if (labelIt != labelToExpressionMap.end()) {
return rowExpressionAdapter->translateExpression(labelIt->second).toBdd() && this->reachableStates;
} else {
if (label == "init") {
return initialStates;
} else if (label == "deadlock") {
return deadlockStates;
}
}
STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentException, "The label " << label << " is invalid for the labeling of the model.");
}
template<storm::dd::DdType Type, typename ValueType>
@ -76,7 +86,12 @@ namespace storm {
template<storm::dd::DdType Type, typename ValueType>
bool Model<Type, ValueType>::hasLabel(std::string const& label) const {
return labelToExpressionMap.find(label) != labelToExpressionMap.end();
auto labelIt = labelToExpressionMap.find(label);
if (labelIt != labelToExpressionMap.end()) {
return true;
} else {
return label == "init" || label == "deadlock";
}
}
template<storm::dd::DdType Type, typename ValueType>

5
src/models/symbolic/Model.h
View File

@ -66,6 +66,7 @@ namespace storm {
* @param manager The manager responsible for the decision diagrams.
* @param reachableStates A DD representing the reachable states.
* @param initialStates A DD representing the initial states of the model.
* @param deadlockStates A DD representing the deadlock states of the model.
* @param transitionMatrix The matrix representing the transitions in the model.
* @param rowVariables The set of row meta variables used in the DDs.
* @param rowExpressionAdapter An object that can be used to translate expressions in terms of the row
@ -81,6 +82,7 @@ namespace storm {
std::shared_ptr<storm::dd::DdManager<Type>> manager,
storm::dd::Bdd<Type> reachableStates,
storm::dd::Bdd<Type> initialStates,
storm::dd::Bdd<Type> deadlockStates,
storm::dd::Add<Type, ValueType> transitionMatrix,
std::set<storm::expressions::Variable> const& rowVariables,
std::shared_ptr<storm::adapters::AddExpressionAdapter<Type, ValueType>> rowExpressionAdapter,
@ -291,6 +293,9 @@ namespace storm {
// A vector representing the initial states of the model.
storm::dd::Bdd<Type> initialStates;
// A vector representing the deadlock states of the model.
storm::dd::Bdd<Type> deadlockStates;
// A matrix representing transition relation.
storm::dd::Add<Type, ValueType> transitionMatrix;

3
src/models/symbolic/NondeterministicModel.cpp
View File

@ -15,6 +15,7 @@ namespace storm {
std::shared_ptr<storm::dd::DdManager<Type>> manager,
storm::dd::Bdd<Type> reachableStates,
storm::dd::Bdd<Type> initialStates,
storm::dd::Bdd<Type> deadlockStates,
storm::dd::Add<Type, ValueType> transitionMatrix,
std::set<storm::expressions::Variable> const& rowVariables,
std::shared_ptr<storm::adapters::AddExpressionAdapter<Type, ValueType>> rowExpressionAdapter,
@ -24,7 +25,7 @@ namespace storm {
std::set<storm::expressions::Variable> const& nondeterminismVariables,
std::map<std::string, storm::expressions::Expression> labelToExpressionMap,
std::unordered_map<std::string, RewardModelType> const& rewardModels)
: Model<Type>(modelType, manager, reachableStates, initialStates, transitionMatrix, rowVariables, rowExpressionAdapter, columnVariables, columnExpressionAdapter, rowColumnMetaVariablePairs, labelToExpressionMap, rewardModels), nondeterminismVariables(nondeterminismVariables) {
: Model<Type>(modelType, manager, reachableStates, initialStates, deadlockStates, transitionMatrix, rowVariables, rowExpressionAdapter, columnVariables, columnExpressionAdapter, rowColumnMetaVariablePairs, labelToExpressionMap, rewardModels), nondeterminismVariables(nondeterminismVariables) {
// Prepare the mask of illegal nondeterministic choices.
illegalMask = transitionMatrix.notZero().existsAbstract(this->getColumnVariables());

2
src/models/symbolic/NondeterministicModel.h
View File

@ -31,6 +31,7 @@ namespace storm {
* @param manager The manager responsible for the decision diagrams.
* @param reachableStates A DD representing the reachable states.
* @param initialStates A DD representing the initial states of the model.
* @param deadlockStates A DD representing the deadlock states of the model.
* @param transitionMatrix The matrix representing the transitions in the model.
* @param rowVariables The set of row meta variables used in the DDs.
* @param rowExpressionAdapter An object that can be used to translate expressions in terms of the row
@ -47,6 +48,7 @@ namespace storm {
std::shared_ptr<storm::dd::DdManager<Type>> manager,
storm::dd::Bdd<Type> reachableStates,
storm::dd::Bdd<Type> initialStates,
storm::dd::Bdd<Type> deadlockStates,
storm::dd::Add<Type, ValueType> transitionMatrix,
std::set<storm::expressions::Variable> const& rowVariables,
std::shared_ptr<storm::adapters::AddExpressionAdapter<Type, ValueType>> rowExpressionAdapter,

3
src/models/symbolic/StochasticTwoPlayerGame.cpp
View File

@ -14,6 +14,7 @@ namespace storm {
StochasticTwoPlayerGame<Type, ValueType>::StochasticTwoPlayerGame(std::shared_ptr<storm::dd::DdManager<Type>> manager,
storm::dd::Bdd<Type> reachableStates,
storm::dd::Bdd<Type> initialStates,
storm::dd::Bdd<Type> deadlockStates,
storm::dd::Add<Type, ValueType> transitionMatrix,
std::set<storm::expressions::Variable> const& rowVariables,
std::shared_ptr<storm::adapters::AddExpressionAdapter<Type, ValueType>> rowExpressionAdapter,
@ -25,7 +26,7 @@ namespace storm {
std::set<storm::expressions::Variable> const& nondeterminismVariables,
std::map<std::string, storm::expressions::Expression> labelToExpressionMap,
std::unordered_map<std::string, RewardModelType> const& rewardModels)
: NondeterministicModel<Type>(storm::models::ModelType::S2pg, manager, reachableStates, initialStates, transitionMatrix, rowVariables, rowExpressionAdapter, columnVariables, columnExpressionAdapter, rowColumnMetaVariablePairs, nondeterminismVariables, labelToExpressionMap, rewardModels), player1Variables(player1Variables), player2Variables(player2Variables) {
: NondeterministicModel<Type>(storm::models::ModelType::S2pg, manager, reachableStates, initialStates, deadlockStates, transitionMatrix, rowVariables, rowExpressionAdapter, columnVariables, columnExpressionAdapter, rowColumnMetaVariablePairs, nondeterminismVariables, labelToExpressionMap, rewardModels), player1Variables(player1Variables), player2Variables(player2Variables) {
// Intentionally left empty.
}

2
src/models/symbolic/StochasticTwoPlayerGame.h
View File

@ -30,6 +30,7 @@ namespace storm {
* @param manager The manager responsible for the decision diagrams.
* @param reachableStates A DD representing the reachable states.
* @param initialStates A DD representing the initial states of the model.
* @param deadlockStates A DD representing the deadlock states of the model.
* @param transitionMatrix The matrix representing the transitions in the model.
* @param rowVariables The set of row meta variables used in the DDs.
* @param rowExpressionAdapter An object that can be used to translate expressions in terms of the row
@ -47,6 +48,7 @@ namespace storm {
StochasticTwoPlayerGame(std::shared_ptr<storm::dd::DdManager<Type>> manager,
storm::dd::Bdd<Type> reachableStates,
storm::dd::Bdd<Type> initialStates,
storm::dd::Bdd<Type> deadlockStates,
storm::dd::Add<Type, ValueType> transitionMatrix,
std::set<storm::expressions::Variable> const& rowVariables,
std::shared_ptr<storm::adapters::AddExpressionAdapter<Type, ValueType>> rowExpressionAdapter,

2
src/storage/sparse/StateStorage.cpp
View File

@ -5,7 +5,7 @@ namespace storm {
namespace sparse {
template <typename StateType>
StateStorage<StateType>::StateStorage(uint64_t bitsPerState) : stateToId(bitsPerState, 10000000), initialStateIndices(), bitsPerState(bitsPerState) {
StateStorage<StateType>::StateStorage(uint64_t bitsPerState) : stateToId(bitsPerState, 10000000), initialStateIndices(), deadlockStateIndices(), bitsPerState(bitsPerState) {
// Intentionally left empty.
}

3
src/storage/sparse/StateStorage.h
View File

@ -21,6 +21,9 @@ namespace storm {
// A list of initial states in terms of their global indices.
std::vector<StateType> initialStateIndices;
// A list of deadlock states.
std::vector<StateType> deadlockStateIndices;
// The number of bits of each state.
uint64_t bitsPerState;

Write Preview
Loading…
Cancel
Save