diff --git a/src/storm/generator/JaniNextStateGenerator.cpp b/src/storm/generator/JaniNextStateGenerator.cpp
index bd034ece7..21b796683 100644
--- a/src/storm/generator/JaniNextStateGenerator.cpp
+++ b/src/storm/generator/JaniNextStateGenerator.cpp
@@ -301,8 +301,8 @@ namespace storm {
return this->outOfBoundsState;
}
} else if (this->options.isExplorationChecksSet()) {
- STORM_LOG_THROW(assignedValue >= intInfo.lowerBound, storm::exceptions::WrongFormatException, "The update " << assignmentIt->getExpressionVariable().getName() << " := " << assignmentIt->getAssignedExpression() << " leads to an out-of-bounds value (" << assignedValue << ") for the variable '" << assignmentIt->getExpressionVariable().getName() << "'.");
- STORM_LOG_THROW(assignedValue <= intInfo.upperBound, storm::exceptions::WrongFormatException, "The update " << assignmentIt->getExpressionVariable().getName() << " := " << assignmentIt->getAssignedExpression() << " leads to an out-of-bounds value (" << assignedValue << ") for the variable '" << assignmentIt->getExpressionVariable().getName() << "'.");
+ STORM_LOG_THROW(assignedValue >= intInfo.lowerBound, storm::exceptions::WrongFormatException, "The update " << assignmentIt->getLValue() << " := " << assignmentIt->getAssignedExpression() << " leads to an out-of-bounds value (" << assignedValue << ") for the variable '" << assignmentIt->getExpressionVariable().getName() << "'.");
+ STORM_LOG_THROW(assignedValue <= intInfo.upperBound, storm::exceptions::WrongFormatException, "The update " << assignmentIt->getLValue() << " := " << assignmentIt->getAssignedExpression() << " leads to an out-of-bounds value (" << assignedValue << ") for the variable '" << assignmentIt->getExpressionVariable().getName() << "'.");
}
newState.setFromInt(intInfo.bitOffset, intInfo.bitWidth, assignedValue - intInfo.lowerBound);
STORM_LOG_ASSERT(static_cast<int_fast64_t>(newState.getAsInt(intInfo.bitOffset, intInfo.bitWidth)) + intInfo.lowerBound == assignedValue, "Writing to the bit vector bucket failed (read " << newState.getAsInt(intInfo.bitOffset, intInfo.bitWidth) << " but wrote " << assignedValue << ").");
@@ -444,16 +444,19 @@ namespace storm {
auto valueIt = stateActionRewards.begin();
performTransientAssignments(destination.getOrderedAssignments().getTransientAssignments(assignmentLevel), *this->evaluator, [&] (ValueType const& value) { *valueIt += (value * probability); ++valueIt; } );
}
- while (assignmentLevel < highestLevel) {
- ++assignmentLevel;
- auto currentLevelEvaluator = storm::expressions::ExpressionEvaluator<ValueType>(model.getManager());
- unpackStateIntoEvaluator(newState, this->variableInformation, currentLevelEvaluator);
- newState = applyUpdate(newState, destination, this->variableInformation.locationVariables[automatonIndex], assignmentLevel, currentLevelEvaluator);
- if (hasTransientRewardAssignments) {
- // update the rewards for this destination
- auto valueIt = stateActionRewards.begin();
- performTransientAssignments(destination.getOrderedAssignments().getTransientAssignments(assignmentLevel), currentLevelEvaluator, [&] (ValueType const& value) { *valueIt += (value * probability); ++valueIt; } );
+ if (assignmentLevel < highestLevel) {
+ while (assignmentLevel < highestLevel) {
+ ++assignmentLevel;
+ unpackStateIntoEvaluator(newState, this->variableInformation, *this->evaluator);
+ newState = applyUpdate(newState, destination, this->variableInformation.locationVariables[automatonIndex], assignmentLevel, *this->evaluator);
+ if (hasTransientRewardAssignments) {
+ // update the rewards for this destination
+ auto valueIt = stateActionRewards.begin();
+ performTransientAssignments(destination.getOrderedAssignments().getTransientAssignments(assignmentLevel), *this->evaluator, [&] (ValueType const& value) { *valueIt += (value * probability); ++valueIt; } );
+ }
}
+ // Restore the old state information
+ unpackStateIntoEvaluator(state, this->variableInformation, *this->evaluator);
}
StateType stateIndex = stateToIdCallback(newState);
@@ -509,17 +512,17 @@ namespace storm {
nextDistribution.clear();
EdgeIndexSet edgeIndices;
- int64_t assignmentLevel = std::numeric_limits<uint64_t>::max();
- int64_t highestLevel = std::numeric_limits<uint64_t>::min();
+ int64_t lowestLevel = std::numeric_limits<int64_t>::max();
+ int64_t highestLevel = std::numeric_limits<int64_t>::min();
for (uint_fast64_t i = 0; i < iteratorList.size(); ++i) {
if (this->getOptions().isBuildChoiceOriginsSet()) {
edgeIndices.insert(model.encodeAutomatonAndEdgeIndices(edgeCombination[i].first, iteratorList[i]->first));
}
- assignmentLevel = std::min(assignmentLevel, iteratorList[i]->second->getLowestAssignmentLevel());
+ lowestLevel = std::min(lowestLevel, iteratorList[i]->second->getLowestAssignmentLevel());
highestLevel = std::max(highestLevel, iteratorList[i]->second->getHighestAssignmentLevel());
}
- if (assignmentLevel >= highestLevel) {
+ if (lowestLevel >= highestLevel) {
// When all assignments have the same level, we can perform the assignments of the different automata sequentially
for (uint_fast64_t i = 0; i < iteratorList.size(); ++i) {
auto const& indexAndEdge = *iteratorList[i];
@@ -536,7 +539,7 @@ namespace storm {
}
for (auto const& stateProbability : currentDistribution) {
// Compute the new state under the current update and add it to the set of new target states.
- CompressedState newTargetState = applyUpdate(stateProbability.getState(), destination, this->variableInformation.locationVariables[edgeCombination[i].first], assignmentLevel, *this->evaluator);
+ CompressedState newTargetState = applyUpdate(stateProbability.getState(), destination, this->variableInformation.locationVariables[edgeCombination[i].first], lowestLevel, *this->evaluator);
// If the new state was already found as a successor state, update the probability
// and insert it.
@@ -597,30 +600,32 @@ namespace storm {
break;
}
- successorState = applyUpdate(successorState, *destinations.back(), *locationVars.back(), assignmentLevel, *this->evaluator);
+ successorState = applyUpdate(successorState, *destinations.back(), *locationVars.back(), lowestLevel, *this->evaluator);
// add the reward for this destination to the destination rewards
auto valueIt = destinationRewards.begin();
- performTransientAssignments(destinations.back()->getOrderedAssignments().getTransientAssignments(assignmentLevel), *this->evaluator, [&valueIt] (ValueType const& value) { *valueIt += value; ++valueIt; } );
+ performTransientAssignments(destinations.back()->getOrderedAssignments().getTransientAssignments(lowestLevel), *this->evaluator, [&valueIt] (ValueType const& value) { *valueIt += value; ++valueIt; } );
}
if (!storm::utility::isZero(successorProbability)) {
+ int64_t assignmentLevel = lowestLevel;
// remaining assignment levels
while (assignmentLevel < highestLevel) {
++assignmentLevel;
- auto currentLevelEvaluator = storm::expressions::ExpressionEvaluator<ValueType>(model.getManager());
- unpackStateIntoEvaluator(successorState, this->variableInformation, currentLevelEvaluator);
+ unpackStateIntoEvaluator(successorState, this->variableInformation, *this->evaluator);
auto locationVarIt = locationVars.begin();
for (auto const& destPtr : destinations) {
- successorState = applyUpdate(successorState, *destPtr, **locationVarIt, assignmentLevel, currentLevelEvaluator);
+ successorState = applyUpdate(successorState, *destPtr, **locationVarIt, assignmentLevel, *this->evaluator);
// add the reward for this destination to the destination rewards
auto valueIt = destinationRewards.begin();
- performTransientAssignments(destinations.back()->getOrderedAssignments().getTransientAssignments(assignmentLevel), currentLevelEvaluator, [&valueIt] (ValueType const& value) { *valueIt += value; ++valueIt; } );
+ performTransientAssignments(destinations.back()->getOrderedAssignments().getTransientAssignments(assignmentLevel), *this->evaluator, [&valueIt] (ValueType const& value) { *valueIt += value; ++valueIt; } );
++locationVarIt;
}
}
nextDistribution.add(successorState, successorProbability);
storm::utility::vector::addScaledVector(stateActionRewards, destinationRewards, successorProbability);
+ // Restore the old state information
+ unpackStateIntoEvaluator(state, this->variableInformation, *this->evaluator);
}
++destinationId;
} while (!lastDestinationId);
diff --git a/src/storm/storage/jani/ArrayEliminator.cpp b/src/storm/storage/jani/ArrayEliminator.cpp
index e04d20d13..16e0c5671 100644
--- a/src/storm/storage/jani/ArrayEliminator.cpp
+++ b/src/storm/storage/jani/ArrayEliminator.cpp
@@ -5,6 +5,9 @@
#include "storm/storage/expressions/ExpressionVisitor.h"
#include "storm/storage/jani/expressions/JaniExpressionVisitor.h"
#include "storm/storage/jani/Variable.h"
+#include "storm/storage/jani/Model.h"
+#include "storm/storage/jani/Property.h"
+#include "storm/storage/jani/traverser/JaniTraverser.h"
#include "storm/storage/jani/traverser/ArrayExpressionFinder.h"
#include "storm/storage/expressions/Expressions.h"
@@ -13,8 +16,12 @@
#include "storm/exceptions/NotSupportedException.h"
#include "storm/exceptions/UnexpectedException.h"
+#include "storm/exceptions/OutOfRangeException.h"
namespace storm {
+
+
+
namespace jani {
namespace detail {
@@ -128,17 +135,42 @@ namespace storm {
storm::expressions::Expression eliminate(storm::expressions::Expression const& expression) {
// here, data is the accessed index of the most recent array access expression. Initially, there is none.
- std::cout << "Eliminating arrays in expression " << expression << std::endl;
auto res = storm::expressions::Expression(boost::any_cast<BaseExprPtr>(expression.accept(*this, boost::any())));
STORM_LOG_ASSERT(!containsArrayExpression(res), "Expression still contains array expressions. Before: " << std::endl << expression << std::endl << "After:" << std::endl << res);
return res.simplify();
}
virtual boost::any visit(storm::expressions::IfThenElseExpression const& expression, boost::any const& data) override {
+ BaseExprPtr thenExpression, elseExpression;
+
+ // We need to handle expressions of the kind '42<size : A[42] : 0', where size is a variable.
+ // If an out of range exception occurrs in the 'then' or the 'else' branch, we assume that the this expression represents the other branch.
+ // TODO: Make this more reliable
+ bool thenOutOfRange(false), elseOutOfRange(false);
+ try {
+ thenExpression = boost::any_cast<BaseExprPtr>(expression.getThenExpression()->accept(*this, data));
+ } catch (storm::exceptions::OutOfRangeException const&) {
+ thenOutOfRange = true;
+ }
+ try {
+ elseExpression = boost::any_cast<BaseExprPtr>(expression.getElseExpression()->accept(*this, data));
+ } catch (storm::exceptions::OutOfRangeException const& e) {
+ if (thenOutOfRange) {
+ throw e;
+ } else {
+ elseOutOfRange = true;
+ }
+ }
+
+ if (thenOutOfRange) {
+ assert(!elseOutOfRange);
+ return elseExpression;
+ } else if (elseOutOfRange) {
+ return thenExpression;
+ }
+
// for the condition expression, outer array accesses should not matter.
BaseExprPtr conditionExpression = boost::any_cast<BaseExprPtr>(expression.getCondition()->accept(*this, boost::any()));
- BaseExprPtr thenExpression = boost::any_cast<BaseExprPtr>(expression.getThenExpression()->accept(*this, data));
- BaseExprPtr elseExpression = boost::any_cast<BaseExprPtr>(expression.getElseExpression()->accept(*this, data));
// If the arguments did not change, we simply push the expression itself.
if (conditionExpression.get() == expression.getCondition().get() && thenExpression.get() == expression.getThenExpression().get() && elseExpression.get() == expression.getElseExpression().get()) {
@@ -193,7 +225,8 @@ namespace storm {
uint64_t index = boost::any_cast<uint64_t>(data);
STORM_LOG_ASSERT(replacements.find(expression.getVariable()) != replacements.end(), "Unable to find array variable " << expression << " in array replacements.");
auto const& arrayVarReplacements = replacements.at(expression.getVariable());
- STORM_LOG_ASSERT(index < arrayVarReplacements.size(), "No replacement for array variable, since index " << index << " is out of bounds.");
+ if (index >= arrayVarReplacements.size()) throw storm::exceptions::OutOfRangeException();
+ //STORM_LOG_THROW(index < arrayVarReplacements.size(), storm::exceptions::OutOfRangeException, "Array index " << index << " for variable " << expression << " is out of bounds.");
return arrayVarReplacements[index]->getExpressionVariable().getExpression().getBaseExpressionPointer();
} else {
STORM_LOG_ASSERT(data.empty(), "VariableExpression of non-array variable should not be a subexpressions of array access expressions. However, the expression " << expression << " is.");
@@ -242,7 +275,8 @@ namespace storm {
STORM_LOG_THROW(!data.empty(), storm::exceptions::NotSupportedException, "Unable to translate ValueArrayExpression to element expression since it does not seem to be within an array access expression.");
uint64_t index = boost::any_cast<uint64_t>(data);
STORM_LOG_ASSERT(expression.size()->isIntegerLiteralExpression(), "unexpected kind of size expression of ValueArrayExpression (" << expression.size()->toExpression() << ").");
- STORM_LOG_THROW(index < static_cast<uint64_t>(expression.size()->evaluateAsInt()), storm::exceptions::UnexpectedException, "Out of bounds array access occured while accessing index " << index << " of expression " << expression);
+ if (index >= static_cast<uint64_t>(expression.size()->evaluateAsInt())) throw storm::exceptions::OutOfRangeException();
+ // STORM_LOG_THROW(index < static_cast<uint64_t>(expression.size()->evaluateAsInt()), storm::exceptions::OutOfRangeException, "Out of bounds array access occured while accessing index " << index << " of expression " << expression);
return boost::any_cast<BaseExprPtr>(expression.at(index)->accept(*this, boost::any()));
}
@@ -252,7 +286,8 @@ namespace storm {
if (expression.size()->containsVariables()) {
STORM_LOG_WARN("Ignoring length of constructorArrayExpression " << expression << " as it still contains variables.");
} else {
- STORM_LOG_THROW(index < static_cast<uint64_t>(expression.size()->evaluateAsInt()), storm::exceptions::UnexpectedException, "Out of bounds array access occured while accessing index " << index << " of expression " << expression);
+ if (index >= static_cast<uint64_t>(expression.size()->evaluateAsInt())) throw storm::exceptions::OutOfRangeException();
+ // STORM_LOG_THROW(index < static_cast<uint64_t>(expression.size()->evaluateAsInt()), storm::exceptions::OutOfRangeException, "Out of bounds array access occured while accessing index " << index << " of expression " << expression);
}
return boost::any_cast<BaseExprPtr>(expression.at(index)->accept(*this, boost::any()));
}
@@ -450,7 +485,6 @@ namespace storm {
if (!insertionRes.second) {
insertionRes.first->second.push_back(&assignment);
}
- continue;
} else {
// Keeping array access LValue
LValue newLValue(LValue(assignment.getLValue().getArray()), arrayExprEliminator->eliminate(assignment.getLValue().getArrayIndex()));
diff --git a/src/storm/storage/jani/ArrayEliminator.h b/src/storm/storage/jani/ArrayEliminator.h
index 70d2fe897..26f4f3df8 100644
--- a/src/storm/storage/jani/ArrayEliminator.h
+++ b/src/storm/storage/jani/ArrayEliminator.h
@@ -1,13 +1,17 @@
#pragma once
-#include <boost/any.hpp>
-
-#include "storm/storage/jani/traverser/JaniTraverser.h"
-#include "storm/storage/jani/Property.h"
+#include "storm/storage/jani/Variable.h"
+#include "storm/storage/expressions/Variable.h"
namespace storm {
+ namespace expressions {
+ class Expression;
+ }
+
namespace jani {
+ class Model;
+ class Property;
struct ArrayEliminatorData {
std::vector<std::shared_ptr<ArrayVariable>> eliminatedArrayVariables;
@@ -29,9 +33,6 @@ namespace storm {
ArrayEliminatorData eliminate(Model& model, bool keepNonTrivialArrayAccess = false);
- private:
-
-
};
}
}
diff --git a/src/storm/storage/jani/Edge.cpp b/src/storm/storage/jani/Edge.cpp
index 240317817..301c695a0 100644
--- a/src/storm/storage/jani/Edge.cpp
+++ b/src/storm/storage/jani/Edge.cpp
@@ -147,6 +147,33 @@ namespace storm {
return templateEdge;
}
-
+ std::ostream& operator<<(std::ostream& stream, Edge const& edge) {
+ stream << "[" << (edge.hasSilentAction() ? "" : ("action_id: " + std::to_string(edge.getActionIndex()))) << "]";
+ stream << "guard: '" << edge.getGuard() << "'\t from_location_id: " << edge.getSourceLocationIndex();
+ if (edge.hasRate()) {
+ stream << " with rate '" << edge.getRate() << "'";
+ }
+ if (edge.getDestinations().empty()) {
+ stream << "without any destination";
+ } else {
+ stream << " to ... [" << std::endl;
+ for (auto const& dest : edge.getDestinations()) {
+ stream << "\tlocation_id: " << dest.getLocationIndex() << " with probability '" << dest.getProbability() << "' and updates: ";
+ if (dest.getOrderedAssignments().empty()) {
+ stream << "none" << std::endl;
+ }
+ bool first = true;
+ for (auto const& a : dest.getOrderedAssignments()) {
+ if (first) {
+ first = false;
+ stream << a;
+ }
+ stream << ", " << a;
+ }
+ }
+ stream << "]";
+ }
+ return stream;
+ }
}
}
diff --git a/src/storm/storage/jani/Edge.h b/src/storm/storage/jani/Edge.h
index c6ab6d28d..36abaa5f3 100644
--- a/src/storm/storage/jani/Edge.h
+++ b/src/storm/storage/jani/Edge.h
@@ -4,6 +4,7 @@
#include <boost/optional.hpp>
#include <boost/container/flat_set.hpp>
+#include <iostream>
#include "storm/storage/jani/EdgeDestination.h"
#include "storm/storage/jani/OrderedAssignments.h"
@@ -152,5 +153,8 @@ namespace storm {
std::vector<EdgeDestination> destinations;
};
+ std::ostream& operator<<(std::ostream& stream, Edge const& edge);
+
+
}
}
diff --git a/src/storm/storage/jani/traverser/ArrayExpressionFinder.cpp b/src/storm/storage/jani/traverser/ArrayExpressionFinder.cpp
index 8e5d11a92..8ade7df61 100644
--- a/src/storm/storage/jani/traverser/ArrayExpressionFinder.cpp
+++ b/src/storm/storage/jani/traverser/ArrayExpressionFinder.cpp
@@ -104,7 +104,7 @@ namespace storm {
bool containsArrayExpression(storm::expressions::Expression const& expression) {
detail::ArrayExpressionFinderExpressionVisitor v;
- return boost::any_cast<bool>(expression.accept(v, boost::none));
+ return boost::any_cast<bool>(expression.accept(v, boost::any()));
}
}
}