diff --git a/src/storm/modelchecker/results/ExplicitQuantitativeCheckResult.cpp b/src/storm/modelchecker/results/ExplicitQuantitativeCheckResult.cpp index 0392a37c5..a4dd5f96c 100644 --- a/src/storm/modelchecker/results/ExplicitQuantitativeCheckResult.cpp +++ b/src/storm/modelchecker/results/ExplicitQuantitativeCheckResult.cpp @@ -209,7 +209,7 @@ namespace storm { printAsRange = true; } else { if (valuesAsMap.size() == 1) { - out << valuesAsMap.begin()->second; + print(out, valuesAsMap.begin()->second); } else { out << "{"; bool first = true; diff --git a/src/storm/storage/expressions/ExpressionEvaluator.cpp b/src/storm/storage/expressions/ExpressionEvaluator.cpp index 541e2f7e7..abea0ce73 100644 --- a/src/storm/storage/expressions/ExpressionEvaluator.cpp +++ b/src/storm/storage/expressions/ExpressionEvaluator.cpp @@ -1,6 +1,8 @@ #include "storm/storage/expressions/ExpressionEvaluator.h" #include "storm/storage/expressions/ExpressionManager.h" +#include "storm/utility/constants.h" + namespace storm { namespace expressions { ExpressionEvaluator<double>::ExpressionEvaluator(storm::expressions::ExpressionManager const& manager) : ExprtkExpressionEvaluator(manager) { @@ -31,22 +33,52 @@ namespace storm { } #ifdef STORM_HAVE_CARL - ExpressionEvaluator<RationalNumber>::ExpressionEvaluator(storm::expressions::ExpressionManager const& manager) : ExpressionEvaluatorWithVariableToExpressionMap<RationalNumber>(manager) { + ExpressionEvaluator<RationalNumber>::ExpressionEvaluator(storm::expressions::ExpressionManager const& manager) : ExprtkExpressionEvaluatorBase<RationalNumber>(manager) { // Intentionally left empty. } + void ExpressionEvaluator<RationalNumber>::setBooleanValue(storm::expressions::Variable const& variable, bool value) { + ExprtkExpressionEvaluatorBase<RationalNumber>::setBooleanValue(variable, value); + + // Not forwarding value of variable to rational number visitor as it cannot treat boolean variables anyway. + } + + void ExpressionEvaluator<RationalNumber>::setIntegerValue(storm::expressions::Variable const& variable, int_fast64_t value) { + ExprtkExpressionEvaluatorBase<RationalNumber>::setIntegerValue(variable, value); + rationalNumberVisitor.setMapping(variable, storm::utility::convertNumber<RationalNumber>(value)); + } + + void ExpressionEvaluator<RationalNumber>::setRationalValue(storm::expressions::Variable const& variable, double value) { + ExprtkExpressionEvaluatorBase<RationalNumber>::setRationalValue(variable, value); + rationalNumberVisitor.setMapping(variable, storm::utility::convertNumber<RationalNumber>(value)); + } + RationalNumber ExpressionEvaluator<RationalNumber>::asRational(Expression const& expression) const { - Expression substitutedExpression = expression.substitute(this->variableToExpressionMap); - return this->rationalNumberVisitor.toRationalNumber(substitutedExpression); + return this->rationalNumberVisitor.toRationalNumber(expression); } - ExpressionEvaluator<RationalFunction>::ExpressionEvaluator(storm::expressions::ExpressionManager const& manager) : ExpressionEvaluatorWithVariableToExpressionMap<RationalFunction>(manager) { + ExpressionEvaluator<RationalFunction>::ExpressionEvaluator(storm::expressions::ExpressionManager const& manager) : ExprtkExpressionEvaluatorBase<RationalFunction>(manager) { // Intentionally left empty. } + void ExpressionEvaluator<RationalFunction>::setBooleanValue(storm::expressions::Variable const& variable, bool value) { + ExprtkExpressionEvaluatorBase<RationalFunction>::setBooleanValue(variable, value); + + // Not forwarding value of variable to rational number visitor as it cannot treat boolean variables anyway. + } + + void ExpressionEvaluator<RationalFunction>::setIntegerValue(storm::expressions::Variable const& variable, int_fast64_t value) { + ExprtkExpressionEvaluatorBase<RationalFunction>::setIntegerValue(variable, value); + rationalFunctionVisitor.setMapping(variable, storm::utility::convertNumber<RationalFunction>(value)); + } + + void ExpressionEvaluator<RationalFunction>::setRationalValue(storm::expressions::Variable const& variable, double value) { + ExprtkExpressionEvaluatorBase<RationalFunction>::setRationalValue(variable, value); + rationalFunctionVisitor.setMapping(variable, storm::utility::convertNumber<RationalFunction>(value)); + } + RationalFunction ExpressionEvaluator<RationalFunction>::asRational(Expression const& expression) const { - Expression substitutedExpression = expression.substitute(this->variableToExpressionMap); - return this->rationalFunctionVisitor.toRationalFunction(substitutedExpression); + return this->rationalFunctionVisitor.toRationalFunction(expression); } template class ExpressionEvaluatorWithVariableToExpressionMap<RationalNumber>; diff --git a/src/storm/storage/expressions/ExpressionEvaluator.h b/src/storm/storage/expressions/ExpressionEvaluator.h index 376b530c2..9308c912b 100644 --- a/src/storm/storage/expressions/ExpressionEvaluator.h +++ b/src/storm/storage/expressions/ExpressionEvaluator.h @@ -37,10 +37,14 @@ namespace storm { #ifdef STORM_HAVE_CARL template<> - class ExpressionEvaluator<RationalNumber> : public ExpressionEvaluatorWithVariableToExpressionMap<RationalNumber> { + class ExpressionEvaluator<RationalNumber> : public ExprtkExpressionEvaluatorBase<RationalNumber> { public: ExpressionEvaluator(storm::expressions::ExpressionManager const& manager); + void setBooleanValue(storm::expressions::Variable const& variable, bool value) override; + void setIntegerValue(storm::expressions::Variable const& variable, int_fast64_t value) override; + void setRationalValue(storm::expressions::Variable const& variable, double value) override; + RationalNumber asRational(Expression const& expression) const override; private: @@ -49,10 +53,14 @@ namespace storm { }; template<> - class ExpressionEvaluator<RationalFunction> : public ExpressionEvaluatorWithVariableToExpressionMap<RationalFunction> { + class ExpressionEvaluator<RationalFunction> : public ExprtkExpressionEvaluatorBase<RationalFunction> { public: ExpressionEvaluator(storm::expressions::ExpressionManager const& manager); + void setBooleanValue(storm::expressions::Variable const& variable, bool value) override; + void setIntegerValue(storm::expressions::Variable const& variable, int_fast64_t value) override; + void setRationalValue(storm::expressions::Variable const& variable, double value) override; + RationalFunction asRational(Expression const& expression) const override; private: diff --git a/src/storm/storage/expressions/ExpressionManager.cpp b/src/storm/storage/expressions/ExpressionManager.cpp index 3072c30e0..d1b3d15cd 100644 --- a/src/storm/storage/expressions/ExpressionManager.cpp +++ b/src/storm/storage/expressions/ExpressionManager.cpp @@ -52,7 +52,7 @@ namespace storm { } } - ExpressionManager::ExpressionManager() : nameToIndexMapping(), indexToNameMapping(), indexToTypeMapping(), numberOfBooleanVariables(0), numberOfIntegerVariables(0), numberOfBitVectorVariables(0), numberOfRationalVariables(0), numberOfAuxiliaryVariables(0), numberOfAuxiliaryBooleanVariables(0), numberOfAuxiliaryIntegerVariables(0), numberOfAuxiliaryBitVectorVariables(0), numberOfAuxiliaryRationalVariables(0), freshVariableCounter(0), types() { + ExpressionManager::ExpressionManager() : nameToIndexMapping(), indexToNameMapping(), indexToTypeMapping(), numberOfBooleanVariables(0), numberOfIntegerVariables(0), numberOfBitVectorVariables(0), numberOfRationalVariables(0), numberOfAuxiliaryVariables(0), numberOfAuxiliaryBooleanVariables(0), numberOfAuxiliaryIntegerVariables(0), numberOfAuxiliaryBitVectorVariables(0), numberOfAuxiliaryRationalVariables(0), freshVariableCounter(0) { // Intentionally left empty. } @@ -65,19 +65,19 @@ namespace storm { } Expression ExpressionManager::boolean(bool value) const { - return Expression(std::shared_ptr<BaseExpression>(new BooleanLiteralExpression(*this, value))); + return Expression(std::make_shared<BooleanLiteralExpression>(*this, value)); } Expression ExpressionManager::integer(int_fast64_t value) const { - return Expression(std::shared_ptr<BaseExpression>(new IntegerLiteralExpression(*this, value))); + return Expression(std::make_shared<IntegerLiteralExpression>(*this, value)); } Expression ExpressionManager::rational(double value) const { - return Expression(std::shared_ptr<BaseExpression>(new RationalLiteralExpression(*this, value))); + return Expression(std::make_shared<RationalLiteralExpression>(*this, value)); } Expression ExpressionManager::rational(storm::RationalNumber const& value) const { - return Expression(std::shared_ptr<BaseExpression>(new RationalLiteralExpression(*this, value))); + return Expression(std::make_shared<RationalLiteralExpression>(*this, value)); } bool ExpressionManager::operator==(ExpressionManager const& other) const { @@ -85,43 +85,34 @@ namespace storm { } Type const& ExpressionManager::getBooleanType() const { - Type type(this->getSharedPointer(), std::shared_ptr<BaseType>(new BooleanType())); - auto typeIterator = types.find(type); - if (typeIterator == types.end()) { - auto iteratorBoolPair = types.insert(type); - return *iteratorBoolPair.first; + if (!booleanType) { + booleanType = Type(this->getSharedPointer(), std::shared_ptr<BaseType>(new BooleanType())); } - return *typeIterator; + return booleanType.get(); } Type const& ExpressionManager::getIntegerType() const { - Type type(this->getSharedPointer(), std::shared_ptr<BaseType>(new IntegerType())); - auto typeIterator = types.find(type); - if (typeIterator == types.end()) { - auto iteratorBoolPair = types.insert(type); - return *iteratorBoolPair.first; + if (!integerType) { + integerType = Type(this->getSharedPointer(), std::shared_ptr<BaseType>(new IntegerType())); } - return *typeIterator; + return integerType.get(); } Type const& ExpressionManager::getBitVectorType(std::size_t width) const { Type type(this->getSharedPointer(), std::shared_ptr<BaseType>(new BitVectorType(width))); - auto typeIterator = types.find(type); - if (typeIterator == types.end()) { - auto iteratorBoolPair = types.insert(type); + auto typeIterator = bitvectorTypes.find(type); + if (typeIterator == bitvectorTypes.end()) { + auto iteratorBoolPair = bitvectorTypes.insert(type); return *iteratorBoolPair.first; } return *typeIterator; } Type const& ExpressionManager::getRationalType() const { - Type type(this->getSharedPointer(), std::shared_ptr<BaseType>(new RationalType())); - auto typeIterator = types.find(type); - if (typeIterator == types.end()) { - auto iteratorBoolPair = types.insert(type); - return *iteratorBoolPair.first; + if (!rationalType) { + rationalType = Type(this->getSharedPointer(), std::shared_ptr<BaseType>(new RationalType())); } - return *typeIterator; + return rationalType.get(); } bool ExpressionManager::isValidVariableName(std::string const& name) { diff --git a/src/storm/storage/expressions/ExpressionManager.h b/src/storm/storage/expressions/ExpressionManager.h index 9630a719d..1ad82b939 100644 --- a/src/storm/storage/expressions/ExpressionManager.h +++ b/src/storm/storage/expressions/ExpressionManager.h @@ -8,6 +8,8 @@ #include <unordered_set> #include <iostream> +#include <boost/optional.hpp> + #include "storm/storage/expressions/Variable.h" #include "storm/storage/expressions/Expression.h" #include "storm/adapters/CarlAdapter.h" @@ -455,8 +457,11 @@ namespace storm { uint_fast64_t freshVariableCounter; // The types managed by this manager. - mutable std::unordered_set<Type> types; - + mutable boost::optional<Type> booleanType; + mutable boost::optional<Type> integerType; + mutable std::unordered_set<Type> bitvectorTypes; + mutable boost::optional<Type> rationalType; + // A mask that can be used to query whether a variable is an auxiliary variable. static const uint64_t auxiliaryMask = (1ull << 50); diff --git a/src/storm/storage/expressions/ToCppVisitor.cpp b/src/storm/storage/expressions/ToCppVisitor.cpp index 25b7dd5a3..d336d0d40 100644 --- a/src/storm/storage/expressions/ToCppVisitor.cpp +++ b/src/storm/storage/expressions/ToCppVisitor.cpp @@ -317,7 +317,7 @@ namespace storm { ToCppTranslationOptions const& options = boost::any_cast<ToCppTranslationOptions const&>(data); switch (options.getMode()) { case ToCppTranslationMode::KeepType: - stream << "(static_cast<double>(" << carl::getNum(expression.getValue()) << ")/carl::getDenom(expression.getValue()))"; + stream << "(static_cast<double>(" << carl::getNum(expression.getValue()) << ")/" << carl::getDenom(expression.getValue()) << ")"; break; case ToCppTranslationMode::CastDouble: stream << "static_cast<double>(" << expression.getValueAsDouble() << ")"; diff --git a/src/storm/storage/expressions/ToRationalFunctionVisitor.cpp b/src/storm/storage/expressions/ToRationalFunctionVisitor.cpp index 9dff8b060..9f8ab16ec 100644 --- a/src/storm/storage/expressions/ToRationalFunctionVisitor.cpp +++ b/src/storm/storage/expressions/ToRationalFunctionVisitor.cpp @@ -68,6 +68,11 @@ namespace storm { template<typename RationalFunctionType> boost::any ToRationalFunctionVisitor<RationalFunctionType>::visit(VariableExpression const& expression, boost::any const&) { + auto valueIt = valueMapping.find(expression.getVariable()); + if (valueIt != valueMapping.end()) { + return valueIt->second; + } + auto variablePair = variableToVariableMap.find(expression.getVariable()); if (variablePair != variableToVariableMap.end()) { return convertVariableToPolynomial(variablePair->second); @@ -95,13 +100,18 @@ namespace storm { template<typename RationalFunctionType> boost::any ToRationalFunctionVisitor<RationalFunctionType>::visit(IntegerLiteralExpression const& expression, boost::any const&) { - return RationalFunctionType(carl::rationalize<storm::RationalNumber>(static_cast<size_t>(expression.getValue()))); + return RationalFunctionType(storm::utility::convertNumber<storm::RationalFunction>(expression.getValue())); } template<typename RationalFunctionType> boost::any ToRationalFunctionVisitor<RationalFunctionType>::visit(RationalLiteralExpression const& expression, boost::any const&) { return storm::utility::convertNumber<storm::RationalFunction>(expression.getValue()); } + + template<typename RationalFunctionType> + void ToRationalFunctionVisitor<RationalFunctionType>::setMapping(storm::expressions::Variable const& variable, RationalFunctionType const& value) { + valueMapping[variable] = value; + } template class ToRationalFunctionVisitor<storm::RationalFunction>; #endif diff --git a/src/storm/storage/expressions/ToRationalFunctionVisitor.h b/src/storm/storage/expressions/ToRationalFunctionVisitor.h index 44696f940..7c7cfacf5 100644 --- a/src/storm/storage/expressions/ToRationalFunctionVisitor.h +++ b/src/storm/storage/expressions/ToRationalFunctionVisitor.h @@ -1,7 +1,10 @@ #ifndef STORM_STORAGE_EXPRESSIONS_TORATIONALFUNCTIONVISITOR_H_ #define STORM_STORAGE_EXPRESSIONS_TORATIONALFUNCTIONVISITOR_H_ +#include <unordered_map> + #include "storm/adapters/CarlAdapter.h" + #include "storm/storage/expressions/Expression.h" #include "storm/storage/expressions/Expressions.h" #include "storm/storage/expressions/ExpressionVisitor.h" @@ -29,6 +32,8 @@ namespace storm { virtual boost::any visit(IntegerLiteralExpression const& expression, boost::any const& data) override; virtual boost::any visit(RationalLiteralExpression const& expression, boost::any const& data) override; + void setMapping(storm::expressions::Variable const& variable, RationalFunctionType const& value); + private: template<typename TP = typename RationalFunctionType::PolyType, carl::EnableIf<carl::needs_cache<TP>> = carl::dummy> RationalFunctionType convertVariableToPolynomial(carl::Variable const& variable) { @@ -45,6 +50,9 @@ namespace storm { // The cache that is used in case the underlying type needs a cache. std::shared_ptr<carl::Cache<carl::PolynomialFactorizationPair<RawPolynomial>>> cache; + + // A mapping from variables to their values. + std::unordered_map<storm::expressions::Variable, RationalFunctionType> valueMapping; }; #endif } diff --git a/src/storm/storage/expressions/ToRationalNumberVisitor.cpp b/src/storm/storage/expressions/ToRationalNumberVisitor.cpp index 8a3643842..d4ba17c06 100644 --- a/src/storm/storage/expressions/ToRationalNumberVisitor.cpp +++ b/src/storm/storage/expressions/ToRationalNumberVisitor.cpp @@ -68,8 +68,8 @@ namespace storm { } template<typename RationalNumberType> - boost::any ToRationalNumberVisitor<RationalNumberType>::visit(VariableExpression const&, boost::any const&) { - STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Cannot transform expressions containing variables to a rational number."); + boost::any ToRationalNumberVisitor<RationalNumberType>::visit(VariableExpression const& expression, boost::any const&) { + return valueMapping.at(expression.getVariable()); } template<typename RationalNumberType> @@ -112,6 +112,11 @@ namespace storm { #endif } + template<typename RationalNumberType> + void ToRationalNumberVisitor<RationalNumberType>::setMapping(storm::expressions::Variable const& variable, RationalNumberType const& value) { + valueMapping[variable] = value; + } + #ifdef STORM_HAVE_CARL template class ToRationalNumberVisitor<storm::RationalNumber>; #endif diff --git a/src/storm/storage/expressions/ToRationalNumberVisitor.h b/src/storm/storage/expressions/ToRationalNumberVisitor.h index c6badc7b1..6177fd2ae 100644 --- a/src/storm/storage/expressions/ToRationalNumberVisitor.h +++ b/src/storm/storage/expressions/ToRationalNumberVisitor.h @@ -1,6 +1,9 @@ #pragma once +#include <unordered_map> + #include "storm/adapters/CarlAdapter.h" + #include "storm/storage/expressions/Expression.h" #include "storm/storage/expressions/Expressions.h" #include "storm/storage/expressions/ExpressionVisitor.h" @@ -26,6 +29,11 @@ namespace storm { virtual boost::any visit(BooleanLiteralExpression const& expression, boost::any const& data) override; virtual boost::any visit(IntegerLiteralExpression const& expression, boost::any const& data) override; virtual boost::any visit(RationalLiteralExpression const& expression, boost::any const& data) override; + + void setMapping(storm::expressions::Variable const& variable, RationalNumberType const& value); + + private: + std::unordered_map<storm::expressions::Variable, RationalNumberType> valueMapping; }; } } diff --git a/src/storm/storage/jani/Model.cpp b/src/storm/storage/jani/Model.cpp index 7b1c6e908..e02bac355 100644 --- a/src/storm/storage/jani/Model.cpp +++ b/src/storm/storage/jani/Model.cpp @@ -998,7 +998,12 @@ namespace storm { for (auto const& location : automaton.get().getLocations()) { for (auto const& assignment : location.getAssignments().getTransientAssignments()) { if (assignment.getExpressionVariable() == transientVariable.getExpressionVariable()) { - auto newExpression = (locationVariable == this->getManager().integer(automaton.get().getLocationIndex(location.getName()))) && (negate ? !assignment.getAssignedExpression() : assignment.getAssignedExpression()); + storm::expressions::Expression newExpression; + if (automaton.get().getNumberOfLocations() <= 1) { + newExpression = (negate ? !assignment.getAssignedExpression() : assignment.getAssignedExpression()); + } else { + newExpression = (locationVariable == this->getManager().integer(automaton.get().getLocationIndex(location.getName()))) && (negate ? !assignment.getAssignedExpression() : assignment.getAssignedExpression()); + } if (result.isInitialized()) { result = result || newExpression; } else { diff --git a/src/storm/storage/prism/ToJaniConverter.cpp b/src/storm/storage/prism/ToJaniConverter.cpp index 963683b19..4e451d177 100644 --- a/src/storm/storage/prism/ToJaniConverter.cpp +++ b/src/storm/storage/prism/ToJaniConverter.cpp @@ -94,10 +94,18 @@ namespace storm { } } + // Go through the labels and construct assignments to transient variables that are added to the loctions. + std::vector<storm::jani::Assignment> transientLocationAssignments; + for (auto const& label : program.getLabels()) { + auto newExpressionVariable = manager->declareBooleanVariable("label_" + label.getName()); + storm::jani::BooleanVariable const& newTransientVariable = janiModel.addVariable(storm::jani::BooleanVariable(newExpressionVariable.getName(), newExpressionVariable, manager->boolean(false), true)); + + transientLocationAssignments.emplace_back(newTransientVariable, label.getStatePredicateExpression()); + } + // Go through the reward models and construct assignments to the transient variables that are to be added to // edges and transient assignments that are added to the locations. std::map<uint_fast64_t, std::vector<storm::jani::Assignment>> transientEdgeAssignments; - std::vector<storm::jani::Assignment> transientLocationAssignments; for (auto const& rewardModel : program.getRewardModels()) { auto newExpressionVariable = manager->declareRationalVariable(rewardModel.getName().empty() ? "default" : rewardModel.getName()); storm::jani::RealVariable const& newTransientVariable = janiModel.addVariable(storm::jani::RealVariable(rewardModel.getName().empty() ? "default" : rewardModel.getName(), newExpressionVariable, manager->rational(0.0), true)); diff --git a/src/storm/utility/constants.cpp b/src/storm/utility/constants.cpp index 66805146b..7eeae8106 100644 --- a/src/storm/utility/constants.cpp +++ b/src/storm/utility/constants.cpp @@ -357,11 +357,23 @@ namespace storm { return carl::rationalize<RationalNumber>(static_cast<carl::uint>(number)); } + template<> + RationalNumber convertNumber(int_fast64_t const& number){ + STORM_LOG_ASSERT(static_cast<carl::sint>(number) == number, "Rationalizing failed, because the number is too large."); + return carl::rationalize<RationalNumber>(static_cast<carl::sint>(number)); + } + template<> RationalFunction convertNumber(double const& number){ return RationalFunction(carl::rationalize<RationalNumber>(number)); } + 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))); + } + template<> RationalNumber convertNumber(std::string const& number) { return carl::rationalize<RationalNumber>(number); diff --git a/src/test/modelchecker/SymbolicDtmcPrctlModelCheckerTest.cpp b/src/test/modelchecker/SymbolicDtmcPrctlModelCheckerTest.cpp index 7a2be484b..451d2ad49 100644 --- a/src/test/modelchecker/SymbolicDtmcPrctlModelCheckerTest.cpp +++ b/src/test/modelchecker/SymbolicDtmcPrctlModelCheckerTest.cpp @@ -76,8 +76,8 @@ TEST(SymbolicDtmcPrctlModelCheckerTest, Die_Cudd) { result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates())); storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::CUDD>& quantitativeResult4 = result->asSymbolicQuantitativeCheckResult<storm::dd::DdType::CUDD, double>(); - EXPECT_NEAR(3.6666622161865234, quantitativeResult4.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); - EXPECT_NEAR(3.6666622161865234, quantitativeResult4.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); + EXPECT_NEAR(3.6666646003723145, quantitativeResult4.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); + EXPECT_NEAR(3.6666646003723145, quantitativeResult4.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision()); } TEST(SymbolicDtmcPrctlModelCheckerTest, Die_Sylvan) {