Merge branch 'master' of https://sselab.de/lab9/private/git/storm

Former-commit-id: 92d7f60455

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 {

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.

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)];

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());