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

tearing apart explicit model builder and 'next-state generation' 

Former-commit-id: 2ccda8d931
main
dehnert 9 years ago
parent
7ce969b312
commit
8a0bd32b55
14 changed files with 607 additions and 537 deletions
Split View
  1. 4
      src/CMakeLists.txt
  2. 369
      src/builder/ExplicitPrismModelBuilder.cpp
  3. 98
      src/builder/ExplicitPrismModelBuilder.h
  4. 4
      src/generator/Choice.cpp
  5. 4
      src/generator/Choice.h
  6. 8
      src/generator/NextStateGenerator.h
  7. 249
      src/generator/PrismNextStateGenerator.cpp
  8. 90
      src/generator/PrismNextStateGenerator.h
  9. 42
      src/generator/VariableInformation.cpp
  10. 71
      src/generator/VariableInformation.h
  11. 44
      src/generator/prism/VariableInformation.cpp
  12. 73
      src/generator/prism/VariableInformation.h
  13. 4
      src/storage/prism/Program.cpp
  14. 12
      src/storage/prism/Program.h

4
src/CMakeLists.txt
View File

@ -11,8 +11,7 @@ file(GLOB_RECURSE STORM_SOURCES_CLI ${PROJECT_SOURCE_DIR}/src/cli/*.cpp)
file(GLOB_RECURSE STORM_MAIN_FILE ${PROJECT_SOURCE_DIR}/src/storm.cpp)
file(GLOB_RECURSE STORM_ADAPTERS_FILES ${PROJECT_SOURCE_DIR}/src/adapters/*.h ${PROJECT_SOURCE_DIR}/src/adapters/*.cpp)
file(GLOB_RECURSE STORM_BUILDER_FILES ${PROJECT_SOURCE_DIR}/src/builder/*.h ${PROJECT_SOURCE_DIR}/src/builder/*.cpp)
file(GLOB STORM_GENERATOR_FILES ${PROJECT_SOURCE_DIR}/src/generator/*.h ${PROJECT_SOURCE_DIR}/src/generator/*.cpp)
file(GLOB_RECURSE STORM_GENERATOR_PRISM_FILES ${PROJECT_SOURCE_DIR}/src/generator/prism/*.h ${PROJECT_SOURCE_DIR}/src/generator/prism/*.cpp)
file(GLOB_RECURSE STORM_GENERATOR_FILES ${PROJECT_SOURCE_DIR}/src/generator/*.h ${PROJECT_SOURCE_DIR}/src/generator/*.cpp)
file(GLOB_RECURSE STORM_CLI_FILES ${PROJECT_SOURCE_DIR}/src/cli/*.h ${PROJECT_SOURCE_DIR}/src/cli/*.cpp)
file(GLOB_RECURSE STORM_EXCEPTIONS_FILES ${PROJECT_SOURCE_DIR}/src/exceptions/*.h ${PROJECT_SOURCE_DIR}/src/exceptions/*.cpp)
file(GLOB_RECURSE STORM_LOGIC_FILES ${PROJECT_SOURCE_DIR}/src/logic/*.h ${PROJECT_SOURCE_DIR}/src/logic/*.cpp)
@ -60,7 +59,6 @@ source_group(main FILES ${STORM_MAIN_FILE})
source_group(adapters FILES ${STORM_ADAPTERS_FILES})
source_group(builder FILES ${STORM_BUILDER_FILES})
source_group(generator FILES ${STORM_GENERATOR_FILES})
source_group(generator\\prism FILES ${STORM_GENERATOR_PRISM_FILES})
source_group(cli FILES ${STORM_CLI_FILES})
source_group(exceptions FILES ${STORM_EXCEPTIONS_FILES})
source_group(logic FILES ${STORM_LOGIC_FILES})

369
src/builder/ExplicitPrismModelBuilder.cpp
View File

@ -66,33 +66,33 @@ namespace storm {
storm::storage::SparseMatrixBuilder<ValueType> transitionRewardMatrixBuilder;
};
template <typename ValueType, typename RewardModelType, typename IndexType>
ExplicitPrismModelBuilder<ValueType, RewardModelType, IndexType>::StateInformation::StateInformation(uint_fast64_t numberOfStates) : valuations(numberOfStates) {
template <typename ValueType, typename RewardModelType, typename StateType>
ExplicitPrismModelBuilder<ValueType, RewardModelType, StateType>::StateInformation::StateInformation(uint_fast64_t numberOfStates) : valuations(numberOfStates) {
// Intentionally left empty.
}
template <typename ValueType, typename RewardModelType, typename IndexType>
ExplicitPrismModelBuilder<ValueType, RewardModelType, IndexType>::InternalStateInformation::InternalStateInformation(uint64_t bitsPerState) : stateStorage(bitsPerState, 10000000), bitsPerState(bitsPerState), reachableStates() {
template <typename ValueType, typename RewardModelType, typename StateType>
ExplicitPrismModelBuilder<ValueType, RewardModelType, StateType>::InternalStateInformation::InternalStateInformation(uint64_t bitsPerState) : stateStorage(bitsPerState, 10000000), bitsPerState(bitsPerState), numberOfStates() {
// Intentionally left empty.
}
template <typename ValueType, typename RewardModelType, typename IndexType>
ExplicitPrismModelBuilder<ValueType, RewardModelType, IndexType>::ModelComponents::ModelComponents() : transitionMatrix(), stateLabeling(), rewardModels(), choiceLabeling() {
template <typename ValueType, typename RewardModelType, typename StateType>
ExplicitPrismModelBuilder<ValueType, RewardModelType, StateType>::ModelComponents::ModelComponents() : transitionMatrix(), stateLabeling(), rewardModels(), choiceLabeling() {
// Intentionally left empty.
}
template <typename ValueType, typename RewardModelType, typename IndexType>
ExplicitPrismModelBuilder<ValueType, RewardModelType, IndexType>::Options::Options() : buildCommandLabels(false), buildAllRewardModels(true), buildStateInformation(false), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(true), labelsToBuild(), expressionLabels(), terminalStates(), negatedTerminalStates() {
template <typename ValueType, typename RewardModelType, typename StateType>
ExplicitPrismModelBuilder<ValueType, RewardModelType, StateType>::Options::Options() : buildCommandLabels(false), buildAllRewardModels(true), buildStateInformation(false), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(true), labelsToBuild(), expressionLabels(), terminalStates(), negatedTerminalStates() {
// Intentionally left empty.
}
template <typename ValueType, typename RewardModelType, typename IndexType>
ExplicitPrismModelBuilder<ValueType, RewardModelType, IndexType>::Options::Options(storm::logic::Formula const& formula) : buildCommandLabels(false), buildAllRewardModels(false), buildStateInformation(false), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(false), labelsToBuild(std::set<std::string>()), expressionLabels(std::vector<storm::expressions::Expression>()), terminalStates(), negatedTerminalStates() {
template <typename ValueType, typename RewardModelType, typename StateType>
ExplicitPrismModelBuilder<ValueType, RewardModelType, StateType>::Options::Options(storm::logic::Formula const& formula) : buildCommandLabels(false), buildAllRewardModels(false), buildStateInformation(false), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(false), labelsToBuild(std::set<std::string>()), expressionLabels(std::vector<storm::expressions::Expression>()), terminalStates(), negatedTerminalStates() {
this->preserveFormula(formula);
}
template <typename ValueType, typename RewardModelType, typename IndexType>
ExplicitPrismModelBuilder<ValueType, RewardModelType, IndexType>::Options::Options(std::vector<std::shared_ptr<const storm::logic::Formula>> const& formulas) : buildCommandLabels(false), buildAllRewardModels(false), buildStateInformation(false), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(false), labelsToBuild(), expressionLabels(), terminalStates(), negatedTerminalStates() {
template <typename ValueType, typename RewardModelType, typename StateType>
ExplicitPrismModelBuilder<ValueType, RewardModelType, StateType>::Options::Options(std::vector<std::shared_ptr<const storm::logic::Formula>> const& formulas) : buildCommandLabels(false), buildAllRewardModels(false), buildStateInformation(false), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(false), labelsToBuild(), expressionLabels(), terminalStates(), negatedTerminalStates() {
if (formulas.empty()) {
this->buildAllRewardModels = true;
this->buildAllLabels = true;
@ -106,8 +106,8 @@ namespace storm {
}
}
template <typename ValueType, typename RewardModelType, typename IndexType>
void ExplicitPrismModelBuilder<ValueType, RewardModelType, IndexType>::Options::setTerminalStatesFromFormula(storm::logic::Formula const& formula) {
template <typename ValueType, typename RewardModelType, typename StateType>
void ExplicitPrismModelBuilder<ValueType, RewardModelType, StateType>::Options::setTerminalStatesFromFormula(storm::logic::Formula const& formula) {
if (formula.isAtomicExpressionFormula()) {
terminalStates = formula.asAtomicExpressionFormula().getExpression();
} else if (formula.isAtomicLabelFormula()) {
@ -136,8 +136,8 @@ namespace storm {
}
}
template <typename ValueType, typename RewardModelType, typename IndexType>
void ExplicitPrismModelBuilder<ValueType, RewardModelType, IndexType>::Options::preserveFormula(storm::logic::Formula const& formula) {
template <typename ValueType, typename RewardModelType, typename StateType>
void ExplicitPrismModelBuilder<ValueType, RewardModelType, StateType>::Options::preserveFormula(storm::logic::Formula const& formula) {
// If we already had terminal states, we need to erase them.
if (terminalStates) {
terminalStates.reset();
@ -174,40 +174,29 @@ namespace storm {
}
}
template <typename ValueType, typename RewardModelType, typename IndexType>
void ExplicitPrismModelBuilder<ValueType, RewardModelType, IndexType>::Options::addConstantDefinitionsFromString(storm::prism::Program const& program, std::string const& constantDefinitionString) {
template <typename ValueType, typename RewardModelType, typename StateType>
void ExplicitPrismModelBuilder<ValueType, RewardModelType, StateType>::Options::addConstantDefinitionsFromString(storm::prism::Program const& program, std::string const& constantDefinitionString) {
constantDefinitions = storm::utility::prism::parseConstantDefinitionString(program, constantDefinitionString);
}
template <typename ValueType, typename RewardModelType, typename IndexType>
typename ExplicitPrismModelBuilder<ValueType, RewardModelType, IndexType>::StateInformation const& ExplicitPrismModelBuilder<ValueType, RewardModelType, IndexType>::getStateInformation() const {
STORM_LOG_THROW(static_cast<bool>(stateInformation), storm::exceptions::InvalidOperationException, "The state information was not properly build.");
return stateInformation.get();
}
template <typename ValueType, typename RewardModelType, typename IndexType>
storm::prism::Program const& ExplicitPrismModelBuilder<ValueType, RewardModelType, IndexType>::getTranslatedProgram() const {
return preparedProgram.get();
}
template <typename ValueType, typename RewardModelType, typename IndexType>
std::shared_ptr<storm::models::sparse::Model<ValueType, RewardModelType>> ExplicitPrismModelBuilder<ValueType, RewardModelType, IndexType>::translateProgram(storm::prism::Program program, Options const& options) {
template <typename ValueType, typename RewardModelType, typename StateType>
ExplicitPrismModelBuilder<ValueType, RewardModelType, StateType>::ExplicitPrismModelBuilder(storm::prism::Program const& program, Options const& options) : options(options), program(program) {
// Start by defining the undefined constants in the model.
if (options.constantDefinitions) {
preparedProgram = program.defineUndefinedConstants(options.constantDefinitions.get());
this->program = program.defineUndefinedConstants(options.constantDefinitions.get());
} else {
preparedProgram = program;
this->program = program;
}
// If the program still contains undefined constants and we are not in a parametric setting, assemble an appropriate error message.
#ifdef STORM_HAVE_CARL
// If the program either has undefined constants or we are building a parametric model, but the parameters
// not only appear in the probabilities, we re
if (!std::is_same<ValueType, storm::RationalFunction>::value && preparedProgram->hasUndefinedConstants()) {
if (!std::is_same<ValueType, storm::RationalFunction>::value && this->program.hasUndefinedConstants()) {
#else
if (preparedProgram->hasUndefinedConstants()) {
if (this->program->hasUndefinedConstants()) {
#endif
std::vector<std::reference_wrapper<storm::prism::Constant const>> undefinedConstants = preparedProgram->getUndefinedConstants();
std::vector<std::reference_wrapper<storm::prism::Constant const>> undefinedConstants = this->program.getUndefinedConstants();
std::stringstream stream;
bool printComma = false;
for (auto const& constant : undefinedConstants) {
@ -221,7 +210,7 @@ namespace storm {
stream << ".";
STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Program still contains these undefined constants: " + stream.str());
#ifdef STORM_HAVE_CARL
} else if (std::is_same<ValueType, storm::RationalFunction>::value && !preparedProgram->hasUndefinedConstantsOnlyInUpdateProbabilitiesAndRewards()) {
} else if (std::is_same<ValueType, storm::RationalFunction>::value && !this->program.hasUndefinedConstantsOnlyInUpdateProbabilitiesAndRewards()) {
STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The program contains undefined constants that appear in some places other than update probabilities and reward value expressions, which is not admitted.");
#endif
}
@ -229,50 +218,64 @@ 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());
this->program.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.
if (options.expressionLabels) {
std::map<storm::expressions::Variable, storm::expressions::Expression> constantsSubstitution = preparedProgram->getConstantsSubstitution();
std::map<storm::expressions::Variable, storm::expressions::Expression> constantsSubstitution = this->program.getConstantsSubstitution();
for (auto const& expression : options.expressionLabels.get()) {
std::stringstream stream;
stream << expression.substitute(constantsSubstitution);
std::string name = stream.str();
if (!preparedProgram->hasLabel(name)) {
preparedProgram->addLabel(name, expression);
if (!this->program.hasLabel(name)) {
this->program.addLabel(name, expression);
}
}
}
// Now that the program is fixed, we we need to substitute all constants with their concrete value.
preparedProgram = preparedProgram->substituteConstants();
this->program = program.substituteConstants();
}
STORM_LOG_DEBUG("Building representation of program:" << std::endl << *preparedProgram << std::endl);
template <typename ValueType, typename RewardModelType, typename StateType>
typename ExplicitPrismModelBuilder<ValueType, RewardModelType, StateType>::StateInformation const& ExplicitPrismModelBuilder<ValueType, RewardModelType, StateType>::getStateInformation() const {
STORM_LOG_THROW(static_cast<bool>(stateInformation), storm::exceptions::InvalidOperationException, "The state information was not properly build.");
return stateInformation.get();
}
template <typename ValueType, typename RewardModelType, typename StateType>
storm::prism::Program const& ExplicitPrismModelBuilder<ValueType, RewardModelType, StateType>::getTranslatedProgram() const {
return program;
}
template <typename ValueType, typename RewardModelType, typename StateType>
std::shared_ptr<storm::models::sparse::Model<ValueType, RewardModelType>> ExplicitPrismModelBuilder<ValueType, RewardModelType, StateType>::translate() {
STORM_LOG_DEBUG("Building representation of program:" << std::endl << *program << 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 << "'.");
STORM_LOG_THROW(rewardModelName.empty() || program.hasRewardModel(rewardModelName), storm::exceptions::InvalidArgumentException, "Model does not possess a reward model with the name '" << rewardModelName << "'.");
}
for (auto const& rewardModel : preparedProgram->getRewardModels()) {
for (auto const& rewardModel : program.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));
if (selectedRewardModels.empty() && program.getNumberOfRewardModels() == 1 && options.rewardModelsToBuild.size() == 1 && *options.rewardModelsToBuild.begin() == "") {
selectedRewardModels.push_back(program.getRewardModel(0));
}
ModelComponents modelComponents = buildModelComponents(*preparedProgram, selectedRewardModels, options);
ModelComponents modelComponents = buildModelComponents(*program, selectedRewardModels, options);
std::shared_ptr<storm::models::sparse::Model<ValueType, RewardModelType>> result;
switch (program.getModelType()) {
@ -293,18 +296,8 @@ namespace storm {
return result;
}
template <typename ValueType, typename RewardModelType, typename IndexType>
void ExplicitPrismModelBuilder<ValueType, RewardModelType, IndexType>::unpackStateIntoEvaluator(storm::storage::BitVector const& currentState, VariableInformation const& variableInformation, storm::expressions::ExpressionEvaluator<ValueType>& evaluator) {
for (auto const& booleanVariable : variableInformation.booleanVariables) {
evaluator.setBooleanValue(booleanVariable.variable, currentState.get(booleanVariable.bitOffset));
}
for (auto const& integerVariable : variableInformation.integerVariables) {
evaluator.setIntegerValue(integerVariable.variable, currentState.getAsInt(integerVariable.bitOffset, integerVariable.bitWidth) + integerVariable.lowerBound);
}
}
template <typename ValueType, typename RewardModelType, typename IndexType>
storm::expressions::SimpleValuation ExplicitPrismModelBuilder<ValueType, RewardModelType, IndexType>::unpackStateIntoValuation(storm::storage::BitVector const& currentState, VariableInformation const& variableInformation) {
template <typename ValueType, typename RewardModelType, typename StateType>
storm::expressions::SimpleValuation ExplicitPrismModelBuilder<ValueType, RewardModelType, StateType>::unpackStateIntoValuation(storm::storage::BitVector const& currentState) {
storm::expressions::SimpleValuation result(variableInformation.manager.getSharedPointer());
for (auto const& booleanVariable : variableInformation.booleanVariables) {
result.setBooleanValue(booleanVariable.variable, currentState.get(booleanVariable.bitOffset));
@ -315,254 +308,26 @@ namespace storm {
return result;
}
template <typename ValueType, typename RewardModelType, typename IndexType>
typename ExplicitPrismModelBuilder<ValueType, RewardModelType, IndexType>::CompressedState ExplicitPrismModelBuilder<ValueType, RewardModelType, IndexType>::applyUpdate(VariableInformation const& variableInformation, CompressedState const& state, storm::prism::Update const& update, storm::expressions::ExpressionEvaluator<ValueType> const& evaluator) {
return applyUpdate(variableInformation, state, state, update, evaluator);
}
template <typename ValueType, typename RewardModelType, typename IndexType>
typename ExplicitPrismModelBuilder<ValueType, RewardModelType, IndexType>::CompressedState ExplicitPrismModelBuilder<ValueType, RewardModelType, IndexType>::applyUpdate(VariableInformation const& variableInformation, CompressedState const& state, CompressedState const& baseState, storm::prism::Update const& update, storm::expressions::ExpressionEvaluator<ValueType> const& evaluator) {
CompressedState newState(state);
auto assignmentIt = update.getAssignments().begin();
auto assignmentIte = update.getAssignments().end();
// Iterate over all boolean assignments and carry them out.
auto boolIt = variableInformation.booleanVariables.begin();
for (; assignmentIt != assignmentIte && assignmentIt->getExpression().hasBooleanType(); ++assignmentIt) {
while (assignmentIt->getVariable() != boolIt->variable) {
++boolIt;
}
newState.set(boolIt->bitOffset, evaluator.asBool(assignmentIt->getExpression()));
}
// Iterate over all integer assignments and carry them out.
auto integerIt = variableInformation.integerVariables.begin();
for (; assignmentIt != assignmentIte && assignmentIt->getExpression().hasIntegerType(); ++assignmentIt) {
while (assignmentIt->getVariable() != integerIt->variable) {
++integerIt;
}
int_fast64_t assignedValue = evaluator.asInt(assignmentIt->getExpression());
STORM_LOG_THROW(assignedValue <= integerIt->upperBound, storm::exceptions::WrongFormatException, "The update " << update << " leads to an out-of-bounds value (" << assignedValue << ") for the variable '" << assignmentIt->getVariableName() << "'.");
newState.setFromInt(integerIt->bitOffset, integerIt->bitWidth, assignedValue - integerIt->lowerBound);
STORM_LOG_ASSERT(static_cast<int_fast64_t>(newState.getAsInt(integerIt->bitOffset, integerIt->bitWidth)) + integerIt->lowerBound == assignedValue, "Writing to the bit vector bucket failed (read " << newState.getAsInt(integerIt->bitOffset, integerIt->bitWidth) << " but wrote " << assignedValue << ").");
}
// Check that we processed all assignments.
STORM_LOG_ASSERT(assignmentIt == assignmentIte, "Not all assignments were consumed.");
return newState;
}
template <typename ValueType, typename RewardModelType, typename IndexType>
IndexType ExplicitPrismModelBuilder<ValueType, RewardModelType, IndexType>::getOrAddStateIndex(CompressedState const& state, InternalStateInformation& internalStateInformation, std::queue<storm::storage::BitVector>& stateQueue) {
template <typename ValueType, typename RewardModelType, typename StateType>
StateType ExplicitPrismModelBuilder<ValueType, RewardModelType, StateType>::getOrAddStateIndex(CompressedState const& state) {
uint32_t newIndex = internalStateInformation.reachableStates.size();
// Check, if the state was already registered.
std::pair<uint32_t, std::size_t> actualIndexBucketPair = internalStateInformation.stateStorage.findOrAddAndGetBucket(state, newIndex);
if (actualIndexBucketPair.first == newIndex) {
stateQueue.push(state);
internalStateInformation.reachableStates.push_back(state);
statesToExplore.push(state);
++internalStateInformation.numberOfStates;
}
return actualIndexBucketPair.first;
}
template <typename ValueType, typename RewardModelType, typename IndexType>
boost::optional<std::vector<std::vector<std::reference_wrapper<storm::prism::Command const>>>> ExplicitPrismModelBuilder<ValueType, RewardModelType, IndexType>::getActiveCommandsByActionIndex(storm::prism::Program const& program,storm::expressions::ExpressionEvaluator<ValueType> const& evaluator, uint_fast64_t const& actionIndex) {
boost::optional<std::vector<std::vector<std::reference_wrapper<storm::prism::Command const>>>> result((std::vector<std::vector<std::reference_wrapper<storm::prism::Command const>>>()));
// Iterate over all modules.
for (uint_fast64_t i = 0; i < program.getNumberOfModules(); ++i) {
storm::prism::Module const& module = program.getModule(i);
// If the module has no command labeled with the given action, we can skip this module.
if (!module.hasActionIndex(actionIndex)) {
continue;
}
std::set<uint_fast64_t> const& commandIndices = module.getCommandIndicesByActionIndex(actionIndex);
// If the module contains the action, but there is no command in the module that is labeled with
// this action, we don't have any feasible command combinations.
if (commandIndices.empty()) {
return boost::optional<std::vector<std::vector<std::reference_wrapper<storm::prism::Command const>>>>();
}
std::vector<std::reference_wrapper<storm::prism::Command const>> commands;
// Look up commands by their indices and add them if the guard evaluates to true in the given state.
for (uint_fast64_t commandIndex : commandIndices) {
storm::prism::Command const& command = module.getCommand(commandIndex);
if (evaluator.asBool(command.getGuardExpression())) {
commands.push_back(command);
}
}
// If there was no enabled command although the module has some command with the required action label,
// we must not return anything.
if (commands.size() == 0) {
return boost::optional<std::vector<std::vector<std::reference_wrapper<storm::prism::Command const>>>>();
}
result.get().push_back(std::move(commands));
}
return result;
}
template <typename ValueType, typename RewardModelType, typename IndexType>
std::vector<Choice<ValueType>> ExplicitPrismModelBuilder<ValueType, RewardModelType, IndexType>::getUnlabeledTransitions(storm::prism::Program const& program, bool discreteTimeModel, InternalStateInformation& internalStateInformation, VariableInformation const& variableInformation, storm::storage::BitVector const& currentState, bool choiceLabeling, storm::expressions::ExpressionEvaluator<ValueType> const& evaluator, std::queue<storm::storage::BitVector>& stateQueue, storm::utility::ConstantsComparator<ValueType> const& comparator) {
std::vector<Choice<ValueType>> result;
// Iterate over all modules.
for (uint_fast64_t i = 0; i < program.getNumberOfModules(); ++i) {
storm::prism::Module const& module = program.getModule(i);
// Iterate over all commands.
for (uint_fast64_t j = 0; j < module.getNumberOfCommands(); ++j) {
storm::prism::Command const& command = module.getCommand(j);
// Only consider unlabeled commands.
if (command.isLabeled()) continue;
// Skip the command, if it is not enabled.
if (!evaluator.asBool(command.getGuardExpression())) {
continue;
}
result.push_back(Choice<ValueType>(0, choiceLabeling));
Choice<ValueType>& choice = result.back();
// Remember the command labels only if we were asked to.
if (choiceLabeling) {
choice.addChoiceLabel(command.getGlobalIndex());
}
// Iterate over all updates of the current command.
ValueType probabilitySum = storm::utility::zero<ValueType>();
for (uint_fast64_t k = 0; k < command.getNumberOfUpdates(); ++k) {
storm::prism::Update const& update = command.getUpdate(k);
// Obtain target state index and add it to the list of known states. If it has not yet been
// seen, we also add it to the set of states that have yet to be explored.
uint32_t stateIndex = getOrAddStateIndex(applyUpdate(variableInformation, currentState, update, evaluator), internalStateInformation, stateQueue);
// Update the choice by adding the probability/target state to it.
ValueType probability = evaluator.asRational(update.getLikelihoodExpression());
choice.addProbability(stateIndex, probability);
probabilitySum += probability;
}
// Check that the resulting distribution is in fact a distribution.
STORM_LOG_THROW(!discreteTimeModel || comparator.isOne(probabilitySum), storm::exceptions::WrongFormatException, "Probabilities do not sum to one for command '" << command << "' (actually sum to " << probabilitySum << ").");
}
}
return result;
}
template <typename ValueType, typename RewardModelType, typename IndexType>
std::vector<Choice<ValueType>> ExplicitPrismModelBuilder<ValueType, RewardModelType, IndexType>::getLabeledTransitions(storm::prism::Program const& program, bool discreteTimeModel, InternalStateInformation& internalStateInformation, VariableInformation const& variableInformation, storm::storage::BitVector const& currentState, bool choiceLabeling, storm::expressions::ExpressionEvaluator<ValueType> const& evaluator, std::queue<storm::storage::BitVector>& stateQueue, storm::utility::ConstantsComparator<ValueType> const& comparator) {
std::vector<Choice<ValueType>> result;
for (uint_fast64_t actionIndex : program.getSynchronizingActionIndices()) {
boost::optional<std::vector<std::vector<std::reference_wrapper<storm::prism::Command const>>>> optionalActiveCommandLists = getActiveCommandsByActionIndex(program, evaluator, actionIndex);
// Only process this action label, if there is at least one feasible solution.
if (optionalActiveCommandLists) {
std::vector<std::vector<std::reference_wrapper<storm::prism::Command const>>> const& activeCommandList = optionalActiveCommandLists.get();
std::vector<std::vector<std::reference_wrapper<storm::prism::Command const>>::const_iterator> iteratorList(activeCommandList.size());
// Initialize the list of iterators.
for (size_t i = 0; i < activeCommandList.size(); ++i) {
iteratorList[i] = activeCommandList[i].cbegin();
}
// As long as there is one feasible combination of commands, keep on expanding it.
bool done = false;
while (!done) {
std::unordered_map<CompressedState, ValueType>* currentTargetStates = new std::unordered_map<CompressedState, ValueType>();
std::unordered_map<CompressedState, ValueType>* newTargetStates = new std::unordered_map<CompressedState, ValueType>();
currentTargetStates->emplace(currentState, storm::utility::one<ValueType>());
for (uint_fast64_t i = 0; i < iteratorList.size(); ++i) {
storm::prism::Command const& command = *iteratorList[i];
for (uint_fast64_t j = 0; j < command.getNumberOfUpdates(); ++j) {
storm::prism::Update const& update = command.getUpdate(j);
for (auto const& stateProbabilityPair : *currentTargetStates) {
// Compute the new state under the current update and add it to the set of new target states.
CompressedState newTargetState = applyUpdate(variableInformation, stateProbabilityPair.first, currentState, update, evaluator);
newTargetStates->emplace(newTargetState, stateProbabilityPair.second * evaluator.asRational(update.getLikelihoodExpression()));
}
}
// If there is one more command to come, shift the target states one time step back.
if (i < iteratorList.size() - 1) {
delete currentTargetStates;
currentTargetStates = newTargetStates;
newTargetStates = new std::unordered_map<CompressedState, ValueType>();
}
}
// At this point, we applied all commands of the current command combination and newTargetStates
// contains all target states and their respective probabilities. That means we are now ready to
// add the choice to the list of transitions.
result.push_back(Choice<ValueType>(actionIndex, choiceLabeling));
// Now create the actual distribution.
Choice<ValueType>& choice = result.back();
// Remember the command labels only if we were asked to.
if (choiceLabeling) {
// Add the labels of all commands to this choice.
for (uint_fast64_t i = 0; i < iteratorList.size(); ++i) {
choice.addChoiceLabel(iteratorList[i]->get().getGlobalIndex());
}
}
ValueType probabilitySum = storm::utility::zero<ValueType>();
for (auto const& stateProbabilityPair : *newTargetStates) {
uint32_t actualIndex = getOrAddStateIndex(stateProbabilityPair.first, internalStateInformation, stateQueue);
choice.addProbability(actualIndex, stateProbabilityPair.second);
probabilitySum += stateProbabilityPair.second;
}
// Check that the resulting distribution is in fact a distribution.
STORM_LOG_THROW(!discreteTimeModel || !comparator.isConstant(probabilitySum) || comparator.isOne(probabilitySum), storm::exceptions::WrongFormatException, "Sum of update probabilities do not some to one for some command (actually sum to " << probabilitySum << ").");
// Dispose of the temporary maps.
delete currentTargetStates;
delete newTargetStates;
// Now, check whether there is one more command combination to consider.
bool movedIterator = false;
for (int_fast64_t j = iteratorList.size() - 1; j >= 0; --j) {
++iteratorList[j];
if (iteratorList[j] != activeCommandList[j].end()) {
movedIterator = true;
} else {
// Reset the iterator to the beginning of the list.
iteratorList[j] = activeCommandList[j].begin();
}
}
done = !movedIterator;
}
}
}
return result;
}
template <typename ValueType, typename RewardModelType, typename IndexType>
boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>> ExplicitPrismModelBuilder<ValueType, RewardModelType, IndexType>::buildMatrices(storm::prism::Program const& program, VariableInformation const& variableInformation, std::vector<std::reference_wrapper<storm::prism::RewardModel const>> const& selectedRewardModels, InternalStateInformation& internalStateInformation, bool commandLabels, bool deterministicModel, bool discreteTimeModel, storm::storage::SparseMatrixBuilder<ValueType>& transitionMatrixBuilder, std::vector<RewardModelBuilder<typename RewardModelType::ValueType>>& rewardModelBuilders, boost::optional<storm::expressions::Expression> const& terminalExpression) {
template <typename ValueType, typename RewardModelType, typename StateType>
boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>> ExplicitPrismModelBuilder<ValueType, RewardModelType, StateType>::buildMatrices(std::vector<std::reference_wrapper<storm::prism::RewardModel const>> const& selectedRewardModels, InternalStateInformation& internalStateInformation, storm::storage::SparseMatrixBuilder<ValueType>& transitionMatrixBuilder, std::vector<RewardModelBuilder<typename RewardModelType::ValueType>>& rewardModelBuilders, boost::optional<storm::expressions::Expression> const& terminalExpression) {
// Create choice labels, if requested,
boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>> choiceLabels;
if (commandLabels) {
if (options.buildCommandLabels) {
choiceLabels = std::vector<boost::container::flat_set<uint_fast64_t>>();
}
@ -606,7 +371,7 @@ namespace storm {
// Get the current state and unpack it.
storm::storage::BitVector currentState = stateQueue.front();
stateQueue.pop();
IndexType stateIndex = internalStateInformation.stateStorage.getValue(currentState);
StateType stateIndex = internalStateInformation.stateStorage.getValue(currentState);
STORM_LOG_TRACE("Exploring state with id " << stateIndex << ".");
unpackStateIntoEvaluator(currentState, variableInformation, evaluator);
@ -615,10 +380,6 @@ namespace storm {
std::vector<Choice<ValueType>> allLabeledChoices;
bool deadlockOnPurpose = false;
if (terminalExpression && evaluator.asBool(terminalExpression.get())) {
//std::cout << unpackStateIntoValuation(currentState, variableInformation).toString(true) << std::endl;
//allUnlabeledChoices = getUnlabeledTransitions(program, discreteTimeModel, internalStateInformation, variableInformation, currentState, commandLabels, evaluator, stateQueue, comparator);
//allLabeledChoices = getLabeledTransitions(program, discreteTimeModel, internalStateInformation, variableInformation, currentState, commandLabels, evaluator, stateQueue, comparator);
// Nothing to do in this case.
deadlockOnPurpose = true;
} else {
@ -886,8 +647,8 @@ namespace storm {
return choiceLabels;
}
template <typename ValueType, typename RewardModelType, typename IndexType>
typename ExplicitPrismModelBuilder<ValueType, RewardModelType, IndexType>::ModelComponents ExplicitPrismModelBuilder<ValueType, RewardModelType, IndexType>::buildModelComponents(storm::prism::Program const& program, std::vector<std::reference_wrapper<storm::prism::RewardModel const>> const& selectedRewardModels, Options const& options) {
template <typename ValueType, typename RewardModelType, typename StateType>
typename ExplicitPrismModelBuilder<ValueType, RewardModelType, StateType>::ModelComponents ExplicitPrismModelBuilder<ValueType, RewardModelType, StateType>::buildModelComponents(storm::prism::Program const& program, std::vector<std::reference_wrapper<storm::prism::RewardModel const>> const& selectedRewardModels, Options const& options) {
ModelComponents modelComponents;
uint_fast64_t bitOffset = 0;
@ -991,8 +752,8 @@ namespace storm {
return modelComponents;
}
template <typename ValueType, typename RewardModelType, typename IndexType>
storm::models::sparse::StateLabeling ExplicitPrismModelBuilder<ValueType, RewardModelType, IndexType>::buildStateLabeling(storm::prism::Program const& program, VariableInformation const& variableInformation, InternalStateInformation const& internalStateInformation) {
template <typename ValueType, typename RewardModelType, typename StateType>
storm::models::sparse::StateLabeling ExplicitPrismModelBuilder<ValueType, RewardModelType, StateType>::buildStateLabeling(storm::prism::Program const& program, VariableInformation const& variableInformation, InternalStateInformation const& internalStateInformation) {
storm::expressions::ExpressionEvaluator<ValueType> evaluator(program.getManager());
std::vector<storm::prism::Label> const& labels = program.getLabels();

98
src/builder/ExplicitPrismModelBuilder.h
View File

@ -22,9 +22,11 @@
#include "src/storage/SparseMatrix.h"
#include "src/settings/SettingsManager.h"
#include "src/utility/constants.h"
#include "src/utility/prism.h"
#include "src/generator/VariableInformation.h"
namespace storm {
namespace utility {
template<typename ValueType> class ConstantsComparator;
@ -37,7 +39,7 @@ namespace storm {
// Forward-declare classes.
template <typename ValueType> struct RewardModelBuilder;
template<typename ValueType, typename RewardModelType = storm::models::sparse::StandardRewardModel<ValueType>, typename IndexType = uint32_t>
template<typename ValueType, typename RewardModelType = storm::models::sparse::StandardRewardModel<ValueType>, typename StateType = uint32_t>
class ExplicitPrismModelBuilder {
public:
typedef storm::storage::BitVector CompressedState;
@ -47,16 +49,16 @@ namespace storm {
InternalStateInformation(uint64_t bitsPerState);
// This member stores all the states and maps them to their unique indices.
storm::storage::BitVectorHashMap<IndexType> stateStorage;
storm::storage::BitVectorHashMap<StateType> stateStorage;
// A list of initial states in terms of their global indices.
std::vector<IndexType> initialStateIndices;
std::vector<StateType> initialStateIndices;
// The number of bits of each state.
uint64_t bitsPerState;
// A list of reachable states as indices in the stateToIndexMap.
std::vector<storm::storage::BitVector> reachableStates;
// The number of states that were found in the exploration so far.
uint_fast64_t numberOfStates;
};
// A structure holding information about the reachable state space that can be retrieved from the outside.
@ -174,6 +176,13 @@ namespace storm {
boost::optional<boost::variant<storm::expressions::Expression, std::string>> negatedTerminalStates;
};
/*!
* Creates a builder for the given program.
*
* @param program The program to build.
*/
ExplicitPrismModelBuilder(storm::prism::Program const& program, Options const& options = Options());
/*!
* Convert the program given at construction time to an abstract model. The type of the model is the one
* specified in the program. The given reward model name selects the rewards that the model will contain.
@ -184,7 +193,7 @@ namespace storm {
* @param rewardModel The reward model that is to be built.
* @return The explicit model that was given by the probabilistic program.
*/
std::shared_ptr<storm::models::sparse::Model<ValueType, RewardModelType>> translateProgram(storm::prism::Program program, Options const& options = Options());
std::shared_ptr<storm::models::sparse::Model<ValueType, RewardModelType>> translate();
/*!
* If requested in the options, information about the variable valuations in the reachable states can be
@ -195,39 +204,14 @@ namespace storm {
StateInformation const& getStateInformation() const;
/*!
* Retrieves the program that was actually translated (i.e. including constant substitutions etc.). Note
* that this function may only be called after a succesful translation.
* Retrieves the program that was actually translated (i.e. including constant substitutions etc.).
*
* @return The translated program.
*/
storm::prism::Program const& getTranslatedProgram() const;
private:
static void unpackStateIntoEvaluator(storm::storage::BitVector const& currentState, VariableInformation const& variableInformation, storm::expressions::ExpressionEvaluator<ValueType>& evaluator);
static storm::expressions::SimpleValuation unpackStateIntoValuation(storm::storage::BitVector const& currentState, VariableInformation const& variableInformation);
/*!
* Applies an update to the given state and returns the resulting new state object. This methods does not
* modify the given state but returns a new one.
*
* @params state The state to which to apply the update.
* @params update The update to apply.
* @return The resulting state.
*/
static CompressedState applyUpdate(VariableInformation const& variableInformation, CompressedState const& state, storm::prism::Update const& update, storm::expressions::ExpressionEvaluator<ValueType> const& evaluator);
/*!
* Applies an update to the given state and returns the resulting new state object. The update is evaluated
* over the variable values of the given base state. This methods does not modify the given state but
* returns a new one.
*
* @param state The state to which to apply the update.
* @param baseState The state used for evaluating the update.
* @param update The update to apply.
* @return The resulting state.
*/
static CompressedState applyUpdate(VariableInformation const& variableInformation, CompressedState const& state, CompressedState const& baseState, storm::prism::Update const& update, storm::expressions::ExpressionEvaluator<ValueType> const& evaluator);
storm::expressions::SimpleValuation unpackStateIntoValuation(storm::storage::BitVector const& currentState);
/*!
* Retrieves the state id of the given state. If the state has not been encountered yet, it will be added to
@ -239,29 +223,8 @@ namespace storm {
* @param internalStateInformation The information about the already explored part of the reachable state space.
* @return A pair indicating whether the state was already discovered before and the state id of the state.
*/
static IndexType getOrAddStateIndex(CompressedState const& state, InternalStateInformation& internalStateInformation, std::queue<storm::storage::BitVector>& stateQueue);
StateType getOrAddStateIndex(CompressedState const& state);
/*!
* Retrieves all commands that are labeled with the given label and enabled in the given state, grouped by
* modules.
*
* This function will iterate over all modules and retrieve all commands that are labeled with the given
* action and active (i.e. enabled) in the current state. The result is a list of lists of commands in which
* the inner lists contain all commands of exactly one module. If a module does not have *any* (including
* disabled) commands, there will not be a list of commands of that module in the result. If, however, the
* module has a command with a relevant label, but no enabled one, nothing is returned to indicate that there
* is no legal transition possible.
*
* @param The program in which to search for active commands.
* @param state The current state.
* @param actionIndex The index of the action label to select.
* @return A list of lists of active commands or nothing.
*/
static boost::optional<std::vector<std::vector<std::reference_wrapper<storm::prism::Command const>>>> getActiveCommandsByActionIndex(storm::prism::Program const& program,storm::expressions::ExpressionEvaluator<ValueType> const& evaluator, uint_fast64_t const& actionIndex);
static std::vector<Choice<ValueType>> getUnlabeledTransitions(storm::prism::Program const& program, bool discreteTimeModel, InternalStateInformation& internalStateInformation, VariableInformation const& variableInformation, storm::storage::BitVector const& currentState, bool choiceLabeling, storm::expressions::ExpressionEvaluator<ValueType> const& evaluator, std::queue<storm::storage::BitVector>& stateQueue, storm::utility::ConstantsComparator<ValueType> const& comparator);
static std::vector<Choice<ValueType>> getLabeledTransitions(storm::prism::Program const& program, bool discreteTimeModel, InternalStateInformation& internalStateInformation, VariableInformation const& variableInformation, storm::storage::BitVector const& currentState, bool choiceLabeling, storm::expressions::ExpressionEvaluator<ValueType> const& evaluator, std::queue<storm::storage::BitVector>& stateQueue, storm::utility::ConstantsComparator<ValueType> const& comparator);
/*!
* Builds the transition matrix and the transition reward matrix based for the given program.
*
@ -279,7 +242,7 @@ namespace storm {
* @return A tuple containing a vector with all rows at which the nondeterministic choices of each state begin
* and a vector containing the labels associated with each choice.
*/
static boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>> buildMatrices(storm::prism::Program const& program, VariableInformation const& variableInformation, std::vector<std::reference_wrapper<storm::prism::RewardModel const>> const& selectedRewardModels, InternalStateInformation& internalStateInformation, bool commandLabels, bool deterministicModel, bool discreteTimeModel, storm::storage::SparseMatrixBuilder<ValueType>& transitionMatrixBuilder, std::vector<RewardModelBuilder<typename RewardModelType::ValueType>>& rewardModelBuilders, boost::optional<storm::expressions::Expression> const& terminalExpression);
boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>> buildMatrices(std::vector<std::reference_wrapper<storm::prism::RewardModel const>> const& selectedRewardModels, InternalStateInformation& internalStateInformation, storm::storage::SparseMatrixBuilder<ValueType>& transitionMatrixBuilder, std::vector<RewardModelBuilder<typename RewardModelType::ValueType>>& rewardModelBuilders, boost::optional<storm::expressions::Expression> const& terminalExpression);
/*!
* Explores the state space of the given program and returns the components of the model as a result.
@ -289,7 +252,7 @@ namespace storm {
* @param options A set of options used to customize the building process.
* @return A structure containing the components of the resulting model.
*/
ModelComponents buildModelComponents(storm::prism::Program const& program, std::vector<std::reference_wrapper<storm::prism::RewardModel const>> const& selectedRewardModels, Options const& options);
ModelComponents buildModelComponents(std::vector<std::reference_wrapper<storm::prism::RewardModel const>> const& selectedRewardModels);
/*!
* Builds the state labeling for the given program.
@ -299,14 +262,27 @@ namespace storm {
* @param internalStateInformation Information about the state space of the program.
* @return The state labeling of the given program.
*/
static storm::models::sparse::StateLabeling buildStateLabeling(storm::prism::Program const& program, VariableInformation const& variableInformation, InternalStateInformation const& internalStateInformation);
storm::models::sparse::StateLabeling buildStateLabeling();
// The program to translate. The necessary transformations are performed upon construction of the builder.
storm::prism::Program program;
// The options to be used for translating the program.
Options options;
// The variable information.
storm::generator::VariableInformation variableInformation;
// Internal information about the states that were explored.
InternalStateInformation internalStateInformation;
// This member holds information about reachable states that can be retrieved from the outside after a
// successful build.
boost::optional<StateInformation> stateInformation;
// This member holds the program that was most recently translated (if any).
boost::optional<storm::prism::Program> preparedProgram;
// A queue of states that still need to be explored.
std::queue<storm::storage::BitVector> statesToExplore;
};
} // namespace adapters

