From 78d5f89ea26371cb61f8776f5408cf45e31d0825 Mon Sep 17 00:00:00 2001 From: dehnert Date: Fri, 8 Nov 2013 00:06:21 +0100 Subject: [PATCH 1/7] Added formula support for PRISM models. ExplicitModelAdapter now properly checks for out-of-bound values for integer variables. Former-commit-id: d990e1b3883ef9fabd3123b23f4823059a0ab450 --- src/adapters/ExplicitModelAdapter.h | 9 ++++++++- .../prismparser/BooleanExpressionGrammar.cpp | 4 ++-- .../ConstBooleanExpressionGrammar.cpp | 4 ++-- .../prismparser/ConstDoubleExpressionGrammar.cpp | 4 ++-- .../ConstIntegerExpressionGrammar.cpp | 4 ++-- .../prismparser/IntegerExpressionGrammar.cpp | 4 ++-- src/parser/prismparser/PrismGrammar.cpp | 16 ++++++++++++++++ src/parser/prismparser/PrismGrammar.h | 9 +++++++++ src/parser/prismparser/VariableState.cpp | 7 +++++++ src/parser/prismparser/VariableState.h | 2 +- src/utility/IRUtility.h | 14 +++++++++++++- 11 files changed, 64 insertions(+), 13 deletions(-) diff --git a/src/adapters/ExplicitModelAdapter.h b/src/adapters/ExplicitModelAdapter.h index a2924c97e..4b21e29d6 100644 --- a/src/adapters/ExplicitModelAdapter.h +++ b/src/adapters/ExplicitModelAdapter.h @@ -168,7 +168,14 @@ namespace storm { setValue(newState, variableInformation.booleanVariableToIndexMap.at(variableAssignmentPair.first), variableAssignmentPair.second.getExpression()->getValueAsBool(baseState)); } for (auto variableAssignmentPair : update.getIntegerAssignments()) { - setValue(newState, variableInformation.integerVariableToIndexMap.at(variableAssignmentPair.first), variableAssignmentPair.second.getExpression()->getValueAsInt(baseState)); + int_fast64_t newVariableValue = variableAssignmentPair.second.getExpression()->getValueAsInt(baseState); + bool isLegalValueForVariable = newVariableValue >= variableInformation.lowerBounds.at(variableInformation.integerVariableToIndexMap.at(variableAssignmentPair.first)) && newVariableValue <= variableInformation.upperBounds.at(variableInformation.integerVariableToIndexMap.at(variableAssignmentPair.first)); + + if (!isLegalValueForVariable) { + throw storm::exceptions::InvalidStateException() << "Invalid value '" << newVariableValue << "' for variable \"" << variableInformation.integerVariables.at(variableInformation.integerVariableToIndexMap.at(variableAssignmentPair.first)).getName() << "\". Please strengthen the guards if necessary or enlarge the domains of the variables."; + } + + setValue(newState, variableInformation.integerVariableToIndexMap.at(variableAssignmentPair.first), newVariableValue); } return newState; } diff --git a/src/parser/prismparser/BooleanExpressionGrammar.cpp b/src/parser/prismparser/BooleanExpressionGrammar.cpp index 380fd8ac9..a7d9366f8 100644 --- a/src/parser/prismparser/BooleanExpressionGrammar.cpp +++ b/src/parser/prismparser/BooleanExpressionGrammar.cpp @@ -22,7 +22,7 @@ namespace storm { notExpression = atomicBooleanExpression[qi::_val = qi::_1] | (qi::lit("!") >> atomicBooleanExpression)[qi::_val = phoenix::bind(&BaseGrammar::createNot, this, qi::_1)]; notExpression.name("boolean expression"); - atomicBooleanExpression %= (relativeExpression | booleanVariableExpression | qi::lit("(") >> booleanExpression >> qi::lit(")") | ConstBooleanExpressionGrammar::instance(this->state)); + atomicBooleanExpression %= (relativeExpression | booleanVariableExpression | this->state->constantBooleanFormulas_ | this->state->booleanFormulas_ | qi::lit("(") >> booleanExpression >> qi::lit(")") | ConstBooleanExpressionGrammar::instance(this->state)); atomicBooleanExpression.name("boolean expression"); relativeExpression = (IntegerExpressionGrammar::instance(this->state) >> relations_ >> IntegerExpressionGrammar::instance(this->state))[qi::_val = phoenix::bind(&BaseGrammar::createRelation, this, qi::_1, qi::_2, qi::_3)]; @@ -39,4 +39,4 @@ namespace storm { } // namespace prism } // namespace parser -} // namespace storm \ No newline at end of file +} // namespace storm diff --git a/src/parser/prismparser/ConstBooleanExpressionGrammar.cpp b/src/parser/prismparser/ConstBooleanExpressionGrammar.cpp index fa1fccab2..a5ce0567d 100644 --- a/src/parser/prismparser/ConstBooleanExpressionGrammar.cpp +++ b/src/parser/prismparser/ConstBooleanExpressionGrammar.cpp @@ -21,7 +21,7 @@ namespace prism { constantNotExpression = constantAtomicBooleanExpression[qi::_val = qi::_1] | (qi::lit("!") >> constantAtomicBooleanExpression)[qi::_val = phoenix::bind(&BaseGrammar::createNot, this, qi::_1)]; constantNotExpression.name("constant boolean expression"); - constantAtomicBooleanExpression %= (constantRelativeExpression | qi::lit("(") >> constantBooleanExpression >> qi::lit(")") | booleanLiteralExpression | booleanConstantExpression); + constantAtomicBooleanExpression %= (constantRelativeExpression | this->state->constantBooleanFormulas_ | qi::lit("(") >> constantBooleanExpression >> qi::lit(")") | booleanLiteralExpression | booleanConstantExpression); constantAtomicBooleanExpression.name("constant boolean expression"); constantRelativeExpression = (ConstIntegerExpressionGrammar::instance(this->state) >> relations_ >> ConstIntegerExpressionGrammar::instance(this->state))[qi::_val = phoenix::bind(&BaseGrammar::createRelation, this, qi::_1, qi::_2, qi::_3)]; @@ -35,4 +35,4 @@ namespace prism { } } } -} \ No newline at end of file +} diff --git a/src/parser/prismparser/ConstDoubleExpressionGrammar.cpp b/src/parser/prismparser/ConstDoubleExpressionGrammar.cpp index 0e3b45622..18cd5ae31 100644 --- a/src/parser/prismparser/ConstDoubleExpressionGrammar.cpp +++ b/src/parser/prismparser/ConstDoubleExpressionGrammar.cpp @@ -18,7 +18,7 @@ ConstDoubleExpressionGrammar::ConstDoubleExpressionGrammar(std::shared_ptr> constantDoubleExpression >> qi::lit(")") | doubleConstantExpression); + constantAtomicDoubleExpression %= (qi::lit("(") >> constantDoubleExpression >> qi::lit(")") | this->state->constantDoubleFormulas_ | this->state->constantIntegerFormulas_ | doubleConstantExpression); constantAtomicDoubleExpression.name("constant double expression"); doubleConstantExpression %= (this->state->doubleConstants_ | this->state->integerConstants_ | doubleLiteralExpression); @@ -31,4 +31,4 @@ ConstDoubleExpressionGrammar::ConstDoubleExpressionGrammar(std::shared_ptr> constantIntegerExpression >> qi::lit(")") | integerConstantExpression); + constantAtomicIntegerExpression %= (constantIntegerMinMaxExpression | constantIntegerFloorCeilExpression | this->state->constantIntegerFormulas_ | qi::lit("(") >> constantIntegerExpression >> qi::lit(")") | integerConstantExpression); constantAtomicIntegerExpression.name("constant integer expression"); constantIntegerMinMaxExpression = ((qi::lit("min")[qi::_a = true] | qi::lit("max")[qi::_a = false]) >> qi::lit("(") >> constantIntegerExpression >> qi::lit(",") >> constantIntegerExpression >> qi::lit(")"))[qi::_val = phoenix::bind(&BaseGrammar::createIntMinMax, this, qi::_a, qi::_1, qi::_2)]; @@ -38,4 +38,4 @@ namespace storm { } // namespace prism } // namespace parser -} // namespace storm \ No newline at end of file +} // namespace storm diff --git a/src/parser/prismparser/IntegerExpressionGrammar.cpp b/src/parser/prismparser/IntegerExpressionGrammar.cpp index 19170455c..3bcfd4d4f 100644 --- a/src/parser/prismparser/IntegerExpressionGrammar.cpp +++ b/src/parser/prismparser/IntegerExpressionGrammar.cpp @@ -19,7 +19,7 @@ namespace storm { integerMultExpression %= atomicIntegerExpression[qi::_val = qi::_1] >> *(qi::lit("*") >> atomicIntegerExpression[qi::_val = phoenix::bind(&BaseGrammar::createIntMult, this, qi::_val, qi::_1)]); integerMultExpression.name("integer expression"); - atomicIntegerExpression %= (integerMinMaxExpression | integerFloorCeilExpression | qi::lit("(") >> integerExpression >> qi::lit(")") | integerVariableExpression | ConstIntegerExpressionGrammar::instance(this->state)); + atomicIntegerExpression %= (integerMinMaxExpression | integerFloorCeilExpression | this->state->constantIntegerFormulas_ | this->state->integerFormulas_ | qi::lit("(") >> integerExpression >> qi::lit(")") | integerVariableExpression | ConstIntegerExpressionGrammar::instance(this->state)); atomicIntegerExpression.name("integer expression"); integerMinMaxExpression = ((qi::lit("min")[qi::_a = true] | qi::lit("max")[qi::_a = false]) >> qi::lit("(") >> integerExpression >> qi::lit(",") >> integerExpression >> qi::lit(")"))[qi::_val = phoenix::bind(&BaseGrammar::createIntMinMax, this, qi::_a, qi::_1, qi::_2)]; @@ -39,4 +39,4 @@ namespace storm { } } -} \ No newline at end of file +} diff --git a/src/parser/prismparser/PrismGrammar.cpp b/src/parser/prismparser/PrismGrammar.cpp index 220663a99..b6de4f0f4 100644 --- a/src/parser/prismparser/PrismGrammar.cpp +++ b/src/parser/prismparser/PrismGrammar.cpp @@ -242,12 +242,28 @@ namespace storm { constantDefinitionList = *(definedConstantDefinition | undefinedConstantDefinition(qi::_r1, qi::_r2, qi::_r3)); constantDefinitionList.name("constant declaration list"); + constantBooleanFormulaDefinition = (qi::lit("formula") >> FreeIdentifierGrammar::instance(this->state) >> qi::lit("=") >> ConstBooleanExpressionGrammar::instance(this->state) >> qi::lit(";"))[phoenix::bind(this->state->constantBooleanFormulas_.add, qi::_1, qi::_2)]; + constantBooleanFormulaDefinition.name("constant boolean formula definition"); + booleanFormulaDefinition = (qi::lit("formula") >> FreeIdentifierGrammar::instance(this->state) >> qi::lit("=") >> BooleanExpressionGrammar::instance(this->state) >> qi::lit(";"))[phoenix::bind(this->state->booleanFormulas_.add, qi::_1, qi::_2)]; + booleanFormulaDefinition.name("boolean formula definition"); + constantIntegerFormulaDefinition = (qi::lit("formula") >> FreeIdentifierGrammar::instance(this->state) >> qi::lit("=") >> ConstIntegerExpressionGrammar::instance(this->state) >> qi::lit(";"))[phoenix::bind(this->state->constantIntegerFormulas_.add, qi::_1, qi::_2)]; + constantIntegerFormulaDefinition.name("constant integer formula definition"); + integerFormulaDefinition = (qi::lit("formula") >> FreeIdentifierGrammar::instance(this->state) >> qi::lit("=") >> IntegerExpressionGrammar::instance(this->state) >> qi::lit(";"))[phoenix::bind(this->state->integerFormulas_.add, qi::_1, qi::_2)]; + integerFormulaDefinition.name("integer formula definition"); + constantDoubleFormulaDefinition = (qi::lit("formula") >> FreeIdentifierGrammar::instance(this->state) >> qi::lit("=") >> ConstDoubleExpressionGrammar::instance(this->state) >> qi::lit(";"))[phoenix::bind(this->state->constantDoubleFormulas_.add, qi::_1, qi::_2)]; + constantDoubleFormulaDefinition.name("constant double formula definition"); + formulaDefinition = constantBooleanFormulaDefinition | booleanFormulaDefinition | constantIntegerFormulaDefinition | integerFormulaDefinition | constantDoubleFormulaDefinition; + formulaDefinition.name("formula definition"); + formulaDefinitionList = *formulaDefinition; + formulaDefinitionList.name("formula definition list"); + // This block defines all entities that are needed for parsing a program. modelTypeDefinition = modelType_; modelTypeDefinition.name("model type"); start = (qi::eps > modelTypeDefinition > constantDefinitionList(qi::_a, qi::_b, qi::_c) > + formulaDefinitionList > globalVariableDefinitionList(qi::_d) > moduleDefinitionList > rewardDefinitionList(qi::_e) > diff --git a/src/parser/prismparser/PrismGrammar.h b/src/parser/prismparser/PrismGrammar.h index d71fefd9f..57ba55c5b 100644 --- a/src/parser/prismparser/PrismGrammar.h +++ b/src/parser/prismparser/PrismGrammar.h @@ -139,6 +139,15 @@ namespace storm { qi::rule(), Skipper> definedIntegerConstantDefinition; qi::rule(), Skipper> definedDoubleConstantDefinition; + // Rules for formula definitions. + qi::rule formulaDefinitionList; + qi::rule formulaDefinition; + qi::rule constantIntegerFormulaDefinition; + qi::rule integerFormulaDefinition; + qi::rule constantDoubleFormulaDefinition; + qi::rule constantBooleanFormulaDefinition; + qi::rule booleanFormulaDefinition; + // Rules for variable recognition. qi::rule(), Skipper> booleanVariableCreatorExpression; qi::rule(), qi::locals>, Skipper> integerVariableCreatorExpression; diff --git a/src/parser/prismparser/VariableState.cpp b/src/parser/prismparser/VariableState.cpp index 045b4dee6..a3d85579b 100644 --- a/src/parser/prismparser/VariableState.cpp +++ b/src/parser/prismparser/VariableState.cpp @@ -149,11 +149,18 @@ namespace storm { } bool VariableState::isFreeIdentifier(std::string const& identifier) const { + if (this->booleanVariableNames_.find(identifier) != nullptr) return false; if (this->integerVariableNames_.find(identifier) != nullptr) return false; if (this->allConstantNames_.find(identifier) != nullptr) return false; if (this->labelNames_.find(identifier) != nullptr) return false; if (this->moduleNames_.find(identifier) != nullptr) return false; if (this->keywords.find(identifier) != nullptr) return false; + if (this->booleanFormulas_.find(identifier) != nullptr) return false; + if (this->integerFormulas_.find(identifier) != nullptr) return false; + if (this->doubleFormulas_.find(identifier) != nullptr) return false; + if (this->constantBooleanFormulas_.find(identifier) != nullptr) return false; + if (this->constantIntegerFormulas_.find(identifier) != nullptr) return false; + if (this->constantDoubleFormulas_.find(identifier) != nullptr) return false; return true; } diff --git a/src/parser/prismparser/VariableState.h b/src/parser/prismparser/VariableState.h index deccd4da4..6dc7170a4 100644 --- a/src/parser/prismparser/VariableState.h +++ b/src/parser/prismparser/VariableState.h @@ -124,7 +124,7 @@ namespace storm { // Structures mapping variable and constant names to the corresponding expression nodes of // the intermediate representation. struct qi::symbols> integerVariables_, booleanVariables_; - struct qi::symbols> integerConstants_, booleanConstants_, doubleConstants_; + struct qi::symbols> integerConstants_, booleanConstants_, doubleConstants_, booleanFormulas_, constantBooleanFormulas_, integerFormulas_, constantIntegerFormulas_, doubleFormulas_, constantDoubleFormulas_; // A structure representing the identity function over identifier names. struct variableNamesStruct : qi::symbols { } diff --git a/src/utility/IRUtility.h b/src/utility/IRUtility.h index b3f79a380..dda032a12 100644 --- a/src/utility/IRUtility.h +++ b/src/utility/IRUtility.h @@ -268,10 +268,16 @@ namespace storm { // A mapping of boolean variable names to their indices. std::map booleanVariableToIndexMap; - + // List of all integer variables. std::vector integerVariables; + // List of all lower bounds for integer variables. + std::vector lowerBounds; + + // List of all upper bounds for integer variables. + std::vector upperBounds; + // A mapping of integer variable names to their indices. std::map integerVariableToIndexMap; }; @@ -299,6 +305,8 @@ namespace storm { // Resize the variable vectors appropriately. result.booleanVariables.resize(numberOfBooleanVariables); result.integerVariables.resize(numberOfIntegerVariables); + result.lowerBounds.resize(numberOfIntegerVariables); + result.upperBounds.resize(numberOfIntegerVariables); // Create variables. for (uint_fast64_t i = 0; i < program.getNumberOfGlobalBooleanVariables(); ++i) { @@ -310,6 +318,8 @@ namespace storm { storm::ir::IntegerVariable const& var = program.getGlobalIntegerVariable(i); result.integerVariables[var.getGlobalIndex()] = var; result.integerVariableToIndexMap[var.getName()] = var.getGlobalIndex(); + result.lowerBounds[var.getGlobalIndex()] = var.getLowerBound()->getValueAsInt(nullptr); + result.upperBounds[var.getGlobalIndex()] = var.getUpperBound()->getValueAsInt(nullptr); } for (uint_fast64_t i = 0; i < program.getNumberOfModules(); ++i) { storm::ir::Module const& module = program.getModule(i); @@ -323,6 +333,8 @@ namespace storm { storm::ir::IntegerVariable const& var = module.getIntegerVariable(j); result.integerVariables[var.getGlobalIndex()] = var; result.integerVariableToIndexMap[var.getName()] = var.getGlobalIndex(); + result.lowerBounds[var.getGlobalIndex()] = var.getLowerBound()->getValueAsInt(nullptr); + result.upperBounds[var.getGlobalIndex()] = var.getUpperBound()->getValueAsInt(nullptr); } } From 5cd18c1cf51253cde40c4a8c4859b23997132ecc Mon Sep 17 00:00:00 2001 From: dehnert Date: Wed, 13 Nov 2013 15:07:20 +0100 Subject: [PATCH 2/7] Resolved some ambiguities that produced problems under Linux. Added option USE_LIBCXX to CMakeLists.txt to also use libc++ under Linux. Former-commit-id: f2f7bb6d8008e4f3cf9f91410d6478b2ae36a948 --- CMakeLists.txt | 3 ++- src/adapters/Z3ExpressionAdapter.h | 4 ++-- src/counterexamples/SMTMinimalCommandSetGenerator.h | 2 +- 3 files changed, 5 insertions(+), 4 deletions(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index 9bb6e10da..51a4b9004 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -31,6 +31,7 @@ option(USE_BOOST_STATIC_LIBRARIES "Sets whether the Boost libraries should be li option(USE_INTELTBB "Sets whether the Intel TBB Extensions should be used." OFF) option(STORM_USE_COTIRE "Sets whether Cotire should be used (for building precompiled headers)." OFF) option(LINK_LIBCXXABI "Sets whether libc++abi should be linked." OFF) +option(USE_LIBCXX "Sets whether the standard library is libc++." OFF) set(GUROBI_ROOT "" CACHE STRING "The root directory of Gurobi (if available).") set(Z3_ROOT "" CACHE STRING "The root directory of Z3 (if available).") set(ADDITIONAL_INCLUDE_DIRS "" CACHE STRING "Additional directories added to the include directories.") @@ -138,7 +139,7 @@ else(CLANG) set (CLANG ON) # Set standard flags for clang set (CMAKE_CXX_FLAGS_RELEASE "${CMAKE_CXX_FLAGS_RELEASE} -funroll-loops -O3") - if(UNIX AND NOT APPLE) + if(UNIX AND NOT APPLE AND NOT USE_LIBCXX) set(CLANG_STDLIB libstdc++) message(STATUS "StoRM - Linking against libstdc++") else() diff --git a/src/adapters/Z3ExpressionAdapter.h b/src/adapters/Z3ExpressionAdapter.h index 6a6ce210a..09bc1dac4 100644 --- a/src/adapters/Z3ExpressionAdapter.h +++ b/src/adapters/Z3ExpressionAdapter.h @@ -166,11 +166,11 @@ namespace storm { << ". Integer constant '" << expression->getConstantName() << "' is undefined."; } - stack.push(context.int_val(expression->getValue())); + stack.push(context.int_val(static_cast(expression->getValue()))); } virtual void visit(ir::expressions::IntegerLiteralExpression* expression) { - stack.push(context.int_val(expression->getValueAsInt(nullptr))); + stack.push(context.int_val(static_cast(expression->getValueAsInt(nullptr)))); } virtual void visit(ir::expressions::UnaryBooleanFunctionExpression* expression) { diff --git a/src/counterexamples/SMTMinimalCommandSetGenerator.h b/src/counterexamples/SMTMinimalCommandSetGenerator.h index 645ba0268..6ab3e5bc0 100644 --- a/src/counterexamples/SMTMinimalCommandSetGenerator.h +++ b/src/counterexamples/SMTMinimalCommandSetGenerator.h @@ -555,7 +555,7 @@ namespace storm { } for (uint_fast64_t index = 0; index < programVariableInformation.integerVariables.size(); ++index) { storm::ir::IntegerVariable const& variable = programVariableInformation.integerVariables[index]; - initialStateExpression = initialStateExpression && (solverVariables.at(variable.getName()) == localContext.int_val(std::get<1>(*initialState).at(programVariableInformation.integerVariableToIndexMap.at(variable.getName())))); + initialStateExpression = initialStateExpression && (solverVariables.at(variable.getName()) == localContext.int_val(static_cast(std::get<1>(*initialState).at(programVariableInformation.integerVariableToIndexMap.at(variable.getName()))))); } // Store the found implications in a container similar to the preceding label sets. From 7c0dd5eaf592aa07db31c6222b91e18d24f4658f Mon Sep 17 00:00:00 2001 From: David_Korzeniewski Date: Wed, 13 Nov 2013 20:38:11 +0100 Subject: [PATCH 3/7] Fixed build errors on Windows Former-commit-id: 10929f075db4834acc86a9398a9d6e33c265c19b --- CMakeLists.txt | 6 +++--- src/ir/expressions/BinaryNumericalFunctionExpression.cpp | 1 + src/storage/VectorSet.h | 1 + 3 files changed, 5 insertions(+), 3 deletions(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index 9bb6e10da..72f1adad9 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -361,9 +361,9 @@ endif(ENABLE_GUROBI) if (ENABLE_Z3) message (STATUS "StoRM - Linking with Z3") include_directories("${Z3_ROOT}/include") - target_link_libraries(storm "z3") - target_link_libraries(storm-functional-tests "z3") - target_link_libraries(storm-performance-tests "z3") + target_link_libraries(storm "libz3") + target_link_libraries(storm-functional-tests "libz3") + target_link_libraries(storm-performance-tests "libz3") endif(ENABLE_Z3) ############################################################# diff --git a/src/ir/expressions/BinaryNumericalFunctionExpression.cpp b/src/ir/expressions/BinaryNumericalFunctionExpression.cpp index 452fb278a..a80e04ae4 100644 --- a/src/ir/expressions/BinaryNumericalFunctionExpression.cpp +++ b/src/ir/expressions/BinaryNumericalFunctionExpression.cpp @@ -6,6 +6,7 @@ */ #include +#include #include "BinaryNumericalFunctionExpression.h" diff --git a/src/storage/VectorSet.h b/src/storage/VectorSet.h index 1bbf30652..b225348cd 100644 --- a/src/storage/VectorSet.h +++ b/src/storage/VectorSet.h @@ -8,6 +8,7 @@ #ifndef STORM_STORAGE_VECTORSET_H #define STORM_STORAGE_VECTORSET_H +#include #include #include From 9e66447eb298c8a2541b06ea20c23d101868d984 Mon Sep 17 00:00:00 2001 From: David_Korzeniewski Date: Fri, 15 Nov 2013 12:21:05 +0100 Subject: [PATCH 4/7] Add "lib" prefix for z3 only on Windows Former-commit-id: bdfa503070ebf25b278f38bbc648f60d9ce4e2bd --- CMakeLists.txt | 11 ++++++++--- 1 file changed, 8 insertions(+), 3 deletions(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index 3b368f957..1f6c9b578 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -90,6 +90,7 @@ if ("${Z3_ROOT}" STREQUAL "") set(ENABLE_Z3 OFF) else() set(ENABLE_Z3 ON) + set(Z3_LIB_NAME "z3") endif() message(STATUS "StoRM - CMAKE_BUILD_TYPE: ${CMAKE_BUILD_TYPE}") @@ -132,6 +133,10 @@ elseif(MSVC) # Windows.h breaks GMM in gmm_except.h because of its macro definition for min and max add_definitions(/DNOMINMAX) + if(ENABLE_Z3) + set(Z3_LIB_NAME "libz3") + endif() + # MSVC does not do strict-aliasing, so no option needed else(CLANG) message(STATUS "StoRM - Using Compiler Configuration: Clang (LLVM)") @@ -362,9 +367,9 @@ endif(ENABLE_GUROBI) if (ENABLE_Z3) message (STATUS "StoRM - Linking with Z3") include_directories("${Z3_ROOT}/include") - target_link_libraries(storm "libz3") - target_link_libraries(storm-functional-tests "libz3") - target_link_libraries(storm-performance-tests "libz3") + target_link_libraries(storm ${Z3_LIB_NAME}) + target_link_libraries(storm-functional-tests ${Z3_LIB_NAME}) + target_link_libraries(storm-performance-tests ${Z3_LIB_NAME}) endif(ENABLE_Z3) ############################################################# From 9e941e6b4ab04edffffcd54b2adf9764988cebee Mon Sep 17 00:00:00 2001 From: dehnert Date: Sun, 17 Nov 2013 17:20:18 +0100 Subject: [PATCH 5/7] Added scheduler classes. Added method to model classes that applies a scheduler. Former-commit-id: 73a4be11b277cbb993fe5ba038b4bcf2b6f0634f --- .../MILPMinimalLabelSetGenerator.h | 2 +- .../SMTMinimalCommandSetGenerator.h | 2 +- src/models/AbstractModel.h | 12 ++++- src/models/AbstractNondeterministicModel.h | 7 +-- src/models/Ctmc.h | 11 ++++ src/models/Ctmdp.h | 12 +++++ src/models/Dtmc.h | 14 ++++- src/models/Mdp.h | 15 +++++- src/storage/PartialScheduler.cpp | 24 +++++++++ src/storage/PartialScheduler.h | 24 +++++++++ src/storage/Scheduler.h | 36 +++++++++++++ src/storage/TotalScheduler.cpp | 21 ++++++++ src/storage/TotalScheduler.h | 26 ++++++++++ src/utility/matrix.h | 52 +++++++++++++++++++ 14 files changed, 250 insertions(+), 8 deletions(-) create mode 100644 src/storage/PartialScheduler.cpp create mode 100644 src/storage/PartialScheduler.h create mode 100644 src/storage/Scheduler.h create mode 100644 src/storage/TotalScheduler.cpp create mode 100644 src/storage/TotalScheduler.h create mode 100644 src/utility/matrix.h diff --git a/src/counterexamples/MILPMinimalLabelSetGenerator.h b/src/counterexamples/MILPMinimalLabelSetGenerator.h index 5f0d10a75..78911ef29 100644 --- a/src/counterexamples/MILPMinimalLabelSetGenerator.h +++ b/src/counterexamples/MILPMinimalLabelSetGenerator.h @@ -1268,7 +1268,7 @@ namespace storm { static storm::storage::VectorSet getMinimalLabelSet(storm::models::Mdp const& labeledMdp, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, double probabilityThreshold, bool strictBound, bool checkThresholdFeasible = false, bool includeSchedulerCuts = false) { #ifdef STORM_HAVE_GUROBI // (0) Check whether the MDP is indeed labeled. - if (!labeledMdp.hasChoiceLabels()) { + if (!labeledMdp.hasChoiceLabeling()) { throw storm::exceptions::InvalidArgumentException() << "Minimal label set generation is impossible for unlabeled model."; } diff --git a/src/counterexamples/SMTMinimalCommandSetGenerator.h b/src/counterexamples/SMTMinimalCommandSetGenerator.h index 6ab3e5bc0..1d7a3a90f 100644 --- a/src/counterexamples/SMTMinimalCommandSetGenerator.h +++ b/src/counterexamples/SMTMinimalCommandSetGenerator.h @@ -1447,7 +1447,7 @@ namespace storm { storm::utility::ir::defineUndefinedConstants(program, constantDefinitionString); // (0) Check whether the MDP is indeed labeled. - if (!labeledMdp.hasChoiceLabels()) { + if (!labeledMdp.hasChoiceLabeling()) { throw storm::exceptions::InvalidArgumentException() << "Minimal command set generation is impossible for unlabeled model."; } diff --git a/src/models/AbstractModel.h b/src/models/AbstractModel.h index 6516884a8..375d6a957 100644 --- a/src/models/AbstractModel.h +++ b/src/models/AbstractModel.h @@ -9,6 +9,7 @@ #include "src/models/AtomicPropositionsLabeling.h" #include "src/storage/BitVector.h" #include "src/storage/SparseMatrix.h" +#include "src/storage/Scheduler.h" #include "src/storage/VectorSet.h" #include "src/utility/Hash.h" @@ -403,7 +404,7 @@ class AbstractModel: public std::enable_shared_from_this> { * Retrieves whether this model has a labeling for the choices. * @return True if this model has a labeling. */ - bool hasChoiceLabels() const { + bool hasChoiceLabeling() const { return choiceLabeling; } @@ -459,6 +460,15 @@ class AbstractModel: public std::enable_shared_from_this> { * @return void */ virtual void setStateIdBasedChoiceLabeling() = 0; + + /* + * Applies the given scheduler to the model. + * + * @param scheduler The scheduler to apply. + * @return The model resulting from applying the scheduler to the model. + */ + virtual std::shared_ptr> applyScheduler(storm::storage::Scheduler const& scheduler) const = 0; + protected: /*! * Exports the model to the dot-format and prints the result to the given stream. diff --git a/src/models/AbstractNondeterministicModel.h b/src/models/AbstractNondeterministicModel.h index d45e2a51a..21de66e12 100644 --- a/src/models/AbstractNondeterministicModel.h +++ b/src/models/AbstractNondeterministicModel.h @@ -1,10 +1,11 @@ #ifndef STORM_MODELS_ABSTRACTNONDETERMINISTICMODEL_H_ #define STORM_MODELS_ABSTRACTNONDETERMINISTICMODEL_H_ -#include "AbstractModel.h" - #include +#include "AbstractModel.h" +#include "src/storage/Scheduler.h" + namespace storm { namespace models { @@ -235,7 +236,7 @@ namespace storm { this->choiceLabeling.reset(newChoiceLabeling); } - + private: /*! A vector of indices mapping states to the choices (rows) in the transition matrix. */ std::vector nondeterministicChoiceIndices; diff --git a/src/models/Ctmc.h b/src/models/Ctmc.h index 2385ce2cf..60250d461 100644 --- a/src/models/Ctmc.h +++ b/src/models/Ctmc.h @@ -86,6 +86,17 @@ public: virtual std::size_t getHash() const override { return AbstractDeterministicModel::getHash(); } + + virtual std::shared_ptr> applyScheduler(storm::storage::Scheduler const& scheduler) const override { + std::vector nondeterministicChoiceIndices(this->getNumberOfStates() + 1); + for (uint_fast64_t state = 0; state < this->getNumberOfStates(); ++state) { + nondeterministicChoiceIndices[state] = state; + } + nondeterministicChoiceIndices[this->getNumberOfStates()] = this->getNumberOfStates(); + storm::storage::SparseMatrix newTransitionMatrix = storm::utility::matrix::applyScheduler(this->getTransitionMatrix(), nondeterministicChoiceIndices, scheduler); + + return std::shared_ptr>(new Ctmc(newTransitionMatrix, this->getStateLabeling(), this->hasStateRewards() ? this->getStateRewardVector() : boost::optional>(), this->hasTransitionRewards() ? this->getTransitionRewardMatrix() : boost::optional>(), this->hasChoiceLabeling() ? this->getChoiceLabeling() : boost::optional>>())); +} }; } // namespace models diff --git a/src/models/Ctmdp.h b/src/models/Ctmdp.h index b8d3145e2..ccf465361 100644 --- a/src/models/Ctmdp.h +++ b/src/models/Ctmdp.h @@ -115,6 +115,18 @@ public: return AbstractNondeterministicModel::getHash(); } + virtual std::shared_ptr> applyScheduler(storm::storage::Scheduler const& scheduler) const override { + storm::storage::SparseMatrix newTransitionMatrix = storm::utility::matrix::applyScheduler(this->getTransitionMatrix(), this->getNondeterministicChoiceIndices(), scheduler); + + // Construct the new nondeterministic choice indices for the resulting matrix. + std::vector nondeterministicChoiceIndices(this->getNumberOfStates() + 1); + for (uint_fast64_t state = 0; state < this->getNumberOfStates(); ++state) { + nondeterministicChoiceIndices[state] = state; + } + nondeterministicChoiceIndices[this->getNumberOfStates()] = this->getNumberOfStates(); + return std::shared_ptr>(new Ctmdp(newTransitionMatrix, this->getStateLabeling(), nondeterministicChoiceIndices, this->hasStateRewards() ? this->getStateRewardVector() : boost::optional>(), this->hasTransitionRewards() ? this->getTransitionRewardMatrix() : boost::optional>(), this->hasChoiceLabeling() ? this->getChoiceLabeling() : boost::optional>>())); + } + private: /*! diff --git a/src/models/Dtmc.h b/src/models/Dtmc.h index c21d06d2f..b573f848d 100644 --- a/src/models/Dtmc.h +++ b/src/models/Dtmc.h @@ -19,6 +19,7 @@ #include "src/exceptions/InvalidArgumentException.h" #include "src/settings/Settings.h" #include "src/utility/vector.h" +#include "src/utility/matrix.h" namespace storm { @@ -276,7 +277,7 @@ public: } boost::optional>> newChoiceLabels; - if(this->hasChoiceLabels()) { + if(this->hasChoiceLabeling()) { // Get the choice label sets and move the needed values to the front. std::vector> newChoice(this->getChoiceLabeling()); @@ -299,6 +300,17 @@ public: } + virtual std::shared_ptr> applyScheduler(storm::storage::Scheduler const& scheduler) const override { + std::vector nondeterministicChoiceIndices(this->getNumberOfStates() + 1); + for (uint_fast64_t state = 0; state < this->getNumberOfStates(); ++state) { + nondeterministicChoiceIndices[state] = state; + } + nondeterministicChoiceIndices[this->getNumberOfStates()] = this->getNumberOfStates(); + storm::storage::SparseMatrix newTransitionMatrix = storm::utility::matrix::applyScheduler(this->getTransitionMatrix(), nondeterministicChoiceIndices, scheduler); + + return std::shared_ptr>(new Dtmc(newTransitionMatrix, this->getStateLabeling(), this->hasStateRewards() ? this->getStateRewardVector() : boost::optional>(), this->hasTransitionRewards() ? this->getTransitionRewardMatrix() : boost::optional>(), this->hasChoiceLabeling() ? this->getChoiceLabeling() : boost::optional>>())); + } + private: /*! * @brief Perform some sanity checks. diff --git a/src/models/Mdp.h b/src/models/Mdp.h index 5507ddfb2..6af4b3ffd 100644 --- a/src/models/Mdp.h +++ b/src/models/Mdp.h @@ -18,6 +18,7 @@ #include "src/settings/Settings.h" #include "src/models/AbstractNondeterministicModel.h" #include "src/utility/set.h" +#include "src/utility/matrix.h" namespace storm { @@ -136,7 +137,7 @@ public: */ Mdp restrictChoiceLabels(storm::storage::VectorSet const& enabledChoiceLabels) const { // Only perform this operation if the given model has choice labels. - if (!this->hasChoiceLabels()) { + if (!this->hasChoiceLabeling()) { throw storm::exceptions::InvalidArgumentException() << "Restriction to label set is impossible for unlabeled model."; } @@ -192,6 +193,18 @@ public: return AbstractNondeterministicModel::getHash(); } + virtual std::shared_ptr> applyScheduler(storm::storage::Scheduler const& scheduler) const override { + storm::storage::SparseMatrix newTransitionMatrix = storm::utility::matrix::applyScheduler(this->getTransitionMatrix(), this->getNondeterministicChoiceIndices(), scheduler); + + // Construct the new nondeterministic choice indices for the resulting matrix. + std::vector nondeterministicChoiceIndices(this->getNumberOfStates() + 1); + for (uint_fast64_t state = 0; state < this->getNumberOfStates(); ++state) { + nondeterministicChoiceIndices[state] = state; + } + nondeterministicChoiceIndices[this->getNumberOfStates()] = this->getNumberOfStates(); + return std::shared_ptr>(new Mdp(newTransitionMatrix, this->getStateLabeling(), nondeterministicChoiceIndices, this->hasStateRewards() ? this->getStateRewardVector() : boost::optional>(), this->hasTransitionRewards() ? this->getTransitionRewardMatrix() : boost::optional>(), this->hasChoiceLabeling() ? this->getChoiceLabeling() : boost::optional>>())); + } + private: /*! diff --git a/src/storage/PartialScheduler.cpp b/src/storage/PartialScheduler.cpp new file mode 100644 index 000000000..e6804cea3 --- /dev/null +++ b/src/storage/PartialScheduler.cpp @@ -0,0 +1,24 @@ +#include "src/storage/PartialScheduler.h" +#include "src/exceptions/InvalidArgumentException.h" + +namespace storm { + namespace storage { + + void PartialScheduler::setChoice(uint_fast64_t state, uint_fast64_t choice) { + choices[state] = choice; + } + + bool PartialScheduler::isChoiceDefined(uint_fast64_t state) const { + return choices.find(state) != choices.end(); + } + + uint_fast64_t PartialScheduler::getChoice(uint_fast64_t state) const { + auto stateChoicePair = choices.find(state); + + if (stateChoicePair == choices.end()) { + throw storm::exceptions::InvalidArgumentException() << "Scheduler does not define a choice for state " << state; + } + } + + } // namespace storage +} // namespace storm \ No newline at end of file diff --git a/src/storage/PartialScheduler.h b/src/storage/PartialScheduler.h new file mode 100644 index 000000000..41ca228e4 --- /dev/null +++ b/src/storage/PartialScheduler.h @@ -0,0 +1,24 @@ +#ifndef STORM_STORAGE_PARTIALSCHEDULER_H_ +#define STORM_STORAGE_PARTIALSCHEDULER_H_ + +#include "src/storage/Scheduler.h" + +namespace storm { + namespace storage { + + class PartialScheduler : public Scheduler { + public: + void setChoice(uint_fast64_t state, uint_fast64_t choice) override; + + bool isChoiceDefined(uint_fast64_t state) const override; + + uint_fast64_t getChoice(uint_fast64_t state) const override; + + private: + // A mapping from all states that have defined choices to their respective choices. + std::unsorted_map choices; + }; + } +} + +#endif /* STORM_STORAGE_PARTIALSCHEDULER_H_ */ diff --git a/src/storage/Scheduler.h b/src/storage/Scheduler.h new file mode 100644 index 000000000..9f31a2a48 --- /dev/null +++ b/src/storage/Scheduler.h @@ -0,0 +1,36 @@ +#ifndef STORM_STORAGE_SCHEDULER_H_ +#define STORM_STORAGE_SCHEDULER_H_ + +namespace storm { + namespace storage { + + /* + * This class is the abstract base class of all scheduler classes. Scheduler classes define which action is chosen in a particular state of a non-deterministic model. + */ + class Scheduler { + public: + /* + * Sets the choice defined by the scheduler for the given state. + * + * @param state The state for which to set the choice. + * @param choice The choice to set for the given state. + */ + virtual void setChoice(uint_fast64_t state, uint_fast64_t choice) = 0; + + /* + * Retrieves whether this scheduler defines a choice for the given state. + * + * @param state The state for which to check whether the scheduler defines a choice. + * @return True if the scheduler defines a choice for the given state. + */ + virtual bool isChoiceDefined(uint_fast64_t state) const = 0; + + /*! + * Retrieves the choice for the given state under the assumption that the scheduler defines a proper choice for the state. + */ + virtual uint_fast64_t getChoice(uint_fast64_t state) const = 0; + }; + } +} + +#endif /* STORM_STORAGE_SCHEDULER_H_ */ diff --git a/src/storage/TotalScheduler.cpp b/src/storage/TotalScheduler.cpp new file mode 100644 index 000000000..e240fd24c --- /dev/null +++ b/src/storage/TotalScheduler.cpp @@ -0,0 +1,21 @@ +#include "src/storage/TotalScheduler.h" + +namespace storm { + namespace storage { + TotalScheduler::TotalScheduler(uint_fast64_t numberOfStates) : choices(numberOfStates) { + // Intentionally left empty. + } + + void setChoice(uint_fast64_t state, uint_fast64_t choice) override { + choices[state] = choice; + } + + bool isChoiceDefined(uint_fast64_t state) const override { + return true; + } + + uint_fast64_t getChoice(uint_fast64_t state) const override { + return choices[state]; + } + } +} \ No newline at end of file diff --git a/src/storage/TotalScheduler.h b/src/storage/TotalScheduler.h new file mode 100644 index 000000000..1679766ad --- /dev/null +++ b/src/storage/TotalScheduler.h @@ -0,0 +1,26 @@ +#ifndef STORM_STORAGE_TOTALSCHEDULER_H_ +#define STORM_STORAGE_TOTALSCHEDULER_H_ + +#include "src/storage/Scheduler.h" + +namespace storm { + namespace storage { + + class TotalScheduler : public Scheduler { + public: + TotalScheduler(uint_fast64_t numberOfStates); + + void setChoice(uint_fast64_t state, uint_fast64_t choice) override; + + bool isChoiceDefined(uint_fast64_t state) const override; + + uint_fast64_t getChoice(uint_fast64_t state) const override; + + private: + // A vector that stores the choice for each state. + std::vector choices; + }; + } // namespace storage +} // namespace storm + +#endif /* STORM_STORAGE_TOTALSCHEDULER_H_ */ diff --git a/src/utility/matrix.h b/src/utility/matrix.h new file mode 100644 index 000000000..897db4374 --- /dev/null +++ b/src/utility/matrix.h @@ -0,0 +1,52 @@ +#ifndef STORM_UTILITY_MATRIX_H_ +#define STORM_UTILITY_MATRIX_H_ + +#include "src/storage/SparseMatrix.h" +#include "src/storage/Scheduler.h" +#include "src/exceptions/InvalidStateException.h" + +namespace storm { + namespace utility { + namespace matrix { + + /*! + * Applies the given scheduler to the given transition matrix. This means that all choices that are not taken by the scheduler are + * dropped from the transition matrix. If a state has no choice enabled, it is equipped with a self-loop instead. + * + * @param transitionMatrix The transition matrix of the original system. + * @param nondeterministicChoiceIndices A vector indicating at which rows the choices for the states begin. + * @param scheduler The scheduler to apply to the system. + * @return A transition matrix that corresponds to all transitions of the given system that are selected by the given scheduler. + */ + template + storm::storage::SparseMatrix applyScheduler(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::Scheduler const& scheduler) { + storm::storage::SparseMatrix result(nondeterministicChoiceIndices.size() - 1, transitionMatrix.getColumnCount()); + + for (uint_fast64_t state = 0; state < nondeterministicChoiceIndices.size() - 1; ++state) { + if (scheduler.isChoiceDefined(state)) { + // Check whether the choice is valid for this state. + uint_fast64_t choice = nondeterministicChoiceIndices[state] + scheduler.getChoice(state); + if (choice >= nondeterministicChoiceIndices[state + 1]) { + throw storm::exceptions::InvalidStateException() << "Scheduler defines illegal choice " << choice << " for state " << state << "."; + } + + // If a valid choice for this state is defined, we copy over the corresponding entries. + typename storm::storage::SparseMatrix::Rows selectedRow = transitionMatrix.getRow(choice); + for (auto entry : selectedRow) { + result.insertNextValue(state, entry.column(), entry.value()); + } + } else { + // If no valid choice for the state is defined, we insert a self-loop. + result.insertNextValue(state, state, storm::utility::constGetOne()); + } + } + + // Finalize the matrix creation and return result. + result.finalize(); + return result; + } + } + } +} + +#endif /* STORM_UTILITY_MATRIX_H_ */ From 360b506afe8ee186ab0f30fbddaf316bfc9d1bbc Mon Sep 17 00:00:00 2001 From: dehnert Date: Sun, 17 Nov 2013 18:24:44 +0100 Subject: [PATCH 6/7] Sparse MDP model checker now correctly computes (memoryless) schedulers for Until and Reachability Reward formulas. Former-commit-id: c756093fd4f7de5fe448cfffca08e702a4bc2d50 --- examples/mdp/tiny/tiny.pctl | 2 + .../MILPMinimalLabelSetGenerator.h | 2 +- .../SMTMinimalCommandSetGenerator.h | 4 +- .../prctl/SparseMdpPrctlModelChecker.h | 38 ++++++++++--------- src/storage/PartialScheduler.cpp | 16 ++++++++ src/storage/PartialScheduler.h | 7 +++- src/storage/Scheduler.h | 2 + src/storage/TotalScheduler.cpp | 22 +++++++++-- src/storage/TotalScheduler.h | 7 ++++ 9 files changed, 75 insertions(+), 25 deletions(-) create mode 100644 examples/mdp/tiny/tiny.pctl diff --git a/examples/mdp/tiny/tiny.pctl b/examples/mdp/tiny/tiny.pctl new file mode 100644 index 000000000..393670a26 --- /dev/null +++ b/examples/mdp/tiny/tiny.pctl @@ -0,0 +1,2 @@ +Pmin=? [ F a ] +Pmax=? [ F a ] \ No newline at end of file diff --git a/src/counterexamples/MILPMinimalLabelSetGenerator.h b/src/counterexamples/MILPMinimalLabelSetGenerator.h index 78911ef29..8e9e23503 100644 --- a/src/counterexamples/MILPMinimalLabelSetGenerator.h +++ b/src/counterexamples/MILPMinimalLabelSetGenerator.h @@ -1275,7 +1275,7 @@ namespace storm { // (1) Check whether its possible to exceed the threshold if checkThresholdFeasible is set. double maximalReachabilityProbability = 0; storm::modelchecker::prctl::SparseMdpPrctlModelChecker modelchecker(labeledMdp, new storm::solver::GmmxxNondeterministicLinearEquationSolver()); - std::vector result = modelchecker.checkUntil(false, phiStates, psiStates, false, nullptr); + std::vector result = modelchecker.checkUntil(false, phiStates, psiStates, false).first; for (auto state : labeledMdp.getInitialStates()) { maximalReachabilityProbability = std::max(maximalReachabilityProbability, result[state]); } diff --git a/src/counterexamples/SMTMinimalCommandSetGenerator.h b/src/counterexamples/SMTMinimalCommandSetGenerator.h index 1d7a3a90f..e3fa9e394 100644 --- a/src/counterexamples/SMTMinimalCommandSetGenerator.h +++ b/src/counterexamples/SMTMinimalCommandSetGenerator.h @@ -1454,7 +1454,7 @@ namespace storm { // (1) Check whether its possible to exceed the threshold if checkThresholdFeasible is set. double maximalReachabilityProbability = 0; storm::modelchecker::prctl::SparseMdpPrctlModelChecker modelchecker(labeledMdp, new storm::solver::GmmxxNondeterministicLinearEquationSolver()); - std::vector result = modelchecker.checkUntil(false, phiStates, psiStates, false, nullptr); + std::vector result = modelchecker.checkUntil(false, phiStates, psiStates, false).first; for (auto state : labeledMdp.getInitialStates()) { maximalReachabilityProbability = std::max(maximalReachabilityProbability, result[state]); } @@ -1517,7 +1517,7 @@ namespace storm { storm::models::Mdp subMdp = labeledMdp.restrictChoiceLabels(commandSet); storm::modelchecker::prctl::SparseMdpPrctlModelChecker modelchecker(subMdp, new storm::solver::GmmxxNondeterministicLinearEquationSolver()); LOG4CPLUS_DEBUG(logger, "Invoking model checker."); - std::vector result = modelchecker.checkUntil(false, phiStates, psiStates, false, nullptr); + std::vector result = modelchecker.checkUntil(false, phiStates, psiStates, false).first; LOG4CPLUS_DEBUG(logger, "Computed model checking results."); totalModelCheckingTime += std::chrono::high_resolution_clock::now() - modelCheckingClock; diff --git a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h index 9f9683a06..69c2644b4 100644 --- a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h +++ b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h @@ -19,6 +19,7 @@ #include "src/utility/vector.h" #include "src/utility/graph.h" #include "src/settings/Settings.h" +#include "src/storage/TotalScheduler.h" namespace storm { namespace modelchecker { @@ -265,7 +266,7 @@ namespace storm { * checker. If the qualitative flag is set, exact probabilities might not be computed. */ virtual std::vector checkUntil(const storm::property::prctl::Until& formula, bool qualitative) const { - return this->checkUntil(this->minimumOperatorStack.top(), formula.getLeft().check(*this), formula.getRight().check(*this), qualitative, nullptr); + return this->checkUntil(this->minimumOperatorStack.top(), formula.getLeft().check(*this), formula.getRight().check(*this), qualitative).first; } /*! @@ -284,7 +285,7 @@ namespace storm { * @return The probabilities for the satisfying phi until psi for each state of the model. If the * qualitative flag is set, exact probabilities might not be computed. */ - std::vector checkUntil(bool minimize, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, std::vector* scheduler) const { + std::pair, storm::storage::TotalScheduler> checkUntil(bool minimize, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative) const { // We need to identify the states which have to be taken out of the matrix, i.e. // all states that have probability 0 and 1 of satisfying the until-formula. std::pair statesWithProbability01; @@ -347,12 +348,10 @@ namespace storm { storm::utility::vector::setVectorValues(result, statesWithProbability0, storm::utility::constGetZero()); storm::utility::vector::setVectorValues(result, statesWithProbability1, storm::utility::constGetOne()); - // If we were required to generate a scheduler, do so now. - if (scheduler != nullptr) { - this->computeTakenChoices(this->minimumOperatorStack.top(), false, result, *scheduler, this->getModel().getNondeterministicChoiceIndices()); - } + // Finally, compute a scheduler that achieves the extramal value. + storm::storage::TotalScheduler scheduler = this->computeExtremalScheduler(this->minimumOperatorStack.top(), false, result); - return result; + return std::make_pair(result, scheduler); } /*! @@ -443,7 +442,7 @@ namespace storm { * checker. If the qualitative flag is set, exact values might not be computed. */ virtual std::vector checkReachabilityReward(const storm::property::prctl::ReachabilityReward& formula, bool qualitative) const { - return this->checkReachabilityReward(this->minimumOperatorStack.top(), formula.getChild().check(*this), qualitative, nullptr); + return this->checkReachabilityReward(this->minimumOperatorStack.top(), formula.getChild().check(*this), qualitative).first; } /*! @@ -461,7 +460,7 @@ namespace storm { * @return The expected reward values gained before a target state is reached for each state. If the * qualitative flag is set, exact values might not be computed. */ - virtual std::vector checkReachabilityReward(bool minimize, storm::storage::BitVector const& targetStates, bool qualitative, std::vector* scheduler) const { + virtual std::pair, storm::storage::TotalScheduler> checkReachabilityReward(bool minimize, storm::storage::BitVector const& targetStates, bool qualitative) const { // Only compute the result if the model has at least one reward model. if (!(this->getModel().hasStateRewards() || this->getModel().hasTransitionRewards())) { LOG4CPLUS_ERROR(logger, "Missing reward model for formula."); @@ -548,12 +547,10 @@ namespace storm { storm::utility::vector::setVectorValues(result, targetStates, storm::utility::constGetZero()); storm::utility::vector::setVectorValues(result, infinityStates, storm::utility::constGetInfinity()); - // If we were required to generate a scheduler, do so now. - if (scheduler != nullptr) { - this->computeTakenChoices(this->minimumOperatorStack.top(), true, result, *scheduler, this->getModel().getNondeterministicChoiceIndices()); - } + // Finally, compute a scheduler that achieves the extramal value. + storm::storage::TotalScheduler scheduler = this->computeExtremalScheduler(this->minimumOperatorStack.top(), false, result); - return result; + return std::make_pair(result, scheduler); } protected: @@ -565,8 +562,8 @@ namespace storm { * @param takenChoices The output vector that is to store the taken choices. * @param nondeterministicChoiceIndices The assignment of states to their nondeterministic choices in the matrix. */ - void computeTakenChoices(bool minimize, bool addRewards, std::vector const& result, std::vector& takenChoices, std::vector const& nondeterministicChoiceIndices) const { - std::vector temporaryResult(nondeterministicChoiceIndices.size() - 1); + storm::storage::TotalScheduler computeExtremalScheduler(bool minimize, bool addRewards, std::vector const& result) const { + std::vector temporaryResult(this->getModel().getNondeterministicChoiceIndices().size() - 1); std::vector nondeterministicResult(result); storm::solver::GmmxxLinearEquationSolver solver; solver.performMatrixVectorMultiplication(this->getModel().getTransitionMatrix(), nondeterministicResult, nullptr, 1); @@ -585,11 +582,16 @@ namespace storm { } storm::utility::vector::addVectorsInPlace(nondeterministicResult, totalRewardVector); } + + std::vector choices(this->getModel().getNumberOfStates()); + if (minimize) { - storm::utility::vector::reduceVectorMin(nondeterministicResult, temporaryResult, nondeterministicChoiceIndices, &takenChoices); + storm::utility::vector::reduceVectorMin(nondeterministicResult, temporaryResult, this->getModel().getNondeterministicChoiceIndices(), &choices); } else { - storm::utility::vector::reduceVectorMax(nondeterministicResult, temporaryResult, nondeterministicChoiceIndices, &takenChoices); + storm::utility::vector::reduceVectorMax(nondeterministicResult, temporaryResult, this->getModel().getNondeterministicChoiceIndices(), &choices); } + + return storm::storage::TotalScheduler(choices); } /*! diff --git a/src/storage/PartialScheduler.cpp b/src/storage/PartialScheduler.cpp index e6804cea3..850d54a92 100644 --- a/src/storage/PartialScheduler.cpp +++ b/src/storage/PartialScheduler.cpp @@ -18,6 +18,22 @@ namespace storm { if (stateChoicePair == choices.end()) { throw storm::exceptions::InvalidArgumentException() << "Scheduler does not define a choice for state " << state; } + + return stateChoicePair->second; + } + + std::ostream& operator<<(std::ostream& out, PartialScheduler const& scheduler) { + out << "partial scheduler (defined on " << scheduler.choices.size() << " states) [ "; + uint_fast64_t remainingEntries = scheduler.choices.size(); + for (auto stateChoicePair : scheduler.choices) { + out << stateChoicePair.first << " -> " << stateChoicePair.second; + --remainingEntries; + if (remainingEntries > 0) { + out << ", "; + } + } + out << "]"; + return out; } } // namespace storage diff --git a/src/storage/PartialScheduler.h b/src/storage/PartialScheduler.h index 41ca228e4..ca33165d2 100644 --- a/src/storage/PartialScheduler.h +++ b/src/storage/PartialScheduler.h @@ -1,6 +1,9 @@ #ifndef STORM_STORAGE_PARTIALSCHEDULER_H_ #define STORM_STORAGE_PARTIALSCHEDULER_H_ +#include +#include + #include "src/storage/Scheduler.h" namespace storm { @@ -14,9 +17,11 @@ namespace storm { uint_fast64_t getChoice(uint_fast64_t state) const override; + friend std::ostream& operator<<(std::ostream& out, PartialScheduler const& scheduler); + private: // A mapping from all states that have defined choices to their respective choices. - std::unsorted_map choices; + std::unordered_map choices; }; } } diff --git a/src/storage/Scheduler.h b/src/storage/Scheduler.h index 9f31a2a48..9ea87bbdf 100644 --- a/src/storage/Scheduler.h +++ b/src/storage/Scheduler.h @@ -1,6 +1,8 @@ #ifndef STORM_STORAGE_SCHEDULER_H_ #define STORM_STORAGE_SCHEDULER_H_ +#include + namespace storm { namespace storage { diff --git a/src/storage/TotalScheduler.cpp b/src/storage/TotalScheduler.cpp index e240fd24c..41b75119c 100644 --- a/src/storage/TotalScheduler.cpp +++ b/src/storage/TotalScheduler.cpp @@ -6,16 +6,32 @@ namespace storm { // Intentionally left empty. } - void setChoice(uint_fast64_t state, uint_fast64_t choice) override { + TotalScheduler::TotalScheduler(std::vector const& choices) : choices(choices) { + // Intentionally left empty. + } + + void TotalScheduler::setChoice(uint_fast64_t state, uint_fast64_t choice) { choices[state] = choice; } - bool isChoiceDefined(uint_fast64_t state) const override { + bool TotalScheduler::isChoiceDefined(uint_fast64_t state) const { return true; } - uint_fast64_t getChoice(uint_fast64_t state) const override { + uint_fast64_t TotalScheduler::getChoice(uint_fast64_t state) const { return choices[state]; } + + std::ostream& operator<<(std::ostream& out, TotalScheduler const& scheduler) { + out << "total scheduler (defined on " << scheduler.choices.size() << " states) [ "; + for (uint_fast64_t state = 0; state < scheduler.choices.size() - 1; ++state) { + out << state << " -> " << scheduler.choices[state] << ", "; + } + if (scheduler.choices.size() > 0) { + out << (scheduler.choices.size() - 1) << " -> " << scheduler.choices[scheduler.choices.size() - 1] << " ]"; + } + return out; + } + } } \ No newline at end of file diff --git a/src/storage/TotalScheduler.h b/src/storage/TotalScheduler.h index 1679766ad..2e29471f7 100644 --- a/src/storage/TotalScheduler.h +++ b/src/storage/TotalScheduler.h @@ -1,6 +1,9 @@ #ifndef STORM_STORAGE_TOTALSCHEDULER_H_ #define STORM_STORAGE_TOTALSCHEDULER_H_ +#include +#include + #include "src/storage/Scheduler.h" namespace storm { @@ -10,12 +13,16 @@ namespace storm { public: TotalScheduler(uint_fast64_t numberOfStates); + TotalScheduler(std::vector const& choices); + void setChoice(uint_fast64_t state, uint_fast64_t choice) override; bool isChoiceDefined(uint_fast64_t state) const override; uint_fast64_t getChoice(uint_fast64_t state) const override; + friend std::ostream& operator<<(std::ostream& out, TotalScheduler const& scheduler); + private: // A vector that stores the choice for each state. std::vector choices; From e31c3bfb17c3af37c85361c16e427dfaf3cb336a Mon Sep 17 00:00:00 2001 From: dehnert Date: Sun, 17 Nov 2013 18:29:13 +0100 Subject: [PATCH 7/7] Added an important comment. Former-commit-id: 79d8280d83ce027ad7d8d9457361d558a63fd96b --- src/storage/Scheduler.h | 1 + 1 file changed, 1 insertion(+) diff --git a/src/storage/Scheduler.h b/src/storage/Scheduler.h index 9ea87bbdf..d9363c8fb 100644 --- a/src/storage/Scheduler.h +++ b/src/storage/Scheduler.h @@ -8,6 +8,7 @@ namespace storm { /* * This class is the abstract base class of all scheduler classes. Scheduler classes define which action is chosen in a particular state of a non-deterministic model. + * More concretely, a scheduler maps a state s to i if the scheduler takes the i-th action available in s (i.e. the choices are relative to the states). */ class Scheduler { public: