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

Fixed some tests/parser. 

Former-commit-id: d1767861c4
tempestpy_adaptions
dehnert 10 years ago
parent
53196f5610
commit
aaefe7dfa5
8 changed files with 40 additions and 20 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
      src/parser/PrismParser.cpp
  2. 2
      src/storage/BitVectorHashMap.cpp
  3. 23
      src/storage/expressions/BinaryBooleanFunctionExpression.cpp
  4. 18
      src/storage/expressions/ExprtkExpressionEvaluator.cpp
  5. 4
      src/storage/expressions/ExprtkExpressionEvaluator.h
  6. 5
      test/functional/parser/PrismParserTest.cpp
  7. 4
      test/functional/storage/ExpressionEvalutionTest.cpp
  8. 2
      test/functional/storage/ExpressionTest.cpp

2
src/parser/PrismParser.cpp
View File

@ -342,7 +342,7 @@ namespace storm {
storm::prism::TransitionReward PrismParser::createTransitionReward(std::string const& actionName, storm::expressions::Expression statePredicateExpression, storm::expressions::Expression rewardValueExpression, GlobalProgramInformation& globalProgramInformation) const {
auto const& nameIndexPair = globalProgramInformation.actionIndices.find(actionName);
STORM_LOG_THROW(nameIndexPair != globalProgramInformation.actionIndices.end(), storm::exceptions::WrongFormatException, "Transition reward refers to illegal action '" << actionName << "'.");
STORM_LOG_THROW(actionName.empty() || nameIndexPair != globalProgramInformation.actionIndices.end(), storm::exceptions::WrongFormatException, "Transition reward refers to illegal action '" << actionName << "'.");
return storm::prism::TransitionReward(nameIndexPair->second, actionName, statePredicateExpression, rewardValueExpression, this->getFilename());
}

2
src/storage/BitVectorHashMap.cpp
View File

@ -7,7 +7,7 @@
namespace storm {
namespace storage {
template<class ValueType, class Hash1, class Hash2>
const std::vector<std::size_t> BitVectorHashMap<ValueType, Hash1, Hash2>::sizes = {5, 13, 31, 79, 163, 277, 499, 1021, 2029, 3989, 8059, 16001, 32099, 64301, 127921, 256499, 511111, 1024901, 2048003, 4096891, 8192411, 15485863};
const std::vector<std::size_t> BitVectorHashMap<ValueType, Hash1, Hash2>::sizes = {5, 13, 31, 79, 163, 277, 499, 1021, 2029, 3989, 8059, 16001, 32099, 64301, 127921, 256499, 511111, 1024901, 2048003, 4096891, 8192411, 15485863, 32142191};
template<class ValueType, class Hash1, class Hash2>
BitVectorHashMap<ValueType, Hash1, Hash2>::BitVectorHashMap(uint64_t bucketSize, uint64_t initialSize, double loadFactor) : loadFactor(loadFactor), bucketSize(bucketSize), numberOfElements(0) {

23
src/storage/expressions/BinaryBooleanFunctionExpression.cpp
View File

@ -1,5 +1,6 @@
#include "src/storage/expressions/BinaryBooleanFunctionExpression.h"
#include "src/storage/expressions/BooleanLiteralExpression.h"
#include "src/storage/expressions/ExpressionManager.h"
#include "src/utility/macros.h"
#include "src/exceptions/InvalidTypeException.h"
@ -45,7 +46,7 @@ namespace storm {
std::shared_ptr<BaseExpression const> firstOperandSimplified = this->getFirstOperand()->simplify();
std::shared_ptr<BaseExpression const> secondOperandSimplified = this->getSecondOperand()->simplify();
if (firstOperandSimplified->isLiteral() && secondOperandSimplified->isLiteral()) {
if (firstOperandSimplified->isLiteral() || secondOperandSimplified->isLiteral()) {
switch (this->getOperatorType()) {
case OperatorType::And:
if (firstOperandSimplified->isTrue()) {
@ -69,7 +70,21 @@ namespace storm {
return firstOperandSimplified;
}
break;
case OperatorType::Xor: break;
case OperatorType::Xor:
if (firstOperandSimplified->isTrue()) {
if (secondOperandSimplified->isFalse()) {
return firstOperandSimplified;
} else if (secondOperandSimplified->isTrue()) {
return this->getManager().boolean(false).getBaseExpressionPointer();
}
} else if (firstOperandSimplified->isFalse()) {
if (secondOperandSimplified->isTrue()) {
return secondOperandSimplified;
} else if (secondOperandSimplified->isFalse()) {
return this->getManager().boolean(false).getBaseExpressionPointer();
}
}
break;
case OperatorType::Implies:
if (firstOperandSimplified->isTrue()) {
return secondOperandSimplified;
@ -84,6 +99,10 @@ namespace storm {
return std::shared_ptr<BaseExpression>(new BooleanLiteralExpression(this->getManager(), true));
} else if (firstOperandSimplified->isFalse() && secondOperandSimplified->isFalse()) {
return std::shared_ptr<BaseExpression>(new BooleanLiteralExpression(this->getManager(), true));
} else if (firstOperandSimplified->isTrue() && secondOperandSimplified->isFalse()) {
return std::shared_ptr<BaseExpression>(new BooleanLiteralExpression(this->getManager(), false));
} else if (firstOperandSimplified->isFalse() && secondOperandSimplified->isTrue()) {
return std::shared_ptr<BaseExpression>(new BooleanLiteralExpression(this->getManager(), false));
}
break;
}

18
src/storage/expressions/ExpressionEvaluator.cpp → src/storage/expressions/ExprtkExpressionEvaluator.cpp
View File

@ -1,9 +1,9 @@
#include "src/storage/expressions/ExpressionEvaluator.h"
#include "src/storage/expressions/ExprtkExpressionEvaluator.h"
#include "src/storage/expressions/ExpressionManager.h"
namespace storm {
namespace expressions {
ExpressionEvaluator::ExpressionEvaluator(storm::expressions::ExpressionManager const& manager) : manager(manager.getSharedPointer()), booleanValues(manager.getNumberOfBooleanVariables()), integerValues(manager.getNumberOfIntegerVariables()), rationalValues(manager.getNumberOfRationalVariables()) {
ExprtkExpressionEvaluator::ExprtkExpressionEvaluator(storm::expressions::ExpressionManager const& manager) : manager(manager.getSharedPointer()), booleanValues(manager.getNumberOfBooleanVariables()), integerValues(manager.getNumberOfIntegerVariables()), rationalValues(manager.getNumberOfRationalVariables()) {
for (auto const& variableTypePair : manager) {
if (variableTypePair.second.isBooleanType()) {
@ -17,7 +17,7 @@ namespace storm {
symbolTable.add_constants();
}
bool ExpressionEvaluator::asBool(Expression const& expression) {
bool ExprtkExpressionEvaluator::asBool(Expression const& expression) {
BaseExpression const* expressionPtr = expression.getBaseExpressionPointer().get();
auto const& expressionPair = this->compiledExpressions.find(expression.getBaseExpressionPointer().get());
if (expressionPair == this->compiledExpressions.end()) {
@ -27,7 +27,7 @@ namespace storm {
return expressionPair->second.value() == ValueType(1);
}
int_fast64_t ExpressionEvaluator::asInt(Expression const& expression) {
int_fast64_t ExprtkExpressionEvaluator::asInt(Expression const& expression) {
BaseExpression const* expressionPtr = expression.getBaseExpressionPointer().get();
auto const& expressionPair = this->compiledExpressions.find(expression.getBaseExpressionPointer().get());
if (expressionPair == this->compiledExpressions.end()) {
@ -37,7 +37,7 @@ namespace storm {
return static_cast<int_fast64_t>(expressionPair->second.value());
}
double ExpressionEvaluator::asDouble(Expression const& expression) {
double ExprtkExpressionEvaluator::asDouble(Expression const& expression) {
BaseExpression const* expressionPtr = expression.getBaseExpressionPointer().get();
auto const& expressionPair = this->compiledExpressions.find(expression.getBaseExpressionPointer().get());
if (expressionPair == this->compiledExpressions.end()) {
@ -47,7 +47,7 @@ namespace storm {
return static_cast<double>(expressionPair->second.value());
}
ExpressionEvaluator::CompiledExpressionType& ExpressionEvaluator::getCompiledExpression(BaseExpression const* expression) {
ExprtkExpressionEvaluator::CompiledExpressionType& ExprtkExpressionEvaluator::getCompiledExpression(BaseExpression const* expression) {
std::pair<CacheType::iterator, bool> result = this->compiledExpressions.emplace(expression, CompiledExpressionType());
CompiledExpressionType& compiledExpression = result.first->second;
compiledExpression.register_symbol_table(symbolTable);
@ -55,15 +55,15 @@ namespace storm {
return compiledExpression;
}
void ExpressionEvaluator::setBooleanValue(storm::expressions::Variable const& variable, bool value) {
void ExprtkExpressionEvaluator::setBooleanValue(storm::expressions::Variable const& variable, bool value) {
this->booleanValues[variable.getOffset()] = static_cast<ValueType>(value);
}
void ExpressionEvaluator::setIntegerValue(storm::expressions::Variable const& variable, int_fast64_t value) {
void ExprtkExpressionEvaluator::setIntegerValue(storm::expressions::Variable const& variable, int_fast64_t value) {
this->integerValues[variable.getOffset()] = static_cast<ValueType>(value);
}
void ExpressionEvaluator::setRationalValue(storm::expressions::Variable const& variable, double value) {
void ExprtkExpressionEvaluator::setRationalValue(storm::expressions::Variable const& variable, double value) {
this->rationalValues[variable.getOffset()] = static_cast<ValueType>(value);
}
}

4
src/storage/expressions/ExpressionEvaluator.h → src/storage/expressions/ExprtkExpressionEvaluator.h
View File

@ -12,14 +12,14 @@
namespace storm {
namespace expressions {
class ExpressionEvaluator {
class ExprtkExpressionEvaluator {
public:
/*!
* Creates an expression evaluator that is capable of evaluating expressions managed by the given manager.
*
* @param manager The manager responsible for the expressions.
*/
ExpressionEvaluator(storm::expressions::ExpressionManager const& manager);
ExprtkExpressionEvaluator(storm::expressions::ExpressionManager const& manager);
bool asBool(Expression const& expression);
int_fast64_t asInt(Expression const& expression);

5
test/functional/parser/PrismParserTest.cpp
View File

@ -8,6 +8,7 @@ TEST(PrismParser, StandardModelTest) {
EXPECT_NO_THROW(result = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/parser/prism/coin2.nm"));
EXPECT_NO_THROW(result = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/parser/prism/crowds5_5.pm"));
EXPECT_NO_THROW(result = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/parser/prism/csma2_2.nm"));
result = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/parser/prism/die.pm");
EXPECT_NO_THROW(result = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/parser/prism/die.pm"));
EXPECT_NO_THROW(result = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/parser/prism/firewire.nm"));
EXPECT_NO_THROW(result = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/parser/prism/leader3.nm"));
@ -84,12 +85,12 @@ TEST(PrismParser, ComplexTest) {
endinit
rewards "testrewards"
[stateRew] true : a + 7;
[a] true : a + 7;
max(f, a) <= 8 : 2*b;
endrewards
rewards "testrewards2"
[stateRew] true : a + 7;
[b] true : a + 7;
max(f, a) <= 8 : 2*b;
endrewards)";

4
test/functional/storage/ExpressionEvalutionTest.cpp
View File

@ -2,7 +2,7 @@
#include "src/storage/expressions/Expression.h"
#include "src/storage/expressions/ExpressionManager.h"
#include "src/storage/expressions/SimpleValuation.h"
#include "src/storage/expressions/ExpressionEvaluator.h"
#include "src/storage/expressions/ExprtkExpressionEvaluator.h"
TEST(ExpressionEvaluation, NaiveEvaluation) {
std::shared_ptr<storm::expressions::ExpressionManager> manager(new storm::expressions::ExpressionManager());
@ -44,7 +44,7 @@ TEST(ExpressionEvaluation, ExprTkEvaluation) {
ASSERT_NO_THROW(z = manager->declareRationalVariable("z"));
storm::expressions::Expression iteExpression = storm::expressions::ite(x, y + z, manager->integer(3) * z);
storm::expressions::ExpressionEvaluator eval(*manager);
storm::expressions::ExprtkExpressionEvaluator eval(*manager);
eval.setRationalValue(z, 5.5);
eval.setBooleanValue(x, true);

2
test/functional/storage/ExpressionTest.cpp
View File

@ -275,7 +275,7 @@ TEST(Expression, SubstitutionTest) {
storm::expressions::Expression tempExpression;
ASSERT_NO_THROW(tempExpression = (intVarExpression < threeExpression || boolVarExpression) && boolVarExpression);
std::map<storm::expressions::Variable, storm::expressions::Expression> substution = { std::make_pair(manager->getVariable("y"), rationalVarExpression), std::make_pair(manager->getVariable("x"), manager->boolean(true)) };
std::map<storm::expressions::Variable, storm::expressions::Expression> substution = { std::make_pair(manager->getVariable("y"), manager->rational(2.7)), std::make_pair(manager->getVariable("x"), manager->boolean(true)) };
storm::expressions::Expression substitutedExpression;
ASSERT_NO_THROW(substitutedExpression = tempExpression.substitute(substution));
EXPECT_TRUE(substitutedExpression.simplify().isTrue());

Write Preview
Loading…
Cancel
Save