diff --git a/src/models/sparse/Dtmc.cpp b/src/models/sparse/Dtmc.cpp index f2f197428..f1248af39 100644 --- a/src/models/sparse/Dtmc.cpp +++ b/src/models/sparse/Dtmc.cpp @@ -182,6 +182,7 @@ namespace storm { // return storm::models::Dtmc<ValueType>(newMatBuilder.build(), newLabeling, newStateRewards, std::move(newTransitionRewards), newChoiceLabels); } +#ifdef STORM_HAVE_CARL template<typename ValueType> Dtmc<ValueType>::ConstraintCollector::ConstraintCollector(Dtmc<ValueType> const& dtmc) { process(dtmc); @@ -221,6 +222,7 @@ namespace storm { void Dtmc<ValueType>::ConstraintCollector::operator()(storm::models::sparse::Dtmc<ValueType> const& dtmc) { process(dtmc); } +#endif template <typename ValueType> bool Dtmc<ValueType>::checkValidityOfProbabilityMatrix() const { diff --git a/src/models/sparse/Dtmc.h b/src/models/sparse/Dtmc.h index 37095f05e..af1d2ad3f 100644 --- a/src/models/sparse/Dtmc.h +++ b/src/models/sparse/Dtmc.h @@ -59,6 +59,7 @@ namespace storm { */ Dtmc<ValueType> getSubDtmc(storm::storage::BitVector const& states) const; +#ifdef STORM_HAVE_CARL class ConstraintCollector { private: // A set of constraints that says that the DTMC actually has valid probability distributions in all states. @@ -109,7 +110,8 @@ namespace storm { void operator()(storm::models::sparse::Dtmc<ValueType> const& dtmc); }; - +#endif + private: /*! * Checks the probability matrix for validity. diff --git a/src/parser/PrismParser.cpp b/src/parser/PrismParser.cpp index a7e1f522d..bff8c71b8 100644 --- a/src/parser/PrismParser.cpp +++ b/src/parser/PrismParser.cpp @@ -133,7 +133,7 @@ namespace storm { assignmentDefinition = (qi::lit("(") > identifier > qi::lit("'") > qi::lit("=") > expressionParser > qi::lit(")"))[qi::_val = phoenix::bind(&PrismParser::createAssignment, phoenix::ref(*this), qi::_1, qi::_2)]; assignmentDefinition.name("assignment"); - assignmentDefinitionList %= +assignmentDefinition % "&"; + assignmentDefinitionList = (assignmentDefinition % "&")[qi::_val = qi::_1] | (qi::lit("true"))[qi::_val = phoenix::construct<std::vector<storm::prism::Assignment>>()]; assignmentDefinitionList.name("assignment list"); updateDefinition = (((expressionParser > qi::lit(":")) | qi::attr(manager->rational(1))) >> assignmentDefinitionList)[qi::_val = phoenix::bind(&PrismParser::createUpdate, phoenix::ref(*this), qi::_1, qi::_2, qi::_r1)]; diff --git a/test/functional/parser/PrismParserTest.cpp b/test/functional/parser/PrismParserTest.cpp index a3fbc7526..e386b7682 100644 --- a/test/functional/parser/PrismParserTest.cpp +++ b/test/functional/parser/PrismParserTest.cpp @@ -40,6 +40,7 @@ TEST(PrismParser, SimpleTest) { [] x=3 -> 1:(x'=1); [] x=3 -> 1:(x'=4); [] x=4 -> 1:(x'=5); + [] x=5 -> 1: true; endmodule)"; EXPECT_NO_THROW(result = storm::parser::PrismParser::parseFromString(testInput, "testfile")); EXPECT_EQ(1, result.getNumberOfModules());