From eee1a84562238e35ab0877ed538b0c4cb868d21a Mon Sep 17 00:00:00 2001 From: JK Date: Mon, 6 Feb 2017 18:09:30 +0100 Subject: [PATCH 1/9] fix, BinaryNumericalFunctionExpression: simplify for pow(a,b) in double context should not cast result to integer [with Linda Leuschner] Small test case: dtmc const double x = 1E-2; const double y = pow(1-x, 10); module M1 s: [0..2] init 0; [] s = 0 -> y:(s'=1) + (1-y):(s'=2); endmodule should satisfy Pmax>0 [F (s = 1)]. --- .../storage/expressions/BinaryNumericalFunctionExpression.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/storm/storage/expressions/BinaryNumericalFunctionExpression.cpp b/src/storm/storage/expressions/BinaryNumericalFunctionExpression.cpp index 1c0a7908e..5524ca52d 100644 --- a/src/storm/storage/expressions/BinaryNumericalFunctionExpression.cpp +++ b/src/storm/storage/expressions/BinaryNumericalFunctionExpression.cpp @@ -99,7 +99,7 @@ namespace storm { 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(std::pow(firstOperandEvaluation, secondOperandEvaluation)); break; + case OperatorType::Power: newValue = std::pow(firstOperandEvaluation, secondOperandEvaluation); break; case OperatorType::Divide: STORM_LOG_THROW(false, storm::exceptions::InvalidStateException, "Unable to simplify division."); break; } return std::shared_ptr(new RationalLiteralExpression(this->getManager(), newValue)); From e37d0bd5522caddfd5b1c82505da339ad36e53bb Mon Sep 17 00:00:00 2001 From: JK Date: Wed, 8 Feb 2017 18:56:37 +0100 Subject: [PATCH 2/9] ToRationalNumberVisitor: make evaluator optional --- .../storage/expressions/ToRationalNumberVisitor.cpp | 13 ++++++++++++- .../storage/expressions/ToRationalNumberVisitor.h | 7 ++++--- 2 files changed, 16 insertions(+), 4 deletions(-) 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 + ToRationalNumberVisitor::ToRationalNumberVisitor() : ExpressionVisitor() { + // Intentionally left empty. + } + template ToRationalNumberVisitor::ToRationalNumberVisitor(ExpressionEvaluatorBase const& evaluator) : ExpressionVisitor(), evaluator(evaluator) { // Intentionally left empty. @@ -19,7 +24,13 @@ namespace storm { template boost::any ToRationalNumberVisitor::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..55576e5ad 100644 --- a/src/storm/storage/expressions/ToRationalNumberVisitor.h +++ b/src/storm/storage/expressions/ToRationalNumberVisitor.h @@ -16,7 +16,8 @@ namespace storm { template class ToRationalNumberVisitor : public ExpressionVisitor { public: - ToRationalNumberVisitor(ExpressionEvaluatorBase const& evaluator); + ToRationalNumberVisitor(); + ToRationalNumberVisitor(ExpressionEvaluatorBase const& evaluator); RationalNumberType toRationalNumber(Expression const& expression); @@ -36,8 +37,8 @@ namespace storm { private: std::unordered_map valueMapping; - // A reference to an expression evaluator (mainly for resolving the boolean condition in IfThenElse expressions) - ExpressionEvaluatorBase const& evaluator; + // An optional reference to an expression evaluator (mainly for resolving the boolean condition in IfThenElse expressions) + boost::optional const&> evaluator; }; } } From edee041b16c56507a50295467a5fb2c1037dd059 Mon Sep 17 00:00:00 2001 From: JK Date: Wed, 8 Feb 2017 22:29:29 +0100 Subject: [PATCH 3/9] BaseExpression: evaluateAsRational --- src/storm/storage/expressions/BaseExpression.cpp | 8 +++++++- src/storm/storage/expressions/BaseExpression.h | 10 ++++++++++ 2 files changed, 17 insertions(+), 1 deletion(-) 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 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 #include +#include "storm/adapters/NumberAdapter.h" #include "storm/storage/expressions/Type.h" #include "storm/utility/OsDetection.h" #include @@ -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. * From eebfa07618b52907fe21ea6c363dfb9fb3132536 Mon Sep 17 00:00:00 2001 From: JK Date: Wed, 8 Feb 2017 22:31:16 +0100 Subject: [PATCH 4/9] expressions: do simplification involving rationals exactly --- .../BinaryNumericalFunctionExpression.cpp | 14 ++++++--- .../expressions/BinaryRelationExpression.cpp | 29 ++++++++++--------- .../UnaryNumericalFunctionExpression.cpp | 15 +++++----- 3 files changed, 33 insertions(+), 25 deletions(-) diff --git a/src/storm/storage/expressions/BinaryNumericalFunctionExpression.cpp b/src/storm/storage/expressions/BinaryNumericalFunctionExpression.cpp index 5524ca52d..3d2e09153 100644 --- a/src/storm/storage/expressions/BinaryNumericalFunctionExpression.cpp +++ b/src/storm/storage/expressions/BinaryNumericalFunctionExpression.cpp @@ -1,6 +1,7 @@ #include #include +#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(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 = 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(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(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 secondOperandSimplified = this->getSecondOperand()->simplify(); if (firstOperandSimplified->isLiteral() && secondOperandSimplified->isLiteral()) { - boost::variant firstOperandEvaluation; - boost::variant secondOperandEvaluation; - + storm::RationalNumber firstOperandEvaluation; + storm::RationalNumber secondOperandEvaluation; + if (firstOperandSimplified->hasIntegerType()) { - firstOperandEvaluation = firstOperandSimplified->evaluateAsInt(); + firstOperandEvaluation = storm::utility::convertNumber(firstOperandSimplified->evaluateAsInt()); } else { - firstOperandEvaluation = firstOperandSimplified->evaluateAsDouble(); + firstOperandEvaluation = firstOperandSimplified->evaluateAsRational(); } if (secondOperandSimplified->hasIntegerType()) { - secondOperandEvaluation = secondOperandSimplified->evaluateAsInt(); + secondOperandEvaluation = storm::utility::convertNumber(secondOperandSimplified->evaluateAsInt()); } else { - secondOperandEvaluation = secondOperandSimplified->evaluateAsDouble(); + secondOperandEvaluation = secondOperandSimplified->evaluateAsRational(); } - + bool truthValue = false; switch (this->getRelationType()) { - case RelationType::Equal: truthValue = (firstOperandSimplified->hasIntegerType() ? boost::get(firstOperandEvaluation) : boost::get(firstOperandEvaluation)) == (secondOperandSimplified->hasIntegerType() ? boost::get(secondOperandEvaluation) : boost::get(secondOperandEvaluation)); break; - case RelationType::NotEqual: truthValue = (firstOperandSimplified->hasIntegerType() ? boost::get(firstOperandEvaluation) : boost::get(firstOperandEvaluation)) != (secondOperandSimplified->hasIntegerType() ? boost::get(secondOperandEvaluation) : boost::get(secondOperandEvaluation)); break; - case RelationType::Greater: truthValue = (firstOperandSimplified->hasIntegerType() ? boost::get(firstOperandEvaluation) : boost::get(firstOperandEvaluation)) > (secondOperandSimplified->hasIntegerType() ? boost::get(secondOperandEvaluation) : boost::get(secondOperandEvaluation)); break; - case RelationType::GreaterOrEqual: truthValue = (firstOperandSimplified->hasIntegerType() ? boost::get(firstOperandEvaluation) : boost::get(firstOperandEvaluation)) >= (secondOperandSimplified->hasIntegerType() ? boost::get(secondOperandEvaluation) : boost::get(secondOperandEvaluation)); break; - case RelationType::Less: truthValue = (firstOperandSimplified->hasIntegerType() ? boost::get(firstOperandEvaluation) : boost::get(firstOperandEvaluation)) < (secondOperandSimplified->hasIntegerType() ? boost::get(secondOperandEvaluation) : boost::get(secondOperandEvaluation)); break; - case RelationType::LessOrEqual: truthValue = (firstOperandSimplified->hasIntegerType() ? boost::get(firstOperandEvaluation) : boost::get(firstOperandEvaluation)) <= (secondOperandSimplified->hasIntegerType() ? boost::get(secondOperandEvaluation) : boost::get(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(new BooleanLiteralExpression(this->getManager(), truthValue)); } 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 +#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 operandSimplified = this->getOperand()->simplify(); if (operandSimplified->isLiteral()) { - boost::variant operandEvaluation; + boost::variant operandEvaluation; if (operandSimplified->hasIntegerType()) { operandEvaluation = operandSimplified->evaluateAsInt(); } else { - operandEvaluation = operandSimplified->evaluateAsDouble(); + operandEvaluation = operandSimplified->evaluateAsRational(); } - boost::variant result; if (operandSimplified->hasIntegerType()) { int_fast64_t value = 0; switch (this->getOperatorType()) { @@ -82,11 +83,11 @@ namespace storm { } return std::shared_ptr(new IntegerLiteralExpression(this->getManager(), value)); } else { - double value = 0; + storm::RationalNumber value = storm::utility::zero(); switch (this->getOperatorType()) { - case OperatorType::Minus: value = -boost::get(operandEvaluation); break; - case OperatorType::Floor: value = std::floor(boost::get(operandEvaluation)); break; - case OperatorType::Ceil: value = std::ceil(boost::get(operandEvaluation)); break; + case OperatorType::Minus: value = -boost::get(operandEvaluation); break; + case OperatorType::Floor: value = carl::floor(boost::get(operandEvaluation)); break; + case OperatorType::Ceil: value = carl::ceil(boost::get(operandEvaluation)); break; } return std::shared_ptr(new RationalLiteralExpression(this->getManager(), value)); } From b623b4184e95b8421b3b68f3af3ab052eae25ad1 Mon Sep 17 00:00:00 2001 From: JK Date: Thu, 9 Feb 2017 10:37:48 +0100 Subject: [PATCH 5/9] constants.cpp: convertNumber(int_fast64_t) to RationalFunction, fix signed/unsigned cast --- src/storm/utility/constants.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/storm/utility/constants.cpp b/src/storm/utility/constants.cpp index a6326d5e8..34a34ab04 100644 --- a/src/storm/utility/constants.cpp +++ b/src/storm/utility/constants.cpp @@ -397,7 +397,7 @@ namespace storm { template<> RationalFunction convertNumber(int_fast64_t const& number){ STORM_LOG_ASSERT(static_cast(number) == number, "Rationalizing failed, because the number is too large."); - return RationalFunction(carl::rationalize(static_cast(number))); + return RationalFunction(carl::rationalize(static_cast(number))); } template<> From 3c5c609e273bde33643c900e58368ea02a4d4101 Mon Sep 17 00:00:00 2001 From: JK Date: Thu, 9 Feb 2017 10:55:45 +0100 Subject: [PATCH 6/9] utility/cli.cpp, parseConstantDefinitionString: do constants parsing using rational number (exact) Uses convertNumber to obtain a rational number for double constants. Additionally, improve error message if something goes wrong during conversion. --- src/storm/utility/cli.cpp | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) 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(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 << "'."); From d602d2660d93b580c45e26ed59a7b7f6810f5c02 Mon Sep 17 00:00:00 2001 From: JK Date: Mon, 13 Feb 2017 15:58:04 +0100 Subject: [PATCH 7/9] utility/constants.cpp: switch to carl::parse from carl::rationalize carl::parse supports more syntax variants for specifying rational numbers, e.g., 1.23e-10 (scientific notation), 1/24 (fractions), ... --- src/storm/utility/constants.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/storm/utility/constants.cpp b/src/storm/utility/constants.cpp index 34a34ab04..f2d2b98a8 100644 --- a/src/storm/utility/constants.cpp +++ b/src/storm/utility/constants.cpp @@ -402,7 +402,7 @@ namespace storm { template<> RationalNumber convertNumber(std::string const& number) { - return carl::rationalize(number); + return carl::parse(number); } template<> From 9c581bd6350679cf0739b16a59a6e4e9c266fe07 Mon Sep 17 00:00:00 2001 From: dehnert Date: Tue, 14 Feb 2017 10:21:18 +0100 Subject: [PATCH 8/9] fixed two issues: missing include in ToRationalNumberVisitor and missing check for whether actions are reused in a JANI parallel composition --- .../storage/expressions/ToRationalNumberVisitor.h | 2 ++ src/storm/storage/jani/Model.cpp | 2 +- src/storm/storage/jani/ParallelComposition.cpp | 6 ++++-- src/test/builder/DdJaniModelBuilderTest.cpp | 10 ++++++++-- 4 files changed, 15 insertions(+), 5 deletions(-) diff --git a/src/storm/storage/expressions/ToRationalNumberVisitor.h b/src/storm/storage/expressions/ToRationalNumberVisitor.h index 55576e5ad..1f2b88f48 100644 --- a/src/storm/storage/expressions/ToRationalNumberVisitor.h +++ b/src/storm/storage/expressions/ToRationalNumberVisitor.h @@ -2,6 +2,8 @@ #include +#include + #include "storm/adapters/CarlAdapter.h" #include "storm/storage/expressions/Expression.h" 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/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(automataCompositions, synchronizationVectors), storm::exceptions::WrongFormatException); + newComposition = std::make_shared(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(automataCompositions, synchronizationVectors), storm::exceptions::WrongFormatException); + newComposition = std::make_shared(automataCompositions, synchronizationVectors); + janiModel.setSystemComposition(newComposition); + EXPECT_THROW(model = builder.build(janiModel), storm::exceptions::InvalidSettingsException); } TEST(DdJaniModelBuilderTest_Sylvan, Composition) { From 75130ab727ffb6ff4ff587c65f570a4d8db66cb3 Mon Sep 17 00:00:00 2001 From: dehnert Date: Tue, 14 Feb 2017 10:38:46 +0100 Subject: [PATCH 9/9] added patch by Joachim Klein that forwards the boost version storm found to carl --- 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 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)