From 011e3fbaa65c06f67a9ca1258bfc444848bd62a4 Mon Sep 17 00:00:00 2001 From: dehnert Date: Wed, 12 Oct 2016 13:54:29 +0200 Subject: [PATCH] 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; + } } }