diff --git a/CMakeLists.txt b/CMakeLists.txt index 19b9c507f..74394693f 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -129,6 +129,9 @@ elseif(MSVC) # Windows.h breaks GMM in gmm_except.h because of its macro definition for min and max add_definitions(/DNOMINMAX) + # since nobody cares at the moment + add_definitions(/wd4250) + if(ENABLE_Z3) set(Z3_LIB_NAME "libz3") endif() diff --git a/resources/3rdparty/cudd-2.5.0/CMakeLists.txt b/resources/3rdparty/cudd-2.5.0/CMakeLists.txt index c7cff2aca..4d08513de 100644 --- a/resources/3rdparty/cudd-2.5.0/CMakeLists.txt +++ b/resources/3rdparty/cudd-2.5.0/CMakeLists.txt @@ -25,5 +25,14 @@ if(MSVC) add_definitions(/D_SCL_SECURE_NO_DEPRECATE /D_CRT_SECURE_NO_WARNINGS) endif() +# Since we do not target Alphas, this symbol is always set +add_definitions(-DHAVE_IEEE_754) + +if(CMAKE_SIZEOF_VOID_P EQUAL 8) + message(STATUS "CUDD: Targeting 64bit architecture") + add_definitions(-DSIZEOF_VOID_P=8) + add_definitions(-DSIZEOF_LONG=8) +endif() + # Add the library add_library(cudd ${CUDD_SOURCES} ${CUDD_HEADERS} ${CUDD_HEADERS_CXX} ${CUDD_SOURCES_CXX}) \ No newline at end of file diff --git a/resources/3rdparty/cudd-2.5.0/src/cudd/cudd.h b/resources/3rdparty/cudd-2.5.0/src/cudd/cudd.h index 5a2c2f952..51d509b35 100644 --- a/resources/3rdparty/cudd-2.5.0/src/cudd/cudd.h +++ b/resources/3rdparty/cudd-2.5.0/src/cudd/cudd.h @@ -964,6 +964,7 @@ extern DdNode * Cudd_Increasing (DdManager *dd, DdNode *f, int i); extern int Cudd_EquivDC (DdManager *dd, DdNode *F, DdNode *G, DdNode *D); extern int Cudd_bddLeqUnless (DdManager *dd, DdNode *f, DdNode *g, DdNode *D); extern int Cudd_EqualSupNorm (DdManager *dd, DdNode *f, DdNode *g, CUDD_VALUE_TYPE tolerance, int pr); +extern int Cudd_EqualSupNormRel (DdManager *dd, DdNode *f, DdNode *g, CUDD_VALUE_TYPE tolerance, int pr); extern DdNode * Cudd_bddMakePrime (DdManager *dd, DdNode *cube, DdNode *f); extern DdNode * Cudd_bddMaximallyExpand(DdManager *dd, DdNode *lb, DdNode *ub, DdNode *f); extern DdNode * Cudd_bddLargestPrimeUnate(DdManager *dd , DdNode *f, DdNode *phaseBdd); diff --git a/resources/3rdparty/cudd-2.5.0/src/cudd/cuddExport.c b/resources/3rdparty/cudd-2.5.0/src/cudd/cuddExport.c index 3d8da77ac..2392da36a 100644 --- a/resources/3rdparty/cudd-2.5.0/src/cudd/cuddExport.c +++ b/resources/3rdparty/cudd-2.5.0/src/cudd/cuddExport.c @@ -502,9 +502,11 @@ Cudd_DumpDot( scan = nodelist[j]; while (scan != NULL) { if (st_is_member(visited,(char *) scan)) { - retval = fprintf(fp,"\"%p\";\n", - (void *) ((mask & (ptrint) scan) / sizeof(DdNode))); - if (retval == EOF) goto failure; + if (scan != Cudd_ReadZero(dd)) { + retval = fprintf(fp,"\"%p\";\n", + (void *) ((mask & (ptrint) scan) / sizeof(DdNode))); + if (retval == EOF) goto failure; + } } scan = scan->next; } @@ -541,6 +543,12 @@ Cudd_DumpDot( scan = nodelist[j]; while (scan != NULL) { if (st_is_member(visited,(char *) scan)) { + retval = fprintf(fp, + "\"%p\" [label = \"%s\"];\n", + (void *) ((mask & (ptrint) scan) / + sizeof(DdNode)), inames[dd->invperm[i]]); + if (retval == EOF) goto failure; + if (cuddT(scan) != Cudd_ReadZero(dd)) { retval = fprintf(fp, "\"%p\" -> \"%p\";\n", (void *) ((mask & (ptrint) scan) / @@ -548,6 +556,8 @@ Cudd_DumpDot( (void *) ((mask & (ptrint) cuddT(scan)) / sizeof(DdNode))); if (retval == EOF) goto failure; + } + if (cuddE(scan) != Cudd_ReadZero(dd)) { if (Cudd_IsComplement(cuddE(scan))) { retval = fprintf(fp, "\"%p\" -> \"%p\" [style = dotted];\n", @@ -565,6 +575,7 @@ Cudd_DumpDot( } if (retval == EOF) goto failure; } + } scan = scan->next; } } @@ -578,11 +589,13 @@ Cudd_DumpDot( scan = nodelist[j]; while (scan != NULL) { if (st_is_member(visited,(char *) scan)) { + if (scan != Cudd_ReadZero(dd)) { retval = fprintf(fp,"\"%p\" [label = \"%g\"];\n", (void *) ((mask & (ptrint) scan) / sizeof(DdNode)), cuddV(scan)); if (retval == EOF) goto failure; } + } scan = scan->next; } } diff --git a/resources/3rdparty/cudd-2.5.0/src/cudd/cuddSat.c b/resources/3rdparty/cudd-2.5.0/src/cudd/cuddSat.c index 19dcafff0..869733f32 100644 --- a/resources/3rdparty/cudd-2.5.0/src/cudd/cuddSat.c +++ b/resources/3rdparty/cudd-2.5.0/src/cudd/cuddSat.c @@ -853,6 +853,71 @@ Cudd_EqualSupNorm( } /* end of Cudd_EqualSupNorm */ +/**Function******************************************************************** + + Synopsis [Compares two ADDs for equality within tolerance.] + + Description [Same as Cudd_EqualSupNorm but tests for max _relative_ difference + i.e. (f-g/f)0) { + (void) fprintf(dd->out,"Offending nodes:\n"); + (void) fprintf(dd->out, + "f: address = %p\t value = %40.30f\n", + (void *) f, cuddV(f)); + (void) fprintf(dd->out, + "g: address = %p\t value = %40.30f\n", + (void *) g, cuddV(g)); + } + return(0); + } + } + + /* We only insert the result in the cache if the comparison is + ** successful. Therefore, if we hit we return 1. */ + r = cuddCacheLookup2(dd,(DD_CTFP)Cudd_EqualSupNormRel,f,g); + if (r != NULL) { + return(1); + } + + /* Compute the cofactors and solve the recursive subproblems. */ + topf = cuddI(dd,f->index); + topg = cuddI(dd,g->index); + + if (topf <= topg) {fv = cuddT(f); fvn = cuddE(f);} else {fv = fvn = f;} + if (topg <= topf) {gv = cuddT(g); gvn = cuddE(g);} else {gv = gvn = g;} + + if (!Cudd_EqualSupNormRel(dd,fv,gv,tolerance,pr)) return(0); + if (!Cudd_EqualSupNormRel(dd,fvn,gvn,tolerance,pr)) return(0); + + cuddCacheInsert2(dd,(DD_CTFP)Cudd_EqualSupNormRel,f,g,DD_ONE(dd)); + + return(1); + +} /* end of Cudd_EqualSupNormRel */ /**Function******************************************************************** diff --git a/resources/3rdparty/cudd-2.5.0/src/obj/cuddObj.cc b/resources/3rdparty/cudd-2.5.0/src/obj/cuddObj.cc index c9fcf7b11..fcec76782 100644 --- a/resources/3rdparty/cudd-2.5.0/src/obj/cuddObj.cc +++ b/resources/3rdparty/cudd-2.5.0/src/obj/cuddObj.cc @@ -4747,6 +4747,16 @@ ADD::EqualSupNorm( } // ADD::EqualSupNorm +bool +ADD::EqualSupNormRel( + const ADD& g, + CUDD_VALUE_TYPE tolerance, + int pr) const +{ + DdManager *mgr = checkSameManager(g); + return Cudd_EqualSupNormRel(mgr, node, g.node, tolerance, pr) != 0; + +} // ADD::EqualSupNormRel BDD BDD::MakePrime( @@ -5267,14 +5277,14 @@ ABDD::FirstCube( int -NextCube( +ABDD::NextCube( DdGen * gen, int ** cube, - CUDD_VALUE_TYPE * value) + CUDD_VALUE_TYPE * value) { return Cudd_NextCube(gen, cube, value); -} // NextCube +} // ABDD::NextCube BDD diff --git a/resources/3rdparty/cudd-2.5.0/src/obj/cuddObj.hh b/resources/3rdparty/cudd-2.5.0/src/obj/cuddObj.hh index a1a859490..1162a968c 100644 --- a/resources/3rdparty/cudd-2.5.0/src/obj/cuddObj.hh +++ b/resources/3rdparty/cudd-2.5.0/src/obj/cuddObj.hh @@ -192,6 +192,7 @@ public: const; int CountLeaves() const; DdGen * FirstCube(int ** cube, CUDD_VALUE_TYPE * value) const; + static int NextCube(DdGen * gen, int ** cube, CUDD_VALUE_TYPE * value); double Density(int nvars) const; }; // ABDD @@ -426,8 +427,8 @@ public: ADD TimesPlus(const ADD& B, std::vector z) const; ADD Triangle(const ADD& g, std::vector z) const; ADD Eval(int * inputs) const; - bool EqualSupNorm(const ADD& g, CUDD_VALUE_TYPE tolerance, int pr) const; - + bool EqualSupNorm(const ADD& g, CUDD_VALUE_TYPE tolerance, int pr = 0) const; + bool EqualSupNormRel(const ADD& g, CUDD_VALUE_TYPE tolerance, int pr = 0) const; }; // ADD diff --git a/resources/3rdparty/ltl2dstar-0.5.1/src/parsers/nba-parser-lbtt.lex.cpp b/resources/3rdparty/ltl2dstar-0.5.1/src/parsers/nba-parser-lbtt.lex.cpp index f20e1eedb..55e55fbd2 100644 --- a/resources/3rdparty/ltl2dstar-0.5.1/src/parsers/nba-parser-lbtt.lex.cpp +++ b/resources/3rdparty/ltl2dstar-0.5.1/src/parsers/nba-parser-lbtt.lex.cpp @@ -31,7 +31,7 @@ /* C99 systems have . Non-C99 systems may or may not. */ -#if defined __STDC_VERSION__ && __STDC_VERSION__ >= 199901L +#if (defined __STDC_VERSION__ && __STDC_VERSION__ >= 199901L) || defined _WIN32 #include typedef int8_t flex_int8_t; typedef uint8_t flex_uint8_t; diff --git a/resources/3rdparty/ltl2dstar-0.5.1/src/parsers/nba-parser-promela.lex.cpp b/resources/3rdparty/ltl2dstar-0.5.1/src/parsers/nba-parser-promela.lex.cpp index 82812c039..9be4a847a 100644 --- a/resources/3rdparty/ltl2dstar-0.5.1/src/parsers/nba-parser-promela.lex.cpp +++ b/resources/3rdparty/ltl2dstar-0.5.1/src/parsers/nba-parser-promela.lex.cpp @@ -31,7 +31,7 @@ /* C99 systems have . Non-C99 systems may or may not. */ -#if defined __STDC_VERSION__ && __STDC_VERSION__ >= 199901L +#if (defined __STDC_VERSION__ && __STDC_VERSION__ >= 199901L) || defined _WIN32 #include typedef int8_t flex_int8_t; typedef uint8_t flex_uint8_t; diff --git a/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h b/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h index 2f03603d8..9d43dfb52 100644 --- a/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h +++ b/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h @@ -393,7 +393,7 @@ public: // Perform the actual matrix-vector multiplication as long as the bound of the formula is met. if (linearEquationSolver != nullptr) { - this->linearEquationSolver->performMatrixVectorMultiplication(this->getModel().getTransitionMatrix(), result, &totalRewardVector, formula.getBound()); + this->linearEquationSolver->performMatrixVectorMultiplication(this->getModel().getTransitionMatrix(), result, &totalRewardVector, static_cast(formula.getBound())); } else { throw storm::exceptions::InvalidStateException() << "No valid linear equation solver available."; } diff --git a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h index 868f78722..c3e2aec58 100644 --- a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h +++ b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h @@ -410,7 +410,7 @@ namespace storm { result.resize(this->getModel().getNumberOfStates()); } - this->nondeterministicLinearEquationSolver->performMatrixVectorMultiplication(this->minimumOperatorStack.top(), this->getModel().getTransitionMatrix(), result, &totalRewardVector, formula.getBound()); + this->nondeterministicLinearEquationSolver->performMatrixVectorMultiplication(this->minimumOperatorStack.top(), this->getModel().getTransitionMatrix(), result, &totalRewardVector, static_cast(formula.getBound())); return result; } diff --git a/src/parser/PrctlParser.cpp b/src/parser/PrctlParser.cpp index fb58d7ee9..d929c5ac7 100644 --- a/src/parser/PrctlParser.cpp +++ b/src/parser/PrctlParser.cpp @@ -140,7 +140,7 @@ struct PrctlParser::PrctlGrammar : qi::grammar stateFormula)[qi::_val = phoenix::new_>(qi::_1)]; reachabilityReward.name("path formula (for reward operator)"); - instantaneousReward = (qi::lit("I") > qi::lit("=") > qi::double_) + instantaneousReward = (qi::lit("I") > qi::lit("=") > qi::uint_) [qi::_val = phoenix::new_>(qi::_1)]; instantaneousReward.name("path formula (for reward operator)"); steadyStateReward = (qi::lit("S"))[qi::_val = phoenix::new_>()]; diff --git a/src/parser/PrismParser.cpp b/src/parser/PrismParser.cpp index 6039c2c11..ed15050cb 100644 --- a/src/parser/PrismParser.cpp +++ b/src/parser/PrismParser.cpp @@ -88,13 +88,16 @@ namespace storm { plusExpression = multiplicationExpression[qi::_val = qi::_1] >> *((qi::lit("+")[qi::_a = true] | qi::lit("-")[qi::_a = false]) >> multiplicationExpression)[phoenix::if_(qi::_a) [qi::_val = phoenix::bind(&PrismParser::createPlusExpression, phoenix::ref(*this), qi::_val, qi::_1)] .else_ [qi::_val = phoenix::bind(&PrismParser::createMinusExpression, phoenix::ref(*this), qi::_val, qi::_1)]]; plusExpression.name("plus expression"); - relativeExpression = (plusExpression >> qi::lit(">=") >> plusExpression)[qi::_val = phoenix::bind(&PrismParser::createGreaterOrEqualExpression, phoenix::ref(*this), qi::_1, qi::_2)] | (plusExpression >> qi::lit(">") >> plusExpression)[qi::_val = phoenix::bind(&PrismParser::createGreaterExpression, phoenix::ref(*this), qi::_1, qi::_2)] | (plusExpression >> qi::lit("<=") >> plusExpression)[qi::_val = phoenix::bind(&PrismParser::createLessOrEqualExpression, phoenix::ref(*this), qi::_1, qi::_2)] | (plusExpression >> qi::lit("<") >> plusExpression)[qi::_val = phoenix::bind(&PrismParser::createLessExpression, phoenix::ref(*this), qi::_1, qi::_2)] | (plusExpression >> qi::lit("=") >> plusExpression)[qi::_val = phoenix::bind(&PrismParser::createEqualsExpression, phoenix::ref(*this), qi::_1, qi::_2)] | (plusExpression >> qi::lit("!=") >> plusExpression)[qi::_val = phoenix::bind(&PrismParser::createNotEqualsExpression, phoenix::ref(*this), qi::_1, qi::_2)] | plusExpression[qi::_val = qi::_1]; + relativeExpression = (plusExpression >> qi::lit(">=") >> plusExpression)[qi::_val = phoenix::bind(&PrismParser::createGreaterOrEqualExpression, phoenix::ref(*this), qi::_1, qi::_2)] | (plusExpression >> qi::lit(">") >> plusExpression)[qi::_val = phoenix::bind(&PrismParser::createGreaterExpression, phoenix::ref(*this), qi::_1, qi::_2)] | (plusExpression >> qi::lit("<=") >> plusExpression)[qi::_val = phoenix::bind(&PrismParser::createLessOrEqualExpression, phoenix::ref(*this), qi::_1, qi::_2)] | (plusExpression >> qi::lit("<") >> plusExpression)[qi::_val = phoenix::bind(&PrismParser::createLessExpression, phoenix::ref(*this), qi::_1, qi::_2)] | plusExpression[qi::_val = qi::_1]; relativeExpression.name("relative expression"); - andExpression = relativeExpression[qi::_val = qi::_1] >> *(qi::lit("&") >> relativeExpression)[qi::_val = phoenix::bind(&PrismParser::createAndExpression, phoenix::ref(*this), qi::_val, qi::_1)]; + equalityExpression = relativeExpression[qi::_val = qi::_1] >> *((qi::lit("=")[qi::_a = true] | qi::lit("!=")[qi::_a = false]) >> relativeExpression)[phoenix::if_(qi::_a) [ qi::_val = phoenix::bind(&PrismParser::createEqualsExpression, phoenix::ref(*this), qi::_val, qi::_1) ] .else_ [ qi::_val = phoenix::bind(&PrismParser::createNotEqualsExpression, phoenix::ref(*this), qi::_val, qi::_1) ] ]; + equalityExpression.name("equality expression"); + + andExpression = equalityExpression[qi::_val = qi::_1] >> *(qi::lit("&") >> equalityExpression)[qi::_val = phoenix::bind(&PrismParser::createAndExpression, phoenix::ref(*this), qi::_val, qi::_1)]; andExpression.name("and expression"); - orExpression = andExpression[qi::_val = qi::_1] >> *(qi::lit("|") >> andExpression)[qi::_val = phoenix::bind(&PrismParser::createOrExpression, phoenix::ref(*this), qi::_val, qi::_1)]; + orExpression = andExpression[qi::_val = qi::_1] >> *((qi::lit("|")[qi::_a = true] | qi::lit("=>")[qi::_a = false]) >> andExpression)[phoenix::if_(qi::_a) [qi::_val = phoenix::bind(&PrismParser::createOrExpression, phoenix::ref(*this), qi::_val, qi::_1)] .else_ [qi::_val = phoenix::bind(&PrismParser::createImpliesExpression, phoenix::ref(*this), qi::_val, qi::_1)] ]; orExpression.name("or expression"); iteExpression = orExpression[qi::_val = qi::_1] >> -(qi::lit("?") > orExpression > qi::lit(":") > orExpression)[qi::_val = phoenix::bind(&PrismParser::createIteExpression, phoenix::ref(*this), qi::_val, qi::_1, qi::_2)]; @@ -204,6 +207,7 @@ namespace storm { qi::on_error(iteExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4)); qi::on_error(orExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4)); qi::on_error(andExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4)); + qi::on_error(equalityExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4)); qi::on_error(relativeExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4)); qi::on_error(plusExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4)); qi::on_error(multiplicationExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4)); @@ -271,6 +275,14 @@ namespace storm { } } + storm::expressions::Expression PrismParser::createImpliesExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const { + if (!this->secondRun) { + return storm::expressions::Expression::createFalse(); + } else { + return e1.implies(e2); + } + } + storm::expressions::Expression PrismParser::createOrExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const { if (!this->secondRun) { return storm::expressions::Expression::createFalse(); @@ -323,7 +335,11 @@ namespace storm { if (!this->secondRun) { return storm::expressions::Expression::createFalse(); } else { - return e1 == e2; + if (e1.hasBooleanReturnType() && e2.hasBooleanReturnType()) { + return e1.iff(e2); + } else { + return e1 == e2; + } } } @@ -331,7 +347,11 @@ namespace storm { if (!this->secondRun) { return storm::expressions::Expression::createFalse(); } else { - return e1 != e2; + if (e1.hasBooleanReturnType() && e2.hasBooleanReturnType()) { + return e1 ^ e2; + } else { + return e1 != e2; + } } } @@ -585,7 +605,7 @@ namespace storm { auto const& renamingPair = renaming.find(variable.getName()); LOG_THROW(renamingPair != renaming.end(), storm::exceptions::WrongFormatException, "Boolean variable '" << variable.getName() << " was not renamed."); - booleanVariables.push_back(storm::prism::BooleanVariable(renamingPair->second, variable.getInitialValueExpression().substitute(expressionRenaming), this->getFilename(), get_line(qi::_1))); + booleanVariables.push_back(storm::prism::BooleanVariable(renamingPair->second, variable.getInitialValueExpression().substitute(expressionRenaming), this->getFilename(), get_line(qi::_1))); } // Rename the integer variables. @@ -594,7 +614,7 @@ namespace storm { auto const& renamingPair = renaming.find(variable.getName()); LOG_THROW(renamingPair != renaming.end(), storm::exceptions::WrongFormatException, "Integer variable '" << variable.getName() << " was not renamed."); - integerVariables.push_back(storm::prism::IntegerVariable(renamingPair->second, variable.getLowerBoundExpression().substitute(expressionRenaming), variable.getUpperBoundExpression().substitute(expressionRenaming), variable.getInitialValueExpression().substitute(expressionRenaming), this->getFilename(), get_line(qi::_1))); + integerVariables.push_back(storm::prism::IntegerVariable(renamingPair->second, variable.getLowerBoundExpression().substitute(expressionRenaming), variable.getUpperBoundExpression().substitute(expressionRenaming), variable.getInitialValueExpression().substitute(expressionRenaming), this->getFilename(), get_line(qi::_1))); } // Rename commands. @@ -606,12 +626,12 @@ namespace storm { for (auto const& assignment : update.getAssignments()) { auto const& renamingPair = renaming.find(assignment.getVariableName()); if (renamingPair != renaming.end()) { - assignments.emplace_back(renamingPair->second, assignment.getExpression().substitute(expressionRenaming), this->getFilename(), get_line(qi::_1)); + assignments.emplace_back(renamingPair->second, assignment.getExpression().substitute(expressionRenaming), this->getFilename(), get_line(qi::_1)); } else { - assignments.emplace_back(assignment.getVariableName(), assignment.getExpression().substitute(expressionRenaming), this->getFilename(), get_line(qi::_1)); + assignments.emplace_back(assignment.getVariableName(), assignment.getExpression().substitute(expressionRenaming), this->getFilename(), get_line(qi::_1)); } } - updates.emplace_back(globalProgramInformation.currentUpdateIndex, update.getLikelihoodExpression().substitute(expressionRenaming), assignments, this->getFilename(), get_line(qi::_1)); + updates.emplace_back(globalProgramInformation.currentUpdateIndex, update.getLikelihoodExpression().substitute(expressionRenaming), assignments, this->getFilename(), get_line(qi::_1)); ++globalProgramInformation.currentUpdateIndex; } @@ -621,7 +641,7 @@ namespace storm { newActionName = renamingPair->second; } - commands.emplace_back(globalProgramInformation.currentCommandIndex, newActionName, command.getGuardExpression().substitute(expressionRenaming), updates, this->getFilename(), get_line(qi::_1)); + commands.emplace_back(globalProgramInformation.currentCommandIndex, newActionName, command.getGuardExpression().substitute(expressionRenaming), updates, this->getFilename(), get_line(qi::_1)); ++globalProgramInformation.currentCommandIndex; } diff --git a/src/parser/PrismParser.h b/src/parser/PrismParser.h index 3f8f17b65..4a0eec392 100644 --- a/src/parser/PrismParser.h +++ b/src/parser/PrismParser.h @@ -25,6 +25,7 @@ typedef BOOST_TYPEOF(qi::lit("//") >> *(qi::char_ - qi::eol) >> qi::eol | boost: #include "src/storage/prism/Program.h" #include "src/storage/expressions/Expression.h" +#include "src/storage/expressions/Expressions.h" #include "src/exceptions/ExceptionMacros.h" namespace storm { @@ -32,7 +33,7 @@ namespace storm { class GlobalProgramInformation { public: // Default construct the header information. - GlobalProgramInformation() = default; + GlobalProgramInformation() : hasInitialStatesExpression(false), currentCommandIndex(0), currentUpdateIndex(0) {} // Members for all essential information that needs to be collected. storm::prism::Program::ModelType modelType; @@ -85,7 +86,7 @@ namespace storm { } }; - struct keywordsStruct : qi::symbols { + struct keywordsStruct : qi::symbols { keywordsStruct() { add ("dtmc", 1) @@ -244,9 +245,10 @@ namespace storm { // Rules for parsing a composed expression. qi::rule expression; qi::rule iteExpression; - qi::rule orExpression; + qi::rule, Skipper> orExpression; qi::rule andExpression; qi::rule relativeExpression; + qi::rule, Skipper> equalityExpression; qi::rule, Skipper> plusExpression; qi::rule, Skipper> multiplicationExpression; qi::rule unaryExpression; @@ -269,6 +271,7 @@ namespace storm { bool addInitialStatesExpression(storm::expressions::Expression initialStatesExpression, GlobalProgramInformation& globalProgramInformation); storm::expressions::Expression createIteExpression(storm::expressions::Expression e1, storm::expressions::Expression e2, storm::expressions::Expression e3) const; + storm::expressions::Expression createImpliesExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const; storm::expressions::Expression createOrExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const; storm::expressions::Expression createAndExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const; storm::expressions::Expression createGreaterExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const; diff --git a/src/storage/dd/CuddDd.cpp b/src/storage/dd/CuddDd.cpp index 0e163c5f7..4daf835a6 100644 --- a/src/storage/dd/CuddDd.cpp +++ b/src/storage/dd/CuddDd.cpp @@ -1,3 +1,4 @@ +#include #include #include "src/storage/dd/CuddDd.h" @@ -19,6 +20,14 @@ namespace storm { return this->cuddAdd != other.getCuddAdd(); } + Dd Dd::ite(Dd const& thenDd, Dd const& elseDd) const { + std::set metaVariableNames(this->getContainedMetaVariableNames()); + metaVariableNames.insert(thenDd.getContainedMetaVariableNames().begin(), thenDd.getContainedMetaVariableNames().end()); + metaVariableNames.insert(elseDd.getContainedMetaVariableNames().begin(), elseDd.getContainedMetaVariableNames().end()); + + return Dd(this->getDdManager(), this->getCuddAdd().Ite(thenDd.getCuddAdd(), elseDd.getCuddAdd())); + } + Dd Dd::operator+(Dd const& other) const { Dd result(*this); result += other; @@ -55,6 +64,10 @@ namespace storm { return result; } + Dd Dd::operator-() const { + return this->getDdManager()->getZero() - *this; + } + Dd& Dd::operator-=(Dd const& other) { this->cuddAdd -= other.getCuddAdd(); @@ -79,11 +92,25 @@ namespace storm { return *this; } - Dd Dd::operator~() const { + Dd Dd::operator!() const { Dd result(*this); result.complement(); return result; } + + Dd Dd::operator&&(Dd const& other) const { + std::set metaVariableNames(this->getContainedMetaVariableNames()); + metaVariableNames.insert(other.getContainedMetaVariableNames().begin(), other.getContainedMetaVariableNames().end()); + + // Rewrite a and b to not((not a) or (not b)). + return Dd(this->getDdManager(), ~(~this->getCuddAdd()).Or(~other.getCuddAdd()), metaVariableNames); + } + + Dd Dd::operator||(Dd const& other) const { + std::set metaVariableNames(this->getContainedMetaVariableNames()); + metaVariableNames.insert(other.getContainedMetaVariableNames().begin(), other.getContainedMetaVariableNames().end()); + return Dd(this->getDdManager(), this->getCuddAdd().Or(other.getCuddAdd()), metaVariableNames); + } Dd& Dd::complement() { this->cuddAdd = ~this->cuddAdd; @@ -194,6 +221,14 @@ namespace storm { this->cuddAdd = this->cuddAdd.MaxAbstract(cubeDd.getCuddAdd()); } + bool Dd::equalModuloPrecision(Dd const& other, double precision, bool relative) const { + if (relative) { + return this->getCuddAdd().EqualSupNormRel(other.getCuddAdd(), precision); + } else { + return this->getCuddAdd().EqualSupNorm(other.getCuddAdd(), precision); + } + } + void Dd::swapVariables(std::vector> const& metaVariablePairs) { std::vector from; std::vector to; @@ -230,7 +265,7 @@ namespace storm { this->cuddAdd = this->cuddAdd.SwapVariables(from, to); } - Dd Dd::multiplyMatrix(Dd const& otherMatrix, std::set const& summationMetaVariableNames) { + Dd Dd::multiplyMatrix(Dd const& otherMatrix, std::set const& summationMetaVariableNames) const { std::vector summationDdVariables; // Create the CUDD summation variables. @@ -358,9 +393,32 @@ namespace storm { if (filename.empty()) { this->getDdManager()->getCuddManager().DumpDot(cuddAddVector); } else { + // Build the name input of the DD. + std::vector ddNames; + std::string ddName("f"); + ddNames.push_back(new char[ddName.size() + 1]); + std::copy(ddName.c_str(), ddName.c_str() + 2, ddNames.back()); + + // Now build the variables names. + std::vector ddVariableNamesAsStrings = this->getDdManager()->getDdVariableNames(); + std::vector ddVariableNames; + for (auto const& element : ddVariableNamesAsStrings) { + ddVariableNames.push_back(new char[element.size() + 1]); + std::copy(element.c_str(), element.c_str() + element.size() + 1, ddVariableNames.back()); + } + + // Open the file, dump the DD and close it again. FILE* filePointer = fopen(filename.c_str() , "w"); - this->getDdManager()->getCuddManager().DumpDot(cuddAddVector, nullptr, nullptr, filePointer); + this->getDdManager()->getCuddManager().DumpDot(cuddAddVector, &ddVariableNames[0], &ddNames[0], filePointer); fclose(filePointer); + + // Finally, delete the names. + for (char* element : ddNames) { + delete element; + } + for (char* element : ddVariableNames) { + delete element; + } } } @@ -384,6 +442,17 @@ namespace storm { return this->ddManager; } + DdForwardIterator Dd::begin() const { + int* cube; + double value; + DdGen* generator = this->getCuddAdd().FirstCube(&cube, &value); + return DdForwardIterator(this->getDdManager(), generator, cube, value, Cudd_IsGenEmpty(generator), &this->getContainedMetaVariableNames()); + } + + DdForwardIterator Dd::end() const { + return DdForwardIterator(this->getDdManager(), nullptr, nullptr, 0, true, nullptr); + } + std::ostream & operator<<(std::ostream& out, const Dd& dd) { dd.exportToDot(); return out; diff --git a/src/storage/dd/CuddDd.h b/src/storage/dd/CuddDd.h index 6da2dc9c3..32762b6cb 100644 --- a/src/storage/dd/CuddDd.h +++ b/src/storage/dd/CuddDd.h @@ -7,6 +7,7 @@ #include #include "src/storage/dd/Dd.h" +#include "src/storage/dd/CuddDdForwardIterator.h" #include "src/utility/OsDetection.h" // Include the C++-interface of CUDD. @@ -20,8 +21,9 @@ namespace storm { template<> class Dd { public: - // Declare the DdManager class as friend so it can access the internals of a DD. + // Declare the DdManager and DdIterator class as friend so it can access the internals of a DD. friend class DdManager; + friend class DdForwardIterator; // Instantiate all copy/move constructors/assignments with the default implementation. Dd() = default; @@ -48,6 +50,27 @@ namespace storm { */ bool operator!=(Dd const& other) const; + /*! + * Performs an if-then-else with the given operands, i.e. maps all valuations that are mapped to a non-zero + * function value to the function values specified by the first DD and all others to the function values + * specified by the second DD. + */ + Dd ite(Dd const& thenDd, Dd const& elseDd) const; + + /*! + * Performs a logical or of the current and the given DD. + * + * @return The logical or of the operands. + */ + Dd operator||(Dd const& other) const; + + /*! + * Performs a logical and of the current and the given DD. + * + * @return The logical and of the operands. + */ + Dd operator&&(Dd const& other) const; + /*! * Adds the two DDs. * @@ -88,6 +111,13 @@ namespace storm { */ Dd operator-(Dd const& other) const; + /*! + * Subtracts the DD from the constant zero function. + * + * @return The resulting function represented as a DD. + */ + Dd operator-() const; + /*! * Subtracts the given DD from the current one and assigns the result to the current DD. * @@ -112,20 +142,13 @@ namespace storm { */ Dd& operator/=(Dd const& other); - /*! - * Subtracts the DD from the constant zero function. - * - * @return The resulting function represented as a DD. - */ - Dd minus() const; - /*! * Retrieves the logical complement of the current DD. The result will map all encodings with a value * unequal to zero to false and all others to true. * * @return The logical complement of the current DD. */ - Dd operator~() const; + Dd operator!() const; /*! * Logically complements the current DD. The result will map all encodings with a value @@ -215,6 +238,17 @@ namespace storm { */ void maxAbstract(std::set const& metaVariableNames); + /*! + * Checks whether the current and the given DD represent the same function modulo some given precision. + * + * @param other The DD with which to compare. + * @param precision An upper bound on the maximal difference between any two function values that is to be + * tolerated. + * @param relative If set to true, not the absolute values have to be within the precision, but the relative + * values. + */ + bool equalModuloPrecision(Dd const& other, double precision, bool relative = true) const; + /*! * Swaps the given pairs of meta variables in the DD. The pairs of meta variables must be guaranteed to have * the same number of underlying DD variables. @@ -232,7 +266,7 @@ namespace storm { * matrix multiplication. * @return A DD representing the result of the matrix-matrix multiplication. */ - Dd multiplyMatrix(Dd const& otherMatrix, std::set const& summationMetaVariableNames); + Dd multiplyMatrix(Dd const& otherMatrix, std::set const& summationMetaVariableNames) const; /*! * Retrieves the number of encodings that are mapped to a non-zero value. @@ -380,6 +414,20 @@ namespace storm { */ std::shared_ptr> getDdManager() const; + /*! + * Retrieves an iterator that points to the first meta variable assignment with a non-zero function value. + * + * @return An iterator that points to the first meta variable assignment with a non-zero function value. + */ + DdForwardIterator begin() const; + + /*! + * Retrieves an iterator that points past the end of the container. + * + * @return An iterator that points past the end of the container. + */ + DdForwardIterator end() const; + friend std::ostream & operator<<(std::ostream& out, const Dd& dd); private: /*! diff --git a/src/storage/dd/CuddDdForwardIterator.cpp b/src/storage/dd/CuddDdForwardIterator.cpp new file mode 100644 index 000000000..c0e754c8b --- /dev/null +++ b/src/storage/dd/CuddDdForwardIterator.cpp @@ -0,0 +1,161 @@ +#include "src/storage/dd/CuddDdForwardIterator.h" +#include "src/storage/dd/CuddDdManager.h" +#include "src/storage/dd/DdMetaVariable.h" +#include "src/exceptions/ExceptionMacros.h" + +namespace storm { + namespace dd { + DdForwardIterator::DdForwardIterator(std::shared_ptr> ddManager, DdGen* generator, int* cube, double value, bool isAtEnd, std::set const* metaVariables) : ddManager(ddManager), generator(generator), cube(cube), value(value), isAtEnd(isAtEnd), metaVariables(metaVariables), cubeCounter(), relevantDontCareDdVariables(), currentValuation() { + // If the given generator is not yet at its end, we need to create the current valuation from the cube from + // scratch. + if (!this->isAtEnd) { + // Start by registering all meta variables in the valuation with the appropriate type. + for (auto const& metaVariableName : *this->metaVariables) { + auto const& metaVariable = this->ddManager->getMetaVariable(metaVariableName); + switch (metaVariable.getType()) { + case DdMetaVariable::MetaVariableType::Bool: currentValuation.addBooleanIdentifier(metaVariableName); break; + case DdMetaVariable::MetaVariableType::Int: currentValuation.addIntegerIdentifier(metaVariableName); break; + } + } + + // And then get ready for treating the first cube. + this->treatNewCube(); + } + } + + DdForwardIterator::DdForwardIterator(DdForwardIterator&& other) : ddManager(other.ddManager), generator(other.generator), cube(other.cube), value(other.value), isAtEnd(other.isAtEnd), metaVariables(other.metaVariables), cubeCounter(other.cubeCounter), relevantDontCareDdVariables(other.relevantDontCareDdVariables), currentValuation(other.currentValuation) { + // Null-out the pointers of which we took possession. + other.cube = nullptr; + other.generator = nullptr; + } + + DdForwardIterator& DdForwardIterator::operator=(DdForwardIterator&& other) { + if (this != &other) { + this->ddManager = other.ddManager; + this->generator = other.generator; + this->cube = other.cube; + this->value = other.value; + this->isAtEnd = other.isAtEnd; + this->metaVariables = other.metaVariables; + this->cubeCounter = other.cubeCounter; + this->relevantDontCareDdVariables = other.relevantDontCareDdVariables; + this->currentValuation = other.currentValuation; + + // Null-out the pointers of which we took possession. + other.cube = nullptr; + other.generator = nullptr; + } + return *this; + } + + DdForwardIterator::~DdForwardIterator() { + if (this->cube != nullptr) { + free(this->cube); + } + if (this->generator != nullptr) { + free(this->generator); + } + } + + DdForwardIterator& DdForwardIterator::operator++() { + LOG_ASSERT(!this->isAtEnd, "Illegally incrementing iterator that is already at its end."); + + // If there were no (relevant) don't cares or we have enumerated all combination, we need to eliminate the + // found solutions and get the next "first" cube. + if (this->relevantDontCareDdVariables.empty() || this->cubeCounter >= std::pow(2, this->relevantDontCareDdVariables.size()) - 1) { + // Get the next cube and check for emptiness. + ABDD::NextCube(generator, &cube, &value); + this->isAtEnd = Cudd_IsGenEmpty(generator); + + // In case we are not done yet, we get ready to treat the next cube. + if (!this->isAtEnd) { + this->treatNewCube(); + } + } else { + // Treat the next solution of the cube. + this->treatNextInCube(); + } + + return *this; + } + + void DdForwardIterator::treatNextInCube() { + // Start by increasing the counter and check which bits we need to set/unset in the new valuation. + ++this->cubeCounter; + + for (uint_fast64_t index = 0; index < this->relevantDontCareDdVariables.size(); ++index) { + auto const& metaVariable = this->ddManager->getMetaVariable(std::get<1>(this->relevantDontCareDdVariables[index])); + if (metaVariable.getType() == DdMetaVariable::MetaVariableType::Bool) { + if ((this->cubeCounter & (1ull << index)) != 0) { + currentValuation.setBooleanValue(metaVariable.getName(), true); + } else { + currentValuation.setBooleanValue(metaVariable.getName(), false); + } + } else { + if ((this->cubeCounter & (1ull << index)) != 0) { + currentValuation.setIntegerValue(metaVariable.getName(), ((currentValuation.getIntegerValue(metaVariable.getName()) - metaVariable.getLow()) | (1ull << std::get<2>(this->relevantDontCareDdVariables[index]))) + metaVariable.getLow()); + } else { + currentValuation.setIntegerValue(metaVariable.getName(), ((currentValuation.getIntegerValue(metaVariable.getName()) - metaVariable.getLow()) & ~(1ull << std::get<2>(this->relevantDontCareDdVariables[index]))) + metaVariable.getLow()); + } + } + } + } + + void DdForwardIterator::treatNewCube() { + this->relevantDontCareDdVariables.clear(); + + // Now loop through the bits of all meta variables and check whether they need to be set, not set or are + // don't cares. In the latter case, we add them to a special list, so we can iterate over their concrete + // valuations later. + for (auto const& metaVariableName : *this->metaVariables) { + auto const& metaVariable = this->ddManager->getMetaVariable(metaVariableName); + if (metaVariable.getType() == DdMetaVariable::MetaVariableType::Bool) { + if (this->cube[metaVariable.getDdVariables()[0].getCuddAdd().NodeReadIndex()] == 0) { + currentValuation.setBooleanValue(metaVariableName, false); + } else if (this->cube[metaVariable.getDdVariables()[0].getCuddAdd().NodeReadIndex()] == 1) { + currentValuation.setBooleanValue(metaVariableName, true); + } else { + relevantDontCareDdVariables.push_back(std::make_tuple(metaVariable.getDdVariables()[0].getCuddAdd(), metaVariableName, 0)); + } + } else { + int_fast64_t intValue = 0; + for (uint_fast64_t bitIndex = 0; bitIndex < metaVariable.getNumberOfDdVariables(); ++bitIndex) { + if (cube[metaVariable.getDdVariables()[bitIndex].getCuddAdd().NodeReadIndex()] == 0) { + // Leave bit unset. + } else if (cube[metaVariable.getDdVariables()[bitIndex].getCuddAdd().NodeReadIndex()] == 1) { + intValue |= 1ull << (metaVariable.getNumberOfDdVariables() - bitIndex - 1); + } else { + // Temporarily leave bit unset so we can iterate trough the other option later. + // Add the bit to the relevant don't care bits. + this->relevantDontCareDdVariables.push_back(std::make_tuple(metaVariable.getDdVariables()[bitIndex].getCuddAdd(), metaVariableName, metaVariable.getNumberOfDdVariables() - bitIndex - 1)); + } + } + currentValuation.setIntegerValue(metaVariableName, intValue + metaVariable.getLow()); + } + } + + // Finally, reset the cube counter. + this->cubeCounter = 0; + } + + bool DdForwardIterator::operator==(DdForwardIterator const& other) const { + if (this->isAtEnd && other.isAtEnd) { + return true; + } else { + return this->ddManager.get() == other.ddManager.get() && this->generator == other.generator + && this->cube == other.cube && this->value == other.value && this->isAtEnd == other.isAtEnd + && this->metaVariables == other.metaVariables && this->cubeCounter == other.cubeCounter + && this->relevantDontCareDdVariables == other.relevantDontCareDdVariables + && this->currentValuation == other.currentValuation; + } + } + + bool DdForwardIterator::operator!=(DdForwardIterator const& other) const { + return !(*this == other); + } + + std::pair DdForwardIterator::operator*() const { + return std::make_pair(currentValuation, value); + } + } +} \ No newline at end of file diff --git a/src/storage/dd/CuddDdForwardIterator.h b/src/storage/dd/CuddDdForwardIterator.h new file mode 100644 index 000000000..054438d2e --- /dev/null +++ b/src/storage/dd/CuddDdForwardIterator.h @@ -0,0 +1,130 @@ +#ifndef STORM_STORAGE_DD_CUDDDDFORWARDITERATOR_H_ +#define STORM_STORAGE_DD_CUDDDDFORWARDITERATOR_H_ + +#include +#include +#include +#include +#include + +#include "src/storage/dd/DdForwardIterator.h" +#include "src/storage/expressions/SimpleValuation.h" + +// Include the C++-interface of CUDD. +#include "cuddObj.hh" + +namespace storm { + namespace dd { + // Forward-declare the DdManager class. + template class DdManager; + template class Dd; + + template<> + class DdForwardIterator { + public: + friend class Dd; + + // Default-instantiate the constructor. + DdForwardIterator() = default; + + // Forbid copy-construction and copy assignment, because ownership of the internal pointer is unclear then. + DdForwardIterator(DdForwardIterator const& other) = delete; + DdForwardIterator& operator=(DdForwardIterator const& other) = delete; + + // Provide move-construction and move-assignment, though. + DdForwardIterator(DdForwardIterator&& other); + DdForwardIterator& operator=(DdForwardIterator&& other); + + /*! + * Destroys the forward iterator and frees the generator as well as the cube if they are not the nullptr. + */ + ~DdForwardIterator(); + + /*! + * Moves the iterator one position forward. + */ + DdForwardIterator& operator++(); + + /*! + * Returns a pair consisting of a valuation of meta variables and the value to which this valuation is + * mapped. Note that the result is returned by value. + * + * @return A pair of a valuation and the function value. + */ + std::pair operator*() const; + + /*! + * Compares the iterator with the given one. Two iterators are considered equal when all their underlying + * data members are the same or they both are at their end. + * + * @param other The iterator with which to compare. + * @return True if the two iterators are considered equal. + */ + bool operator==(DdForwardIterator const& other) const; + + /*! + * Compares the iterator with the given one. Two iterators are considered unequal iff they are not + * considered equal. + * + * @param other The iterator with which to compare. + * @return True if the two iterators are considered unequal. + */ + bool operator!=(DdForwardIterator const& other) const; + + private: + /*! + * Constructs a forward iterator using the given generator with the given set of relevant meta variables. + * + * @param ddManager The manager responsible for the DD over which to iterate. + * @param generator The generator used to enumerate the cubes of the DD. + * @param cube The cube as represented by CUDD. + * @param value The value the cube is mapped to. + * @param isAtEnd A flag that indicates whether the iterator is at its end and may not be moved forward any + * more. + * @param metaVariables The meta variables that appear in the DD. + */ + DdForwardIterator(std::shared_ptr> ddManager, DdGen* generator, int* cube, double value, bool isAtEnd, std::set const* metaVariables = nullptr); + + /*! + * Recreates the internal information when a new cube needs to be treated. + */ + void treatNewCube(); + + /*! + * Updates the internal information when the next solution of the current cube needs to be treated. + */ + void treatNextInCube(); + + // The manager responsible for the meta variables (and therefore the underlying DD). + std::shared_ptr> ddManager; + + // The CUDD generator used to enumerate the cubes of the DD. + DdGen* generator; + + // The currently considered cube of the DD. + int* cube; + + // The function value of the current cube. + double value; + + // A flag that indicates whether the iterator is at its end and may not be moved further. This is also used + // for the check against the end iterator. + bool isAtEnd; + + // The set of meta variables appearing in the DD. + std::set const* metaVariables; + + // A number that represents how many assignments of the current cube have already been returned previously. + // This is needed, because cubes may represent many assignments (if they have don't care variables). + uint_fast64_t cubeCounter; + + // A vector of tuples of the form . + std::vector> relevantDontCareDdVariables; + + // The current valuation of meta variables. + storm::expressions::SimpleValuation currentValuation; + }; + } +} + +#endif /* STORM_STORAGE_DD_CUDDDDFORWARDITERATOR_H_ */ \ No newline at end of file diff --git a/src/storage/dd/CuddDdManager.cpp b/src/storage/dd/CuddDdManager.cpp index 9843b5c92..c75a7c211 100644 --- a/src/storage/dd/CuddDdManager.cpp +++ b/src/storage/dd/CuddDdManager.cpp @@ -1,4 +1,5 @@ #include +#include #include #include "src/storage/dd/CuddDdManager.h" @@ -44,14 +45,14 @@ namespace storm { if (value & (1ull << (ddVariables.size() - 1))) { result = ddVariables[0]; } else { - result = ~ddVariables[0]; + result = !ddVariables[0]; } for (std::size_t i = 1; i < ddVariables.size(); ++i) { if (value & (1ull << (ddVariables.size() - i - 1))) { result *= ddVariables[i]; } else { - result *= ~ddVariables[i]; + result *= !ddVariables[i]; } } @@ -110,6 +111,18 @@ namespace storm { metaVariableMap.emplace(name, DdMetaVariable(name, low, high, variables, this->shared_from_this())); } + void DdManager::addMetaVariable(std::string const& name) { + // Check whether a meta variable already exists. + if (this->hasMetaVariable(name)) { + throw storm::exceptions::InvalidArgumentException() << "A meta variable '" << name << "' already exists."; + } + + std::vector> variables; + variables.emplace_back(Dd(this->shared_from_this(), cuddManager.addVar(), {name})); + + metaVariableMap.emplace(name, DdMetaVariable(name, variables, this->shared_from_this())); + } + void DdManager::addMetaVariablesInterleaved(std::vector const& names, int_fast64_t low, int_fast64_t high) { // Make sure that at least one meta variable is added. if (names.size() == 0) { @@ -179,5 +192,27 @@ namespace storm { Cudd& DdManager::getCuddManager() { return this->cuddManager; } + + std::vector DdManager::getDdVariableNames() const { + // First, we initialize a list DD variables and their names. + std::vector> variableNamePairs; + for (auto const& nameMetaVariablePair : this->metaVariableMap) { + DdMetaVariable const& metaVariable = nameMetaVariablePair.second; + for (uint_fast64_t variableIndex = 0; variableIndex < metaVariable.getNumberOfDdVariables(); ++variableIndex) { + variableNamePairs.emplace_back(metaVariable.getDdVariables()[variableIndex].getCuddAdd(), metaVariable.getName() + "." + std::to_string(variableIndex)); + } + } + + // Then, we sort this list according to the indices of the ADDs. + std::sort(variableNamePairs.begin(), variableNamePairs.end(), [](std::pair const& a, std::pair const& b) { return a.first.NodeReadIndex() < b.first.NodeReadIndex(); }); + + // Now, we project the sorted vector to its second component. + std::vector result; + for (auto const& element : variableNamePairs) { + result.push_back(element.second); + } + + return result; + } } } \ No newline at end of file diff --git a/src/storage/dd/CuddDdManager.h b/src/storage/dd/CuddDdManager.h index ca3f9c2c3..6df3dc25c 100644 --- a/src/storage/dd/CuddDdManager.h +++ b/src/storage/dd/CuddDdManager.h @@ -5,7 +5,6 @@ #include "src/storage/dd/DdManager.h" #include "src/storage/dd/DdMetaVariable.h" -#include "src/storage/dd/CuddDd.h" #include "src/utility/OsDetection.h" // Include the C++-interface of CUDD. @@ -16,7 +15,6 @@ namespace storm { template<> class DdManager : public std::enable_shared_from_this> { public: - // To break the cylic dependencies, we need to forward-declare the other DD-related classes. friend class Dd; /*! @@ -83,7 +81,7 @@ namespace storm { Dd getIdentity(std::string const& metaVariableName); /*! - * Adds a meta variable with the given name and range. + * Adds an integer meta variable with the given name and range. * * @param name The name of the meta variable. * @param low The lowest value of the range of the variable. @@ -92,7 +90,15 @@ namespace storm { void addMetaVariable(std::string const& name, int_fast64_t low, int_fast64_t high); /*! - * Adds meta variables with the given names and (equal) range and arranges the DD variables in an interleaved order. + * Adds a boolean meta variable with the given name. + * + * @param name The name of the meta variable. + */ + void addMetaVariable(std::string const& name); + + /*! + * Adds integer meta variables with the given names and (equal) range and arranges the DD variables in an + * interleaved order. * * @param names The names of the variables. * @param low The lowest value of the ranges of the variables. @@ -131,6 +137,13 @@ namespace storm { bool hasMetaVariable(std::string const& metaVariableName) const; private: + /*! + * Retrieves a list of names of the DD variables in the order of their index. + * + * @return A list of DD variable names. + */ + std::vector getDdVariableNames() const; + /*! * Retrieves the underlying CUDD manager. * diff --git a/src/storage/dd/DdForwardIterator.h b/src/storage/dd/DdForwardIterator.h new file mode 100644 index 000000000..2eed23090 --- /dev/null +++ b/src/storage/dd/DdForwardIterator.h @@ -0,0 +1,13 @@ +#ifndef STORM_STORAGE_DD_DDFORWARDITERATOR_H_ +#define STORM_STORAGE_DD_DDFORWARDITERATOR_H_ + +#include "src/storage/dd/DdType.h" + +namespace storm { + namespace dd { + // Declare DdIterator class so we can then specialize it for the different DD types. + template class DdForwardIterator; + } +} + +#endif /* STORM_STORAGE_DD_DDFORWARDITERATOR_H_ */ \ No newline at end of file diff --git a/src/storage/dd/DdMetaVariable.cpp b/src/storage/dd/DdMetaVariable.cpp index 9132eab03..453b83cc8 100644 --- a/src/storage/dd/DdMetaVariable.cpp +++ b/src/storage/dd/DdMetaVariable.cpp @@ -4,7 +4,15 @@ namespace storm { namespace dd { template - DdMetaVariable::DdMetaVariable(std::string const& name, int_fast64_t low, int_fast64_t high, std::vector> const& ddVariables, std::shared_ptr> manager) : name(name), low(low), high(high), ddVariables(ddVariables), cube(manager->getOne()), manager(manager) { + DdMetaVariable::DdMetaVariable(std::string const& name, int_fast64_t low, int_fast64_t high, std::vector> const& ddVariables, std::shared_ptr> manager) : name(name), type(MetaVariableType::Int), low(low), high(high), ddVariables(ddVariables), cube(manager->getOne()), manager(manager) { + // Create the cube of all variables of this meta variable. + for (auto const& ddVariable : this->ddVariables) { + this->cube *= ddVariable; + } + } + + template + DdMetaVariable::DdMetaVariable(std::string const& name, std::vector> const& ddVariables, std::shared_ptr> manager) : name(name), type(MetaVariableType::Bool), ddVariables(ddVariables), cube(manager->getOne()), manager(manager) { // Create the cube of all variables of this meta variable. for (auto const& ddVariable : this->ddVariables) { this->cube *= ddVariable; @@ -16,6 +24,11 @@ namespace storm { return this->name; } + template + typename DdMetaVariable::MetaVariableType DdMetaVariable::getType() const { + return this->type; + } + template int_fast64_t DdMetaVariable::getLow() const { return this->low; diff --git a/src/storage/dd/DdMetaVariable.h b/src/storage/dd/DdMetaVariable.h index f6c90cc21..47936d805 100644 --- a/src/storage/dd/DdMetaVariable.h +++ b/src/storage/dd/DdMetaVariable.h @@ -8,6 +8,7 @@ #include "utility/OsDetection.h" #include "src/storage/dd/CuddDd.h" +#include "src/storage/expressions/Expression.h" namespace storm { namespace dd { @@ -20,9 +21,13 @@ namespace storm { // Declare the DdManager class as friend so it can access the internals of a meta variable. friend class DdManager; friend class Dd; + friend class DdForwardIterator; + + // An enumeration for all legal types of meta variables. + enum class MetaVariableType { Bool, Int }; /*! - * Creates a meta variable with the given name, range bounds. + * Creates an integer meta variable with the given name and range bounds. * * @param name The name of the meta variable. * @param low The lowest value of the range of the variable. @@ -32,6 +37,14 @@ namespace storm { */ DdMetaVariable(std::string const& name, int_fast64_t low, int_fast64_t high, std::vector> const& ddVariables, std::shared_ptr> manager); + /*! + * Creates a boolean meta variable with the given name. + * @param name The name of the meta variable. + * @param ddVariables The vector of variables used to encode this variable. + * @param manager A pointer to the manager that is responsible for this meta variable. + */ + DdMetaVariable(std::string const& name, std::vector> const& ddVariables, std::shared_ptr> manager); + // Explictly generate all default versions of copy/move constructors/assignments. DdMetaVariable(DdMetaVariable const& other) = default; DdMetaVariable& operator=(DdMetaVariable const& other) = default; @@ -47,6 +60,13 @@ namespace storm { */ std::string const& getName() const; + /*! + * Retrieves the type of the meta variable. + * + * @return The type of the meta variable. + */ + MetaVariableType getType() const; + /*! * Retrieves the lowest value of the range of the variable. * @@ -93,6 +113,9 @@ namespace storm { // The name of the meta variable. std::string name; + // The type of the variable. + MetaVariableType type; + // The lowest value of the range of the variable. int_fast64_t low; diff --git a/src/storage/expressions/BinaryBooleanFunctionExpression.cpp b/src/storage/expressions/BinaryBooleanFunctionExpression.cpp index 9f5e5edeb..02cd9686b 100644 --- a/src/storage/expressions/BinaryBooleanFunctionExpression.cpp +++ b/src/storage/expressions/BinaryBooleanFunctionExpression.cpp @@ -23,6 +23,7 @@ namespace storm { switch (this->getOperatorType()) { case OperatorType::And: result = firstOperandEvaluation && secondOperandEvaluation; break; case OperatorType::Or: result = firstOperandEvaluation || secondOperandEvaluation; break; + case OperatorType::Xor: result = firstOperandEvaluation ^ secondOperandEvaluation; break; case OperatorType::Implies: result = !firstOperandEvaluation || secondOperandEvaluation; break; case OperatorType::Iff: result = (firstOperandEvaluation && secondOperandEvaluation) || (!firstOperandEvaluation && !secondOperandEvaluation); break; } @@ -55,6 +56,7 @@ namespace storm { return firstOperandSimplified; } break; + case OperatorType::Xor: break; case OperatorType::Implies: if (firstOperandSimplified->isTrue()) { return secondOperandSimplified; } else if (firstOperandSimplified->isFalse()) { @@ -88,8 +90,9 @@ namespace storm { switch (this->getOperatorType()) { case OperatorType::And: stream << " & "; break; case OperatorType::Or: stream << " | "; break; + case OperatorType::Xor: stream << " != "; break; case OperatorType::Implies: stream << " => "; break; - case OperatorType::Iff: stream << " <=> "; break; + case OperatorType::Iff: stream << " = "; break; } stream << *this->getSecondOperand() << ")"; } diff --git a/src/storage/expressions/BinaryBooleanFunctionExpression.h b/src/storage/expressions/BinaryBooleanFunctionExpression.h index 7a05a1ab5..8b1bb7437 100644 --- a/src/storage/expressions/BinaryBooleanFunctionExpression.h +++ b/src/storage/expressions/BinaryBooleanFunctionExpression.h @@ -11,7 +11,7 @@ namespace storm { /*! * An enum type specifying the different operators applicable. */ - enum class OperatorType {And, Or, Implies, Iff}; + enum class OperatorType {And, Or, Xor, Implies, Iff}; /*! * Creates a binary boolean function expression with the given return type, operands and operator. diff --git a/src/storage/expressions/Expression.cpp b/src/storage/expressions/Expression.cpp index 7eb94966b..90570f244 100644 --- a/src/storage/expressions/Expression.cpp +++ b/src/storage/expressions/Expression.cpp @@ -27,15 +27,21 @@ namespace storm { // Intentionally left empty. } - template class MapType> - Expression Expression::substitute(MapType const& identifierToExpressionMap) const { - return SubstitutionVisitor(identifierToExpressionMap).substitute(this->getBaseExpressionPointer().get()); + Expression Expression::substitute(std::map const& identifierToExpressionMap) const { + return SubstitutionVisitor< std::map >(identifierToExpressionMap).substitute(this->getBaseExpressionPointer().get()); } + + Expression Expression::substitute(std::unordered_map const& identifierToExpressionMap) const { + return SubstitutionVisitor< std::unordered_map >(identifierToExpressionMap).substitute(this->getBaseExpressionPointer().get()); + } - template class MapType> - Expression Expression::substitute(MapType const& identifierToIdentifierMap) const { - return IdentifierSubstitutionVisitor(identifierToIdentifierMap).substitute(this->getBaseExpressionPointer().get()); + Expression Expression::substitute(std::map const& identifierToIdentifierMap) const { + return IdentifierSubstitutionVisitor< std::map >(identifierToIdentifierMap).substitute(this->getBaseExpressionPointer().get()); } + + Expression Expression::substitute(std::unordered_map const& identifierToIdentifierMap) const { + return IdentifierSubstitutionVisitor< std::unordered_map >(identifierToIdentifierMap).substitute(this->getBaseExpressionPointer().get()); + } bool Expression::evaluateAsBool(Valuation const* valuation) const { return this->getBaseExpression().evaluateAsBool(valuation); @@ -166,6 +172,11 @@ namespace storm { return Expression(std::shared_ptr(new BinaryNumericalFunctionExpression(this->getReturnType() == ExpressionReturnType::Int && other.getReturnType() == ExpressionReturnType::Int ? ExpressionReturnType::Int : ExpressionReturnType::Double, this->getBaseExpressionPointer(), other.getBaseExpressionPointer(), BinaryNumericalFunctionExpression::OperatorType::Divide))); } + Expression Expression::operator^(Expression const& other) const { + LOG_THROW(this->hasBooleanReturnType() && other.hasBooleanReturnType(), storm::exceptions::InvalidTypeException, "Operator '^' requires boolean operands."); + return Expression(std::shared_ptr(new BinaryBooleanFunctionExpression(ExpressionReturnType::Bool, this->getBaseExpressionPointer(), other.getBaseExpressionPointer(), BinaryBooleanFunctionExpression::OperatorType::Xor))); + } + Expression Expression::operator&&(Expression const& other) const { LOG_THROW(this->hasBooleanReturnType() && other.hasBooleanReturnType(), storm::exceptions::InvalidTypeException, "Operator '&&' requires boolean operands."); return Expression(std::shared_ptr(new BinaryBooleanFunctionExpression(ExpressionReturnType::Bool, this->getBaseExpressionPointer(), other.getBaseExpressionPointer(), BinaryBooleanFunctionExpression::OperatorType::And))); @@ -247,11 +258,6 @@ namespace storm { return Expression(std::shared_ptr(new UnaryNumericalFunctionExpression(ExpressionReturnType::Int, this->getBaseExpressionPointer(), UnaryNumericalFunctionExpression::OperatorType::Ceil))); } - template Expression Expression::substitute(std::map const&) const; - template Expression Expression::substitute(std::unordered_map const&) const; - template Expression Expression::substitute(std::map const&) const; - template Expression Expression::substitute(std::unordered_map const&) const; - std::ostream& operator<<(std::ostream& stream, Expression const& expression) { stream << expression.getBaseExpression(); return stream; diff --git a/src/storage/expressions/Expression.h b/src/storage/expressions/Expression.h index ea7d99572..15936219c 100644 --- a/src/storage/expressions/Expression.h +++ b/src/storage/expressions/Expression.h @@ -2,6 +2,8 @@ #define STORM_STORAGE_EXPRESSIONS_EXPRESSION_H_ #include +#include +#include #include "src/storage/expressions/BaseExpression.h" #include "src/utility/OsDetection.h" @@ -47,6 +49,7 @@ namespace storm { Expression operator-() const; Expression operator*(Expression const& other) const; Expression operator/(Expression const& other) const; + Expression operator^(Expression const& other) const; Expression operator&&(Expression const& other) const; Expression operator||(Expression const& other) const; Expression operator!() const; @@ -76,8 +79,18 @@ namespace storm { * @return An expression in which all identifiers in the key set of the mapping are replaced by the * expression they are mapped to. */ - template class MapType> - Expression substitute(MapType const& identifierToExpressionMap) const; + Expression substitute(std::map const& identifierToExpressionMap) const; + + /*! + * Substitutes all occurrences of identifiers according to the given map. Note that this substitution is + * done simultaneously, i.e., identifiers appearing in the expressions that were "plugged in" are not + * substituted. + * + * @param identifierToExpressionMap A mapping from identifiers to the expression they are substituted with. + * @return An expression in which all identifiers in the key set of the mapping are replaced by the + * expression they are mapped to. + */ + Expression substitute(std::unordered_map const& identifierToExpressionMap) const; /*! * Substitutes all occurrences of identifiers with different names given by a mapping. @@ -86,8 +99,16 @@ namespace storm { * @return An expression in which all identifiers in the key set of the mapping are replaced by the * identifiers they are mapped to. */ - template class MapType> - Expression substitute(MapType const& identifierToIdentifierMap) const; + Expression substitute(std::map const& identifierToIdentifierMap) const; + + /*! + * Substitutes all occurrences of identifiers with different names given by a mapping. + * + * @param identifierToIdentifierMap A mapping from identifiers to identifiers they are substituted with. + * @return An expression in which all identifiers in the key set of the mapping are replaced by the + * identifiers they are mapped to. + */ + Expression substitute(std::unordered_map const& identifierToIdentifierMap) const; /*! * Evaluates the expression under the valuation of unknowns (variables and constants) given by the diff --git a/src/storage/expressions/IdentifierSubstitutionVisitor.cpp b/src/storage/expressions/IdentifierSubstitutionVisitor.cpp index 17161775a..1b058bed2 100644 --- a/src/storage/expressions/IdentifierSubstitutionVisitor.cpp +++ b/src/storage/expressions/IdentifierSubstitutionVisitor.cpp @@ -1,5 +1,6 @@ #include #include +#include #include "src/storage/expressions/IdentifierSubstitutionVisitor.h" @@ -19,18 +20,18 @@ namespace storm { namespace expressions { - template class MapType> - IdentifierSubstitutionVisitor::IdentifierSubstitutionVisitor(MapType const& identifierToIdentifierMap) : identifierToIdentifierMap(identifierToIdentifierMap) { + template + IdentifierSubstitutionVisitor::IdentifierSubstitutionVisitor(MapType const& identifierToIdentifierMap) : identifierToIdentifierMap(identifierToIdentifierMap) { // Intentionally left empty. } - template class MapType> + template Expression IdentifierSubstitutionVisitor::substitute(BaseExpression const* expression) { expression->accept(this); return Expression(this->expressionStack.top()); } - template class MapType> + template void IdentifierSubstitutionVisitor::visit(IfThenElseExpression const* expression) { expression->getCondition()->accept(this); std::shared_ptr conditionExpression = expressionStack.top(); @@ -52,7 +53,7 @@ namespace storm { } } - template class MapType> + template void IdentifierSubstitutionVisitor::visit(BinaryBooleanFunctionExpression const* expression) { expression->getFirstOperand()->accept(this); std::shared_ptr firstExpression = expressionStack.top(); @@ -70,7 +71,7 @@ namespace storm { } } - template class MapType> + template void IdentifierSubstitutionVisitor::visit(BinaryNumericalFunctionExpression const* expression) { expression->getFirstOperand()->accept(this); std::shared_ptr firstExpression = expressionStack.top(); @@ -88,7 +89,7 @@ namespace storm { } } - template class MapType> + template void IdentifierSubstitutionVisitor::visit(BinaryRelationExpression const* expression) { expression->getFirstOperand()->accept(this); std::shared_ptr firstExpression = expressionStack.top(); @@ -106,7 +107,7 @@ namespace storm { } } - template class MapType> + template void IdentifierSubstitutionVisitor::visit(BooleanConstantExpression const* expression) { // If the boolean constant is in the key set of the substitution, we need to replace it. auto const& namePair = this->identifierToIdentifierMap.find(expression->getConstantName()); @@ -117,7 +118,7 @@ namespace storm { } } - template class MapType> + template void IdentifierSubstitutionVisitor::visit(DoubleConstantExpression const* expression) { // If the double constant is in the key set of the substitution, we need to replace it. auto const& namePair = this->identifierToIdentifierMap.find(expression->getConstantName()); @@ -128,7 +129,7 @@ namespace storm { } } - template class MapType> + template void IdentifierSubstitutionVisitor::visit(IntegerConstantExpression const* expression) { // If the integer constant is in the key set of the substitution, we need to replace it. auto const& namePair = this->identifierToIdentifierMap.find(expression->getConstantName()); @@ -139,7 +140,7 @@ namespace storm { } } - template class MapType> + template void IdentifierSubstitutionVisitor::visit(VariableExpression const* expression) { // If the variable is in the key set of the substitution, we need to replace it. auto const& namePair = this->identifierToIdentifierMap.find(expression->getVariableName()); @@ -150,7 +151,7 @@ namespace storm { } } - template class MapType> + template void IdentifierSubstitutionVisitor::visit(UnaryBooleanFunctionExpression const* expression) { expression->getOperand()->accept(this); std::shared_ptr operandExpression = expressionStack.top(); @@ -164,7 +165,7 @@ namespace storm { } } - template class MapType> + template void IdentifierSubstitutionVisitor::visit(UnaryNumericalFunctionExpression const* expression) { expression->getOperand()->accept(this); std::shared_ptr operandExpression = expressionStack.top(); @@ -178,23 +179,23 @@ namespace storm { } } - template class MapType> + template void IdentifierSubstitutionVisitor::visit(BooleanLiteralExpression const* expression) { this->expressionStack.push(expression->getSharedPointer()); } - template class MapType> + template void IdentifierSubstitutionVisitor::visit(IntegerLiteralExpression const* expression) { this->expressionStack.push(expression->getSharedPointer()); } - template class MapType> + template void IdentifierSubstitutionVisitor::visit(DoubleLiteralExpression const* expression) { this->expressionStack.push(expression->getSharedPointer()); } // Explicitly instantiate the class with map and unordered_map. - template class IdentifierSubstitutionVisitor; - template class IdentifierSubstitutionVisitor; + template class IdentifierSubstitutionVisitor< std::map >; + template class IdentifierSubstitutionVisitor< std::unordered_map >; } } diff --git a/src/storage/expressions/IdentifierSubstitutionVisitor.h b/src/storage/expressions/IdentifierSubstitutionVisitor.h index 6be7aa9ca..e8412d949 100644 --- a/src/storage/expressions/IdentifierSubstitutionVisitor.h +++ b/src/storage/expressions/IdentifierSubstitutionVisitor.h @@ -8,7 +8,7 @@ namespace storm { namespace expressions { - template class MapType> + template class IdentifierSubstitutionVisitor : public ExpressionVisitor { public: /*! @@ -16,7 +16,7 @@ namespace storm { * * @param identifierToExpressionMap A mapping from identifiers to expressions. */ - IdentifierSubstitutionVisitor(MapType const& identifierToExpressionMap); + IdentifierSubstitutionVisitor(MapType const& identifierToExpressionMap); /*! * Substitutes the identifiers in the given expression according to the previously given map and returns the @@ -47,7 +47,7 @@ namespace storm { std::stack> expressionStack; // A mapping of identifier names to expressions with which they shall be replaced. - MapType const& identifierToIdentifierMap; + MapType const& identifierToIdentifierMap; }; } } diff --git a/src/storage/expressions/SimpleValuation.cpp b/src/storage/expressions/SimpleValuation.cpp index 6674dfbd3..d29e6a7c8 100644 --- a/src/storage/expressions/SimpleValuation.cpp +++ b/src/storage/expressions/SimpleValuation.cpp @@ -1,6 +1,7 @@ -#include "src/storage/expressions/SimpleValuation.h" - #include +#include "src/storage/expressions/SimpleValuation.h" +#include "src/exceptions/ExceptionMacros.h" +#include "src/exceptions/InvalidArgumentException.h" namespace storm { namespace expressions { @@ -13,16 +14,22 @@ namespace storm { } void SimpleValuation::addBooleanIdentifier(std::string const& name, bool initialValue) { + LOG_THROW(this->booleanIdentifierToIndexMap->find(name) == this->booleanIdentifierToIndexMap->end(), storm::exceptions::InvalidArgumentException, "Boolean identifier '" << name << "' already registered."); + this->booleanIdentifierToIndexMap->emplace(name, this->booleanValues.size()); this->booleanValues.push_back(initialValue); } void SimpleValuation::addIntegerIdentifier(std::string const& name, int_fast64_t initialValue) { + LOG_THROW(this->booleanIdentifierToIndexMap->find(name) == this->booleanIdentifierToIndexMap->end(), storm::exceptions::InvalidArgumentException, "Integer identifier '" << name << "' already registered."); + this->integerIdentifierToIndexMap->emplace(name, this->integerValues.size()); this->integerValues.push_back(initialValue); } void SimpleValuation::addDoubleIdentifier(std::string const& name, double initialValue) { + LOG_THROW(this->booleanIdentifierToIndexMap->find(name) == this->booleanIdentifierToIndexMap->end(), storm::exceptions::InvalidArgumentException, "Double identifier '" << name << "' already registered."); + this->doubleIdentifierToIndexMap->emplace(name, this->doubleValues.size()); this->doubleValues.push_back(initialValue); } diff --git a/src/storage/expressions/SimpleValuation.h b/src/storage/expressions/SimpleValuation.h index 35b74291b..a196921a6 100644 --- a/src/storage/expressions/SimpleValuation.h +++ b/src/storage/expressions/SimpleValuation.h @@ -7,6 +7,7 @@ #include #include "src/storage/expressions/Valuation.h" +#include "src/utility/OsDetection.h" namespace storm { namespace expressions { @@ -23,8 +24,10 @@ namespace storm { // Instantiate some constructors and assignments with their default implementations. SimpleValuation(SimpleValuation const&) = default; SimpleValuation& operator=(SimpleValuation const&) = default; - SimpleValuation(SimpleValuation&&) = default; +#ifndef WINDOWS + SimpleValuation(SimpleValuation&&) = default; SimpleValuation& operator=(SimpleValuation&&) = default; +#endif virtual ~SimpleValuation() = default; /*! diff --git a/src/storage/expressions/SubstitutionVisitor.cpp b/src/storage/expressions/SubstitutionVisitor.cpp index c3f2ea0a8..54b533d49 100644 --- a/src/storage/expressions/SubstitutionVisitor.cpp +++ b/src/storage/expressions/SubstitutionVisitor.cpp @@ -1,5 +1,6 @@ #include #include +#include #include "src/storage/expressions/SubstitutionVisitor.h" @@ -19,18 +20,18 @@ namespace storm { namespace expressions { - template class MapType> - SubstitutionVisitor::SubstitutionVisitor(MapType const& identifierToExpressionMap) : identifierToExpressionMap(identifierToExpressionMap) { + template + SubstitutionVisitor::SubstitutionVisitor(MapType const& identifierToExpressionMap) : identifierToExpressionMap(identifierToExpressionMap) { // Intentionally left empty. } - template class MapType> + template Expression SubstitutionVisitor::substitute(BaseExpression const* expression) { expression->accept(this); return Expression(this->expressionStack.top()); } - template class MapType> + template void SubstitutionVisitor::visit(IfThenElseExpression const* expression) { expression->getCondition()->accept(this); std::shared_ptr conditionExpression = expressionStack.top(); @@ -52,7 +53,7 @@ namespace storm { } } - template class MapType> + template void SubstitutionVisitor::visit(BinaryBooleanFunctionExpression const* expression) { expression->getFirstOperand()->accept(this); std::shared_ptr firstExpression = expressionStack.top(); @@ -70,7 +71,7 @@ namespace storm { } } - template class MapType> + template void SubstitutionVisitor::visit(BinaryNumericalFunctionExpression const* expression) { expression->getFirstOperand()->accept(this); std::shared_ptr firstExpression = expressionStack.top(); @@ -88,7 +89,7 @@ namespace storm { } } - template class MapType> + template void SubstitutionVisitor::visit(BinaryRelationExpression const* expression) { expression->getFirstOperand()->accept(this); std::shared_ptr firstExpression = expressionStack.top(); @@ -106,7 +107,7 @@ namespace storm { } } - template class MapType> + template void SubstitutionVisitor::visit(BooleanConstantExpression const* expression) { // If the boolean constant is in the key set of the substitution, we need to replace it. auto const& nameExpressionPair = this->identifierToExpressionMap.find(expression->getConstantName()); @@ -117,7 +118,7 @@ namespace storm { } } - template class MapType> + template void SubstitutionVisitor::visit(DoubleConstantExpression const* expression) { // If the double constant is in the key set of the substitution, we need to replace it. auto const& nameExpressionPair = this->identifierToExpressionMap.find(expression->getConstantName()); @@ -128,7 +129,7 @@ namespace storm { } } - template class MapType> + template void SubstitutionVisitor::visit(IntegerConstantExpression const* expression) { // If the integer constant is in the key set of the substitution, we need to replace it. auto const& nameExpressionPair = this->identifierToExpressionMap.find(expression->getConstantName()); @@ -139,7 +140,7 @@ namespace storm { } } - template class MapType> + template void SubstitutionVisitor::visit(VariableExpression const* expression) { // If the variable is in the key set of the substitution, we need to replace it. auto const& nameExpressionPair = this->identifierToExpressionMap.find(expression->getVariableName()); @@ -150,7 +151,7 @@ namespace storm { } } - template class MapType> + template void SubstitutionVisitor::visit(UnaryBooleanFunctionExpression const* expression) { expression->getOperand()->accept(this); std::shared_ptr operandExpression = expressionStack.top(); @@ -164,7 +165,7 @@ namespace storm { } } - template class MapType> + template void SubstitutionVisitor::visit(UnaryNumericalFunctionExpression const* expression) { expression->getOperand()->accept(this); std::shared_ptr operandExpression = expressionStack.top(); @@ -178,23 +179,23 @@ namespace storm { } } - template class MapType> + template void SubstitutionVisitor::visit(BooleanLiteralExpression const* expression) { this->expressionStack.push(expression->getSharedPointer()); } - template class MapType> + template void SubstitutionVisitor::visit(IntegerLiteralExpression const* expression) { this->expressionStack.push(expression->getSharedPointer()); } - template class MapType> + template void SubstitutionVisitor::visit(DoubleLiteralExpression const* expression) { this->expressionStack.push(expression->getSharedPointer()); } // Explicitly instantiate the class with map and unordered_map. - template class SubstitutionVisitor; - template class SubstitutionVisitor; + template class SubstitutionVisitor< std::map >; + template class SubstitutionVisitor< std::unordered_map >; } } diff --git a/src/storage/expressions/SubstitutionVisitor.h b/src/storage/expressions/SubstitutionVisitor.h index ad29ad6ab..d46d62cee 100644 --- a/src/storage/expressions/SubstitutionVisitor.h +++ b/src/storage/expressions/SubstitutionVisitor.h @@ -8,7 +8,7 @@ namespace storm { namespace expressions { - template class MapType> + template class SubstitutionVisitor : public ExpressionVisitor { public: /*! @@ -16,7 +16,7 @@ namespace storm { * * @param identifierToExpressionMap A mapping from identifiers to expressions. */ - SubstitutionVisitor(MapType const& identifierToExpressionMap); + SubstitutionVisitor(MapType const& identifierToExpressionMap); /*! * Substitutes the identifiers in the given expression according to the previously given map and returns the @@ -47,7 +47,7 @@ namespace storm { std::stack> expressionStack; // A mapping of identifier names to expressions with which they shall be replaced. - MapType const& identifierToExpressionMap; + MapType const& identifierToExpressionMap; }; } } diff --git a/src/storage/prism/Assignment.cpp b/src/storage/prism/Assignment.cpp index f15797e6d..3b63703ed 100644 --- a/src/storage/prism/Assignment.cpp +++ b/src/storage/prism/Assignment.cpp @@ -15,7 +15,7 @@ namespace storm { } Assignment Assignment::substitute(std::map const& substitution) const { - return Assignment(this->getVariableName(), this->getExpression().substitute(substitution), this->getFilename(), this->getLineNumber()); + return Assignment(this->getVariableName(), this->getExpression().substitute(substitution), this->getFilename(), this->getLineNumber()); } std::ostream& operator<<(std::ostream& stream, Assignment const& assignment) { diff --git a/src/storage/prism/BooleanVariable.cpp b/src/storage/prism/BooleanVariable.cpp index 478b9322d..ef88cefc4 100644 --- a/src/storage/prism/BooleanVariable.cpp +++ b/src/storage/prism/BooleanVariable.cpp @@ -11,7 +11,7 @@ namespace storm { } BooleanVariable BooleanVariable::substitute(std::map const& substitution) const { - return BooleanVariable(this->getName(), this->getInitialValueExpression().substitute(substitution), this->getFilename(), this->getLineNumber()); + return BooleanVariable(this->getName(), this->getInitialValueExpression().substitute(substitution), this->getFilename(), this->getLineNumber()); } std::ostream& operator<<(std::ostream& stream, BooleanVariable const& variable) { diff --git a/src/storage/prism/Command.cpp b/src/storage/prism/Command.cpp index f075ff6c6..4b36942df 100644 --- a/src/storage/prism/Command.cpp +++ b/src/storage/prism/Command.cpp @@ -37,7 +37,7 @@ namespace storm { newUpdates.emplace_back(update.substitute(substitution)); } - return Command(this->getGlobalIndex(), this->getActionName(), this->getGuardExpression().substitute(substitution), newUpdates, this->getFilename(), this->getLineNumber()); + return Command(this->getGlobalIndex(), this->getActionName(), this->getGuardExpression().substitute(substitution), newUpdates, this->getFilename(), this->getLineNumber()); } std::ostream& operator<<(std::ostream& stream, Command const& command) { diff --git a/src/storage/prism/Constant.cpp b/src/storage/prism/Constant.cpp index 160e9ad22..641336c76 100644 --- a/src/storage/prism/Constant.cpp +++ b/src/storage/prism/Constant.cpp @@ -1,4 +1,6 @@ #include "src/storage/prism/Constant.h" +#include "src/exceptions/ExceptionMacros.h" +#include "src/exceptions/IllegalFunctionCallException.h" namespace storm { namespace prism { @@ -23,11 +25,12 @@ namespace storm { } storm::expressions::Expression const& Constant::getExpression() const { + LOG_THROW(this->isDefined(), storm::exceptions::IllegalFunctionCallException, "Unable to retrieve defining expression for undefined constant."); return this->expression; } Constant Constant::substitute(std::map const& substitution) const { - return Constant(this->getType(), this->getName(), this->getExpression().substitute(substitution), this->getFilename(), this->getLineNumber()); + return Constant(this->getType(), this->getName(), this->getExpression().substitute(substitution), this->getFilename(), this->getLineNumber()); } std::ostream& operator<<(std::ostream& stream, Constant const& constant) { diff --git a/src/storage/prism/Formula.cpp b/src/storage/prism/Formula.cpp index 3bf72a7de..fbda0c69d 100644 --- a/src/storage/prism/Formula.cpp +++ b/src/storage/prism/Formula.cpp @@ -19,7 +19,7 @@ namespace storm { } Formula Formula::substitute(std::map const& substitution) const { - return Formula(this->getName(), this->getExpression().substitute(substitution), this->getFilename(), this->getLineNumber()); + return Formula(this->getName(), this->getExpression().substitute(substitution), this->getFilename(), this->getLineNumber()); } std::ostream& operator<<(std::ostream& stream, Formula const& formula) { diff --git a/src/storage/prism/IntegerVariable.cpp b/src/storage/prism/IntegerVariable.cpp index a80b6394e..1968a07ca 100644 --- a/src/storage/prism/IntegerVariable.cpp +++ b/src/storage/prism/IntegerVariable.cpp @@ -19,7 +19,7 @@ namespace storm { } IntegerVariable IntegerVariable::substitute(std::map const& substitution) const { - return IntegerVariable(this->getName(), this->getLowerBoundExpression().substitute(substitution), this->getUpperBoundExpression().substitute(substitution), this->getInitialValueExpression().substitute(substitution), this->getFilename(), this->getLineNumber()); + return IntegerVariable(this->getName(), this->getLowerBoundExpression().substitute(substitution), this->getUpperBoundExpression().substitute(substitution), this->getInitialValueExpression().substitute(substitution), this->getFilename(), this->getLineNumber()); } std::ostream& operator<<(std::ostream& stream, IntegerVariable const& variable) { diff --git a/src/storage/prism/Label.cpp b/src/storage/prism/Label.cpp index a78f9079f..cb8a13f25 100644 --- a/src/storage/prism/Label.cpp +++ b/src/storage/prism/Label.cpp @@ -15,7 +15,7 @@ namespace storm { } Label Label::substitute(std::map const& substitution) const { - return Label(this->getName(), this->getStatePredicateExpression().substitute(substitution), this->getFilename(), this->getLineNumber()); + return Label(this->getName(), this->getStatePredicateExpression().substitute(substitution), this->getFilename(), this->getLineNumber()); } std::ostream& operator<<(std::ostream& stream, Label const& label) { diff --git a/src/storage/prism/LocatedInformation.h b/src/storage/prism/LocatedInformation.h index 8aa4d301e..81f5334b5 100644 --- a/src/storage/prism/LocatedInformation.h +++ b/src/storage/prism/LocatedInformation.h @@ -2,6 +2,7 @@ #define STORM_STORAGE_PRISM_LOCATEDINFORMATION_H_ #include +#include #include "src/utility/OsDetection.h" diff --git a/src/storage/prism/Program.cpp b/src/storage/prism/Program.cpp index 4b2996cb8..585695d4e 100644 --- a/src/storage/prism/Program.cpp +++ b/src/storage/prism/Program.cpp @@ -229,7 +229,7 @@ namespace storm { LOG_THROW(constantDefinitions.find(constant.getName()) == constantDefinitions.end(), storm::exceptions::InvalidArgumentException, "Illegally defining already defined constant '" << constant.getName() << "'."); // Now replace the occurrences of undefined constants in its defining expression. - newConstants.emplace_back(constant.getType(), constant.getName(), constant.getExpression().substitute(constantDefinitions), constant.getFilename(), constant.getLineNumber()); + newConstants.emplace_back(constant.getType(), constant.getName(), constant.getExpression().substitute(constantDefinitions), constant.getFilename(), constant.getLineNumber()); } else { auto const& variableExpressionPair = constantDefinitions.find(constant.getName()); @@ -310,7 +310,7 @@ namespace storm { newRewardModels.emplace_back(rewardModel.substitute(constantSubstitution)); } - storm::expressions::Expression newInitialStateExpression = this->getInitialStatesExpression().substitute(constantSubstitution); + storm::expressions::Expression newInitialStateExpression = this->getInitialStatesExpression().substitute(constantSubstitution); std::vector