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

support for *local* unbounded integer variables.

tempestpy_adaptions
TimQu 6 years ago
parent
949bc4cb65
commit
b8b84e3f8a
2 changed files with 68 additions and 70 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 130
      src/storm/generator/VariableInformation.cpp
  2. 8
      src/storm/generator/VariableInformation.h

130
src/storm/generator/VariableInformation.cpp
View File

@ -69,11 +69,9 @@ namespace storm {
}
VariableInformation::VariableInformation(storm::jani::Model const& model, std::vector<std::reference_wrapper<storm::jani::Automaton const>> 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<uint_fast64_t>(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<uint64_t> 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<uint64_t> 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<uint_fast64_t>(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<uint_fast64_t>(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 {

8
src/storm/generator/VariableInformation.h
View File

@ -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);
};
}

Write Preview
Loading…
Cancel
Save