From d62539165e028328e4d58aabca76c5a8f3c08398 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Mon, 3 Aug 2015 15:36:45 +0200
Subject: [PATCH 1/3] 'Identity updates' can now be described as applying
'true' in PRISM programs.
Former-commit-id: b2f70eb465618290b2bd9467bd8254ef2a49c273
---
src/parser/PrismParser.cpp | 2 +-
test/functional/parser/PrismParserTest.cpp | 1 +
2 files changed, 2 insertions(+), 1 deletion(-)
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());
From ecb37ccd1d9b16186954f4fe1362da718b6d1929 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Mon, 3 Aug 2015 16:09:49 +0200
Subject: [PATCH 2/3] made compilation of ConstraintCollector in Dtmc
predicated on CARL being available
Former-commit-id: 8d0e3ea6365fc72ee266c1aeae49024599b895ec
---
src/models/sparse/Dtmc.cpp | 2 ++
src/models/sparse/Dtmc.h | 2 ++
2 files changed, 4 insertions(+)
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..43ec31487 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.
@@ -118,6 +119,7 @@ namespace storm {
*/
bool checkValidityOfProbabilityMatrix() const;
};
+#endif
} // namespace sparse
} // namespace models
From f879c608ebaa288a118395eb487b75b002e548d6 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Mon, 3 Aug 2015 16:25:09 +0200
Subject: [PATCH 3/3] fix for wrong ifdef
Former-commit-id: dd17e10d08a5d1daadede33e0a8ad3dfad3db08c
---
src/models/sparse/Dtmc.h | 4 ++--
1 file changed, 2 insertions(+), 2 deletions(-)
diff --git a/src/models/sparse/Dtmc.h b/src/models/sparse/Dtmc.h
index 43ec31487..af1d2ad3f 100644
--- a/src/models/sparse/Dtmc.h
+++ b/src/models/sparse/Dtmc.h
@@ -110,7 +110,8 @@ namespace storm {
void operator()(storm::models::sparse::Dtmc<ValueType> const& dtmc);
};
-
+#endif
+
private:
/*!
* Checks the probability matrix for validity.
@@ -119,7 +120,6 @@ namespace storm {
*/
bool checkValidityOfProbabilityMatrix() const;
};
-#endif
} // namespace sparse
} // namespace models