sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

Merge branch 'master' into nativepolytopes

tempestpy_adaptions
TimQu 8 years ago
parent
7dfc43c828 75130ab727
commit
dfb6ded682
13 changed files with 91 additions and 40 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 2
      resources/3rdparty/CMakeLists.txt
  2. 8
      src/storm/storage/expressions/BaseExpression.cpp
  3. 10
      src/storm/storage/expressions/BaseExpression.h
  4. 14
      src/storm/storage/expressions/BinaryNumericalFunctionExpression.cpp
  5. 29
      src/storm/storage/expressions/BinaryRelationExpression.cpp
  6. 13
      src/storm/storage/expressions/ToRationalNumberVisitor.cpp
  7. 9
      src/storm/storage/expressions/ToRationalNumberVisitor.h
  8. 15
      src/storm/storage/expressions/UnaryNumericalFunctionExpression.cpp
  9. 2
      src/storm/storage/jani/Model.cpp
  10. 6
      src/storm/storage/jani/ParallelComposition.cpp
  11. 9
      src/storm/utility/cli.cpp
  12. 4
      src/storm/utility/constants.cpp
  13. 10
      src/test/builder/DdJaniModelBuilderTest.cpp

2
resources/3rdparty/CMakeLists.txt
View File

@ -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)

8
src/storm/storage/expressions/BaseExpression.cpp
View File

@ -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;
}

10
src/storm/storage/expressions/BaseExpression.h
View File

@ -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.
*

14
src/storm/storage/expressions/BinaryNumericalFunctionExpression.cpp
View File

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

29
src/storm/storage/expressions/BinaryRelationExpression.cpp
View File

@ -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));
}

13
src/storm/storage/expressions/ToRationalNumberVisitor.cpp
View File

@ -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 {

9
src/storm/storage/expressions/ToRationalNumberVisitor.h
View File

@ -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;
};
}
}

15
src/storm/storage/expressions/UnaryNumericalFunctionExpression.cpp
View File

@ -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));
}

2
src/storm/storage/jani/Model.cpp
View File

@ -1134,7 +1134,7 @@ namespace storm {
}
bool Model::reusesActionsInComposition() const {
if(composition->isParallelComposition()) {
if (composition->isParallelComposition()) {
return composition->asParallelComposition().areActionsReused();
}
return false;

6
src/storm/storage/jani/ParallelComposition.cpp
View File

@ -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;
}
}

9
src/storm/utility/cli.cpp
View File

@ -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 << "'.");

4
src/storm/utility/constants.cpp
View File

@ -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<>

10
src/test/builder/DdJaniModelBuilderTest.cpp
View File

@ -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) {

Write Preview
Loading…
Cancel
Save