From 9d5c3e7e2fb5e0d21a4ddf61169abbec744b1360 Mon Sep 17 00:00:00 2001 From: dehnert Date: Thu, 23 Jul 2015 23:23:35 -0700 Subject: [PATCH] added functionality to flatten the modules of a PRISM program into one module Former-commit-id: 04faac9c67b984c7164b66774d08c4ea79488a8c --- src/models/sparse/StochasticTwoPlayerGame.cpp | 34 ++- src/models/sparse/StochasticTwoPlayerGame.h | 45 ++- src/settings/modules/GeneralSettings.cpp | 14 + src/settings/modules/GeneralSettings.h | 13 +- src/solver/NativeLinearEquationSolver.cpp | 1 + src/storage/expressions/ExpressionManager.cpp | 4 + src/storage/expressions/ExpressionManager.h | 8 + src/storage/prism/Program.cpp | 269 +++++++++++++++++- src/storage/prism/Program.h | 23 ++ src/utility/solver.cpp | 25 ++ src/utility/solver.h | 27 ++ test/functional/parser/PrismParserTest.cpp | 2 - ...olverTest.cpp => MathsatSmtSolverTest.cpp} | 0 test/functional/storage/PrismProgramTest.cpp | 24 ++ 14 files changed, 473 insertions(+), 16 deletions(-) rename test/functional/solver/{MathSatSmtSolverTest.cpp => MathsatSmtSolverTest.cpp} (100%) create mode 100644 test/functional/storage/PrismProgramTest.cpp diff --git a/src/models/sparse/StochasticTwoPlayerGame.cpp b/src/models/sparse/StochasticTwoPlayerGame.cpp index 8e6daa52a..188ef7f12 100644 --- a/src/models/sparse/StochasticTwoPlayerGame.cpp +++ b/src/models/sparse/StochasticTwoPlayerGame.cpp @@ -13,7 +13,7 @@ namespace storm { boost::optional> const& optionalStateRewardVector, boost::optional> const& optionalPlayer1ChoiceLabeling, boost::optional> const& optionalPlayer2ChoiceLabeling) - : NondeterministicModel(storm::models::ModelType::S2pg, player2Matrix, stateLabeling, optionalStateRewardVector, boost::optional>(), optionalPlayer2ChoiceLabeling), player1Matrix(player1Matrix), player1Labels(optionalPlayer1ChoiceLabeling) { + : NondeterministicModel(storm::models::ModelType::S2pg, player2Matrix, stateLabeling, optionalStateRewardVector, boost::optional>(), optionalPlayer2ChoiceLabeling), player1Matrix(player1Matrix), player1ChoiceLabeling(optionalPlayer1ChoiceLabeling) { // Intentionally left empty. } @@ -25,10 +25,40 @@ namespace storm { boost::optional>&& optionalStateRewardVector, boost::optional>&& optionalPlayer1ChoiceLabeling, boost::optional>&& optionalPlayer2ChoiceLabeling) - : NondeterministicModel(storm::models::ModelType::S2pg, std::move(player2Matrix), std::move(stateLabeling), std::move(optionalStateRewardVector), boost::optional>(), std::move(optionalPlayer2ChoiceLabeling)), player1Matrix(std::move(player1Matrix)), player1Labels(std::move(optionalPlayer1ChoiceLabeling)) { + : NondeterministicModel(storm::models::ModelType::S2pg, std::move(player2Matrix), std::move(stateLabeling), std::move(optionalStateRewardVector), boost::optional>(), std::move(optionalPlayer2ChoiceLabeling)), player1Matrix(std::move(player1Matrix)), player1ChoiceLabeling(std::move(optionalPlayer1ChoiceLabeling)) { // Intentionally left empty. } + template + storm::storage::SparseMatrix const& StochasticTwoPlayerGame::getPlayer1Matrix() const { + return player1Matrix; + } + + template + storm::storage::SparseMatrix const& StochasticTwoPlayerGame::getPlayer2Matrix() const { + return this->getTransitionMatrix(); + } + + template + bool StochasticTwoPlayerGame::hasPlayer1ChoiceLabeling() const { + return static_cast(player1ChoiceLabeling); + } + + template + std::vector const& StochasticTwoPlayerGame::getPlayer1ChoiceLabeling() const { + return player1ChoiceLabeling.get(); + } + + template + bool StochasticTwoPlayerGame::hasPlayer2ChoiceLabeling() const { + return this->hasChoiceLabeling(); + } + + template + std::vector const& StochasticTwoPlayerGame::getPlayer2ChoiceLabeling() const { + return this->getChoiceLabeling(); + } + template class StochasticTwoPlayerGame; template class StochasticTwoPlayerGame; diff --git a/src/models/sparse/StochasticTwoPlayerGame.h b/src/models/sparse/StochasticTwoPlayerGame.h index cbd2988ca..c72e46fe8 100644 --- a/src/models/sparse/StochasticTwoPlayerGame.h +++ b/src/models/sparse/StochasticTwoPlayerGame.h @@ -56,6 +56,49 @@ namespace storm { StochasticTwoPlayerGame& operator=(StochasticTwoPlayerGame&& other) = default; #endif + /*! + * Retrieves the matrix representing the choices in player 1 states. + * + * @return A matrix representing the choices in player 1 states. + */ + storm::storage::SparseMatrix const& getPlayer1Matrix() const; + + /*! + * Retrieves the matrix representing the choices in player 2 states and the associated probability + * distributions. + * + * @return A matrix representing the choices in player 2 states. + */ + storm::storage::SparseMatrix const& getPlayer2Matrix() const; + + /*! + * Retrieves the whether the game has labels attached to the choices in player 1 states. + * + * @return True if the game has player 1 choice labels. + */ + bool hasPlayer1ChoiceLabeling() const; + + /*! + * Retrieves the labels attached to the choices of player 1 states. + * + * @return A vector containing the labels of each player 1 choice. + */ + std::vector const& getPlayer1ChoiceLabeling() const; + + /*! + * Retrieves whether the game has labels attached to player 2 states. + * + * @return True if the game has player 2 labels. + */ + bool hasPlayer2ChoiceLabeling() const; + + /*! + * Retrieves the labels attached to the choices of player 2 states. + * + * @return A vector containing the labels of each player 2 choice. + */ + std::vector const& getPlayer2ChoiceLabeling() const; + private: // A matrix that stores the player 1 choices. This matrix contains a row group for each player 1 node. Every // row group contains a row for each choice in that player 1 node. Each such row contains exactly one @@ -65,7 +108,7 @@ namespace storm { // An (optional) vector of labels attached to the choices of player 1. Each row of the matrix can be equipped // with a set of labels to tag certain choices. - boost::optional> player1Labels; + boost::optional> player1ChoiceLabeling; // The matrix and labels for player 2 are stored in the superclass. }; diff --git a/src/settings/modules/GeneralSettings.cpp b/src/settings/modules/GeneralSettings.cpp index 807823f67..8824d8b42 100644 --- a/src/settings/modules/GeneralSettings.cpp +++ b/src/settings/modules/GeneralSettings.cpp @@ -35,6 +35,7 @@ namespace storm { const std::string GeneralSettings::timeoutOptionShortName = "t"; const std::string GeneralSettings::eqSolverOptionName = "eqsolver"; const std::string GeneralSettings::lpSolverOptionName = "lpsolver"; + const std::string GeneralSettings::smtSolverOptionName = "smtsolver"; const std::string GeneralSettings::constantsOptionName = "constants"; const std::string GeneralSettings::constantsOptionShortName = "const"; const std::string GeneralSettings::statisticsOptionName = "statistics"; @@ -96,6 +97,9 @@ namespace storm { std::vector lpSolvers = {"gurobi", "glpk"}; this->addOption(storm::settings::OptionBuilder(moduleName, lpSolverOptionName, false, "Sets which LP solver is preferred.") .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of an LP solver. Available are: gurobi and glpk.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(lpSolvers)).setDefaultValueString("glpk").build()).build()); + std::vector smtSolvers = {"z3", "mathsat"}; + this->addOption(storm::settings::OptionBuilder(moduleName, smtSolverOptionName, false, "Sets which SMT solver is preferred.") + .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of an SMT solver. Available are: z3 and mathsat.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(smtSolvers)).setDefaultValueString("z3").build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, constantsOptionName, false, "Specifies the constant replacements to use in symbolic models. Note that Note that this requires the model to be given as an symbolic model (i.e., via --" + symbolicOptionName + ").").setShortName(constantsOptionShortName) .addArgument(storm::settings::ArgumentBuilder::createStringArgument("values", "A comma separated list of constants and their value, e.g. a=1,b=2,c=3.").setDefaultValueString("").build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, statisticsOptionName, false, "Sets whether to display statistics if available.").setShortName(statisticsOptionShortName).build()); @@ -259,6 +263,16 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown LP solver '" << lpSolverName << "'."); } + GeneralSettings::SmtSolver GeneralSettings::getSmtSolver() const { + std::string smtSolverName = this->getOption(smtSolverOptionName).getArgumentByName("name").getValueAsString(); + if (smtSolverName == "z3") { + return GeneralSettings::SmtSolver::Z3; + } else if (smtSolverName == "mathsat") { + return GeneralSettings::SmtSolver::Mathsat; + } + STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown SMT solver '" << smtSolverName << "'."); + } + bool GeneralSettings::isConstantsSet() const { return this->getOption(constantsOptionName).getHasOptionBeenSet(); } diff --git a/src/settings/modules/GeneralSettings.h b/src/settings/modules/GeneralSettings.h index f2454a28f..15b3d66cd 100644 --- a/src/settings/modules/GeneralSettings.h +++ b/src/settings/modules/GeneralSettings.h @@ -15,7 +15,10 @@ namespace storm { public: // An enumeration of all engines. enum class Engine { Sparse, Hybrid, Dd }; - + + // An enumeration of all available SMT solvers. + enum class SmtSolver { Z3, Mathsat }; + // An enumeration of all available LP solvers. enum class LpSolver { Gurobi, glpk }; @@ -280,6 +283,13 @@ namespace storm { * @return The selected LP solver. */ LpSolver getLpSolver() const; + + /*! + * Retrieves the selected SMT solver. + * + * @return The selected SMT solver. + */ + SmtSolver getSmtSolver() const; /*! * Retrieves whether the export-to-dot option was set. @@ -386,6 +396,7 @@ namespace storm { static const std::string timeoutOptionShortName; static const std::string eqSolverOptionName; static const std::string lpSolverOptionName; + static const std::string smtSolverOptionName; static const std::string constantsOptionName; static const std::string constantsOptionShortName; static const std::string statisticsOptionName; diff --git a/src/solver/NativeLinearEquationSolver.cpp b/src/solver/NativeLinearEquationSolver.cpp index a389853c6..a9960d6c3 100644 --- a/src/solver/NativeLinearEquationSolver.cpp +++ b/src/solver/NativeLinearEquationSolver.cpp @@ -156,6 +156,7 @@ namespace storm { std::string NativeLinearEquationSolver::methodToString() const { switch (method) { case SolutionMethod::Jacobi: return "jacobi"; + default: return "unsupported"; } } diff --git a/src/storage/expressions/ExpressionManager.cpp b/src/storage/expressions/ExpressionManager.cpp index 6738a0502..9a2643546 100644 --- a/src/storage/expressions/ExpressionManager.cpp +++ b/src/storage/expressions/ExpressionManager.cpp @@ -204,6 +204,10 @@ namespace storm { std::string newName = "__x" + std::to_string(freshVariableCounter++); return declareOrGetVariable(newName, variableType, auxiliary, false); } + + Variable ExpressionManager::declareFreshBooleanVariable(bool auxiliary) { + return declareFreshVariable(this->getBooleanType()); + } uint_fast64_t ExpressionManager::getNumberOfVariables(storm::expressions::Type const& variableType) const { if (variableType.isBooleanType()) { diff --git a/src/storage/expressions/ExpressionManager.h b/src/storage/expressions/ExpressionManager.h index c0bda2a5c..cfd37ae34 100644 --- a/src/storage/expressions/ExpressionManager.h +++ b/src/storage/expressions/ExpressionManager.h @@ -234,6 +234,14 @@ namespace storm { */ Variable declareFreshVariable(storm::expressions::Type const& variableType, bool auxiliary = false); + /*! + * Declares a boolean variable with the given type whose name is guaranteed to be unique and not yet in use. + * + * @param auxiliary A flag indicating whether the new variable should be tagged as an auxiliary variable. + * @return The variable. + */ + Variable declareFreshBooleanVariable(bool auxiliary = false); + /*! * Retrieves the number of variables. * diff --git a/src/storage/prism/Program.cpp b/src/storage/prism/Program.cpp index 258d4e14d..d21b3dca6 100644 --- a/src/storage/prism/Program.cpp +++ b/src/storage/prism/Program.cpp @@ -1,10 +1,12 @@ #include "src/storage/prism/Program.h" #include +#include #include "src/storage/expressions/ExpressionManager.h" #include "src/settings/SettingsManager.h" #include "src/utility/macros.h" +#include "src/utility/solver.h" #include "src/exceptions/InvalidArgumentException.h" #include "src/exceptions/OutOfRangeException.h" #include "src/exceptions/WrongFormatException.h" @@ -724,6 +726,250 @@ namespace storm { } } + Program Program::flattenModules(std::unique_ptr const& smtSolverFactory) const { + // If the current program has only one module, we can simply return a copy. + if (this->getNumberOfModules() == 1) { + return Program(*this); + } + + STORM_LOG_THROW(this->getModelType() == ModelType::DTMC || this->getModelType() == ModelType::MDP, storm::exceptions::InvalidTypeException, "Unable to flatten modules for model of type '" << this->getModelType() << "'."); + + // Otherwise, we need to actually flatten the contained modules. + + // Get an SMT solver for computing the possible guard combinations. + std::unique_ptr solver = smtSolverFactory->create(*manager); + + // Set up the data we need to gather to create the flat module. + std::stringstream newModuleName; + std::vector allBooleanVariables; + std::vector allIntegerVariables; + std::vector newCommands; + uint_fast64_t nextCommandIndex = 0; + uint_fast64_t nextUpdateIndex = 0; + + // Assert the values of the constants. + for (auto const& constant : this->getConstants()) { + if (constant.isDefined()) { + solver->add(constant.getExpressionVariable() == constant.getExpression()); + } + } + + // Assert the bounds of the global variables. + for (auto const& variable : this->getGlobalIntegerVariables()) { + solver->add(variable.getExpression() >= variable.getLowerBoundExpression()); + solver->add(variable.getExpression() <= variable.getUpperBoundExpression()); + } + + // Make the global variables local, such that the resulting module covers all occurring variables. Note that + // this is just for simplicity and is not needed. + allBooleanVariables.insert(allBooleanVariables.end(), this->getGlobalBooleanVariables().begin(), this->getGlobalBooleanVariables().end()); + allIntegerVariables.insert(allIntegerVariables.end(), this->getGlobalIntegerVariables().begin(), this->getGlobalIntegerVariables().end()); + + // Now go through the modules, gather the variables, construct the name of the new module and assert the + // bounds of the discovered variables. + for (auto const& module : this->getModules()) { + newModuleName << module.getName() << "_"; + allBooleanVariables.insert(allBooleanVariables.end(), module.getBooleanVariables().begin(), module.getBooleanVariables().end()); + allIntegerVariables.insert(allIntegerVariables.end(), module.getIntegerVariables().begin(), module.getIntegerVariables().end()); + + for (auto const& variable : module.getIntegerVariables()) { + solver->add(variable.getExpression() >= variable.getLowerBoundExpression()); + solver->add(variable.getExpression() <= variable.getUpperBoundExpression()); + } + + // The commands without a synchronizing action name, can simply be copied (plus adjusting the global + // indices of the command and its updates). + for (auto const& command : module.getCommands()) { + if (!command.isLabeled()) { + std::vector updates; + updates.reserve(command.getUpdates().size()); + + for (auto const& update : command.getUpdates()) { + updates.push_back(storm::prism::Update(nextUpdateIndex, update.getLikelihoodExpression(), update.getAssignments(), update.getFilename(), 0)); + ++nextUpdateIndex; + } + + newCommands.push_back(storm::prism::Command(nextCommandIndex, command.isMarkovian(), actionToIndexMap.find("")->second, "", command.getGuardExpression(), updates, command.getFilename(), 0)); + ++nextCommandIndex; + } + } + } + + // Save state of solver so that we can always restore the point where we have exactly the constant values + // and variables bounds on the assertion stack. + solver->push(); + + // Now we need to enumerate all possible combinations of synchronizing commands. For this, we iterate over + // all actions and let the solver enumerate the possible combinations of commands that can be enabled together. + for (auto const& actionIndex : this->getActionIndices()) { + bool noCombinationsForAction = false; + + // Prepare the list that stores for each module the list of commands with the given action. + std::vector>> possibleCommands; + + for (auto const& module : this->getModules()) { + // If the module has no command with this action, we can skip it. + if (!module.hasActionIndex(actionIndex)) { + continue; + } + + std::set const& commandIndices = module.getCommandIndicesByActionIndex(actionIndex); + + // If there is no command even though the module has this action, there is no valid command + // combination with this action. + if (commandIndices.empty()) { + noCombinationsForAction = true; + break; + } + + // Prepare empty list of commands for this module. + possibleCommands.push_back(std::vector>()); + + // Add references to the commands labeled with the current action. + for (auto const& commandIndex : commandIndices) { + possibleCommands.back().push_back(module.getCommand(commandIndex)); + } + } + + // If there are no valid combinations for the action, we need to skip the generation of synchronizing + // commands. + if (!noCombinationsForAction) { + // Save the solver state to be able to restore it when this action index is done. + solver->push(); + + // Start by creating a fresh auxiliary variable for each command and link it with the guard. + std::vector> commandVariables(possibleCommands.size()); + std::vector allCommandVariables; + for (uint_fast64_t outerIndex = 0; outerIndex < possibleCommands.size(); ++outerIndex) { + // Create auxiliary variables and link them with the guards. + for (uint_fast64_t innerIndex = 0; innerIndex < possibleCommands[outerIndex].size(); ++innerIndex) { + commandVariables[outerIndex].push_back(manager->declareFreshBooleanVariable()); + allCommandVariables.push_back(commandVariables[outerIndex].back()); + solver->add(implies(commandVariables[outerIndex].back(), possibleCommands[outerIndex][innerIndex].get().getGuardExpression())); + } + + storm::expressions::Expression atLeastOneCommandFromModule = manager->boolean(false); + for (auto const& commandVariable : commandVariables[outerIndex]) { + atLeastOneCommandFromModule = atLeastOneCommandFromModule || commandVariable; + } + solver->add(atLeastOneCommandFromModule); + } + + // Now we are in a position to start the enumeration over all command variables. + uint_fast64_t modelCount = 0; + solver->allSat(allCommandVariables, [&] (storm::solver::SmtSolver::ModelReference& modelReference) -> bool { + // Now we need to reconstruct the chosen commands from the valuation of the command variables. + std::vector>> chosenCommands(possibleCommands.size()); + + for (uint_fast64_t outerIndex = 0; outerIndex < commandVariables.size(); ++outerIndex) { + for (uint_fast64_t innerIndex = 0; innerIndex < commandVariables[outerIndex].size(); ++innerIndex) { + if (modelReference.getBooleanValue(commandVariables[outerIndex][innerIndex])) { + chosenCommands[outerIndex].push_back(possibleCommands[outerIndex][innerIndex]); + } + } + } + + // Now that we have retrieved the commands, we need to build their synchronizations and add them + // to the flattened module. + std::vector>::const_iterator> iterators; + for (auto const& element : chosenCommands) { + iterators.push_back(element.begin()); + } + + bool movedAtLeastOneIterator = false; + std::vector> commandCombination(chosenCommands.size(), chosenCommands.front().front()); + do { + for (uint_fast64_t index = 0; index < iterators.size(); ++index) { + commandCombination[index] = *iterators[index]; + } + + newCommands.push_back(synchronizeCommands(nextCommandIndex, actionIndex, nextUpdateIndex, indexToActionMap.find(actionIndex)->second, commandCombination)); + + // Move the counters appropriately. + ++nextCommandIndex; + nextUpdateIndex += newCommands.back().getNumberOfUpdates(); + + movedAtLeastOneIterator = false; + for (uint_fast64_t index = 0; index < iterators.size(); ++index) { + ++iterators[index]; + if (iterators[index] != chosenCommands[index].cend()) { + movedAtLeastOneIterator = true; + break; + } else { + iterators[index] = chosenCommands[index].cbegin(); + } + } + } while (movedAtLeastOneIterator); + + return true; + }); + + solver->pop(); + } + } + + // Finally, we can create the module and the program and return it. + storm::prism::Module singleModule(newModuleName.str(), allBooleanVariables, allIntegerVariables, newCommands, this->getFilename(), 0); + return Program(manager, this->getModelType(), this->getConstants(), std::vector(), std::vector(), this->getFormulas(), {singleModule}, actionToIndexMap, this->getRewardModels(), false, this->getInitialConstruct(), this->getLabels(), this->getFilename(), 0, true); + } + + Command Program::synchronizeCommands(uint_fast64_t newCommandIndex, uint_fast64_t actionIndex, uint_fast64_t firstUpdateIndex, std::string const& actionName, std::vector> const& commands) const { + // To construct the synchronous product of the commands, we need to store a list of its updates. + std::vector newUpdates; + uint_fast64_t numberOfUpdates = 1; + for (uint_fast64_t i = 0; i < commands.size(); ++i) { + numberOfUpdates *= commands[i].get().getNumberOfUpdates(); + } + newUpdates.reserve(numberOfUpdates); + + // Initialize all update iterators. + std::vector::const_iterator> updateIterators; + for (uint_fast64_t i = 0; i < commands.size(); ++i) { + updateIterators.push_back(commands[i].get().getUpdates().cbegin()); + } + + bool doneUpdates = false; + do { + // We create the new likelihood expression by multiplying the particapting updates' expressions. + storm::expressions::Expression newLikelihoodExpression = updateIterators[0]->getLikelihoodExpression(); + for (uint_fast64_t i = 1; i < updateIterators.size(); ++i) { + newLikelihoodExpression = newLikelihoodExpression * updateIterators[i]->getLikelihoodExpression(); + } + + // Now concatenate all assignments of all participating updates. + std::vector newAssignments; + for (uint_fast64_t i = 0; i < updateIterators.size(); ++i) { + newAssignments.insert(newAssignments.end(), updateIterators[i]->getAssignments().begin(), updateIterators[i]->getAssignments().end()); + } + + // Then we are ready to create the new update. + newUpdates.push_back(storm::prism::Update(firstUpdateIndex, newLikelihoodExpression, newAssignments, this->getFilename(), 0)); + ++firstUpdateIndex; + + // Now check whether there is some update combination we have not yet explored. + bool movedIterator = false; + for (int_fast64_t j = updateIterators.size() - 1; j >= 0; --j) { + ++updateIterators[j]; + if (updateIterators[j] != commands[j].get().getUpdates().cend()) { + movedIterator = true; + break; + } else { + // Reset the iterator to the beginning of the list. + updateIterators[j] = commands[j].get().getUpdates().cbegin(); + } + } + + doneUpdates = !movedIterator; + } while (!doneUpdates); + + storm::expressions::Expression newGuard = commands[0].get().getGuardExpression(); + for (uint_fast64_t i = 1; i < commands.size(); ++i) { + newGuard = newGuard && commands[i].get().getGuardExpression(); + } + + return Command(newCommandIndex, false, actionIndex, actionName, newGuard, newUpdates, this->getFilename(), 0); + } + storm::expressions::ExpressionManager const& Program::getManager() const { return *this->manager; } @@ -732,17 +978,20 @@ namespace storm { return *this->manager; } - std::ostream& operator<<(std::ostream& stream, Program const& program) { - switch (program.getModelType()) { - case Program::ModelType::UNDEFINED: stream << "undefined"; break; - case Program::ModelType::DTMC: stream << "dtmc"; break; - case Program::ModelType::CTMC: stream << "ctmc"; break; - case Program::ModelType::MDP: stream << "mdp"; break; - case Program::ModelType::CTMDP: stream << "ctmdp"; break; - case Program::ModelType::MA: stream << "ma"; break; + std::ostream& operator<<(std::ostream& out, Program::ModelType const& type) { + switch (type) { + case Program::ModelType::UNDEFINED: out << "undefined"; break; + case Program::ModelType::DTMC: out << "dtmc"; break; + case Program::ModelType::CTMC: out << "ctmc"; break; + case Program::ModelType::MDP: out << "mdp"; break; + case Program::ModelType::CTMDP: out << "ctmdp"; break; + case Program::ModelType::MA: out << "ma"; break; } - stream << std::endl; - + return out; + } + + std::ostream& operator<<(std::ostream& stream, Program const& program) { + stream << program.getModelType() << std::endl; for (auto const& constant : program.getConstants()) { stream << constant << std::endl; } diff --git a/src/storage/prism/Program.h b/src/storage/prism/Program.h index 5bb241a24..3037c4f7c 100644 --- a/src/storage/prism/Program.h +++ b/src/storage/prism/Program.h @@ -13,6 +13,7 @@ #include "src/storage/prism/Module.h" #include "src/storage/prism/RewardModel.h" #include "src/storage/prism/InitialConstruct.h" +#include "src/utility/solver.h" #include "src/utility/OsDetection.h" namespace storm { @@ -389,6 +390,14 @@ namespace storm { */ void checkValidity() const; + /*! + * Creates an equivalent program that contains exactly one module. + * + * @param smtSolverFactory an SMT solver factory to use. If none is given, the default one is used. + * @return The resulting program. + */ + Program flattenModules(std::unique_ptr const& smtSolverFactory = std::unique_ptr(new storm::utility::solver::SmtSolverFactory())) const; + friend std::ostream& operator<<(std::ostream& stream, Program const& program); /*! @@ -406,6 +415,18 @@ namespace storm { storm::expressions::ExpressionManager& getManager(); private: + /*! + * This function builds a command that corresponds to the synchronization of the given list of commands. + * + * @param newCommandIndex The index of the command to construct. + * @param actionIndex The index of the action of the resulting command. + * @param firstUpdateIndex The index of the first update of the resulting command. + * @param actionName The name of the action of the resulting command. + * @param commands The commands to synchronize. + * @return The resulting command. + */ + Command synchronizeCommands(uint_fast64_t newCommandIndex, uint_fast64_t actionIndex, uint_fast64_t firstUpdateIndex, std::string const& actionName, std::vector> const& commands) const; + // The manager responsible for the variables/expressions of the program. std::shared_ptr manager; @@ -476,6 +497,8 @@ namespace storm { std::map variableToModuleIndexMap; }; + std::ostream& operator<<(std::ostream& out, Program::ModelType const& type); + } // namespace prism } // namespace storm diff --git a/src/utility/solver.cpp b/src/utility/solver.cpp index 785f1d00c..4b7d3248c 100644 --- a/src/utility/solver.cpp +++ b/src/utility/solver.cpp @@ -14,6 +14,9 @@ #include "src/solver/GurobiLpSolver.h" #include "src/solver/GlpkLpSolver.h" +#include "src/solver/Z3SmtSolver.h" +#include "src/solver/MathsatSmtSolver.h" + namespace storm { namespace utility { namespace solver { @@ -110,6 +113,28 @@ namespace storm { return factory->create(name); } + std::unique_ptr SmtSolverFactory::create(storm::expressions::ExpressionManager& manager) const { + storm::settings::modules::GeneralSettings::SmtSolver smtSolver = storm::settings::generalSettings().getSmtSolver(); + switch (smtSolver) { + case storm::settings::modules::GeneralSettings::SmtSolver::Z3: return std::unique_ptr(new storm::solver::Z3SmtSolver(manager)); + case storm::settings::modules::GeneralSettings::SmtSolver::Mathsat: return std::unique_ptr(new storm::solver::MathsatSmtSolver(manager)); + } + + } + + std::unique_ptr Z3SmtSolverFactory::create(storm::expressions::ExpressionManager& manager) const { + return std::unique_ptr(new storm::solver::Z3SmtSolver(manager)); + } + + std::unique_ptr MathsatSmtSolverFactory::create(storm::expressions::ExpressionManager& manager) const { + return std::unique_ptr(new storm::solver::MathsatSmtSolver(manager)); + } + + std::unique_ptr getSmtSolver(storm::expressions::ExpressionManager& manager) { + std::unique_ptr factory(new MathsatSmtSolverFactory()); + return factory->create(manager); + } + template class SymbolicLinearEquationSolverFactory; template class SymbolicGameSolverFactory; template class LinearEquationSolverFactory; diff --git a/src/utility/solver.h b/src/utility/solver.h index cd56695f0..2492e18f7 100644 --- a/src/utility/solver.h +++ b/src/utility/solver.h @@ -7,8 +7,11 @@ #include "src/solver/LinearEquationSolver.h" #include "src/solver/NativeLinearEquationSolver.h" #include "src/solver/MinMaxLinearEquationSolver.h" + #include "src/solver/LpSolver.h" +#include "src/solver/SmtSolver.h" + #include "src/storage/dd/DdType.h" #include "src/settings/modules/NativeEquationSolverSettings.h" @@ -109,6 +112,30 @@ namespace storm { }; std::unique_ptr getLpSolver(std::string const& name); + + class SmtSolverFactory { + public: + /*! + * Creates a new SMT solver instance. + * + * @param manager The expression manager responsible for the expressions that will be given to the SMT + * solver. + * @return A pointer to the newly created solver. + */ + virtual std::unique_ptr create(storm::expressions::ExpressionManager& manager) const; + }; + + class Z3SmtSolverFactory : public SmtSolverFactory { + public: + virtual std::unique_ptr create(storm::expressions::ExpressionManager& manager) const; + }; + + class MathsatSmtSolverFactory : public SmtSolverFactory { + public: + virtual std::unique_ptr create(storm::expressions::ExpressionManager& manager) const; + }; + + std::unique_ptr getSmtSolver(storm::expressions::ExpressionManager& manager); } } } diff --git a/test/functional/parser/PrismParserTest.cpp b/test/functional/parser/PrismParserTest.cpp index a3fbc7526..23bc2d917 100644 --- a/test/functional/parser/PrismParserTest.cpp +++ b/test/functional/parser/PrismParserTest.cpp @@ -4,11 +4,9 @@ TEST(PrismParser, StandardModelTest) { storm::prism::Program result; - result = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/parser/prism/coin2.nm"); EXPECT_NO_THROW(result = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/parser/prism/coin2.nm")); EXPECT_NO_THROW(result = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/parser/prism/crowds5_5.pm")); EXPECT_NO_THROW(result = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/parser/prism/csma2_2.nm")); - result = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/parser/prism/die.pm"); EXPECT_NO_THROW(result = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/parser/prism/die.pm")); EXPECT_NO_THROW(result = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/parser/prism/firewire.nm")); EXPECT_NO_THROW(result = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/parser/prism/leader3.nm")); diff --git a/test/functional/solver/MathSatSmtSolverTest.cpp b/test/functional/solver/MathsatSmtSolverTest.cpp similarity index 100% rename from test/functional/solver/MathSatSmtSolverTest.cpp rename to test/functional/solver/MathsatSmtSolverTest.cpp diff --git a/test/functional/storage/PrismProgramTest.cpp b/test/functional/storage/PrismProgramTest.cpp new file mode 100644 index 000000000..36607a13c --- /dev/null +++ b/test/functional/storage/PrismProgramTest.cpp @@ -0,0 +1,24 @@ +#include "gtest/gtest.h" +#include "storm-config.h" +#include "src/parser/PrismParser.h" + +#include "src/utility/solver.h" + +#ifdef STORM_HAVE_MSAT +TEST(PrismProgramTest, FlattenModules) { + storm::prism::Program result; + ASSERT_NO_THROW(result = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/parser/prism/leader3.nm")); + + std::unique_ptr smtSolverFactory(new storm::utility::solver::MathsatSmtSolverFactory()); + + ASSERT_NO_THROW(result = result.flattenModules(smtSolverFactory)); + EXPECT_EQ(1, result.getNumberOfModules()); + EXPECT_EQ(74, result.getModule(0).getNumberOfCommands()); + + ASSERT_NO_THROW(result = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/parser/prism/wlan0_collide.nm")); + + ASSERT_NO_THROW(result = result.flattenModules(smtSolverFactory)); + EXPECT_EQ(1, result.getNumberOfModules()); + EXPECT_EQ(180, result.getModule(0).getNumberOfCommands()); +} +#endif