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

Merge branch 'master' into LRA_for_dtmc_mdp 

Former-commit-id: 2a78b1e8ae
tempestpy_adaptions
David_Korzeniewski 10 years ago
parent
7e672cddd9 96539f41a5
commit
bc1a97e38a
4 changed files with 17 additions and 7 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. 13
      src/builder/ExplicitPrismModelBuilder.cpp
  2. 7
      src/storage/expressions/BinaryNumericalFunctionExpression.cpp
  3. 2
      src/storage/expressions/UnaryNumericalFunctionExpression.cpp
  4. 2
      src/storage/prism/BooleanVariable.cpp

13
src/builder/ExplicitPrismModelBuilder.cpp
View File

@ -127,6 +127,7 @@ namespace storm {
// all expressions in the program so we can then evaluate them without having to store the values of the
// constants in the state (i.e., valuation).
preparedProgram = preparedProgram.substituteConstants();
storm::prism::RewardModel rewardModel = storm::prism::RewardModel();
// Select the appropriate reward model.
@ -564,7 +565,11 @@ namespace storm {
}
for (auto const& stateProbabilityPair : choice) {
globalChoice.getOrAddEntry(stateProbabilityPair.first) += stateProbabilityPair.second / totalNumberOfChoices;
if (discreteTimeModel) {
globalChoice.getOrAddEntry(stateProbabilityPair.first) += stateProbabilityPair.second / totalNumberOfChoices;
} else {
globalChoice.getOrAddEntry(stateProbabilityPair.first) += stateProbabilityPair.second;
}
// Now add all rewards that match this choice.
for (auto const& transitionReward : transitionRewards) {
@ -580,7 +585,11 @@ namespace storm {
}
for (auto const& stateProbabilityPair : choice) {
globalChoice.getOrAddEntry(stateProbabilityPair.first) += stateProbabilityPair.second / totalNumberOfChoices;
if (discreteTimeModel) {
globalChoice.getOrAddEntry(stateProbabilityPair.first) += stateProbabilityPair.second / totalNumberOfChoices;
} else {
globalChoice.getOrAddEntry(stateProbabilityPair.first) += stateProbabilityPair.second;
}
// Now add all rewards that match this choice.
for (auto const& transitionReward : transitionRewards) {

7
src/storage/expressions/BinaryNumericalFunctionExpression.cpp
View File

@ -6,6 +6,7 @@
#include "src/storage/expressions/DoubleLiteralExpression.h"
#include "src/utility/macros.h"
#include "src/exceptions/InvalidTypeException.h"
#include "src/exceptions/InvalidStateException.h"
namespace storm {
namespace expressions {
@ -65,7 +66,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() && this->getOperatorType() != OperatorType::Divide) {
if (this->hasIntegerType()) {
int_fast64_t firstOperandEvaluation = firstOperandSimplified->evaluateAsInt();
int_fast64_t secondOperandEvaluation = secondOperandSimplified->evaluateAsInt();
@ -74,10 +75,10 @@ namespace storm {
case OperatorType::Plus: newValue = firstOperandEvaluation + secondOperandEvaluation; break;
case OperatorType::Minus: newValue = firstOperandEvaluation - secondOperandEvaluation; break;
case OperatorType::Times: newValue = firstOperandEvaluation * secondOperandEvaluation; break;
case OperatorType::Divide: 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::Divide: STORM_LOG_THROW(false, storm::exceptions::InvalidStateException, "Unable to simplify division."); break;
}
return std::shared_ptr<BaseExpression>(new IntegerLiteralExpression(this->getManager(), newValue));
} else if (this->hasRationalType()) {
@ -88,10 +89,10 @@ namespace storm {
case OperatorType::Plus: newValue = firstOperandEvaluation + secondOperandEvaluation; break;
case OperatorType::Minus: newValue = firstOperandEvaluation - secondOperandEvaluation; break;
case OperatorType::Times: newValue = firstOperandEvaluation * secondOperandEvaluation; break;
case OperatorType::Divide: 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::Divide: STORM_LOG_THROW(false, storm::exceptions::InvalidStateException, "Unable to simplify division."); break;
}
return std::shared_ptr<BaseExpression>(new DoubleLiteralExpression(this->getManager(), newValue));
}

2
src/storage/expressions/UnaryNumericalFunctionExpression.cpp
View File

@ -76,7 +76,7 @@ namespace storm {
case OperatorType::Floor: value = std::floor(boost::get<double>(operandEvaluation)); break;
case OperatorType::Ceil: value = std::ceil(boost::get<double>(operandEvaluation)); break;
}
return std::shared_ptr<BaseExpression>(new DoubleLiteralExpression(this->getManager(), boost::get<double>(result)));
return std::shared_ptr<BaseExpression>(new DoubleLiteralExpression(this->getManager(), value));
}
}

2
src/storage/prism/BooleanVariable.cpp
View File

@ -11,7 +11,7 @@ namespace storm {
}
std::ostream& operator<<(std::ostream& stream, BooleanVariable const& variable) {
stream << variable.getName() << ": bool init" << variable.getInitialValueExpression() << ";";
stream << variable.getName() << ": bool init " << variable.getInitialValueExpression() << ";";
return stream;
}

Write Preview
Loading…
Cancel
Save