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

fixed bug in DD-based JANI model generation related to transient edge assignments 

Former-commit-id: b2cf168189 [formerly 0c50ca2d16]
Former-commit-id: 05686fd6f1
main
dehnert 9 years ago
parent
011e3fbaa6
commit
91e6bb2999
2 changed files with 5 additions and 5 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Unified View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 8
      src/builder/DdJaniModelBuilder.cpp
  2. 2
      src/generator/JaniNextStateGenerator.cpp

8
src/builder/DdJaniModelBuilder.cpp
View File

@ -895,7 +895,6 @@ namespace storm {
if (action.isInputEnabled()) { if (action.isInputEnabled()) {
// If the action is input-enabled, we add self-loops to all states. // 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); 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 { } else {
transitions *= action.transitions; transitions *= action.transitions;
} }
@ -1107,7 +1106,8 @@ namespace storm {
} }
// Add the source location and the guard. // 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 we multiply the ranges of global variables, make sure everything stays within its bounds.
if (!globalVariablesInSomeDestination.empty()) { if (!globalVariablesInSomeDestination.empty()) {
@ -1124,7 +1124,9 @@ namespace storm {
// Finally treat the transient assignments. // Finally treat the transient assignments.
std::map<storm::expressions::Variable, storm::dd::Add<Type, ValueType>> transientEdgeAssignments; std::map<storm::expressions::Variable, storm::dd::Add<Type, ValueType>> transientEdgeAssignments;
if (!this->transientVariables.empty()) { 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); return EdgeDd(isMarkovian, guard, guard * transitions, transientEdgeAssignments, globalVariablesInSomeDestination);

2
src/generator/JaniNextStateGenerator.cpp
View File

@ -178,14 +178,12 @@ namespace storm {
std::shared_ptr<storm::solver::SmtSolver::ModelReference> model = solver->getModel(); std::shared_ptr<storm::solver::SmtSolver::ModelReference> model = solver->getModel();
for (auto const& booleanVariable : this->variableInformation.booleanVariables) { for (auto const& booleanVariable : this->variableInformation.booleanVariables) {
bool variableValue = model->getBooleanValue(booleanVariable.variable); 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; storm::expressions::Expression localBlockingExpression = variableValue ? !booleanVariable.variable : booleanVariable.variable;
blockingExpression = blockingExpression.isInitialized() ? blockingExpression || localBlockingExpression : localBlockingExpression; blockingExpression = blockingExpression.isInitialized() ? blockingExpression || localBlockingExpression : localBlockingExpression;
initialState.set(booleanVariable.bitOffset, variableValue); initialState.set(booleanVariable.bitOffset, variableValue);
} }
for (auto const& integerVariable : this->variableInformation.integerVariables) { for (auto const& integerVariable : this->variableInformation.integerVariables) {
int_fast64_t variableValue = model->getIntegerValue(integerVariable.variable); 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); storm::expressions::Expression localBlockingExpression = integerVariable.variable != model->getManager().integer(variableValue);
blockingExpression = blockingExpression.isInitialized() ? blockingExpression || localBlockingExpression : localBlockingExpression; blockingExpression = blockingExpression.isInitialized() ? blockingExpression || localBlockingExpression : localBlockingExpression;
initialState.setFromInt(integerVariable.bitOffset, integerVariable.bitWidth, static_cast<uint_fast64_t>(variableValue - integerVariable.lowerBound)); initialState.setFromInt(integerVariable.bitOffset, integerVariable.bitWidth, static_cast<uint_fast64_t>(variableValue - integerVariable.lowerBound));

Write Preview
Loading…
Cancel
Save