Browse Source

Merge branch 'master' into deterministicScheds

tempestpy_adaptions
Tim Quatmann 5 years ago
parent
commit
63fe1c01d1
  1. 2
      README.md
  2. 4
      src/storm-parsers/parser/ExpressionParser.cpp
  3. 2
      src/storm/storage/expressions/ToRationalFunctionVisitor.cpp
  4. 2
      src/test/storm/transformer/EndComponentEliminatorTest.cpp

2
README.md

@ -11,7 +11,7 @@ Benchmarks
Example input files for Storm can be obtained from Example input files for Storm can be obtained from
https://github.com/moves-rwth/storm-examples. https://github.com/moves-rwth/storm-examples.
Various Benchmarks together with example invocations of Storm can be found at the [Quantitative Verification Benchmark Suite (QVBS)](http://qcomp.org/benchmarks).
Various Benchmarks together with example invocations of Storm can be found at the [Quantitative Verification Benchmark Set (QVBS)](http://qcomp.org/benchmarks).
Further examples and benchmarks can be found in the following repositories: Further examples and benchmarks can be found in the following repositories:

4
src/storm-parsers/parser/ExpressionParser.cpp

@ -91,9 +91,9 @@ namespace storm {
unaryExpression.name("unary expression"); unaryExpression.name("unary expression");
if (allowBacktracking) { if (allowBacktracking) {
infixPowerModuloExpression = unaryExpression[qi::_val = qi::_1] >> -(infixPowerModuloOperator_ >> expression)[qi::_val = phoenix::bind(&ExpressionCreator::createPowerModuloExpression, phoenix::ref(*expressionCreator), qi::_val, qi::_1, qi::_2, qi::_pass)];
infixPowerModuloExpression = unaryExpression[qi::_val = qi::_1] >> -(infixPowerModuloOperator_ >> unaryExpression)[qi::_val = phoenix::bind(&ExpressionCreator::createPowerModuloExpression, phoenix::ref(*expressionCreator), qi::_val, qi::_1, qi::_2, qi::_pass)];
} else { } else {
infixPowerModuloExpression = unaryExpression[qi::_val = qi::_1] > -(infixPowerModuloOperator_ >> expression)[qi::_val = phoenix::bind(&ExpressionCreator::createPowerModuloExpression, phoenix::ref(*expressionCreator), qi::_val, qi::_1, qi::_2, qi::_pass)];
infixPowerModuloExpression = unaryExpression[qi::_val = qi::_1] > -(infixPowerModuloOperator_ >> unaryExpression)[qi::_val = phoenix::bind(&ExpressionCreator::createPowerModuloExpression, phoenix::ref(*expressionCreator), qi::_val, qi::_1, qi::_2, qi::_pass)];
} }
infixPowerModuloExpression.name("(infix) power/modulo expression"); infixPowerModuloExpression.name("(infix) power/modulo expression");

2
src/storm/storage/expressions/ToRationalFunctionVisitor.cpp

@ -54,7 +54,7 @@ namespace storm {
return firstOperandAsRationalFunction / secondOperandAsRationalFunction; return firstOperandAsRationalFunction / secondOperandAsRationalFunction;
break; break;
case BinaryNumericalFunctionExpression::OperatorType::Power: case BinaryNumericalFunctionExpression::OperatorType::Power:
STORM_LOG_THROW(storm::utility::isInteger(secondOperandAsRationalFunction), storm::exceptions::InvalidArgumentException, "Exponent of power operator must be a positive integer.");
STORM_LOG_THROW(storm::utility::isInteger(secondOperandAsRationalFunction), storm::exceptions::InvalidArgumentException, "Exponent of power operator must be a positive integer but is " << secondOperandAsRationalFunction << ".");
exponentAsInteger = storm::utility::convertNumber<uint_fast64_t>(secondOperandAsRationalFunction); exponentAsInteger = storm::utility::convertNumber<uint_fast64_t>(secondOperandAsRationalFunction);
return storm::utility::pow(firstOperandAsRationalFunction, exponentAsInteger); return storm::utility::pow(firstOperandAsRationalFunction, exponentAsInteger);
break; break;

2
src/test/storm/transformer/EndComponentEliminatorTest.cpp

@ -98,7 +98,7 @@ TEST(NeutralECRemover, SimpleModelTest) {
ASSERT_LT(expectedNewState, std::numeric_limits<uint_fast64_t>::max()) << " Mapping does not match for oldState " << oldState; ASSERT_LT(expectedNewState, std::numeric_limits<uint_fast64_t>::max()) << " Mapping does not match for oldState " << oldState;
actualToExpectedStateMapping[actualNewState] = expectedNewState; actualToExpectedStateMapping[actualNewState] = expectedNewState;
} else { } else {
ASSERT_LT(expectedNewState, actualNewState) << " Mapping does not match for oldState " << oldState;
ASSERT_EQ(expectedNewState, actualNewState) << " Mapping does not match for oldState " << oldState;
} }
} }
std::vector<uint64_t> actualToExpectedRowMapping; std::vector<uint64_t> actualToExpectedRowMapping;

Loading…
Cancel
Save