diff --git a/CMakeLists.txt b/CMakeLists.txt index cf7643c0c..16c9c63d0 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -27,6 +27,7 @@ option(USE_LIBCXX "Sets whether the standard library is libc++." OFF) option(USE_CARL "Sets whether carl should be included." ON) option(FORCE_COLOR "Force color output" OFF) option(STORM_PYTHON "Builds the API for Python" OFF) +option(STOMR_COMPILE_WITH_CCACHE "Compile using CCache" ON) set(GUROBI_ROOT "" CACHE STRING "A hint to the root directory of Gurobi (optional).") set(Z3_ROOT "" CACHE STRING "A hint to the root directory of Z3 (optional).") set(CUDA_ROOT "" CACHE STRING "The root directory of CUDA.") @@ -44,7 +45,16 @@ endif() message(STATUS "StoRM - Building ${CMAKE_BUILD_TYPE} version.") message(STATUS "StoRM - CMAKE_BUILD_TYPE (ENV): $ENV{CMAKE_BUILD_TYPE}") - +if(STOMR_COMPILE_WITH_CCACHE) + find_program(CCACHE_FOUND ccache) + if(CCACHE_FOUND) + message(STATUS "SToRM - Using ccache") + set_property(GLOBAL PROPERTY RULE_LAUNCH_COMPILE ccache) + set_property(GLOBAL PROPERTY RULE_LAUNCH_LINK ccache) + else() + message(STATUS "Could not find ccache") + endif() +endif() # Base path for test files set(STORM_CPP_TESTS_BASE_PATH "${PROJECT_SOURCE_DIR}/test") diff --git a/src/cli/cli.cpp b/src/cli/cli.cpp index c9e0aa7e6..36b6df27e 100644 --- a/src/cli/cli.cpp +++ b/src/cli/cli.cpp @@ -1,4 +1,5 @@ #include "cli.h" +#include "entrypoints.h" #include "../utility/storm.h" @@ -7,6 +8,7 @@ #include "src/utility/storm-version.h" + // Includes for the linked libraries and versions header. #ifdef STORM_HAVE_INTELTBB # include "tbb/tbb_stddef.h" @@ -110,7 +112,7 @@ namespace storm { std::cout << "Compiled with CUDA support, but an error occured trying to find CUDA devices." << std::endl; } #endif - + // "Compute" the command line argument string with which STORM was invoked. std::stringstream commandStream; for (int i = 1; i < argc; ++i) { diff --git a/src/logic/Formula.cpp b/src/logic/Formula.cpp index 4037cb723..e621c1c78 100644 --- a/src/logic/Formula.cpp +++ b/src/logic/Formula.cpp @@ -1,4 +1,5 @@ #include "src/logic/Formulas.h" +#include namespace storm { namespace logic { @@ -404,6 +405,12 @@ namespace storm { return; } + std::string Formula::toString() const { + std::stringstream str2; + writeToStream(str2); + return str2.str(); + } + std::ostream& operator<<(std::ostream& out, Formula const& formula) { return formula.writeToStream(out); } diff --git a/src/logic/Formula.h b/src/logic/Formula.h index 3c3c3b5aa..4d831e456 100644 --- a/src/logic/Formula.h +++ b/src/logic/Formula.h @@ -174,6 +174,7 @@ namespace storm { std::shared_ptr asSharedPointer(); std::shared_ptr asSharedPointer() const; + std::string toString() const; virtual std::ostream& writeToStream(std::ostream& out) const = 0; virtual void gatherAtomicExpressionFormulas(std::vector>& atomicExpressionFormulas) const; diff --git a/src/modelchecker/reachability/MenuGameMdpModelChecker.cpp b/src/modelchecker/reachability/MenuGameMdpModelChecker.cpp new file mode 100644 index 000000000..09ad129d3 --- /dev/null +++ b/src/modelchecker/reachability/MenuGameMdpModelChecker.cpp @@ -0,0 +1,61 @@ +#include "src/modelchecker/reachability/MenuGameMdpModelChecker.h" + +#include "src/utility/macros.h" + +#include "src/exceptions/NotSupportedException.h" + +#include "src/modelchecker/results/CheckResult.h" + +namespace storm { + namespace modelchecker { + MenuGameMdpModelChecker::MenuGameMdpModelChecker(storm::prism::Program const& program, std::unique_ptr&& smtSolverFactory) : originalProgram(program), smtSolverFactory(std::move(smtSolverFactory)) { + STORM_LOG_THROW(program.getModelType() == storm::prism::Program::ModelType::MDP, storm::exceptions::NotSupportedException, "Currently only MDPs are supported by the game-based model checker."); + + // Start by preparing the program. That is, we flatten the modules if there is more than one. + if (originalProgram.getNumberOfModules() > 1) { + preprocessedProgram = originalProgram.flattenModules(smtSolverFactory); + } else { + preprocessedProgram = originalProgram; + } + } + + bool MenuGameMdpModelChecker::canHandle(storm::logic::Formula const& formula) const { + if (formula.isProbabilityOperatorFormula()) { + storm::logic::ProbabilityOperatorFormula const& probabilityOperatorFormula = formula.asProbabilityOperatorFormula(); + return this->canHandle(probabilityOperatorFormula.getSubformula()); + } else if (formula.isUntilFormula() || formula.isEventuallyFormula()) { + if (formula.isUntilFormula()) { + storm::logic::UntilFormula const& untilFormula = formula.asUntilFormula(); + if (untilFormula.getLeftSubformula().isPropositionalFormula() && untilFormula.getRightSubformula().isPropositionalFormula()) { + return true; + } + } else if (formula.isEventuallyFormula()) { + storm::logic::EventuallyFormula const& eventuallyFormula = formula.asEventuallyFormula(); + if (eventuallyFormula.getSubformula().isPropositionalFormula()) { + return true; + } + } + } + return false; + } + + std::unique_ptr MenuGameMdpModelChecker::checkProbabilityOperatorFormula(storm::logic::ProbabilityOperatorFormula const& stateFormula) { + // Depending on whether or not there is a bound, we do something slightly different here. + + return nullptr; + } + + std::unique_ptr computeUntilProbabilities(storm::logic::UntilFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { + // TODO + + return nullptr; + } + + std::unique_ptr computeEventuallyProbabilities(storm::logic::EventuallyFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { + // TODO + + return nullptr; + } + + } +} \ No newline at end of file diff --git a/src/modelchecker/reachability/MenuGameMdpModelChecker.h b/src/modelchecker/reachability/MenuGameMdpModelChecker.h new file mode 100644 index 000000000..7919d1bed --- /dev/null +++ b/src/modelchecker/reachability/MenuGameMdpModelChecker.h @@ -0,0 +1,59 @@ +#ifndef STORM_MODELCHECKER_MENUGAMEMDPMODELCHECKER_H_ +#define STORM_MODELCHECKER_MENUGAMEMDPMODELCHECKER_H_ + +#include "src/modelchecker/AbstractModelChecker.h" + +#include "src/storage/prism/Program.h" + +#include "src/utility/solver.h" + +namespace storm { + namespace modelchecker { + class MenuGameMdpModelChecker : public AbstractModelChecker { + public: + /*! + * Constructs a model checker whose underlying model is implicitly given by the provided program. All + * verification calls will be answererd with respect to this model. + * + * @param program The program that implicitly specifies the model to check. + * @param smtSolverFactory A factory used to create SMT solver when necessary. + */ + explicit MenuGameMdpModelChecker(storm::prism::Program const& program, std::unique_ptr&& smtSolverFactory); + + virtual bool canHandle(storm::logic::Formula const& formula) const override; + + virtual std::unique_ptr checkProbabilityOperatorFormula(storm::logic::ProbabilityOperatorFormula const& stateFormula) override; + + virtual std::unique_ptr computeUntilProbabilities(storm::logic::UntilFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; + virtual std::unique_ptr computeEventuallyProbabilities(storm::logic::EventuallyFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; + + private: + /*! + * Performs game-based abstraction refinement on the model until either the precision is met or the provided + * proof goal was successfully proven. + * + * @param filterPredicate A predicate that needs to hold until the target predicate holds. + * @param targetPredicate A predicate characterizing the target states. + * @param precision The precision to use. This governs what difference between lower and upper bounds is + * acceptable. + * @param proofGoal A proof goal that says the probability must only be established to be above/below a given + * threshold. If the proof goal is met before the precision is achieved, the refinement procedure will abort + * and return the current result. + * @return A pair of values, that are under- and over-approximations of the actual probability, respectively. + */ + std::pair performGameBasedRefinement(storm::expressions::Expression const& filterPredicate, storm::expressions::Expression const& targetPredicate, double precision, boost::optional> const& proofGoal); + + // The original program that was used to create this model checker. + storm::prism::Program originalProgram; + + // The preprocessed program that contains only one module and otherwhise corresponds to the semantics of the + // original program. + storm::prism::Program preprocessedProgram; + + // A factory that is used for creating SMT solvers when needed. + std::unique_ptr smtSolverFactory; + }; + } +} + +#endif /* STORM_MODELCHECKER_MENUGAMEMDPMODELCHECKER_H_ */ \ No newline at end of file diff --git a/src/models/sparse/Ctmc.cpp b/src/models/sparse/Ctmc.cpp index 371d48270..62347c81b 100644 --- a/src/models/sparse/Ctmc.cpp +++ b/src/models/sparse/Ctmc.cpp @@ -11,7 +11,7 @@ namespace storm { Ctmc::Ctmc(storm::storage::SparseMatrix const& rateMatrix, storm::models::sparse::StateLabeling const& stateLabeling, std::unordered_map const& rewardModels, boost::optional> const& optionalChoiceLabeling) - : DeterministicModel(storm::models::ModelType::Ctmc, rateMatrix, stateLabeling, rewardModels, optionalChoiceLabeling) { + : DeterministicModel(storm::models::ModelType::Ctmc, rateMatrix, stateLabeling, rewardModels, optionalChoiceLabeling) { exitRates = createExitRateVector(this->getTransitionMatrix()); } @@ -19,7 +19,7 @@ namespace storm { Ctmc::Ctmc(storm::storage::SparseMatrix&& rateMatrix, storm::models::sparse::StateLabeling&& stateLabeling, std::unordered_map&& rewardModels, boost::optional>&& optionalChoiceLabeling) - : DeterministicModel(storm::models::ModelType::Ctmc, std::move(rateMatrix), std::move(stateLabeling), std::move(rewardModels), std::move(optionalChoiceLabeling)) { + : DeterministicModel(storm::models::ModelType::Ctmc, std::move(rateMatrix), std::move(stateLabeling), std::move(rewardModels), std::move(optionalChoiceLabeling)) { // It is important to refer to the transition matrix here, because the given rate matrix has been move elsewhere. exitRates = createExitRateVector(this->getTransitionMatrix()); } @@ -41,6 +41,8 @@ namespace storm { template class Ctmc; #ifdef STORM_HAVE_CARL + template class Ctmc>; + template class Ctmc; #endif diff --git a/src/models/sparse/DeterministicModel.cpp b/src/models/sparse/DeterministicModel.cpp index d774d5e7f..0fb6de34a 100644 --- a/src/models/sparse/DeterministicModel.cpp +++ b/src/models/sparse/DeterministicModel.cpp @@ -12,7 +12,7 @@ namespace storm { storm::models::sparse::StateLabeling const& stateLabeling, std::unordered_map const& rewardModels, boost::optional> const& optionalChoiceLabeling) - : Model(modelType, transitionMatrix, stateLabeling, rewardModels, optionalChoiceLabeling) { + : Model(modelType, transitionMatrix, stateLabeling, rewardModels, optionalChoiceLabeling) { // Intentionally left empty. } @@ -22,13 +22,13 @@ namespace storm { storm::models::sparse::StateLabeling&& stateLabeling, std::unordered_map&& rewardModels, boost::optional>&& optionalChoiceLabeling) - : Model(modelType, std::move(transitionMatrix), std::move(stateLabeling), std::move(rewardModels), std::move(optionalChoiceLabeling)) { + : Model(modelType, std::move(transitionMatrix), std::move(stateLabeling), std::move(rewardModels), std::move(optionalChoiceLabeling)) { // Intentionally left empty. } template void DeterministicModel::writeDotToStream(std::ostream& outStream, bool includeLabeling, storm::storage::BitVector const* subsystem, std::vector const* firstValue, std::vector const* secondValue, std::vector const* stateColoring, std::vector const* colors, std::vector* scheduler, bool finalizeOutput) const { - Model::writeDotToStream(outStream, includeLabeling, subsystem, firstValue, secondValue, stateColoring, colors, scheduler, false); + Model::writeDotToStream(outStream, includeLabeling, subsystem, firstValue, secondValue, stateColoring, colors, scheduler, false); // Simply iterate over all transitions and draw the arrows with probability information attached. auto rowIt = this->getTransitionMatrix().begin(); @@ -59,6 +59,8 @@ namespace storm { template class DeterministicModel; #ifdef STORM_HAVE_CARL + template class DeterministicModel>; + template class DeterministicModel; #endif diff --git a/src/models/sparse/DeterministicModel.h b/src/models/sparse/DeterministicModel.h index fb3e367df..cc886c401 100644 --- a/src/models/sparse/DeterministicModel.h +++ b/src/models/sparse/DeterministicModel.h @@ -49,7 +49,7 @@ namespace storm { #ifndef WINDOWS DeterministicModel(DeterministicModel&& other) = default; - DeterministicModel& operator=(DeterministicModel&& model) = default; + DeterministicModel& operator=(DeterministicModel&& model) = default; #endif virtual void reduceToStateBasedRewards() override; diff --git a/src/models/sparse/Dtmc.cpp b/src/models/sparse/Dtmc.cpp index 9cc968136..31c222207 100644 --- a/src/models/sparse/Dtmc.cpp +++ b/src/models/sparse/Dtmc.cpp @@ -14,14 +14,14 @@ namespace storm { storm::models::sparse::StateLabeling const& stateLabeling, std::unordered_map const& rewardModels, boost::optional> const& optionalChoiceLabeling) - : DeterministicModel(storm::models::ModelType::Dtmc, probabilityMatrix, stateLabeling, rewardModels, optionalChoiceLabeling) { + : DeterministicModel(storm::models::ModelType::Dtmc, probabilityMatrix, stateLabeling, rewardModels, optionalChoiceLabeling) { STORM_LOG_THROW(probabilityMatrix.isProbabilistic(), storm::exceptions::InvalidArgumentException, "The probability matrix is invalid."); } template Dtmc::Dtmc(storm::storage::SparseMatrix&& probabilityMatrix, storm::models::sparse::StateLabeling&& stateLabeling, std::unordered_map&& rewardModels, boost::optional>&& optionalChoiceLabeling) - : DeterministicModel(storm::models::ModelType::Dtmc, std::move(probabilityMatrix), std::move(stateLabeling), std::move(rewardModels), std::move(optionalChoiceLabeling)) { + : DeterministicModel(storm::models::ModelType::Dtmc, std::move(probabilityMatrix), std::move(stateLabeling), std::move(rewardModels), std::move(optionalChoiceLabeling)) { STORM_LOG_THROW(probabilityMatrix.isProbabilistic(), storm::exceptions::InvalidArgumentException, "The probability matrix is invalid."); } @@ -225,6 +225,8 @@ namespace storm { template class Dtmc; #ifdef STORM_HAVE_CARL + template class Dtmc>; + template class Dtmc; #endif diff --git a/src/models/sparse/MarkovAutomaton.cpp b/src/models/sparse/MarkovAutomaton.cpp index b04c294f7..56a6400d1 100644 --- a/src/models/sparse/MarkovAutomaton.cpp +++ b/src/models/sparse/MarkovAutomaton.cpp @@ -15,7 +15,7 @@ namespace storm { std::vector const& exitRates, std::unordered_map const& rewardModels, boost::optional> const& optionalChoiceLabeling) - : NondeterministicModel(storm::models::ModelType::MarkovAutomaton, transitionMatrix, stateLabeling, rewardModels, optionalChoiceLabeling), markovianStates(markovianStates), exitRates(exitRates), closed(false) { + : NondeterministicModel(storm::models::ModelType::MarkovAutomaton, transitionMatrix, stateLabeling, rewardModels, optionalChoiceLabeling), markovianStates(markovianStates), exitRates(exitRates), closed(false) { this->turnRatesToProbabilities(); } @@ -26,7 +26,7 @@ namespace storm { std::vector const& exitRates, std::unordered_map&& rewardModels, boost::optional>&& optionalChoiceLabeling) - : NondeterministicModel(storm::models::ModelType::MarkovAutomaton, std::move(transitionMatrix), std::move(stateLabeling), std::move(rewardModels), std::move(optionalChoiceLabeling)), markovianStates(markovianStates), exitRates(std::move(exitRates)), closed(false) { + : NondeterministicModel(storm::models::ModelType::MarkovAutomaton, std::move(transitionMatrix), std::move(stateLabeling), std::move(rewardModels), std::move(optionalChoiceLabeling)), markovianStates(markovianStates), exitRates(std::move(exitRates)), closed(false) { this->turnRatesToProbabilities(); } @@ -124,7 +124,7 @@ namespace storm { template void MarkovAutomaton::writeDotToStream(std::ostream& outStream, bool includeLabeling, storm::storage::BitVector const* subsystem, std::vector const* firstValue, std::vector const* secondValue, std::vector const* stateColoring, std::vector const* colors, std::vector* scheduler, bool finalizeOutput) const { - NondeterministicModel::writeDotToStream(outStream, includeLabeling, subsystem, firstValue, secondValue, stateColoring, colors, scheduler, false); + NondeterministicModel::writeDotToStream(outStream, includeLabeling, subsystem, firstValue, secondValue, stateColoring, colors, scheduler, false); // Write the probability distributions for all the states. for (uint_fast64_t state = 0; state < this->getNumberOfStates(); ++state) { @@ -205,7 +205,7 @@ namespace storm { template std::size_t MarkovAutomaton::getSizeInBytes() const { - return NondeterministicModel::getSizeInBytes() + markovianStates.getSizeInBytes() + exitRates.size() * sizeof(ValueType); + return NondeterministicModel::getSizeInBytes() + markovianStates.getSizeInBytes() + exitRates.size() * sizeof(ValueType); } template @@ -220,9 +220,11 @@ namespace storm { template class MarkovAutomaton; // template class MarkovAutomaton; -//#ifdef STORM_HAVE_CARL -// template class MarkovAutomaton; -//#endif +#ifdef STORM_HAVE_CARL + template class MarkovAutomaton>; + + template class MarkovAutomaton; +#endif } // namespace sparse } // namespace models diff --git a/src/models/sparse/MarkovAutomaton.h b/src/models/sparse/MarkovAutomaton.h index 98d561964..731b845f3 100644 --- a/src/models/sparse/MarkovAutomaton.h +++ b/src/models/sparse/MarkovAutomaton.h @@ -12,7 +12,7 @@ namespace storm { * This class represents a Markov automaton. */ template> - class MarkovAutomaton : public NondeterministicModel { + class MarkovAutomaton : public NondeterministicModel { public: /*! * Constructs a model from the given data. diff --git a/src/models/sparse/Mdp.cpp b/src/models/sparse/Mdp.cpp index 0ba1e7c28..f6e4b4800 100644 --- a/src/models/sparse/Mdp.cpp +++ b/src/models/sparse/Mdp.cpp @@ -9,42 +9,42 @@ namespace storm { namespace models { namespace sparse { - + template Mdp::Mdp(storm::storage::SparseMatrix const& transitionMatrix, storm::models::sparse::StateLabeling const& stateLabeling, std::unordered_map const& rewardModels, boost::optional> const& optionalChoiceLabeling) - : NondeterministicModel(storm::models::ModelType::Mdp, transitionMatrix, stateLabeling, rewardModels, optionalChoiceLabeling) { + : NondeterministicModel(storm::models::ModelType::Mdp, transitionMatrix, stateLabeling, rewardModels, optionalChoiceLabeling) { STORM_LOG_THROW(transitionMatrix.isProbabilistic(), storm::exceptions::InvalidArgumentException, "The probability matrix is invalid."); } - - + + template Mdp::Mdp(storm::storage::SparseMatrix&& transitionMatrix, storm::models::sparse::StateLabeling&& stateLabeling, std::unordered_map&& rewardModels, boost::optional>&& optionalChoiceLabeling) - : NondeterministicModel(storm::models::ModelType::Mdp, std::move(transitionMatrix), std::move(stateLabeling), std::move(rewardModels), std::move(optionalChoiceLabeling)) { + : NondeterministicModel(storm::models::ModelType::Mdp, std::move(transitionMatrix), std::move(stateLabeling), std::move(rewardModels), std::move(optionalChoiceLabeling)) { STORM_LOG_THROW(transitionMatrix.isProbabilistic(), storm::exceptions::InvalidArgumentException, "The probability matrix is invalid."); } - + template - Mdp Mdp::restrictChoiceLabels(LabelSet const& enabledChoiceLabels) const { + Mdp Mdp::restrictChoiceLabels(LabelSet const& enabledChoiceLabels) const { STORM_LOG_THROW(this->hasChoiceLabeling(), storm::exceptions::InvalidArgumentException, "Restriction to label set is impossible for unlabeled model."); - + std::vector const& choiceLabeling = this->getChoiceLabeling(); - + storm::storage::SparseMatrixBuilder transitionMatrixBuilder(0, this->getTransitionMatrix().getColumnCount(), 0, true, true); std::vector newChoiceLabeling; - + // Check for each choice of each state, whether the choice labels are fully contained in the given label set. uint_fast64_t currentRow = 0; for(uint_fast64_t state = 0; state < this->getNumberOfStates(); ++state) { bool stateHasValidChoice = false; for (uint_fast64_t choice = this->getTransitionMatrix().getRowGroupIndices()[state]; choice < this->getTransitionMatrix().getRowGroupIndices()[state + 1]; ++choice) { bool choiceValid = std::includes(enabledChoiceLabels.begin(), enabledChoiceLabels.end(), choiceLabeling[choice].begin(), choiceLabeling[choice].end()); - + // If the choice is valid, copy over all its elements. if (choiceValid) { if (!stateHasValidChoice) { @@ -58,7 +58,7 @@ namespace storm { ++currentRow; } } - + // If no choice of the current state may be taken, we insert a self-loop to the state instead. if (!stateHasValidChoice) { transitionMatrixBuilder.newRowGroup(currentRow); @@ -67,27 +67,29 @@ namespace storm { ++currentRow; } } - - Mdp restrictedMdp(transitionMatrixBuilder.build(), storm::models::sparse::StateLabeling(this->getStateLabeling()), - std::unordered_map(this->getRewardModels()), boost::optional>(newChoiceLabeling)); - + + Mdp restrictedMdp(transitionMatrixBuilder.build(), storm::models::sparse::StateLabeling(this->getStateLabeling()), + std::unordered_map(this->getRewardModels()), boost::optional>(newChoiceLabeling)); + return restrictedMdp; } - + template - Mdp Mdp::restrictActions(storm::storage::BitVector const& enabledActions) const { + Mdp Mdp::restrictActions(storm::storage::BitVector const& enabledActions) const { storm::storage::SparseMatrix restrictedTransitions = this->getTransitionMatrix().restrictRows(enabledActions); std::unordered_map newRewardModels; for (auto const& rewardModel : this->getRewardModels()) { newRewardModels.emplace(rewardModel.first, rewardModel.second.restrictActions(enabledActions)); } - return Mdp(restrictedTransitions, this->getStateLabeling(), newRewardModels, this->getOptionalChoiceLabeling()); + return Mdp(restrictedTransitions, this->getStateLabeling(), newRewardModels, this->getOptionalChoiceLabeling()); } - + template class Mdp; template class Mdp; #ifdef STORM_HAVE_CARL + template class Mdp>; + template class Mdp; #endif diff --git a/src/models/sparse/Mdp.h b/src/models/sparse/Mdp.h index 6354551f9..9bc29bbc9 100644 --- a/src/models/sparse/Mdp.h +++ b/src/models/sparse/Mdp.h @@ -57,7 +57,7 @@ namespace storm { * and which ones need to be ignored. * @return A restricted version of the current MDP that only uses choice labels from the given set. */ - Mdp restrictChoiceLabels(LabelSet const& enabledChoiceLabels) const; + Mdp restrictChoiceLabels(LabelSet const& enabledChoiceLabels) const; /*! * Constructs an MDP by copying the current MDP and restricting the choices of each state to the ones given by the bitvector. @@ -65,7 +65,7 @@ namespace storm { * @param enabledActions A BitVector of lenght numberOfChoices(), which is one iff the action should be kept. * @return A subMDP. */ - Mdp restrictActions(storm::storage::BitVector const& enabledActions) const; + Mdp restrictActions(storm::storage::BitVector const& enabledActions) const; }; } // namespace sparse diff --git a/src/models/sparse/Model.cpp b/src/models/sparse/Model.cpp index 8ed43e87a..cf22ecf6c 100644 --- a/src/models/sparse/Model.cpp +++ b/src/models/sparse/Model.cpp @@ -300,6 +300,8 @@ namespace storm { template class Model; #ifdef STORM_HAVE_CARL + template class Model>; + template class Model; #endif diff --git a/src/models/sparse/NondeterministicModel.cpp b/src/models/sparse/NondeterministicModel.cpp index c5e3e9ecf..9cfbe75f9 100644 --- a/src/models/sparse/NondeterministicModel.cpp +++ b/src/models/sparse/NondeterministicModel.cpp @@ -16,7 +16,7 @@ namespace storm { storm::models::sparse::StateLabeling const& stateLabeling, std::unordered_map const& rewardModels, boost::optional> const& optionalChoiceLabeling) - : Model(modelType, transitionMatrix, stateLabeling, rewardModels, optionalChoiceLabeling) { + : Model(modelType, transitionMatrix, stateLabeling, rewardModels, optionalChoiceLabeling) { // Intentionally left empty. } @@ -26,7 +26,7 @@ namespace storm { storm::models::sparse::StateLabeling&& stateLabeling, std::unordered_map&& rewardModels, boost::optional>&& optionalChoiceLabeling) - : Model(modelType, std::move(transitionMatrix), std::move(stateLabeling), std::move(rewardModels), + : Model(modelType, std::move(transitionMatrix), std::move(stateLabeling), std::move(rewardModels), std::move(optionalChoiceLabeling)) { // Intentionally left empty. } @@ -79,7 +79,7 @@ namespace storm { template void NondeterministicModel::writeDotToStream(std::ostream& outStream, bool includeLabeling, storm::storage::BitVector const* subsystem, std::vector const* firstValue, std::vector const* secondValue, std::vector const* stateColoring, std::vector const* colors, std::vector* scheduler, bool finalizeOutput) const { - Model::writeDotToStream(outStream, includeLabeling, subsystem, firstValue, secondValue, stateColoring, colors, scheduler, false); + Model::writeDotToStream(outStream, includeLabeling, subsystem, firstValue, secondValue, stateColoring, colors, scheduler, false); // Write the probability distributions for all the states. for (uint_fast64_t state = 0; state < this->getNumberOfStates(); ++state) { @@ -151,6 +151,8 @@ namespace storm { template class NondeterministicModel; #ifdef STORM_HAVE_CARL + template class NondeterministicModel>; + template class NondeterministicModel; #endif diff --git a/src/models/sparse/StochasticTwoPlayerGame.cpp b/src/models/sparse/StochasticTwoPlayerGame.cpp index ecbb204c5..c8ce13bec 100644 --- a/src/models/sparse/StochasticTwoPlayerGame.cpp +++ b/src/models/sparse/StochasticTwoPlayerGame.cpp @@ -15,7 +15,7 @@ namespace storm { std::unordered_map const& rewardModels, boost::optional> const& optionalPlayer1ChoiceLabeling, boost::optional> const& optionalPlayer2ChoiceLabeling) - : NondeterministicModel(storm::models::ModelType::S2pg, player2Matrix, stateLabeling, rewardModels, optionalPlayer2ChoiceLabeling), player1Matrix(player1Matrix), player1Labels(optionalPlayer1ChoiceLabeling) { + : NondeterministicModel(storm::models::ModelType::S2pg, player2Matrix, stateLabeling, rewardModels, optionalPlayer2ChoiceLabeling), player1Matrix(player1Matrix), player1ChoiceLabeling(optionalPlayer1ChoiceLabeling) { // Intentionally left empty. } @@ -27,16 +27,46 @@ namespace storm { std::unordered_map&& rewardModels, boost::optional>&& optionalPlayer1ChoiceLabeling, boost::optional>&& optionalPlayer2ChoiceLabeling) - : NondeterministicModel(storm::models::ModelType::S2pg, std::move(player2Matrix), std::move(stateLabeling), std::move(rewardModels), std::move(optionalPlayer2ChoiceLabeling)), player1Matrix(std::move(player1Matrix)), player1Labels(std::move(optionalPlayer1ChoiceLabeling)) { + : NondeterministicModel(storm::models::ModelType::S2pg, std::move(player2Matrix), std::move(stateLabeling), std::move(rewardModels), 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; -//#ifdef STORM_HAVE_CARL +#ifdef STORM_HAVE_CARL // template class StochasticTwoPlayerGame; -//#endif +#endif } // namespace sparse } // namespace models diff --git a/src/models/sparse/StochasticTwoPlayerGame.h b/src/models/sparse/StochasticTwoPlayerGame.h index 41628efd6..313361e3a 100644 --- a/src/models/sparse/StochasticTwoPlayerGame.h +++ b/src/models/sparse/StochasticTwoPlayerGame.h @@ -57,6 +57,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 @@ -66,7 +109,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/parser/AutoParser.cpp b/src/parser/AutoParser.cpp index ca01c758f..2ec30fb64 100644 --- a/src/parser/AutoParser.cpp +++ b/src/parser/AutoParser.cpp @@ -10,6 +10,8 @@ #include "src/utility/macros.h" #include "src/exceptions/WrongFormatException.h" +#include "src/adapters/CarlAdapter.h" + #include "src/utility/cstring.h" #include "src/utility/OsDetection.h" @@ -19,7 +21,7 @@ namespace storm { using namespace storm::utility::cstring; template - std::shared_ptr> AutoParser::parseModel(std::string const& transitionsFilename, + std::shared_ptr>> AutoParser::parseModel(std::string const& transitionsFilename, std::string const& labelingFilename, std::string const& stateRewardFilename, std::string const& transitionRewardFilename, @@ -33,22 +35,22 @@ namespace storm { switch (type) { case storm::models::ModelType::Dtmc: { - model.reset(new storm::models::sparse::Dtmc>(std::move(DeterministicModelParser::parseDtmc(transitionsFilename, labelingFilename, stateRewardFilename, transitionRewardFilename)))); + model = std::shared_ptr>>(new storm::models::sparse::Dtmc>(std::move(DeterministicModelParser::parseDtmc(transitionsFilename, labelingFilename, stateRewardFilename, transitionRewardFilename)))); break; } case storm::models::ModelType::Ctmc: { - model.reset(new storm::models::sparse::Ctmc>(std::move(DeterministicModelParser::parseCtmc(transitionsFilename, labelingFilename, stateRewardFilename, transitionRewardFilename)))); + model = std::shared_ptr>>(new storm::models::sparse::Ctmc>(std::move(DeterministicModelParser::parseCtmc(transitionsFilename, labelingFilename, stateRewardFilename, transitionRewardFilename)))); break; } case storm::models::ModelType::Mdp: { - model.reset(new storm::models::sparse::Mdp>(std::move(NondeterministicModelParser::parseMdp(transitionsFilename, labelingFilename, stateRewardFilename, transitionRewardFilename, choiceLabelingFilename)))); + model = std::shared_ptr>>(new storm::models::sparse::Mdp>(std::move(NondeterministicModelParser::parseMdp(transitionsFilename, labelingFilename, stateRewardFilename, transitionRewardFilename, choiceLabelingFilename)))); break; } case storm::models::ModelType::MarkovAutomaton: { - model.reset(new storm::models::sparse::MarkovAutomaton>(storm::parser::MarkovAutomatonParser::parseMarkovAutomaton(transitionsFilename, labelingFilename, stateRewardFilename, transitionRewardFilename))); + model = std::shared_ptr>>(new storm::models::sparse::MarkovAutomaton>(std::move(storm::parser::MarkovAutomatonParser::parseMarkovAutomaton(transitionsFilename, labelingFilename, stateRewardFilename, transitionRewardFilename)))); break; } default: @@ -94,6 +96,10 @@ namespace storm { // Explicitly instantiate the parser. template class AutoParser; + +#ifdef STORM_HAVE_CARL + template class AutoParser; +#endif } // namespace parser } // namespace storm diff --git a/src/parser/AutoParser.h b/src/parser/AutoParser.h index fd144b24e..525795e9d 100644 --- a/src/parser/AutoParser.h +++ b/src/parser/AutoParser.h @@ -47,7 +47,7 @@ namespace storm { * is meaningful, this file will not be parsed. * @return A shared_ptr containing the resulting model. */ - static std::shared_ptr> parseModel(std::string const& transitionsFilename, + static std::shared_ptr>> parseModel(std::string const& transitionsFilename, std::string const& labelingFilename, std::string const& stateRewardFilename = "", std::string const& transitionRewardFilename = "", diff --git a/src/parser/DeterministicModelParser.cpp b/src/parser/DeterministicModelParser.cpp index 34bec0855..18f14428a 100644 --- a/src/parser/DeterministicModelParser.cpp +++ b/src/parser/DeterministicModelParser.cpp @@ -9,6 +9,8 @@ #include "src/parser/AtomicPropositionLabelingParser.h" #include "src/parser/SparseStateRewardParser.h" +#include "src/adapters/CarlAdapter.h" + namespace storm { namespace parser { @@ -62,6 +64,10 @@ namespace storm { } template class DeterministicModelParser; + +#ifdef STORM_HAVE_CARL + template class DeterministicModelParser; +#endif } /* namespace parser */ } /* namespace storm */ diff --git a/src/parser/DeterministicSparseTransitionParser.cpp b/src/parser/DeterministicSparseTransitionParser.cpp index bb91355d4..94b82a4c7 100644 --- a/src/parser/DeterministicSparseTransitionParser.cpp +++ b/src/parser/DeterministicSparseTransitionParser.cpp @@ -16,6 +16,8 @@ #include "src/settings/SettingsManager.h" #include "src/settings/modules/GeneralSettings.h" +#include "src/adapters/CarlAdapter.h" + #include "log4cplus/logger.h" #include "log4cplus/loggingmacros.h" extern log4cplus::Logger logger; @@ -297,5 +299,12 @@ namespace storm { template class DeterministicSparseTransitionParser; template storm::storage::SparseMatrix DeterministicSparseTransitionParser::parseDeterministicTransitionRewards(std::string const& filename, storm::storage::SparseMatrix const& transitionMatrix); template storm::storage::SparseMatrix DeterministicSparseTransitionParser::parse(std::string const& filename, bool isRewardFile, storm::storage::SparseMatrix const& transitionMatrix); + +#ifdef STORM_HAVE_CARL + template class DeterministicSparseTransitionParser; + + template storm::storage::SparseMatrix DeterministicSparseTransitionParser::parseDeterministicTransitionRewards(std::string const& filename, storm::storage::SparseMatrix const& transitionMatrix); + template storm::storage::SparseMatrix DeterministicSparseTransitionParser::parse(std::string const& filename, bool isRewardFile, storm::storage::SparseMatrix const& transitionMatrix); +#endif } // namespace parser } // namespace storm diff --git a/src/parser/MarkovAutomatonParser.cpp b/src/parser/MarkovAutomatonParser.cpp index 683b4142c..6a68abda8 100644 --- a/src/parser/MarkovAutomatonParser.cpp +++ b/src/parser/MarkovAutomatonParser.cpp @@ -6,6 +6,8 @@ #include "src/exceptions/WrongFormatException.h" +#include "src/adapters/CarlAdapter.h" + #include "log4cplus/logger.h" #include "log4cplus/loggingmacros.h" extern log4cplus::Logger logger; @@ -31,7 +33,7 @@ namespace storm { stateRewards.reset(storm::parser::SparseStateRewardParser::parseSparseStateReward(transitionMatrix.getColumnCount(), stateRewardFilename)); } std::unordered_map> rewardModels; - rewardModels.insert(std::make_pair("", storm::models::sparse::StandardRewardModel(stateRewards, boost::optional>(), boost::optional>()))); + rewardModels.insert(std::make_pair("", storm::models::sparse::StandardRewardModel(stateRewards, boost::optional>(), boost::optional>()))); // Since Markov Automata do not support transition rewards no path should be given here. if (transitionRewardFilename != "") { @@ -46,6 +48,10 @@ namespace storm { } template class MarkovAutomatonParser; - + +#ifdef STORM_HAVE_CARL + template class MarkovAutomatonParser; +#endif + } // namespace parser } // namespace storm diff --git a/src/parser/MarkovAutomatonSparseTransitionParser.cpp b/src/parser/MarkovAutomatonSparseTransitionParser.cpp index 539a67739..6bc214cab 100644 --- a/src/parser/MarkovAutomatonSparseTransitionParser.cpp +++ b/src/parser/MarkovAutomatonSparseTransitionParser.cpp @@ -8,7 +8,6 @@ #include "src/utility/cstring.h" #include "src/utility/macros.h" - namespace storm { namespace parser { diff --git a/src/parser/NondeterministicModelParser.cpp b/src/parser/NondeterministicModelParser.cpp index 743d6e9b2..220451c33 100644 --- a/src/parser/NondeterministicModelParser.cpp +++ b/src/parser/NondeterministicModelParser.cpp @@ -10,6 +10,8 @@ #include "src/parser/SparseStateRewardParser.h" #include "src/parser/SparseChoiceLabelingParser.h" +#include "src/adapters/CarlAdapter.h" + namespace storm { namespace parser { @@ -31,7 +33,7 @@ namespace storm { } // Only parse transition rewards if a file is given. - boost::optional> transitionRewards; + boost::optional> transitionRewards; if (!transitionRewardFilename.empty()) { transitionRewards = std::move(storm::parser::NondeterministicSparseTransitionParser::parseNondeterministicTransitionRewards(transitionRewardFilename, transitions)); } @@ -61,6 +63,10 @@ namespace storm { } template class NondeterministicModelParser; - + +#ifdef STORM_HAVE_CARL + template class NondeterministicModelParser; +#endif + } /* namespace parser */ } /* namespace storm */ diff --git a/src/parser/NondeterministicSparseTransitionParser.cpp b/src/parser/NondeterministicSparseTransitionParser.cpp index 646fc0352..3136bc36f 100644 --- a/src/parser/NondeterministicSparseTransitionParser.cpp +++ b/src/parser/NondeterministicSparseTransitionParser.cpp @@ -13,6 +13,8 @@ #include "src/utility/cstring.h" +#include "src/adapters/CarlAdapter.h" + #include "log4cplus/logger.h" #include "log4cplus/loggingmacros.h" extern log4cplus::Logger logger; @@ -189,7 +191,7 @@ namespace storm { // Finally, build the actual matrix, test and return it. storm::storage::SparseMatrix resultMatrix = matrixBuilder.build(); - // Since we cannot do the testing if each transition for which there is a reward in the reward file also exists in the transition matrix during parsing, we have to do it afterwards. + // Since we cannot check if each transition for which there is a reward in the reward file also exists in the transition matrix during parsing, we have to do it afterwards. if (isRewardFile && !resultMatrix.isSubmatrixOf(modelInformation)) { LOG4CPLUS_ERROR(logger, "There are rewards for non existent transitions given in the reward file."); throw storm::exceptions::WrongFormatException() << "There are rewards for non existent transitions given in the reward file."; @@ -336,6 +338,13 @@ namespace storm { template class NondeterministicSparseTransitionParser; template storm::storage::SparseMatrix NondeterministicSparseTransitionParser::parseNondeterministicTransitionRewards(std::string const& filename, storm::storage::SparseMatrix const& modelInformation); template storm::storage::SparseMatrix NondeterministicSparseTransitionParser::parse(std::string const& filename, bool isRewardFile, storm::storage::SparseMatrix const& modelInformation); - + +#ifdef STORM_HAVE_CARL + template class NondeterministicSparseTransitionParser; + + template storm::storage::SparseMatrix NondeterministicSparseTransitionParser::parseNondeterministicTransitionRewards(std::string const& filename, storm::storage::SparseMatrix const& modelInformation); + template storm::storage::SparseMatrix NondeterministicSparseTransitionParser::parse(std::string const& filename, bool isRewardFile, storm::storage::SparseMatrix const& modelInformation); +#endif + } // namespace parser } // namespace storm diff --git a/src/parser/SparseStateRewardParser.cpp b/src/parser/SparseStateRewardParser.cpp index d2424740d..b60856eb8 100644 --- a/src/parser/SparseStateRewardParser.cpp +++ b/src/parser/SparseStateRewardParser.cpp @@ -6,6 +6,9 @@ #include "src/exceptions/FileIoException.h" #include "src/utility/cstring.h" #include "src/parser/MappedFile.h" + +#include "src/adapters/CarlAdapter.h" + #include "log4cplus/logger.h" #include "log4cplus/loggingmacros.h" extern log4cplus::Logger logger; @@ -27,7 +30,7 @@ namespace storm { char const* buf = file.getData(); // Create state reward vector with given state count. - std::vector stateRewards(stateCount); + std::vector stateRewards(stateCount); // Now parse state reward assignments. uint_fast64_t state = 0; @@ -71,5 +74,9 @@ namespace storm { template class SparseStateRewardParser; +#ifdef STORM_HAVE_CARL + template class SparseStateRewardParser; +#endif + } // namespace parser } // namespace storm diff --git a/src/settings/modules/GeneralSettings.cpp b/src/settings/modules/GeneralSettings.cpp index fd63cd780..eeef1ff1a 100644 --- a/src/settings/modules/GeneralSettings.cpp +++ b/src/settings/modules/GeneralSettings.cpp @@ -42,6 +42,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"; @@ -102,6 +103,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()); @@ -256,6 +260,16 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown LP solver '" << lpSolverName << "'."); } + storm::solver::SmtSolverType GeneralSettings::getSmtSolver() const { + std::string smtSolverName = this->getOption(smtSolverOptionName).getArgumentByName("name").getValueAsString(); + if (smtSolverName == "z3") { + return storm::solver::SmtSolverType::Z3; + } else if (smtSolverName == "mathsat") { + return storm::solver::SmtSolverType::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 f4c69d835..2f9064e1b 100644 --- a/src/settings/modules/GeneralSettings.h +++ b/src/settings/modules/GeneralSettings.h @@ -9,6 +9,7 @@ namespace storm { enum class EquationSolverType; enum class LpSolverType; enum class MinMaxTechnique; + enum class SmtSolverType; } namespace settings { @@ -268,6 +269,13 @@ namespace storm { */ storm::solver::LpSolverType getLpSolver() const; + /*! + * Retrieves the selected SMT solver. + * + * @return The selected SMT solver. + */ + storm::solver::SmtSolverType getSmtSolver() const; + /*! * Retrieves whether the export-to-dot option was set. * @@ -374,6 +382,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/SolverSelectionOptions.cpp b/src/solver/SolverSelectionOptions.cpp index 68e76ead8..2b42908aa 100644 --- a/src/solver/SolverSelectionOptions.cpp +++ b/src/solver/SolverSelectionOptions.cpp @@ -11,7 +11,8 @@ namespace storm { } } - std::string toString(LpSolverType t) { + + std::string toString(LpSolverType t) { switch(t) { case LpSolverType::Gurobi: return "Gurobi"; @@ -19,7 +20,7 @@ namespace storm { return "Glpk"; } } - + std::string toString(EquationSolverType t) { switch(t) { case EquationSolverType::Native: @@ -30,5 +31,14 @@ namespace storm { return "Topological"; } } + + std::string toString(SmtSolverType t) { + switch(t) { + case SmtSolverType::Z3: + return "Z3"; + case SmtSolverType::Mathsat: + return "Mathsat"; + } + } } } diff --git a/src/solver/SolverSelectionOptions.h b/src/solver/SolverSelectionOptions.h index 51f448644..1379343c9 100644 --- a/src/solver/SolverSelectionOptions.h +++ b/src/solver/SolverSelectionOptions.h @@ -1,4 +1,3 @@ - #ifndef SOLVERSELECTIONOPTIONS_H #define SOLVERSELECTIONOPTIONS_H @@ -7,13 +6,11 @@ namespace storm { namespace solver { - ExtendEnumsWithSelectionField(MinMaxTechnique, PolicyIteration, ValueIteration) + ExtendEnumsWithSelectionField(MinMaxTechnique, PolicyIteration, ValueIteration) - ExtendEnumsWithSelectionField(LpSolverType, Gurobi, Glpk) ExtendEnumsWithSelectionField(EquationSolverType, Native, Gmmxx, Topological) - - + ExtendEnumsWithSelectionField(SmtSolverType, Z3, Mathsat) } } diff --git a/src/storage/SparseMatrix.cpp b/src/storage/SparseMatrix.cpp index 20b7cd7f5..4648950b3 100644 --- a/src/storage/SparseMatrix.cpp +++ b/src/storage/SparseMatrix.cpp @@ -1081,7 +1081,8 @@ namespace storm { } template - bool SparseMatrix::isSubmatrixOf(SparseMatrix const& matrix) const { + template + bool SparseMatrix::isSubmatrixOf(SparseMatrix const& matrix) const { // Check for matching sizes. if (this->getRowCount() != matrix.getRowCount()) return false; if (this->getColumnCount() != matrix.getColumnCount()) return false; @@ -1089,7 +1090,9 @@ namespace storm { // Check the subset property for all rows individually. for (index_type row = 0; row < this->getRowCount(); ++row) { - for (const_iterator it1 = this->begin(row), ite1 = this->end(row), it2 = matrix.begin(row), ite2 = matrix.end(row); it1 != ite1; ++it1) { + auto it2 = matrix.begin(row); + auto ite2 = matrix.end(row); + for (const_iterator it1 = this->begin(row), ite1 = this->end(row); it1 != ite1; ++it1) { // Skip over all entries of the other matrix that are before the current entry in the current matrix. while (it2 != ite2 && it2->getColumn() < it1->getColumn()) { ++it2; @@ -1165,14 +1168,16 @@ namespace storm { template class SparseMatrix; template std::ostream& operator<<(std::ostream& out, SparseMatrix const& matrix); template std::vector SparseMatrix::getPointwiseProductRowSumVector(storm::storage::SparseMatrix const& otherMatrix) const; - - // float + template bool SparseMatrix::isSubmatrixOf(SparseMatrix const& matrix) const; + + // float template class MatrixEntry::index_type, float>; template std::ostream& operator<<(std::ostream& out, MatrixEntry const& entry); template class SparseMatrixBuilder; template class SparseMatrix; template std::ostream& operator<<(std::ostream& out, SparseMatrix const& matrix); template std::vector SparseMatrix::getPointwiseProductRowSumVector(storm::storage::SparseMatrix const& otherMatrix) const; + template bool SparseMatrix::isSubmatrixOf(SparseMatrix const& matrix) const; // int template class MatrixEntry::index_type, int>; @@ -1180,6 +1185,7 @@ namespace storm { template class SparseMatrixBuilder; template class SparseMatrix; template std::ostream& operator<<(std::ostream& out, SparseMatrix const& matrix); + template bool SparseMatrix::isSubmatrixOf(SparseMatrix const& matrix) const; #ifdef STORM_HAVE_CARL // Rat Function @@ -1192,6 +1198,7 @@ namespace storm { template std::vector SparseMatrix::getPointwiseProductRowSumVector(storm::storage::SparseMatrix const& otherMatrix) const; template std::vector SparseMatrix::getPointwiseProductRowSumVector(storm::storage::SparseMatrix const& otherMatrix) const; template std::vector SparseMatrix::getPointwiseProductRowSumVector(storm::storage::SparseMatrix const& otherMatrix) const; + template bool SparseMatrix::isSubmatrixOf(SparseMatrix const& matrix) const; // Intervals template std::vector SparseMatrix::getPointwiseProductRowSumVector(storm::storage::SparseMatrix const& otherMatrix) const; @@ -1201,6 +1208,9 @@ namespace storm { template class SparseMatrix; template std::ostream& operator<<(std::ostream& out, SparseMatrix const& matrix); template std::vector SparseMatrix::getPointwiseProductRowSumVector(storm::storage::SparseMatrix const& otherMatrix) const; + template bool SparseMatrix::isSubmatrixOf(SparseMatrix const& matrix) const; + + template bool SparseMatrix::isSubmatrixOf(SparseMatrix const& matrix) const; #endif diff --git a/src/storage/SparseMatrix.h b/src/storage/SparseMatrix.h index 03de1bd6b..1b5bef847 100644 --- a/src/storage/SparseMatrix.h +++ b/src/storage/SparseMatrix.h @@ -753,7 +753,8 @@ namespace storm { * @param matrix The matrix that possibly is a supermatrix of the current matrix. * @return True iff the current matrix is a submatrix of the given matrix. */ - bool isSubmatrixOf(SparseMatrix const& matrix) const; + template + bool isSubmatrixOf(SparseMatrix const& matrix) const; template friend std::ostream& operator<<(std::ostream& out, SparseMatrix const& matrix); diff --git a/src/storage/expressions/ExpressionManager.cpp b/src/storage/expressions/ExpressionManager.cpp index 55ef846ed..d1add4402 100644 --- a/src/storage/expressions/ExpressionManager.cpp +++ b/src/storage/expressions/ExpressionManager.cpp @@ -205,7 +205,7 @@ namespace storm { std::string newName = prefix + std::to_string(freshVariableCounter++); return declareOrGetVariable(newName, variableType, auxiliary, false); } - + Variable ExpressionManager::declareFreshBooleanVariable(bool auxiliary, const std::string& prefix) { return declareFreshVariable(this->getBooleanType(), auxiliary, prefix); } diff --git a/src/storage/prism/Program.cpp b/src/storage/prism/Program.cpp index 9859df52a..e62cfc114 100644 --- a/src/storage/prism/Program.cpp +++ b/src/storage/prism/Program.cpp @@ -1,15 +1,18 @@ #include "src/storage/prism/Program.h" #include +#include #include "src/storage/expressions/ExpressionManager.h" #include "src/settings/SettingsManager.h" #include "src/settings/modules/GeneralSettings.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" #include "src/exceptions/InvalidTypeException.h" +#include "src/solver/SmtSolver.h" namespace storm { namespace prism { @@ -878,6 +881,250 @@ namespace storm { return Program(this->manager, modelType, newConstants, getGlobalBooleanVariables(), getGlobalIntegerVariables(), getFormulas(), newModules, getActionNameToIndexMapping(), getRewardModels(), false, getInitialConstruct(), getLabels(), "", 0, false); } + 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->getSynchronizingActionIndices()) { + 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; } @@ -886,17 +1133,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 e4f64af8a..f2b13781d 100644 --- a/src/storage/prism/Program.h +++ b/src/storage/prism/Program.h @@ -12,6 +12,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 { @@ -419,6 +420,14 @@ namespace storm { */ void checkValidity(Program::ValidityCheckLevel lvl = Program::ValidityCheckLevel::READYFORPROCESSING) 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); /*! @@ -436,6 +445,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; @@ -517,6 +538,8 @@ namespace storm { Program replaceModulesAndConstantsInProgram(std::vector const& newModules, std::vector const& newConstants); }; + 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 6c63004bd..ef3744ff9 100644 --- a/src/utility/solver.cpp +++ b/src/utility/solver.cpp @@ -16,13 +16,14 @@ #include "src/solver/GurobiLpSolver.h" #include "src/solver/GlpkLpSolver.h" +#include "src/solver/Z3SmtSolver.h" +#include "src/solver/MathsatSmtSolver.h" #include "src/settings/SettingsManager.h" #include "src/settings/modules/GeneralSettings.h" #include "src/settings/modules/NativeEquationSolverSettings.h" #include "src/exceptions/InvalidSettingsException.h" - namespace storm { namespace utility { namespace solver { @@ -163,7 +164,27 @@ namespace storm { return factory->create(name, solvType); } + std::unique_ptr SmtSolverFactory::create(storm::expressions::ExpressionManager& manager) const { + storm::solver::SmtSolverType smtSolverType = storm::settings::generalSettings().getSmtSolver(); + switch (smtSolverType) { + case storm::solver::SmtSolverType::Z3: return std::unique_ptr(new storm::solver::Z3SmtSolver(manager)); + case storm::solver::SmtSolverType::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 SymbolicMinMaxLinearEquationSolverFactory; template class SymbolicGameSolverFactory; diff --git a/src/utility/solver.h b/src/utility/solver.h index ff5abb3e2..81e2d1d23 100644 --- a/src/utility/solver.h +++ b/src/utility/solver.h @@ -16,10 +16,12 @@ namespace storm { template class LinearEquationSolver; template class MinMaxLinearEquationSolver; class LpSolver; + class SmtSolver; template class NativeLinearEquationSolver; enum class NativeLinearEquationSolverSolutionMethod; } + namespace storage { template class SparseMatrix; } @@ -28,8 +30,10 @@ namespace storm { template class Add; template class Bdd; } + namespace expressions { class Variable; + class ExpressionManager; } namespace utility { @@ -126,6 +130,30 @@ namespace storm { }; std::unique_ptr getLpSolver(std::string const& name, storm::solver::LpSolverTypeSelection solvType = storm::solver::LpSolverTypeSelection::FROMSETTINGS) ; + + 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/src/utility/storm.h b/src/utility/storm.h index 7fa547588..19f84b85d 100644 --- a/src/utility/storm.h +++ b/src/utility/storm.h @@ -170,28 +170,26 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Unable to generate counterexample for parametric model."); } #endif - + template - void verifySparseModel(std::shared_ptr> model, std::vector> const& formulas) { - for (auto const& formula : formulas) { - - std::cout << std::endl << "Model checking property: " << *formula << " ..."; - std::unique_ptr result; - if (model->getType() == storm::models::ModelType::Dtmc) { - std::shared_ptr> dtmc = model->template as>(); - storm::modelchecker::SparseDtmcPrctlModelChecker> modelchecker(*dtmc); - if (modelchecker.canHandle(*formula)) { - result = modelchecker.check(*formula); - } else { - storm::modelchecker::SparseDtmcEliminationModelChecker> modelchecker2(*dtmc); - if (modelchecker2.canHandle(*formula)) { - result = modelchecker2.check(*formula); - } + std::unique_ptr verifySparseModel(std::shared_ptr> model, std::shared_ptr const& formula) { + + std::unique_ptr result; + if (model->getType() == storm::models::ModelType::Dtmc) { + std::shared_ptr> dtmc = model->template as>(); + storm::modelchecker::SparseDtmcPrctlModelChecker> modelchecker(*dtmc); + if (modelchecker.canHandle(*formula)) { + result = modelchecker.check(*formula); + } else { + storm::modelchecker::SparseDtmcEliminationModelChecker> modelchecker2(*dtmc); + if (modelchecker2.canHandle(*formula)) { + result = modelchecker2.check(*formula); } - } else if (model->getType() == storm::models::ModelType::Mdp) { - std::shared_ptr> mdp = model->template as>(); + } + } else if (model->getType() == storm::models::ModelType::Mdp) { + std::shared_ptr> mdp = model->template as>(); #ifdef STORM_HAVE_CUDA - if (settings.isCudaSet()) { + if (settings.isCudaSet()) { storm::modelchecker::TopologicalValueIterationMdpPrctlModelChecker modelchecker(*mdp); result = modelchecker.check(*formula); } else { @@ -199,26 +197,19 @@ namespace storm { result = modelchecker.check(*formula); } #else - storm::modelchecker::SparseMdpPrctlModelChecker> modelchecker(*mdp); - result = modelchecker.check(*formula); + storm::modelchecker::SparseMdpPrctlModelChecker> modelchecker(*mdp); + result = modelchecker.check(*formula); #endif - } else if (model->getType() == storm::models::ModelType::Ctmc) { - std::shared_ptr> ctmc = model->template as>(); + } else if (model->getType() == storm::models::ModelType::Ctmc) { + std::shared_ptr> ctmc = model->template as>(); - storm::modelchecker::SparseCtmcCslModelChecker> modelchecker(*ctmc); - result = modelchecker.check(*formula); - } - - if (result) { - std::cout << " done." << std::endl; - std::cout << "Result (initial states): "; - result->filter(storm::modelchecker::ExplicitQualitativeCheckResult(model->getInitialStates())); - std::cout << *result << std::endl; - } else { - std::cout << " skipped, because the modelling formalism is currently unsupported." << std::endl; - } + storm::modelchecker::SparseCtmcCslModelChecker> modelchecker(*ctmc); + result = modelchecker.check(*formula); } + return result; + } + #ifdef STORM_HAVE_CARL inline void exportParametricResultToFile(storm::RationalFunction const& result, storm::models::sparse::Dtmc::ConstraintCollector const& constraintCollector, std::string const& path) { @@ -236,163 +227,71 @@ namespace storm { std::copy(constraintCollector.getGraphPreservingConstraints().begin(), constraintCollector.getGraphPreservingConstraints().end(), std::ostream_iterator>(filestream, "\n")); filestream.close(); } - + template<> - inline void verifySparseModel(std::shared_ptr> model, std::vector> const& formulas) { + inline std::unique_ptr verifySparseModel(std::shared_ptr> model, std::shared_ptr const& formula) { + std::unique_ptr result; + std::shared_ptr> dtmc = model->template as>(); - for (auto const& formula : formulas) { - STORM_LOG_THROW(model->getType() == storm::models::ModelType::Dtmc, storm::exceptions::InvalidSettingsException, "Currently parametric verification is only available for DTMCs."); - std::shared_ptr> dtmc = model->template as>(); + storm::modelchecker::SparseDtmcEliminationModelChecker> modelchecker(*dtmc); + if (modelchecker.canHandle(*formula)) { + result = modelchecker.check(*formula); + } else { + STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "The parametric engine currently does not support this property."); + } + return result; + } + - std::cout << std::endl << "Model checking property: " << *formula << " ..."; - std::unique_ptr result; +#endif - storm::modelchecker::SparseDtmcEliminationModelChecker> modelchecker(*dtmc); + template + std::unique_ptr verifySymbolicModelWithHybridEngine(std::shared_ptr> model, std::shared_ptr const& formula) { + std::unique_ptr result; + if (model->getType() == storm::models::ModelType::Dtmc) { + std::shared_ptr> dtmc = model->template as>(); + storm::modelchecker::HybridDtmcPrctlModelChecker modelchecker(*dtmc); if (modelchecker.canHandle(*formula)) { result = modelchecker.check(*formula); - } else { - STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "The parametric engine currently does not support this property."); } - - if (result) { - std::cout << " done." << std::endl; - std::cout << "Result (initial states): "; - result->filter(storm::modelchecker::ExplicitQualitativeCheckResult(dtmc->getInitialStates())); - std::cout << *result << std::endl; - } else { - std::cout << " skipped, because the modelling formalism is currently unsupported." << std::endl; + } else if (model->getType() == storm::models::ModelType::Ctmc) { + std::shared_ptr> ctmc = model->template as>(); + storm::modelchecker::HybridCtmcCslModelChecker modelchecker(*ctmc); + if (modelchecker.canHandle(*formula)) { + result = modelchecker.check(*formula); } - - storm::settings::modules::ParametricSettings const& parametricSettings = storm::settings::parametricSettings(); - if (parametricSettings.exportResultToFile()) { - exportParametricResultToFile(result->asExplicitQuantitativeCheckResult()[*dtmc->getInitialStates().begin()], storm::models::sparse::Dtmc::ConstraintCollector(*dtmc), parametricSettings.exportResultPath()); + } else if (model->getType() == storm::models::ModelType::Mdp) { + std::shared_ptr> mdp = model->template as>(); + storm::modelchecker::HybridMdpPrctlModelChecker modelchecker(*mdp); + if (modelchecker.canHandle(*formula)) { + result = modelchecker.check(*formula); } + } else { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This functionality is not yet implemented."); } + return result; } -#endif - - template - void verifySymbolicModelWithHybridEngine(std::shared_ptr> model, std::vector> const& formulas) { - for (auto const& formula : formulas) { - std::cout << std::endl << "Model checking property: " << *formula << " ..."; - std::unique_ptr result; - if (model->getType() == storm::models::ModelType::Dtmc) { - std::shared_ptr> dtmc = model->template as>(); - storm::modelchecker::HybridDtmcPrctlModelChecker modelchecker(*dtmc); - if (modelchecker.canHandle(*formula)) { - result = modelchecker.check(*formula); - } - } else if (model->getType() == storm::models::ModelType::Ctmc) { - std::shared_ptr> ctmc = model->template as>(); - storm::modelchecker::HybridCtmcCslModelChecker modelchecker(*ctmc); - if (modelchecker.canHandle(*formula)) { - result = modelchecker.check(*formula); - } - } else if (model->getType() == storm::models::ModelType::Mdp) { - std::shared_ptr> mdp = model->template as>(); - storm::modelchecker::HybridMdpPrctlModelChecker modelchecker(*mdp); - if (modelchecker.canHandle(*formula)) { - result = modelchecker.check(*formula); - } - } else { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This functionality is not yet implemented."); - } - if (result) { - std::cout << " done." << std::endl; - std::cout << "Result (initial states): "; - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - std::cout << *result << std::endl; - } else { - std::cout << " skipped, because the modelling formalism is currently unsupported." << std::endl; - } - } - } - - template - void verifySymbolicModelWithSymbolicEngine(std::shared_ptr> model, std::vector> const& formulas) { - for (auto const& formula : formulas) { - std::cout << std::endl << "Model checking property: " << *formula << " ..."; - std::unique_ptr result; - if (model->getType() == storm::models::ModelType::Dtmc) { - std::shared_ptr> dtmc = model->template as>(); - storm::modelchecker::SymbolicDtmcPrctlModelChecker modelchecker(*dtmc); - if (modelchecker.canHandle(*formula)) { - result = modelchecker.check(*formula); - } - } else if (model->getType() == storm::models::ModelType::Mdp) { - std::shared_ptr> mdp = model->template as>(); - storm::modelchecker::SymbolicMdpPrctlModelChecker modelchecker(*mdp); - if (modelchecker.canHandle(*formula)) { - result = modelchecker.check(*formula); - } - } else { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This functionality is not yet implemented."); - } - if (result) { - std::cout << " done." << std::endl; - std::cout << "Result (initial states): "; - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - std::cout << *result << std::endl; - } else { - std::cout << " skipped, because the modelling formalism is currently unsupported." << std::endl; + template + std::unique_ptr verifySymbolicModelWithDdEngine(std::shared_ptr> model, std::shared_ptr const& formula) { + std::unique_ptr result; + if (model->getType() == storm::models::ModelType::Dtmc) { + std::shared_ptr> dtmc = model->template as>(); + storm::modelchecker::SymbolicDtmcPrctlModelChecker modelchecker(*dtmc); + if (modelchecker.canHandle(*formula)) { + result = modelchecker.check(*formula); } - } - } - - - template - void buildAndCheckSymbolicModel(storm::prism::Program const& program, std::vector> const& formulas) { - std::shared_ptr model = buildSymbolicModel(program, formulas); - STORM_LOG_THROW(model != nullptr, storm::exceptions::InvalidStateException, "Model could not be constructed for an unknown reason."); - - // Preprocess the model if needed. - model = preprocessModel(model, formulas); - - // Print some information about the model. - model->printModelInformationToStream(std::cout); - - // Verify the model, if a formula was given. - if (!formulas.empty()) { - if (model->isSparseModel()) { - if(storm::settings::generalSettings().isCounterexampleSet()) { - // If we were requested to generate a counterexample, we now do so for each formula. - for(auto const& formula : formulas) { - generateCounterexample(program, model->as>(), formula); - } - } else { - verifySparseModel(model->as>(), formulas); - } - } else if (model->isSymbolicModel()) { - if (storm::settings::generalSettings().getEngine() == storm::settings::modules::GeneralSettings::Engine::Hybrid) { - verifySymbolicModelWithHybridEngine(model->as>(), formulas); - } else { - verifySymbolicModelWithSymbolicEngine(model->as>(), formulas); - } - } else { - STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Invalid input model type."); + } else if (model->getType() == storm::models::ModelType::Mdp) { + std::shared_ptr> mdp = model->template as>(); + storm::modelchecker::SymbolicMdpPrctlModelChecker modelchecker(*mdp); + if (modelchecker.canHandle(*formula)) { + result = modelchecker.check(*formula); } + } else { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This functionality is not yet implemented."); } - } - - template - void buildAndCheckExplicitModel(std::vector> const& formulas) { - storm::settings::modules::GeneralSettings const& settings = storm::settings::generalSettings(); - - STORM_LOG_THROW(settings.isExplicitSet(), storm::exceptions::InvalidStateException, "Unable to build explicit model without model files."); - std::shared_ptr model = buildExplicitModel(settings.getTransitionFilename(), settings.getLabelingFilename(), settings.isStateRewardsSet() ? settings.getStateRewardsFilename() : boost::optional(), settings.isTransitionRewardsSet() ? settings.getTransitionRewardsFilename() : boost::optional(), settings.isChoiceLabelingSet() ? settings.getChoiceLabelingFilename() : boost::optional()); - // Preprocess the model if needed. - model = preprocessModel(model, formulas); - - // Print some information about the model. - model->printModelInformationToStream(std::cout); - - // Verify the model, if a formula was given. - if (!formulas.empty()) { - STORM_LOG_THROW(model->isSparseModel(), storm::exceptions::InvalidStateException, "Expected sparse model."); - verifySparseModel(model->as>(), formulas); - } + return result; } diff --git a/test/functional/parser/PrismParserTest.cpp b/test/functional/parser/PrismParserTest.cpp index 90b4f8e5d..260c4963a 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