4
src/generator/Choice.cpp
View File

@ -6,7 +6,7 @@ namespace storm {
namespace generator {
template<typename ValueType, typename StateType>
Choice<ValueType, StateType>::Choice(uint_fast64_t actionIndex, bool markovian) : markovian(markovian), actionIndex(actionIndex), distribution(), totalMass(storm::utility::zero<ValueType>()), choiceReward(storm::utility::zero<ValueType>()) {
Choice<ValueType, StateType>::Choice(uint_fast64_t actionIndex, bool markovian) : markovian(markovian), actionIndex(actionIndex), distribution(), totalMass(storm::utility::zero<ValueType>()), choiceRewards() {
// Intentionally left empty.
}
@ -89,7 +89,7 @@ namespace storm {
template<typename ValueType, typename StateType>
void Choice<ValueType, StateType>::addChoiceReward(ValueType const& value) {
choiceReward += value;
choiceRewards.push_back(value);
}
template<typename ValueType, typename StateType>

4
src/generator/Choice.h
View File

@ -142,8 +142,8 @@ namespace storm {
// The total probability mass (or rates) of this choice.
ValueType totalMass;
// The reward value associated with this choice.
ValueType choiceReward;
// The reward values associated with this choice.
std::vector<ValueType> choiceRewards;
// The labels that are associated with this choice.
boost::optional<LabelSet> choiceLabels;

8
src/generator/NextStateGenerator.h
View File

@ -11,15 +11,15 @@
namespace storm {
namespace generator {
typedef storm::storage::BitVector CompressedState;
template<typename ValueType, typename StateType = uint32_t>
class NextStateGenerator {
public:
typedef storm::storage::BitVector InternalStateType;
typedef StateType (*StateToIdCallback)(InternalStateType const&);
typedef StateType (*StateToIdCallback)(CompressedState const&);
virtual std::vector<StateType> getInitialStates(StateToIdCallback stateToIdCallback) = 0;
virtual std::vector<Choice<ValueType>> expand(StateType const& state, StateToIdCallback stateToIdCallback) = 0;
virtual ValueType getStateReward(StateType const& state) = 0;
virtual std::vector<Choice<ValueType>> expand(CompressedState const& state, StateToIdCallback stateToIdCallback) = 0;
};
}
}

249
src/generator/PrismNextStateGenerator.cpp
View File

@ -1,22 +1,263 @@
#include "src/generator/PrismNextStateGenerator.h"
#include "src/utility/constants.h"
#include "src/utility/macros.h"
#include "src/exceptions/WrongFormatException.h"
namespace storm {
namespace generator {
template<typename ValueType, typename StateType>
PrismNextStateGenerator<ValueType, StateType>::PrismNextStateGenerator(storm::prism::Program const& program) : program(program) {
PrismNextStateGenerator<ValueType, StateType>::PrismNextStateGenerator(storm::prism::Program const& program, VariableInformation const& variableInformation, bool buildChoiceLabeling) : program(program), selectedRewardModels(), buildChoiceLabeling(buildChoiceLabeling), variableInformation(variableInformation), evaluator(), comparator() {
// Intentionally left empty.
}
template<typename ValueType, typename StateType>
std::vector<Choice<ValueType>> PrismNextStateGenerator<ValueType, StateType>::expand(StateType const& state, typename NextStateGenerator<ValueType, StateType>::StateToIdCallback stateToIdCallback) {
// TODO
void PrismNextStateGenerator<ValueType, StateType>::addRewardModel(storm::prism::RewardModel const& rewardModel) {
selectedRewardModels.push_back(rewardModel);
}
template<typename ValueType, typename StateType>
ValueType PrismNextStateGenerator<ValueType, StateType>::getStateReward(StateType const& state) {
std::vector<Choice<ValueType>> PrismNextStateGenerator<ValueType, StateType>::expand(CompressedState const& state, typename NextStateGenerator<ValueType, StateType>::StateToIdCallback stateToIdCallback) {
// TODO
}
template<typename ValueType, typename StateType>
void PrismNextStateGenerator<ValueType, StateType>::unpackStateIntoEvaluator(storm::storage::BitVector const& state) {
for (auto const& booleanVariable : variableInformation.booleanVariables) {
evaluator.setBooleanValue(booleanVariable.variable, state.get(booleanVariable.bitOffset));
}
for (auto const& integerVariable : variableInformation.integerVariables) {
evaluator.setIntegerValue(integerVariable.variable, state.getAsInt(integerVariable.bitOffset, integerVariable.bitWidth) + integerVariable.lowerBound);
}
}
template<typename ValueType, typename StateType>
CompressedState PrismNextStateGenerator<ValueType, StateType>::applyUpdate(CompressedState const& state, storm::prism::Update const& update) {
return applyUpdate(variableInformation, state, state, update);
}
template<typename ValueType, typename StateType>
CompressedState PrismNextStateGenerator<ValueType, StateType>::applyUpdate(CompressedState const& state, CompressedState const& baseState, storm::prism::Update const& update) {
CompressedState newState(state);
auto assignmentIt = update.getAssignments().begin();
auto assignmentIte = update.getAssignments().end();
// Iterate over all boolean assignments and carry them out.
auto boolIt = variableInformation.booleanVariables.begin();
for (; assignmentIt != assignmentIte && assignmentIt->getExpression().hasBooleanType(); ++assignmentIt) {
while (assignmentIt->getVariable() != boolIt->variable) {
++boolIt;
}
newState.set(boolIt->bitOffset, evaluator.asBool(assignmentIt->getExpression()));
}
// Iterate over all integer assignments and carry them out.
auto integerIt = variableInformation.integerVariables.begin();
for (; assignmentIt != assignmentIte && assignmentIt->getExpression().hasIntegerType(); ++assignmentIt) {
while (assignmentIt->getVariable() != integerIt->variable) {
++integerIt;
}
int_fast64_t assignedValue = evaluator.asInt(assignmentIt->getExpression());
STORM_LOG_THROW(assignedValue <= integerIt->upperBound, storm::exceptions::WrongFormatException, "The update " << update << " leads to an out-of-bounds value (" << assignedValue << ") for the variable '" << assignmentIt->getVariableName() << "'.");
newState.setFromInt(integerIt->bitOffset, integerIt->bitWidth, assignedValue - integerIt->lowerBound);
STORM_LOG_ASSERT(static_cast<int_fast64_t>(newState.getAsInt(integerIt->bitOffset, integerIt->bitWidth)) + integerIt->lowerBound == assignedValue, "Writing to the bit vector bucket failed (read " << newState.getAsInt(integerIt->bitOffset, integerIt->bitWidth) << " but wrote " << assignedValue << ").");
}
// Check that we processed all assignments.
STORM_LOG_ASSERT(assignmentIt == assignmentIte, "Not all assignments were consumed.");
return newState;
}
template<typename ValueType, typename StateType>
boost::optional<std::vector<std::vector<std::reference_wrapper<storm::prism::Command const>>>> PrismNextStateGenerator<ValueType, StateType>::getActiveCommandsByActionIndex(uint_fast64_t const& actionIndex) {
boost::optional<std::vector<std::vector<std::reference_wrapper<storm::prism::Command const>>>> result((std::vector<std::vector<std::reference_wrapper<storm::prism::Command const>>>()));
// Iterate over all modules.
for (uint_fast64_t i = 0; i < program.getNumberOfModules(); ++i) {
storm::prism::Module const& module = program.getModule(i);
// If the module has no command labeled with the given action, we can skip this module.
if (!module.hasActionIndex(actionIndex)) {
continue;
}
std::set<uint_fast64_t> const& commandIndices = module.getCommandIndicesByActionIndex(actionIndex);
// If the module contains the action, but there is no command in the module that is labeled with
// this action, we don't have any feasible command combinations.
if (commandIndices.empty()) {
return boost::optional<std::vector<std::vector<std::reference_wrapper<storm::prism::Command const>>>>();
}
std::vector<std::reference_wrapper<storm::prism::Command const>> commands;
// Look up commands by their indices and add them if the guard evaluates to true in the given state.
for (uint_fast64_t commandIndex : commandIndices) {
storm::prism::Command const& command = module.getCommand(commandIndex);
if (evaluator.asBool(command.getGuardExpression())) {
commands.push_back(command);
}
}
// If there was no enabled command although the module has some command with the required action label,
// we must not return anything.
if (commands.size() == 0) {
return boost::optional<std::vector<std::vector<std::reference_wrapper<storm::prism::Command const>>>>();
}
result.get().push_back(std::move(commands));
}
return result;
}
template<typename ValueType, typename StateType>
std::vector<Choice<ValueType>> PrismNextStateGenerator<ValueType, StateType>::getUnlabeledTransitions(CompressedState const& state, StateToIdCallback stateToIdCallback) {
std::vector<Choice<ValueType>> result;
// Iterate over all modules.
for (uint_fast64_t i = 0; i < program.getNumberOfModules(); ++i) {
storm::prism::Module const& module = program.getModule(i);
// Iterate over all commands.
for (uint_fast64_t j = 0; j < module.getNumberOfCommands(); ++j) {
storm::prism::Command const& command = module.getCommand(j);
// Only consider unlabeled commands.
if (command.isLabeled()) continue;
// Skip the command, if it is not enabled.
if (!evaluator.asBool(command.getGuardExpression())) {
continue;
}
result.push_back(Choice<ValueType>(0, buildChoiceLabeling));
Choice<ValueType>& choice = result.back();
// Remember the command labels only if we were asked to.
if (buildChoiceLabeling) {
choice.addChoiceLabel(command.getGlobalIndex());
}
// Iterate over all updates of the current command.
ValueType probabilitySum = storm::utility::zero<ValueType>();
for (uint_fast64_t k = 0; k < command.getNumberOfUpdates(); ++k) {
storm::prism::Update const& update = command.getUpdate(k);
// Obtain target state index and add it to the list of known states. If it has not yet been
// seen, we also add it to the set of states that have yet to be explored.
StateType stateIndex = stateToIdCallback(applyUpdate(state, update));
// Update the choice by adding the probability/target state to it.
ValueType probability = evaluator.asRational(update.getLikelihoodExpression());
choice.addProbability(stateIndex, probability);
probabilitySum += probability;
}
// Check that the resulting distribution is in fact a distribution.
STORM_LOG_THROW(!program.isDiscreteTimeModel() || comparator.isOne(probabilitySum), storm::exceptions::WrongFormatException, "Probabilities do not sum to one for command '" << command << "' (actually sum to " << probabilitySum << ").");
}
}
return result;
}
template<typename ValueType, typename StateType>
std::vector<Choice<ValueType>> PrismNextStateGenerator<ValueType, StateType>::getLabeledTransitions(CompressedState const& state, StateToIdCallback stateToIdCallback) {
std::vector<Choice<ValueType>> result;
for (uint_fast64_t actionIndex : program.getSynchronizingActionIndices()) {
boost::optional<std::vector<std::vector<std::reference_wrapper<storm::prism::Command const>>>> optionalActiveCommandLists = getActiveCommandsByActionIndex(program, evaluator, actionIndex);
// Only process this action label, if there is at least one feasible solution.
if (optionalActiveCommandLists) {
std::vector<std::vector<std::reference_wrapper<storm::prism::Command const>>> const& activeCommandList = optionalActiveCommandLists.get();
std::vector<std::vector<std::reference_wrapper<storm::prism::Command const>>::const_iterator> iteratorList(activeCommandList.size());
// Initialize the list of iterators.
for (size_t i = 0; i < activeCommandList.size(); ++i) {
iteratorList[i] = activeCommandList[i].cbegin();
}
// As long as there is one feasible combination of commands, keep on expanding it.
bool done = false;
while (!done) {
std::unordered_map<CompressedState, ValueType>* currentTargetStates = new std::unordered_map<CompressedState, ValueType>();
std::unordered_map<CompressedState, ValueType>* newTargetStates = new std::unordered_map<CompressedState, ValueType>();
currentTargetStates->emplace(state, storm::utility::one<ValueType>());
for (uint_fast64_t i = 0; i < iteratorList.size(); ++i) {
storm::prism::Command const& command = *iteratorList[i];
for (uint_fast64_t j = 0; j < command.getNumberOfUpdates(); ++j) {
storm::prism::Update const& update = command.getUpdate(j);
for (auto const& stateProbabilityPair : *currentTargetStates) {
// Compute the new state under the current update and add it to the set of new target states.
CompressedState newTargetState = applyUpdate(stateProbabilityPair.first, state, update);
newTargetStates->emplace(newTargetState, stateProbabilityPair.second * evaluator.asRational(update.getLikelihoodExpression()));
}
}
// If there is one more command to come, shift the target states one time step back.
if (i < iteratorList.size() - 1) {
delete currentTargetStates;
currentTargetStates = newTargetStates;
newTargetStates = new std::unordered_map<CompressedState, ValueType>();
}
}
// At this point, we applied all commands of the current command combination and newTargetStates
// contains all target states and their respective probabilities. That means we are now ready to
// add the choice to the list of transitions.
result.push_back(Choice<ValueType>(actionIndex, buildChoiceLabeling));
// Now create the actual distribution.
Choice<ValueType>& choice = result.back();
// Remember the command labels only if we were asked to.
if (buildChoiceLabeling) {
// Add the labels of all commands to this choice.
for (uint_fast64_t i = 0; i < iteratorList.size(); ++i) {
choice.addChoiceLabel(iteratorList[i]->get().getGlobalIndex());
}
}
ValueType probabilitySum = storm::utility::zero<ValueType>();
for (auto const& stateProbabilityPair : *newTargetStates) {
StateType actualIndex = stateToIdCallback(stateProbabilityPair.first);
choice.addProbability(actualIndex, stateProbabilityPair.second);
probabilitySum += stateProbabilityPair.second;
}
// Check that the resulting distribution is in fact a distribution.
STORM_LOG_THROW(!program.isDiscreteTimeModel() || !comparator.isConstant(probabilitySum) || comparator.isOne(probabilitySum), storm::exceptions::WrongFormatException, "Sum of update probabilities do not some to one for some command (actually sum to " << probabilitySum << ").");
// Dispose of the temporary maps.
delete currentTargetStates;
delete newTargetStates;
// Now, check whether there is one more command combination to consider.
bool movedIterator = false;
for (int_fast64_t j = iteratorList.size() - 1; j >= 0; --j) {
++iteratorList[j];
if (iteratorList[j] != activeCommandList[j].end()) {
movedIterator = true;
} else {
// Reset the iterator to the beginning of the list.
iteratorList[j] = activeCommandList[j].begin();
}
}
done = !movedIterator;
}
}
}
return result;
}
}
}

90
src/generator/PrismNextStateGenerator.h
View File

@ -2,8 +2,10 @@
#define STORM_GENERATOR_PRISMNEXTSTATEGENERATOR_H_
#include "src/generator/NextStateGenerator.h"
#include "src/generator/VariableInformation.h"
#include "src/storage/prism/Program.h"
#include "src/storage/expressions/ExpressionEvaluator.h"
namespace storm {
namespace generator {
@ -13,17 +15,97 @@ namespace storm {
public:
typedef typename NextStateGenerator<ValueType, StateType>::StateToIdCallback StateToIdCallback;
PrismNextStateGenerator(storm::prism::Program const& program);
PrismNextStateGenerator(storm::prism::Program const& program, VariableInformation const& variableInformation, bool buildChoiceLabeling);
/*!
* Adds a reward model to the list of selected reward models ()
*/
void addRewardModel(storm::prism::RewardModel const& rewardModel);
virtual std::vector<StateType> getInitialStates(StateToIdCallback stateToIdCallback) = 0;
virtual std::vector<Choice<ValueType>> expand(StateType const& state, StateToIdCallback stateToIdCallback) override;
virtual ValueType getStateReward(StateType const& state) override;
virtual std::vector<Choice<ValueType>> expand(CompressedState const& state, StateToIdCallback stateToIdCallback) override;
private:
/*!
* Unpacks the compressed state into the evaluator.
*
* @param state The state to unpack.
*/
void unpackStateIntoEvaluator(CompressedState const& state);
/*!
* Applies an update to the given state and returns the resulting new state object. This methods does not
* modify the given state but returns a new one.
*
* @params state The state to which to apply the update.
* @params update The update to apply.
* @return The resulting state.
*/
CompressedState applyUpdate(CompressedState const& state, storm::prism::Update const& update);
/*!
* Applies an update to the given state and returns the resulting new state object. The update is evaluated
* over the variable values of the given base state. This methods does not modify the given state but
* returns a new one.
*
* @param state The state to which to apply the update.
* @param baseState The state used for evaluating the update.
* @param update The update to apply.
* @return The resulting state.
*/
CompressedState applyUpdate(CompressedState const& state, CompressedState const& baseState, storm::prism::Update const& update);
/*!
* Retrieves all commands that are labeled with the given label and enabled in the given state, grouped by
* modules.
*
* This function will iterate over all modules and retrieve all commands that are labeled with the given
* action and active (i.e. enabled) in the current state. The result is a list of lists of commands in which
* the inner lists contain all commands of exactly one module. If a module does not have *any* (including
* disabled) commands, there will not be a list of commands of that module in the result. If, however, the
* module has a command with a relevant label, but no enabled one, nothing is returned to indicate that there
* is no legal transition possible.
*
* @param The program in which to search for active commands.
* @param state The current state.
* @param actionIndex The index of the action label to select.
* @return A list of lists of active commands or nothing.
*/
boost::optional<std::vector<std::vector<std::reference_wrapper<storm::prism::Command const>>>> getActiveCommandsByActionIndex(uint_fast64_t const& actionIndex);
/*!
* Retrieves all unlabeled choices possible from the given state.
*
* @param state The state for which to retrieve the unlabeled choices.
* @return The unlabeled choices of the state.
*/
std::vector<Choice<ValueType>> getUnlabeledChoices(CompressedState const& state, StateToIdCallback stateToIdCallback);
/*!
* Retrieves all labeled choices possible from the given state.
*
* @param state The state for which to retrieve the unlabeled choices.
* @return The labeled choices of the state.
*/
std::vector<Choice<ValueType>> getLabeledChoices(CompressedState const& state, StateToIdCallback stateToIdCallback);
// The program used for the generation of next states.
storm::prism::Program program;
storm::prism::Program const& program;
// The reward models that need to be considered.
std::vector<std::reference_wrapper<storm::prism::RewardModel const>> selectedRewardModels;
// A flag that stores whether or not to build the choice labeling.
bool buildChoiceLabeling;
// Information about how the variables are packed
VariableInformation const& variableInformation;
// An evaluator used to evaluate expressions.
storm::expressions::ExpressionEvaluator<ValueType> evaluator;
// A comparator used to compare constants.
storm::utility::ConstantsComparator<ValueType> comparator;
};
}

42
src/generator/VariableInformation.cpp
View File

@ -0,0 +1,42 @@
#include "src/generator/prism/VariableInformation.h"
#include "src/utility/macros.h"
#include "src/exceptions/InvalidArgumentException.h"
namespace storm {
namespace generator {
BooleanVariableInformation::BooleanVariableInformation(storm::expressions::Variable const& variable, bool initialValue, uint_fast64_t bitOffset) : variable(variable), initialValue(initialValue), bitOffset(bitOffset) {
// Intentionally left empty.
}
IntegerVariableInformation::IntegerVariableInformation(storm::expressions::Variable const& variable, int_fast64_t initialValue, int_fast64_t lowerBound, int_fast64_t upperBound, uint_fast64_t bitOffset, uint_fast64_t bitWidth) : variable(variable), initialValue(initialValue), lowerBound(lowerBound), upperBound(upperBound), bitOffset(bitOffset), bitWidth(bitWidth) {
// Intentionally left empty.
}
VariableInformation::VariableInformation(storm::expressions::ExpressionManager const& manager) : manager(manager) {
// Intentionally left empty.
}
uint_fast64_t VariableInformation::getBitOffset(storm::expressions::Variable const& variable) const {
auto const& booleanIndex = booleanVariableToIndexMap.find(variable);
if (booleanIndex != booleanVariableToIndexMap.end()) {
return booleanVariables[booleanIndex->second].bitOffset;
}
auto const& integerIndex = integerVariableToIndexMap.find(variable);
if (integerIndex != integerVariableToIndexMap.end()) {
return integerVariables[integerIndex->second].bitOffset;
}
STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Cannot look-up bit index of unknown variable.");
}
uint_fast64_t VariableInformation::getBitWidth(storm::expressions::Variable const& variable) const {
auto const& integerIndex = integerVariableToIndexMap.find(variable);
if (integerIndex != integerVariableToIndexMap.end()) {
return integerVariables[integerIndex->second].bitWidth;
}
STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Cannot look-up bit width of unknown variable.");
}
}
}

71
src/generator/VariableInformation.h
View File

@ -0,0 +1,71 @@
#ifndef STORM_GENERATOR_PRISM_VARIABLEINFORMATION_H_
#define STORM_GENERATOR_PRISM_VARIABLEINFORMATION_H_
#include <vector>
#include <boost/container/flat_map.hpp>
#include "src/storage/expressions/Variable.h"
namespace storm {
namespace generator {
// A structure storing information about the boolean variables of the program.
struct BooleanVariableInformation {
BooleanVariableInformation(storm::expressions::Variable const& variable, bool initialValue, uint_fast64_t bitOffset);
// The boolean variable.
storm::expressions::Variable variable;
// Its initial value.
bool initialValue;
// Its bit offset in the compressed state.
uint_fast64_t bitOffset;
};
// A structure storing information about the integer variables of the program.
struct IntegerVariableInformation {
IntegerVariableInformation(storm::expressions::Variable const& variable, int_fast64_t initialValue, int_fast64_t lowerBound, int_fast64_t upperBound, uint_fast64_t bitOffset, uint_fast64_t bitWidth);
// The integer variable.
storm::expressions::Variable variable;
// Its initial value.
int_fast64_t initialValue;
// The lower bound of its range.
int_fast64_t lowerBound;
// The upper bound of its range.
int_fast64_t upperBound;
// Its bit offset in the compressed state.
uint_fast64_t bitOffset;
// Its bit width in the compressed state.
uint_fast64_t bitWidth;
};
// A structure storing information about the used variables of the program.
struct VariableInformation {
VariableInformation(storm::expressions::ExpressionManager const& manager);
// Provide methods to access the bit offset and width of variables in the compressed state.
uint_fast64_t getBitOffset(storm::expressions::Variable const& variable) const;
uint_fast64_t getBitWidth(storm::expressions::Variable const& variable) const;
// The known boolean variables.
boost::container::flat_map<storm::expressions::Variable, uint_fast64_t> booleanVariableToIndexMap;
std::vector<BooleanVariableInformation> booleanVariables;
// The known integer variables.
boost::container::flat_map<storm::expressions::Variable, uint_fast64_t> integerVariableToIndexMap;
std::vector<IntegerVariableInformation> integerVariables;
storm::expressions::ExpressionManager const& manager;
};
}
}
#endif /* STORM_GENERATOR_PRISM_VARIABLEINFORMATION_H_ */

44
src/generator/prism/VariableInformation.cpp
View File

@ -1,44 +0,0 @@
#include "src/generator/prism/VariableInformation.h"
#include "src/utility/macros.h"
#include "src/exceptions/InvalidArgumentException.h"
namespace storm {
namespace generator {
namespace prism {
BooleanVariableInformation::BooleanVariableInformation(storm::expressions::Variable const& variable, bool initialValue, uint_fast64_t bitOffset) : variable(variable), initialValue(initialValue), bitOffset(bitOffset) {
// Intentionally left empty.
}
IntegerVariableInformation::IntegerVariableInformation(storm::expressions::Variable const& variable, int_fast64_t initialValue, int_fast64_t lowerBound, int_fast64_t upperBound, uint_fast64_t bitOffset, uint_fast64_t bitWidth) : variable(variable), initialValue(initialValue), lowerBound(lowerBound), upperBound(upperBound), bitOffset(bitOffset), bitWidth(bitWidth) {
// Intentionally left empty.
}
VariableInformation::VariableInformation(storm::expressions::ExpressionManager const& manager) : manager(manager) {
// Intentionally left empty.
}
uint_fast64_t VariableInformation::getBitOffset(storm::expressions::Variable const& variable) const {
auto const& booleanIndex = booleanVariableToIndexMap.find(variable);
if (booleanIndex != booleanVariableToIndexMap.end()) {
return booleanVariables[booleanIndex->second].bitOffset;
}
auto const& integerIndex = integerVariableToIndexMap.find(variable);
if (integerIndex != integerVariableToIndexMap.end()) {
return integerVariables[integerIndex->second].bitOffset;
}
STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Cannot look-up bit index of unknown variable.");
}
uint_fast64_t VariableInformation::getBitWidth(storm::expressions::Variable const& variable) const {
auto const& integerIndex = integerVariableToIndexMap.find(variable);
if (integerIndex != integerVariableToIndexMap.end()) {
return integerVariables[integerIndex->second].bitWidth;
}
STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Cannot look-up bit width of unknown variable.");
}
}
}
}

73
src/generator/prism/VariableInformation.h
View File

@ -1,73 +0,0 @@
#ifndef STORM_GENERATOR_PRISM_VARIABLEINFORMATION_H_
#define STORM_GENERATOR_PRISM_VARIABLEINFORMATION_H_
#include <vector>
#include <boost/container/flat_map.hpp>
#include "src/storage/expressions/Variable.h"
namespace storm {
namespace generator {
namespace prism {
// A structure storing information about the boolean variables of the program.
struct BooleanVariableInformation {
BooleanVariableInformation(storm::expressions::Variable const& variable, bool initialValue, uint_fast64_t bitOffset);
// The boolean variable.
storm::expressions::Variable variable;
// Its initial value.
bool initialValue;
// Its bit offset in the compressed state.
uint_fast64_t bitOffset;
};
// A structure storing information about the integer variables of the program.
struct IntegerVariableInformation {
IntegerVariableInformation(storm::expressions::Variable const& variable, int_fast64_t initialValue, int_fast64_t lowerBound, int_fast64_t upperBound, uint_fast64_t bitOffset, uint_fast64_t bitWidth);
// The integer variable.
storm::expressions::Variable variable;
// Its initial value.
int_fast64_t initialValue;
// The lower bound of its range.
int_fast64_t lowerBound;
// The upper bound of its range.
int_fast64_t upperBound;
// Its bit offset in the compressed state.
uint_fast64_t bitOffset;
// Its bit width in the compressed state.
uint_fast64_t bitWidth;
};
// A structure storing information about the used variables of the program.
struct VariableInformation {
VariableInformation(storm::expressions::ExpressionManager const& manager);
// Provide methods to access the bit offset and width of variables in the compressed state.
uint_fast64_t getBitOffset(storm::expressions::Variable const& variable) const;
uint_fast64_t getBitWidth(storm::expressions::Variable const& variable) const;
// The known boolean variables.
boost::container::flat_map<storm::expressions::Variable, uint_fast64_t> booleanVariableToIndexMap;
std::vector<BooleanVariableInformation> booleanVariables;
// The known integer variables.
boost::container::flat_map<storm::expressions::Variable, uint_fast64_t> integerVariableToIndexMap;
std::vector<IntegerVariableInformation> integerVariables;
storm::expressions::ExpressionManager const& manager;
};
}
}
}
#endif /* STORM_GENERATOR_PRISM_VARIABLEINFORMATION_H_ */

4
src/storage/prism/Program.cpp
View File

@ -77,6 +77,10 @@ namespace storm {
return modelType;
}
bool Program::isDiscreteTimeModel() const {
return modelType == ModelType::DTMC || modelType == ModelType::MDP;
}
bool Program::hasUndefinedConstants() const {
for (auto const& constant : this->getConstants()) {
if (!constant.isDefined()) {

12
src/storage/prism/Program.h
View File

@ -67,6 +67,18 @@ namespace storm {
*/
ModelType getModelType() const;
/*!
* Retrieves whether the model is a discrete-time model, i.e. a DTMC or an MDP.
*
* @return True iff the model is a discrete-time model.
*/
bool isDiscreteTimeModel() const;
/*!
* Retrieves whether the model is one without nondeterministic choices, i.e. a DTMC or a CTMC.
*/
bool isDeterministicModel() const;
/*!
* Retrieves whether there are undefined constants of any type in the program.
*

Write Preview
|||||||
100:0
Loading…
Cancel
Save