From 011e3fbaa65c06f67a9ca1258bfc444848bd62a4 Mon Sep 17 00:00:00 2001 From: dehnert Date: Wed, 12 Oct 2016 13:54:29 +0200 Subject: [PATCH 1/3] fixed bug that introduced transient variables in the state space Former-commit-id: b335cf0c0dae3be17160ec6ca44a29c72996b6f9 [formerly 84339f7943cc25252bd8ccd6addc84401e643d2c] Former-commit-id: 6f64020873265b23e9af9cc6c816045ec13d2ce8 --- src/generator/JaniNextStateGenerator.cpp | 4 ++- src/generator/VariableInformation.cpp | 36 +++++++++++++++--------- 2 files changed, 25 insertions(+), 15 deletions(-) diff --git a/src/generator/JaniNextStateGenerator.cpp b/src/generator/JaniNextStateGenerator.cpp index bc166cba3..10053d777 100644 --- a/src/generator/JaniNextStateGenerator.cpp +++ b/src/generator/JaniNextStateGenerator.cpp @@ -178,17 +178,19 @@ namespace storm { std::shared_ptr 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(variableValue - integerVariable.lowerBound)); } - + // Gather iterators to the initial locations of all the automata. std::vector::const_iterator> initialLocationsIterators; uint64_t currentLocationVariable = 0; diff --git a/src/generator/VariableInformation.cpp b/src/generator/VariableInformation.cpp index c1a00e4e6..3545f1e49 100644 --- a/src/generator/VariableInformation.cpp +++ b/src/generator/VariableInformation.cpp @@ -63,15 +63,19 @@ namespace storm { } for (auto const& variable : model.getGlobalVariables().getBooleanVariables()) { - booleanVariables.emplace_back(variable.getExpressionVariable(), totalBitOffset, true); - ++totalBitOffset; + if (!variable.isTransient()) { + booleanVariables.emplace_back(variable.getExpressionVariable(), totalBitOffset, true); + ++totalBitOffset; + } } for (auto const& variable : model.getGlobalVariables().getBoundedIntegerVariables()) { - int_fast64_t lowerBound = variable.getLowerBound().evaluateAsInt(); - int_fast64_t upperBound = variable.getUpperBound().evaluateAsInt(); - uint_fast64_t bitwidth = static_cast(std::ceil(std::log2(upperBound - lowerBound + 1))); - integerVariables.emplace_back(variable.getExpressionVariable(), lowerBound, upperBound, totalBitOffset, bitwidth, true); - totalBitOffset += bitwidth; + if (!variable.isTransient()) { + int_fast64_t lowerBound = variable.getLowerBound().evaluateAsInt(); + int_fast64_t upperBound = variable.getUpperBound().evaluateAsInt(); + uint_fast64_t bitwidth = static_cast(std::ceil(std::log2(upperBound - lowerBound + 1))); + integerVariables.emplace_back(variable.getExpressionVariable(), lowerBound, upperBound, totalBitOffset, bitwidth, true); + totalBitOffset += bitwidth; + } } for (auto const& automaton : model.getAutomata()) { uint_fast64_t bitwidth = static_cast(std::ceil(std::log2(automaton.getNumberOfLocations()))); @@ -79,15 +83,19 @@ namespace storm { totalBitOffset += bitwidth; for (auto const& variable : automaton.getVariables().getBooleanVariables()) { - booleanVariables.emplace_back(variable.getExpressionVariable(), totalBitOffset); - ++totalBitOffset; + if (!variable.isTransient()) { + booleanVariables.emplace_back(variable.getExpressionVariable(), totalBitOffset); + ++totalBitOffset; + } } for (auto const& variable : automaton.getVariables().getBoundedIntegerVariables()) { - int_fast64_t lowerBound = variable.getLowerBound().evaluateAsInt(); - int_fast64_t upperBound = variable.getUpperBound().evaluateAsInt(); - uint_fast64_t bitwidth = static_cast(std::ceil(std::log2(upperBound - lowerBound + 1))); - integerVariables.emplace_back(variable.getExpressionVariable(), lowerBound, upperBound, totalBitOffset, bitwidth); - totalBitOffset += bitwidth; + if (!variable.isTransient()) { + int_fast64_t lowerBound = variable.getLowerBound().evaluateAsInt(); + int_fast64_t upperBound = variable.getUpperBound().evaluateAsInt(); + uint_fast64_t bitwidth = static_cast(std::ceil(std::log2(upperBound - lowerBound + 1))); + integerVariables.emplace_back(variable.getExpressionVariable(), lowerBound, upperBound, totalBitOffset, bitwidth); + totalBitOffset += bitwidth; + } } } From 91e6bb299923773a89fcb9ea649465f7a9283c7c Mon Sep 17 00:00:00 2001 From: dehnert Date: Wed, 12 Oct 2016 15:14:47 +0200 Subject: [PATCH 2/3] 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() * guard; + storm::dd::Add sourceLocationAndGuard = this->variables.manager->getEncoding(this->variables.automatonToLocationDdVariableMap.at(automaton.getName()).first, edge.getSourceLocationIndex()).template toAdd() * 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> 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 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(variableValue - integerVariable.lowerBound)); From ba0d81ca52172d4bd68fbf10c7a60a3714dc29d2 Mon Sep 17 00:00:00 2001 From: dehnert Date: Wed, 12 Oct 2016 21:13:09 +0200 Subject: [PATCH 3/3] bugfix for PRISM program: only check initial values of variables if they have one Former-commit-id: c5c548bd62f28b1d2cdc70bb75f7c84d12233c62 [formerly c27c72bd59e9f07a05cb8e9c5f56b65906ff7a2f] Former-commit-id: 97acb66693b15d0464a7dbc15c70a13c73f60f10 --- src/storage/prism/Module.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/storage/prism/Module.cpp b/src/storage/prism/Module.cpp index 095ac3e11..0a4347396 100644 --- a/src/storage/prism/Module.cpp +++ b/src/storage/prism/Module.cpp @@ -196,12 +196,12 @@ namespace storm { bool Module::containsVariablesOnlyInUpdateProbabilities(std::set const& undefinedConstantVariables) const { for (auto const& booleanVariable : this->getBooleanVariables()) { - if (booleanVariable.getInitialValueExpression().containsVariable(undefinedConstantVariables)) { + if (booleanVariable.hasInitialValue() && booleanVariable.getInitialValueExpression().containsVariable(undefinedConstantVariables)) { return false; } } for (auto const& integerVariable : this->getIntegerVariables()) { - if (integerVariable.getInitialValueExpression().containsVariable(undefinedConstantVariables)) { + if (integerVariable.hasInitialValue() && integerVariable.getInitialValueExpression().containsVariable(undefinedConstantVariables)) { return false; } if (integerVariable.getLowerBoundExpression().containsVariable(undefinedConstantVariables)) {