From b8b84e3f8a54d75f8b361686a26839c8b8cb7567 Mon Sep 17 00:00:00 2001 From: TimQu Date: Tue, 25 Sep 2018 13:44:33 +0200 Subject: [PATCH] support for *local* unbounded integer variables. --- src/storm/generator/VariableInformation.cpp | 130 +++++++++----------- src/storm/generator/VariableInformation.h | 8 +- 2 files changed, 68 insertions(+), 70 deletions(-) diff --git a/src/storm/generator/VariableInformation.cpp b/src/storm/generator/VariableInformation.cpp index 1f156cd8b..3bc1d7d8b 100644 --- a/src/storm/generator/VariableInformation.cpp +++ b/src/storm/generator/VariableInformation.cpp @@ -69,11 +69,9 @@ namespace storm { } VariableInformation::VariableInformation(storm::jani::Model const& model, std::vector> const& parallelAutomata, uint64_t reservedBitsForUnboundedVariables, bool outOfBoundsState) : totalBitOffset(0) { - // Check that the model does not contain non-transient unbounded integer or non-transient real variables. + // Check that the model does not contain non-transient real variables. STORM_LOG_THROW(!model.getGlobalVariables().containsNonTransientRealVariables(), storm::exceptions::InvalidArgumentException, "Cannot build model from JANI model that contains global non-transient real variables."); - STORM_LOG_THROW(!model.getGlobalVariables().containsNonTransientUnboundedIntegerVariables(), storm::exceptions::InvalidArgumentException, "Cannot build model from JANI model that contains non-transient unbounded integer variables."); for (auto const& automaton : model.getAutomata()) { - STORM_LOG_THROW(!automaton.getVariables().containsNonTransientUnboundedIntegerVariables(), storm::exceptions::InvalidArgumentException, "Cannot build model from JANI model that contains non-transient unbounded integer variables in automaton '" << automaton.getName() << "'."); STORM_LOG_THROW(!automaton.getVariables().containsNonTransientRealVariables(), storm::exceptions::InvalidArgumentException, "Cannot build model from JANI model that contains non-transient real variables in automaton '" << automaton.getName() << "'."); } if (outOfBoundsState) { @@ -83,44 +81,10 @@ namespace storm { outOfBoundsBit = boost::none; } - for (auto const& variable : model.getGlobalVariables().getBooleanVariables()) { - if (!variable.isTransient()) { - booleanVariables.emplace_back(variable.getExpressionVariable(), totalBitOffset, true); - ++totalBitOffset; - } - } - for (auto const& variable : model.getGlobalVariables().getBoundedIntegerVariables()) { - if (!variable.isTransient()) { - int64_t lowerBound; - int64_t upperBound; - if (variable.hasLowerBound()) { - lowerBound = variable.getLowerBound().evaluateAsInt(); - if (variable.hasUpperBound()) { - upperBound = variable.getUpperBound().evaluateAsInt(); - } else { - upperBound = lowerBound + ((1u << reservedBitsForUnboundedVariables) - 1); - } - } else { - STORM_LOG_THROW(variable.hasUpperBound(), storm::exceptions::WrongFormatException, "Bounded integer variable has neither a lower nor an upper bound."); - upperBound = variable.getUpperBound().evaluateAsInt(); - lowerBound = upperBound - ((1u << reservedBitsForUnboundedVariables) - 1); - } - uint_fast64_t bitwidth = static_cast(std::ceil(std::log2(upperBound - lowerBound + 1))); - integerVariables.emplace_back(variable.getExpressionVariable(), lowerBound, upperBound, totalBitOffset, bitwidth, true, !variable.hasLowerBound() || !variable.hasUpperBound()); - totalBitOffset += bitwidth; - } - } - for (auto const& variable : model.getGlobalVariables().getUnboundedIntegerVariables()) { - if (!variable.isTransient()) { - int64_t lowerBound = - (1u << (reservedBitsForUnboundedVariables - 1)); - int64_t upperBound = (1u << (reservedBitsForUnboundedVariables - 1)) - 1; - integerVariables.emplace_back(variable.getExpressionVariable(), lowerBound, upperBound, totalBitOffset, reservedBitsForUnboundedVariables, true, true); - totalBitOffset += reservedBitsForUnboundedVariables; - } - } + createVariablesForVariableSet(model.getGlobalVariables(), reservedBitsForUnboundedVariables, true); for (auto const& automatonRef : parallelAutomata) { - createVariablesForAutomaton(automatonRef.get()); + createVariablesForAutomaton(automatonRef.get(), reservedBitsForUnboundedVariables); } sortVariables(); @@ -129,34 +93,38 @@ namespace storm { void VariableInformation::registerArrayVariableReplacements(storm::jani::ArrayEliminatorData const& arrayEliminatorData) { arrayVariableToElementInformations.clear(); // Find for each replaced array variable the corresponding references in this variable information - for (auto const& arrayReplacements : arrayEliminatorData.replacements) { - std::vector varInfoIndices; - for (auto const& replacedVar : arrayReplacements.second) { - if (replacedVar->getExpressionVariable().hasIntegerType()) { - uint64_t index = 0; - for (auto const& intInfo : integerVariables) { - if (intInfo.variable == replacedVar->getExpressionVariable()) { - varInfoIndices.push_back(index); - break; + for (auto const& arrayVariable : arrayEliminatorData.eliminatedArrayVariables) { + if (!arrayVariable->isTransient()) { + STORM_LOG_ASSERT(arrayEliminatorData.replacements.count(arrayVariable->getExpressionVariable()) > 0, "No replacement for array variable."); + auto const& replacements = arrayEliminatorData.replacements.find(arrayVariable->getExpressionVariable())->second; + std::vector varInfoIndices; + for (auto const& replacedVar : replacements) { + if (replacedVar->getExpressionVariable().hasIntegerType()) { + uint64_t index = 0; + for (auto const& intInfo : integerVariables) { + if (intInfo.variable == replacedVar->getExpressionVariable()) { + varInfoIndices.push_back(index); + break; + } + ++index; } - ++index; - } - STORM_LOG_ASSERT(!varInfoIndices.empty() && varInfoIndices.back() == index, "Could not find a basic variable for replacement of array variable " << replacedVar->getExpressionVariable().getName() << " ."); - } else if (replacedVar->getExpressionVariable().hasBooleanType()) { - uint64_t index = 0; - for (auto const& boolInfo : booleanVariables) { - if (boolInfo.variable == replacedVar->getExpressionVariable()) { - varInfoIndices.push_back(index); - break; + STORM_LOG_ASSERT(!varInfoIndices.empty() && varInfoIndices.back() == index, "Could not find a basic variable for replacement of array variable " << replacedVar->getExpressionVariable().getName() << " ."); + } else if (replacedVar->getExpressionVariable().hasBooleanType()) { + uint64_t index = 0; + for (auto const& boolInfo : booleanVariables) { + if (boolInfo.variable == replacedVar->getExpressionVariable()) { + varInfoIndices.push_back(index); + break; + } + ++index; } - ++index; + STORM_LOG_ASSERT(!varInfoIndices.empty() && varInfoIndices.back() == index, "Could not find a basic variable for replacement of array variable " << replacedVar->getExpressionVariable().getName() << " ."); + } else { + STORM_LOG_ASSERT(false, "Unhandled type of base variable."); } - STORM_LOG_ASSERT(!varInfoIndices.empty() && varInfoIndices.back() == index, "Could not find a basic variable for replacement of array variable " << replacedVar->getExpressionVariable().getName() << " ."); - } else { - STORM_LOG_ASSERT(false, "Unhandled type of base variable."); } + this->arrayVariableToElementInformations.emplace(arrayVariable->getExpressionVariable(), std::move(varInfoIndices)); } - this->arrayVariableToElementInformations.emplace(arrayReplacements.first, std::move(varInfoIndices)); } } @@ -172,26 +140,50 @@ namespace storm { return integerVariables[intInfoIndices[arrayIndex]]; } - void VariableInformation::createVariablesForAutomaton(storm::jani::Automaton const& automaton) { + void VariableInformation::createVariablesForAutomaton(storm::jani::Automaton const& automaton, uint64_t reservedBitsForUnboundedVariables) { uint_fast64_t bitwidth = static_cast(std::ceil(std::log2(automaton.getNumberOfLocations()))); locationVariables.emplace_back(automaton.getLocationExpressionVariable(), automaton.getNumberOfLocations() - 1, totalBitOffset, bitwidth); totalBitOffset += bitwidth; - for (auto const& variable : automaton.getVariables().getBooleanVariables()) { + createVariablesForVariableSet(automaton.getVariables(), reservedBitsForUnboundedVariables, false); + } + + void VariableInformation::createVariablesForVariableSet(storm::jani::VariableSet const& variableSet, uint64_t reservedBitsForUnboundedVariables, bool global) { + for (auto const& variable : variableSet.getBooleanVariables()) { if (!variable.isTransient()) { - booleanVariables.emplace_back(variable.getExpressionVariable(), totalBitOffset); + booleanVariables.emplace_back(variable.getExpressionVariable(), totalBitOffset, global); ++totalBitOffset; } } - for (auto const& variable : automaton.getVariables().getBoundedIntegerVariables()) { + for (auto const& variable : variableSet.getBoundedIntegerVariables()) { if (!variable.isTransient()) { - int_fast64_t lowerBound = variable.getLowerBound().evaluateAsInt(); - int_fast64_t upperBound = variable.getUpperBound().evaluateAsInt(); + int64_t lowerBound; + int64_t upperBound; + if (variable.hasLowerBound()) { + lowerBound = variable.getLowerBound().evaluateAsInt(); + if (variable.hasUpperBound()) { + upperBound = variable.getUpperBound().evaluateAsInt(); + } else { + upperBound = lowerBound + ((1u << reservedBitsForUnboundedVariables) - 1); + } + } else { + STORM_LOG_THROW(variable.hasUpperBound(), storm::exceptions::WrongFormatException, "Bounded integer variable has neither a lower nor an upper bound."); + upperBound = variable.getUpperBound().evaluateAsInt(); + lowerBound = upperBound - ((1u << reservedBitsForUnboundedVariables) - 1); + } uint_fast64_t bitwidth = static_cast(std::ceil(std::log2(upperBound - lowerBound + 1))); - integerVariables.emplace_back(variable.getExpressionVariable(), lowerBound, upperBound, totalBitOffset, bitwidth); + integerVariables.emplace_back(variable.getExpressionVariable(), lowerBound, upperBound, totalBitOffset, bitwidth, global, !variable.hasLowerBound() || !variable.hasUpperBound()); totalBitOffset += bitwidth; } } + for (auto const& variable : variableSet.getUnboundedIntegerVariables()) { + if (!variable.isTransient()) { + int64_t lowerBound = - (1u << (reservedBitsForUnboundedVariables - 1)); + int64_t upperBound = (1u << (reservedBitsForUnboundedVariables - 1)) - 1; + integerVariables.emplace_back(variable.getExpressionVariable(), lowerBound, upperBound, totalBitOffset, reservedBitsForUnboundedVariables, global, true); + totalBitOffset += reservedBitsForUnboundedVariables; + } + } } uint_fast64_t VariableInformation::getTotalBitOffset(bool roundTo64Bit) const { diff --git a/src/storm/generator/VariableInformation.h b/src/storm/generator/VariableInformation.h index 7189e3335..0326e8d0c 100644 --- a/src/storm/generator/VariableInformation.h +++ b/src/storm/generator/VariableInformation.h @@ -17,6 +17,7 @@ namespace storm { class Model; class Automaton; class ArrayEliminatorData; + class VariableSet; } namespace generator { @@ -120,7 +121,12 @@ namespace storm { /*! * Creates all necessary variables for a JANI automaton. */ - void createVariablesForAutomaton(storm::jani::Automaton const& automaton); + void createVariablesForAutomaton(storm::jani::Automaton const& automaton, uint64_t reservedBitsForUnboundedVariables); + + /*! + * Creates all non-transient variables from the given set + */ + void createVariablesForVariableSet(storm::jani::VariableSet const& variableSet, uint64_t reservedBitsForUnboundedVariables, bool global); }; }