diff --git a/CMakeLists.txt b/CMakeLists.txt index 311fb0515..fb878f8d2 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -32,6 +32,7 @@ option(USE_INTELTBB "Sets whether the Intel TBB Extensions should be used." OFF) option(STORM_USE_COTIRE "Sets whether Cotire should be used (for building precompiled headers)." OFF) option(LINK_LIBCXXABI "Sets whether libc++abi should be linked." OFF) set(GUROBI_ROOT "" CACHE STRING "The root directory of Gurobi (if available).") +set(Z3_ROOT "" CACHE STRING "The root directory of Z3 (if available).") set(ADDITIONAL_INCLUDE_DIRS "" CACHE STRING "Additional directories added to the include directories.") set(ADDITIONAL_LINK_DIRS "" CACHE STRING "Additional directories added to the link directories.") set(CUSTOM_BOOST_ROOT "" CACHE STRING "A custom path to the Boost root directory.") @@ -84,6 +85,12 @@ else() set(ENABLE_GUROBI ON) endif() +if ("${Z3_ROOT}" STREQUAL "") + set(ENABLE_Z3 OFF) +else() + set(ENABLE_Z3 ON) +endif() + message(STATUS "StoRM - CMAKE_BUILD_TYPE: ${CMAKE_BUILD_TYPE}") message(STATUS "StoRM - CMAKE_BUILD_TYPE (ENV): $ENV{CMAKE_BUILD_TYPE}") @@ -171,6 +178,13 @@ else() set(STORM_CPP_GUROBI_DEF "undef") endif() +# Z3 Defines +if (ENABLE_Z3) + set(STORM_CPP_Z3_DEF "define") +else() + set(STORM_CPP_Z3_DEF "undef") +endif() + # Intel TBB Defines if (TBB_FOUND AND USE_INTELTBB) set(STORM_CPP_INTELTBB_DEF "define") @@ -264,6 +278,9 @@ endif(ADDITIONAL_LINK_DIRS) if (ENABLE_GUROBI) link_directories("${GUROBI_ROOT}/lib") endif() +if (ENABLE_Z3) + link_directories("${Z3_ROOT}/build") +endif() if ((NOT Boost_LIBRARY_DIRS) OR ("${Boost_LIBRARY_DIRS}" STREQUAL "")) set(Boost_LIBRARY_DIRS "${Boost_INCLUDE_DIRS}/stage/lib") endif () @@ -336,6 +353,19 @@ if (ENABLE_GUROBI) target_link_libraries(storm-performance-tests "gurobi55") endif(ENABLE_GUROBI) +############################################################# +## +## Z3 (optional) +## +############################################################# +if (ENABLE_Z3) + message (STATUS "StoRM - Linking with Z3") + include_directories("${Z3_ROOT}/src/c++") + target_link_libraries(storm "z3") + target_link_libraries(storm-functional-tests "z3") + target_link_libraries(storm-performance-tests "z3") +endif(ENABLE_Z3) + ############################################################# ## ## Google Test gtest diff --git a/src/adapters/ExplicitModelAdapter.h b/src/adapters/ExplicitModelAdapter.h index 20d2c1133..9e01e8952 100644 --- a/src/adapters/ExplicitModelAdapter.h +++ b/src/adapters/ExplicitModelAdapter.h @@ -257,7 +257,7 @@ namespace storm { public: // A structure holding information about the reachable state space. struct StateInformation { - StateInformation() : reachableStates(), stateToIndexMap(), numberOfChoices(), numberOfTransitions(0) { + StateInformation() : reachableStates(), stateToIndexMap() { // Intentionally left empty. } @@ -266,12 +266,6 @@ namespace storm { // A mapping from states to indices in the list of reachable states. std::unordered_map stateToIndexMap; - - // A vector storing the number of choices for each state. - std::vector numberOfChoices; - - // The total number of transitions discovered. - uint_fast64_t numberOfTransitions; }; // A structure holding the individual components of a model. @@ -339,16 +333,16 @@ namespace storm { std::shared_ptr> result; switch (program.getModelType()) { case storm::ir::Program::DTMC: - result = std::shared_ptr>(new storm::models::Dtmc(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), std::move(modelComponents.stateRewards), std::move(modelComponents.transitionRewardMatrix), std::move(modelComponents.choiceLabeling))); + result = std::shared_ptr>(new storm::models::Dtmc(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), rewardModelName != "" ? std::move(modelComponents.stateRewards) : boost::optional>(), rewardModelName != "" ? std::move(modelComponents.transitionRewardMatrix) : boost::optional>(), std::move(modelComponents.choiceLabeling))); break; case storm::ir::Program::CTMC: - result = std::shared_ptr>(new storm::models::Ctmc(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), std::move(modelComponents.stateRewards), std::move(modelComponents.transitionRewardMatrix), std::move(modelComponents.choiceLabeling))); + result = std::shared_ptr>(new storm::models::Ctmc(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), rewardModelName != "" ? std::move(modelComponents.stateRewards) : boost::optional>(), rewardModelName != "" ? std::move(modelComponents.transitionRewardMatrix) : boost::optional>(), std::move(modelComponents.choiceLabeling))); break; case storm::ir::Program::MDP: - result = std::shared_ptr>(new storm::models::Mdp(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), std::move(modelComponents.nondeterministicChoiceIndices), std::move(modelComponents.stateRewards), std::move(modelComponents.transitionRewardMatrix), std::move(modelComponents.choiceLabeling))); + result = std::shared_ptr>(new storm::models::Mdp(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), std::move(modelComponents.nondeterministicChoiceIndices), rewardModelName != "" ? std::move(modelComponents.stateRewards) : boost::optional>(), rewardModelName != "" ? std::move(modelComponents.transitionRewardMatrix) : boost::optional>(), std::move(modelComponents.choiceLabeling))); break; case storm::ir::Program::CTMDP: - result = std::shared_ptr>(new storm::models::Ctmdp(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), std::move(modelComponents.nondeterministicChoiceIndices), std::move(modelComponents.stateRewards), std::move(modelComponents.transitionRewardMatrix), std::move(modelComponents.choiceLabeling))); + result = std::shared_ptr>(new storm::models::Ctmdp(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), std::move(modelComponents.nondeterministicChoiceIndices), rewardModelName != "" ? std::move(modelComponents.stateRewards) : boost::optional>(), rewardModelName != "" ? std::move(modelComponents.transitionRewardMatrix) : boost::optional>(), std::move(modelComponents.choiceLabeling))); break; default: LOG4CPLUS_ERROR(logger, "Error while creating model from probabilistic program: cannot handle this model type."); @@ -572,7 +566,6 @@ namespace storm { if (indexIt == stateInformation.stateToIndexMap.end()) { // The state has not been seen, yet, so add it to the list of all reachable states. stateInformation.stateToIndexMap[state] = stateInformation.reachableStates.size(); - stateInformation.numberOfChoices.push_back(0); stateInformation.reachableStates.push_back(state); return std::make_pair(false, stateInformation.stateToIndexMap[state]); } else { @@ -581,59 +574,7 @@ namespace storm { return std::make_pair(true, indexIt->second); } } - - /*! - * Expands all unlabeled (i.e. independent) transitions of the given state and adds newly discovered states - * to the given queue. - * - * @param program The program that defines the transitions. - * @param stateInformation Provides information about the discovered state space. - * @param variableInformation A structure with information about the variables in the program. - * @param stateIndex The index of the state to expand. - * @param stateQueue The queue of states into which newly discovered states are inserted. - */ - static void exploreUnlabeledTransitions(storm::ir::Program const& program, StateInformation& stateInformation, VariableInformation const& variableInformation, uint_fast64_t stateIndex, std::queue& stateQueue) { - StateType const* currentState = stateInformation.reachableStates[stateIndex]; - - // Iterate over all modules. - for (uint_fast64_t i = 0; i < program.getNumberOfModules(); ++i) { - storm::ir::Module const& module = program.getModule(i); - - // Iterate over all commands. - for (uint_fast64_t j = 0; j < module.getNumberOfCommands(); ++j) { - storm::ir::Command const& command = module.getCommand(j); - - // Only consider unlabeled commands. - if (command.getActionName() != "") continue; - // Skip the command, if it is not enabled. - if (!command.getGuard()->getValueAsBool(currentState)) continue; - - ++stateInformation.numberOfChoices[stateIndex]; - - std::set targetStates; - - // Iterate over all updates of the current command. - for (uint_fast64_t k = 0; k < command.getNumberOfUpdates(); ++k) { - storm::ir::Update const& update = command.getUpdate(k); - - // Obtain target state index. - std::pair flagAndTargetStateIndexPair = getOrAddStateIndex(applyUpdate(variableInformation, currentState, update), stateInformation); - - // If the state has not yet been discovered, add it to the queue. - if (!flagAndTargetStateIndexPair.first) { - stateQueue.push(flagAndTargetStateIndexPair.second); - } - - // In any case, record that there is a transition to the newly found state to count the number - // of transitions correctly. - targetStates.insert(flagAndTargetStateIndexPair.second); - } - - stateInformation.numberOfTransitions += targetStates.size(); - } - } - } - + /*! * Retrieves all commands that are labeled with the given label and enabled in the given state, grouped by * modules. @@ -684,149 +625,6 @@ namespace storm { return result; } - /*! - * Expands all labeled (i.e. synchronizing) transitions of the given state and adds newly discovered states - * to the given queue. - * - * @param program The program that defines the transitions. - * @param stateInformation Provides information about the discovered state space. - * @param variableInformation A structure with information about the variables in the program. - * @param stateIndex The index of the state to expand. - * @param stateQueue The queue of states into which newly discovered states are inserted. - */ - static void exploreLabeledTransitions(storm::ir::Program const& program, StateInformation& stateInformation, VariableInformation const& variableInformation, uint_fast64_t stateIndex, std::queue& stateQueue) { - for (std::string const& action : program.getActions()) { - StateType const* currentState = stateInformation.reachableStates[stateIndex]; - boost::optional>> optionalActiveCommandLists = getActiveCommandsByAction(program, currentState, action); - - // Only process this action label, if there is at least one feasible solution. - if (optionalActiveCommandLists) { - std::vector> const& activeCommandList = optionalActiveCommandLists.get(); - std::vector::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) { - ++stateInformation.numberOfChoices[stateIndex]; - - std::unordered_set* currentTargetStates = new std::unordered_set(); - std::unordered_set* newTargetStates = new std::unordered_set(); - currentTargetStates->insert(new StateType(*currentState)); - - // FIXME: This does not check whether a global variable is written multiple times. While the - // behaviour for this is undefined anyway, a warning should be issued in that case. - for (uint_fast64_t i = 0; i < iteratorList.size(); ++i) { - storm::ir::Command const& command = *iteratorList[i]; - - for (uint_fast64_t j = 0; j < command.getNumberOfUpdates(); ++j) { - storm::ir::Update const& update = command.getUpdate(j); - - for (auto const& targetState : *currentTargetStates) { - StateType* newTargetState = applyUpdate(variableInformation, targetState, currentState, update); - - auto existingState = newTargetStates->find(newTargetState); - if (existingState == newTargetStates->end()) { - newTargetStates->insert(newTargetState); - } else { - // If the state was already seen in one of the other updates, we need to delete this copy. - delete newTargetState; - } - } - } - - // If there is one more command to come, shift the target states one time step back. - if (i < iteratorList.size() - 1) { - for (auto const& state : *currentTargetStates) { - delete state; - } - delete currentTargetStates; - currentTargetStates = newTargetStates; - newTargetStates = new std::unordered_set(); - } - } - - // If there are states that have not yet been discovered, add them to the queue. - for (auto const& state : *newTargetStates) { - std::pair flagAndNewStateIndexPair = getOrAddStateIndex(state, stateInformation); - - if (!flagAndNewStateIndexPair.first) { - stateQueue.push(flagAndNewStateIndexPair.second); - } - } - - stateInformation.numberOfTransitions += newTargetStates->size(); - - // 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; - } - } - } - } - - /*! - * Explores the reachable state space given by the program and returns a list of all states as well as a - * mapping from states to their indices. - * - * @param program The program whose state space to explore. - * @param variableInformation A structure with information about the variables in the program. - * @return A structure containing all reachable states and a mapping from states to their indices. - */ - static StateInformation exploreReachableStateSpace(storm::ir::Program const& program, VariableInformation const& variableInformation) { - StateInformation stateInformation; - - // Initialize a queue and insert the initial state. - std::queue stateQueue; - StateType* initialState = getInitialState(program, variableInformation); - getOrAddStateIndex(initialState, stateInformation); - stateQueue.push(stateInformation.stateToIndexMap[initialState]); - - // Now explore the current state until there is no more reachable state. - while (!stateQueue.empty()) { - uint_fast64_t currentStateIndex = stateQueue.front(); - - exploreUnlabeledTransitions(program, stateInformation, variableInformation, currentStateIndex, stateQueue); - exploreLabeledTransitions(program, stateInformation, variableInformation, currentStateIndex, stateQueue); - - // If the state does not have any outgoing transitions, we fix this by adding a self-loop if the - // option was set. - if (stateInformation.numberOfChoices[currentStateIndex] == 0) { - if (storm::settings::Settings::getInstance()->isSet("fixDeadlocks")) { - ++stateInformation.numberOfTransitions; - ++stateInformation.numberOfChoices[currentStateIndex] = 1; - } else { - LOG4CPLUS_ERROR(logger, "Error while creating sparse matrix from probabilistic program: found deadlock state. For fixing these, please provide the appropriate option."); - throw storm::exceptions::WrongFormatException() << "Error while creating sparse matrix from probabilistic program: found deadlock state. For fixing these, please provide the appropriate option."; - } - } - - - // After exploring a state, remove it from the queue. - stateQueue.pop(); - } - - return stateInformation; - } - /*! * Aggregates information about the variables in the program. * @@ -879,7 +677,7 @@ namespace storm { return result; } - static std::list> getUnlabeledTransitions(storm::ir::Program const& program, StateInformation const& stateInformation, VariableInformation const& variableInformation, uint_fast64_t stateIndex) { + static std::list> getUnlabeledTransitions(storm::ir::Program const& program, StateInformation& stateInformation, VariableInformation const& variableInformation, uint_fast64_t stateIndex, std::queue& stateQueue) { std::list> result; StateType const* currentState = stateInformation.reachableStates[stateIndex]; @@ -907,12 +705,17 @@ namespace storm { storm::ir::Update const& update = command.getUpdate(k); // Obtain target state index. - uint_fast64_t targetStateIndex = stateInformation.stateToIndexMap.at(applyUpdate(variableInformation, currentState, update)); + std::pair flagTargetStateIndexPair = getOrAddStateIndex(applyUpdate(variableInformation, currentState, update), stateInformation); + + // If the state has not been discovered yet, add it to the queue of states to be explored. + if (!flagTargetStateIndexPair.first) { + stateQueue.push(flagTargetStateIndexPair.second); + } // Update the choice by adding the probability/target state to it. double probabilityToAdd = update.getLikelihoodExpression()->getValueAsDouble(currentState); probabilitySum += probabilityToAdd; - addProbabilityToChoice(choice, targetStateIndex, probabilityToAdd, {update.getGlobalIndex()}); + addProbabilityToChoice(choice, flagTargetStateIndexPair.second, probabilityToAdd, {update.getGlobalIndex()}); } // Check that the resulting distribution is in fact a distribution. @@ -926,7 +729,7 @@ namespace storm { return result; } - static std::list> getLabeledTransitions(storm::ir::Program const& program, StateInformation const& stateInformation, VariableInformation const& variableInformation, uint_fast64_t stateIndex) { + static std::list> getLabeledTransitions(storm::ir::Program const& program, StateInformation& stateInformation, VariableInformation const& variableInformation, uint_fast64_t stateIndex, std::queue& stateQueue) { std::list> result; for (std::string const& action : program.getActions()) { @@ -997,10 +800,15 @@ namespace storm { } double probabilitySum = 0; - std::set labels; for (auto const& stateProbabilityPair : *newTargetStates) { - uint_fast64_t newStateIndex = stateInformation.stateToIndexMap.at(stateProbabilityPair.first); - addProbabilityToChoice(choice, newStateIndex, stateProbabilityPair.second, labels); + std::pair flagTargetStateIndexPair = getOrAddStateIndex(stateProbabilityPair.first, stateInformation); + + // If the state has not been discovered yet, add it to the queue of states to be explored. + if (!flagTargetStateIndexPair.first) { + stateQueue.push(flagTargetStateIndexPair.second); + } + + addProbabilityToChoice(choice, flagTargetStateIndexPair.second, stateProbabilityPair.second, std::set()); probabilitySum += stateProbabilityPair.second; } @@ -1035,18 +843,39 @@ namespace storm { } /*! + * Builds the transition matrix and the transition reward matrix based for the given program. * + * @param program The program for which to build the matrices. + * @param variableInformation A structure containing information about the variables in the program. + * @param transitionRewards A list of transition rewards that are to be considered in the transition reward + * matrix. + * @param stateInformation A structure containing information about the states of the program. + * @param deterministicModel A flag indicating whether the model is supposed to be deterministic or not. + * @param transitionMatrix A reference to an initialized matrix which is filled with all transitions by this + * function. + * @param transitionRewardMatrix A reference to an initialized matrix which is filled with all transition + * rewards by this function. + * @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 std::pair, std::vector>> buildMatrices(storm::ir::Program const& program, VariableInformation const& variableInformation, std::vector const& transitionRewards, StateInformation const& stateInformation, bool deterministicModel, storm::storage::SparseMatrix& transitionMatrix, storm::storage::SparseMatrix& transitionRewardMatrix) { - std::vector nondeterministicChoiceIndices(stateInformation.reachableStates.size() + 1); + static std::pair, std::vector>> buildMatrices(storm::ir::Program const& program, VariableInformation const& variableInformation, std::vector const& transitionRewards, StateInformation& stateInformation, bool deterministicModel, storm::storage::SparseMatrix& transitionMatrix, storm::storage::SparseMatrix& transitionRewardMatrix) { + std::vector nondeterministicChoiceIndices; std::vector> choiceLabels; - // Add transitions and rewards for all states. + // Initialize a queue and insert the initial state. + std::queue stateQueue; + StateType* initialState = getInitialState(program, variableInformation); + getOrAddStateIndex(initialState, stateInformation); + stateQueue.push(stateInformation.stateToIndexMap[initialState]); + + // Now explore the current state until there is no more reachable state. uint_fast64_t currentRow = 0; - for (uint_fast64_t currentState = 0; currentState < stateInformation.reachableStates.size(); ++currentState) { + while (!stateQueue.empty()) { + uint_fast64_t currentState = stateQueue.front(); + // Retrieve all choices for the current state. - std::list> allUnlabeledChoices = getUnlabeledTransitions(program, stateInformation, variableInformation, currentState); - std::list> allLabeledChoices = getLabeledTransitions(program, stateInformation, variableInformation, currentState); + std::list> allUnlabeledChoices = getUnlabeledTransitions(program, stateInformation, variableInformation, currentState, stateQueue); + std::list> allLabeledChoices = getLabeledTransitions(program, stateInformation, variableInformation, currentState, stateQueue); uint_fast64_t totalNumberOfChoices = allUnlabeledChoices.size() + allLabeledChoices.size(); @@ -1054,7 +883,10 @@ namespace storm { // requested and issue an error otherwise. if (totalNumberOfChoices == 0) { if (storm::settings::Settings::getInstance()->isSet("fixDeadlocks")) { - transitionMatrix.insertNextValue(currentRow, currentState, storm::utility::constGetOne()); + transitionMatrix.insertNextValue(currentRow, currentState, storm::utility::constGetOne(), true); + if (transitionRewards.size() > 0) { + transitionRewardMatrix.insertEmptyRow(true); + } ++currentRow; } else { LOG4CPLUS_ERROR(logger, "Error while creating sparse matrix from probabilistic program: found deadlock state. For fixing these, please provide the appropriate option."); @@ -1065,6 +897,7 @@ namespace storm { // or compose them to one choice. if (deterministicModel) { Choice globalChoice(""); + std::map stateToRewardMap; std::set allChoiceLabels; // Combine all the choices and scale them with the total number of choices of the current state. @@ -1072,28 +905,51 @@ namespace storm { globalChoice.addChoiceLabels(choice.getChoiceLabels()); for (auto const& stateProbabilityPair : choice) { globalChoice.getOrAddEntry(stateProbabilityPair.first) += stateProbabilityPair.second / totalNumberOfChoices; + + // Now add all rewards that match this choice. + for (auto const& transitionReward : transitionRewards) { + if (transitionReward.getActionName() == "" && transitionReward.getStatePredicate()->getValueAsBool(stateInformation.reachableStates.at(currentState))) { + stateToRewardMap[stateProbabilityPair.first] += ValueType(transitionReward.getRewardValue()->getValueAsDouble(stateInformation.reachableStates.at(currentState))); + } + } } } for (auto const& choice : allLabeledChoices) { globalChoice.addChoiceLabels(choice.getChoiceLabels()); for (auto const& stateProbabilityPair : choice) { globalChoice.getOrAddEntry(stateProbabilityPair.first) += stateProbabilityPair.second / totalNumberOfChoices; + + // Now add all rewards that match this choice. + for (auto const& transitionReward : transitionRewards) { + if (transitionReward.getActionName() == choice.getActionLabel() && transitionReward.getStatePredicate()->getValueAsBool(stateInformation.reachableStates.at(currentState))) { + stateToRewardMap[stateProbabilityPair.first] += ValueType(transitionReward.getRewardValue()->getValueAsDouble(stateInformation.reachableStates.at(currentState))); + } + } } } // Now add the resulting distribution as the only choice of the current state. - nondeterministicChoiceIndices[currentState] = currentRow; + nondeterministicChoiceIndices.push_back(currentRow); choiceLabels.push_back(globalChoice.getChoiceLabels()); for (auto const& stateProbabilityPair : globalChoice) { - transitionMatrix.insertNextValue(currentRow, stateProbabilityPair.first, stateProbabilityPair.second); + transitionMatrix.insertNextValue(currentRow, stateProbabilityPair.first, stateProbabilityPair.second, true); + } + + // Add all transition rewards to the matrix and add dummy entry if there is none. + if (stateToRewardMap.size() > 0) { + for (auto const& stateRewardPair : stateToRewardMap) { + transitionRewardMatrix.insertNextValue(currentRow, stateRewardPair.first, stateRewardPair.second, true); + } + } else if (transitionRewards.size() > 0) { + transitionRewardMatrix.insertEmptyRow(true); } ++currentRow; } else { // If the model is nondeterministic, we add all choices individually. - nondeterministicChoiceIndices[currentState] = currentRow; + nondeterministicChoiceIndices.push_back(currentRow); // First, process all unlabeled choices. for (auto const& choice : allUnlabeledChoices) { @@ -1101,7 +957,7 @@ namespace storm { choiceLabels.emplace_back(std::move(choice.getChoiceLabels())); for (auto const& stateProbabilityPair : choice) { - transitionMatrix.insertNextValue(currentRow, stateProbabilityPair.first, stateProbabilityPair.second); + transitionMatrix.insertNextValue(currentRow, stateProbabilityPair.first, stateProbabilityPair.second, true); // Now add all rewards that match this choice. for (auto const& transitionReward : transitionRewards) { @@ -1112,9 +968,13 @@ namespace storm { } - // Add all transition rewards to the matrix. - for (auto const& stateRewardPair : stateToRewardMap) { - transitionRewardMatrix.insertNextValue(currentRow, stateRewardPair.first, stateRewardPair.second); + // Add all transition rewards to the matrix and add dummy entry if there is none. + if (stateToRewardMap.size() > 0) { + for (auto const& stateRewardPair : stateToRewardMap) { + transitionRewardMatrix.insertNextValue(currentRow, stateRewardPair.first, stateRewardPair.second, true); + } + } else if (transitionRewards.size() > 0) { + transitionRewardMatrix.insertEmptyRow(true); } ++currentRow; @@ -1130,25 +990,31 @@ namespace storm { // Now add all rewards that match this choice. for (auto const& transitionReward : transitionRewards) { - if (transitionReward.getActionName() == "" && transitionReward.getStatePredicate()->getValueAsBool(stateInformation.reachableStates.at(currentState))) { + if (transitionReward.getActionName() == choice.getActionLabel() && transitionReward.getStatePredicate()->getValueAsBool(stateInformation.reachableStates.at(currentState))) { stateToRewardMap[stateProbabilityPair.first] += ValueType(transitionReward.getRewardValue()->getValueAsDouble(stateInformation.reachableStates.at(currentState))); } } } - // Add all transition rewards to the matrix. - for (auto const& stateRewardPair : stateToRewardMap) { - transitionRewardMatrix.insertNextValue(currentRow, stateRewardPair.first, stateRewardPair.second); + // Add all transition rewards to the matrix and add dummy entry if there is none. + if (stateToRewardMap.size() > 0) { + for (auto const& stateRewardPair : stateToRewardMap) { + transitionRewardMatrix.insertNextValue(currentRow, stateRewardPair.first, stateRewardPair.second, true); + } + } else if (transitionRewards.size() > 0) { + transitionRewardMatrix.insertEmptyRow(true); } ++currentRow; } } } + + stateQueue.pop(); } - nondeterministicChoiceIndices[stateInformation.reachableStates.size()] = currentRow; + nondeterministicChoiceIndices.push_back(currentRow); return std::make_pair(nondeterministicChoiceIndices, choiceLabels); } @@ -1166,38 +1032,28 @@ namespace storm { VariableInformation variableInformation = createVariableInformation(program); - // Start by exploring the state space. - StateInformation stateInformation = exploreReachableStateSpace(program, variableInformation); + // Initialize the matrices. + modelComponents.transitionMatrix.initialize(); + modelComponents.transitionRewardMatrix.initialize(); - // Then build the transition and reward matrices for the reachable states. - bool deterministicModel = program.getModelType() == storm::ir::Program::DTMC || program.getModelType() == storm::ir::Program::CTMC; - if (deterministicModel) { - modelComponents.transitionMatrix = storm::storage::SparseMatrix(stateInformation.reachableStates.size()); - modelComponents.transitionMatrix.initialize(); - modelComponents.transitionRewardMatrix = storm::storage::SparseMatrix(stateInformation.reachableStates.size()); - modelComponents.transitionRewardMatrix.initialize(); - } else { - uint_fast64_t totalNumberOfChoices = 0; - for (auto numberOfChoices : stateInformation.numberOfChoices) { - totalNumberOfChoices += numberOfChoices; - } - modelComponents.transitionMatrix = storm::storage::SparseMatrix(totalNumberOfChoices, stateInformation.reachableStates.size()); - modelComponents.transitionMatrix.initialize(); - modelComponents.transitionRewardMatrix = storm::storage::SparseMatrix(totalNumberOfChoices); - modelComponents.transitionRewardMatrix.initialize(); - } + // Create the structure for storing the reachable state space. + StateInformation stateInformation; // Get the selected reward model or create an empty one if none is selected. storm::ir::RewardModel const& rewardModel = rewardModelName != "" ? program.getRewardModel(rewardModelName) : storm::ir::RewardModel(); + // Determine whether we have to combine different choices to one or whether this model can have more than + // one choice per state. + bool deterministicModel = program.getModelType() == storm::ir::Program::DTMC || program.getModelType() == storm::ir::Program::CTMC; + // Build the transition and reward matrices. std::pair, std::vector>> nondeterministicChoiceIndicesAndChoiceLabelsPair = buildMatrices(program, variableInformation, rewardModel.getTransitionRewards(), stateInformation, deterministicModel, modelComponents.transitionMatrix, modelComponents.transitionRewardMatrix); modelComponents.nondeterministicChoiceIndices = std::move(nondeterministicChoiceIndicesAndChoiceLabelsPair.first); modelComponents.choiceLabeling = std::move(nondeterministicChoiceIndicesAndChoiceLabelsPair.second); // Finalize the resulting matrices. - modelComponents.transitionMatrix.finalize(); - modelComponents.transitionRewardMatrix.finalize(); + modelComponents.transitionMatrix.finalize(true); + modelComponents.transitionRewardMatrix.finalize(true); // Now build the state labeling. modelComponents.stateLabeling = buildStateLabeling(program, variableInformation, stateInformation); @@ -1213,6 +1069,14 @@ namespace storm { return modelComponents; } + /*! + * Builds the state labeling for the given program. + * + * @param program The program for which to build the state labeling. + * @param variableInformation Information about the variables in the program. + * @param stateInformation Information about the state space of the program. + * @return The state labeling of the given program. + */ static storm::models::AtomicPropositionsLabeling buildStateLabeling(storm::ir::Program const& program, VariableInformation const& variableInformation, StateInformation const& stateInformation) { std::map> const& labels = program.getLabels(); @@ -1241,6 +1105,13 @@ namespace storm { return result; } + /*! + * Builds the state rewards for the given state space. + * + * @param rewards A vector of state rewards to consider. + * @param stateInformation Information about the state space. + * @return A vector containing the state rewards for the state space. + */ static std::vector buildStateRewards(std::vector const& rewards, StateInformation const& stateInformation) { std::vector result(stateInformation.reachableStates.size()); for (uint_fast64_t index = 0; index < stateInformation.reachableStates.size(); index++) { diff --git a/src/counterexamples/MinimalLabelSetGenerator.h b/src/counterexamples/MILPMinimalLabelSetGenerator.h similarity index 99% rename from src/counterexamples/MinimalLabelSetGenerator.h rename to src/counterexamples/MILPMinimalLabelSetGenerator.h index 9fe8844ea..611da0f7e 100644 --- a/src/counterexamples/MinimalLabelSetGenerator.h +++ b/src/counterexamples/MILPMinimalLabelSetGenerator.h @@ -1,14 +1,14 @@ /* - * MinimalLabelSetGenerator.h + * MILPMinimalLabelSetGenerator.h * * Created on: 15.09.2013 * Author: Christian Dehnert */ -#ifndef STORM_COUNTEREXAMPLES_MINIMALCOMMANDSETGENERATOR_MDP_H_ -#define STORM_COUNTEREXAMPLES_MINIMALCOMMANDSETGENERATOR_MDP_H_ +#ifndef STORM_COUNTEREXAMPLES_MILPMINIMALLABELSETGENERATOR_MDP_H_ +#define STORM_COUNTEREXAMPLES_MILPMINIMALLABELSETGENERATOR_MDP_H_ -// To detect whether the usage of Gurobi is possible, this include is neccessary +// To detect whether the usage of Gurobi is possible, this include is neccessary. #include "storm-config.h" #ifdef STORM_HAVE_GUROBI @@ -1258,7 +1258,7 @@ namespace storm { }; - } -} + } // namespace counterexamples +} // namespace storm -#endif /* STORM_COUNTEREXAMPLES_MINIMALLABELSETGENERATOR_MDP_H_ */ +#endif /* STORM_COUNTEREXAMPLES_MILPMINIMALLABELSETGENERATOR_MDP_H_ */ diff --git a/src/counterexamples/SMTMinimalCommandSetGenerator.h b/src/counterexamples/SMTMinimalCommandSetGenerator.h new file mode 100644 index 000000000..4608f4e8e --- /dev/null +++ b/src/counterexamples/SMTMinimalCommandSetGenerator.h @@ -0,0 +1,50 @@ +/* + * SMTMinimalCommandSetGenerator.h + * + * Created on: 01.10.2013 + * Author: Christian Dehnert + */ + +#ifndef STORM_COUNTEREXAMPLES_SMTMINIMALCOMMANDSETGENERATOR_MDP_H_ +#define STORM_COUNTEREXAMPLES_SMTMINIMALCOMMANDSETGENERATOR_MDP_H_ + +// To detect whether the usage of Z3 is possible, this include is neccessary. +#include "storm-config.h" + +namespace storm { + namespace counterexamples { + + /*! + * This class provides functionality to generate a minimal counterexample to a probabilistic reachability + * property in terms of used labels. + */ + template + class MinimalLabelSetGenerator { +#ifdef STORM_HAVE_Z3 + private: + +#endif + + public: + static std::unordered_set getMinimalCommandSet(storm::ir::Program const& program, storm::models::Mdp const& labeledMdp, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, double probabilityThreshold, bool checkThresholdFeasible = false) { +#ifdef STORM_HAVE_Z3 + // (0) Check whether the MDP is indeed labeled. + if (!labeledMdp.hasChoiceLabels()) { + throw storm::exceptions::InvalidArgumentException() << "Minimal command set generation is impossible for unlabeled model."; + } + + + + return std::unordered_set(); + +#else + throw storm::exceptions::NotImplementedException() << "This functionality is unavailable since StoRM has been compiled without support for Z3."; +#endif + } + + } + + } // namespace counterexamples +} // namespace storm + +#endif /* STORM_COUNTEREXAMPLES_SMTMINIMALCOMMANDSETGENERATOR_MDP_H_ */ diff --git a/src/models/AbstractNondeterministicModel.h b/src/models/AbstractNondeterministicModel.h index bb6b0fd37..c4569473f 100644 --- a/src/models/AbstractNondeterministicModel.h +++ b/src/models/AbstractNondeterministicModel.h @@ -6,246 +6,241 @@ #include namespace storm { - -namespace models { - -/*! - * @brief Base class for all non-deterministic model classes. - * - * This is base class defines a common interface for all non-deterministic models. - */ -template -class AbstractNondeterministicModel: public AbstractModel { - - public: - /*! Constructs an abstract non-determinstic model from the given parameters. - * All values are copied. - * @param transitionMatrix The matrix representing the transitions in the model. - * @param stateLabeling The labeling that assigns a set of atomic - * propositions to each state. - * @param choiceIndices A mapping from states to rows in the transition matrix. - * @param stateRewardVector The reward values associated with the states. - * @param transitionRewardMatrix The reward values associated with the transitions of the model. - * @param optionalChoiceLabeling A vector that represents the labels associated with the choices of each state. - */ - AbstractNondeterministicModel( - storm::storage::SparseMatrix const& transitionMatrix, - storm::models::AtomicPropositionsLabeling const& stateLabeling, - std::vector const& nondeterministicChoiceIndices, - boost::optional> const& optionalStateRewardVector, - boost::optional> const& optionalTransitionRewardMatrix, - boost::optional>> const& optionalChoiceLabeling) + namespace models { + + /*! + * @brief Base class for all non-deterministic model classes. + * + * This is base class defines a common interface for all non-deterministic models. + */ + template + class AbstractNondeterministicModel: public AbstractModel { + + public: + /*! Constructs an abstract non-determinstic model from the given parameters. + * All values are copied. + * @param transitionMatrix The matrix representing the transitions in the model. + * @param stateLabeling The labeling that assigns a set of atomic + * propositions to each state. + * @param choiceIndices A mapping from states to rows in the transition matrix. + * @param stateRewardVector The reward values associated with the states. + * @param transitionRewardMatrix The reward values associated with the transitions of the model. + * @param optionalChoiceLabeling A vector that represents the labels associated with the choices of each state. + */ + AbstractNondeterministicModel(storm::storage::SparseMatrix const& transitionMatrix, + storm::models::AtomicPropositionsLabeling const& stateLabeling, + std::vector const& nondeterministicChoiceIndices, + boost::optional> const& optionalStateRewardVector, + boost::optional> const& optionalTransitionRewardMatrix, + boost::optional>> const& optionalChoiceLabeling) : AbstractModel(transitionMatrix, stateLabeling, optionalStateRewardVector, optionalTransitionRewardMatrix, optionalChoiceLabeling) { this->nondeterministicChoiceIndices = nondeterministicChoiceIndices; - } - - /*! Constructs an abstract non-determinstic model from the given parameters. - * All values are moved. - * @param transitionMatrix The matrix representing the transitions in the model. - * @param stateLabeling The labeling that assigns a set of atomic - * propositions to each state. - * @param choiceIndices A mapping from states to rows in the transition matrix. - * @param stateRewardVector The reward values associated with the states. - * @param transitionRewardMatrix The reward values associated with the transitions of the model. - */ - AbstractNondeterministicModel( - storm::storage::SparseMatrix&& transitionMatrix, - storm::models::AtomicPropositionsLabeling&& stateLabeling, - std::vector&& nondeterministicChoiceIndices, - boost::optional>&& optionalStateRewardVector, - boost::optional>&& optionalTransitionRewardMatrix, - boost::optional>>&& optionalChoiceLabeling) - // The std::move call must be repeated here because otherwise this calls the copy constructor of the Base Class - : AbstractModel(std::move(transitionMatrix), std::move(stateLabeling), std::move(optionalStateRewardVector), std::move(optionalTransitionRewardMatrix), + } + + /*! Constructs an abstract non-determinstic model from the given parameters. + * All values are moved. + * @param transitionMatrix The matrix representing the transitions in the model. + * @param stateLabeling The labeling that assigns a set of atomic + * propositions to each state. + * @param choiceIndices A mapping from states to rows in the transition matrix. + * @param stateRewardVector The reward values associated with the states. + * @param transitionRewardMatrix The reward values associated with the transitions of the model. + */ + AbstractNondeterministicModel(storm::storage::SparseMatrix&& transitionMatrix, + storm::models::AtomicPropositionsLabeling&& stateLabeling, + std::vector&& nondeterministicChoiceIndices, + boost::optional>&& optionalStateRewardVector, + boost::optional>&& optionalTransitionRewardMatrix, + boost::optional>>&& optionalChoiceLabeling) + // The std::move call must be repeated here because otherwise this calls the copy constructor of the Base Class + : AbstractModel(std::move(transitionMatrix), std::move(stateLabeling), std::move(optionalStateRewardVector), std::move(optionalTransitionRewardMatrix), std::move(optionalChoiceLabeling)), nondeterministicChoiceIndices(std::move(nondeterministicChoiceIndices)) { - // Intentionally left empty. - } - - /*! - * Destructor. - */ - virtual ~AbstractNondeterministicModel() { - // Intentionally left empty. - } - - /*! - * Copy Constructor. - */ - AbstractNondeterministicModel(AbstractNondeterministicModel const& other) : AbstractModel(other), - nondeterministicChoiceIndices(other.nondeterministicChoiceIndices) { - // Intentionally left empty. - } - - /*! - * Move Constructor. - */ - AbstractNondeterministicModel(AbstractNondeterministicModel&& other) : AbstractModel(std::move(other)), - nondeterministicChoiceIndices(std::move(other.nondeterministicChoiceIndices)) { - // Intentionally left empty. - } - - /*! - * Returns the number of choices for all states of the MDP. - * @return The number of choices for all states of the MDP. - */ - uint_fast64_t getNumberOfChoices() const { - return this->transitionMatrix.getRowCount(); - } - - /*! - * Retrieves the size of the internal representation of the model in memory. - * @return the size of the internal representation of the model in memory - * measured in bytes. - */ - virtual uint_fast64_t getSizeInMemory() const { - return AbstractModel::getSizeInMemory() + nondeterministicChoiceIndices.size() * sizeof(uint_fast64_t); - } - - /*! - * Retrieves the vector indicating which matrix rows represent non-deterministic choices - * of a certain state. - * @param the vector indicating which matrix rows represent non-deterministic choices - * of a certain state. - */ - std::vector const& getNondeterministicChoiceIndices() const { - return nondeterministicChoiceIndices; - } - - virtual typename storm::storage::SparseMatrix::Rows getRows(uint_fast64_t state) const override { - return this->transitionMatrix.getRows(nondeterministicChoiceIndices[state], nondeterministicChoiceIndices[state + 1] - 1); - } - - virtual typename storm::storage::SparseMatrix::ConstRowIterator rowIteratorBegin(uint_fast64_t state) const override { - return this->transitionMatrix.begin(nondeterministicChoiceIndices[state]); - } + // Intentionally left empty. + } + + /*! + * Destructor. + */ + virtual ~AbstractNondeterministicModel() { + // Intentionally left empty. + } + + /*! + * Copy Constructor. + */ + AbstractNondeterministicModel(AbstractNondeterministicModel const& other) : AbstractModel(other), + nondeterministicChoiceIndices(other.nondeterministicChoiceIndices) { + // Intentionally left empty. + } + + /*! + * Move Constructor. + */ + AbstractNondeterministicModel(AbstractNondeterministicModel&& other) : AbstractModel(std::move(other)), + nondeterministicChoiceIndices(std::move(other.nondeterministicChoiceIndices)) { + // Intentionally left empty. + } + + /*! + * Returns the number of choices for all states of the MDP. + * @return The number of choices for all states of the MDP. + */ + uint_fast64_t getNumberOfChoices() const { + return this->transitionMatrix.getRowCount(); + } + + /*! + * Retrieves the size of the internal representation of the model in memory. + * + * @return the size of the internal representation of the model in memory + * measured in bytes. + */ + virtual uint_fast64_t getSizeInMemory() const { + return AbstractModel::getSizeInMemory() + nondeterministicChoiceIndices.size() * sizeof(uint_fast64_t); + } + + /*! + * Retrieves the vector indicating which matrix rows represent non-deterministic choices + * of a certain state. + * @param the vector indicating which matrix rows represent non-deterministic choices + * of a certain state. + */ + std::vector const& getNondeterministicChoiceIndices() const { + return nondeterministicChoiceIndices; + } + + virtual typename storm::storage::SparseMatrix::Rows getRows(uint_fast64_t state) const override { + return this->transitionMatrix.getRows(nondeterministicChoiceIndices[state], nondeterministicChoiceIndices[state + 1] - 1); + } + + virtual typename storm::storage::SparseMatrix::ConstRowIterator rowIteratorBegin(uint_fast64_t state) const override { + return this->transitionMatrix.begin(nondeterministicChoiceIndices[state]); + } - virtual typename storm::storage::SparseMatrix::ConstRowIterator rowIteratorEnd(uint_fast64_t state) const override { + virtual typename storm::storage::SparseMatrix::ConstRowIterator rowIteratorEnd(uint_fast64_t state) const override { return this->transitionMatrix.end(nondeterministicChoiceIndices[state + 1] - 1); - } + } - /*! - * Calculates a hash over all values contained in this Model. - * @return size_t A Hash Value - */ - virtual size_t getHash() const override { - std::size_t result = 0; - std::size_t hashTmp = storm::utility::Hash::getHash(nondeterministicChoiceIndices); - std::cout << "nondeterministicChoiceIndices Hash: " << hashTmp << std::endl; + /*! + * Calculates a hash over all values contained in this Model. + * @return size_t A Hash Value + */ + virtual size_t getHash() const override { + std::size_t result = 0; + std::size_t hashTmp = storm::utility::Hash::getHash(nondeterministicChoiceIndices); + boost::hash_combine(result, AbstractModel::getHash()); + boost::hash_combine(result, hashTmp); + return result; + } - boost::hash_combine(result, AbstractModel::getHash()); - boost::hash_combine(result, hashTmp); - return result; - } + /*! + * Prints information about the model to the specified stream. + * @param out The stream the information is to be printed to. + */ + virtual void printModelInformationToStream(std::ostream& out) const override { + out << "-------------------------------------------------------------- " << std::endl; + out << "Model type: \t\t" << this->getType() << std::endl; + out << "States: \t\t" << this->getNumberOfStates() << std::endl; + out << "Transitions: \t\t" << this->getNumberOfTransitions() << std::endl; + out << "Choices: \t\t" << this->getNumberOfChoices() << std::endl; + this->getStateLabeling().printAtomicPropositionsInformationToStream(out); + out << "Size in memory: \t" << (this->getSizeInMemory())/1024 << " kbytes" << std::endl; + out << "-------------------------------------------------------------- " << std::endl; + } - /*! - * Prints information about the model to the specified stream. - * @param out The stream the information is to be printed to. - */ - virtual void printModelInformationToStream(std::ostream& out) const override { - out << "-------------------------------------------------------------- " << std::endl; - out << "Model type: \t\t" << this->getType() << std::endl; - out << "States: \t\t" << this->getNumberOfStates() << std::endl; - out << "Transitions: \t\t" << this->getNumberOfTransitions() << std::endl; - out << "Choices: \t\t" << this->getNumberOfChoices() << std::endl; - this->getStateLabeling().printAtomicPropositionsInformationToStream(out); - out << "Size in memory: \t" << (this->getSizeInMemory())/1024 << " kbytes" << std::endl; - out << "-------------------------------------------------------------- " << std::endl; - } + virtual void writeDotToStream(std::ostream& outStream, bool includeLabeling = true, storm::storage::BitVector const* subsystem = nullptr, std::vector const* firstValue = nullptr, std::vector const* secondValue = nullptr, std::vector const* stateColoring = nullptr, std::vector const* colors = nullptr, std::vector* scheduler = nullptr, bool finalizeOutput = true) const override { + AbstractModel::writeDotToStream(outStream, includeLabeling, subsystem, firstValue, secondValue, stateColoring, colors, scheduler, false); - virtual void writeDotToStream(std::ostream& outStream, bool includeLabeling = true, storm::storage::BitVector const* subsystem = nullptr, std::vector const* firstValue = nullptr, std::vector const* secondValue = nullptr, std::vector const* stateColoring = nullptr, std::vector const* colors = nullptr, std::vector* scheduler = nullptr, bool finalizeOutput = true) const override { - AbstractModel::writeDotToStream(outStream, includeLabeling, subsystem, firstValue, secondValue, stateColoring, colors, scheduler, false); - - // Write the probability distributions for all the states. - auto rowIt = this->transitionMatrix.begin(); - for (uint_fast64_t state = 0, highestStateIndex = this->getNumberOfStates() - 1; state <= highestStateIndex; ++state) { - uint_fast64_t rowCount = nondeterministicChoiceIndices[state + 1] - nondeterministicChoiceIndices[state]; - bool highlightChoice = true; - - // For this, we need to iterate over all available nondeterministic choices in the current state. - for (uint_fast64_t row = 0; row < rowCount; ++row, ++rowIt) { - if (scheduler != nullptr) { - // If the scheduler picked the current choice, we will not make it dotted, but highlight it. - if ((*scheduler)[state] == row) { - highlightChoice = true; - } else { - highlightChoice = false; - } - } - - // For each nondeterministic choice, we draw an arrow to an intermediate node to better display - // the grouping of transitions. - outStream << "\t\"" << state << "c" << row << "\" [shape = \"point\""; - - // If we were given a scheduler to highlight, we do so now. - if (scheduler != nullptr) { - if (highlightChoice) { - outStream << ", fillcolor=\"red\""; + // Write the probability distributions for all the states. + auto rowIt = this->transitionMatrix.begin(); + for (uint_fast64_t state = 0, highestStateIndex = this->getNumberOfStates() - 1; state <= highestStateIndex; ++state) { + uint_fast64_t rowCount = nondeterministicChoiceIndices[state + 1] - nondeterministicChoiceIndices[state]; + bool highlightChoice = true; + + // For this, we need to iterate over all available nondeterministic choices in the current state. + for (uint_fast64_t row = 0; row < rowCount; ++row, ++rowIt) { + if (scheduler != nullptr) { + // If the scheduler picked the current choice, we will not make it dotted, but highlight it. + if ((*scheduler)[state] == row) { + highlightChoice = true; + } else { + highlightChoice = false; + } } - } - outStream << "];" << std::endl; - - outStream << "\t" << state << " -> \"" << state << "c" << row << "\""; - - // If we were given a scheduler to highlight, we do so now. - if (scheduler != nullptr) { - if (highlightChoice) { - outStream << " [color=\"red\", penwidth = 2]"; - } else { - outStream << " [style = \"dotted\"]"; + + // For each nondeterministic choice, we draw an arrow to an intermediate node to better display + // the grouping of transitions. + outStream << "\t\"" << state << "c" << row << "\" [shape = \"point\""; + + // If we were given a scheduler to highlight, we do so now. + if (scheduler != nullptr) { + if (highlightChoice) { + outStream << ", fillcolor=\"red\""; + } } - } - outStream << ";" << std::endl; - - // Now draw all probabilitic arcs that belong to this nondeterminstic choice. - for (auto transitionIt = rowIt.begin(), transitionIte = rowIt.end(); transitionIt != transitionIte; ++transitionIt) { - if (subsystem == nullptr || subsystem->get(transitionIt.column())) { - outStream << "\t\"" << state << "c" << row << "\" -> " << transitionIt.column() << " [ label= \"" << transitionIt.value() << "\" ]"; + outStream << "];" << std::endl; - // If we were given a scheduler to highlight, we do so now. - if (scheduler != nullptr) { - if (highlightChoice) { - outStream << " [color=\"red\", penwidth = 2]"; - } else { - outStream << " [style = \"dotted\"]"; + outStream << "\t" << state << " -> \"" << state << "c" << row << "\""; + + // If we were given a scheduler to highlight, we do so now. + if (scheduler != nullptr) { + if (highlightChoice) { + outStream << " [color=\"red\", penwidth = 2]"; + } else { + outStream << " [style = \"dotted\"]"; + } + } + outStream << ";" << std::endl; + + // Now draw all probabilitic arcs that belong to this nondeterminstic choice. + for (auto transitionIt = rowIt.begin(), transitionIte = rowIt.end(); transitionIt != transitionIte; ++transitionIt) { + if (subsystem == nullptr || subsystem->get(transitionIt.column())) { + outStream << "\t\"" << state << "c" << row << "\" -> " << transitionIt.column() << " [ label= \"" << transitionIt.value() << "\" ]"; + + // If we were given a scheduler to highlight, we do so now. + if (scheduler != nullptr) { + if (highlightChoice) { + outStream << " [color=\"red\", penwidth = 2]"; + } else { + outStream << " [style = \"dotted\"]"; + } } + outStream << ";" << std::endl; } - outStream << ";" << std::endl; } } } + + if (finalizeOutput) { + outStream << "}" << std::endl; + } } - - if (finalizeOutput) { - outStream << "}" << std::endl; - } - } - - /*! - * Assigns this model a new set of choiceLabels, giving each choice a label with the stateId - * @return void - */ - virtual void setStateIdBasedChoiceLabeling() override { - std::vector> newChoiceLabeling; - - size_t stateCount = this->getNumberOfStates(); - size_t choiceCount = this->getNumberOfChoices(); - newChoiceLabeling.resize(choiceCount); - - for (size_t state = 0; state < stateCount; ++state) { - for (size_t choice = this->nondeterministicChoiceIndices.at(state); choice < this->nondeterministicChoiceIndices.at(state + 1); ++choice) { - newChoiceLabeling.at(choice).insert(state); - } - } - - this->choiceLabeling.reset(newChoiceLabeling); - } - private: - /*! A vector of indices mapping states to the choices (rows) in the transition matrix. */ - std::vector nondeterministicChoiceIndices; -}; - -} // namespace models + /*! + * Assigns this model a new set of choiceLabels, giving each choice a label with the stateId + * @return void + */ + virtual void setStateIdBasedChoiceLabeling() override { + std::vector> newChoiceLabeling; + + size_t stateCount = this->getNumberOfStates(); + size_t choiceCount = this->getNumberOfChoices(); + newChoiceLabeling.resize(choiceCount); + + for (size_t state = 0; state < stateCount; ++state) { + for (size_t choice = this->nondeterministicChoiceIndices.at(state); choice < this->nondeterministicChoiceIndices.at(state + 1); ++choice) { + newChoiceLabeling.at(choice).insert(state); + } + } + + this->choiceLabeling.reset(newChoiceLabeling); + } + + private: + /*! A vector of indices mapping states to the choices (rows) in the transition matrix. */ + std::vector nondeterministicChoiceIndices; + }; + } // namespace models } // namespace storm #endif /* STORM_MODELS_ABSTRACTDETERMINISTICMODEL_H_ */ diff --git a/src/models/Dtmc.h b/src/models/Dtmc.h index 849a42344..7b012803d 100644 --- a/src/models/Dtmc.h +++ b/src/models/Dtmc.h @@ -50,7 +50,7 @@ public: throw storm::exceptions::InvalidArgumentException() << "Probability matrix is invalid."; } if (this->hasTransitionRewards()) { - if (!this->getTransitionRewardMatrix().containsAllPositionsOf(this->getTransitionMatrix())) { + if (!this->getTransitionRewardMatrix().isSubmatrixOf(this->getTransitionMatrix())) { LOG4CPLUS_ERROR(logger, "Transition reward matrix is not a submatrix of the transition matrix, i.e. there are rewards for transitions that do not exist."); throw storm::exceptions::InvalidArgumentException() << "There are transition rewards for nonexistent transitions."; } @@ -78,7 +78,7 @@ public: throw storm::exceptions::InvalidArgumentException() << "Probability matrix is invalid."; } if (this->hasTransitionRewards()) { - if (!this->getTransitionRewardMatrix().containsAllPositionsOf(this->getTransitionMatrix())) { + if (!this->getTransitionRewardMatrix().isSubmatrixOf(this->getTransitionMatrix())) { LOG4CPLUS_ERROR(logger, "Transition reward matrix is not a submatrix of the transition matrix, i.e. there are rewards for transitions that do not exist."); throw storm::exceptions::InvalidArgumentException() << "There are transition rewards for nonexistent transitions."; } diff --git a/src/models/Mdp.h b/src/models/Mdp.h index cb988c90b..9523132b0 100644 --- a/src/models/Mdp.h +++ b/src/models/Mdp.h @@ -54,6 +54,12 @@ public: LOG4CPLUS_ERROR(logger, "Probability matrix is invalid."); throw storm::exceptions::InvalidArgumentException() << "Probability matrix is invalid."; } + if (this->hasTransitionRewards()) { + if (!this->getTransitionRewardMatrix().isSubmatrixOf(this->getTransitionMatrix())) { + LOG4CPLUS_ERROR(logger, "Transition reward matrix is not a submatrix of the transition matrix, i.e. there are rewards for transitions that do not exist."); + throw storm::exceptions::InvalidArgumentException() << "There are transition rewards for nonexistent transitions."; + } + } } /*! @@ -78,6 +84,12 @@ public: LOG4CPLUS_ERROR(logger, "Probability matrix is invalid."); throw storm::exceptions::InvalidArgumentException() << "Probability matrix is invalid."; } + if (this->hasTransitionRewards()) { + if (!this->getTransitionRewardMatrix().isSubmatrixOf(this->getTransitionMatrix())) { + LOG4CPLUS_ERROR(logger, "Transition reward matrix is not a submatrix of the transition matrix, i.e. there are rewards for transitions that do not exist."); + throw storm::exceptions::InvalidArgumentException() << "There are transition rewards for nonexistent transitions."; + } + } } /*! @@ -113,6 +125,26 @@ public: return MDP; } +// /*! +// * Constructs an MDP by copying the given MDP and restricting the choices of each state to the ones whose label set +// * is contained in the given label set. +// * +// * @param originalModel The model to restrict. +// * @param enabledChoiceLabels A set of labels that determines which choices of the original model can be taken +// * and which ones need to be ignored. +// */ +// Mdp restrictChoiceLabels(Mdp const& originalModel, std::set const& enabledChoiceLabels) { +// // Only perform this operation if the given model has choice labels. +// if (!originalModel.hasChoiceLabels()) { +// throw storm::exceptions::InvalidArgumentException() << "Restriction to label set is impossible for unlabeled model."; +// } +// +// storm::storage::SparseMatrix transitionMatrix(); +// +// Mdp result; +// return result; +// } + /*! * Calculates a hash over all values contained in this Model. * @return size_t A Hash Value @@ -120,6 +152,7 @@ public: virtual std::size_t getHash() const override { return AbstractNondeterministicModel::getHash(); } + private: /*! diff --git a/src/storage/SparseMatrix.h b/src/storage/SparseMatrix.h index 728ac1265..0623090ac 100644 --- a/src/storage/SparseMatrix.h +++ b/src/storage/SparseMatrix.h @@ -401,10 +401,6 @@ public: triggerErrorState(); LOG4CPLUS_ERROR(logger, "Trying to initialize matrix that is not uninitialized."); throw storm::exceptions::InvalidStateException("Trying to initialize matrix that is not uninitialized."); - } else if ((rowCount == 0) || (colCount == 0)) { - triggerErrorState(); - LOG4CPLUS_ERROR(logger, "Trying to create initialize a matrix with 0 rows or 0 columns."); - throw storm::exceptions::InvalidArgumentException("Trying to create initialize a matrix with 0 rows or 0 columns."); } else if ((rowCount * colCount) < nonZeroEntries) { triggerErrorState(); LOG4CPLUS_ERROR(logger, "Trying to initialize a matrix with more non-zero entries than there can be."); @@ -426,7 +422,7 @@ public: /*! * Sets the matrix element at the given row and column to the given value. After all elements have been added, - * a call to finalize() is mandatory. + * a call to finalize(false) is mandatory. * NOTE: This is a linear setter. It must be called consecutively for each element, * row by row *and* column by column. * NOTE: This method is different from insertNextValue(...) in that the number of nonzero elements must be known @@ -464,7 +460,7 @@ public: /*! * Inserts a value at the given row and column with the given value. After all elements have been inserted, - * a call to finalize() is mandatory. + * a call to finalize(true) is mandatory. * NOTE: This is a linear inserter. It must be called consecutively for each element, row by row *and* column by * column. * NOTE: This method is different from addNextValue(...) in that the number of nonzero elements need not be known @@ -473,22 +469,29 @@ public: * @param row The row in which the matrix element is to be set. * @param col The column in which the matrix element is to be set. * @param value The value that is to be set. + * @param pushRowIndication If set to true, the next row indication value is pushed, otherwise it is added. If the + * number of rows was not set in the beginning, then this needs to be true and false otherwise. */ - void insertNextValue(const uint_fast64_t row, const uint_fast64_t col, T const& value) { + void insertNextValue(const uint_fast64_t row, const uint_fast64_t col, T const& value, bool pushRowIndication = false) { // Check whether the given row and column positions are valid and throw // error otherwise. - if ((row > rowCount) || (col > colCount)) { + if (row < lastRow) { triggerErrorState(); - LOG4CPLUS_ERROR(logger, "Trying to insert a value at illegal position (" << row << ", " << col << ") in matrix of size (" << rowCount << ", " << colCount << ")."); - throw storm::exceptions::OutOfRangeException() << "Trying to insert a value at illegal position (" << row << ", " << col << ") in matrix of size (" << rowCount << ", " << colCount << ")."; + LOG4CPLUS_ERROR(logger, "Trying to insert a value at illegal position (" << row << ", " << col << ")."); + throw storm::exceptions::OutOfRangeException() << "Trying to insert a value at illegal position (" << row << ", " << col << ")."; } // If we switched to another row, we have to adjust the missing entries in the rowIndications array. if (row != lastRow) { for (uint_fast64_t i = lastRow + 1; i <= row; ++i) { - rowIndications[i] = currentSize; + if (pushRowIndication) { + rowIndications.push_back(currentSize); + } else { + rowIndications[i] = currentSize; + } } - lastRow = row; + rowCount = row + 1; + lastRow = row; } // Finally, set the element and increase the current size. @@ -496,14 +499,33 @@ public: columnIndications.push_back(col); ++nonZeroEntryCount; ++currentSize; + + // Check that we also have the correct number of columns. + colCount = std::max(colCount, col + 1); } - - + + /*! + * Inserts an empty row in the matrix. + * + * @param pushRowIndication If set to true, the next row indication value is pushed, otherwise it is added. If the + * number of rows was not set in the beginning, then this needs to be true and false otherwise. + */ + void insertEmptyRow(bool pushRowIndication = false) { + if (pushRowIndication) { + rowIndications.push_back(currentSize); + } else { + rowIndications[lastRow + 1] = currentSize; + } + + ++rowCount; + ++lastRow; + } + /* * Finalizes the sparse matrix to indicate that initialization has been completed and the matrix may now be used. * * @param pushSentinelElement A boolean flag that indicates whether the sentinel element is to be pushed or inserted - * at a fixed location. If the elements have been added to the matrix via insertNextElement, this needs to be true + * at a fixed location. If the elements have been added to the matrix via insertNextValue, this needs to be true * and false otherwise. */ void finalize(bool pushSentinelElement = false) { @@ -519,10 +541,8 @@ public: } else { // Fill in the missing entries in the row_indications array. // (Can happen because of empty rows at the end.) - if (lastRow != rowCount) { - for (uint_fast64_t i = lastRow + 1; i < rowCount; ++i) { - rowIndications[i] = currentSize; - } + for (uint_fast64_t i = lastRow + 1; i < rowCount; ++i) { + rowIndications[i] = currentSize; } // Set a sentinel element at the last position of the row_indications array. This eases iteration work, as @@ -1308,18 +1328,18 @@ public: } /*! - * Checks if the given matrix is a submatrix of the current matrix, where A matrix A is called a + * Checks if the current matrix is a submatrix of the given matrix, where a matrix A is called a * submatrix of B if a value in A is only nonzero, if the value in B at the same position is - * also nonzero. Furthermore, A and B have to have the same size. + * also nonzero. Additionally, the matrices must be of equal size. * - * @param matrix The matrix that is possibly a submatrix of the current matrix. - * @returns True iff the given matrix is a submatrix of the current matrix. + * @param matrix The matrix that possibly is a "supermatrix" of the current matrix. + * @returns True iff the current matrix is a submatrix of the given matrix. */ - bool containsAllPositionsOf(SparseMatrix const& matrix) const { - // Check for mismatching sizes. - if (this->getRowCount() != matrix.getRowCount()) return false; - if (this->getColumnCount() != matrix.getColumnCount()) return false; - + bool isSubmatrixOf(SparseMatrix const& matrix) const { + // Check for matching sizes. + if (this->getRowCount() != matrix.getRowCount()) return false; + if (this->getColumnCount() != matrix.getColumnCount()) return false; + // Check the subset property for all rows individually. for (uint_fast64_t row = 0; row < this->getRowCount(); ++row) { for (uint_fast64_t elem = rowIndications[row], elem2 = matrix.rowIndications[row]; elem < rowIndications[row + 1] && elem < matrix.rowIndications[row + 1]; ++elem) { @@ -1328,7 +1348,9 @@ public: while (elem2 < matrix.rowIndications[row + 1] && matrix.columnIndications[elem2] < columnIndications[elem]) { ++elem2; } - if (!(elem2 < matrix.rowIndications[row + 1]) || columnIndications[elem] != matrix.columnIndications[elem2]) return false; + if (!(elem2 < matrix.rowIndications[row + 1]) || columnIndications[elem] != matrix.columnIndications[elem2]) { + return false; + } } } return true; @@ -1501,8 +1523,9 @@ private: } /*! - * Prepares the internal storage. For this, it requires the number of non-zero entries and the - * amount of rows to be set correctly. + * Prepares the internal storage. It relies on the number of non-zero entries and the + * amount of rows to be set correctly. They may, however, be zero, but then insertNextValue needs to be used rather + * than addNextElement for filling the matrix. * * @param initializeElements If set to true, all entries are initialized. * @return True on success, false otherwise (allocation failed). diff --git a/src/storm.cpp b/src/storm.cpp index 19ec8baee..39497409a 100644 --- a/src/storm.cpp +++ b/src/storm.cpp @@ -26,7 +26,7 @@ #include "src/modelchecker/prctl/SparseMdpPrctlModelChecker.h" #include "src/solver/GmmxxLinearEquationSolver.h" #include "src/solver/GmmxxNondeterministicLinearEquationSolver.h" -#include "src/counterexamples/MinimalLabelSetGenerator.h" +#include "src/counterexamples/MILPMinimalLabelSetGenerator.h" #include "src/parser/AutoParser.h" #include "src/parser/PrctlParser.h" #include "src/utility/ErrorHandling.h" diff --git a/test/functional/parser/ParsePrismTest.cpp b/test/functional/parser/ParsePrismTest.cpp index 63eca2d31..0a8abb420 100644 --- a/test/functional/parser/ParsePrismTest.cpp +++ b/test/functional/parser/ParsePrismTest.cpp @@ -24,7 +24,7 @@ TEST(ParsePrismTest, parseTwoDice) { storm::ir::Program program; ASSERT_NO_THROW(program = storm::parser::PrismParserFromFile(STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.nm")); - std::shared_ptr> model = storm::adapters::ExplicitModelAdapter::translateProgram(program); + std::shared_ptr> model = storm::adapters::ExplicitModelAdapter::translateProgram(program, "", "coinflips"); ASSERT_EQ(model->getNumberOfStates(), 169ull); ASSERT_EQ(model->as>()->getNumberOfChoices(), 254ull);