From e43dfc278409729580d78ce4f9a4a8a527d4e4c6 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Thu, 11 Aug 2016 16:24:43 +0200
Subject: [PATCH 01/20] removed unused setting
Former-commit-id: 18a91c2acb82ec553b91370047e20e4ef3872281
---
src/settings/modules/CoreSettings.cpp | 5 -----
src/settings/modules/CoreSettings.h | 1 -
2 files changed, 6 deletions(-)
diff --git a/src/settings/modules/CoreSettings.cpp b/src/settings/modules/CoreSettings.cpp
index b42a301c8..5a6dfc9c0 100644
--- a/src/settings/modules/CoreSettings.cpp
+++ b/src/settings/modules/CoreSettings.cpp
@@ -30,7 +30,6 @@ namespace storm {
const std::string CoreSettings::engineOptionShortName = "e";
const std::string CoreSettings::ddLibraryOptionName = "ddlib";
const std::string CoreSettings::cudaOptionName = "cuda";
- const std::string CoreSettings::minMaxEquationSolvingTechniqueOptionName = "ndmethod";
CoreSettings::CoreSettings() : ModuleSettings(moduleName), engine(CoreSettings::Engine::Sparse) {
this->addOption(storm::settings::OptionBuilder(moduleName, counterexampleOptionName, false, "Generates a counterexample for the given PRCTL formulas if not satisfied by the model")
@@ -57,10 +56,6 @@ namespace storm {
.addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of an SMT solver. Available are: z3 and mathsat.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(smtSolvers)).setDefaultValueString("z3").build()).build());
this->addOption(storm::settings::OptionBuilder(moduleName, statisticsOptionName, false, "Sets whether to display statistics if available.").setShortName(statisticsOptionShortName).build());
this->addOption(storm::settings::OptionBuilder(moduleName, cudaOptionName, false, "Sets whether to use CUDA to speed up computation time.").build());
-
- std::vector<std::string> minMaxSolvingTechniques = {"vi", "value-iteration", "pi", "policy-iteration"};
- this->addOption(storm::settings::OptionBuilder(moduleName, minMaxEquationSolvingTechniqueOptionName, false, "Sets which min/max linear equation solving technique is preferred.")
- .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of a min/max linear equation solving technique. Available are: value-iteration (vi) and policy-iteration (pi).").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(minMaxSolvingTechniques)).setDefaultValueString("vi").build()).build());
}
bool CoreSettings::isCounterexampleSet() const {
diff --git a/src/settings/modules/CoreSettings.h b/src/settings/modules/CoreSettings.h
index 9b7189e2c..f6c8fbdf2 100644
--- a/src/settings/modules/CoreSettings.h
+++ b/src/settings/modules/CoreSettings.h
@@ -151,7 +151,6 @@ namespace storm {
static const std::string engineOptionShortName;
static const std::string ddLibraryOptionName;
static const std::string cudaOptionName;
- static const std::string minMaxEquationSolvingTechniqueOptionName;
};
} // namespace modules
From 7ab88457a71851fe7d1245d0aedebac1c4fdff5c Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Thu, 11 Aug 2016 18:07:58 +0200
Subject: [PATCH 02/20] corrected reference to wrong settings module
Former-commit-id: 2f35b2dc82efbb76fed5fb17696a13599d9fadd7
---
src/storm.cpp | 13 +++++++------
1 file changed, 7 insertions(+), 6 deletions(-)
diff --git a/src/storm.cpp b/src/storm.cpp
index 0d23f9ecc..236d15a7b 100644
--- a/src/storm.cpp
+++ b/src/storm.cpp
@@ -6,6 +6,7 @@
#include "src/utility/initialize.h"
#include "src/settings/SettingsManager.h"
+#include "src/settings/modules/GeneralSettings.h"
/*!
* Main entry point of the executable storm.
@@ -13,7 +14,7 @@
int main(const int argc, const char** argv) {
try {
- auto starttime = std::chrono::high_resolution_clock::now();
+ auto start = std::chrono::high_resolution_clock::now();
storm::utility::setUp();
storm::cli::printHeader("Storm", argc, argv);
storm::settings::initializeAll("Storm", "storm");
@@ -27,11 +28,11 @@ int main(const int argc, const char** argv) {
// All operations have now been performed, so we clean up everything and terminate.
storm::utility::cleanUp();
- auto endtime = std::chrono::high_resolution_clock::now();
- auto duration = std::chrono::duration_cast<std::chrono::milliseconds>(endtime-starttime);
- auto durationSec = std::chrono::duration_cast<std::chrono::seconds>(endtime-starttime);
- if(storm::settings::getModule<storm::settings::modules::IOSettings>().isPrintTimingsSet()) {
- std::cout << "Overal runtime: " << duration.count() << " ms. ( approx " << durationSec.count() << " seconds)." << std::endl;
+ auto end = std::chrono::high_resolution_clock::now();
+ auto duration = std::chrono::duration_cast<std::chrono::milliseconds>(end - start);
+ auto durationSec = std::chrono::duration_cast<std::chrono::seconds>(end - start);
+ if(storm::settings::getModule<storm::settings::modules::GeneralSettings>().isPrintTimingsSet()) {
+ std::cout << "Overal runtime: " << duration.count() << " ms. (approximately " << durationSec.count() << " seconds)." << std::endl;
}
return 0;
} catch (storm::exceptions::BaseException const& exception) {
From 569b27e11055cb63a1c7c183d1abeff743a242ea Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Mon, 15 Aug 2016 14:49:21 +0200
Subject: [PATCH 03/20] work towards having rational numbers instead of doubles
as literals in expressions
Former-commit-id: c62f8af0612a5cc4c351d79cd224f6439b523e99
---
src/adapters/AddExpressionAdapter.cpp | 2 +-
src/adapters/MathsatExpressionAdapter.h | 2 +-
.../expressions/DoubleLiteralExpression.cpp | 16 ++++-
.../expressions/DoubleLiteralExpression.h | 25 ++++++--
.../expressions/LinearCoefficientVisitor.cpp | 2 +-
.../expressions/ToRationalFunctionVisitor.cpp | 3 +-
.../expressions/ToRationalNumberVisitor.cpp | 29 ++++++---
src/utility/constants.cpp | 61 ++++++++++++++++---
src/utility/constants.h | 3 +
9 files changed, 114 insertions(+), 29 deletions(-)
diff --git a/src/adapters/AddExpressionAdapter.cpp b/src/adapters/AddExpressionAdapter.cpp
index e50620db8..7a22c8f8f 100644
--- a/src/adapters/AddExpressionAdapter.cpp
+++ b/src/adapters/AddExpressionAdapter.cpp
@@ -195,7 +195,7 @@ namespace storm {
template<storm::dd::DdType Type, typename ValueType>
boost::any AddExpressionAdapter<Type, ValueType>::visit(storm::expressions::DoubleLiteralExpression const& expression) {
- return ddManager->getConstant(static_cast<ValueType>(expression.getValue()));
+ return ddManager->getConstant(static_cast<ValueType>(expression.getValueAsDouble()));
}
// Explicitly instantiate the symbolic expression adapter
diff --git a/src/adapters/MathsatExpressionAdapter.h b/src/adapters/MathsatExpressionAdapter.h
index 9fec0cf15..db5bf9b69 100644
--- a/src/adapters/MathsatExpressionAdapter.h
+++ b/src/adapters/MathsatExpressionAdapter.h
@@ -172,7 +172,7 @@ namespace storm {
}
virtual boost::any visit(expressions::DoubleLiteralExpression const& expression) override {
- return msat_make_number(env, std::to_string(expression.getValue()).c_str());
+ return msat_make_number(env, std::to_string(expression.getValueAsDouble()).c_str());
}
virtual boost::any visit(expressions::IntegerLiteralExpression const& expression) override {
diff --git a/src/storage/expressions/DoubleLiteralExpression.cpp b/src/storage/expressions/DoubleLiteralExpression.cpp
index cab9fc31b..192d747ee 100644
--- a/src/storage/expressions/DoubleLiteralExpression.cpp
+++ b/src/storage/expressions/DoubleLiteralExpression.cpp
@@ -2,14 +2,20 @@
#include "src/storage/expressions/ExpressionManager.h"
#include "src/storage/expressions/ExpressionVisitor.h"
+#include "src/utility/constants.h"
+
namespace storm {
namespace expressions {
- DoubleLiteralExpression::DoubleLiteralExpression(ExpressionManager const& manager, double value) : BaseExpression(manager, manager.getRationalType()), value(value) {
+ DoubleLiteralExpression::DoubleLiteralExpression(ExpressionManager const& manager, double value) : BaseExpression(manager, manager.getRationalType()), value(storm::utility::convertNumber<storm::RationalNumber>(value)) {
+ // Intentionally left empty.
+ }
+
+ DoubleLiteralExpression::DoubleLiteralExpression(ExpressionManager const& manager, std::string const& valueAsString) : BaseExpression(manager, manager.getRationalType()), value(storm::utility::convertNumber<storm::RationalNumber>(valueAsString)) {
// Intentionally left empty.
}
double DoubleLiteralExpression::evaluateAsDouble(Valuation const* valuation) const {
- return this->getValue();
+ return this->getValueAsDouble();
}
bool DoubleLiteralExpression::isLiteral() const {
@@ -28,7 +34,11 @@ namespace storm {
return visitor.visit(*this);
}
- double DoubleLiteralExpression::getValue() const {
+ double DoubleLiteralExpression::getValueAsDouble() const {
+ return storm::utility::convertNumber<double>(this->value);
+ }
+
+ storm::RationalNumber DoubleLiteralExpression::getValue() const {
return this->value;
}
diff --git a/src/storage/expressions/DoubleLiteralExpression.h b/src/storage/expressions/DoubleLiteralExpression.h
index 676291a77..6a04f23e3 100644
--- a/src/storage/expressions/DoubleLiteralExpression.h
+++ b/src/storage/expressions/DoubleLiteralExpression.h
@@ -4,6 +4,8 @@
#include "src/storage/expressions/BaseExpression.h"
#include "src/utility/OsDetection.h"
+#include "src/adapters/CarlAdapter.h"
+
namespace storm {
namespace expressions {
class DoubleLiteralExpression : public BaseExpression {
@@ -15,7 +17,15 @@ namespace storm {
* @param value The value of the double literal.
*/
DoubleLiteralExpression(ExpressionManager const& manager, double value);
-
+
+ /*!
+ * Creates an double literal expression with the value given as a string.
+ *
+ * @param manager The manager responsible for this expression.
+ * @param value The string representation of the value of the literal.
+ */
+ DoubleLiteralExpression(ExpressionManager const& manager, std::string const& valueAsString);
+
// Instantiate constructors and assignments with their default implementations.
DoubleLiteralExpression(DoubleLiteralExpression const& other) = default;
DoubleLiteralExpression& operator=(DoubleLiteralExpression const& other) = delete;
@@ -37,15 +47,22 @@ namespace storm {
*
* @return The value of the double literal.
*/
- double getValue() const;
+ double getValueAsDouble() const;
+
+ /*!
+ * Retrieves the value of the double literal.
+ *
+ * @return The value of the double literal.
+ */
+ storm::RationalNumber getValue() const;
protected:
// Override base class method.
virtual void printToStream(std::ostream& stream) const override;
private:
- // The value of the double literal.
- double value;
+ // The value of the literal.
+ storm::RationalNumber value;
};
}
}
diff --git a/src/storage/expressions/LinearCoefficientVisitor.cpp b/src/storage/expressions/LinearCoefficientVisitor.cpp
index 8d7f39278..3d881c25e 100644
--- a/src/storage/expressions/LinearCoefficientVisitor.cpp
+++ b/src/storage/expressions/LinearCoefficientVisitor.cpp
@@ -152,7 +152,7 @@ namespace storm {
}
boost::any LinearCoefficientVisitor::visit(DoubleLiteralExpression const& expression) {
- return VariableCoefficients(expression.getValue());
+ return VariableCoefficients(expression.getValueAsDouble());
}
}
}
\ No newline at end of file
diff --git a/src/storage/expressions/ToRationalFunctionVisitor.cpp b/src/storage/expressions/ToRationalFunctionVisitor.cpp
index 1a3dd0fc3..533fa1f1f 100644
--- a/src/storage/expressions/ToRationalFunctionVisitor.cpp
+++ b/src/storage/expressions/ToRationalFunctionVisitor.cpp
@@ -2,6 +2,7 @@
#include <sstream>
+#include "src/utility/constants.h"
#include "src/utility/macros.h"
#include "src/exceptions/InvalidArgumentException.h"
@@ -93,7 +94,7 @@ namespace storm {
template<typename RationalFunctionType>
boost::any ToRationalFunctionVisitor<RationalFunctionType>::visit(DoubleLiteralExpression const& expression) {
- return RationalFunctionType(carl::rationalize<storm::RationalNumber>(expression.getValue()));
+ return storm::utility::convertNumber<storm::RationalFunction>(expression.getValue());
}
template class ToRationalFunctionVisitor<storm::RationalFunction>;
diff --git a/src/storage/expressions/ToRationalNumberVisitor.cpp b/src/storage/expressions/ToRationalNumberVisitor.cpp
index 785f36950..44194cb4b 100644
--- a/src/storage/expressions/ToRationalNumberVisitor.cpp
+++ b/src/storage/expressions/ToRationalNumberVisitor.cpp
@@ -1,6 +1,7 @@
#include "src/storage/expressions/ToRationalNumberVisitor.h"
#include "src/utility/macros.h"
+#include "src/utility/constants.h"
#include "src/exceptions/InvalidArgumentException.h"
#include "src/exceptions/NotSupportedException.h"
@@ -28,26 +29,36 @@ namespace storm {
template<typename RationalNumberType>
boost::any ToRationalNumberVisitor<RationalNumberType>::visit(BinaryNumericalFunctionExpression const& expression) {
- RationalNumberType firstOperandAsRationalFunction = boost::any_cast<RationalNumberType>(expression.getFirstOperand()->accept(*this));
- RationalNumberType secondOperandAsRationalFunction = boost::any_cast<RationalNumberType>(expression.getSecondOperand()->accept(*this));
+ RationalNumberType firstOperandAsRationalNumber = boost::any_cast<RationalNumberType>(expression.getFirstOperand()->accept(*this));
+ RationalNumberType secondOperandAsRationalNumber = boost::any_cast<RationalNumberType>(expression.getSecondOperand()->accept(*this));
switch(expression.getOperatorType()) {
case BinaryNumericalFunctionExpression::OperatorType::Plus:
- return firstOperandAsRationalFunction + secondOperandAsRationalFunction;
+ return firstOperandAsRationalNumber + secondOperandAsRationalNumber;
break;
case BinaryNumericalFunctionExpression::OperatorType::Minus:
- return firstOperandAsRationalFunction - secondOperandAsRationalFunction;
+ return firstOperandAsRationalNumber - secondOperandAsRationalNumber;
break;
case BinaryNumericalFunctionExpression::OperatorType::Times:
- return firstOperandAsRationalFunction * secondOperandAsRationalFunction;
+ return firstOperandAsRationalNumber * secondOperandAsRationalNumber;
break;
case BinaryNumericalFunctionExpression::OperatorType::Divide:
- return firstOperandAsRationalFunction / secondOperandAsRationalFunction;
+ return firstOperandAsRationalNumber / secondOperandAsRationalNumber;
+ break;
+ case BinaryNumericalFunctionExpression::OperatorType::Min:
+ return std::min(firstOperandAsRationalNumber, secondOperandAsRationalNumber);
+ break;
+ case BinaryNumericalFunctionExpression::OperatorType::Max:
+ return std::max(firstOperandAsRationalNumber, secondOperandAsRationalNumber);
+ break;
+ case BinaryNumericalFunctionExpression::OperatorType::Power:
+ STORM_LOG_THROW(storm::utility::isInteger(secondOperandAsRationalNumber), storm::exceptions::InvalidArgumentException, "Exponent of power operator must be a positive integer.");
+ uint_fast64_t exponentAsInteger = storm::utility::convertNumber<uint_fast64_t>(secondOperandAsRationalNumber);
+ return storm::utility::pow(firstOperandAsRationalNumber, exponentAsInteger);
break;
- default:
- STORM_LOG_ASSERT(false, "Illegal operator type.");
}
// Return a dummy. This point must, however, never be reached.
+ STORM_LOG_ASSERT(false, "Illegal operator type.");
return boost::any();
}
@@ -88,7 +99,7 @@ namespace storm {
template<typename RationalNumberType>
boost::any ToRationalNumberVisitor<RationalNumberType>::visit(DoubleLiteralExpression const& expression) {
#ifdef STORM_HAVE_CARL
- return RationalNumberType(carl::rationalize<storm::RationalNumber>(expression.getValue()));
+ return expression.getValue();
#else
STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Rational numbers are not supported in this build.");
#endif
diff --git a/src/utility/constants.cpp b/src/utility/constants.cpp
index 71d56cd63..2630ed285 100644
--- a/src/utility/constants.cpp
+++ b/src/utility/constants.cpp
@@ -39,6 +39,23 @@ namespace storm {
bool isConstant(ValueType const& a) {
return true;
}
+
+ template<typename ValueType>
+ bool isInteger(ValueType const& number) {
+ ValueType iPart;
+ ValueType result = std::modf(number, &iPart);
+ return result = zero<ValueType>();
+ }
+
+ template<>
+ bool isInteger(int const& number) {
+ return true;
+ }
+
+ template<>
+ bool isInteger(uint_fast64_t const& number) {
+ return true;
+ }
#ifdef STORM_HAVE_CARL
template<>
@@ -50,7 +67,6 @@ namespace storm {
bool isZero(storm::RationalNumber const& a) {
return carl::isZero(a);
}
-
template<>
bool isOne(storm::RationalFunction const& a) {
@@ -93,6 +109,12 @@ namespace storm {
// FIXME: this should be treated more properly.
return storm::RationalNumber(-1);
}
+
+ template<>
+ bool isInteger(storm::RationalNumber const& number) {
+ return carl::isInteger(number);
+ }
+
#endif
template<typename ValueType>
@@ -102,9 +124,9 @@ namespace storm {
template<typename ValueType>
ValueType simplify(ValueType value) {
- // In the general case, we don't do anything here, but merely return the value. If something else is
- // supposed to happen here, the templated function can be specialized for this particular type.
- return value;
+ // In the general case, we don't do anything here, but merely return the value. If something else is
+ // supposed to happen here, the templated function can be specialized for this particular type.
+ return value;
}
template<>
@@ -151,7 +173,12 @@ namespace storm {
double convertNumber(RationalNumber const& number){
return carl::toDouble(number);
}
-
+
+ template<>
+ uint_fast64_t convertNumber(RationalNumber const& number){
+ return carl::toInt<unsigned long>(number);
+ }
+
template<>
RationalNumber convertNumber(double const& number){
return carl::rationalize<RationalNumber>(number);
@@ -167,15 +194,26 @@ namespace storm {
return RationalFunction(carl::rationalize<RationalNumber>(number));
}
+ template<>
+ RationalNumber convertNumber(std::string const& number) {
+ return carl::rationalize<RationalNumber>(number);
+ }
+
template<>
RationalFunction convertNumber(RationalNumber const& number) {
return RationalFunction(number);
}
template<>
- storm::RationalNumber abs(storm::RationalNumber const& number) {
+ RationalNumber abs(storm::RationalNumber const& number) {
return carl::abs(number);
}
+
+ template<>
+ RationalNumber pow(RationalNumber const& value, uint_fast64_t exponent) {
+ return carl::pow(value, exponent);
+ }
+
#endif
template<typename IndexType, typename ValueType>
@@ -214,6 +252,7 @@ namespace storm {
template storm::storage::MatrixEntry<storm::storage::sparse::state_type, double>&& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, double>&& matrixEntry);
template double abs(double const& number);
+ template bool isInteger(double const& number);
template bool isOne(float const& value);
template bool isZero(float const& value);
@@ -224,6 +263,7 @@ namespace storm {
template float infinity();
template float pow(float const& value, uint_fast64_t exponent);
+ template bool isInteger(float const& number);
template float simplify(float value);
@@ -240,7 +280,8 @@ namespace storm {
template int infinity();
template int pow(int const& value, uint_fast64_t exponent);
-
+ template bool isInteger(int const& number);
+
template int simplify(int value);
template storm::storage::MatrixEntry<storm::storage::sparse::state_type, int> simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, int> matrixEntry);
@@ -278,12 +319,14 @@ namespace storm {
template storm::RationalNumber infinity();
template double convertNumber(storm::RationalNumber const& number);
+ template uint_fast64_t convertNumber(storm::RationalNumber const& number);
template storm::RationalNumber convertNumber(double const& number);
template storm::RationalNumber convertNumber(storm::RationalNumber const& number);
-
+ RationalNumber convertNumber(std::string const& number);
+
template storm::RationalNumber abs(storm::RationalNumber const& number);
-// template storm::RationalNumber pow(storm::RationalNumber const& value, uint_fast64_t exponent);
+ template storm::RationalNumber pow(storm::RationalNumber const& value, uint_fast64_t exponent);
template storm::RationalNumber simplify(storm::RationalNumber value);
template storm::storage::MatrixEntry<storm::storage::sparse::state_type, storm::RationalNumber> simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, storm::RationalNumber> matrixEntry);
diff --git a/src/utility/constants.h b/src/utility/constants.h
index 4ec4e7539..66edb9f46 100644
--- a/src/utility/constants.h
+++ b/src/utility/constants.h
@@ -56,6 +56,9 @@ namespace storm {
template<typename ValueType>
ValueType abs(ValueType const& number);
+
+ template<typename ValueType>
+ bool isInteger(ValueType const& number);
}
}
From 7b2a667a9d28b0a81fef0f11116bb9dba652823d Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Mon, 15 Aug 2016 16:53:56 +0200
Subject: [PATCH 04/20] double literal now stores rational internally
Former-commit-id: c0f089b8baa1c6bef553889fb708f8a44cae1937
---
src/parser/ExpressionParser.cpp | 32 +++++++++++++++++--
src/parser/ExpressionParser.h | 16 ++++++++--
.../expressions/DoubleLiteralExpression.cpp | 4 +++
.../expressions/DoubleLiteralExpression.h | 8 +++++
src/storage/expressions/ExpressionManager.cpp | 4 +++
src/storage/expressions/ExpressionManager.h | 9 ++++++
6 files changed, 69 insertions(+), 4 deletions(-)
diff --git a/src/parser/ExpressionParser.cpp b/src/parser/ExpressionParser.cpp
index 20982bd20..d556d799a 100644
--- a/src/parser/ExpressionParser.cpp
+++ b/src/parser/ExpressionParser.cpp
@@ -3,6 +3,34 @@
#include "src/exceptions/InvalidTypeException.h"
#include "src/exceptions/WrongFormatException.h"
+#include "src/utility/constants.h"
+
+namespace boost {
+ namespace spirit {
+ namespace traits {
+ template<>
+ bool scale(int exp, storm::RationalNumber& r, storm::RationalNumber acc) {
+ if (exp >= 0) {
+ r = acc * storm::utility::pow(storm::RationalNumber(10), static_cast<uint_fast64_t>(exp));
+ } else {
+ r = acc / storm::utility::pow(storm::RationalNumber(10), static_cast<uint_fast64_t>(-exp));
+ }
+ return true;
+ }
+
+ template<>
+ bool is_equal_to_one(storm::RationalNumber const& value) {
+ return storm::utility::isOne(value);
+ }
+
+ template<>
+ storm::RationalNumber negate(bool neg, storm::RationalNumber const& number) {
+ return neg ? storm::RationalNumber(-number) : number;
+ }
+ }
+ }
+}
+
namespace storm {
namespace parser {
ExpressionParser::ExpressionParser(storm::expressions::ExpressionManager const& manager, qi::symbols<char, uint_fast64_t> const& invalidIdentifiers_, bool enableErrorHandling, bool allowBacktracking) : ExpressionParser::base_type(expression), orOperator_(), andOperator_(), equalityOperator_(), relationalOperator_(), plusOperator_(), multiplicationOperator_(), infixPowerOperator_(), unaryOperator_(), floorCeilOperator_(), minMaxOperator_(), prefixPowerOperator_(), trueFalse_(manager), manager(manager.getSharedPointer()), createExpressions(false), acceptDoubleLiterals(true), identifiers_(nullptr), invalidIdentifiers_(invalidIdentifiers_) {
@@ -33,7 +61,7 @@ namespace storm {
identifierExpression = identifier[qi::_val = phoenix::bind(&ExpressionParser::getIdentifierExpression, phoenix::ref(*this), qi::_1, allowBacktracking, qi::_pass)];
identifierExpression.name("identifier expression");
- literalExpression = trueFalse_[qi::_val = qi::_1] | strict_double[qi::_val = phoenix::bind(&ExpressionParser::createDoubleLiteralExpression, phoenix::ref(*this), qi::_1, qi::_pass)] | qi::int_[qi::_val = phoenix::bind(&ExpressionParser::createIntegerLiteralExpression, phoenix::ref(*this), qi::_1, qi::_pass)];
+ literalExpression = trueFalse_[qi::_val = qi::_1] | rationalLiteral_[qi::_val = phoenix::bind(&ExpressionParser::createDoubleLiteralExpression, phoenix::ref(*this), qi::_1, qi::_pass)] | qi::int_[qi::_val = phoenix::bind(&ExpressionParser::createIntegerLiteralExpression, phoenix::ref(*this), qi::_1, qi::_pass)];
literalExpression.name("literal expression");
atomicExpression = floorCeilExpression | prefixPowerExpression | minMaxExpression | (qi::lit("(") >> expression >> qi::lit(")")) | literalExpression | identifierExpression;
@@ -295,7 +323,7 @@ namespace storm {
return manager->boolean(false);
}
- storm::expressions::Expression ExpressionParser::createDoubleLiteralExpression(double value, bool& pass) const {
+ storm::expressions::Expression ExpressionParser::createDoubleLiteralExpression(storm::RationalNumber const& value, bool& pass) const {
// If we are not supposed to accept double expressions, we reject it by setting pass to false.
if (!this->acceptDoubleLiterals) {
pass = false;
diff --git a/src/parser/ExpressionParser.h b/src/parser/ExpressionParser.h
index 66d851707..c728e0b84 100644
--- a/src/parser/ExpressionParser.h
+++ b/src/parser/ExpressionParser.h
@@ -8,8 +8,20 @@
#include "src/storage/expressions/Expression.h"
#include "src/storage/expressions/ExpressionManager.h"
+#include "src/adapters/CarlAdapter.h"
+
namespace storm {
namespace parser {
+ template<typename NumberType>
+ struct RationalPolicies : boost::spirit::qi::strict_real_policies<NumberType> {
+ static const bool expect_dot = true;
+
+ template <typename It, typename Attr>
+ static bool parse_nan(It&, It const&, Attr&) { return false; }
+ template <typename It, typename Attr>
+ static bool parse_inf(It&, It const&, Attr&) { return false; }
+ };
+
class ExpressionParser : public qi::grammar<Iterator, storm::expressions::Expression(), Skipper> {
public:
/*!
@@ -236,7 +248,7 @@ namespace storm {
qi::rule<Iterator, std::string(), Skipper> identifier;
// Parser that is used to recognize doubles only (as opposed to Spirit's double_ parser).
- boost::spirit::qi::real_parser<double, boost::spirit::qi::strict_real_policies<double>> strict_double;
+ boost::spirit::qi::real_parser<storm::RationalNumber, RationalPolicies<storm::RationalNumber>> rationalLiteral_;
// Helper functions to create expressions.
storm::expressions::Expression createIteExpression(storm::expressions::Expression e1, storm::expressions::Expression e2, storm::expressions::Expression e3, bool& pass) const;
@@ -248,7 +260,7 @@ namespace storm {
storm::expressions::Expression createMultExpression(storm::expressions::Expression const& e1, storm::expressions::OperatorType const& operatorType, storm::expressions::Expression const& e2, bool& pass) const;
storm::expressions::Expression createPowerExpression(storm::expressions::Expression const& e1, storm::expressions::OperatorType const& operatorType, storm::expressions::Expression const& e2, bool& pass) const;
storm::expressions::Expression createUnaryExpression(boost::optional<storm::expressions::OperatorType> const& operatorType, storm::expressions::Expression const& e1, bool& pass) const;
- storm::expressions::Expression createDoubleLiteralExpression(double value, bool& pass) const;
+ storm::expressions::Expression createDoubleLiteralExpression(storm::RationalNumber const& value, bool& pass) const;
storm::expressions::Expression createIntegerLiteralExpression(int value, bool& pass) const;
storm::expressions::Expression createMinimumMaximumExpression(storm::expressions::Expression const& e1, storm::expressions::OperatorType const& operatorType, storm::expressions::Expression const& e2, bool& pass) const;
storm::expressions::Expression createFloorCeilExpression(storm::expressions::OperatorType const& operatorType, storm::expressions::Expression const& e1, bool& pass) const;
diff --git a/src/storage/expressions/DoubleLiteralExpression.cpp b/src/storage/expressions/DoubleLiteralExpression.cpp
index 192d747ee..86a2ba889 100644
--- a/src/storage/expressions/DoubleLiteralExpression.cpp
+++ b/src/storage/expressions/DoubleLiteralExpression.cpp
@@ -14,6 +14,10 @@ namespace storm {
// Intentionally left empty.
}
+ DoubleLiteralExpression::DoubleLiteralExpression(ExpressionManager const& manager, storm::RationalNumber const& value) : BaseExpression(manager, manager.getRationalType()), value(value) {
+ // Intentionally left empty.
+ }
+
double DoubleLiteralExpression::evaluateAsDouble(Valuation const* valuation) const {
return this->getValueAsDouble();
}
diff --git a/src/storage/expressions/DoubleLiteralExpression.h b/src/storage/expressions/DoubleLiteralExpression.h
index 6a04f23e3..1b6aa28b3 100644
--- a/src/storage/expressions/DoubleLiteralExpression.h
+++ b/src/storage/expressions/DoubleLiteralExpression.h
@@ -26,6 +26,14 @@ namespace storm {
*/
DoubleLiteralExpression(ExpressionManager const& manager, std::string const& valueAsString);
+ /*!
+ * Creates an double literal expression with the rational value.
+ *
+ * @param manager The manager responsible for this expression.
+ * @param value The rational number that is the value of this literal expression.
+ */
+ DoubleLiteralExpression(ExpressionManager const& manager, storm::RationalNumber const& value);
+
// Instantiate constructors and assignments with their default implementations.
DoubleLiteralExpression(DoubleLiteralExpression const& other) = default;
DoubleLiteralExpression& operator=(DoubleLiteralExpression const& other) = delete;
diff --git a/src/storage/expressions/ExpressionManager.cpp b/src/storage/expressions/ExpressionManager.cpp
index d1add4402..a92d908f3 100644
--- a/src/storage/expressions/ExpressionManager.cpp
+++ b/src/storage/expressions/ExpressionManager.cpp
@@ -68,6 +68,10 @@ namespace storm {
return Expression(std::shared_ptr<BaseExpression>(new DoubleLiteralExpression(*this, value)));
}
+ Expression ExpressionManager::rational(storm::RationalNumber const& value) const {
+ return Expression(std::shared_ptr<BaseExpression>(new DoubleLiteralExpression(*this, value)));
+ }
+
bool ExpressionManager::operator==(ExpressionManager const& other) const {
return this == &other;
}
diff --git a/src/storage/expressions/ExpressionManager.h b/src/storage/expressions/ExpressionManager.h
index 6fee92fd6..f3ec7e76b 100644
--- a/src/storage/expressions/ExpressionManager.h
+++ b/src/storage/expressions/ExpressionManager.h
@@ -10,6 +10,7 @@
#include "src/storage/expressions/Variable.h"
#include "src/storage/expressions/Expression.h"
+#include "src/adapters/CarlAdapter.h"
#include "src/utility/OsDetection.h"
namespace storm {
@@ -104,6 +105,14 @@ namespace storm {
* @return The resulting expression.
*/
Expression rational(double value) const;
+
+ /*!
+ * Creates an expression that characterizes the given rational literal.
+ *
+ * @param value The value of the rational literal.
+ * @return The resulting expression.
+ */
+ Expression rational(storm::RationalNumber const& value) const;
/*!
* Compares the two expression managers for equality, which holds iff they are the very same object.
From 58857d62ed395040aa69cbc6b3d1e6e789fa0744 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Mon, 15 Aug 2016 16:55:45 +0200
Subject: [PATCH 05/20] renamed double literal to rational literal
Former-commit-id: 7bafe79eed1fd06aa0254a20699454265ed0eeb2
---
src/adapters/AddExpressionAdapter.cpp | 2 +-
src/adapters/AddExpressionAdapter.h | 2 +-
src/adapters/MathsatExpressionAdapter.h | 2 +-
src/adapters/Z3ExpressionAdapter.cpp | 2 +-
src/adapters/Z3ExpressionAdapter.h | 2 +-
src/parser/ExpressionParser.cpp | 4 ++--
src/parser/ExpressionParser.h | 2 +-
.../BinaryNumericalFunctionExpression.cpp | 4 ++--
.../expressions/DoubleLiteralExpression.cpp | 24 +++++++++----------
.../expressions/DoubleLiteralExpression.h | 24 +++++++++----------
src/storage/expressions/ExpressionManager.cpp | 4 ++--
src/storage/expressions/ExpressionVisitor.h | 4 ++--
src/storage/expressions/Expressions.h | 2 +-
.../expressions/LinearCoefficientVisitor.cpp | 2 +-
.../expressions/LinearCoefficientVisitor.h | 2 +-
.../expressions/LinearityCheckVisitor.cpp | 2 +-
.../expressions/LinearityCheckVisitor.h | 2 +-
.../expressions/SubstitutionVisitor.cpp | 2 +-
src/storage/expressions/SubstitutionVisitor.h | 2 +-
.../expressions/ToExprtkStringVisitor.cpp | 2 +-
.../expressions/ToExprtkStringVisitor.h | 2 +-
.../expressions/ToRationalFunctionVisitor.cpp | 2 +-
.../expressions/ToRationalFunctionVisitor.h | 2 +-
.../expressions/ToRationalNumberVisitor.cpp | 2 +-
.../expressions/ToRationalNumberVisitor.h | 2 +-
.../UnaryNumericalFunctionExpression.cpp | 4 ++--
26 files changed, 53 insertions(+), 53 deletions(-)
diff --git a/src/adapters/AddExpressionAdapter.cpp b/src/adapters/AddExpressionAdapter.cpp
index 7a22c8f8f..2f0dc7190 100644
--- a/src/adapters/AddExpressionAdapter.cpp
+++ b/src/adapters/AddExpressionAdapter.cpp
@@ -194,7 +194,7 @@ namespace storm {
}
template<storm::dd::DdType Type, typename ValueType>
- boost::any AddExpressionAdapter<Type, ValueType>::visit(storm::expressions::DoubleLiteralExpression const& expression) {
+ boost::any AddExpressionAdapter<Type, ValueType>::visit(storm::expressions::RationalLiteralExpression const& expression) {
return ddManager->getConstant(static_cast<ValueType>(expression.getValueAsDouble()));
}
diff --git a/src/adapters/AddExpressionAdapter.h b/src/adapters/AddExpressionAdapter.h
index 89d825d96..dfb13a315 100644
--- a/src/adapters/AddExpressionAdapter.h
+++ b/src/adapters/AddExpressionAdapter.h
@@ -31,7 +31,7 @@ namespace storm {
virtual boost::any visit(storm::expressions::UnaryNumericalFunctionExpression const& expression) override;
virtual boost::any visit(storm::expressions::BooleanLiteralExpression const& expression) override;
virtual boost::any visit(storm::expressions::IntegerLiteralExpression const& expression) override;
- virtual boost::any visit(storm::expressions::DoubleLiteralExpression const& expression) override;
+ virtual boost::any visit(storm::expressions::RationalLiteralExpression const& expression) override;
private:
// The manager responsible for the DDs built by this adapter.
diff --git a/src/adapters/MathsatExpressionAdapter.h b/src/adapters/MathsatExpressionAdapter.h
index db5bf9b69..77b39cc68 100644
--- a/src/adapters/MathsatExpressionAdapter.h
+++ b/src/adapters/MathsatExpressionAdapter.h
@@ -171,7 +171,7 @@ namespace storm {
return expression.getValue() ? msat_make_true(env) : msat_make_false(env);
}
- virtual boost::any visit(expressions::DoubleLiteralExpression const& expression) override {
+ virtual boost::any visit(expressions::RationalLiteralExpression const& expression) override {
return msat_make_number(env, std::to_string(expression.getValueAsDouble()).c_str());
}
diff --git a/src/adapters/Z3ExpressionAdapter.cpp b/src/adapters/Z3ExpressionAdapter.cpp
index 60b4e8e1c..6f4efc178 100644
--- a/src/adapters/Z3ExpressionAdapter.cpp
+++ b/src/adapters/Z3ExpressionAdapter.cpp
@@ -208,7 +208,7 @@ namespace storm {
return context.bool_val(expression.getValue());
}
- boost::any Z3ExpressionAdapter::visit(storm::expressions::DoubleLiteralExpression const& expression) {
+ boost::any Z3ExpressionAdapter::visit(storm::expressions::RationalLiteralExpression const& expression) {
std::stringstream fractionStream;
fractionStream << expression.getValue();
return context.real_val(fractionStream.str().c_str());
diff --git a/src/adapters/Z3ExpressionAdapter.h b/src/adapters/Z3ExpressionAdapter.h
index 4fc60c8a5..2735f5713 100644
--- a/src/adapters/Z3ExpressionAdapter.h
+++ b/src/adapters/Z3ExpressionAdapter.h
@@ -63,7 +63,7 @@ namespace storm {
virtual boost::any visit(storm::expressions::BooleanLiteralExpression const& expression) override;
- virtual boost::any visit(storm::expressions::DoubleLiteralExpression const& expression) override;
+ virtual boost::any visit(storm::expressions::RationalLiteralExpression const& expression) override;
virtual boost::any visit(storm::expressions::IntegerLiteralExpression const& expression) override;
diff --git a/src/parser/ExpressionParser.cpp b/src/parser/ExpressionParser.cpp
index d556d799a..3054f2fe0 100644
--- a/src/parser/ExpressionParser.cpp
+++ b/src/parser/ExpressionParser.cpp
@@ -61,7 +61,7 @@ namespace storm {
identifierExpression = identifier[qi::_val = phoenix::bind(&ExpressionParser::getIdentifierExpression, phoenix::ref(*this), qi::_1, allowBacktracking, qi::_pass)];
identifierExpression.name("identifier expression");
- literalExpression = trueFalse_[qi::_val = qi::_1] | rationalLiteral_[qi::_val = phoenix::bind(&ExpressionParser::createDoubleLiteralExpression, phoenix::ref(*this), qi::_1, qi::_pass)] | qi::int_[qi::_val = phoenix::bind(&ExpressionParser::createIntegerLiteralExpression, phoenix::ref(*this), qi::_1, qi::_pass)];
+ literalExpression = trueFalse_[qi::_val = qi::_1] | rationalLiteral_[qi::_val = phoenix::bind(&ExpressionParser::createRationalLiteralExpression, phoenix::ref(*this), qi::_1, qi::_pass)] | qi::int_[qi::_val = phoenix::bind(&ExpressionParser::createIntegerLiteralExpression, phoenix::ref(*this), qi::_1, qi::_pass)];
literalExpression.name("literal expression");
atomicExpression = floorCeilExpression | prefixPowerExpression | minMaxExpression | (qi::lit("(") >> expression >> qi::lit(")")) | literalExpression | identifierExpression;
@@ -323,7 +323,7 @@ namespace storm {
return manager->boolean(false);
}
- storm::expressions::Expression ExpressionParser::createDoubleLiteralExpression(storm::RationalNumber const& value, bool& pass) const {
+ storm::expressions::Expression ExpressionParser::createRationalLiteralExpression(storm::RationalNumber const& value, bool& pass) const {
// If we are not supposed to accept double expressions, we reject it by setting pass to false.
if (!this->acceptDoubleLiterals) {
pass = false;
diff --git a/src/parser/ExpressionParser.h b/src/parser/ExpressionParser.h
index c728e0b84..077be8db2 100644
--- a/src/parser/ExpressionParser.h
+++ b/src/parser/ExpressionParser.h
@@ -260,7 +260,7 @@ namespace storm {
storm::expressions::Expression createMultExpression(storm::expressions::Expression const& e1, storm::expressions::OperatorType const& operatorType, storm::expressions::Expression const& e2, bool& pass) const;
storm::expressions::Expression createPowerExpression(storm::expressions::Expression const& e1, storm::expressions::OperatorType const& operatorType, storm::expressions::Expression const& e2, bool& pass) const;
storm::expressions::Expression createUnaryExpression(boost::optional<storm::expressions::OperatorType> const& operatorType, storm::expressions::Expression const& e1, bool& pass) const;
- storm::expressions::Expression createDoubleLiteralExpression(storm::RationalNumber const& value, bool& pass) const;
+ storm::expressions::Expression createRationalLiteralExpression(storm::RationalNumber const& value, bool& pass) const;
storm::expressions::Expression createIntegerLiteralExpression(int value, bool& pass) const;
storm::expressions::Expression createMinimumMaximumExpression(storm::expressions::Expression const& e1, storm::expressions::OperatorType const& operatorType, storm::expressions::Expression const& e2, bool& pass) const;
storm::expressions::Expression createFloorCeilExpression(storm::expressions::OperatorType const& operatorType, storm::expressions::Expression const& e1, bool& pass) const;
diff --git a/src/storage/expressions/BinaryNumericalFunctionExpression.cpp b/src/storage/expressions/BinaryNumericalFunctionExpression.cpp
index 95a326de1..7c4367952 100644
--- a/src/storage/expressions/BinaryNumericalFunctionExpression.cpp
+++ b/src/storage/expressions/BinaryNumericalFunctionExpression.cpp
@@ -3,7 +3,7 @@
#include "src/storage/expressions/BinaryNumericalFunctionExpression.h"
#include "src/storage/expressions/IntegerLiteralExpression.h"
-#include "src/storage/expressions/DoubleLiteralExpression.h"
+#include "src/storage/expressions/RationalLiteralExpression.h"
#include "src/storage/expressions/ExpressionVisitor.h"
#include "src/utility/macros.h"
#include "src/exceptions/InvalidTypeException.h"
@@ -102,7 +102,7 @@ namespace storm {
case OperatorType::Power: newValue = static_cast<int_fast64_t>(std::pow(firstOperandEvaluation, secondOperandEvaluation)); break;
case OperatorType::Divide: STORM_LOG_THROW(false, storm::exceptions::InvalidStateException, "Unable to simplify division."); break;
}
- return std::shared_ptr<BaseExpression>(new DoubleLiteralExpression(this->getManager(), newValue));
+ return std::shared_ptr<BaseExpression>(new RationalLiteralExpression(this->getManager(), newValue));
}
}
diff --git a/src/storage/expressions/DoubleLiteralExpression.cpp b/src/storage/expressions/DoubleLiteralExpression.cpp
index 86a2ba889..3fa226a8a 100644
--- a/src/storage/expressions/DoubleLiteralExpression.cpp
+++ b/src/storage/expressions/DoubleLiteralExpression.cpp
@@ -1,4 +1,4 @@
-#include "src/storage/expressions/DoubleLiteralExpression.h"
+#include "src/storage/expressions/RationalLiteralExpression.h"
#include "src/storage/expressions/ExpressionManager.h"
#include "src/storage/expressions/ExpressionVisitor.h"
@@ -6,47 +6,47 @@
namespace storm {
namespace expressions {
- DoubleLiteralExpression::DoubleLiteralExpression(ExpressionManager const& manager, double value) : BaseExpression(manager, manager.getRationalType()), value(storm::utility::convertNumber<storm::RationalNumber>(value)) {
+ RationalLiteralExpression::RationalLiteralExpression(ExpressionManager const& manager, double value) : BaseExpression(manager, manager.getRationalType()), value(storm::utility::convertNumber<storm::RationalNumber>(value)) {
// Intentionally left empty.
}
- DoubleLiteralExpression::DoubleLiteralExpression(ExpressionManager const& manager, std::string const& valueAsString) : BaseExpression(manager, manager.getRationalType()), value(storm::utility::convertNumber<storm::RationalNumber>(valueAsString)) {
+ RationalLiteralExpression::RationalLiteralExpression(ExpressionManager const& manager, std::string const& valueAsString) : BaseExpression(manager, manager.getRationalType()), value(storm::utility::convertNumber<storm::RationalNumber>(valueAsString)) {
// Intentionally left empty.
}
- DoubleLiteralExpression::DoubleLiteralExpression(ExpressionManager const& manager, storm::RationalNumber const& value) : BaseExpression(manager, manager.getRationalType()), value(value) {
+ RationalLiteralExpression::RationalLiteralExpression(ExpressionManager const& manager, storm::RationalNumber const& value) : BaseExpression(manager, manager.getRationalType()), value(value) {
// Intentionally left empty.
}
- double DoubleLiteralExpression::evaluateAsDouble(Valuation const* valuation) const {
+ double RationalLiteralExpression::evaluateAsDouble(Valuation const* valuation) const {
return this->getValueAsDouble();
}
- bool DoubleLiteralExpression::isLiteral() const {
+ bool RationalLiteralExpression::isLiteral() const {
return true;
}
- void DoubleLiteralExpression::gatherVariables(std::set<storm::expressions::Variable>& variables) const {
+ void RationalLiteralExpression::gatherVariables(std::set<storm::expressions::Variable>& variables) const {
return;
}
- std::shared_ptr<BaseExpression const> DoubleLiteralExpression::simplify() const {
+ std::shared_ptr<BaseExpression const> RationalLiteralExpression::simplify() const {
return this->shared_from_this();
}
- boost::any DoubleLiteralExpression::accept(ExpressionVisitor& visitor) const {
+ boost::any RationalLiteralExpression::accept(ExpressionVisitor& visitor) const {
return visitor.visit(*this);
}
- double DoubleLiteralExpression::getValueAsDouble() const {
+ double RationalLiteralExpression::getValueAsDouble() const {
return storm::utility::convertNumber<double>(this->value);
}
- storm::RationalNumber DoubleLiteralExpression::getValue() const {
+ storm::RationalNumber RationalLiteralExpression::getValue() const {
return this->value;
}
- void DoubleLiteralExpression::printToStream(std::ostream& stream) const {
+ void RationalLiteralExpression::printToStream(std::ostream& stream) const {
stream << this->getValue();
}
}
diff --git a/src/storage/expressions/DoubleLiteralExpression.h b/src/storage/expressions/DoubleLiteralExpression.h
index 1b6aa28b3..4eff900b2 100644
--- a/src/storage/expressions/DoubleLiteralExpression.h
+++ b/src/storage/expressions/DoubleLiteralExpression.h
@@ -1,5 +1,5 @@
-#ifndef STORM_STORAGE_EXPRESSIONS_DOUBLELITERALEXPRESSION_H_
-#define STORM_STORAGE_EXPRESSIONS_DOUBLELITERALEXPRESSION_H_
+#ifndef STORM_STORAGE_EXPRESSIONS_RationalLiteralExpression_H_
+#define STORM_STORAGE_EXPRESSIONS_RationalLiteralExpression_H_
#include "src/storage/expressions/BaseExpression.h"
#include "src/utility/OsDetection.h"
@@ -8,7 +8,7 @@
namespace storm {
namespace expressions {
- class DoubleLiteralExpression : public BaseExpression {
+ class RationalLiteralExpression : public BaseExpression {
public:
/*!
* Creates an double literal expression with the given value.
@@ -16,7 +16,7 @@ namespace storm {
* @param manager The manager responsible for this expression.
* @param value The value of the double literal.
*/
- DoubleLiteralExpression(ExpressionManager const& manager, double value);
+ RationalLiteralExpression(ExpressionManager const& manager, double value);
/*!
* Creates an double literal expression with the value given as a string.
@@ -24,7 +24,7 @@ namespace storm {
* @param manager The manager responsible for this expression.
* @param value The string representation of the value of the literal.
*/
- DoubleLiteralExpression(ExpressionManager const& manager, std::string const& valueAsString);
+ RationalLiteralExpression(ExpressionManager const& manager, std::string const& valueAsString);
/*!
* Creates an double literal expression with the rational value.
@@ -32,16 +32,16 @@ namespace storm {
* @param manager The manager responsible for this expression.
* @param value The rational number that is the value of this literal expression.
*/
- DoubleLiteralExpression(ExpressionManager const& manager, storm::RationalNumber const& value);
+ RationalLiteralExpression(ExpressionManager const& manager, storm::RationalNumber const& value);
// Instantiate constructors and assignments with their default implementations.
- DoubleLiteralExpression(DoubleLiteralExpression const& other) = default;
- DoubleLiteralExpression& operator=(DoubleLiteralExpression const& other) = delete;
+ RationalLiteralExpression(RationalLiteralExpression const& other) = default;
+ RationalLiteralExpression& operator=(RationalLiteralExpression const& other) = delete;
#ifndef WINDOWS
- DoubleLiteralExpression(DoubleLiteralExpression&&) = default;
- DoubleLiteralExpression& operator=(DoubleLiteralExpression&&) = delete;
+ RationalLiteralExpression(RationalLiteralExpression&&) = default;
+ RationalLiteralExpression& operator=(RationalLiteralExpression&&) = delete;
#endif
- virtual ~DoubleLiteralExpression() = default;
+ virtual ~RationalLiteralExpression() = default;
// Override base class methods.
virtual double evaluateAsDouble(Valuation const* valuation = nullptr) const override;
@@ -75,4 +75,4 @@ namespace storm {
}
}
-#endif /* STORM_STORAGE_EXPRESSIONS_DOUBLELITERALEXPRESSION_H_ */
\ No newline at end of file
+#endif /* STORM_STORAGE_EXPRESSIONS_RationalLiteralExpression_H_ */
\ No newline at end of file
diff --git a/src/storage/expressions/ExpressionManager.cpp b/src/storage/expressions/ExpressionManager.cpp
index a92d908f3..ed51f76ee 100644
--- a/src/storage/expressions/ExpressionManager.cpp
+++ b/src/storage/expressions/ExpressionManager.cpp
@@ -65,11 +65,11 @@ namespace storm {
}
Expression ExpressionManager::rational(double value) const {
- return Expression(std::shared_ptr<BaseExpression>(new DoubleLiteralExpression(*this, value)));
+ return Expression(std::shared_ptr<BaseExpression>(new RationalLiteralExpression(*this, value)));
}
Expression ExpressionManager::rational(storm::RationalNumber const& value) const {
- return Expression(std::shared_ptr<BaseExpression>(new DoubleLiteralExpression(*this, value)));
+ return Expression(std::shared_ptr<BaseExpression>(new RationalLiteralExpression(*this, value)));
}
bool ExpressionManager::operator==(ExpressionManager const& other) const {
diff --git a/src/storage/expressions/ExpressionVisitor.h b/src/storage/expressions/ExpressionVisitor.h
index 5fdb486c2..1abafc2a6 100644
--- a/src/storage/expressions/ExpressionVisitor.h
+++ b/src/storage/expressions/ExpressionVisitor.h
@@ -15,7 +15,7 @@ namespace storm {
class UnaryNumericalFunctionExpression;
class BooleanLiteralExpression;
class IntegerLiteralExpression;
- class DoubleLiteralExpression;
+ class RationalLiteralExpression;
class ExpressionVisitor {
public:
@@ -28,7 +28,7 @@ namespace storm {
virtual boost::any visit(UnaryNumericalFunctionExpression const& expression) = 0;
virtual boost::any visit(BooleanLiteralExpression const& expression) = 0;
virtual boost::any visit(IntegerLiteralExpression const& expression) = 0;
- virtual boost::any visit(DoubleLiteralExpression const& expression) = 0;
+ virtual boost::any visit(RationalLiteralExpression const& expression) = 0;
};
}
}
diff --git a/src/storage/expressions/Expressions.h b/src/storage/expressions/Expressions.h
index d670c29e3..655cc4aab 100644
--- a/src/storage/expressions/Expressions.h
+++ b/src/storage/expressions/Expressions.h
@@ -4,7 +4,7 @@
#include "src/storage/expressions/BinaryRelationExpression.h"
#include "src/storage/expressions/BooleanLiteralExpression.h"
#include "src/storage/expressions/IntegerLiteralExpression.h"
-#include "src/storage/expressions/DoubleLiteralExpression.h"
+#include "src/storage/expressions/RationalLiteralExpression.h"
#include "src/storage/expressions/UnaryBooleanFunctionExpression.h"
#include "src/storage/expressions/UnaryNumericalFunctionExpression.h"
#include "src/storage/expressions/VariableExpression.h"
diff --git a/src/storage/expressions/LinearCoefficientVisitor.cpp b/src/storage/expressions/LinearCoefficientVisitor.cpp
index 3d881c25e..dc9a909f9 100644
--- a/src/storage/expressions/LinearCoefficientVisitor.cpp
+++ b/src/storage/expressions/LinearCoefficientVisitor.cpp
@@ -151,7 +151,7 @@ namespace storm {
return VariableCoefficients(static_cast<double>(expression.getValue()));
}
- boost::any LinearCoefficientVisitor::visit(DoubleLiteralExpression const& expression) {
+ boost::any LinearCoefficientVisitor::visit(RationalLiteralExpression const& expression) {
return VariableCoefficients(expression.getValueAsDouble());
}
}
diff --git a/src/storage/expressions/LinearCoefficientVisitor.h b/src/storage/expressions/LinearCoefficientVisitor.h
index b48c53d09..dea1bfc2e 100644
--- a/src/storage/expressions/LinearCoefficientVisitor.h
+++ b/src/storage/expressions/LinearCoefficientVisitor.h
@@ -75,7 +75,7 @@ namespace storm {
virtual boost::any visit(UnaryNumericalFunctionExpression const& expression) override;
virtual boost::any visit(BooleanLiteralExpression const& expression) override;
virtual boost::any visit(IntegerLiteralExpression const& expression) override;
- virtual boost::any visit(DoubleLiteralExpression const& expression) override;
+ virtual boost::any visit(RationalLiteralExpression const& expression) override;
};
}
}
diff --git a/src/storage/expressions/LinearityCheckVisitor.cpp b/src/storage/expressions/LinearityCheckVisitor.cpp
index 35e1e5c76..7a33a501a 100644
--- a/src/storage/expressions/LinearityCheckVisitor.cpp
+++ b/src/storage/expressions/LinearityCheckVisitor.cpp
@@ -85,7 +85,7 @@ namespace storm {
return LinearityStatus::LinearWithoutVariables;
}
- boost::any LinearityCheckVisitor::visit(DoubleLiteralExpression const& expression) {
+ boost::any LinearityCheckVisitor::visit(RationalLiteralExpression const& expression) {
return LinearityStatus::LinearWithoutVariables;
}
}
diff --git a/src/storage/expressions/LinearityCheckVisitor.h b/src/storage/expressions/LinearityCheckVisitor.h
index 2df8f8084..6bb35b7e8 100644
--- a/src/storage/expressions/LinearityCheckVisitor.h
+++ b/src/storage/expressions/LinearityCheckVisitor.h
@@ -29,7 +29,7 @@ namespace storm {
virtual boost::any visit(UnaryNumericalFunctionExpression const& expression) override;
virtual boost::any visit(BooleanLiteralExpression const& expression) override;
virtual boost::any visit(IntegerLiteralExpression const& expression) override;
- virtual boost::any visit(DoubleLiteralExpression const& expression) override;
+ virtual boost::any visit(RationalLiteralExpression const& expression) override;
private:
enum class LinearityStatus { NonLinear, LinearContainsVariables, LinearWithoutVariables };
diff --git a/src/storage/expressions/SubstitutionVisitor.cpp b/src/storage/expressions/SubstitutionVisitor.cpp
index c736de156..1490e6f59 100644
--- a/src/storage/expressions/SubstitutionVisitor.cpp
+++ b/src/storage/expressions/SubstitutionVisitor.cpp
@@ -116,7 +116,7 @@ namespace storm {
}
template<typename MapType>
- boost::any SubstitutionVisitor<MapType>::visit(DoubleLiteralExpression const& expression) {
+ boost::any SubstitutionVisitor<MapType>::visit(RationalLiteralExpression const& expression) {
return expression.getSharedPointer();
}
diff --git a/src/storage/expressions/SubstitutionVisitor.h b/src/storage/expressions/SubstitutionVisitor.h
index 343521335..5f1a93cb2 100644
--- a/src/storage/expressions/SubstitutionVisitor.h
+++ b/src/storage/expressions/SubstitutionVisitor.h
@@ -37,7 +37,7 @@ namespace storm {
virtual boost::any visit(UnaryNumericalFunctionExpression const& expression) override;
virtual boost::any visit(BooleanLiteralExpression const& expression) override;
virtual boost::any visit(IntegerLiteralExpression const& expression) override;
- virtual boost::any visit(DoubleLiteralExpression const& expression) override;
+ virtual boost::any visit(RationalLiteralExpression const& expression) override;
private:
// A mapping of variables to expressions with which they shall be replaced.
diff --git a/src/storage/expressions/ToExprtkStringVisitor.cpp b/src/storage/expressions/ToExprtkStringVisitor.cpp
index 51d9c1f34..1492aeae5 100644
--- a/src/storage/expressions/ToExprtkStringVisitor.cpp
+++ b/src/storage/expressions/ToExprtkStringVisitor.cpp
@@ -212,7 +212,7 @@ namespace storm {
return boost::any();
}
- boost::any ToExprtkStringVisitor::visit(DoubleLiteralExpression const& expression) {
+ boost::any ToExprtkStringVisitor::visit(RationalLiteralExpression const& expression) {
stream << expression.getValue();
return boost::any();
}
diff --git a/src/storage/expressions/ToExprtkStringVisitor.h b/src/storage/expressions/ToExprtkStringVisitor.h
index 6c285ff28..d68da589d 100644
--- a/src/storage/expressions/ToExprtkStringVisitor.h
+++ b/src/storage/expressions/ToExprtkStringVisitor.h
@@ -25,7 +25,7 @@ namespace storm {
virtual boost::any visit(UnaryNumericalFunctionExpression const& expression) override;
virtual boost::any visit(BooleanLiteralExpression const& expression) override;
virtual boost::any visit(IntegerLiteralExpression const& expression) override;
- virtual boost::any visit(DoubleLiteralExpression const& expression) override;
+ virtual boost::any visit(RationalLiteralExpression const& expression) override;
private:
std::stringstream stream;
diff --git a/src/storage/expressions/ToRationalFunctionVisitor.cpp b/src/storage/expressions/ToRationalFunctionVisitor.cpp
index 533fa1f1f..60fecc08c 100644
--- a/src/storage/expressions/ToRationalFunctionVisitor.cpp
+++ b/src/storage/expressions/ToRationalFunctionVisitor.cpp
@@ -93,7 +93,7 @@ namespace storm {
}
template<typename RationalFunctionType>
- boost::any ToRationalFunctionVisitor<RationalFunctionType>::visit(DoubleLiteralExpression const& expression) {
+ boost::any ToRationalFunctionVisitor<RationalFunctionType>::visit(RationalLiteralExpression const& expression) {
return storm::utility::convertNumber<storm::RationalFunction>(expression.getValue());
}
diff --git a/src/storage/expressions/ToRationalFunctionVisitor.h b/src/storage/expressions/ToRationalFunctionVisitor.h
index 12603f44e..1cda5028f 100644
--- a/src/storage/expressions/ToRationalFunctionVisitor.h
+++ b/src/storage/expressions/ToRationalFunctionVisitor.h
@@ -27,7 +27,7 @@ namespace storm {
virtual boost::any visit(UnaryNumericalFunctionExpression const& expression) override;
virtual boost::any visit(BooleanLiteralExpression const& expression) override;
virtual boost::any visit(IntegerLiteralExpression const& expression) override;
- virtual boost::any visit(DoubleLiteralExpression const& expression) override;
+ virtual boost::any visit(RationalLiteralExpression const& expression) override;
private:
template<typename TP = typename RationalFunctionType::PolyType, carl::EnableIf<carl::needs_cache<TP>> = carl::dummy>
diff --git a/src/storage/expressions/ToRationalNumberVisitor.cpp b/src/storage/expressions/ToRationalNumberVisitor.cpp
index 44194cb4b..1b7319927 100644
--- a/src/storage/expressions/ToRationalNumberVisitor.cpp
+++ b/src/storage/expressions/ToRationalNumberVisitor.cpp
@@ -97,7 +97,7 @@ namespace storm {
}
template<typename RationalNumberType>
- boost::any ToRationalNumberVisitor<RationalNumberType>::visit(DoubleLiteralExpression const& expression) {
+ boost::any ToRationalNumberVisitor<RationalNumberType>::visit(RationalLiteralExpression const& expression) {
#ifdef STORM_HAVE_CARL
return expression.getValue();
#else
diff --git a/src/storage/expressions/ToRationalNumberVisitor.h b/src/storage/expressions/ToRationalNumberVisitor.h
index 2254931f6..3d53b8a87 100644
--- a/src/storage/expressions/ToRationalNumberVisitor.h
+++ b/src/storage/expressions/ToRationalNumberVisitor.h
@@ -25,7 +25,7 @@ namespace storm {
virtual boost::any visit(UnaryNumericalFunctionExpression const& expression) override;
virtual boost::any visit(BooleanLiteralExpression const& expression) override;
virtual boost::any visit(IntegerLiteralExpression const& expression) override;
- virtual boost::any visit(DoubleLiteralExpression const& expression) override;
+ virtual boost::any visit(RationalLiteralExpression const& expression) override;
};
}
}
diff --git a/src/storage/expressions/UnaryNumericalFunctionExpression.cpp b/src/storage/expressions/UnaryNumericalFunctionExpression.cpp
index fa7cad7e3..f5178fb6f 100644
--- a/src/storage/expressions/UnaryNumericalFunctionExpression.cpp
+++ b/src/storage/expressions/UnaryNumericalFunctionExpression.cpp
@@ -4,7 +4,7 @@
#include "src/storage/expressions/UnaryNumericalFunctionExpression.h"
#include "src/storage/expressions/IntegerLiteralExpression.h"
-#include "src/storage/expressions/DoubleLiteralExpression.h"
+#include "src/storage/expressions/RationalLiteralExpression.h"
#include "ExpressionVisitor.h"
#include "src/utility/macros.h"
#include "src/exceptions/InvalidTypeException.h"
@@ -87,7 +87,7 @@ namespace storm {
case OperatorType::Floor: value = std::floor(boost::get<double>(operandEvaluation)); break;
case OperatorType::Ceil: value = std::ceil(boost::get<double>(operandEvaluation)); break;
}
- return std::shared_ptr<BaseExpression>(new DoubleLiteralExpression(this->getManager(), value));
+ return std::shared_ptr<BaseExpression>(new RationalLiteralExpression(this->getManager(), value));
}
}
From 984abfd22bfc0df35d90d3c933f282b089f0fd20 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Mon, 15 Aug 2016 16:56:26 +0200
Subject: [PATCH 06/20] proper renaming of files
Former-commit-id: 5594ddec3849939f24194f7d3d6c8648b3e70ee8
---
...{DoubleLiteralExpression.cpp => RationalLiteralExpression.cpp} | 0
.../{DoubleLiteralExpression.h => RationalLiteralExpression.h} | 0
2 files changed, 0 insertions(+), 0 deletions(-)
rename src/storage/expressions/{DoubleLiteralExpression.cpp => RationalLiteralExpression.cpp} (100%)
rename src/storage/expressions/{DoubleLiteralExpression.h => RationalLiteralExpression.h} (100%)
diff --git a/src/storage/expressions/DoubleLiteralExpression.cpp b/src/storage/expressions/RationalLiteralExpression.cpp
similarity index 100%
rename from src/storage/expressions/DoubleLiteralExpression.cpp
rename to src/storage/expressions/RationalLiteralExpression.cpp
diff --git a/src/storage/expressions/DoubleLiteralExpression.h b/src/storage/expressions/RationalLiteralExpression.h
similarity index 100%
rename from src/storage/expressions/DoubleLiteralExpression.h
rename to src/storage/expressions/RationalLiteralExpression.h
From f342ce3287f8b2aacb6fd9149fe24a548b1a2ca3 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Mon, 15 Aug 2016 20:29:50 +0200
Subject: [PATCH 07/20] translation from expressions involving the power
operator to rational functions/rational numbers is now possible
Former-commit-id: e0ce43ab35f88de46426b967c91b584e5adbe955
---
src/storage/expressions/ToRationalFunctionVisitor.cpp | 6 ++++++
src/utility/constants.cpp | 11 ++++++++++-
2 files changed, 16 insertions(+), 1 deletion(-)
diff --git a/src/storage/expressions/ToRationalFunctionVisitor.cpp b/src/storage/expressions/ToRationalFunctionVisitor.cpp
index 60fecc08c..a219066e4 100644
--- a/src/storage/expressions/ToRationalFunctionVisitor.cpp
+++ b/src/storage/expressions/ToRationalFunctionVisitor.cpp
@@ -34,6 +34,7 @@ namespace storm {
boost::any ToRationalFunctionVisitor<RationalFunctionType>::visit(BinaryNumericalFunctionExpression const& expression) {
RationalFunctionType firstOperandAsRationalFunction = boost::any_cast<RationalFunctionType>(expression.getFirstOperand()->accept(*this));
RationalFunctionType secondOperandAsRationalFunction = boost::any_cast<RationalFunctionType>(expression.getSecondOperand()->accept(*this));
+ uint_fast64_t exponentAsInteger = 0;
switch(expression.getOperatorType()) {
case BinaryNumericalFunctionExpression::OperatorType::Plus:
return firstOperandAsRationalFunction + secondOperandAsRationalFunction;
@@ -47,6 +48,11 @@ namespace storm {
case BinaryNumericalFunctionExpression::OperatorType::Divide:
return firstOperandAsRationalFunction / secondOperandAsRationalFunction;
break;
+ case BinaryNumericalFunctionExpression::OperatorType::Power:
+ STORM_LOG_THROW(storm::utility::isInteger(secondOperandAsRationalFunction), storm::exceptions::InvalidArgumentException, "Exponent of power operator must be a positive integer.");
+ exponentAsInteger = storm::utility::convertNumber<uint_fast64_t>(secondOperandAsRationalFunction);
+ return storm::utility::pow(firstOperandAsRationalFunction, exponentAsInteger);
+ break;
default:
STORM_LOG_ASSERT(false, "Illegal operator type.");
}
diff --git a/src/utility/constants.cpp b/src/utility/constants.cpp
index 2630ed285..6d954722a 100644
--- a/src/utility/constants.cpp
+++ b/src/utility/constants.cpp
@@ -115,6 +115,10 @@ namespace storm {
return carl::isInteger(number);
}
+ template<>
+ bool isInteger(storm::RationalFunction const& func) {
+ return storm::utility::isConstant(func) && storm::utility::isOne(func.denominator());
+ }
#endif
template<typename ValueType>
@@ -203,7 +207,12 @@ namespace storm {
RationalFunction convertNumber(RationalNumber const& number) {
return RationalFunction(number);
}
-
+
+ template<>
+ uint_fast64_t convertNumber(RationalFunction const& func) {
+ return carl::toInt<unsigned long>(func.nominatorAsNumber());
+ }
+
template<>
RationalNumber abs(storm::RationalNumber const& number) {
return carl::abs(number);
From 49b663aa87da00c0277e3ba3be664d121b8803ba Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Mon, 15 Aug 2016 22:03:29 +0200
Subject: [PATCH 08/20] started working on python script that automatically
packages the binary for mac os
Former-commit-id: 11a73f85e7493bc3ab940241599cdab6d505ab91
---
util/osx-package/packager.py | 47 ++++++++++++++++++++++++++++++++++++
1 file changed, 47 insertions(+)
create mode 100644 util/osx-package/packager.py
diff --git a/util/osx-package/packager.py b/util/osx-package/packager.py
new file mode 100644
index 000000000..39d06a667
--- /dev/null
+++ b/util/osx-package/packager.py
@@ -0,0 +1,47 @@
+import argparse
+import subprocess
+import os
+
+def get_dependencies(file):
+ # Call otool -L file to obtain the dependencies.
+ proc = subprocess.Popen(["otool", "-L", args.binary], stdout=subprocess.PIPE)
+ result = {}
+ for line_bytes in proc.stdout:
+ line = line_bytes.decode("utf-8").strip()
+ lib = line.split()[0]
+ if (lib.startswith("@")):
+ lib = lib.split("/", 1)[1]
+ (base, file) = os.path.split(lib)
+ print(base + " // " + file)
+
+ return result
+
+def parse_arguments():
+ parser = argparse.ArgumentParser(description='Package the storm binary on Mac OS.')
+ parser.add_argument('binary', help='the binary to package')
+ args = parser.parse_args()
+ return args
+
+dep_exeptions = set()
+dep_exeptions.add("libSystem.B.dylib")
+dep_exeptions.add("libc++.1.dylib")
+
+def rec_gather_all_dependencies(file, deps = set()):
+ current_deps = get_dependencies(file)
+ new_deps = current_deps.keys() - dep_exeptions - deps
+ deps = deps | current_deps.keys()
+
+ for d in new_deps:
+ rec_gather_all_dependencies(file, deps)
+
+ return deps
+
+def print_deps(deps):
+ print("Found the following dependencies:")
+ for d in deps:
+ print(d)
+
+if __name__ == "__main__":
+ args = parse_arguments()
+ deps = rec_gather_all_dependencies(args.binary)
+ print_deps(deps)
From 8d88572b03a3095f8ff9d604850f5553339deae8 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Tue, 16 Aug 2016 15:50:37 +0200
Subject: [PATCH 09/20] packager and script
Former-commit-id: 4db9b3616e8549a9b1a436f62e9b9f1a14d3728c
---
util/osx-package/packager.py | 94 ++++++++++++++++++++++++++++--------
util/osx-package/run.sh | 10 ++++
2 files changed, 85 insertions(+), 19 deletions(-)
create mode 100644 util/osx-package/run.sh
diff --git a/util/osx-package/packager.py b/util/osx-package/packager.py
index 39d06a667..60b26a8b8 100644
--- a/util/osx-package/packager.py
+++ b/util/osx-package/packager.py
@@ -1,6 +1,7 @@
import argparse
import subprocess
import os
+from shutil import copyfile
def get_dependencies(file):
# Call otool -L file to obtain the dependencies.
@@ -16,32 +17,87 @@ def get_dependencies(file):
return result
+def create_package(args):
+ create_package_dirs(args.dir)
+ copy_binary_to_package_dir(args.bin, args.binary_basename, args.dir)
+ run_dylibbundler(args.bundler_binary, args.dir, args.binary_basename)
+ pass
+
def parse_arguments():
parser = argparse.ArgumentParser(description='Package the storm binary on Mac OS.')
- parser.add_argument('binary', help='the binary to package')
+ parser.add_argument('--bin', dest='bin', help='the binary to package', default='storm')
+ parser.add_argument('--dir', dest='dir', help='the root directory of the package (will be created if it does not exist)', default='.')
+ parser.add_argument('--dylibbundler', dest='bundler_binary', help='the binary of the dylibbundler', default='dylibbundler')
args = parser.parse_args()
+ args.binary_dir = os.path.split(args.bin)[0]
+ args.binary_basename = os.path.split(args.bin)[1]
return args
-dep_exeptions = set()
-dep_exeptions.add("libSystem.B.dylib")
-dep_exeptions.add("libc++.1.dylib")
+def create_package_dirs(root_dir):
+ if not os.path.exists(root_dir):
+ os.makedirs(root_dir)
+ if not os.path.exists(root_dir + "/bin"):
+ os.makedirs(root_dir + "/bin")
+ if not os.path.exists(root_dir + "/lib"):
+ os.makedirs(root_dir + "/bin")
+ pass
-def rec_gather_all_dependencies(file, deps = set()):
- current_deps = get_dependencies(file)
- new_deps = current_deps.keys() - dep_exeptions - deps
- deps = deps | current_deps.keys()
-
- for d in new_deps:
- rec_gather_all_dependencies(file, deps)
-
- return deps
+def copy_binary_to_package_dir(binary, binary_basename, root_dir):
+ copyfile(binary, root_dir + "/bin/storm")
+ pass
+
+def run_dylibbundler(bundler_binary, root_dir, binary_basename):
+ command = [bundler_binary, "-cd", "-od", "-b", "-p", "@executable_path/../lib", "-x", root_dir + "/bin/" + binary_basename, "-d", root_dir + "/lib"]
+ print("executing " + str(command))
+ #proc = subprocess.Popen(command, stdin=subprocess.PIPE, stdout=subprocess.PIPE)
+ pass
+
+def fix_paths(root_dir, binary_basename):
+ fix_paths_file(root_dir + "/bin/" + binary_basename)
+ for file in os.listdir(root_dir + "/lib"):
+ fix_paths_file(root_dir + "/lib/" + file)
+ pass
+ pass
+
+def fix_paths_file(file):
+ print("fixing paths for " + file)
+ fixable_deps = get_fixable_deps(file)
+ for (path, lib) in fixable_deps:
+ change_fixable_dep(file, path, lib)
+
+native_libs = ["libc++.1.dylib", "libSystem.B.dylib"]
+
+def get_fixable_deps(file):
+ # Call otool -L file to obtain the dependencies.
+ proc = subprocess.Popen(["otool", "-L", file], stdin=subprocess.PIPE, stdout=subprocess.PIPE)
+ result = []
+ for line_bytes in proc.stdout:
+ line = line_bytes.decode("utf-8").strip()
+ lib = line.split()[0]
+ if lib.startswith("@rpath/"):
+ result.append(("@rpath", lib.split("/", 1)[1]))
+ elif lib.startswith("/"):
+ path_file = os.path.split(lib)
+ if path_file[1] not in native_libs:
+ result.append((path_file[0], path_file[1]))
+ return result
-def print_deps(deps):
- print("Found the following dependencies:")
- for d in deps:
- print(d)
+def change_fixable_dep(file, path, lib):
+ # Call install_name_tool to change the fixable dependencies
+ command = ["install_name_tool", "-change", path + "/" + lib, "@executable_path/../lib/" + lib, file]
+ print("executing " + str(command))
+ proc = subprocess.Popen(command, stdout=subprocess.PIPE)
+ #print ("after call to install_name_tool")
+ #proc = subprocess.Popen(["otool", "-L", file], stdout=subprocess.PIPE)
+ #for line_bytes in proc.stdout:
+ # line = line_bytes.decode("utf-8").strip()
+ # print(line)
+ pass
if __name__ == "__main__":
args = parse_arguments()
- deps = rec_gather_all_dependencies(args.binary)
- print_deps(deps)
+
+ #create_package(args)
+ fix_paths(args.dir, args.binary_basename)
+
+
diff --git a/util/osx-package/run.sh b/util/osx-package/run.sh
new file mode 100644
index 000000000..0db5b2b5d
--- /dev/null
+++ b/util/osx-package/run.sh
@@ -0,0 +1,10 @@
+#!/bin/sh
+
+DYLIBBUNDLER_DIR=/Users/chris/work/macdylibbundler/
+
+mkdir -p $1
+mkdir -p $1/bin
+mkdir -p $1/lib
+cp $2 $1/bin
+$DYLIBBUNDLER_DIR/dylibbundler -cd -od -b -p @executable_path/../lib -x $1/bin/storm -d $1/lib
+python packager.py --bin storm --dir $1
From 07a457b5d1beded6946652ed83dc900183d94120 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Wed, 17 Aug 2016 11:33:14 +0200
Subject: [PATCH 10/20] renaming packaging script
Former-commit-id: ef506391b4d4211df4c021ac720e8c9da9fd43d2
---
util/osx-package/{run.sh => package.sh} | 0
1 file changed, 0 insertions(+), 0 deletions(-)
rename util/osx-package/{run.sh => package.sh} (100%)
diff --git a/util/osx-package/run.sh b/util/osx-package/package.sh
similarity index 100%
rename from util/osx-package/run.sh
rename to util/osx-package/package.sh
From 5109c45c23af58398e7751db8639b039f62082c3 Mon Sep 17 00:00:00 2001
From: Mavo <matthias.volk@rwth-aachen.de>
Date: Fri, 19 Aug 2016 12:09:48 +0200
Subject: [PATCH 11/20] Fixed returning result for pCTMC
Former-commit-id: 2db7f87f65cefd4da1250163fe73af85a8f9c806
---
src/utility/storm.h | 4 ++--
1 file changed, 2 insertions(+), 2 deletions(-)
diff --git a/src/utility/storm.h b/src/utility/storm.h
index ad9cb1de0..4a32c7ad4 100644
--- a/src/utility/storm.h
+++ b/src/utility/storm.h
@@ -381,10 +381,10 @@ namespace storm {
if (model->getType() == storm::models::ModelType::Dtmc) {
result = verifySparseDtmc(model->template as<storm::models::sparse::Dtmc<storm::RationalFunction>>(), task);
} else if (model->getType() == storm::models::ModelType::Mdp) {
- std::shared_ptr<storm::models::sparse::Mdp<storm::RationalFunction>> mdp = model->template as<storm::models::sparse::Mdp<storm::RationalFunction>>();
+ //std::shared_ptr<storm::models::sparse::Mdp<storm::RationalFunction>> mdp = model->template as<storm::models::sparse::Mdp<storm::RationalFunction>>();
STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "The parametric engine currently does not support MDPs.");
} else if (model->getType() == storm::models::ModelType::Ctmc) {
- verifySparseCtmc(model->template as<storm::models::sparse::Ctmc<storm::RationalFunction>>(), task);
+ result = verifySparseCtmc(model->template as<storm::models::sparse::Ctmc<storm::RationalFunction>>(), task);
} else {
STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "The parametric engine currently does not support " << model->getType());
}
From 6d5f4dc9c924985e7e0879a480750c1b8e4f70a9 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Fri, 19 Aug 2016 08:56:59 +0200
Subject: [PATCH 12/20] fixed bug in detection whether parameters are only used
in probabilities/rewards
Former-commit-id: 1929f5e079a03863d9b838043070be4ffe640314
---
src/storage/prism/Constant.cpp | 7 ++++++-
src/storage/prism/Module.cpp | 4 +++-
src/storage/prism/Program.cpp | 6 ++++--
3 files changed, 13 insertions(+), 4 deletions(-)
diff --git a/src/storage/prism/Constant.cpp b/src/storage/prism/Constant.cpp
index 0416dc4b9..1c3b07057 100644
--- a/src/storage/prism/Constant.cpp
+++ b/src/storage/prism/Constant.cpp
@@ -42,7 +42,12 @@ namespace storm {
}
std::ostream& operator<<(std::ostream& stream, Constant const& constant) {
- stream << "const " << constant.getExpressionVariable().getType() << " ";
+ stream << "const ";
+ if (constant.getType().isRationalType()) {
+ stream << "double" << " ";
+ } else {
+ stream << constant.getType() << " ";
+ }
stream << constant.getName();
if (constant.isDefined()) {
stream << " = " << constant.getExpression();
diff --git a/src/storage/prism/Module.cpp b/src/storage/prism/Module.cpp
index d4168196d..7b929edfc 100644
--- a/src/storage/prism/Module.cpp
+++ b/src/storage/prism/Module.cpp
@@ -216,7 +216,9 @@ namespace storm {
}
for (auto const& command : this->getCommands()) {
- command.containsVariablesOnlyInUpdateProbabilities(undefinedConstantVariables);
+ if (!command.containsVariablesOnlyInUpdateProbabilities(undefinedConstantVariables)) {
+ return false;
+ }
}
return true;
diff --git a/src/storage/prism/Program.cpp b/src/storage/prism/Program.cpp
index c1a1e4cf0..4962157eb 100644
--- a/src/storage/prism/Program.cpp
+++ b/src/storage/prism/Program.cpp
@@ -230,7 +230,7 @@ namespace storm {
// constants' variables is empty (except for the update probabilities).
// Start by checking the defining expressions of all defined constants. If it contains a currently undefined
- //constant, we need to mark the target constant as undefined as well.
+ // constant, we need to mark the target constant as undefined as well.
for (auto const& constant : this->getConstants()) {
if (constant.isDefined()) {
if (constant.getExpression().containsVariable(undefinedConstantVariables)) {
@@ -266,7 +266,9 @@ namespace storm {
// Proceed by checking each of the modules.
for (auto const& module : this->getModules()) {
- module.containsVariablesOnlyInUpdateProbabilities(undefinedConstantVariables);
+ if (!module.containsVariablesOnlyInUpdateProbabilities(undefinedConstantVariables)) {
+ return false;
+ }
}
// Check the reward models.
From e6d9c85749964659472384a2fe5d40ddaf26de01 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Fri, 19 Aug 2016 19:33:40 +0200
Subject: [PATCH 13/20] fixed some bugs related to simplifaction of PRISM
programs
Former-commit-id: 3c81bcac8d34b9a88180a0542c7b1e1f305848b3
---
src/generator/JaniNextStateGenerator.cpp | 3 +
src/generator/PrismNextStateGenerator.cpp | 9 ++-
src/parser/PrismParser.cpp | 2 +
src/storage/prism/Module.h | 1 -
src/storage/prism/Program.cpp | 72 ++++++++++++++++++-----
src/storage/prism/RewardModel.cpp | 18 ++++++
src/storage/prism/RewardModel.h | 9 +++
src/utility/storm.cpp | 2 +-
8 files changed, 95 insertions(+), 21 deletions(-)
diff --git a/src/generator/JaniNextStateGenerator.cpp b/src/generator/JaniNextStateGenerator.cpp
index cfb08fb79..0b2fad41a 100644
--- a/src/generator/JaniNextStateGenerator.cpp
+++ b/src/generator/JaniNextStateGenerator.cpp
@@ -161,6 +161,9 @@ namespace storm {
}
// Block the current initial state to search for the next one.
+ if (!blockingExpression.isInitialized()) {
+ break;
+ }
solver->add(blockingExpression);
}
diff --git a/src/generator/PrismNextStateGenerator.cpp b/src/generator/PrismNextStateGenerator.cpp
index c0026a98d..7eb2291c5 100644
--- a/src/generator/PrismNextStateGenerator.cpp
+++ b/src/generator/PrismNextStateGenerator.cpp
@@ -23,8 +23,9 @@ namespace storm {
template<typename ValueType, typename StateType>
PrismNextStateGenerator<ValueType, StateType>::PrismNextStateGenerator(storm::prism::Program const& program, NextStateGeneratorOptions const& options, bool flag) : NextStateGenerator<ValueType, StateType>(program.getManager(), options), program(program), rewardModels() {
+ STORM_LOG_TRACE("Creating next-state generator for PRISM program: " << program);
STORM_LOG_THROW(!this->program.specifiesSystemComposition(), storm::exceptions::WrongFormatException, "The explicit next-state generator currently does not support custom system compositions.");
-
+
// Only after checking validity of the program, we initialize the variable information.
this->checkValid(program);
this->variableInformation = VariableInformation(program);
@@ -166,6 +167,9 @@ namespace storm {
initialStateIndices.push_back(id);
// Block the current initial state to search for the next one.
+ if (!blockingExpression.isInitialized()) {
+ break;
+ }
solver->add(blockingExpression);
}
@@ -314,7 +318,7 @@ namespace storm {
template<typename ValueType, typename StateType>
boost::optional<std::vector<std::vector<std::reference_wrapper<storm::prism::Command const>>>> PrismNextStateGenerator<ValueType, StateType>::getActiveCommandsByActionIndex(uint_fast64_t const& actionIndex) {
boost::optional<std::vector<std::vector<std::reference_wrapper<storm::prism::Command const>>>> result((std::vector<std::vector<std::reference_wrapper<storm::prism::Command const>>>()));
-
+
// Iterate over all modules.
for (uint_fast64_t i = 0; i < program.getNumberOfModules(); ++i) {
storm::prism::Module const& module = program.getModule(i);
@@ -445,7 +449,6 @@ namespace storm {
for (uint_fast64_t i = 0; i < iteratorList.size(); ++i) {
storm::prism::Command const& command = *iteratorList[i];
-
for (uint_fast64_t j = 0; j < command.getNumberOfUpdates(); ++j) {
storm::prism::Update const& update = command.getUpdate(j);
diff --git a/src/parser/PrismParser.cpp b/src/parser/PrismParser.cpp
index 7d54f18c6..f9f4350b9 100644
--- a/src/parser/PrismParser.cpp
+++ b/src/parser/PrismParser.cpp
@@ -65,6 +65,8 @@ namespace storm {
STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << lineNumber << " of file " << filename << ".");
}
+ STORM_LOG_TRACE("Parsed PRISM input: " << result);
+
return result;
}
diff --git a/src/storage/prism/Module.h b/src/storage/prism/Module.h
index 620432580..df8a61c21 100644
--- a/src/storage/prism/Module.h
+++ b/src/storage/prism/Module.h
@@ -104,7 +104,6 @@ namespace storm {
*/
std::set<storm::expressions::Variable> getAllExpressionVariables() const;
-
/*!
* Retrieves a list of expressions that characterize the legal ranges of all variables declared by this
* module.
diff --git a/src/storage/prism/Program.cpp b/src/storage/prism/Program.cpp
index 4962157eb..acb17a17e 100644
--- a/src/storage/prism/Program.cpp
+++ b/src/storage/prism/Program.cpp
@@ -734,6 +734,12 @@ namespace storm {
}
}
+ // As we possibly delete some commands and some actions might be dropped from modules altogether, we need to
+ // maintain a list of actions that we need to remove in other modules. For example, if module A loses all [a]
+ // commands, we need to delete all [a] commands from all other modules as well. If we do not do that, we will
+ // remove the forced synchronization that was there before.
+ std::set<uint_fast64_t> actionIndicesToDelete;
+
// Now we can substitute the constants in all expressions appearing in the program.
std::vector<BooleanVariable> newBooleanVariables;
newBooleanVariables.reserve(this->getNumberOfGlobalBooleanVariables());
@@ -757,6 +763,9 @@ namespace storm {
newModules.reserve(this->getNumberOfModules());
for (auto const& module : this->getModules()) {
newModules.emplace_back(module.substitute(constantSubstitution));
+
+ // Determine the set of action indices that have been deleted entirely.
+ std::set_difference(module.getSynchronizingActionIndices().begin(), module.getSynchronizingActionIndices().end(), newModules.back().getSynchronizingActionIndices().begin(), newModules.back().getSynchronizingActionIndices().end(), std::inserter(actionIndicesToDelete, actionIndicesToDelete.begin()));
}
std::vector<RewardModel> newRewardModels;
@@ -773,7 +782,37 @@ namespace storm {
newLabels.emplace_back(label.substitute(constantSubstitution));
}
- return Program(this->manager, this->getModelType(), newConstants, newBooleanVariables, newIntegerVariables, newFormulas, newModules, this->getActionNameToIndexMapping(), newRewardModels, newLabels, newInitialConstruct, this->getOptionalSystemCompositionConstruct());
+ // If we have to delete whole actions, do so now.
+ std::map<std::string, uint_fast64_t> newActionToIndexMap;
+ if (!actionIndicesToDelete.empty()) {
+ boost::container::flat_set<uint_fast64_t> actionsToKeep;
+ std::set_difference(this->getSynchronizingActionIndices().begin(), this->getSynchronizingActionIndices().end(), actionIndicesToDelete.begin(), actionIndicesToDelete.end(), std::inserter(actionsToKeep, actionsToKeep.begin()));
+
+ // Insert the silent action as this is not contained in the synchronizing action indices.
+ actionsToKeep.insert(0);
+
+ std::vector<Module> cleanedModules;
+ cleanedModules.reserve(this->getNumberOfModules());
+ for (auto const& module : newModules) {
+ cleanedModules.emplace_back(module.restrictCommands(actionsToKeep));
+ }
+ newModules = std::move(cleanedModules);
+
+ std::vector<RewardModel> cleanedRewardModels;
+ cleanedRewardModels.reserve(this->getNumberOfRewardModels());
+ for (auto const& rewardModel : newRewardModels) {
+ cleanedRewardModels.emplace_back(rewardModel.restrictActionRelatedRewards(actionsToKeep));
+ }
+ newRewardModels = std::move(cleanedRewardModels);
+
+ for (auto const& entry : this->getActionNameToIndexMapping()) {
+ if (actionsToKeep.find(entry.second) != actionsToKeep.end()) {
+ newActionToIndexMap.emplace(entry.first, entry.second);
+ }
+ }
+ }
+
+ return Program(this->manager, this->getModelType(), newConstants, newBooleanVariables, newIntegerVariables, newFormulas, newModules, actionIndicesToDelete.empty() ? this->getActionNameToIndexMapping() : newActionToIndexMap, newRewardModels, newLabels, newInitialConstruct, this->getOptionalSystemCompositionConstruct());
}
void Program::checkValidity(Program::ValidityCheckLevel lvl) const {
@@ -1153,17 +1192,19 @@ namespace storm {
}
Program Program::simplify() {
+ // Start by substituting the constants, because this will potentially erase some commands or even actions.
+ Program substitutedProgram = this->substituteConstants();
+
std::vector<Module> newModules;
- std::vector<Constant> newConstants = this->getConstants();
- for (auto const& module : this->getModules()) {
- // Remove identity assignments from the updates
+ std::vector<Constant> newConstants = substitutedProgram.getConstants();
+ for (auto const& module : substitutedProgram.getModules()) {
+ // Remove identity assignments from the updates.
std::vector<Command> newCommands;
for (auto const& command : module.getCommands()) {
newCommands.emplace_back(command.removeIdentityAssignmentsFromUpdates());
}
- // Substitute Variables by Global constants if possible.
-
+ // Substitute variables by global constants if possible.
std::map<storm::expressions::Variable, storm::expressions::Expression> booleanVars;
std::map<storm::expressions::Variable, storm::expressions::Expression> integerVars;
for (auto const& variable : module.getBooleanVariables()) {
@@ -1179,11 +1220,11 @@ namespace storm {
// Check all assignments.
for (auto const& assignment : update.getAssignments()) {
auto bit = booleanVars.find(assignment.getVariable());
- if(bit != booleanVars.end()) {
+ if (bit != booleanVars.end()) {
booleanVars.erase(bit);
} else {
auto iit = integerVars.find(assignment.getVariable());
- if(iit != integerVars.end()) {
+ if (iit != integerVars.end()) {
integerVars.erase(iit);
}
}
@@ -1192,31 +1233,30 @@ namespace storm {
}
std::vector<storm::prism::BooleanVariable> newBVars;
- for(auto const& variable : module.getBooleanVariables()) {
- if(booleanVars.count(variable.getExpressionVariable()) == 0) {
+ for (auto const& variable : module.getBooleanVariables()) {
+ if (booleanVars.find(variable.getExpressionVariable()) == booleanVars.end()) {
newBVars.push_back(variable);
}
}
std::vector<storm::prism::IntegerVariable> newIVars;
- for(auto const& variable : module.getIntegerVariables()) {
- if(integerVars.count(variable.getExpressionVariable()) == 0) {
+ for (auto const& variable : module.getIntegerVariables()) {
+ if (integerVars.find(variable.getExpressionVariable()) == integerVars.end()) {
newIVars.push_back(variable);
}
}
newModules.emplace_back(module.getName(), newBVars, newIVars, newCommands);
- for(auto const& entry : booleanVars) {
+ for (auto const& entry : booleanVars) {
newConstants.emplace_back(entry.first, entry.second);
}
- for(auto const& entry : integerVars) {
+ for (auto const& entry : integerVars) {
newConstants.emplace_back(entry.first, entry.second);
}
}
- return replaceModulesAndConstantsInProgram(newModules, newConstants).substituteConstants();
-
+ return substitutedProgram.replaceModulesAndConstantsInProgram(newModules, newConstants);
}
Program Program::replaceModulesAndConstantsInProgram(std::vector<Module> const& newModules, std::vector<Constant> const& newConstants) {
diff --git a/src/storage/prism/RewardModel.cpp b/src/storage/prism/RewardModel.cpp
index 30c43728c..52ef5dc67 100644
--- a/src/storage/prism/RewardModel.cpp
+++ b/src/storage/prism/RewardModel.cpp
@@ -81,6 +81,24 @@ namespace storm {
return true;
}
+ RewardModel RewardModel::restrictActionRelatedRewards(boost::container::flat_set<uint_fast64_t> const& actionIndicesToKeep) const {
+ std::vector<StateActionReward> newStateActionRewards;
+ for (auto const& stateActionReward : this->getStateActionRewards()) {
+ if (actionIndicesToKeep.find(stateActionReward.getActionIndex()) != actionIndicesToKeep.end()) {
+ newStateActionRewards.emplace_back(stateActionReward);
+ }
+ }
+
+ std::vector<TransitionReward> newTransitionRewards;
+ for (auto const& transitionReward : this->getTransitionRewards()) {
+ if (actionIndicesToKeep.find(transitionReward.getActionIndex()) != actionIndicesToKeep.end()) {
+ newTransitionRewards.emplace_back(transitionReward);
+ }
+ }
+
+ return RewardModel(this->getName(), this->getStateRewards(), newStateActionRewards, newTransitionRewards, this->getFilename(), this->getLineNumber());
+ }
+
std::ostream& operator<<(std::ostream& stream, RewardModel const& rewardModel) {
stream << "rewards";
if (rewardModel.getName() != "") {
diff --git a/src/storage/prism/RewardModel.h b/src/storage/prism/RewardModel.h
index c62aff61a..01ab69508 100644
--- a/src/storage/prism/RewardModel.h
+++ b/src/storage/prism/RewardModel.h
@@ -4,6 +4,7 @@
#include <string>
#include <vector>
#include <map>
+#include <boost/container/flat_set.hpp>
#include "src/storage/prism/StateReward.h"
#include "src/storage/prism/StateActionReward.h"
@@ -108,6 +109,14 @@ namespace storm {
*/
bool containsVariablesOnlyInRewardValueExpressions(std::set<storm::expressions::Variable> const& undefinedConstantVariables) const;
+ /*!
+ * Restricts all action-related rewards of the reward model to the ones with an action index in the provided set.
+ *
+ * @param actionIndicesToKeep The set of action indices to keep.
+ * @return The resulting reward model.
+ */
+ RewardModel restrictActionRelatedRewards(boost::container::flat_set<uint_fast64_t> const& actionIndicesToKeep) const;
+
friend std::ostream& operator<<(std::ostream& stream, RewardModel const& rewardModel);
private:
diff --git a/src/utility/storm.cpp b/src/utility/storm.cpp
index 5956e72c9..c6d2f9c65 100644
--- a/src/utility/storm.cpp
+++ b/src/utility/storm.cpp
@@ -10,7 +10,7 @@
namespace storm {
storm::prism::Program parseProgram(std::string const& path) {
- storm::prism::Program program= storm::parser::PrismParser::parse(path).simplify().simplify();
+ storm::prism::Program program = storm::parser::PrismParser::parse(path).simplify().simplify();
program.checkValidity();
return program;
}
From 3ea11188b7f0c9bb6e3784686eece7678594108d Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Fri, 19 Aug 2016 19:35:03 +0200
Subject: [PATCH 14/20] fixed an issue in the CMakeLists.txt that prevented
carl from being properly loaded if it's not already present
Former-commit-id: 95b83d39882a6bd743d65b484fb3e5d168cb7020
---
resources/3rdparty/CMakeLists.txt | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/resources/3rdparty/CMakeLists.txt b/resources/3rdparty/CMakeLists.txt
index 042eaea43..244e24057 100644
--- a/resources/3rdparty/CMakeLists.txt
+++ b/resources/3rdparty/CMakeLists.txt
@@ -204,7 +204,7 @@ if(USE_CARL)
LOG_INSTALL ON
)
- add_dependencies(resources xercesc)
+ add_dependencies(resources carl)
include_directories(${STORM_3RDPARTY_BINARY_DIR}/carl/include)
list(APPEND STORM_LINK_LIBRARIES ${STORM_3RDPARTY_BINARY_DIR}/carl/lib/libcarl${DYNAMIC_EXT})
set(STORM_HAVE_CARL ON)
From bcb13a4fe1140ea6d415ba94c9fd9ca167404a2b Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Fri, 19 Aug 2016 21:36:56 +0200
Subject: [PATCH 15/20] moved deletion of commands (if guard becomes false)
from Program::substitute to Program::simplify
Former-commit-id: ec5b4d4a579898eb36252f1e0b0fb786b8ea7c50
---
src/storage/prism/Module.cpp | 5 +-
src/storage/prism/Program.cpp | 119 +++++++++++++++++-----------------
src/storage/prism/Program.h | 8 ---
3 files changed, 61 insertions(+), 71 deletions(-)
diff --git a/src/storage/prism/Module.cpp b/src/storage/prism/Module.cpp
index 7b929edfc..755c4c78a 100644
--- a/src/storage/prism/Module.cpp
+++ b/src/storage/prism/Module.cpp
@@ -188,10 +188,7 @@ namespace storm {
std::vector<Command> newCommands;
newCommands.reserve(this->getNumberOfCommands());
for (auto const& command : this->getCommands()) {
- Command newCommand = command.substitute(substitution);
- if (!newCommand.getGuardExpression().isFalse()) {
- newCommands.emplace_back(newCommand);
- }
+ newCommands.emplace_back(command.substitute(substitution));
}
return Module(this->getName(), newBooleanVariables, newIntegerVariables, newCommands, this->getFilename(), this->getLineNumber());
diff --git a/src/storage/prism/Program.cpp b/src/storage/prism/Program.cpp
index acb17a17e..cdc3d323a 100644
--- a/src/storage/prism/Program.cpp
+++ b/src/storage/prism/Program.cpp
@@ -717,7 +717,7 @@ namespace storm {
}
Program Program::substituteConstants() const {
- // We start by creating the appropriate substitution
+ // We start by creating the appropriate substitution.
std::map<storm::expressions::Variable, storm::expressions::Expression> constantSubstitution;
std::vector<Constant> newConstants(this->getConstants());
for (uint_fast64_t constantIndex = 0; constantIndex < newConstants.size(); ++constantIndex) {
@@ -734,12 +734,6 @@ namespace storm {
}
}
- // As we possibly delete some commands and some actions might be dropped from modules altogether, we need to
- // maintain a list of actions that we need to remove in other modules. For example, if module A loses all [a]
- // commands, we need to delete all [a] commands from all other modules as well. If we do not do that, we will
- // remove the forced synchronization that was there before.
- std::set<uint_fast64_t> actionIndicesToDelete;
-
// Now we can substitute the constants in all expressions appearing in the program.
std::vector<BooleanVariable> newBooleanVariables;
newBooleanVariables.reserve(this->getNumberOfGlobalBooleanVariables());
@@ -763,9 +757,6 @@ namespace storm {
newModules.reserve(this->getNumberOfModules());
for (auto const& module : this->getModules()) {
newModules.emplace_back(module.substitute(constantSubstitution));
-
- // Determine the set of action indices that have been deleted entirely.
- std::set_difference(module.getSynchronizingActionIndices().begin(), module.getSynchronizingActionIndices().end(), newModules.back().getSynchronizingActionIndices().begin(), newModules.back().getSynchronizingActionIndices().end(), std::inserter(actionIndicesToDelete, actionIndicesToDelete.begin()));
}
std::vector<RewardModel> newRewardModels;
@@ -782,37 +773,7 @@ namespace storm {
newLabels.emplace_back(label.substitute(constantSubstitution));
}
- // If we have to delete whole actions, do so now.
- std::map<std::string, uint_fast64_t> newActionToIndexMap;
- if (!actionIndicesToDelete.empty()) {
- boost::container::flat_set<uint_fast64_t> actionsToKeep;
- std::set_difference(this->getSynchronizingActionIndices().begin(), this->getSynchronizingActionIndices().end(), actionIndicesToDelete.begin(), actionIndicesToDelete.end(), std::inserter(actionsToKeep, actionsToKeep.begin()));
-
- // Insert the silent action as this is not contained in the synchronizing action indices.
- actionsToKeep.insert(0);
-
- std::vector<Module> cleanedModules;
- cleanedModules.reserve(this->getNumberOfModules());
- for (auto const& module : newModules) {
- cleanedModules.emplace_back(module.restrictCommands(actionsToKeep));
- }
- newModules = std::move(cleanedModules);
-
- std::vector<RewardModel> cleanedRewardModels;
- cleanedRewardModels.reserve(this->getNumberOfRewardModels());
- for (auto const& rewardModel : newRewardModels) {
- cleanedRewardModels.emplace_back(rewardModel.restrictActionRelatedRewards(actionsToKeep));
- }
- newRewardModels = std::move(cleanedRewardModels);
-
- for (auto const& entry : this->getActionNameToIndexMapping()) {
- if (actionsToKeep.find(entry.second) != actionsToKeep.end()) {
- newActionToIndexMap.emplace(entry.first, entry.second);
- }
- }
- }
-
- return Program(this->manager, this->getModelType(), newConstants, newBooleanVariables, newIntegerVariables, newFormulas, newModules, actionIndicesToDelete.empty() ? this->getActionNameToIndexMapping() : newActionToIndexMap, newRewardModels, newLabels, newInitialConstruct, this->getOptionalSystemCompositionConstruct());
+ return Program(this->manager, this->getModelType(), newConstants, newBooleanVariables, newIntegerVariables, newFormulas, newModules, this->getActionNameToIndexMapping(), newRewardModels, newLabels, newInitialConstruct, this->getOptionalSystemCompositionConstruct());
}
void Program::checkValidity(Program::ValidityCheckLevel lvl) const {
@@ -1195,13 +1156,22 @@ namespace storm {
// Start by substituting the constants, because this will potentially erase some commands or even actions.
Program substitutedProgram = this->substituteConstants();
+ // As we possibly delete some commands and some actions might be dropped from modules altogether, we need to
+ // maintain a list of actions that we need to remove in other modules. For example, if module A loses all [a]
+ // commands, we need to delete all [a] commands from all other modules as well. If we do not do that, we will
+ // remove the forced synchronization that was there before.
+ std::set<uint_fast64_t> actionIndicesToDelete;
+
std::vector<Module> newModules;
std::vector<Constant> newConstants = substitutedProgram.getConstants();
for (auto const& module : substitutedProgram.getModules()) {
- // Remove identity assignments from the updates.
+
+ // Discard all commands with a guard equivalent to false and remove identity assignments from the updates.
std::vector<Command> newCommands;
for (auto const& command : module.getCommands()) {
- newCommands.emplace_back(command.removeIdentityAssignmentsFromUpdates());
+ if (!command.getGuardExpression().isFalse()) {
+ newCommands.emplace_back(command.removeIdentityAssignmentsFromUpdates());
+ }
}
// Substitute variables by global constants if possible.
@@ -1214,38 +1184,44 @@ namespace storm {
integerVars.emplace(variable.getExpressionVariable(), variable.getInitialValueExpression());
}
+ // Collect all variables that are being written. These variables cannot be turned to constants.
for (auto const& command : newCommands) {
// Check all updates.
for (auto const& update : command.getUpdates()) {
// Check all assignments.
for (auto const& assignment : update.getAssignments()) {
- auto bit = booleanVars.find(assignment.getVariable());
- if (bit != booleanVars.end()) {
- booleanVars.erase(bit);
+ if (assignment.getVariable().getType().isBooleanType()) {
+ auto it = booleanVars.find(assignment.getVariable());
+ if (it != booleanVars.end()) {
+ booleanVars.erase(it);
+ }
} else {
- auto iit = integerVars.find(assignment.getVariable());
- if (iit != integerVars.end()) {
- integerVars.erase(iit);
+ auto it = integerVars.find(assignment.getVariable());
+ if (it != integerVars.end()) {
+ integerVars.erase(it);
}
}
}
}
}
- std::vector<storm::prism::BooleanVariable> newBVars;
+ std::vector<storm::prism::BooleanVariable> newBooleanVars;
for (auto const& variable : module.getBooleanVariables()) {
if (booleanVars.find(variable.getExpressionVariable()) == booleanVars.end()) {
- newBVars.push_back(variable);
+ newBooleanVars.push_back(variable);
}
}
- std::vector<storm::prism::IntegerVariable> newIVars;
+ std::vector<storm::prism::IntegerVariable> newIntegerVars;
for (auto const& variable : module.getIntegerVariables()) {
if (integerVars.find(variable.getExpressionVariable()) == integerVars.end()) {
- newIVars.push_back(variable);
+ newIntegerVars.push_back(variable);
}
}
- newModules.emplace_back(module.getName(), newBVars, newIVars, newCommands);
+ newModules.emplace_back(module.getName(), newBooleanVars, newIntegerVars, newCommands);
+
+ // Determine the set of action indices that have been deleted entirely.
+ std::set_difference(module.getSynchronizingActionIndices().begin(), module.getSynchronizingActionIndices().end(), newModules.back().getSynchronizingActionIndices().begin(), newModules.back().getSynchronizingActionIndices().end(), std::inserter(actionIndicesToDelete, actionIndicesToDelete.begin()));
for (auto const& entry : booleanVars) {
newConstants.emplace_back(entry.first, entry.second);
@@ -1256,11 +1232,36 @@ namespace storm {
}
}
- return substitutedProgram.replaceModulesAndConstantsInProgram(newModules, newConstants);
- }
-
- Program Program::replaceModulesAndConstantsInProgram(std::vector<Module> const& newModules, std::vector<Constant> const& newConstants) {
- return Program(this->manager, modelType, newConstants, getGlobalBooleanVariables(), getGlobalIntegerVariables(), getFormulas(), newModules, getActionNameToIndexMapping(), getRewardModels(), getLabels(), getInitialConstruct(), this->getOptionalSystemCompositionConstruct());
+ // If we have to delete whole actions, do so now.
+ std::map<std::string, uint_fast64_t> newActionToIndexMap;
+ std::vector<RewardModel> newRewardModels;
+ if (!actionIndicesToDelete.empty()) {
+ boost::container::flat_set<uint_fast64_t> actionsToKeep;
+ std::set_difference(this->getSynchronizingActionIndices().begin(), this->getSynchronizingActionIndices().end(), actionIndicesToDelete.begin(), actionIndicesToDelete.end(), std::inserter(actionsToKeep, actionsToKeep.begin()));
+
+ // Insert the silent action as this is not contained in the synchronizing action indices.
+ actionsToKeep.insert(0);
+
+ std::vector<Module> cleanedModules;
+ cleanedModules.reserve(newModules.size());
+ for (auto const& module : newModules) {
+ cleanedModules.emplace_back(module.restrictCommands(actionsToKeep));
+ }
+ newModules = std::move(cleanedModules);
+
+ newRewardModels.reserve(substitutedProgram.getNumberOfRewardModels());
+ for (auto const& rewardModel : substitutedProgram.getRewardModels()) {
+ newRewardModels.emplace_back(rewardModel.restrictActionRelatedRewards(actionsToKeep));
+ }
+
+ for (auto const& entry : this->getActionNameToIndexMapping()) {
+ if (actionsToKeep.find(entry.second) != actionsToKeep.end()) {
+ newActionToIndexMap.emplace(entry.first, entry.second);
+ }
+ }
+ }
+
+ return Program(this->manager, modelType, newConstants, getGlobalBooleanVariables(), getGlobalIntegerVariables(), getFormulas(), newModules, actionIndicesToDelete.empty() ? getActionNameToIndexMapping() : newActionToIndexMap, actionIndicesToDelete.empty() ? this->getRewardModels() : newRewardModels, getLabels(), getInitialConstruct(), this->getOptionalSystemCompositionConstruct());
}
Program Program::flattenModules(std::unique_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory) const {
diff --git a/src/storage/prism/Program.h b/src/storage/prism/Program.h
index 71719c583..8c30079e0 100644
--- a/src/storage/prism/Program.h
+++ b/src/storage/prism/Program.h
@@ -661,14 +661,6 @@ namespace storm {
// A mapping from variable names to the modules in which they were declared.
std::map<std::string, uint_fast64_t> variableToModuleIndexMap;
-
- /**
- * Takes the current program and replaces all modules. As we reuse the expression manager, we recommend to not use the original program any further.
- * @param newModules the modules which replace the old modules.
- * @param newConstants the constants which replace the old constants.
- * @return A program with the new modules and constants.
- */
- Program replaceModulesAndConstantsInProgram(std::vector<Module> const& newModules, std::vector<Constant> const& newConstants);
};
std::ostream& operator<<(std::ostream& out, Program::ModelType const& type);
From 96891acfe7e53805c6ed6813538319704354adc7 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Mon, 22 Aug 2016 13:10:03 +0200
Subject: [PATCH 16/20] included missing (at least for some compilers) header
Former-commit-id: 4792acf519378b62e9899f5b941559c5b6fffcd6
---
src/modelchecker/AbstractModelChecker.cpp | 1 +
1 file changed, 1 insertion(+)
diff --git a/src/modelchecker/AbstractModelChecker.cpp b/src/modelchecker/AbstractModelChecker.cpp
index 616dcf828..5d1759b94 100644
--- a/src/modelchecker/AbstractModelChecker.cpp
+++ b/src/modelchecker/AbstractModelChecker.cpp
@@ -17,6 +17,7 @@
#include "src/models/symbolic/Mdp.h"
#include "src/models/sparse/MarkovAutomaton.h"
#include "src/models/sparse/StandardRewardModel.h"
+#include "src/models/sparse/StandardRewardModel.h"
#include "src/storage/dd/Add.h"
#include "src/storage/dd/Bdd.h"
From a8383a283df2ec0de677d411ccf52d2e01a2704b Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Mon, 22 Aug 2016 13:40:20 +0200
Subject: [PATCH 17/20] fixed wrong header inclusion in previous commit
Former-commit-id: f91e63cccd11cc119e4c7eb4320b4575693250aa
---
src/modelchecker/AbstractModelChecker.cpp | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/src/modelchecker/AbstractModelChecker.cpp b/src/modelchecker/AbstractModelChecker.cpp
index 5d1759b94..660906acb 100644
--- a/src/modelchecker/AbstractModelChecker.cpp
+++ b/src/modelchecker/AbstractModelChecker.cpp
@@ -17,7 +17,7 @@
#include "src/models/symbolic/Mdp.h"
#include "src/models/sparse/MarkovAutomaton.h"
#include "src/models/sparse/StandardRewardModel.h"
-#include "src/models/sparse/StandardRewardModel.h"
+#include "src/models/symbolic/StandardRewardModel.h"
#include "src/storage/dd/Add.h"
#include "src/storage/dd/Bdd.h"
From d1ea67524587f8cb6744d6f5c69158a5fcde7c65 Mon Sep 17 00:00:00 2001
From: TimQu <tim.quatmann@web.de>
Date: Tue, 30 Aug 2016 01:54:24 +0200
Subject: [PATCH 18/20] Added missing case for Power when converting to
z3::expr
Former-commit-id: 4279fba636d06c93c030003b6c1f105139a6e2a8
---
src/adapters/Z3ExpressionAdapter.cpp | 2 ++
1 file changed, 2 insertions(+)
diff --git a/src/adapters/Z3ExpressionAdapter.cpp b/src/adapters/Z3ExpressionAdapter.cpp
index 6f4efc178..a80355422 100644
--- a/src/adapters/Z3ExpressionAdapter.cpp
+++ b/src/adapters/Z3ExpressionAdapter.cpp
@@ -177,6 +177,8 @@ namespace storm {
return ite(leftResult <= rightResult, leftResult, rightResult);
case storm::expressions::BinaryNumericalFunctionExpression::OperatorType::Max:
return ite(leftResult >= rightResult, leftResult, rightResult);
+ case storm::expressions::BinaryNumericalFunctionExpression::OperatorType::Power:
+ return pw(leftResult,rightResult);
default:
STORM_LOG_THROW(false, storm::exceptions::ExpressionEvaluationException, "Cannot evaluate expression: unknown numerical binary operator '" << static_cast<int>(expression.getOperatorType()) << "' in expression " << expression << ".");
}
From 1b19372a14a34fa5c828964df264fc7be1a8ebde Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Sat, 3 Sep 2016 19:20:05 +0200
Subject: [PATCH 19/20] changed a default argument initializer list to make
compilers happier
Former-commit-id: 41dcbd2f10c6528714e4bb727c78f70f519e0400
---
src/parser/JaniParser.h | 5 ++---
1 file changed, 2 insertions(+), 3 deletions(-)
diff --git a/src/parser/JaniParser.h b/src/parser/JaniParser.h
index e4fafcd2a..90891c759 100644
--- a/src/parser/JaniParser.h
+++ b/src/parser/JaniParser.h
@@ -34,7 +34,8 @@ namespace storm {
storm::jani::Model parseModel();
storm::jani::Automaton parseAutomaton(json const& automatonStructure);
std::shared_ptr<storm::jani::Variable> parseVariable(json const& variableStructure, std::string const& scopeDescription, bool prefWithScope = false);
- storm::expressions::Expression parseExpression(json const& expressionStructure, std::string const& scopeDescription, std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>> const& localVars = {});
+ storm::expressions::Expression parseExpression(json const& expressionStructure, std::string const& scopeDescription, std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>> const& localVars = std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>>());
+
private:
/**
* Helper for parsing the actions of a model.
@@ -43,8 +44,6 @@ namespace storm {
std::shared_ptr<storm::jani::Composition> parseComposition(json const& compositionStructure);
-
-
};
}
}
From 92932fced10eecd82b93c5fedcfea557b2e49b2f Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Mon, 5 Sep 2016 17:12:30 +0200
Subject: [PATCH 20/20] support for initial constructs in PRISM programs
Former-commit-id: 0c8132aa432a46bff8de64792bd9a9204efd2ce3
---
src/parser/PrismParser.cpp | 18 +--
src/parser/PrismParser.h | 6 +-
src/storage/prism/BooleanVariable.cpp | 16 ++-
src/storage/prism/BooleanVariable.h | 2 +
src/storage/prism/IntegerVariable.cpp | 14 ++-
src/storage/prism/IntegerVariable.h | 2 +
src/storage/prism/Module.cpp | 11 +-
src/storage/prism/Module.h | 5 +
src/storage/prism/Program.cpp | 171 ++++++++++++++++----------
src/storage/prism/Program.h | 7 +-
src/storage/prism/Variable.cpp | 12 +-
src/storage/prism/Variable.h | 27 ++--
12 files changed, 199 insertions(+), 92 deletions(-)
diff --git a/src/parser/PrismParser.cpp b/src/parser/PrismParser.cpp
index f9f4350b9..d3e5191e2 100644
--- a/src/parser/PrismParser.cpp
+++ b/src/parser/PrismParser.cpp
@@ -105,10 +105,10 @@ namespace storm {
formulaDefinition = (qi::lit("formula") > identifier > qi::lit("=") > expressionParser > qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createFormula, phoenix::ref(*this), qi::_1, qi::_2)];
formulaDefinition.name("formula definition");
- booleanVariableDefinition = ((identifier >> qi::lit(":") >> qi::lit("bool")) > ((qi::lit("init") > expressionParser) | qi::attr(manager->boolean(false))) > qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createBooleanVariable, phoenix::ref(*this), qi::_1, qi::_2)];
+ booleanVariableDefinition = ((identifier >> qi::lit(":") >> qi::lit("bool")) > -((qi::lit("init") > expressionParser[qi::_a = qi::_1]) | qi::attr(manager->boolean(false))) > qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createBooleanVariable, phoenix::ref(*this), qi::_1, qi::_a)];
booleanVariableDefinition.name("boolean variable definition");
- integerVariableDefinition = ((identifier >> qi::lit(":") >> qi::lit("[")[phoenix::bind(&PrismParser::allowDoubleLiterals, phoenix::ref(*this), false)]) > expressionParser[qi::_a = qi::_1] > qi::lit("..") > expressionParser > qi::lit("]")[phoenix::bind(&PrismParser::allowDoubleLiterals, phoenix::ref(*this), true)] > -(qi::lit("init") > expressionParser[qi::_a = qi::_1]) > qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createIntegerVariable, phoenix::ref(*this), qi::_1, qi::_2, qi::_3, qi::_a)];
+ integerVariableDefinition = ((identifier >> qi::lit(":") >> qi::lit("[")[phoenix::bind(&PrismParser::allowDoubleLiterals, phoenix::ref(*this), false)]) > expressionParser > qi::lit("..") > expressionParser > qi::lit("]")[phoenix::bind(&PrismParser::allowDoubleLiterals, phoenix::ref(*this), true)] > -(qi::lit("init") > expressionParser[qi::_a = qi::_1]) > qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createIntegerVariable, phoenix::ref(*this), qi::_1, qi::_2, qi::_3, qi::_a)];
integerVariableDefinition.name("integer variable definition");
variableDefinition = (booleanVariableDefinition[phoenix::push_back(qi::_r1, qi::_1)] | integerVariableDefinition[phoenix::push_back(qi::_r2, qi::_1)]);
@@ -210,7 +210,7 @@ namespace storm {
moduleDefinitionList %= +(moduleRenaming(qi::_r1) | moduleDefinition(qi::_r1))[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::modules, qi::_r1), qi::_1)];
moduleDefinitionList.name("module list");
- start = (qi::eps
+ start = (qi::eps[phoenix::bind(&PrismParser::removeInitialConstruct, phoenix::ref(*this), qi::_a)]
> modelTypeDefinition[phoenix::bind(&GlobalProgramInformation::modelType, qi::_a) = qi::_1]
> *(definedConstantDefinition[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::constants, qi::_a), qi::_1)]
| undefinedConstantDefinition[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::constants, qi::_a), qi::_1)]
@@ -278,7 +278,7 @@ namespace storm {
return true;
}
- bool PrismParser::addInitialStatesConstruct(storm::expressions::Expression initialStatesExpression, GlobalProgramInformation& globalProgramInformation) {
+ bool PrismParser::addInitialStatesConstruct(storm::expressions::Expression const& initialStatesExpression, GlobalProgramInformation& globalProgramInformation) {
STORM_LOG_THROW(!globalProgramInformation.hasInitialConstruct, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Program must not define two initial constructs.");
if (globalProgramInformation.hasInitialConstruct) {
return false;
@@ -587,7 +587,7 @@ namespace storm {
auto const& renamingPair = renaming.find(variable.getName());
STORM_LOG_THROW(renamingPair != renaming.end(), storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Boolean variable '" << variable.getName() << " was not renamed.");
- booleanVariables.push_back(storm::prism::BooleanVariable(manager->getVariable(renamingPair->second), variable.getInitialValueExpression().substitute(expressionRenaming), this->getFilename(), get_line(qi::_1)));
+ booleanVariables.push_back(storm::prism::BooleanVariable(manager->getVariable(renamingPair->second), variable.hasInitialValue() ? variable.getInitialValueExpression().substitute(expressionRenaming) : variable.getInitialValueExpression(), this->getFilename(), get_line(qi::_1)));
}
// Rename the integer variables.
@@ -596,7 +596,7 @@ namespace storm {
auto const& renamingPair = renaming.find(variable.getName());
STORM_LOG_THROW(renamingPair != renaming.end(), storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Integer variable '" << variable.getName() << " was not renamed.");
- integerVariables.push_back(storm::prism::IntegerVariable(manager->getVariable(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(manager->getVariable(renamingPair->second), variable.getLowerBoundExpression().substitute(expressionRenaming), variable.getUpperBoundExpression().substitute(expressionRenaming), variable.hasInitialValue() ? variable.getInitialValueExpression().substitute(expressionRenaming) : variable.getInitialValueExpression(), this->getFilename(), get_line(qi::_1)));
}
// Rename commands.
@@ -642,7 +642,11 @@ namespace storm {
}
storm::prism::Program PrismParser::createProgram(GlobalProgramInformation const& globalProgramInformation) const {
- return storm::prism::Program(manager, globalProgramInformation.modelType, globalProgramInformation.constants, globalProgramInformation.globalBooleanVariables, globalProgramInformation.globalIntegerVariables, globalProgramInformation.formulas, globalProgramInformation.modules, globalProgramInformation.actionIndices, globalProgramInformation.rewardModels, globalProgramInformation.labels, secondRun && !globalProgramInformation.hasInitialConstruct ? boost::none : boost::optional<storm::prism::InitialConstruct>(storm::prism::InitialConstruct(manager->boolean(false))), globalProgramInformation.systemCompositionConstruct, this->getFilename(), 1, this->secondRun);
+ return storm::prism::Program(manager, globalProgramInformation.modelType, globalProgramInformation.constants, globalProgramInformation.globalBooleanVariables, globalProgramInformation.globalIntegerVariables, globalProgramInformation.formulas, globalProgramInformation.modules, globalProgramInformation.actionIndices, globalProgramInformation.rewardModels, globalProgramInformation.labels, secondRun && !globalProgramInformation.hasInitialConstruct ? boost::none : boost::make_optional(globalProgramInformation.initialConstruct), globalProgramInformation.systemCompositionConstruct, this->getFilename(), 1, this->secondRun);
+ }
+
+ void PrismParser::removeInitialConstruct(GlobalProgramInformation& globalProgramInformation) const {
+ globalProgramInformation.hasInitialConstruct = false;
}
} // namespace parser
} // namespace storm
diff --git a/src/parser/PrismParser.h b/src/parser/PrismParser.h
index 84a5b601e..2a83e3193 100644
--- a/src/parser/PrismParser.h
+++ b/src/parser/PrismParser.h
@@ -188,7 +188,7 @@ namespace storm {
// Rules for variable definitions.
qi::rule<Iterator, qi::unused_type(std::vector<storm::prism::BooleanVariable>&, std::vector<storm::prism::IntegerVariable>&), Skipper> variableDefinition;
- qi::rule<Iterator, storm::prism::BooleanVariable(), Skipper> booleanVariableDefinition;
+ qi::rule<Iterator, storm::prism::BooleanVariable(), qi::locals<storm::expressions::Expression>, Skipper> booleanVariableDefinition;
qi::rule<Iterator, storm::prism::IntegerVariable(), qi::locals<storm::expressions::Expression>, Skipper> integerVariableDefinition;
// Rules for command definitions.
@@ -241,7 +241,7 @@ namespace storm {
// Helper methods used in the grammar.
bool isValidIdentifier(std::string const& identifier);
- bool addInitialStatesConstruct(storm::expressions::Expression initialStatesExpression, GlobalProgramInformation& globalProgramInformation);
+ bool addInitialStatesConstruct(storm::expressions::Expression const& initialStatesExpression, GlobalProgramInformation& globalProgramInformation);
bool addSystemCompositionConstruct(std::shared_ptr<storm::prism::Composition> const& composition, GlobalProgramInformation& globalProgramInformation);
@@ -274,6 +274,8 @@ namespace storm {
storm::prism::Module createRenamedModule(std::string const& newModuleName, std::string const& oldModuleName, std::map<std::string, std::string> const& renaming, GlobalProgramInformation& globalProgramInformation) const;
storm::prism::Program createProgram(GlobalProgramInformation const& globalProgramInformation) const;
+ void removeInitialConstruct(GlobalProgramInformation& globalProgramInformation) const;
+
// An error handler function.
phoenix::function<SpiritErrorHandler> handler;
};
diff --git a/src/storage/prism/BooleanVariable.cpp b/src/storage/prism/BooleanVariable.cpp
index c38812ec6..422b2266f 100644
--- a/src/storage/prism/BooleanVariable.cpp
+++ b/src/storage/prism/BooleanVariable.cpp
@@ -1,5 +1,7 @@
#include "src/storage/prism/BooleanVariable.h"
+#include "src/storage/expressions/ExpressionManager.h"
+
namespace storm {
namespace prism {
BooleanVariable::BooleanVariable(storm::expressions::Variable const& variable, storm::expressions::Expression const& initialValueExpression, std::string const& filename, uint_fast64_t lineNumber) : Variable(variable, initialValueExpression, false, filename, lineNumber) {
@@ -7,11 +9,21 @@ namespace storm {
}
BooleanVariable BooleanVariable::substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const {
- return BooleanVariable(this->getExpressionVariable(), this->getInitialValueExpression().substitute(substitution), this->getFilename(), this->getLineNumber());
+ return BooleanVariable(this->getExpressionVariable(), this->getInitialValueExpression().isInitialized() ? this->getInitialValueExpression().substitute(substitution) : this->getInitialValueExpression(), this->getFilename(), this->getLineNumber());
+ }
+
+ void BooleanVariable::createMissingInitialValue() {
+ if (!this->hasInitialValue()) {
+ this->setInitialValueExpression(this->getExpressionVariable().getManager().boolean(false));
+ }
}
std::ostream& operator<<(std::ostream& stream, BooleanVariable const& variable) {
- stream << variable.getName() << ": bool init " << variable.getInitialValueExpression() << ";";
+ stream << variable.getName() << ": bool";
+ if (variable.hasInitialValue()) {
+ stream << " init " << variable.getInitialValueExpression();
+ }
+ stream << ";";
return stream;
}
diff --git a/src/storage/prism/BooleanVariable.h b/src/storage/prism/BooleanVariable.h
index 5b43e191c..c5c3ba8e4 100644
--- a/src/storage/prism/BooleanVariable.h
+++ b/src/storage/prism/BooleanVariable.h
@@ -37,6 +37,8 @@ namespace storm {
*/
BooleanVariable substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const;
+ virtual void createMissingInitialValue() override;
+
friend std::ostream& operator<<(std::ostream& stream, BooleanVariable const& variable);
};
diff --git a/src/storage/prism/IntegerVariable.cpp b/src/storage/prism/IntegerVariable.cpp
index b2306ece0..8b60b0e56 100644
--- a/src/storage/prism/IntegerVariable.cpp
+++ b/src/storage/prism/IntegerVariable.cpp
@@ -19,11 +19,21 @@ namespace storm {
}
IntegerVariable IntegerVariable::substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const {
- return IntegerVariable(this->getExpressionVariable(), this->getLowerBoundExpression().substitute(substitution), this->getUpperBoundExpression().substitute(substitution), this->getInitialValueExpression().substitute(substitution), this->getFilename(), this->getLineNumber());
+ return IntegerVariable(this->getExpressionVariable(), this->getLowerBoundExpression().substitute(substitution), this->getUpperBoundExpression().substitute(substitution), this->getInitialValueExpression().isInitialized() ? this->getInitialValueExpression().substitute(substitution) : this->getInitialValueExpression(), this->getFilename(), this->getLineNumber());
+ }
+
+ void IntegerVariable::createMissingInitialValue() {
+ if (!this->hasInitialValue()) {
+ this->setInitialValueExpression(this->getLowerBoundExpression());
+ }
}
std::ostream& operator<<(std::ostream& stream, IntegerVariable const& variable) {
- stream << variable.getName() << ": [" << variable.getLowerBoundExpression() << ".." << variable.getUpperBoundExpression() << "]" << " init " << variable.getInitialValueExpression() << ";";
+ stream << variable.getName() << ": [" << variable.getLowerBoundExpression() << ".." << variable.getUpperBoundExpression() << "]";
+ if (variable.hasInitialValue()) {
+ stream << " init " << variable.getInitialValueExpression();
+ }
+ stream << ";";
return stream;
}
} // namespace prism
diff --git a/src/storage/prism/IntegerVariable.h b/src/storage/prism/IntegerVariable.h
index fc1c6ecf5..335c2ce05 100644
--- a/src/storage/prism/IntegerVariable.h
+++ b/src/storage/prism/IntegerVariable.h
@@ -60,6 +60,8 @@ namespace storm {
*/
IntegerVariable substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const;
+ virtual void createMissingInitialValue() override;
+
friend std::ostream& operator<<(std::ostream& stream, IntegerVariable const& variable);
private:
diff --git a/src/storage/prism/Module.cpp b/src/storage/prism/Module.cpp
index 755c4c78a..095ac3e11 100644
--- a/src/storage/prism/Module.cpp
+++ b/src/storage/prism/Module.cpp
@@ -42,7 +42,7 @@ namespace storm {
std::vector<storm::prism::IntegerVariable> const& Module::getIntegerVariables() const {
return this->integerVariables;
}
-
+
std::set<storm::expressions::Variable> Module::getAllExpressionVariables() const {
std::set<storm::expressions::Variable> result;
for (auto const& var : this->getBooleanVariables()) {
@@ -221,6 +221,15 @@ namespace storm {
return true;
}
+ void Module::createMissingInitialValues() {
+ for (auto& variable : booleanVariables) {
+ variable.createMissingInitialValue();
+ }
+ for (auto& variable : integerVariables) {
+ variable.createMissingInitialValue();
+ }
+ }
+
std::ostream& operator<<(std::ostream& stream, Module const& module) {
stream << "module " << module.getName() << std::endl;
for (auto const& booleanVariable : module.getBooleanVariables()) {
diff --git a/src/storage/prism/Module.h b/src/storage/prism/Module.h
index df8a61c21..c3179b407 100644
--- a/src/storage/prism/Module.h
+++ b/src/storage/prism/Module.h
@@ -225,6 +225,11 @@ namespace storm {
*/
bool containsVariablesOnlyInUpdateProbabilities(std::set<storm::expressions::Variable> const& undefinedConstantVariables) const;
+ /*!
+ * Equips all of the modules' variables without initial values with initial values based on their type.
+ */
+ void createMissingInitialValues();
+
friend std::ostream& operator<<(std::ostream& stream, Module const& module);
private:
diff --git a/src/storage/prism/Program.cpp b/src/storage/prism/Program.cpp
index cdc3d323a..3cf9df8ae 100644
--- a/src/storage/prism/Program.cpp
+++ b/src/storage/prism/Program.cpp
@@ -152,20 +152,26 @@ namespace storm {
if (initialConstruct) {
this->initialConstruct = initialConstruct.get();
} else {
+ // First, add all missing initial values.
+ this->createMissingInitialValues();
+ for (auto& modules : this->modules) {
+ modules.createMissingInitialValues();
+ }
+
// Create a new initial construct if none was given.
storm::expressions::Expression newInitialExpression = manager->boolean(true);
- for (auto const& booleanVariable : this->getGlobalBooleanVariables()) {
+ for (auto& booleanVariable : this->getGlobalBooleanVariables()) {
newInitialExpression = newInitialExpression && storm::expressions::iff(booleanVariable.getExpression(), booleanVariable.getInitialValueExpression());
}
- for (auto const& integerVariable : this->getGlobalIntegerVariables()) {
+ for (auto& integerVariable : this->getGlobalIntegerVariables()) {
newInitialExpression = newInitialExpression && integerVariable.getExpression() == integerVariable.getInitialValueExpression();
}
- for (auto const& module : this->getModules()) {
- for (auto const& booleanVariable : module.getBooleanVariables()) {
+ for (auto& module : this->getModules()) {
+ for (auto& booleanVariable : module.getBooleanVariables()) {
newInitialExpression = newInitialExpression && storm::expressions::iff(booleanVariable.getExpression(), booleanVariable.getInitialValueExpression());
}
- for (auto const& integerVariable : module.getIntegerVariables()) {
+ for (auto& integerVariable : module.getIntegerVariables()) {
newInitialExpression = newInitialExpression && integerVariable.getExpression() == integerVariable.getInitialValueExpression();
}
}
@@ -241,13 +247,17 @@ namespace storm {
// Now check initial value expressions of global variables.
for (auto const& booleanVariable : this->getGlobalBooleanVariables()) {
- if (booleanVariable.getInitialValueExpression().containsVariable(undefinedConstantVariables)) {
- return false;
+ if (booleanVariable.hasInitialValue()) {
+ if (booleanVariable.getInitialValueExpression().containsVariable(undefinedConstantVariables)) {
+ return false;
+ }
}
}
for (auto const& integerVariable : this->getGlobalIntegerVariables()) {
- if (integerVariable.getInitialValueExpression().containsVariable(undefinedConstantVariables)) {
- return false;
+ if (integerVariable.hasInitialValue()) {
+ if (integerVariable.getInitialValueExpression().containsVariable(undefinedConstantVariables)) {
+ return false;
+ }
}
if (integerVariable.getLowerBoundExpression().containsVariable(undefinedConstantVariables)) {
return false;
@@ -809,18 +819,20 @@ namespace storm {
// Now we check the variable declarations. We start with the global variables.
std::set<storm::expressions::Variable> variables;
for (auto const& variable : this->getGlobalBooleanVariables()) {
- // Check the initial value of the variable.
- std::set<storm::expressions::Variable> containedVariables = variable.getInitialValueExpression().getVariables();
- std::set<storm::expressions::Variable> illegalVariables;
- std::set_difference(containedVariables.begin(), containedVariables.end(), constants.begin(), constants.end(), std::inserter(illegalVariables, illegalVariables.begin()));
- bool isValid = illegalVariables.empty();
-
- if (!isValid) {
- std::vector<std::string> illegalVariableNames;
- for (auto const& var : illegalVariables) {
- illegalVariableNames.push_back(var.getName());
+ if (variable.hasInitialValue()) {
+ // Check the initial value of the variable.
+ std::set<storm::expressions::Variable> containedVariables = variable.getInitialValueExpression().getVariables();
+ std::set<storm::expressions::Variable> illegalVariables;
+ std::set_difference(containedVariables.begin(), containedVariables.end(), constants.begin(), constants.end(), std::inserter(illegalVariables, illegalVariables.begin()));
+ bool isValid = illegalVariables.empty();
+
+ if (!isValid) {
+ std::vector<std::string> illegalVariableNames;
+ for (auto const& var : illegalVariables) {
+ illegalVariableNames.push_back(var.getName());
+ }
+ STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": initial value expression refers to unknown constants: " << boost::algorithm::join(illegalVariableNames, ",") << ".");
}
- STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": initial value expression refers to unknown constants: " << boost::algorithm::join(illegalVariableNames, ",") << ".");
}
// Record the new identifier for future checks.
@@ -855,16 +867,18 @@ namespace storm {
STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": upper bound expression refers to unknown constants: " << boost::algorithm::join(illegalVariableNames, ",") << ".");
}
- // Check the initial value of the variable.
- containedVariables = variable.getInitialValueExpression().getVariables();
- std::set_difference(containedVariables.begin(), containedVariables.end(), constants.begin(), constants.end(), std::inserter(illegalVariables, illegalVariables.begin()));
- isValid = illegalVariables.empty();
- if (!isValid) {
- std::vector<std::string> illegalVariableNames;
- for (auto const& var : illegalVariables) {
- illegalVariableNames.push_back(var.getName());
+ if (variable.hasInitialValue()) {
+ // Check the initial value of the variable.
+ containedVariables = variable.getInitialValueExpression().getVariables();
+ std::set_difference(containedVariables.begin(), containedVariables.end(), constants.begin(), constants.end(), std::inserter(illegalVariables, illegalVariables.begin()));
+ isValid = illegalVariables.empty();
+ if (!isValid) {
+ std::vector<std::string> illegalVariableNames;
+ for (auto const& var : illegalVariables) {
+ illegalVariableNames.push_back(var.getName());
+ }
+ STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": initial value expression refers to unknown constants: " << boost::algorithm::join(illegalVariableNames, ",") << ".");
}
- STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": initial value expression refers to unknown constants: " << boost::algorithm::join(illegalVariableNames, ",") << ".");
}
// Record the new identifier for future checks.
@@ -877,17 +891,19 @@ namespace storm {
// Now go through the variables of the modules.
for (auto const& module : this->getModules()) {
for (auto const& variable : module.getBooleanVariables()) {
- // Check the initial value of the variable.
- std::set<storm::expressions::Variable> containedVariables = variable.getInitialValueExpression().getVariables();
- std::set<storm::expressions::Variable> illegalVariables;
- std::set_difference(containedVariables.begin(), containedVariables.end(), constants.begin(), constants.end(), std::inserter(illegalVariables, illegalVariables.begin()));
- bool isValid = illegalVariables.empty();
- if (!isValid) {
- std::vector<std::string> illegalVariableNames;
- for (auto const& var : illegalVariables) {
- illegalVariableNames.push_back(var.getName());
+ if (variable.hasInitialValue()) {
+ // Check the initial value of the variable.
+ std::set<storm::expressions::Variable> containedVariables = variable.getInitialValueExpression().getVariables();
+ std::set<storm::expressions::Variable> illegalVariables;
+ std::set_difference(containedVariables.begin(), containedVariables.end(), constants.begin(), constants.end(), std::inserter(illegalVariables, illegalVariables.begin()));
+ bool isValid = illegalVariables.empty();
+ if (!isValid) {
+ std::vector<std::string> illegalVariableNames;
+ for (auto const& var : illegalVariables) {
+ illegalVariableNames.push_back(var.getName());
+ }
+ STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": initial value expression refers to unknown constants: " << boost::algorithm::join(illegalVariableNames, ",") << ".");
}
- STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": initial value expression refers to unknown constants: " << boost::algorithm::join(illegalVariableNames, ",") << ".");
}
// Record the new identifier for future checks.
@@ -920,17 +936,19 @@ namespace storm {
STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": upper bound expression refers to unknown constants: " << boost::algorithm::join(illegalVariableNames, ",") << ".");
}
- // Check the initial value of the variable.
- containedVariables = variable.getInitialValueExpression().getVariables();
- illegalVariables.clear();
- std::set_difference(containedVariables.begin(), containedVariables.end(), constants.begin(), constants.end(), std::inserter(illegalVariables, illegalVariables.begin()));
- isValid = illegalVariables.empty();
- if (!isValid) {
- std::vector<std::string> illegalVariableNames;
- for (auto const& var : illegalVariables) {
- illegalVariableNames.push_back(var.getName());
+ if (variable.hasInitialValue()) {
+ // Check the initial value of the variable.
+ containedVariables = variable.getInitialValueExpression().getVariables();
+ illegalVariables.clear();
+ std::set_difference(containedVariables.begin(), containedVariables.end(), constants.begin(), constants.end(), std::inserter(illegalVariables, illegalVariables.begin()));
+ isValid = illegalVariables.empty();
+ if (!isValid) {
+ std::vector<std::string> illegalVariableNames;
+ for (auto const& var : illegalVariables) {
+ illegalVariableNames.push_back(var.getName());
+ }
+ STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": initial value expression refers to unknown constants: " << boost::algorithm::join(illegalVariableNames, ",") << ".");
}
- STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": initial value expression refers to unknown constants: " << boost::algorithm::join(illegalVariableNames, ",") << ".");
}
// Record the new identifier for future checks.
@@ -1571,7 +1589,7 @@ namespace storm {
}
storm::jani::Model janiModel("jani_from_prism", modelType, 1, manager);
storm::expressions::Expression globalInitialStatesExpression;
-
+
// Add all constants of the PRISM program to the JANI model.
for (auto const& constant : constants) {
janiModel.addConstant(storm::jani::Constant(constant.getName(), constant.getExpressionVariable(), constant.isDefined() ? boost::optional<storm::expressions::Expression>(constant.getExpression()) : boost::none));
@@ -1580,13 +1598,17 @@ namespace storm {
// Add all global variables of the PRISM program to the JANI model.
for (auto const& variable : globalIntegerVariables) {
janiModel.addBoundedIntegerVariable(storm::jani::BoundedIntegerVariable(variable.getName(), variable.getExpressionVariable(), variable.getLowerBoundExpression(), variable.getUpperBoundExpression()));
- storm::expressions::Expression variableInitialExpression = variable.getExpressionVariable() == variable.getInitialValueExpression();
- globalInitialStatesExpression = globalInitialStatesExpression.isInitialized() ? globalInitialStatesExpression && variableInitialExpression : variableInitialExpression;
+ if (variable.hasInitialValue()) {
+ storm::expressions::Expression variableInitialExpression = variable.getExpressionVariable() == variable.getInitialValueExpression();
+ globalInitialStatesExpression = globalInitialStatesExpression.isInitialized() ? globalInitialStatesExpression && variableInitialExpression : variableInitialExpression;
+ }
}
for (auto const& variable : globalBooleanVariables) {
janiModel.addBooleanVariable(storm::jani::BooleanVariable(variable.getName(), variable.getExpressionVariable()));
- storm::expressions::Expression variableInitialExpression = storm::expressions::iff(variable.getExpressionVariable(), variable.getInitialValueExpression());
- globalInitialStatesExpression = globalInitialStatesExpression.isInitialized() ? globalInitialStatesExpression && variableInitialExpression : variableInitialExpression;
+ if (variable.hasInitialValue()) {
+ storm::expressions::Expression variableInitialExpression = storm::expressions::iff(variable.getExpressionVariable(), variable.getInitialValueExpression());
+ globalInitialStatesExpression = globalInitialStatesExpression.isInitialized() ? globalInitialStatesExpression && variableInitialExpression : variableInitialExpression;
+ }
}
// Add all actions of the PRISM program to the JANI model.
@@ -1598,7 +1620,7 @@ namespace storm {
}
// Because of the rules of JANI, we have to make all variables of modules global that are read by other modules.
-
+
// Create a mapping from variables to the indices of module indices that write/read the variable.
std::map<storm::expressions::Variable, std::set<uint_fast64_t>> variablesToAccessingModuleIndices;
for (uint_fast64_t index = 0; index < modules.size(); ++index) {
@@ -1627,20 +1649,24 @@ namespace storm {
for (auto const& module : modules) {
storm::jani::Automaton automaton(module.getName());
storm::expressions::Expression initialStatesExpression;
-
+
for (auto const& variable : module.getIntegerVariables()) {
storm::jani::BoundedIntegerVariable newIntegerVariable(variable.getName(), variable.getExpressionVariable(), variable.getLowerBoundExpression(), variable.getUpperBoundExpression());
std::set<uint_fast64_t> const& accessingModuleIndices = variablesToAccessingModuleIndices[variable.getExpressionVariable()];
// If there is exactly one module reading and writing the variable, we can make the variable local to this module.
if (!allVariablesGlobal && accessingModuleIndices.size() == 1) {
automaton.addBoundedIntegerVariable(newIntegerVariable);
- storm::expressions::Expression variableInitialExpression = variable.getExpressionVariable() == variable.getInitialValueExpression();
- initialStatesExpression = initialStatesExpression.isInitialized() ? initialStatesExpression && variableInitialExpression : variableInitialExpression;
+ if (variable.hasInitialValue()) {
+ storm::expressions::Expression variableInitialExpression = variable.getExpressionVariable() == variable.getInitialValueExpression();
+ initialStatesExpression = initialStatesExpression.isInitialized() ? initialStatesExpression && variableInitialExpression : variableInitialExpression;
+ }
} else if (!accessingModuleIndices.empty()) {
// Otherwise, we need to make it global.
janiModel.addBoundedIntegerVariable(newIntegerVariable);
- storm::expressions::Expression variableInitialExpression = variable.getExpressionVariable() == variable.getInitialValueExpression();
- globalInitialStatesExpression = globalInitialStatesExpression.isInitialized() ? globalInitialStatesExpression && variableInitialExpression : variableInitialExpression;
+ if (variable.hasInitialValue()) {
+ storm::expressions::Expression variableInitialExpression = variable.getExpressionVariable() == variable.getInitialValueExpression();
+ globalInitialStatesExpression = globalInitialStatesExpression.isInitialized() ? globalInitialStatesExpression && variableInitialExpression : variableInitialExpression;
+ }
}
}
for (auto const& variable : module.getBooleanVariables()) {
@@ -1649,13 +1675,17 @@ namespace storm {
// If there is exactly one module reading and writing the variable, we can make the variable local to this module.
if (!allVariablesGlobal && accessingModuleIndices.size() == 1) {
automaton.addBooleanVariable(newBooleanVariable);
- storm::expressions::Expression variableInitialExpression = storm::expressions::iff(variable.getExpressionVariable(), variable.getInitialValueExpression());
- initialStatesExpression = initialStatesExpression.isInitialized() ? initialStatesExpression && variableInitialExpression : variableInitialExpression;
+ if (variable.hasInitialValue()) {
+ storm::expressions::Expression variableInitialExpression = storm::expressions::iff(variable.getExpressionVariable(), variable.getInitialValueExpression());
+ initialStatesExpression = initialStatesExpression.isInitialized() ? initialStatesExpression && variableInitialExpression : variableInitialExpression;
+ }
} else if (!accessingModuleIndices.empty()) {
// Otherwise, we need to make it global.
janiModel.addBooleanVariable(newBooleanVariable);
- storm::expressions::Expression variableInitialExpression = storm::expressions::iff(variable.getExpressionVariable(), variable.getInitialValueExpression());
- globalInitialStatesExpression = globalInitialStatesExpression.isInitialized() ? globalInitialStatesExpression && variableInitialExpression : variableInitialExpression;
+ if (variable.hasInitialValue()) {
+ storm::expressions::Expression variableInitialExpression = storm::expressions::iff(variable.getExpressionVariable(), variable.getInitialValueExpression());
+ globalInitialStatesExpression = globalInitialStatesExpression.isInitialized() ? globalInitialStatesExpression && variableInitialExpression : variableInitialExpression;
+ }
}
}
@@ -1713,6 +1743,19 @@ namespace storm {
return janiModel;
}
+ void Program::createMissingInitialValues() {
+ for (auto& variable : globalBooleanVariables) {
+ if (!variable.hasInitialValue()) {
+ variable.setInitialValueExpression(manager->boolean(false));
+ }
+ }
+ for (auto& variable : globalIntegerVariables) {
+ if (!variable.hasInitialValue()) {
+ variable.setInitialValueExpression(variable.getLowerBoundExpression());
+ }
+ }
+ }
+
std::ostream& operator<<(std::ostream& out, Program::ModelType const& type) {
switch (type) {
case Program::ModelType::UNDEFINED: out << "undefined"; break;
diff --git a/src/storage/prism/Program.h b/src/storage/prism/Program.h
index 8c30079e0..50bd84603 100644
--- a/src/storage/prism/Program.h
+++ b/src/storage/prism/Program.h
@@ -175,7 +175,7 @@ namespace storm {
* @return The global boolean variables of the program.
*/
std::vector<BooleanVariable> const& getGlobalBooleanVariables() const;
-
+
/*!
* Retrieves a the global boolean variable with the given name.
*
@@ -587,6 +587,11 @@ namespace storm {
*/
Command synchronizeCommands(uint_fast64_t newCommandIndex, uint_fast64_t actionIndex, uint_fast64_t firstUpdateIndex, std::string const& actionName, std::vector<std::reference_wrapper<Command const>> const& commands) const;
+ /*!
+ * Equips all global variables without initial values with initial values based on their type.
+ */
+ void createMissingInitialValues();
+
// The manager responsible for the variables/expressions of the program.
std::shared_ptr<storm::expressions::ExpressionManager> manager;
diff --git a/src/storage/prism/Variable.cpp b/src/storage/prism/Variable.cpp
index 7d347bcec..cda8317a5 100644
--- a/src/storage/prism/Variable.cpp
+++ b/src/storage/prism/Variable.cpp
@@ -5,11 +5,11 @@
namespace storm {
namespace prism {
- Variable::Variable(storm::expressions::Variable const& variable, storm::expressions::Expression const& initialValueExpression, bool defaultInitialValue, std::string const& filename, uint_fast64_t lineNumber) : LocatedInformation(filename, lineNumber), variable(variable), initialValueExpression(initialValueExpression), defaultInitialValue(defaultInitialValue) {
+ Variable::Variable(storm::expressions::Variable const& variable, storm::expressions::Expression const& initialValueExpression, bool defaultInitialValue, std::string const& filename, uint_fast64_t lineNumber) : LocatedInformation(filename, lineNumber), variable(variable), initialValueExpression(initialValueExpression) {
// Nothing to do here.
}
- Variable::Variable(storm::expressions::ExpressionManager& manager, Variable const& oldVariable, std::string const& newName, std::map<storm::expressions::Variable, storm::expressions::Expression> const& renaming, std::string const& filename, uint_fast64_t lineNumber) : LocatedInformation(filename, lineNumber), variable(manager.declareVariable(newName, oldVariable.variable.getType())), initialValueExpression(oldVariable.getInitialValueExpression().substitute(renaming)), defaultInitialValue(oldVariable.hasDefaultInitialValue()) {
+ Variable::Variable(storm::expressions::ExpressionManager& manager, Variable const& oldVariable, std::string const& newName, std::map<storm::expressions::Variable, storm::expressions::Expression> const& renaming, std::string const& filename, uint_fast64_t lineNumber) : LocatedInformation(filename, lineNumber), variable(manager.declareVariable(newName, oldVariable.variable.getType())), initialValueExpression(oldVariable.getInitialValueExpression().substitute(renaming)) {
// Intentionally left empty.
}
@@ -17,14 +17,18 @@ namespace storm {
return this->variable.getName();
}
- bool Variable::hasDefaultInitialValue() const {
- return this->defaultInitialValue;
+ bool Variable::hasInitialValue() const {
+ return this->initialValueExpression.isInitialized();
}
storm::expressions::Expression const& Variable::getInitialValueExpression() const {
return this->initialValueExpression;
}
+ void Variable::setInitialValueExpression(storm::expressions::Expression const& initialValueExpression) {
+ this->initialValueExpression = initialValueExpression;
+ }
+
storm::expressions::Variable const& Variable::getExpressionVariable() const {
return this->variable;
}
diff --git a/src/storage/prism/Variable.h b/src/storage/prism/Variable.h
index 3a19c2b75..40f47eb27 100644
--- a/src/storage/prism/Variable.h
+++ b/src/storage/prism/Variable.h
@@ -28,19 +28,27 @@ namespace storm {
std::string const& getName() const;
/*!
- * Retrieves the expression defining the initial value of the variable.
+ * Retrieves whether the variable has an initial value.
+ *
+ * @return True iff the variable has an initial value.
+ */
+ bool hasInitialValue() const;
+
+ /*!
+ * Retrieves the expression defining the initial value of the variable. This can only be called if there is
+ * an initial value (expression).
*
* @return The expression defining the initial value of the variable.
*/
storm::expressions::Expression const& getInitialValueExpression() const;
-
+
/*!
- * Retrieves whether the variable has the default initial value with respect to its type.
+ * Sets the expression defining the initial value of the variable.
*
- * @return True iff the variable has the default initial value.
+ * @param initialValueExpression The expression defining the initial value of the variable.
*/
- bool hasDefaultInitialValue() const;
-
+ void setInitialValueExpression(storm::expressions::Expression const& initialValueExpression);
+
/*!
* Retrieves the expression variable associated with this variable.
*
@@ -55,6 +63,10 @@ namespace storm {
*/
storm::expressions::Expression getExpression() const;
+ /*!
+ * Equips the variable with an initial value based on its type if not initial value is present.
+ */
+ virtual void createMissingInitialValue() = 0;
// Make the constructors protected to forbid instantiation of this class.
protected:
@@ -90,9 +102,6 @@ namespace storm {
// The constant expression defining the initial value of the variable.
storm::expressions::Expression initialValueExpression;
-
- // A flag that stores whether the variable has its default initial expression.
- bool defaultInitialValue;
};
} // namespace prism