diff --git a/resources/3rdparty/CMakeLists.txt b/resources/3rdparty/CMakeLists.txt
index 64fc5d7b3..8c013f86f 100644
--- a/resources/3rdparty/CMakeLists.txt
+++ b/resources/3rdparty/CMakeLists.txt
@@ -201,7 +201,7 @@ if(USE_CARL)
message("START CARL CONFIG PROCESS")
file(MAKE_DIRECTORY ${STORM_3RDPARTY_BINARY_DIR}/carl_download)
execute_process(
- COMMAND ${CMAKE_COMMAND} ${STORM_3RDPARTY_SOURCE_DIR}/carl "-DSTORM_3RDPARTY_BINARY_DIR=${STORM_3RDPARTY_BINARY_DIR}"
+ COMMAND ${CMAKE_COMMAND} ${STORM_3RDPARTY_SOURCE_DIR}/carl "-DSTORM_3RDPARTY_BINARY_DIR=${STORM_3RDPARTY_BINARY_DIR}" "-DBoost_LIBRARY_DIRS=${Boost_LIBRARY_DIRS}" "-DBoost_INCLUDE_DIRS=${Boost_INCLUDE_DIRS}"
WORKING_DIRECTORY ${STORM_3RDPARTY_BINARY_DIR}/carl_download
OUTPUT_VARIABLE carlconfig_out
RESULT_VARIABLE carlconfig_result)
diff --git a/src/storm/storage/expressions/BaseExpression.cpp b/src/storm/storage/expressions/BaseExpression.cpp
index 7780351eb..4e07fd089 100644
--- a/src/storm/storage/expressions/BaseExpression.cpp
+++ b/src/storm/storage/expressions/BaseExpression.cpp
@@ -5,6 +5,7 @@
#include "storm/exceptions/InvalidAccessException.h"
#include "storm/storage/expressions/Expressions.h"
+#include "storm/storage/expressions/ToRationalNumberVisitor.h"
namespace storm {
namespace expressions {
@@ -51,7 +52,12 @@ namespace storm {
double BaseExpression::evaluateAsDouble(Valuation const*) const {
STORM_LOG_THROW(false, storm::exceptions::InvalidTypeException, "Unable to evaluate expression as double.");
}
-
+
+ storm::RationalNumber BaseExpression::evaluateAsRational() const {
+ ToRationalNumberVisitor<storm::RationalNumber> v;
+ return v.toRationalNumber(this->toExpression());
+ }
+
uint_fast64_t BaseExpression::getArity() const {
return 0;
}
diff --git a/src/storm/storage/expressions/BaseExpression.h b/src/storm/storage/expressions/BaseExpression.h
index 325aa33d4..83c76f7ae 100644
--- a/src/storm/storage/expressions/BaseExpression.h
+++ b/src/storm/storage/expressions/BaseExpression.h
@@ -7,6 +7,7 @@
#include <map>
#include <iostream>
+#include "storm/adapters/NumberAdapter.h"
#include "storm/storage/expressions/Type.h"
#include "storm/utility/OsDetection.h"
#include <boost/any.hpp>
@@ -90,6 +91,15 @@ namespace storm {
*/
virtual double evaluateAsDouble(Valuation const* valuation = nullptr) const;
+ /*!
+ * Evaluates the expression and returns the resulting rational number.
+ * If the return type of the expression is not a rational number
+ * or the expression could not be evaluated, an exception is thrown.
+ *
+ * @return The rational number value of the expression.
+ */
+ virtual storm::RationalNumber evaluateAsRational() const;
+
/*!
* Returns the arity of the expression.
*
diff --git a/src/storm/storage/expressions/BinaryNumericalFunctionExpression.cpp b/src/storm/storage/expressions/BinaryNumericalFunctionExpression.cpp
index 1c0a7908e..3d2e09153 100644
--- a/src/storm/storage/expressions/BinaryNumericalFunctionExpression.cpp
+++ b/src/storm/storage/expressions/BinaryNumericalFunctionExpression.cpp
@@ -1,6 +1,7 @@
#include <algorithm>
#include <cmath>
+#include "storm/adapters/NumberAdapter.h"
#include "storm/storage/expressions/BinaryNumericalFunctionExpression.h"
#include "storm/storage/expressions/IntegerLiteralExpression.h"
#include "storm/storage/expressions/RationalLiteralExpression.h"
@@ -90,16 +91,21 @@ namespace storm {
}
return std::shared_ptr<BaseExpression>(new IntegerLiteralExpression(this->getManager(), newValue));
} else if (this->hasRationalType()) {
- double firstOperandEvaluation = firstOperandSimplified->evaluateAsDouble();
- double secondOperandEvaluation = secondOperandSimplified->evaluateAsDouble();
- double newValue = 0;
+ storm::RationalNumber firstOperandEvaluation = firstOperandSimplified->evaluateAsRational();
+ storm::RationalNumber secondOperandEvaluation = secondOperandSimplified->evaluateAsRational();
+ storm::RationalNumber newValue = 0;
switch (this->getOperatorType()) {
case OperatorType::Plus: newValue = firstOperandEvaluation + secondOperandEvaluation; break;
case OperatorType::Minus: newValue = firstOperandEvaluation - secondOperandEvaluation; break;
case OperatorType::Times: newValue = firstOperandEvaluation * secondOperandEvaluation; break;
case OperatorType::Min: newValue = std::min(firstOperandEvaluation, secondOperandEvaluation); break;
case OperatorType::Max: newValue = std::max(firstOperandEvaluation, secondOperandEvaluation); break;
- case OperatorType::Power: newValue = static_cast<int_fast64_t>(std::pow(firstOperandEvaluation, secondOperandEvaluation)); break;
+ case OperatorType::Power: {
+ STORM_LOG_THROW(carl::isInteger(secondOperandEvaluation), storm::exceptions::InvalidStateException, "Can not simplify pow() with fractional exponent.");
+ std::size_t exponent = carl::toInt<carl::uint>(secondOperandEvaluation);
+ newValue = carl::pow(firstOperandEvaluation, exponent);
+ break;
+ }
case OperatorType::Divide: STORM_LOG_THROW(false, storm::exceptions::InvalidStateException, "Unable to simplify division."); break;
}
return std::shared_ptr<BaseExpression>(new RationalLiteralExpression(this->getManager(), newValue));
diff --git a/src/storm/storage/expressions/BinaryRelationExpression.cpp b/src/storm/storage/expressions/BinaryRelationExpression.cpp
index 7602fbf3c..a610802e8 100644
--- a/src/storm/storage/expressions/BinaryRelationExpression.cpp
+++ b/src/storm/storage/expressions/BinaryRelationExpression.cpp
@@ -4,6 +4,7 @@
#include "storm/storage/expressions/BooleanLiteralExpression.h"
#include "storm/utility/macros.h"
+#include "storm/utility/constants.h"
#include "storm/exceptions/InvalidTypeException.h"
#include "storm/storage/expressions/ExpressionVisitor.h"
@@ -48,28 +49,28 @@ namespace storm {
std::shared_ptr<BaseExpression const> secondOperandSimplified = this->getSecondOperand()->simplify();
if (firstOperandSimplified->isLiteral() && secondOperandSimplified->isLiteral()) {
- boost::variant<int_fast64_t, double> firstOperandEvaluation;
- boost::variant<int_fast64_t, double> secondOperandEvaluation;
-
+ storm::RationalNumber firstOperandEvaluation;
+ storm::RationalNumber secondOperandEvaluation;
+
if (firstOperandSimplified->hasIntegerType()) {
- firstOperandEvaluation = firstOperandSimplified->evaluateAsInt();
+ firstOperandEvaluation = storm::utility::convertNumber<storm::RationalNumber>(firstOperandSimplified->evaluateAsInt());
} else {
- firstOperandEvaluation = firstOperandSimplified->evaluateAsDouble();
+ firstOperandEvaluation = firstOperandSimplified->evaluateAsRational();
}
if (secondOperandSimplified->hasIntegerType()) {
- secondOperandEvaluation = secondOperandSimplified->evaluateAsInt();
+ secondOperandEvaluation = storm::utility::convertNumber<storm::RationalNumber>(secondOperandSimplified->evaluateAsInt());
} else {
- secondOperandEvaluation = secondOperandSimplified->evaluateAsDouble();
+ secondOperandEvaluation = secondOperandSimplified->evaluateAsRational();
}
-
+
bool truthValue = false;
switch (this->getRelationType()) {
- case RelationType::Equal: truthValue = (firstOperandSimplified->hasIntegerType() ? boost::get<int_fast64_t>(firstOperandEvaluation) : boost::get<double>(firstOperandEvaluation)) == (secondOperandSimplified->hasIntegerType() ? boost::get<int_fast64_t>(secondOperandEvaluation) : boost::get<double>(secondOperandEvaluation)); break;
- case RelationType::NotEqual: truthValue = (firstOperandSimplified->hasIntegerType() ? boost::get<int_fast64_t>(firstOperandEvaluation) : boost::get<double>(firstOperandEvaluation)) != (secondOperandSimplified->hasIntegerType() ? boost::get<int_fast64_t>(secondOperandEvaluation) : boost::get<double>(secondOperandEvaluation)); break;
- case RelationType::Greater: truthValue = (firstOperandSimplified->hasIntegerType() ? boost::get<int_fast64_t>(firstOperandEvaluation) : boost::get<double>(firstOperandEvaluation)) > (secondOperandSimplified->hasIntegerType() ? boost::get<int_fast64_t>(secondOperandEvaluation) : boost::get<double>(secondOperandEvaluation)); break;
- case RelationType::GreaterOrEqual: truthValue = (firstOperandSimplified->hasIntegerType() ? boost::get<int_fast64_t>(firstOperandEvaluation) : boost::get<double>(firstOperandEvaluation)) >= (secondOperandSimplified->hasIntegerType() ? boost::get<int_fast64_t>(secondOperandEvaluation) : boost::get<double>(secondOperandEvaluation)); break;
- case RelationType::Less: truthValue = (firstOperandSimplified->hasIntegerType() ? boost::get<int_fast64_t>(firstOperandEvaluation) : boost::get<double>(firstOperandEvaluation)) < (secondOperandSimplified->hasIntegerType() ? boost::get<int_fast64_t>(secondOperandEvaluation) : boost::get<double>(secondOperandEvaluation)); break;
- case RelationType::LessOrEqual: truthValue = (firstOperandSimplified->hasIntegerType() ? boost::get<int_fast64_t>(firstOperandEvaluation) : boost::get<double>(firstOperandEvaluation)) <= (secondOperandSimplified->hasIntegerType() ? boost::get<int_fast64_t>(secondOperandEvaluation) : boost::get<double>(secondOperandEvaluation)); break;
+ case RelationType::Equal: truthValue = firstOperandEvaluation == secondOperandEvaluation; break;
+ case RelationType::NotEqual: truthValue = firstOperandEvaluation != secondOperandEvaluation; break;
+ case RelationType::Greater: truthValue = firstOperandEvaluation > secondOperandEvaluation; break;
+ case RelationType::GreaterOrEqual: truthValue = firstOperandEvaluation >= secondOperandEvaluation; break;
+ case RelationType::Less: truthValue = firstOperandEvaluation < secondOperandEvaluation; break;
+ case RelationType::LessOrEqual: truthValue = firstOperandEvaluation <= secondOperandEvaluation; break;
}
return std::shared_ptr<BaseExpression>(new BooleanLiteralExpression(this->getManager(), truthValue));
}
diff --git a/src/storm/storage/expressions/ToRationalNumberVisitor.cpp b/src/storm/storage/expressions/ToRationalNumberVisitor.cpp
index 26ad15b5a..c8931c7f3 100644
--- a/src/storm/storage/expressions/ToRationalNumberVisitor.cpp
+++ b/src/storm/storage/expressions/ToRationalNumberVisitor.cpp
@@ -7,6 +7,11 @@
namespace storm {
namespace expressions {
+ template<typename RationalNumberType>
+ ToRationalNumberVisitor<RationalNumberType>::ToRationalNumberVisitor() : ExpressionVisitor() {
+ // Intentionally left empty.
+ }
+
template<typename RationalNumberType>
ToRationalNumberVisitor<RationalNumberType>::ToRationalNumberVisitor(ExpressionEvaluatorBase<RationalNumberType> const& evaluator) : ExpressionVisitor(), evaluator(evaluator) {
// Intentionally left empty.
@@ -19,7 +24,13 @@ namespace storm {
template<typename RationalNumberType>
boost::any ToRationalNumberVisitor<RationalNumberType>::visit(IfThenElseExpression const& expression, boost::any const& data) {
- bool conditionValue = evaluator.asBool(expression.getCondition());
+ bool conditionValue;
+ if (evaluator) {
+ conditionValue = evaluator->asBool(expression.getCondition());
+ } else {
+ // no evaluator, fall back to evaluateBool
+ conditionValue = expression.getCondition()->evaluateAsBool();
+ }
if (conditionValue) {
return expression.getThenExpression()->accept(*this, data);
} else {
diff --git a/src/storm/storage/expressions/ToRationalNumberVisitor.h b/src/storm/storage/expressions/ToRationalNumberVisitor.h
index 89cb9f81f..1f2b88f48 100644
--- a/src/storm/storage/expressions/ToRationalNumberVisitor.h
+++ b/src/storm/storage/expressions/ToRationalNumberVisitor.h
@@ -2,6 +2,8 @@
#include <unordered_map>
+#include <boost/optional.hpp>
+
#include "storm/adapters/CarlAdapter.h"
#include "storm/storage/expressions/Expression.h"
@@ -16,7 +18,8 @@ namespace storm {
template<typename RationalNumberType>
class ToRationalNumberVisitor : public ExpressionVisitor {
public:
- ToRationalNumberVisitor(ExpressionEvaluatorBase<RationalNumberType> const& evaluator);
+ ToRationalNumberVisitor();
+ ToRationalNumberVisitor(ExpressionEvaluatorBase<RationalNumberType> const& evaluator);
RationalNumberType toRationalNumber(Expression const& expression);
@@ -36,8 +39,8 @@ namespace storm {
private:
std::unordered_map<storm::expressions::Variable, RationalNumberType> valueMapping;
- // A reference to an expression evaluator (mainly for resolving the boolean condition in IfThenElse expressions)
- ExpressionEvaluatorBase<RationalNumberType> const& evaluator;
+ // An optional reference to an expression evaluator (mainly for resolving the boolean condition in IfThenElse expressions)
+ boost::optional<ExpressionEvaluatorBase<RationalNumberType> const&> evaluator;
};
}
}
diff --git a/src/storm/storage/expressions/UnaryNumericalFunctionExpression.cpp b/src/storm/storage/expressions/UnaryNumericalFunctionExpression.cpp
index 2382e1399..9fc2c5639 100644
--- a/src/storm/storage/expressions/UnaryNumericalFunctionExpression.cpp
+++ b/src/storm/storage/expressions/UnaryNumericalFunctionExpression.cpp
@@ -2,11 +2,13 @@
#include <boost/variant.hpp>
+#include "storm/adapters/NumberAdapter.h"
#include "storm/storage/expressions/UnaryNumericalFunctionExpression.h"
#include "storm/storage/expressions/IntegerLiteralExpression.h"
#include "storm/storage/expressions/RationalLiteralExpression.h"
#include "ExpressionVisitor.h"
#include "storm/utility/macros.h"
+#include "storm/utility/constants.h"
#include "storm/exceptions/InvalidTypeException.h"
#include "storm/exceptions/InvalidOperationException.h"
@@ -65,14 +67,13 @@ namespace storm {
std::shared_ptr<BaseExpression const> operandSimplified = this->getOperand()->simplify();
if (operandSimplified->isLiteral()) {
- boost::variant<int_fast64_t, double> operandEvaluation;
+ boost::variant<int_fast64_t, storm::RationalNumber> operandEvaluation;
if (operandSimplified->hasIntegerType()) {
operandEvaluation = operandSimplified->evaluateAsInt();
} else {
- operandEvaluation = operandSimplified->evaluateAsDouble();
+ operandEvaluation = operandSimplified->evaluateAsRational();
}
- boost::variant<int_fast64_t, double> result;
if (operandSimplified->hasIntegerType()) {
int_fast64_t value = 0;
switch (this->getOperatorType()) {
@@ -82,11 +83,11 @@ namespace storm {
}
return std::shared_ptr<BaseExpression>(new IntegerLiteralExpression(this->getManager(), value));
} else {
- double value = 0;
+ storm::RationalNumber value = storm::utility::zero<storm::RationalNumber>();
switch (this->getOperatorType()) {
- case OperatorType::Minus: value = -boost::get<double>(operandEvaluation); break;
- case OperatorType::Floor: value = std::floor(boost::get<double>(operandEvaluation)); break;
- case OperatorType::Ceil: value = std::ceil(boost::get<double>(operandEvaluation)); break;
+ case OperatorType::Minus: value = -boost::get<storm::RationalNumber>(operandEvaluation); break;
+ case OperatorType::Floor: value = carl::floor(boost::get<storm::RationalNumber>(operandEvaluation)); break;
+ case OperatorType::Ceil: value = carl::ceil(boost::get<storm::RationalNumber>(operandEvaluation)); break;
}
return std::shared_ptr<BaseExpression>(new RationalLiteralExpression(this->getManager(), value));
}
diff --git a/src/storm/storage/jani/Model.cpp b/src/storm/storage/jani/Model.cpp
index 083b8f7fb..8f6791441 100644
--- a/src/storm/storage/jani/Model.cpp
+++ b/src/storm/storage/jani/Model.cpp
@@ -1134,7 +1134,7 @@ namespace storm {
}
bool Model::reusesActionsInComposition() const {
- if(composition->isParallelComposition()) {
+ if (composition->isParallelComposition()) {
return composition->asParallelComposition().areActionsReused();
}
return false;
diff --git a/src/storm/storage/jani/ParallelComposition.cpp b/src/storm/storage/jani/ParallelComposition.cpp
index 1eaa0ff08..d81db1d91 100644
--- a/src/storm/storage/jani/ParallelComposition.cpp
+++ b/src/storm/storage/jani/ParallelComposition.cpp
@@ -195,13 +195,15 @@ namespace storm {
for (auto const& vector : synchronizationVectors) {
std::string const& action = vector.getInput(inputIndex);
if (action != SynchronizationVector::NO_ACTION_INPUT) {
- return true;
+ if (actions.find(action) != actions.end()) {
+ return true;
+ }
actions.insert(action);
}
}
// And check recursively, in case we have nested parallel composition
if (subcompositions.at(inputIndex)->isParallelComposition()) {
- if(subcompositions.at(inputIndex)->asParallelComposition().areActionsReused()) {
+ if (subcompositions.at(inputIndex)->asParallelComposition().areActionsReused()) {
return true;
}
}
diff --git a/src/storm/utility/cli.cpp b/src/storm/utility/cli.cpp
index d7606149b..4798fd531 100644
--- a/src/storm/utility/cli.cpp
+++ b/src/storm/utility/cli.cpp
@@ -1,6 +1,7 @@
#include "storm/utility/cli.h"
#include "storm/utility/macros.h"
+#include "storm/utility/constants.h"
#include "storm/exceptions/WrongFormatException.h"
namespace storm {
@@ -52,8 +53,12 @@ namespace storm {
int_fast64_t integerValue = std::stoi(value);
constantDefinitions[variable] = manager.integer(integerValue);
} else if (variable.hasRationalType()) {
- double doubleValue = std::stod(value);
- constantDefinitions[variable] = manager.rational(doubleValue);
+ try {
+ storm::RationalNumber rationalValue = storm::utility::convertNumber<storm::RationalNumber>(value);
+ constantDefinitions[variable] = manager.rational(rationalValue);
+ } catch (std::exception& e) {
+ STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Illegal constant definition string '" << constantName << "=" << value << "': " << e.what());
+ }
}
} else {
STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Illegal constant definition string: unknown undefined constant '" << constantName << "'.");
diff --git a/src/storm/utility/constants.cpp b/src/storm/utility/constants.cpp
index a6326d5e8..f2d2b98a8 100644
--- a/src/storm/utility/constants.cpp
+++ b/src/storm/utility/constants.cpp
@@ -397,12 +397,12 @@ namespace storm {
template<>
RationalFunction convertNumber(int_fast64_t const& number){
STORM_LOG_ASSERT(static_cast<carl::sint>(number) == number, "Rationalizing failed, because the number is too large.");
- return RationalFunction(carl::rationalize<RationalNumber>(static_cast<carl::uint>(number)));
+ return RationalFunction(carl::rationalize<RationalNumber>(static_cast<carl::sint>(number)));
}
template<>
RationalNumber convertNumber(std::string const& number) {
- return carl::rationalize<RationalNumber>(number);
+ return carl::parse<RationalNumber>(number);
}
template<>
diff --git a/src/test/builder/DdJaniModelBuilderTest.cpp b/src/test/builder/DdJaniModelBuilderTest.cpp
index 14f5e8081..2622662dc 100644
--- a/src/test/builder/DdJaniModelBuilderTest.cpp
+++ b/src/test/builder/DdJaniModelBuilderTest.cpp
@@ -17,6 +17,8 @@
#include "storm/settings/SettingsManager.h"
#include "storm/settings/modules/IOSettings.h"
+#include "storm/exceptions/InvalidSettingsException.h"
+
TEST(DdJaniModelBuilderTest_Sylvan, Dtmc) {
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/die.pm");
storm::jani::Model janiModel = modelDescription.toJani(true).preprocess().asJaniModel();
@@ -363,7 +365,9 @@ TEST(DdJaniModelBuilderTest_Cudd, SynchronizationVectors) {
inputVector.push_back("c");
inputVector.push_back("b");
synchronizationVectors.push_back(storm::jani::SynchronizationVector(inputVector, "e"));
- EXPECT_THROW(newComposition = std::make_shared<storm::jani::ParallelComposition>(automataCompositions, synchronizationVectors), storm::exceptions::WrongFormatException);
+ newComposition = std::make_shared<storm::jani::ParallelComposition>(automataCompositions, synchronizationVectors);
+ janiModel.setSystemComposition(newComposition);
+ EXPECT_THROW(model = builder.build(janiModel), storm::exceptions::InvalidSettingsException);
}
TEST(DdJaniModelBuilderTest_Sylvan, SynchronizationVectors) {
@@ -419,7 +423,9 @@ TEST(DdJaniModelBuilderTest_Sylvan, SynchronizationVectors) {
inputVector.push_back("c");
inputVector.push_back("b");
synchronizationVectors.push_back(storm::jani::SynchronizationVector(inputVector, "e"));
- EXPECT_THROW(newComposition = std::make_shared<storm::jani::ParallelComposition>(automataCompositions, synchronizationVectors), storm::exceptions::WrongFormatException);
+ newComposition = std::make_shared<storm::jani::ParallelComposition>(automataCompositions, synchronizationVectors);
+ janiModel.setSystemComposition(newComposition);
+ EXPECT_THROW(model = builder.build(janiModel), storm::exceptions::InvalidSettingsException);
}
TEST(DdJaniModelBuilderTest_Sylvan, Composition) {