From 12a92fc6ee231d1975d4ea0f998bc2d0e7a69f1b Mon Sep 17 00:00:00 2001 From: dehnert Date: Mon, 16 Sep 2013 18:57:11 +0200 Subject: [PATCH] Several fixes and additions to IR. Modifications to CMakeLists.txt of log4cplus to enable proper compilation under Mac OS. Fixes to coin2.nm. Added global variables to grammar and IR. Established basis for defining undefined constants of the model. Started to write MinimalLabelSetGenerator. Former-commit-id: b65bb063fa363fe14ae917877d04db6655dbd9b7 --- examples/mdp/consensus/coin2.nm | 12 +- .../log4cplus-1.1.2-rc2/CMakeLists.txt | 10 +- src/adapters/ExplicitModelAdapter.cpp | 71 +++++++++++- src/adapters/ExplicitModelAdapter.h | 4 +- .../MinimalLabelSetGenerator.h | 49 +++++++- src/ir/Module.h | 4 +- src/ir/Program.cpp | 69 ++++++++++- src/ir/Program.h | 107 +++++++++++++++++- .../expressions/IntegerConstantExpression.cpp | 4 +- src/models/AbstractModel.h | 18 ++- src/parser/prismparser/PrismGrammar.cpp | 70 +++++++----- src/parser/prismparser/PrismGrammar.h | 26 ++++- src/parser/prismparser/VariableState.h | 3 +- src/storm.cpp | 10 +- 14 files changed, 392 insertions(+), 65 deletions(-) diff --git a/examples/mdp/consensus/coin2.nm b/examples/mdp/consensus/coin2.nm index 07ec59e17..a08bb8741 100644 --- a/examples/mdp/consensus/coin2.nm +++ b/examples/mdp/consensus/coin2.nm @@ -29,18 +29,18 @@ module process1 // flip coin [] (pc1=0) -> 0.5 : (coin1'=0) & (pc1'=1) + 0.5 : (coin1'=1) & (pc1'=1); // write tails -1 (reset coin to add regularity) - [] (pc1=1) & (coin1=0) & (counter>0) -> (counter'=counter-1) & (pc1'=2) & (coin1'=0); + [] (pc1=1) & (coin1=0) & (counter>0) -> 1 : (counter'=counter-1) & (pc1'=2) & (coin1'=0); // write heads +1 (reset coin to add regularity) - [] (pc1=1) & (coin1=1) & (counter (counter'=counter+1) & (pc1'=2) & (coin1'=0); + [] (pc1=1) & (coin1=1) & (counter 1 : (counter'=counter+1) & (pc1'=2) & (coin1'=0); // check // decide tails - [] (pc1=2) & (counter<=left) -> (pc1'=3) & (coin1'=0); + [] (pc1=2) & (counter<=left) -> 1 : (pc1'=3) & (coin1'=0); // decide heads - [] (pc1=2) & (counter>=right) -> (pc1'=3) & (coin1'=1); + [] (pc1=2) & (counter>=right) -> 1 : (pc1'=3) & (coin1'=1); // flip again - [] (pc1=2) & (counter>left) & (counter (pc1'=0); + [] (pc1=2) & (counter>left) & (counter 1 : (pc1'=0); // loop (all loop together when done) - [done] (pc1=3) -> (pc1'=3); + [done] (pc1=3) -> 1 : (pc1'=3); endmodule diff --git a/resources/3rdparty/log4cplus-1.1.2-rc2/CMakeLists.txt b/resources/3rdparty/log4cplus-1.1.2-rc2/CMakeLists.txt index be347664f..319db1c64 100644 --- a/resources/3rdparty/log4cplus-1.1.2-rc2/CMakeLists.txt +++ b/resources/3rdparty/log4cplus-1.1.2-rc2/CMakeLists.txt @@ -33,9 +33,17 @@ endif (WIN32) if (MSVC) set (LOG4CPLUS_WORKING_LOCALE_DEFAULT ON) -else (MSVC) +elseif(CMAKE_COMPILER_IS_GNUCC) set (CMAKE_CXX_FLAGS "-std=c++11") set (LOG4CPLUS_WORKING_LOCALE_DEFAULT OFF) +else(CLANG) + set (CLANG ON) + if(UNIX AND NOT APPLE) + set(CLANG_STDLIB libstdc++) + else() + set(CLANG_STDLIB libc++) + endif() + set (CMAKE_CXX_FLAGS "-std=c++11 -stdlib=${CLANG_STDLIB}") endif (MSVC) option(LOG4CPLUS_WORKING_LOCALE "Define for compilers/standard libraries that support more than just the C locale." diff --git a/src/adapters/ExplicitModelAdapter.cpp b/src/adapters/ExplicitModelAdapter.cpp index 55d476e47..0d9eb7cf7 100644 --- a/src/adapters/ExplicitModelAdapter.cpp +++ b/src/adapters/ExplicitModelAdapter.cpp @@ -15,6 +15,8 @@ #include "src/models/Mdp.h" #include "src/models/Ctmdp.h" +#include + #include #include "log4cplus/logger.h" @@ -37,7 +39,60 @@ namespace storm { this->clearInternalState(); } - std::shared_ptr> ExplicitModelAdapter::getModel(std::string const& rewardModelName) { + std::shared_ptr> ExplicitModelAdapter::getModel(std::string const& constantDefinitionString, std::string const& rewardModelName) { + // Parse the string that defines the undefined constants of the model and make sure that it contains exactly + // one value for each undefined constant of the model. + std::vector definitions; + boost::split(definitions, constantDefinitionString, boost::is_any_of(",")); + for (auto& definition : definitions) { + boost::trim(definition); + + // Check whether the token could be a legal constant definition. + uint_fast64_t positionOfAssignmentOperator = definition.find('='); + if (positionOfAssignmentOperator == std::string::npos) { + throw storm::exceptions::InvalidArgumentException() << "Illegal constant definition string: syntax error."; + } + + // Now extract the variable name and the value from the string. + std::string constantName = definition.substr(0, positionOfAssignmentOperator); + boost::trim(constantName); + std::string value = definition.substr(positionOfAssignmentOperator + 1); + boost::trim(value); + + // Check whether the constant is a legal undefined constant of the program and if so, of what type it is. + if (program.hasUndefinedBooleanConstant(constantName)) { + if (value == "true") { + program.getUndefinedBooleanConstantExpression(constantName)->define(true); + } else if (value == "false") { + program.getUndefinedBooleanConstantExpression(constantName)->define(false); + } else { + throw storm::exceptions::InvalidArgumentException() << "Illegal value for boolean constant: " << value << "."; + } + } else if (program.hasUndefinedIntegerConstant(constantName)) { + try { + int_fast64_t integerValue = std::stoi(value); + program.getUndefinedIntegerConstantExpression(constantName)->define(integerValue); + } catch (std::invalid_argument const& e) { + throw storm::exceptions::InvalidArgumentException() << "Illegal value of integer constant: " << value << "."; + } catch (std::out_of_range const& e) { + throw storm::exceptions::InvalidArgumentException() << "Illegal value of integer constant: " << value << " (value too big)."; + } + } else if (program.hasUndefinedDoubleConstant(constantName)) { + try { + double doubleValue = std::stod(value); + program.getUndefinedDoubleConstantExpression(constantName)->define(doubleValue); + } catch (std::invalid_argument const& e) { + throw storm::exceptions::InvalidArgumentException() << "Illegal value of double constant: " << value << "."; + } catch (std::out_of_range const& e) { + throw storm::exceptions::InvalidArgumentException() << "Illegal value of double constant: " << value << " (value too big)."; + } + + } else { + throw storm::exceptions::InvalidArgumentException() << "Illegal constant definition string: unknown undefined constant " << constantName << "."; + } + + } + // Initialize reward model. this->rewardModel = nullptr; if (rewardModelName != "") { @@ -149,15 +204,27 @@ namespace storm { uint_fast64_t numberOfBooleanVariables = 0; // Count number of variables. + numberOfBooleanVariables += program.getNumberOfGlobalBooleanVariables(); + numberOfIntegerVariables += program.getNumberOfGlobalIntegerVariables(); for (uint_fast64_t i = 0; i < program.getNumberOfModules(); ++i) { - numberOfIntegerVariables += program.getModule(i).getNumberOfIntegerVariables(); numberOfBooleanVariables += program.getModule(i).getNumberOfBooleanVariables(); + numberOfIntegerVariables += program.getModule(i).getNumberOfIntegerVariables(); } this->booleanVariables.resize(numberOfBooleanVariables); this->integerVariables.resize(numberOfIntegerVariables); // Create variables. + for (uint_fast64_t i = 0; i < program.getNumberOfGlobalBooleanVariables(); ++i) { + storm::ir::BooleanVariable var = program.getGlobalBooleanVariable(i); + this->booleanVariables[var.getGlobalIndex()] = var; + this->booleanVariableToIndexMap[var.getName()] = var.getGlobalIndex(); + } + for (uint_fast64_t i = 0; i < program.getNumberOfGlobalIntegerVariables(); ++i) { + storm::ir::IntegerVariable var = program.getGlobalIntegerVariable(i); + this->integerVariables[var.getGlobalIndex()] = var; + this->integerVariableToIndexMap[var.getName()] = var.getGlobalIndex(); + } for (uint_fast64_t i = 0; i < program.getNumberOfModules(); ++i) { storm::ir::Module const& module = program.getModule(i); diff --git a/src/adapters/ExplicitModelAdapter.h b/src/adapters/ExplicitModelAdapter.h index 78f36f9c0..a691bb05a 100644 --- a/src/adapters/ExplicitModelAdapter.h +++ b/src/adapters/ExplicitModelAdapter.h @@ -75,12 +75,14 @@ namespace storm { * Convert the program given at construction time to an abstract model. The type of the model is the one * specified in the program. The given reward model name selects the rewards that the model will contain. * + * @param constantDefinitionString A string that contains a comma-separated definition of all undefined + * constants in the model. * @param rewardModelName The name of reward model to be added to the model. This must be either a reward * model of the program or the empty string. In the latter case, the constructed model will contain no * rewards. * @return The explicit model that was given by the probabilistic program. */ - std::shared_ptr> getModel(std::string const& rewardModelName = ""); + std::shared_ptr> getModel(std::string const& constantDefinitionString = "", std::string const& rewardModelName = ""); private: // Copying/Moving is disabled for this class diff --git a/src/counterexamples/MinimalLabelSetGenerator.h b/src/counterexamples/MinimalLabelSetGenerator.h index a827b5635..5ff42b59b 100644 --- a/src/counterexamples/MinimalLabelSetGenerator.h +++ b/src/counterexamples/MinimalLabelSetGenerator.h @@ -12,10 +12,9 @@ #include #endif -#include "src/models/Mdp.h" +#include "src/models/Mdp.h" #include "src/exceptions/NotImplementedException.h" -#include "src/storage/SparseMatrix.h" -#include "src/storage/BitVector.h" +#include "src/exceptions/InvalidArgumentException.h" namespace storm { namespace counterexamples { @@ -27,10 +26,50 @@ namespace storm { template class MinimalLabelSetGenerator { + public: + static std::unordered_set getMinimalLabelSet(storm::models::Mdp const& labeledMdp, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, T lowerProbabilityBound, bool checkThresholdFeasible = false) { #ifdef HAVE_GUROBI - // (1) Check whether its possible to exceed the threshold if checkThresholdFeasible is set. - // (2) Identify relevant labels and states. + // (0) Check whether the MDP is indeed labeled. + if (!labeledMdp.hasChoiceLabels()) { + throw storm::exceptions::InvalidArgumentException() << "Minimal label set generation is impossible for unlabeled model."; + } + + // (1) TODO: check whether its possible to exceed the threshold if checkThresholdFeasible is set. + + // (2) Identify relevant and problematic states. + storm::storage::SparseMatrix backwardTransitions = labeledMdp.getBackwardTransitions(); + storm::storage::BitVector relevantStates = storm::utility::graph::performProbGreater0A(labeledMdp, backwardTransitions, phiStates, psiStates); + relevantStates.complement(); + storm::storage::BitVector problematicStates = storm::utility::graph::performProbGreater0E(labeledMdp, backwardTransitions, phiStates, psiStates); + problematicStates &= relevantStates; + + // (3) Determine set of relevant labels. + std::unordered_set relevantLabels; + storm::storage::SparseMatrix const& transitionMatrix = labeledMdp.getTransitionMatrix(); + std::vector const& nondeterministicChoiceIndices = labeledMdp.getNondeterministicChoiceIndices(); + std::vector> const& choiceLabeling = labeledMdp.getChoiceLabeling(); + // Now traverse all choices of all relevant states and check whether there is a relevant target state. + // If so, the associated labels become relevant. + for (auto state : relevantStates) { + for (uint_fast64_t row = nondeterministicChoiceIndices[state]; row < nondeterministicChoiceIndices[state - 1]; ++row) { + for (typename storm::storage::SparseMatrix::ConstIndexIterator successorIt = transitionMatrix.constColumnIteratorBegin(row); successorIt != transitionMatrix.constColumnIteratorEnd(row); ++successorIt) { + // If there is a relevant successor, we need to add the labels of the current choice. + if (relevantStates.get(*successorIt)) { + for (auto const& label : choiceLabeling[row]) { + relevantLabels.insert(label); + } + } + } + } + } + std::cout << "relevant labels: " << std::endl; + for (auto const& label : relevantLabels) { + std::cout << "label: " << label << std::endl; + } + + return relevantLabels; + // (3) Encode resulting system as MILP problem. // (3.1) Initialize MILP solver. // (3.2) Create variables. diff --git a/src/ir/Module.h b/src/ir/Module.h index f79fa14a0..03e4d0be8 100644 --- a/src/ir/Module.h +++ b/src/ir/Module.h @@ -51,8 +51,8 @@ namespace storm { * @param moduleName The name of the module. * @param booleanVariables The boolean variables defined by the module. * @param integerVariables The integer variables defined by the module. - * @param booleanVariableToLocalIndexMap A mapping of boolean variables to global (i.e. module-local) indices. - * @param integerVariableToLocalIndexMap A mapping of integer variables to global (i.e. module-local) indices. + * @param booleanVariableToLocalIndexMap A mapping of boolean variables to local (i.e. module-local) indices. + * @param integerVariableToLocalIndexMap A mapping of integer variables to local (i.e. module-local) indices. * @param commands The commands of the module. */ Module(std::string const& moduleName, std::vector const& booleanVariables, diff --git a/src/ir/Program.cpp b/src/ir/Program.cpp index 276b59134..eb21aa9f2 100644 --- a/src/ir/Program.cpp +++ b/src/ir/Program.cpp @@ -23,8 +23,18 @@ namespace storm { // Nothing to do here. } - Program::Program(ModelType modelType, std::map> booleanUndefinedConstantExpressions, std::map> integerUndefinedConstantExpressions, std::map> doubleUndefinedConstantExpressions, std::vector modules, std::map rewards, std::map> labels) - : modelType(modelType), booleanUndefinedConstantExpressions(booleanUndefinedConstantExpressions), integerUndefinedConstantExpressions(integerUndefinedConstantExpressions), doubleUndefinedConstantExpressions(doubleUndefinedConstantExpressions), modules(modules), rewards(rewards), labels(labels), actionsToModuleIndexMap(), variableToModuleIndexMap() { + Program::Program(ModelType modelType, + std::map> const& booleanUndefinedConstantExpressions, + std::map> const& integerUndefinedConstantExpressions, + std::map> const& doubleUndefinedConstantExpressions, + std::vector const& globalBooleanVariables, + std::vector const& globalIntegerVariables, + std::map const& globalBooleanVariableToIndexMap, + std::map const& globalIntegerVariableToIndexMap, + std::vector const& modules, + std::map const& rewards, + std::map> const& labels) + : modelType(modelType), booleanUndefinedConstantExpressions(booleanUndefinedConstantExpressions), integerUndefinedConstantExpressions(integerUndefinedConstantExpressions), doubleUndefinedConstantExpressions(doubleUndefinedConstantExpressions), globalBooleanVariables(globalBooleanVariables), globalIntegerVariables(globalIntegerVariables), globalBooleanVariableToIndexMap(globalBooleanVariableToIndexMap), globalIntegerVariableToIndexMap(globalIntegerVariableToIndexMap), modules(modules), rewards(rewards), labels(labels), actionsToModuleIndexMap(), variableToModuleIndexMap() { // Now build the mapping from action names to module indices so that the lookup can later be performed quickly. for (unsigned int moduleIndex = 0; moduleIndex < this->modules.size(); moduleIndex++) { Module const& module = this->modules[moduleIndex]; @@ -88,6 +98,14 @@ namespace storm { return result.str(); } + storm::ir::BooleanVariable const& Program::getGlobalBooleanVariable(uint_fast64_t index) const { + return this->globalBooleanVariables[index]; + } + + storm::ir::IntegerVariable const& Program::getGlobalIntegerVariable(uint_fast64_t index) const { + return this->globalIntegerVariables[index]; + } + uint_fast64_t Program::getNumberOfModules() const { return this->modules.size(); } @@ -117,6 +135,14 @@ namespace storm { throw storm::exceptions::OutOfRangeException() << "Variable '" << variableName << "' does not exist."; } + uint_fast64_t Program::getNumberOfGlobalBooleanVariables() const { + return this->globalBooleanVariables.size(); + } + + uint_fast64_t Program::getNumberOfGlobalIntegerVariables() const { + return this->globalIntegerVariables.size(); + } + storm::ir::RewardModel const& Program::getRewardModel(std::string const& name) const { auto nameRewardModelPair = this->rewards.find(name); if (nameRewardModelPair == this->rewards.end()) { @@ -130,5 +156,44 @@ namespace storm { return this->labels; } + bool Program::hasUndefinedBooleanConstant(std::string const& constantName) const { + return this->booleanUndefinedConstantExpressions.find(constantName) != this->booleanUndefinedConstantExpressions.end(); + } + + std::shared_ptr Program::getUndefinedBooleanConstantExpression(std::string const& constantName) const { + auto constantExpressionPair = this->booleanUndefinedConstantExpressions.find(constantName); + if (constantExpressionPair != this->booleanUndefinedConstantExpressions.end()) { + return constantExpressionPair->second; + } else { + throw storm::exceptions::InvalidArgumentException() << "Unknown undefined boolean constant " << constantName << "."; + } + } + + bool Program::hasUndefinedIntegerConstant(std::string const& constantName) const { + return this->integerUndefinedConstantExpressions.find(constantName) != this->integerUndefinedConstantExpressions.end(); + } + + std::shared_ptr Program::getUndefinedIntegerConstantExpression(std::string const& constantName) const { + auto constantExpressionPair = this->integerUndefinedConstantExpressions.find(constantName); + if (constantExpressionPair != this->integerUndefinedConstantExpressions.end()) { + return constantExpressionPair->second; + } else { + throw storm::exceptions::InvalidArgumentException() << "Unknown undefined integer constant " << constantName << "."; + } + } + + bool Program::hasUndefinedDoubleConstant(std::string const& constantName) const { + return this->doubleUndefinedConstantExpressions.find(constantName) != this->doubleUndefinedConstantExpressions.end(); + } + + std::shared_ptr Program::getUndefinedDoubleConstantExpression(std::string const& constantName) const { + auto constantExpressionPair = this->doubleUndefinedConstantExpressions.find(constantName); + if (constantExpressionPair != this->doubleUndefinedConstantExpressions.end()) { + return constantExpressionPair->second; + } else { + throw storm::exceptions::InvalidArgumentException() << "Unknown undefined double constant " << constantName << "."; + } + } + } // namespace ir } // namepsace storm diff --git a/src/ir/Program.h b/src/ir/Program.h index 23d154110..ae92db0de 100644 --- a/src/ir/Program.h +++ b/src/ir/Program.h @@ -49,17 +49,27 @@ namespace storm { * expression nodes. * @param doubleUndefinedConstantExpressions A map of undefined double constants to their * expression nodes. + * @param globalBooleanVariables A list of global boolean variables. + * @param globalIntegerVariables A list of global integer variables. + * @param globalBooleanVariableToIndexMap A mapping from global boolean variable names to the index in the + * list of global boolean variables. + * @param globalIntegerVariableToIndexMap A mapping from global integer variable names to the index in the + * list of global integer variables. * @param modules The modules of the program. * @param rewards The reward models of the program. * @param labels The labels defined for this model. */ Program(ModelType modelType, - std::map> booleanUndefinedConstantExpressions, - std::map> integerUndefinedConstantExpressions, - std::map> doubleUndefinedConstantExpressions, - std::vector modules, - std::map rewards, - std::map> labels); + std::map> const& booleanUndefinedConstantExpressions, + std::map> const& integerUndefinedConstantExpressions, + std::map> const& doubleUndefinedConstantExpressions, + std::vector const& globalBooleanVariables, + std::vector const& globalIntegerVariables, + std::map const& globalBooleanVariableToIndexMap, + std::map const& globalIntegerVariableToIndexMap, + std::vector const& modules, + std::map const& rewards, + std::map> const& labels); /*! * Retrieves the number of modules in the program. @@ -90,6 +100,20 @@ namespace storm { */ std::string toString() const; + /*! + * Retrieves a reference to the global boolean variable with the given index. + * + * @return A reference to the global boolean variable with the given index. + */ + storm::ir::BooleanVariable const& getGlobalBooleanVariable(uint_fast64_t index) const; + + /*! + * Retrieves a reference to the global integer variable with the given index. + * + * @return A reference to the global integer variable with the given index. + */ + storm::ir::IntegerVariable const& getGlobalIntegerVariable(uint_fast64_t index) const; + /*! * Retrieves the set of actions present in this module. * @@ -114,6 +138,20 @@ namespace storm { */ uint_fast64_t getModuleIndexForVariable(std::string const& variableName) const; + /*! + * Retrieves the number of global boolean variables of the program. + * + * @return The number of global boolean variables of the program. + */ + uint_fast64_t getNumberOfGlobalBooleanVariables() const; + + /*! + * Retrieves the number of global integer variables of the program. + * + * @return The number of global integer variables of the program. + */ + uint_fast64_t getNumberOfGlobalIntegerVariables() const; + /*! * Retrieves the reward model with the given name. * @@ -129,6 +167,51 @@ namespace storm { */ std::map> const& getLabels() const; + /*! + * Retrieves whether the given constant name is an undefined boolean constant of the program. + * + * @return True if the given constant name is an undefined boolean constant of the program. + */ + bool hasUndefinedBooleanConstant(std::string const& constantName) const; + + /*! + * Retrieves the expression associated with the given undefined boolean constant. + * + * @param constantName The name of the undefined boolean constant for which to retrieve the expression. + * @return The expression associated with the given undefined boolean constant. + */ + std::shared_ptr getUndefinedBooleanConstantExpression(std::string const& constantName) const; + + /*! + * Retrieves whether the given constant name is an undefined integer constant of the program. + * + * @return True if the given constant name is an undefined integer constant of the program. + */ + bool hasUndefinedIntegerConstant(std::string const& constantName) const; + + /*! + * Retrieves the expression associated with the given undefined integer constant. + * + * @param constantName The name of the undefined integer constant for which to retrieve the expression. + * @return The expression associated with the given undefined integer constant. + */ + std::shared_ptr getUndefinedIntegerConstantExpression(std::string const& constantName) const; + + /*! + * Retrieves whether the given constant name is an undefined double constant of the program. + * + * @return True if the given constant name is an undefined double constant of the program. + */ + bool hasUndefinedDoubleConstant(std::string const& constantName) const; + + /*! + * Retrieves the expression associated with the given undefined double constant. + * + * @param constantName The name of the undefined double constant for which to retrieve the expression. + * @return The expression associated with the given undefined double constant. + */ + std::shared_ptr getUndefinedDoubleConstantExpression(std::string const& constantName) const; + private: // The type of the model. ModelType modelType; @@ -142,6 +225,18 @@ namespace storm { // A map of undefined double constants to their expressions nodes. std::map> doubleUndefinedConstantExpressions; + // A list of global boolean variables. + std::vector globalBooleanVariables; + + // A list of global integer variables. + std::vector globalIntegerVariables; + + // A mapping from global boolean variable names to their indices. + std::map globalBooleanVariableToIndexMap; + + // A mapping from global integer variable names to their indices. + std::map globalIntegerVariableToIndexMap; + // The modules associated with the program. std::vector modules; diff --git a/src/ir/expressions/IntegerConstantExpression.cpp b/src/ir/expressions/IntegerConstantExpression.cpp index 4daa4c244..40676ab7b 100644 --- a/src/ir/expressions/IntegerConstantExpression.cpp +++ b/src/ir/expressions/IntegerConstantExpression.cpp @@ -6,7 +6,7 @@ */ #include - +#include #include "IntegerConstantExpression.h" namespace storm { @@ -14,11 +14,13 @@ namespace storm { namespace expressions { IntegerConstantExpression::IntegerConstantExpression(std::string const& constantName) : ConstantExpression(int_, constantName), value(0), defined(false) { + std::cout << "Creating constant integer expression with constant name " << constantName << "[" << this << "]" << std::endl; // Nothing to do here. } IntegerConstantExpression::IntegerConstantExpression(IntegerConstantExpression const& integerConstantExpression) : ConstantExpression(integerConstantExpression), value(integerConstantExpression.value), defined(integerConstantExpression.defined) { + std::cout << "Creating constant integer expression as copy of " << integerConstantExpression.toString() << "[" << this << "]" << std::endl; // Nothing to do here. } diff --git a/src/models/AbstractModel.h b/src/models/AbstractModel.h index 27aef7480..7790bd7b9 100644 --- a/src/models/AbstractModel.h +++ b/src/models/AbstractModel.h @@ -18,7 +18,7 @@ namespace models { * @brief Enumeration of all supported types of models. */ enum ModelType { - Unknown, DTMC, CTMC, MDP, UPDATE_LABELED_MDP, CTMDP + Unknown, DTMC, CTMC, MDP, CTMDP }; /*! @@ -345,6 +345,14 @@ class AbstractModel: public std::enable_shared_from_this> { std::vector const& getStateRewardVector() const { return stateRewardVector.get(); } + + /*! + * Returns the labels for the choices of the model, if there are any. + * @return The labels for the choices of the model. + */ + std::vector> const& getChoiceLabeling() const { + return choiceLabeling.get(); + } /*! * Returns the set of labels with which the given state is labeled. @@ -379,6 +387,14 @@ class AbstractModel: public std::enable_shared_from_this> { bool hasTransitionRewards() const { return transitionRewardMatrix; } + + /*! + * Retrieves whether this model has a labeling for the choices. + * @return True if this model has a labeling. + */ + bool hasChoiceLabels() const { + return choiceLabeling; + } /*! * Retrieves the size of the internal representation of the model in memory. diff --git a/src/parser/prismparser/PrismGrammar.cpp b/src/parser/prismparser/PrismGrammar.cpp index 8d3ed0fc8..99dbf0efd 100644 --- a/src/parser/prismparser/PrismGrammar.cpp +++ b/src/parser/prismparser/PrismGrammar.cpp @@ -50,16 +50,16 @@ void PrismGrammar::addLabel(std::string const& name, std::shared_ptr const& value, std::map& variableToAssignmentMap) { - this->state->assignedLocalIntegerVariables_.add(variable, variable); + this->state->assignedIntegerVariables_.add(variable, variable); variableToAssignmentMap[variable] = Assignment(variable, value); } void PrismGrammar::addBooleanAssignment(std::string const& variable, std::shared_ptr const& value, std::map& variableToAssigmentMap) { - this->state->assignedLocalBooleanVariables_.add(variable, variable); + this->state->assignedBooleanVariables_.add(variable, variable); variableToAssigmentMap[variable] = Assignment(variable, value); } -Module PrismGrammar::renameModule(std::string const& newName, std::string const& oldName, std::map& renaming) { +Module PrismGrammar::renameModule(std::string const& newName, std::string const& oldName, std::map const& renaming) { this->state->moduleNames_.add(newName, newName); Module* old = this->moduleMap_.find(oldName); if (old == nullptr) { @@ -78,34 +78,40 @@ Module PrismGrammar::createModule(std::string const& name, std::vector const& lower, std::shared_ptr const& upper, std::shared_ptr const& init, std::vector& vars, std::map& varids) { +void PrismGrammar::createIntegerVariable(std::string const& name, std::shared_ptr const& lower, std::shared_ptr const& upper, std::shared_ptr const& init, std::vector& vars, std::map& varids, bool isGlobalVariable) { uint_fast64_t id = this->state->addIntegerVariable(name); uint_fast64_t newLocalIndex = this->state->nextLocalIntegerVariableIndex; vars.emplace_back(newLocalIndex, id, name, lower, upper, init); varids[name] = newLocalIndex; ++this->state->nextLocalIntegerVariableIndex; this->state->localIntegerVariables_.add(name, name); + if (isGlobalVariable) { + this->state->globalIntegerVariables_.add(name, name); + } } -void PrismGrammar::createBooleanVariable(std::string const& name, std::shared_ptr const& init, std::vector& vars, std::map& varids) { +void PrismGrammar::createBooleanVariable(std::string const& name, std::shared_ptr const& init, std::vector& vars, std::map& varids, bool isGlobalVariable) { uint_fast64_t id = this->state->addBooleanVariable(name); uint_fast64_t newLocalIndex = this->state->nextLocalBooleanVariableIndex; vars.emplace_back(newLocalIndex, id, name, init); varids[name] = newLocalIndex; ++this->state->nextLocalBooleanVariableIndex; this->state->localBooleanVariables_.add(name, name); + if (isGlobalVariable) { + this->state->globalBooleanVariables_.add(name, name); + } } StateReward createStateReward(std::shared_ptr guard, std::shared_ptr reward) { return StateReward(guard, reward); } -TransitionReward createTransitionReward(std::string label, std::shared_ptr guard, std::shared_ptr reward) { +TransitionReward createTransitionReward(std::string const& label, std::shared_ptr guard, std::shared_ptr reward) { return TransitionReward(label, guard, reward); } -void createRewardModel(std::string name, std::vector& stateRewards, std::vector& transitionRewards, std::map& mapping) { +void createRewardModel(std::string const& name, std::vector& stateRewards, std::vector& transitionRewards, std::map& mapping) { mapping[name] = RewardModel(name, stateRewards, transitionRewards); } -Update createUpdate(std::shared_ptr likelihood, std::map& bools, std::map ints) { +Update createUpdate(std::shared_ptr likelihood, std::map const& bools, std::map const& ints) { return Update(likelihood, bools, ints); } Command PrismGrammar::createCommand(std::string const& label, std::shared_ptr guard, std::vector const& updates) { @@ -114,13 +120,17 @@ Command PrismGrammar::createCommand(std::string const& label, std::shared_ptr> undefBoolConst, - std::map> undefIntConst, - std::map> undefDoubleConst, - std::vector modules, - std::map rewards, - std::map> labels) { - return Program(modelType, undefBoolConst, undefIntConst, undefDoubleConst, modules, rewards, labels); + std::map> const& undefBoolConst, + std::map> const& undefIntConst, + std::map> const& undefDoubleConst, + GlobalVariableInformation const& globalVariableInformation, + std::vector const& modules, + std::map const& rewards, + std::map> const& labels) { + return Program(modelType, undefBoolConst, undefIntConst, undefDoubleConst, + globalVariableInformation.booleanVariables, globalVariableInformation.integerVariables, + globalVariableInformation.booleanVariableToIndexMap, + globalVariableInformation.integerVariableToIndexMap, modules, rewards, labels); } PrismGrammar::PrismGrammar() : PrismGrammar::base_type(start), state(new VariableState()) { @@ -144,10 +154,10 @@ PrismGrammar::PrismGrammar() : PrismGrammar::base_type(start), state(new Variabl commandName %= this->state->commandNames_; commandName.name("command name"); - unassignedLocalBooleanVariableName %= this->state->localBooleanVariables_ - this->state->assignedLocalBooleanVariables_; - unassignedLocalBooleanVariableName.name("unassigned local boolean variable"); - unassignedLocalIntegerVariableName %= this->state->localIntegerVariables_ - this->state->assignedLocalIntegerVariables_; - unassignedLocalIntegerVariableName.name("unassigned local integer variable"); + unassignedLocalBooleanVariableName %= (this->state->localBooleanVariables_ | this->state->globalBooleanVariables_) - this->state->assignedBooleanVariables_; + unassignedLocalBooleanVariableName.name("unassigned local/global boolean variable"); + unassignedLocalIntegerVariableName %= (this->state->localIntegerVariables_ | this->state->globalIntegerVariables_) - this->state->assignedIntegerVariables_; + unassignedLocalIntegerVariableName.name("unassigned local/global integer variable"); // This block defines all entities that are needed for parsing a single command. assignmentDefinition = @@ -157,7 +167,7 @@ PrismGrammar::PrismGrammar() : PrismGrammar::base_type(start), state(new Variabl assignmentDefinitionList = assignmentDefinition(qi::_r1, qi::_r2) % "&"; assignmentDefinitionList.name("assignment list"); updateDefinition = ( - ConstDoubleExpressionGrammar::instance(this->state) > qi::lit(":")[phoenix::clear(phoenix::ref(this->state->assignedLocalBooleanVariables_)), phoenix::clear(phoenix::ref(this->state->assignedLocalIntegerVariables_))] > assignmentDefinitionList(qi::_a, qi::_b))[qi::_val = phoenix::bind(&createUpdate, qi::_1, qi::_a, qi::_b)]; + ConstDoubleExpressionGrammar::instance(this->state) > qi::lit(":")[phoenix::clear(phoenix::ref(this->state->assignedBooleanVariables_)), phoenix::clear(phoenix::ref(this->state->assignedIntegerVariables_))] > assignmentDefinitionList(qi::_a, qi::_b))[qi::_val = phoenix::bind(&createUpdate, qi::_1, qi::_a, qi::_b)]; updateDefinition.name("update"); updateListDefinition = +updateDefinition % "+"; updateListDefinition.name("update list"); @@ -170,17 +180,13 @@ PrismGrammar::PrismGrammar() : PrismGrammar::base_type(start), state(new Variabl // This block defines all entities that are needed for parsing variable definitions. booleanVariableDefinition = (FreeIdentifierGrammar::instance(this->state) >> qi::lit(":") >> qi::lit("bool") > -(qi::lit("init") > ConstBooleanExpressionGrammar::instance(this->state)[qi::_b = phoenix::construct>(qi::_1)]) > qi::lit(";")) - [ - phoenix::bind(&PrismGrammar::createBooleanVariable, this, qi::_1, qi::_b, qi::_r1, qi::_r2) - ]; + [phoenix::bind(&PrismGrammar::createBooleanVariable, this, qi::_1, qi::_b, qi::_r1, qi::_r2, qi::_r3)]; booleanVariableDefinition.name("boolean variable declaration"); integerVariableDefinition = (FreeIdentifierGrammar::instance(this->state) >> qi::lit(":") >> qi::lit("[") > ConstIntegerExpressionGrammar::instance(this->state) > qi::lit("..") > ConstIntegerExpressionGrammar::instance(this->state) > qi::lit("]") > -(qi::lit("init") > ConstIntegerExpressionGrammar::instance(this->state)[qi::_b = phoenix::construct>(qi::_1)]) > qi::lit(";")) - [ - phoenix::bind(&PrismGrammar::createIntegerVariable, this, qi::_1, qi::_2, qi::_3, qi::_b, qi::_r1, qi::_r2) - ]; + [phoenix::bind(&PrismGrammar::createIntegerVariable, this, qi::_1, qi::_2, qi::_3, qi::_b, qi::_r1, qi::_r2, qi::_r3)]; integerVariableDefinition.name("integer variable declaration"); - variableDefinition = (booleanVariableDefinition(qi::_r1, qi::_r3) | integerVariableDefinition(qi::_r2, qi::_r4)); + variableDefinition = (booleanVariableDefinition(qi::_r1, qi::_r3, false) | integerVariableDefinition(qi::_r2, qi::_r4, false)); variableDefinition.name("variable declaration"); // This block defines all entities that are needed for parsing a module. @@ -198,6 +204,10 @@ PrismGrammar::PrismGrammar() : PrismGrammar::base_type(start), state(new Variabl moduleDefinitionList %= +(moduleDefinition | moduleRenaming); moduleDefinitionList.name("module list"); + // This block defines all entities that are needed for parsing global variable definitions. + globalVariableDefinitionList = *(qi::lit("global") > (booleanVariableDefinition(bind(&GlobalVariableInformation::booleanVariables, qi::_r1), bind(&GlobalVariableInformation::booleanVariableToIndexMap, qi::_r1), true) | integerVariableDefinition(bind(&GlobalVariableInformation::integerVariables, qi::_r1), bind(&GlobalVariableInformation::integerVariableToIndexMap, qi::_r1), true))); + globalVariableDefinitionList.name("global variable declaration list"); + // This block defines all entities that are needed for parsing constant definitions. definedBooleanConstantDefinition = (qi::lit("const") >> qi::lit("bool") >> FreeIdentifierGrammar::instance(this->state) >> qi::lit("=") > ConstBooleanExpressionGrammar::instance(this->state) > qi::lit(";"))[phoenix::bind(this->state->booleanConstants_.add, qi::_1, qi::_2), phoenix::bind(this->state->allConstantNames_.add, qi::_1, qi::_1), qi::_val = qi::_2]; definedBooleanConstantDefinition.name("defined boolean constant declaration"); @@ -227,10 +237,10 @@ PrismGrammar::PrismGrammar() : PrismGrammar::base_type(start), state(new Variabl start = ( modelTypeDefinition > constantDefinitionList(qi::_a, qi::_b, qi::_c) > + globalVariableDefinitionList(qi::_d) > moduleDefinitionList > - rewardDefinitionList(qi::_d) > - labelDefinitionList(qi::_e) - )[qi::_val = phoenix::bind(&createProgram, qi::_1, qi::_a, qi::_b, qi::_c, qi::_2, qi::_d, qi::_e)]; + rewardDefinitionList(qi::_e) > + labelDefinitionList(qi::_f))[qi::_val = phoenix::bind(&createProgram, qi::_1, qi::_a, qi::_b, qi::_c, qi::_d, qi::_2, qi::_e, qi::_f)]; start.name("probabilistic program declaration"); } diff --git a/src/parser/prismparser/PrismGrammar.h b/src/parser/prismparser/PrismGrammar.h index bb0b9e8f7..d953d67fa 100644 --- a/src/parser/prismparser/PrismGrammar.h +++ b/src/parser/prismparser/PrismGrammar.h @@ -31,6 +31,13 @@ namespace prism { using namespace storm::ir; using namespace storm::ir::expressions; +struct GlobalVariableInformation { + std::vector booleanVariables; + std::vector integerVariables; + std::map booleanVariableToIndexMap; + std::map integerVariableToIndexMap; +}; + /*! * The Boost spirit grammar for the PRISM language. Returns the intermediate representation of * the input that complies with the PRISM syntax. @@ -42,6 +49,7 @@ class PrismGrammar : public qi::grammar< std::map>, std::map>, std::map>, + GlobalVariableInformation, std::map, std::map> >, @@ -68,7 +76,7 @@ private: std::shared_ptr state; struct qi::symbols moduleMap_; - + // The starting point of the grammar. qi::rule< Iterator, @@ -77,6 +85,7 @@ private: std::map>, std::map>, std::map>, + GlobalVariableInformation, std::map, std::map> >, @@ -84,6 +93,9 @@ private: qi::rule modelTypeDefinition; qi::rule>&, std::map>&, std::map>&), Skipper> constantDefinitionList; qi::rule(), Skipper> moduleDefinitionList; + + // Rules for global variable definitions + qi::rule globalVariableDefinitionList; // Rules for module definition. qi::rule, std::vector, std::map, std::map>, Skipper> moduleDefinition; @@ -91,8 +103,8 @@ private: // Rules for variable definitions. qi::rule&, std::vector&, std::map&, std::map&), Skipper> variableDefinition; - qi::rule&, std::map&), qi::locals>, Skipper> booleanVariableDefinition; - qi::rule&, std::map&), qi::locals>, Skipper> integerVariableDefinition; + qi::rule&, std::map&, bool), qi::locals>, Skipper> booleanVariableDefinition; + qi::rule&, std::map&, bool), qi::locals>, Skipper> integerVariableDefinition; // Rules for command definitions. qi::rule, Skipper> commandDefinition; @@ -180,7 +192,7 @@ private: * @param oldName The name of the module that is to be copied (modulo renaming). * @param renaming A mapping from identifiers to their new names. */ - Module renameModule(std::string const& name, std::string const& oldName, std::map& renaming); + Module renameModule(std::string const& name, std::string const& oldName, std::map const& renaming); /*! * Creates a new module with the given name, boolean and integer variables and commands. @@ -203,8 +215,9 @@ private: * @param upper The expression that defines the upper bound of the domain. * @param init The expression that defines the initial value of the variable. * @param integerVariableToGlobalIndexMap A mapping of integer variables to global indices. + * @param isGlobalVariable A flag indicating whether the variable is supposed to be global or not. */ - void createIntegerVariable(std::string const& name, std::shared_ptr const& lower, std::shared_ptr const& upper, std::shared_ptr const& init, std::vector& integerVariables, std::map& integerVariableToGlobalIndexMap); + void createIntegerVariable(std::string const& name, std::shared_ptr const& lower, std::shared_ptr const& upper, std::shared_ptr const& init, std::vector& integerVariables, std::map& integerVariableToGlobalIndexMap, bool isGlobalVariable); /*! * Creates an boolean variable with the given name and initial value and adds it to the @@ -213,8 +226,9 @@ private: * @param name The name of the boolean variable. * @param init The expression that defines the initial value of the variable. * @param booleanVariableToGlobalIndexMap A mapping of boolean variables to global indices. + * @param isGlobalVariable A flag indicating whether the variable is supposed to be global or not. */ - void createBooleanVariable(std::string const& name, std::shared_ptr const& init, std::vector& booleanVariables, std::map& booleanVariableToGlobalIndexMap); + void createBooleanVariable(std::string const& name, std::shared_ptr const& init, std::vector& booleanVariables, std::map& booleanVariableToGlobalIndexMap, bool isGlobalVariable); /*! * Creates a command with the given label, guard and updates. diff --git a/src/parser/prismparser/VariableState.h b/src/parser/prismparser/VariableState.h index 1895eefe0..fe10d86cf 100644 --- a/src/parser/prismparser/VariableState.h +++ b/src/parser/prismparser/VariableState.h @@ -119,7 +119,8 @@ public: // A structure representing the identity function over identifier names. struct variableNamesStruct : qi::symbols { } integerVariableNames_, booleanVariableNames_, commandNames_, labelNames_, allConstantNames_, moduleNames_, - localBooleanVariables_, localIntegerVariables_, assignedLocalBooleanVariables_, assignedLocalIntegerVariables_; + localBooleanVariables_, localIntegerVariables_, assignedBooleanVariables_, assignedIntegerVariables_, + globalBooleanVariables_, globalIntegerVariables_; /*! * Adds a new boolean variable with the given name. diff --git a/src/storm.cpp b/src/storm.cpp index 537c52d5e..eb39452cb 100644 --- a/src/storm.cpp +++ b/src/storm.cpp @@ -332,8 +332,16 @@ int main(const int argc, const char* argv[]) { } else if (s->isSet("symbolic")) { std::string const arg = s->getOptionByLongName("symbolic").getArgument(0).getValueAsString(); storm::adapters::ExplicitModelAdapter adapter(storm::parser::PrismParserFromFile(arg)); - std::shared_ptr> model = adapter.getModel(); + std::shared_ptr> model = adapter.getModel("K=2"); model->printModelInformationToStream(std::cout); + + if (model->getType() == storm::models::MDP) { + std::shared_ptr> labeledMdp = model->as>(); + storm::storage::BitVector const& finishedStates = labeledMdp->getLabeledStates("finished"); + storm::storage::BitVector const& allCoinsEqualStates = labeledMdp->getLabeledStates("agree"); + storm::storage::BitVector targetStates = finishedStates & allCoinsEqualStates; + storm::counterexamples::MinimalLabelSetGenerator::getMinimalLabelSet(*labeledMdp, storm::storage::BitVector(labeledMdp->getNumberOfStates(), true), targetStates, 0.4, true); + } } // Perform clean-up and terminate.