From 91e6bb299923773a89fcb9ea649465f7a9283c7c Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Wed, 12 Oct 2016 15:14:47 +0200
Subject: [PATCH] fixed bug in DD-based JANI model generation related to
transient edge assignments
Former-commit-id: b2cf168189706f22201bf54c00cd0f822acbbd14 [formerly 0c50ca2d16cc56b2c1a12db38b6736d79e6780c7]
Former-commit-id: 05686fd6f1b6198355e31940b5b764998047810a
---
src/builder/DdJaniModelBuilder.cpp | 8 +++++---
src/generator/JaniNextStateGenerator.cpp | 2 --
2 files changed, 5 insertions(+), 5 deletions(-)
diff --git a/src/builder/DdJaniModelBuilder.cpp b/src/builder/DdJaniModelBuilder.cpp
index 8b54e0eba..1b759cfc5 100644
--- a/src/builder/DdJaniModelBuilder.cpp
+++ b/src/builder/DdJaniModelBuilder.cpp
@@ -895,7 +895,6 @@ namespace storm {
if (action.isInputEnabled()) {
// If the action is input-enabled, we add self-loops to all states.
transitions *= actionGuard.ite(action.transitions, encodeIndex(0, action.getLowestLocalNondeterminismVariable(), action.getHighestLocalNondeterminismVariable() - action.getLowestLocalNondeterminismVariable(), this->variables) * actionIdentityPair.second);
- actionGuard.ite(action.transitions, encodeIndex(0, action.getLowestLocalNondeterminismVariable(), action.getHighestLocalNondeterminismVariable() - action.getLowestLocalNondeterminismVariable(), this->variables) * actionIdentityPair.second).exportToDot("this.dot");
} else {
transitions *= action.transitions;
}
@@ -1107,7 +1106,8 @@ namespace storm {
}
// Add the source location and the guard.
- transitions *= this->variables.manager->getEncoding(this->variables.automatonToLocationDdVariableMap.at(automaton.getName()).first, edge.getSourceLocationIndex()).template toAdd<ValueType>() * guard;
+ storm::dd::Add<Type, ValueType> sourceLocationAndGuard = this->variables.manager->getEncoding(this->variables.automatonToLocationDdVariableMap.at(automaton.getName()).first, edge.getSourceLocationIndex()).template toAdd<ValueType>() * guard;
+ transitions *= sourceLocationAndGuard;
// If we multiply the ranges of global variables, make sure everything stays within its bounds.
if (!globalVariablesInSomeDestination.empty()) {
@@ -1124,7 +1124,9 @@ namespace storm {
// Finally treat the transient assignments.
std::map<storm::expressions::Variable, storm::dd::Add<Type, ValueType>> transientEdgeAssignments;
if (!this->transientVariables.empty()) {
- performTransientAssignments(edge.getAssignments().getTransientAssignments(), [this, &transientEdgeAssignments, &guard] (storm::jani::Assignment const& assignment) { transientEdgeAssignments[assignment.getExpressionVariable()] = guard * this->variables.rowExpressionAdapter->translateExpression(assignment.getAssignedExpression()); } );
+ performTransientAssignments(edge.getAssignments().getTransientAssignments(), [this, &transientEdgeAssignments, &guard, &sourceLocationAndGuard] (storm::jani::Assignment const& assignment) {
+ transientEdgeAssignments[assignment.getExpressionVariable()] = sourceLocationAndGuard * this->variables.rowExpressionAdapter->translateExpression(assignment.getAssignedExpression());
+ } );
}
return EdgeDd(isMarkovian, guard, guard * transitions, transientEdgeAssignments, globalVariablesInSomeDestination);
diff --git a/src/generator/JaniNextStateGenerator.cpp b/src/generator/JaniNextStateGenerator.cpp
index 10053d777..b2c786b77 100644
--- a/src/generator/JaniNextStateGenerator.cpp
+++ b/src/generator/JaniNextStateGenerator.cpp
@@ -178,14 +178,12 @@ namespace storm {
std::shared_ptr<storm::solver::SmtSolver::ModelReference> model = solver->getModel();
for (auto const& booleanVariable : this->variableInformation.booleanVariables) {
bool variableValue = model->getBooleanValue(booleanVariable.variable);
- std::cout << booleanVariable.variable.getName() << " has val " << variableValue << std::endl;
storm::expressions::Expression localBlockingExpression = variableValue ? !booleanVariable.variable : booleanVariable.variable;
blockingExpression = blockingExpression.isInitialized() ? blockingExpression || localBlockingExpression : localBlockingExpression;
initialState.set(booleanVariable.bitOffset, variableValue);
}
for (auto const& integerVariable : this->variableInformation.integerVariables) {
int_fast64_t variableValue = model->getIntegerValue(integerVariable.variable);
- std::cout << integerVariable.variable.getName() << " has val " << variableValue << std::endl;
storm::expressions::Expression localBlockingExpression = integerVariable.variable != model->getManager().integer(variableValue);
blockingExpression = blockingExpression.isInitialized() ? blockingExpression || localBlockingExpression : localBlockingExpression;
initialState.setFromInt(integerVariable.bitOffset, integerVariable.bitWidth, static_cast<uint_fast64_t>(variableValue - integerVariable.lowerBound));