diff --git a/src/storm-cli-utilities/model-handling.h b/src/storm-cli-utilities/model-handling.h index bcdf2be6e8..6bbfe942b8 100644 --- a/src/storm-cli-utilities/model-handling.h +++ b/src/storm-cli-utilities/model-handling.h @@ -612,6 +612,7 @@ std::shared_ptr buildModelExplicit(storm::settings::mo storm::umb::ImportOptions options; options.buildChoiceLabeling = buildSettings.isBuildChoiceLabelsSet(); options.buildStateValuations = buildSettings.isBuildStateValuationsSet(); + options.buildObservationValuations = buildSettings.isBuildObservationValuationsSet(); if constexpr (std::is_same_v) { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "RationalFunction currently not supported for UMB models."); } else if constexpr (std::is_same_v) { diff --git a/src/storm-counterexamples/counterexamples/PathCounterexample.cpp b/src/storm-counterexamples/counterexamples/PathCounterexample.cpp index e604ae5ac7..0d161b3a3a 100644 --- a/src/storm-counterexamples/counterexamples/PathCounterexample.cpp +++ b/src/storm-counterexamples/counterexamples/PathCounterexample.cpp @@ -26,7 +26,7 @@ void PathCounterexample::writeToStream(std::ostream& out) const { for (auto it = shortestPaths[i].rbegin(); it != shortestPaths[i].rend(); ++it) { out << "\tstate " << *it; if (model->hasStateValuations()) { - out << ": " << model->getStateValuations().getStateInfo(*it); + out << ": " << model->getStateValuations().toString(*it); } out << ": {"; storm::io::outputFixedWidth(out, model->getLabelsOfState(*it), 0); diff --git a/src/storm-pars/transformer/BinaryDtmcTransformer.cpp b/src/storm-pars/transformer/BinaryDtmcTransformer.cpp index a49b40da71..2b721ac338 100644 --- a/src/storm-pars/transformer/BinaryDtmcTransformer.cpp +++ b/src/storm-pars/transformer/BinaryDtmcTransformer.cpp @@ -24,7 +24,7 @@ std::shared_ptr> BinaryDtmcTransfo } components.transitionMatrix = std::move(data.simpleMatrix); if (keepStateValuations && dtmc.hasStateValuations()) { - components.stateValuations = dtmc.getStateValuations().blowup(data.simpleStateToOriginalState); + components.stateValuations = dtmc.getStateValuations().selectEntities(data.simpleStateToOriginalState); } return std::make_shared>(std::move(components.transitionMatrix), std::move(components.stateLabeling), diff --git a/src/storm-pomdp/analysis/IterativePolicySearch.cpp b/src/storm-pomdp/analysis/IterativePolicySearch.cpp index c026cfc9b3..df6dfe6a38 100644 --- a/src/storm-pomdp/analysis/IterativePolicySearch.cpp +++ b/src/storm-pomdp/analysis/IterativePolicySearch.cpp @@ -863,7 +863,7 @@ void IterativePolicySearch::coveredStatesToStream(std::ostream& os, s } std::cout << state; if (pomdp.hasStateValuations()) { - os << ":" << pomdp.getStateValuations().getStateInfo(state); + os << ":" << pomdp.getStateValuations().toString(state); } } } diff --git a/src/storm-pomdp/generator/GenerateMonitorVerifier.cpp b/src/storm-pomdp/generator/GenerateMonitorVerifier.cpp index e76e71323a..d5546001b9 100644 --- a/src/storm-pomdp/generator/GenerateMonitorVerifier.cpp +++ b/src/storm-pomdp/generator/GenerateMonitorVerifier.cpp @@ -15,6 +15,9 @@ #include "storm/storage/BitVector.h" #include "storm/storage/SparseMatrix.h" #include "storm/storage/expressions/ExpressionManager.h" +#include "storm/storage/valuations/ValuationDescriptionBuilder.h" +#include "storm/storage/valuations/Valuations.h" +#include "storm/storage/valuations/ValuationsStorage.h" #include "storm/utility/constants.h" #include "storm/utility/macros.h" @@ -331,82 +334,46 @@ std::shared_ptr> GenerateMonitorVerifier:: if (mc.hasStateValuations()) { // Add state valuations - storm::storage::sparse::StateValuationsBuilder svBuilder; - svBuilder.addVariable(monvar); - svBuilder.addVariable(mcvar); - std::set variables; - for (uint64_t i = 0; i < mc.getNumberOfStates(); i++) { - const auto& valAssignment = mc.getStateValuations().at(i); - for (auto val = valAssignment.begin(); val != valAssignment.end(); ++val) { - if (val.isVariableAssignment() && !variables.contains(val.getVariable())) { - variables.emplace(val.getVariable()); - svBuilder.addVariable(val.getVariable()); - } - } - } + auto const& oldValuations = mc.getStateValuations().getStorage(); + storm::storage::sparse::ValuationsStorage stateValuations = [this, &oldValuations]() { + storm::storage::sparse::ValuationDescriptionBuilder svBuilder(exprManager); + svBuilder.addIntegerVariable(monvar, -1, monitor.getNumberOfStates() - 1); + svBuilder.addIntegerVariable(mcvar, -1, mc.getNumberOfStates() - 1); + STORM_LOG_ASSERT(oldValuations.numClasses() == 1, "Only one class of valuations supported."); + svBuilder.addVariables(oldValuations.getClassDescription()); + return storm::storage::sparse::ValuationsStorage(svBuilder.buildClassDescription(), exprManager); + }(); + stateValuations.resize(numberOfStates); for (uint64_t i = 0; i < mc.getNumberOfStates(); i++) { for (uint64_t j = 0; j < monitor.getNumberOfStates(); j++) { - product_state_type s(i, j); + product_state_type const s(i, j); if (!prodToIndexMap.contains(s)) continue; - - std::vector booleanValues; - std::vector integerValues; - std::vector rationalValues; - - integerValues.push_back(j); // Set monvar - integerValues.push_back(i); // Set mcvar - - const auto& valAssignment = mc.getStateValuations().at(i); - - for (auto& var : variables) { - for (auto val = valAssignment.begin(); val != valAssignment.end(); ++val) { - if (var == val.getVariable()) { - if (val.isBoolean()) { - booleanValues.push_back(val.getBooleanValue()); - } else if (val.isInteger()) { - integerValues.push_back(val.getIntegerValue()); - } else if (val.isRational()) { - rationalValues.push_back(val.getRationalValue()); - } - break; + auto const productStateIndex = prodToIndexMap[s]; + // Set the variable values for the product state. + // We copy the valuations from the original model and set the monvar and mcvar to the corresponding state indices. + stateValuations.writeCallback(productStateIndex, [this, &oldValuations, i, j](auto, auto const& var, auto& value) { + using VT = std::remove_cvref_t; + if (var == monvar || var == mcvar) { + if constexpr (std::is_same_v) { + value = var == monvar ? j : i; + } else { + STORM_LOG_ASSERT(false, "Unexpected type."); } + } else { + // This is a variable of the original model. Copy old valuation value. + value = oldValuations.template readValue(i, var); } - } - svBuilder.addState(prodToIndexMap[std::make_pair(i, j)], std::move(booleanValues), std::move(integerValues), std::move(rationalValues)); - } - } - - std::vector goalBooleanValues; - std::vector goalIntegerValues(2, -1); - std::vector goalRationalValues; - for (auto& var : variables) { - if (var.hasBooleanType()) { - goalBooleanValues.push_back(false); - } else if (var.hasIntegerType()) { - goalIntegerValues.push_back(-1); - } else if (var.hasRationalType()) { - goalRationalValues.emplace_back(-1); - } - } - svBuilder.addState(goalIndex, std::move(goalBooleanValues), std::move(goalIntegerValues), std::move(goalRationalValues)); - - std::vector stopBooleanValues; - std::vector stopIntegerValues(2, -1); - std::vector stopRationalValues; - for (auto& var : variables) { - if (var.hasBooleanType()) { - stopBooleanValues.push_back(false); - } else if (var.hasIntegerType()) { - stopIntegerValues.push_back(-1); - } else if (var.hasRationalType()) { - stopRationalValues.emplace_back(-1); + }); } } - svBuilder.addState(stopIndex, std::move(stopBooleanValues), std::move(stopIntegerValues), std::move(stopRationalValues)); - components.stateValuations = svBuilder.build(); + stateValuations.writeValue(goalIndex, monvar, -1); + stateValuations.writeValue(goalIndex, mcvar, -1); + stateValuations.writeValue(stopIndex, monvar, -1); + stateValuations.writeValue(stopIndex, mcvar, -1); + components.stateValuations.emplace(std::move(stateValuations)); } // Store model diff --git a/src/storm-pomdp/storage/BeliefManager.cpp b/src/storm-pomdp/storage/BeliefManager.cpp index b8be630aac..b064f2e408 100644 --- a/src/storm-pomdp/storage/BeliefManager.cpp +++ b/src/storm-pomdp/storage/BeliefManager.cpp @@ -787,7 +787,7 @@ uint64_t BeliefManager::getRepresentative template std::string BeliefManager::getObservationLabel(BeliefId const &beliefId) { if (pomdp.hasObservationValuations()) { - return pomdp.getObservationValuations().getStateInfo(getBeliefObservation(beliefId)); + return pomdp.getObservationValuations().toString(getBeliefObservation(beliefId)); } else { STORM_LOG_TRACE("Cannot get observation labels as no observation valuation has been defined for the POMDP. Return empty label instead."); return ""; diff --git a/src/storm-pomdp/transformer/BinaryPomdpTransformer.cpp b/src/storm-pomdp/transformer/BinaryPomdpTransformer.cpp index 897049a750..0117585a62 100644 --- a/src/storm-pomdp/transformer/BinaryPomdpTransformer.cpp +++ b/src/storm-pomdp/transformer/BinaryPomdpTransformer.cpp @@ -27,7 +27,7 @@ PomdpTransformationResult BinaryPomdpTransformer::transfor components.transitionMatrix = std::move(data.simpleMatrix); components.observabilityClasses = std::move(data.simpleObservations); if (keepStateValuations && pomdp.hasStateValuations()) { - components.stateValuations = pomdp.getStateValuations().blowup(data.simpleStateToOriginalState); + components.stateValuations = pomdp.getStateValuations().selectEntities(data.simpleStateToOriginalState); } PomdpTransformationResult result; result.transformedPomdp = std::make_shared>(std::move(components), true); diff --git a/src/storm-pomdp/transformer/ObservationTraceUnfolder.cpp b/src/storm-pomdp/transformer/ObservationTraceUnfolder.cpp index a78d92c7b3..b1fdb8a62b 100644 --- a/src/storm-pomdp/transformer/ObservationTraceUnfolder.cpp +++ b/src/storm-pomdp/transformer/ObservationTraceUnfolder.cpp @@ -6,6 +6,9 @@ #include "storm/adapters/RationalNumberForward.h" #include "storm/exceptions/InvalidArgumentException.h" #include "storm/storage/expressions/ExpressionManager.h" +#include "storm/storage/valuations/ValuationDescriptionBuilder.h" +#include "storm/storage/valuations/Valuations.h" +#include "storm/storage/valuations/ValuationsStorage.h" #include "storm/utility/ConstantsComparator.h" #undef _VERBOSE_OBSERVATION_UNFOLDING @@ -42,9 +45,18 @@ std::shared_ptr> ObservationTraceUnfolder< #ifdef _VERBOSE_OBSERVATION_UNFOLDING std::cout << "build valution builder..\n"; #endif - storm::storage::sparse::StateValuationsBuilder svbuilder; - svbuilder.addVariable(svvar); - svbuilder.addVariable(tsvar); + // Initialize state valuations + storm::storage::sparse::ValuationsStorage stateValuations = [this, &observations]() { + storm::storage::sparse::ValuationDescriptionBuilder svBuilder(exprManager); + svBuilder.addIntegerVariable(svvar, -1, static_cast(model.getNumberOfStates()) - 1); + svBuilder.addIntegerVariable(tsvar, -1, observations.size() - 1); + return storm::storage::sparse::ValuationsStorage(svBuilder.buildClassDescription(), exprManager); + }(); + + // Shorthand for adding the next state's valuations with input model state index s and trace step t + auto addStateValuation = [this, &stateValuations](int64_t s, int64_t t) { + stateValuations.emplaceBack([this, s, t](auto, auto const& var, auto& value) { value = var == svvar ? s : t; }); + }; std::unordered_map unfoldedToOld; std::unordered_map unfoldedToOldNextStep; @@ -73,7 +85,7 @@ std::shared_ptr> ObservationTraceUnfolder< // the violated state (only used when no rejection sampling) is a sink state transitionMatrixBuilder.newRowGroup(violatedState); transitionMatrixBuilder.addNextValue(violatedState, violatedState, storm::utility::one()); - svbuilder.addState(violatedState, {}, {-1, -1}); + addStateValuation(-1, -1); } // Now we are starting to build the MDP from the initial state onwards. @@ -93,7 +105,7 @@ std::shared_ptr> ObservationTraceUnfolder< #endif STORM_LOG_ASSERT(step == 0 || newRowCount == transitionMatrixBuilder.getLastRow() + 1, "step " << step << " newRowCount " << newRowCount << " lastRow " << transitionMatrixBuilder.getLastRow()); - svbuilder.addState(unfoldedToOldEntry.first, {}, {static_cast(unfoldedToOldEntry.second), static_cast(step)}); + addStateValuation(unfoldedToOldEntry.second, step); uint64_t oldRowIndexStart = model.getNondeterministicChoiceIndices()[unfoldedToOldEntry.second]; uint64_t oldRowIndexEnd = model.getNondeterministicChoiceIndices()[unfoldedToOldEntry.second + 1]; @@ -159,8 +171,7 @@ std::shared_ptr> ObservationTraceUnfolder< uint64_t sinkState = newStateIndex; uint64_t targetState = newStateIndex + 1; for (auto const& unfoldedToOldEntry : unfoldedToOldNextStep) { - svbuilder.addState(unfoldedToOldEntry.first, {}, {static_cast(unfoldedToOldEntry.second), static_cast(observations.size() - 1)}); - + addStateValuation(unfoldedToOldEntry.second, observations.size() - 1); transitionMatrixBuilder.newRowGroup(newRowGroupStart); STORM_LOG_ASSERT(risk.size() > unfoldedToOldEntry.second, "Must be a state"); STORM_LOG_ASSERT(storm::utility::isBetween(storm::utility::zero(), risk[unfoldedToOldEntry.second], storm::utility::one()), @@ -177,13 +188,14 @@ std::shared_ptr> ObservationTraceUnfolder< // sink state transitionMatrixBuilder.newRowGroup(newRowGroupStart); transitionMatrixBuilder.addNextValue(newRowGroupStart, sinkState, storm::utility::one()); - svbuilder.addState(sinkState, {}, {-1, -1}); + addStateValuation(-1, -1); newRowGroupStart++; transitionMatrixBuilder.newRowGroup(newRowGroupStart); // target state transitionMatrixBuilder.addNextValue(newRowGroupStart, targetState, storm::utility::one()); - svbuilder.addState(targetState, {}, {-1, -1}); + addStateValuation(-1, -1); + #ifdef _VERBOSE_OBSERVATION_UNFOLDING std::cout << "build matrix...\n"; #endif @@ -207,7 +219,7 @@ std::shared_ptr> ObservationTraceUnfolder< labeling.addLabel("init"); labeling.addLabelToState("init", initialState); components.stateLabeling = labeling; - components.stateValuations = svbuilder.build(); + components.stateValuations = std::move(stateValuations); return std::make_shared>(std::move(components)); } diff --git a/src/storm-pomdp/transformer/PomdpMemoryUnfolder.cpp b/src/storm-pomdp/transformer/PomdpMemoryUnfolder.cpp index 784c2f9964..3533ba60c7 100644 --- a/src/storm-pomdp/transformer/PomdpMemoryUnfolder.cpp +++ b/src/storm-pomdp/transformer/PomdpMemoryUnfolder.cpp @@ -39,7 +39,7 @@ std::shared_ptr> PomdpMemoryUnfolder::buildMatrices( StateAndChoiceInformationBuilder& stateAndChoiceInformationBuilder) { // Initialize building state valuations (if necessary) if (stateAndChoiceInformationBuilder.isBuildStateValuations()) { - stateAndChoiceInformationBuilder.stateValuationsBuilder() = generator->initializeStateValuationsBuilder(); + stateAndChoiceInformationBuilder.initializeStateValuations(generator->initializeStateValuations()); } // Create a callback for the next-state generator to enable it to request the index of states. @@ -181,7 +181,7 @@ void ExplicitModelBuilder::buildMatrices( generator->load(currentState); if (stateAndChoiceInformationBuilder.isBuildStateValuations()) { - generator->addStateValuation(currentIndex, stateAndChoiceInformationBuilder.stateValuationsBuilder()); + generator->addStateValuation(currentIndex, stateAndChoiceInformationBuilder.stateValuations()); } storm::generator::StateBehavior behavior; @@ -396,7 +396,7 @@ storm::storage::sparse::ModelComponents ExplicitMode } // If requested, build the state valuations and choice origins if (stateAndChoiceInformationBuilder.isBuildStateValuations()) { - modelComponents.stateValuations = stateAndChoiceInformationBuilder.stateValuationsBuilder().build(); + modelComponents.stateValuations = std::move(stateAndChoiceInformationBuilder.stateValuations()); } if (stateAndChoiceInformationBuilder.isBuildChoiceOrigins()) { auto originData = stateAndChoiceInformationBuilder.buildDataOfChoiceOrigins(numChoices); diff --git a/src/storm/builder/StateAndChoiceInformationBuilder.cpp b/src/storm/builder/StateAndChoiceInformationBuilder.cpp index 7c66f9f45f..f37ef0806a 100644 --- a/src/storm/builder/StateAndChoiceInformationBuilder.cpp +++ b/src/storm/builder/StateAndChoiceInformationBuilder.cpp @@ -116,9 +116,15 @@ bool StateAndChoiceInformationBuilder::isBuildStateValuations() const { return _buildStateValuations; } -storm::storage::sparse::StateValuationsBuilder& StateAndChoiceInformationBuilder::stateValuationsBuilder() { +void StateAndChoiceInformationBuilder::initializeStateValuations(storm::storage::sparse::Valuations&& valuations) { STORM_LOG_ASSERT(_buildStateValuations, "Building StateValuations was not enabled."); - return _stateValuationsBuilder; + _stateValuations = std::move(valuations); +} + +storm::storage::sparse::Valuations& StateAndChoiceInformationBuilder::stateValuations() { + STORM_LOG_ASSERT(_buildStateValuations, "Building StateValuations was not enabled."); + STORM_LOG_ASSERT(_stateValuations.has_value(), "State valuations not initialized."); + return _stateValuations.value(); } } // namespace builder diff --git a/src/storm/builder/StateAndChoiceInformationBuilder.h b/src/storm/builder/StateAndChoiceInformationBuilder.h index 232a01e1cf..b3a63c12f6 100644 --- a/src/storm/builder/StateAndChoiceInformationBuilder.h +++ b/src/storm/builder/StateAndChoiceInformationBuilder.h @@ -11,7 +11,7 @@ #include "storm/storage/PlayerIndex.h" #include "storm/storage/prism/Program.h" #include "storm/storage/sparse/PrismChoiceOrigins.h" -#include "storm/storage/sparse/StateValuations.h" +#include "storm/storage/valuations/Valuations.h" namespace storm { namespace builder { @@ -50,7 +50,12 @@ class StateAndChoiceInformationBuilder { void setBuildStateValuations(bool value); bool isBuildStateValuations() const; - storm::storage::sparse::StateValuationsBuilder& stateValuationsBuilder(); + void initializeStateValuations(storm::storage::sparse::Valuations&& valuations); + /*! + * @return a reference to the state valuations. Must only be called if buildStateValuations() is true and initializeStateValuations() has been called + * before. + */ + storm::storage::sparse::Valuations& stateValuations(); private: bool _buildChoiceLabels; @@ -66,7 +71,7 @@ class StateAndChoiceInformationBuilder { storm::storage::BitVector _markovianStates; bool _buildStateValuations; - storm::storage::sparse::StateValuationsBuilder _stateValuationsBuilder; + std::optional _stateValuations; }; } // namespace builder } // namespace storm diff --git a/src/storm/generator/CompressedState.cpp b/src/storm/generator/CompressedState.cpp index 9abe1ac0c6..f79ff97c44 100644 --- a/src/storm/generator/CompressedState.cpp +++ b/src/storm/generator/CompressedState.cpp @@ -9,6 +9,7 @@ #include "storm/storage/expressions/ExpressionEvaluator.h" #include "storm/storage/expressions/ExpressionManager.h" #include "storm/storage/expressions/SimpleValuation.h" +#include "storm/storage/valuations/ValuationsStorage.h" namespace storm { namespace generator { @@ -76,21 +77,66 @@ CompressedState packStateFromValuation(expressions::SimpleValuation const& valua return result; } -void extractVariableValues(CompressedState const& state, VariableInformation const& variableInformation, std::vector& locationValues, - std::vector& booleanValues, std::vector& integerValues) { +namespace detail { +enum class UnpackStateIntoValuationsMode { State, Observation }; +template +void unpackIntoValuations(CompressedState const& entityEncoding, uint64_t const entityIndex, VariableInformation const& variableInformation, + storm::storage::sparse::ValuationsStorage& valuations) { + using enum UnpackStateIntoValuationsMode; + STORM_LOG_ASSERT(entityIndex < valuations.size(), + "Valuation entity index " << entityIndex << " is out of bounds for valuations of size " << valuations.size() << "."); + STORM_LOG_ASSERT(Mode != State || entityEncoding.size() == variableInformation.getTotalBitOffset(true), + "State size does not match the expected size based on the variable information."); + STORM_LOG_ASSERT( + Mode != Observation || entityEncoding.size() == variableInformation.getTotalBitOffset(true) + variableInformation.observationLabels.size() * 64, + "Observation class size does not match the expected size based on the variable information."); + + if (Mode == State && variableInformation.hasOutOfBoundsBit()) { + valuations.writeValue(entityIndex, variableInformation.outOfBoundsBit->variable, entityEncoding.get(variableInformation.getOutOfBoundsBit())); + } for (auto const& locationVariable : variableInformation.locationVariables) { - if (locationVariable.bitWidth != 0) { - locationValues.push_back(state.getAsInt(locationVariable.bitOffset, locationVariable.bitWidth)); - } else { - locationValues.push_back(0); + if (Mode == Observation && !locationVariable.observable) { + continue; } + int64_t const value = locationVariable.bitWidth != 0 ? entityEncoding.getAsInt(locationVariable.bitOffset, locationVariable.bitWidth) : 0; + valuations.writeValue(entityIndex, locationVariable.variable, value); } for (auto const& booleanVariable : variableInformation.booleanVariables) { - booleanValues.push_back(state.get(booleanVariable.bitOffset)); + if (Mode == Observation && !booleanVariable.observable) { + continue; + } + valuations.writeValue(entityIndex, booleanVariable.variable, entityEncoding.get(booleanVariable.bitOffset)); } for (auto const& integerVariable : variableInformation.integerVariables) { - integerValues.push_back(static_cast(state.getAsInt(integerVariable.bitOffset, integerVariable.bitWidth)) + integerVariable.lowerBound); + if (Mode == Observation && !integerVariable.observable) { + continue; + } + int64_t const value = entityEncoding.getAsInt(integerVariable.bitOffset, integerVariable.bitWidth) + integerVariable.lowerBound; + valuations.writeValue(entityIndex, integerVariable.variable, value); } + if constexpr (Mode == Observation) { + uint64_t labelEncodingStart = variableInformation.getTotalBitOffset(true); + for (auto const& observationLabel : variableInformation.observationLabels) { + STORM_LOG_ASSERT(observationLabel.deterministic, "Only deterministic observation labels supported for unpacking into valuations."); + STORM_LOG_ASSERT(labelEncodingStart + 64 <= entityEncoding.size(), "Not enough bits left in the observation class encoding."); + int64_t const labelValue = entityEncoding.getAsInt(labelEncodingStart, 64); + valuations.writeCallback(entityIndex, observationLabel.variable, + [labelValue](auto, auto, auto& value) { value = labelValue; }); + } + } +} + +} // namespace detail + +void unpackStateAppendToValuations(CompressedState const& state, VariableInformation const& variableInformation, + storm::storage::sparse::ValuationsStorage& valuations) { + valuations.resize(valuations.size() + 1); + detail::unpackIntoValuations(state, valuations.size() - 1, variableInformation, valuations); +} + +void unpackObservationClassIntoValuations(CompressedState const& observationClass, uint64_t const observationClassIndex, + VariableInformation const& variableInformation, storm::storage::sparse::ValuationsStorage& valuations) { + detail::unpackIntoValuations(observationClass, observationClassIndex, variableInformation, valuations); } std::string toString(CompressedState const& state, VariableInformation const& variableInformation) { @@ -188,9 +234,6 @@ storm::json unpackStateIntoJson(CompressedState const& state, Variabl return result; } -storm::expressions::SimpleValuation unpackStateIntoValuation(CompressedState const& state, VariableInformation const& variableInformation, - storm::expressions::ExpressionManager const& manager); - CompressedState createOutOfBoundsState(VariableInformation const& varInfo, bool roundTo64Bit) { CompressedState result(varInfo.getTotalBitOffset(roundTo64Bit)); assert(varInfo.hasOutOfBoundsBit()); diff --git a/src/storm/generator/CompressedState.h b/src/storm/generator/CompressedState.h index 2c488760a6..dfa3818673 100644 --- a/src/storm/generator/CompressedState.h +++ b/src/storm/generator/CompressedState.h @@ -7,6 +7,9 @@ #include "storm/storage/BitVector.h" namespace storm { +namespace storage::sparse { +class ValuationsStorage; +} namespace expressions { template class ExpressionEvaluator; @@ -56,16 +59,20 @@ template storm::json unpackStateIntoJson(CompressedState const& state, VariableInformation const& variableInformation, bool onlyObservable); /*! - * Appends the values of the given variables in the given state to the corresponding result vectors. - * locationValues are inserted before integerValues (relevant if both, locationValues and integerValues actually refer to the same vector) - * @param state The state - * @param variableInformation The variables - * @param locationValues - * @param booleanValues - * @param integerValues + * Appends the values of the variables in the given state to the valuations object. + * Assumes that the order of variables in the variableInformation and valuations objects are aligned. + * @param state The state. + * @param variableInformation The variables. + * @param valuations the valuations to which the variable values should be appended. */ -void extractVariableValues(CompressedState const& state, VariableInformation const& variableInformation, std::vector& locationValues, - std::vector& booleanValues, std::vector& integerValues); +void unpackStateAppendToValuations(CompressedState const& state, VariableInformation const& variableInformation, + storm::storage::sparse::ValuationsStorage& valuations); + +/*! + * Sets the values of observable variables and observation expressions to the given observationClassIndex of the given valuations. + */ +void unpackObservationClassIntoValuations(CompressedState const& observationClass, uint64_t const observationClassIndex, + VariableInformation const& variableInformation, storm::storage::sparse::ValuationsStorage& valuations); /*! * Returns a (human readable) string representation of the variable valuation encoded by the given state diff --git a/src/storm/generator/JaniNextStateGenerator.cpp b/src/storm/generator/JaniNextStateGenerator.cpp index 08d8fa4ad8..276cce7b77 100644 --- a/src/storm/generator/JaniNextStateGenerator.cpp +++ b/src/storm/generator/JaniNextStateGenerator.cpp @@ -22,6 +22,7 @@ #include "storm/storage/jani/traverser/RewardModelInformation.h" #include "storm/storage/jani/visitor/CompositionInformationVisitor.h" #include "storm/storage/sparse/JaniChoiceOrigins.h" +#include "storm/storage/valuations/ValuationDescriptionBuilder.h" #include "storm/utility/combinatorics.h" #include "storm/utility/constants.h" #include "storm/utility/macros.h" @@ -563,75 +564,49 @@ void JaniNextStateGenerator::unpackTransientVariableValues } template -storm::storage::sparse::StateValuationsBuilder JaniNextStateGenerator::initializeStateValuationsBuilder() const { - auto result = NextStateGenerator::initializeStateValuationsBuilder(); +storm::storage::sparse::Valuations JaniNextStateGenerator::initializeStateValuations() const { + storm::storage::sparse::ValuationDescriptionBuilder builder(this->model.getManager().shared_from_this()); + if (this->variableInformation.hasOutOfBoundsBit()) { + builder.addBooleanVariable(this->variableInformation.outOfBoundsBit->variable); + } + for (auto const& v : this->variableInformation.locationVariables) { + builder.addIntegerVariable(v.variable, 0, v.highestValue); + } + for (auto const& v : this->variableInformation.booleanVariables) { + builder.addBooleanVariable(v.variable); + } + for (auto const& v : this->variableInformation.integerVariables) { + builder.addIntegerVariable(v.variable, v.lowerBound, v.upperBound); + } // Also add information for transient variables for (auto const& varInfo : transientVariableInformation.booleanVariableInformation) { - result.addVariable(varInfo.variable); + builder.addBooleanVariable(varInfo.variable); } for (auto const& varInfo : transientVariableInformation.integerVariableInformation) { - result.addVariable(varInfo.variable); + builder.addIntegerVariable(varInfo.variable, varInfo.lowerBound.value_or(std::numeric_limits::min()), + varInfo.upperBound.value_or(std::numeric_limits::max())); } for (auto const& varInfo : transientVariableInformation.rationalVariableInformation) { - result.addVariable(varInfo.variable); + if (std::is_same_v) { + uint64_t const bitSize = std::max(64, this->getOptions().getReservedBitsForUnboundedVariables()); + builder.addRationalVariable(varInfo.variable, bitSize * 2); // reserve bits for numerator and denominator + } else { + STORM_LOG_THROW((std::is_same_v), storm::exceptions::NotSupportedException, + "State valuations for transient variables of the given value type are not supported."); + builder.addDoubleVariable(varInfo.variable); + } } - return result; + return storm::storage::sparse::Valuations(builder.buildClassDescription(), builder.getManager().shared_from_this()); } template void JaniNextStateGenerator::addStateValuation(storm::storage::sparse::state_type const& currentStateIndex, - storm::storage::sparse::StateValuationsBuilder& valuationsBuilder) const { - std::vector booleanValues; - booleanValues.reserve(this->variableInformation.booleanVariables.size() + transientVariableInformation.booleanVariableInformation.size()); - std::vector integerValues; - integerValues.reserve(this->variableInformation.locationVariables.size() + this->variableInformation.integerVariables.size() + - transientVariableInformation.integerVariableInformation.size()); - std::vector rationalValues; - rationalValues.reserve(transientVariableInformation.rationalVariableInformation.size()); - + storm::storage::sparse::Valuations& valuations) const { // Add values for non-transient variables - extractVariableValues(*this->state, this->variableInformation, integerValues, booleanValues, integerValues); + unpackStateAppendToValuations(*this->state, this->variableInformation, valuations.getStorage()); - // Add values for transient variables auto transientVariableValuation = getTransientVariableValuationAtLocations(getLocations(*this->state), *this->evaluator); - { - auto varIt = transientVariableValuation.booleanValues.begin(); - auto varIte = transientVariableValuation.booleanValues.end(); - for (auto const& varInfo : transientVariableInformation.booleanVariableInformation) { - if (varIt != varIte && varIt->first->variable == varInfo.variable) { - booleanValues.push_back(varIt->second); - ++varIt; - } else { - booleanValues.push_back(varInfo.defaultValue); - } - } - } - { - auto varIt = transientVariableValuation.integerValues.begin(); - auto varIte = transientVariableValuation.integerValues.end(); - for (auto const& varInfo : transientVariableInformation.integerVariableInformation) { - if (varIt != varIte && varIt->first->variable == varInfo.variable) { - integerValues.push_back(varIt->second); - ++varIt; - } else { - integerValues.push_back(varInfo.defaultValue); - } - } - } - { - auto varIt = transientVariableValuation.rationalValues.begin(); - auto varIte = transientVariableValuation.rationalValues.end(); - for (auto const& varInfo : transientVariableInformation.rationalVariableInformation) { - if (varIt != varIte && varIt->first->variable == varInfo.variable) { - rationalValues.push_back(storm::utility::convertNumber(varIt->second)); - ++varIt; - } else { - rationalValues.push_back(storm::utility::convertNumber(varInfo.defaultValue)); - } - } - } - - valuationsBuilder.addState(currentStateIndex, std::move(booleanValues), std::move(integerValues), std::move(rationalValues)); + transientVariableValuation.setInValuations(currentStateIndex, transientVariableInformation, valuations.getStorage()); } template diff --git a/src/storm/generator/JaniNextStateGenerator.h b/src/storm/generator/JaniNextStateGenerator.h index d273c77ac6..a60eae630c 100644 --- a/src/storm/generator/JaniNextStateGenerator.h +++ b/src/storm/generator/JaniNextStateGenerator.h @@ -46,14 +46,13 @@ class JaniNextStateGenerator : public NextStateGenerator { virtual bool isPartiallyObservable() const override; virtual std::vector getInitialStates(StateToIdCallback const& stateToIdCallback) override; - /// Initializes a builder for state valuations by adding the appropriate variables. - virtual storm::storage::sparse::StateValuationsBuilder initializeStateValuationsBuilder() const override; + /// Initializes state valuations by adding the appropriate variables. + virtual storm::storage::sparse::Valuations initializeStateValuations() const override; virtual StateBehavior expand(StateToIdCallback const& stateToIdCallback) override; /// Adds the valuation for the currently loaded state to the given builder - virtual void addStateValuation(storm::storage::sparse::state_type const& currentStateIndex, - storm::storage::sparse::StateValuationsBuilder& valuationsBuilder) const override; + virtual void addStateValuation(storm::storage::sparse::state_type const& currentStateIndex, storm::storage::sparse::Valuations& valuations) const override; virtual std::size_t getNumberOfRewardModels() const override; virtual storm::builder::RewardModelInformation getRewardModelInformation(uint64_t const& index) const override; diff --git a/src/storm/generator/NextStateGenerator.cpp b/src/storm/generator/NextStateGenerator.cpp index aa3d1cf334..c34d8ade01 100644 --- a/src/storm/generator/NextStateGenerator.cpp +++ b/src/storm/generator/NextStateGenerator.cpp @@ -11,6 +11,7 @@ #include "storm/storage/expressions/ExpressionEvaluator.h" #include "storm/storage/expressions/ExpressionManager.h" #include "storm/storage/expressions/SimpleValuation.h" +#include "storm/storage/valuations/ValuationDescriptionBuilder.h" #include "storm/utility/macros.h" namespace storm { @@ -80,37 +81,46 @@ void NextStateGenerator::initializeSpecialStates() { } template -storm::storage::sparse::StateValuationsBuilder NextStateGenerator::initializeStateValuationsBuilder() const { - storm::storage::sparse::StateValuationsBuilder result; +storm::storage::sparse::Valuations NextStateGenerator::initializeStateValuations() const { + storm::storage::sparse::ValuationDescriptionBuilder builder(expressionManager); + if (variableInformation.hasOutOfBoundsBit()) { + builder.addBooleanVariable(variableInformation.outOfBoundsBit->variable); + } for (auto const& v : variableInformation.locationVariables) { - result.addVariable(v.variable); + builder.addIntegerVariable(v.variable, 0, v.highestValue); } for (auto const& v : variableInformation.booleanVariables) { - result.addVariable(v.variable); + builder.addBooleanVariable(v.variable); } for (auto const& v : variableInformation.integerVariables) { - result.addVariable(v.variable); + builder.addIntegerVariable(v.variable, v.lowerBound, v.upperBound); } - return result; + return storm::storage::sparse::Valuations(builder.buildClassDescription(), expressionManager); } template -storm::storage::sparse::StateValuationsBuilder NextStateGenerator::initializeObservationValuationsBuilder() const { - storm::storage::sparse::StateValuationsBuilder result; +storm::storage::sparse::Valuations NextStateGenerator::initializeObservationValuations() const { + storm::storage::sparse::ValuationDescriptionBuilder builder(expressionManager); for (auto const& v : variableInformation.booleanVariables) { if (v.observable) { - result.addVariable(v.variable); + builder.addBooleanVariable(v.variable); } } for (auto const& v : variableInformation.integerVariables) { if (v.observable) { - result.addVariable(v.variable); + builder.addIntegerVariable(v.variable, v.lowerBound, v.upperBound); } } for (auto const& l : variableInformation.observationLabels) { - result.addObservationLabel(l.name); + if (l.variable.hasBooleanType()) { + builder.addBooleanVariable(l.variable); + } else { + STORM_LOG_ASSERT(l.variable.hasIntegerType(), "Observation label " << l.variable.getName() << " has neither boolean nor integer type."); + builder.addIntegerVariable(l.variable, std::numeric_limits::min(), std::numeric_limits::max()); + } } - return result; + storm::storage::sparse::Valuations res(builder.buildClassDescription(), expressionManager, observabilityMap.size()); + return res; } template @@ -137,43 +147,17 @@ VariableInformation const& NextStateGenerator::getVariable template void NextStateGenerator::addStateValuation(storm::storage::sparse::state_type const& currentStateIndex, - storm::storage::sparse::StateValuationsBuilder& valuationsBuilder) const { - std::vector booleanValues; - booleanValues.reserve(variableInformation.booleanVariables.size()); - std::vector integerValues; - integerValues.reserve(variableInformation.locationVariables.size() + variableInformation.integerVariables.size()); - extractVariableValues(*this->state, variableInformation, integerValues, booleanValues, integerValues); - valuationsBuilder.addState(currentStateIndex, std::move(booleanValues), std::move(integerValues)); + storm::storage::sparse::Valuations& valuations) const { + unpackStateAppendToValuations(*this->state, variableInformation, valuations.getStorage()); } template -storm::storage::sparse::StateValuations NextStateGenerator::makeObservationValuation() const { - storm::storage::sparse::StateValuationsBuilder valuationsBuilder = initializeObservationValuationsBuilder(); +storm::storage::sparse::Valuations NextStateGenerator::makeObservationValuation() const { + storm::storage::sparse::Valuations valuations = initializeObservationValuations(); for (auto const& observationEntry : observabilityMap) { - std::vector booleanValues; - booleanValues.reserve(variableInformation.booleanVariables.size()); // TODO: use number of observable boolean variables - std::vector integerValues; - integerValues.reserve(variableInformation.locationVariables.size() + - variableInformation.integerVariables.size()); // TODO: use number of observable integer variables - std::vector observationLabelValues; - observationLabelValues.reserve(variableInformation.observationLabels.size()); - expressions::SimpleValuation val = unpackStateIntoValuation(observationEntry.first, variableInformation, *expressionManager); - for (auto const& v : variableInformation.booleanVariables) { - if (v.observable) { - booleanValues.push_back(val.getBooleanValue(v.variable)); - } - } - for (auto const& v : variableInformation.integerVariables) { - if (v.observable) { - integerValues.push_back(val.getIntegerValue(v.variable)); - } - } - for (uint64_t labelStart = variableInformation.getTotalBitOffset(true); labelStart < observationEntry.first.size(); labelStart += 64) { - observationLabelValues.push_back(observationEntry.first.getAsInt(labelStart, 64)); - } - valuationsBuilder.addState(observationEntry.second, std::move(booleanValues), std::move(integerValues), {}, std::move(observationLabelValues)); + unpackObservationClassIntoValuations(observationEntry.first, observationEntry.second, variableInformation, valuations.getStorage()); } - return valuationsBuilder.build(); + return valuations; } template diff --git a/src/storm/generator/NextStateGenerator.h b/src/storm/generator/NextStateGenerator.h index 10101ff518..b8c5d42d54 100644 --- a/src/storm/generator/NextStateGenerator.h +++ b/src/storm/generator/NextStateGenerator.h @@ -12,7 +12,7 @@ #include "storm/storage/expressions/Expression.h" #include "storm/storage/sparse/ChoiceOrigins.h" #include "storm/storage/sparse/StateStorage.h" -#include "storm/storage/sparse/StateValuations.h" +#include "storm/storage/valuations/Valuations.h" #include "storm/utility/ConstantsComparator.h" namespace storm { @@ -90,18 +90,17 @@ class NextStateGenerator { /// Initializes the out-of-bounds state and states with overlapping guards. void initializeSpecialStates(); - /// Initializes a builder for state valuations by adding the appropriate variables. - virtual storm::storage::sparse::StateValuationsBuilder initializeStateValuationsBuilder() const; + /// Initializes state valuations by adding the appropriate variables. + virtual storm::storage::sparse::Valuations initializeStateValuations() const; void load(CompressedState const& state); virtual StateBehavior expand(StateToIdCallback const& stateToIdCallback) = 0; bool satisfies(storm::expressions::Expression const& expression) const; /// Adds the valuation for the currently loaded state to the given builder - virtual void addStateValuation(storm::storage::sparse::state_type const& currentStateIndex, - storm::storage::sparse::StateValuationsBuilder& valuationsBuilder) const; + virtual void addStateValuation(storm::storage::sparse::state_type const& currentStateIndex, storm::storage::sparse::Valuations& valuations) const; /// Adds the valuation for the currently loaded state - virtual storm::storage::sparse::StateValuations makeObservationValuation() const; + virtual storm::storage::sparse::Valuations makeObservationValuation() const; virtual std::size_t getNumberOfRewardModels() const = 0; virtual storm::builder::RewardModelInformation getRewardModelInformation(uint64_t const& index) const = 0; @@ -164,7 +163,7 @@ class NextStateGenerator { virtual void extendStateInformation(storm::json& stateInfo) const; - virtual storm::storage::sparse::StateValuationsBuilder initializeObservationValuationsBuilder() const; + virtual storm::storage::sparse::Valuations initializeObservationValuations() const; void postprocess(StateBehavior& result); diff --git a/src/storm/generator/TransientVariableInformation.cpp b/src/storm/generator/TransientVariableInformation.cpp index ff22f21d47..302fab658a 100644 --- a/src/storm/generator/TransientVariableInformation.cpp +++ b/src/storm/generator/TransientVariableInformation.cpp @@ -8,6 +8,7 @@ #include "storm/storage/jani/AutomatonComposition.h" #include "storm/storage/jani/ParallelComposition.h" #include "storm/storage/jani/eliminator/ArrayEliminator.h" +#include "storm/storage/valuations/ValuationsStorage.h" #include "storm/exceptions/OutOfRangeException.h" #include "storm/exceptions/WrongFormatException.h" @@ -44,6 +45,66 @@ TransientVariableData::TransientVariableData(storm::expressions::V // Intentionally left empty. } +template +void TransientVariableValuation::clear() { + booleanValues.clear(); + integerValues.clear(); + rationalValues.clear(); +} + +template +bool TransientVariableValuation::empty() const { + return booleanValues.empty() && integerValues.empty() && rationalValues.empty(); +} + +template +void TransientVariableValuation::setInEvaluator(storm::expressions::ExpressionEvaluator& evaluator, bool explorationChecks) const { + for (auto const& varValue : booleanValues) { + evaluator.setBooleanValue(varValue.first->variable, varValue.second); + } + for (auto const& varValue : integerValues) { + if (explorationChecks) { + STORM_LOG_THROW(!varValue.first->lowerBound.is_initialized() || varValue.first->lowerBound.get() <= varValue.second, + storm::exceptions::OutOfRangeException, + "The assigned value for transient variable " << varValue.first->variable.getName() << " is smaller than its lower bound."); + STORM_LOG_THROW(!varValue.first->upperBound.is_initialized() || varValue.second <= varValue.first->upperBound.get(), + storm::exceptions::OutOfRangeException, + "The assigned value for transient variable " << varValue.first->variable.getName() << " is higher than its upper bound."); + } + evaluator.setIntegerValue(varValue.first->variable, varValue.second); + } + for (auto const& varValue : rationalValues) { + evaluator.setRationalValue(varValue.first->variable, varValue.second); + } +} + +template +void TransientVariableValuation::setInValuations(uint64_t const stateIndex, TransientVariableInformation const& info, + storm::storage::sparse::ValuationsStorage& valuations) const { + auto writeValues = [stateIndex, &valuations](auto const& varInfos, auto const& varValues) { + auto varIt = varValues.begin(); + auto const varIte = varValues.end(); + for (auto const& varInfo : varInfos) { + bool const hasValue = varIt != varIte && varIt->first->variable == varInfo.variable; + auto const& value = hasValue ? varIt->second : varInfo.defaultValue; + if (hasValue) { + ++varIt; + } + if constexpr (std::is_same_v, storm::RationalFunction>) { + STORM_LOG_THROW( + storm::utility::isConstant(value), storm::exceptions::NotSupportedException, + "Non-constant variable valuations are not supported. Got value " << value << " for variable " << varInfo.variable.getName() << "."); + valuations.writeValue(stateIndex, varInfo.variable, storm::utility::convertNumber(value)); + } else { + valuations.writeValue(stateIndex, varInfo.variable, value); + } + } + }; + writeValues(info.booleanVariableInformation, booleanValues); + writeValues(info.integerVariableInformation, integerValues); + writeValues(info.rationalVariableInformation, rationalValues); +} + template TransientVariableInformation::TransientVariableInformation( storm::jani::Model const& model, std::vector> const& parallelAutomata) { @@ -166,6 +227,9 @@ void TransientVariableInformation::setDefaultValuesInEvaluator(storm: } } +template struct TransientVariableValuation; +template struct TransientVariableValuation; +template struct TransientVariableValuation; template struct TransientVariableInformation; template struct TransientVariableInformation; template struct TransientVariableInformation; diff --git a/src/storm/generator/TransientVariableInformation.h b/src/storm/generator/TransientVariableInformation.h index 4aaf4d0e67..c04ada1431 100644 --- a/src/storm/generator/TransientVariableInformation.h +++ b/src/storm/generator/TransientVariableInformation.h @@ -26,10 +26,16 @@ template class ExpressionEvaluator; } +namespace storage::sparse { +class ValuationsStorage; +} + namespace generator { -// A structure storing information about a transient variable +template +struct TransientVariableInformation; +// A structure storing information about a transient variable template struct TransientVariableData { TransientVariableData(storm::expressions::Variable const& variable, boost::optional const& lowerBound, @@ -58,35 +64,14 @@ struct TransientVariableValuation { std::vector const*, int64_t>> integerValues; std::vector const*, ValueType>> rationalValues; - void clear() { - booleanValues.clear(); - integerValues.clear(); - rationalValues.clear(); - } - - bool empty() const { - return booleanValues.empty() && integerValues.empty() && rationalValues.empty(); - } - - void setInEvaluator(storm::expressions::ExpressionEvaluator& evaluator, bool explorationChecks) const { - for (auto const& varValue : booleanValues) { - evaluator.setBooleanValue(varValue.first->variable, varValue.second); - } - for (auto const& varValue : integerValues) { - if (explorationChecks) { - STORM_LOG_THROW(!varValue.first->lowerBound.is_initialized() || varValue.first->lowerBound.get() <= varValue.second, - storm::exceptions::OutOfRangeException, - "The assigned value for transient variable " << varValue.first->variable.getName() << " is smaller than its lower bound."); - STORM_LOG_THROW(!varValue.first->upperBound.is_initialized() || varValue.second <= varValue.first->upperBound.get(), - storm::exceptions::OutOfRangeException, - "The assigned value for transient variable " << varValue.first->variable.getName() << " is higher than its upper bound."); - } - evaluator.setIntegerValue(varValue.first->variable, varValue.second); - } - for (auto const& varValue : rationalValues) { - evaluator.setRationalValue(varValue.first->variable, varValue.second); - } - } + void clear(); + + bool empty() const; + + void setInEvaluator(storm::expressions::ExpressionEvaluator& evaluator, bool explorationChecks) const; + + void setInValuations(uint64_t const stateIndex, TransientVariableInformation const& info, + storm::storage::sparse::ValuationsStorage& valuations) const; }; // A structure storing information about the used variables of the program. diff --git a/src/storm/generator/VariableInformation.cpp b/src/storm/generator/VariableInformation.cpp index 8c2ac87171..ed18528e1d 100644 --- a/src/storm/generator/VariableInformation.cpp +++ b/src/storm/generator/VariableInformation.cpp @@ -10,6 +10,7 @@ #include "storm/storage/jani/eliminator/ArrayEliminator.h" #include "storm/exceptions/InvalidArgumentException.h" +#include "storm/exceptions/NotSupportedException.h" #include "storm/exceptions/UnexpectedException.h" #include "storm/exceptions/WrongFormatException.h" #include "storm/utility/macros.h" @@ -44,7 +45,7 @@ LocationVariableInformation::LocationVariableInformation(storm::expressions::Var // Intentionally left empty. } -ObservationLabelInformation::ObservationLabelInformation(const std::string& name) : name(name) { +ObservationLabelInformation::ObservationLabelInformation(storm::expressions::Variable const& variable) : variable(variable) { // Intentionally left empty. } @@ -95,12 +96,9 @@ uint64_t getBitWidthLowerUpperBound(bool const& hasLowerBound, int64_t& lowerBou VariableInformation::VariableInformation(storm::prism::Program const& program, uint64_t reservedBitsForUnboundedVariables, bool outOfBoundsState) : totalBitOffset(0) { if (outOfBoundsState) { - outOfBoundsBit = 0; + outOfBoundsBit.emplace(program.getManager().declareBooleanVariable("_OutOfBoundsBit"), totalBitOffset, true, false); ++totalBitOffset; - } else { - outOfBoundsBit = boost::none; } - for (auto const& booleanVariable : program.getGlobalBooleanVariables()) { booleanVariables.emplace_back(booleanVariable.getExpressionVariable(), totalBitOffset, true, booleanVariable.isObservable()); ++totalBitOffset; @@ -141,7 +139,19 @@ VariableInformation::VariableInformation(storm::prism::Program const& program, u } } for (auto const& oblab : program.getObservationLabels()) { - observationLabels.emplace_back(oblab.getName()); + storm::expressions::Variable obVar; + if (program.getManager().hasVariable(oblab.getName())) { + obVar = program.getManager().getVariable(oblab.getName()); + auto const& obPredicate = oblab.getStatePredicateExpression(); + STORM_LOG_THROW(obPredicate.isVariable() && obPredicate.getBaseExpression().asVariableExpression().getVariable() == obVar, + storm::exceptions::NotSupportedException, + "Observation valuations for label '" << oblab << " is not supported since a variable '" << oblab.getName() + << "' is already known and the expression '" << oblab.getStatePredicateExpression() + << "' is not equal to it."); + } else { + obVar = program.getManager().declareVariable(oblab.getName(), oblab.getStatePredicateExpression().getType()); + } + observationLabels.emplace_back(obVar); } sortVariables(); @@ -160,10 +170,12 @@ VariableInformation::VariableInformation(storm::jani::Model const& model, } if (outOfBoundsState) { - outOfBoundsBit = 0; + std::string outOfBoundsVarName = "_OutOfBoundsBit"; + while (model.getManager().hasVariable(outOfBoundsVarName)) { + outOfBoundsVarName += "_"; + } + outOfBoundsBit.emplace(model.getManager().declareBooleanVariable(outOfBoundsVarName), totalBitOffset, true, false); ++totalBitOffset; - } else { - outOfBoundsBit = boost::none; } createVariablesForVariableSet(model.getGlobalVariables(), reservedBitsForUnboundedVariables, true); @@ -260,12 +272,12 @@ uint_fast64_t VariableInformation::getTotalBitOffset(bool roundTo64Bit) const { } bool VariableInformation::hasOutOfBoundsBit() const { - return outOfBoundsBit != boost::none; + return outOfBoundsBit.has_value(); } uint64_t VariableInformation::getOutOfBoundsBit() const { assert(hasOutOfBoundsBit()); - return outOfBoundsBit.get(); + return outOfBoundsBit->bitOffset; } void VariableInformation::sortVariables() { diff --git a/src/storm/generator/VariableInformation.h b/src/storm/generator/VariableInformation.h index 6ca21952f3..2ce4dce0f9 100644 --- a/src/storm/generator/VariableInformation.h +++ b/src/storm/generator/VariableInformation.h @@ -1,8 +1,6 @@ #ifndef STORM_GENERATOR_VARIABLEINFORMATION_H_ #define STORM_GENERATOR_VARIABLEINFORMATION_H_ -#include -#include #include #include @@ -97,8 +95,14 @@ struct LocationVariableInformation { }; struct ObservationLabelInformation { - ObservationLabelInformation(std::string const& name); - std::string name; + ObservationLabelInformation(storm::expressions::Variable const& variable); + + std::string const& getName() const { + return variable.getName(); + } + + storm::expressions::Variable variable; + bool deterministic = true; }; @@ -139,9 +143,9 @@ struct VariableInformation { uint64_t getOutOfBoundsBit() const; - private: - boost::optional outOfBoundsBit; + std::optional outOfBoundsBit; + private: /*! * Sorts the variables to establish a known ordering. */ diff --git a/src/storm/io/DirectEncodingExporter.cpp b/src/storm/io/DirectEncodingExporter.cpp index 2f21aede6f..0c9cf4e798 100644 --- a/src/storm/io/DirectEncodingExporter.cpp +++ b/src/storm/io/DirectEncodingExporter.cpp @@ -166,7 +166,7 @@ void explicitExportSparseModel(std::ostream& os, std::shared_ptrhasStateValuations()) { - os << "//" << sparseModel->getStateValuations().getStateInfo(group) << '\n'; + os << "//" << sparseModel->getStateValuations().toString(group) << '\n'; } // Write probabilities diff --git a/src/storm/modelchecker/results/ExplicitQualitativeCheckResult.cpp b/src/storm/modelchecker/results/ExplicitQualitativeCheckResult.cpp index ef076bb206..959c31ee3e 100644 --- a/src/storm/modelchecker/results/ExplicitQualitativeCheckResult.cpp +++ b/src/storm/modelchecker/results/ExplicitQualitativeCheckResult.cpp @@ -298,7 +298,7 @@ storm::storage::Scheduler& ExplicitQualitativeCheckResult: template void insertJsonEntry(storm::json& json, uint64_t const& id, bool value, - std::optional const& stateValuations = std::nullopt, + std::optional const& stateValuations = std::nullopt, std::optional const& stateLabels = std::nullopt) { storm::json entry; if (stateValuations) { @@ -316,7 +316,7 @@ void insertJsonEntry(storm::json& json, uint64_t const& id, bo template template -storm::json ExplicitQualitativeCheckResult::toJson(std::optional const& stateValuations, +storm::json ExplicitQualitativeCheckResult::toJson(std::optional const& stateValuations, std::optional const& stateLabels) const { storm::json result; if (this->isResultForAllStates()) { @@ -335,29 +335,29 @@ storm::json ExplicitQualitativeCheckResult::toJson( // Explicit template instantiations template class ExplicitQualitativeCheckResult; -template storm::json ExplicitQualitativeCheckResult::toJson(std::optional const&, +template storm::json ExplicitQualitativeCheckResult::toJson(std::optional const&, std::optional const&) const; template storm::json ExplicitQualitativeCheckResult::toJson( - std::optional const&, std::optional const&) const; + std::optional const&, std::optional const&) const; template class ExplicitQualitativeCheckResult; template storm::json ExplicitQualitativeCheckResult::toJson( - std::optional const&, std::optional const&) const; + std::optional const&, std::optional const&) const; template storm::json ExplicitQualitativeCheckResult::toJson( - std::optional const&, std::optional const&) const; + std::optional const&, std::optional const&) const; template class ExplicitQualitativeCheckResult; template storm::json ExplicitQualitativeCheckResult::toJson( - std::optional const&, std::optional const&) const; + std::optional const&, std::optional const&) const; template storm::json ExplicitQualitativeCheckResult::toJson( - std::optional const&, std::optional const&) const; + std::optional const&, std::optional const&) const; template class ExplicitQualitativeCheckResult; -template storm::json ExplicitQualitativeCheckResult::toJson(std::optional const&, +template storm::json ExplicitQualitativeCheckResult::toJson(std::optional const&, std::optional const&) const; template storm::json ExplicitQualitativeCheckResult::toJson( - std::optional const&, std::optional const&) const; + std::optional const&, std::optional const&) const; } // namespace modelchecker } // namespace storm diff --git a/src/storm/modelchecker/results/ExplicitQualitativeCheckResult.h b/src/storm/modelchecker/results/ExplicitQualitativeCheckResult.h index 70a1053755..503e227c61 100644 --- a/src/storm/modelchecker/results/ExplicitQualitativeCheckResult.h +++ b/src/storm/modelchecker/results/ExplicitQualitativeCheckResult.h @@ -10,7 +10,7 @@ #include "storm/storage/BitVector.h" #include "storm/storage/Scheduler.h" #include "storm/storage/sparse/StateType.h" -#include "storm/storage/sparse/StateValuations.h" +#include "storm/storage/valuations/Valuations.h" namespace storm { @@ -69,7 +69,7 @@ class ExplicitQualitativeCheckResult : public QualitativeCheckResult { storm::storage::Scheduler& getScheduler(); template - storm::json toJson(std::optional const& stateValuations = std::nullopt, + storm::json toJson(std::optional const& stateValuations = std::nullopt, std::optional const& stateLabels = std::nullopt) const; private: diff --git a/src/storm/modelchecker/results/ExplicitQuantitativeCheckResult.cpp b/src/storm/modelchecker/results/ExplicitQuantitativeCheckResult.cpp index 57115c7751..3110fff724 100644 --- a/src/storm/modelchecker/results/ExplicitQuantitativeCheckResult.cpp +++ b/src/storm/modelchecker/results/ExplicitQuantitativeCheckResult.cpp @@ -458,7 +458,7 @@ void ExplicitQuantitativeCheckResult::oneMinus() { template void insertJsonEntry(storm::json& json, uint64_t const& id, ValueType const& value, - std::optional const& stateValuations = std::nullopt, + std::optional const& stateValuations = std::nullopt, std::optional const& stateLabels = std::nullopt) { typename storm::json entry; if (stateValuations) { @@ -475,7 +475,7 @@ void insertJsonEntry(storm::json& json, uint64_t const& id, ValueType } template -storm::json ExplicitQuantitativeCheckResult::toJson(std::optional const& stateValuations, +storm::json ExplicitQuantitativeCheckResult::toJson(std::optional const& stateValuations, std::optional const& stateLabels) const { storm::json result; if (this->isResultForAllStates()) { @@ -494,7 +494,7 @@ storm::json ExplicitQuantitativeCheckResult::toJson(std::o template<> storm::json ExplicitQuantitativeCheckResult::toJson( - std::optional const&, std::optional const&) const { + std::optional const&, std::optional const&) const { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Export of Check results is not supported for Rational Functions."); } diff --git a/src/storm/modelchecker/results/ExplicitQuantitativeCheckResult.h b/src/storm/modelchecker/results/ExplicitQuantitativeCheckResult.h index b1f9568576..173d2a49ef 100644 --- a/src/storm/modelchecker/results/ExplicitQuantitativeCheckResult.h +++ b/src/storm/modelchecker/results/ExplicitQuantitativeCheckResult.h @@ -10,7 +10,7 @@ #include "storm/models/sparse/StateLabeling.h" #include "storm/storage/Scheduler.h" #include "storm/storage/sparse/StateType.h" -#include "storm/storage/sparse/StateValuations.h" +#include "storm/storage/valuations/Valuations.h" namespace storm { @@ -77,7 +77,7 @@ class ExplicitQuantitativeCheckResult : public QuantitativeCheckResult const& getScheduler() const; storm::storage::Scheduler& getScheduler(); - storm::json toJson(std::optional const& stateValuations = std::nullopt, + storm::json toJson(std::optional const& stateValuations = std::nullopt, std::optional const& stateLabels = std::nullopt) const; private: diff --git a/src/storm/models/sparse/Model.cpp b/src/storm/models/sparse/Model.cpp index 4838cb89a2..989de61deb 100644 --- a/src/storm/models/sparse/Model.cpp +++ b/src/storm/models/sparse/Model.cpp @@ -86,8 +86,8 @@ void Model::assertValidityOfComponents( !this->hasChoiceLabeling() || this->getChoiceLabeling().getNumberOfItems() == choiceCount, storm::exceptions::IllegalArgumentException, "Invalid choice count of choice labeling (choices: " << choiceCount << " vs. labeling:" << this->getChoiceLabeling().getNumberOfItems() << ")."); STORM_LOG_THROW( - !this->hasStateValuations() || this->getStateValuations().getNumberOfStates() == stateCount, storm::exceptions::IllegalArgumentException, - "Invalid state count for state valuations (states: " << stateCount << " vs. valuations:" << this->getStateValuations().getNumberOfStates() << ")."); + !this->hasStateValuations() || this->getStateValuations().getNumberOfEntities() == stateCount, storm::exceptions::IllegalArgumentException, + "Invalid state count for state valuations (states: " << stateCount << " vs. valuations:" << this->getStateValuations().getNumberOfEntities() << ")."); STORM_LOG_THROW( !this->hasChoiceOrigins() || this->getChoiceOrigins()->getNumberOfChoices() == choiceCount, storm::exceptions::IllegalArgumentException, "Invalid choice count for choice origins. (choices: " << choiceCount << " vs. origins:" << this->getChoiceOrigins()->getNumberOfChoices() << ")."); @@ -352,17 +352,17 @@ bool Model::hasStateValuations() const { } template -storm::storage::sparse::StateValuations const& Model::getStateValuations() const { +storm::storage::sparse::Valuations const& Model::getStateValuations() const { return stateValuations.value(); } template -std::optional const& Model::getOptionalStateValuations() const { +std::optional const& Model::getOptionalStateValuations() const { return stateValuations; } template -std::optional& Model::getOptionalStateValuations() { +std::optional& Model::getOptionalStateValuations() { return stateValuations; } @@ -470,7 +470,7 @@ void Model::writeDotToStream(std::ostream& outStream if (includeLabeling || firstValue != nullptr || secondValue != nullptr || hasStateValuations()) { outStream << "label = \"" << state; if (hasStateValuations()) { - std::string stateInfo = getStateValuations().getStateInfo(state); + std::string stateInfo = getStateValuations().toString(state); std::vector results; boost::split(results, stateInfo, [](char c) { return c == ','; }); storm::io::outputFixedWidth(outStream, results, maxWidthLabel); diff --git a/src/storm/models/sparse/Model.h b/src/storm/models/sparse/Model.h index 469fdc03db..c1536af942 100644 --- a/src/storm/models/sparse/Model.h +++ b/src/storm/models/sparse/Model.h @@ -13,7 +13,7 @@ #include "storm/storage/sparse/ChoiceOrigins.h" #include "storm/storage/sparse/ModelComponents.h" #include "storm/storage/sparse/StateType.h" -#include "storm/storage/sparse/StateValuations.h" +#include "storm/storage/valuations/Valuations.h" namespace storm { namespace storage { @@ -271,21 +271,21 @@ class Model : public storm::models::Model { * * @return The valuations of the states of the model. */ - storm::storage::sparse::StateValuations const& getStateValuations() const; + storm::storage::sparse::Valuations const& getStateValuations() const; /*! * Retrieves an optional value that contains the state valuations if there are some. * * @return The state valuations, if they're saved. */ - std::optional const& getOptionalStateValuations() const; + std::optional const& getOptionalStateValuations() const; /*! * Retrieves an optional value that contains the state valuations if there are some. * * @return The state valuations, if they're saved. */ - std::optional& getOptionalStateValuations(); + std::optional& getOptionalStateValuations(); /*! * Retrieves whether this model was build with choice origins. @@ -440,7 +440,7 @@ class Model : public storm::models::Model { std::optional choiceLabeling; // if set, retrieves for each state the variable valuation that this state represents - std::optional stateValuations; + std::optional stateValuations; // if set, gives information about where each choice originates w.r.t. the input model description std::optional> choiceOrigins; diff --git a/src/storm/models/sparse/Pomdp.cpp b/src/storm/models/sparse/Pomdp.cpp index 8f52964b25..57d1f51ef3 100644 --- a/src/storm/models/sparse/Pomdp.cpp +++ b/src/storm/models/sparse/Pomdp.cpp @@ -121,12 +121,12 @@ bool Pomdp::hasObservationValuations() const { } template -storm::storage::sparse::StateValuations const &Pomdp::getObservationValuations() const { +storm::storage::sparse::Valuations const &Pomdp::getObservationValuations() const { return observationValuations.value(); } template -std::optional const &Pomdp::getOptionalObservationValuations() const { +std::optional const &Pomdp::getOptionalObservationValuations() const { return observationValuations; } diff --git a/src/storm/models/sparse/Pomdp.h b/src/storm/models/sparse/Pomdp.h index 1bbf21a17d..d96147cee6 100644 --- a/src/storm/models/sparse/Pomdp.h +++ b/src/storm/models/sparse/Pomdp.h @@ -77,9 +77,9 @@ class Pomdp : public Mdp { bool hasObservationValuations() const; - storm::storage::sparse::StateValuations const &getObservationValuations() const; + storm::storage::sparse::Valuations const &getObservationValuations() const; - std::optional const &getOptionalObservationValuations() const; + std::optional const &getOptionalObservationValuations() const; bool isCanonic() const; @@ -102,7 +102,7 @@ class Pomdp : public Mdp { uint64_t nrObservations; bool canonicFlag = false; - std::optional observationValuations; + std::optional observationValuations; void computeNrObservations(); }; diff --git a/src/storm/storage/Scheduler.cpp b/src/storm/storage/Scheduler.cpp index 7b772ecb9c..5e7d7ccf08 100644 --- a/src/storm/storage/Scheduler.cpp +++ b/src/storm/storage/Scheduler.cpp @@ -203,7 +203,7 @@ void Scheduler::printToStream(std::ostream& out, std::shared_ptrhasChoiceOrigins(); uint_fast64_t widthOfStates = std::to_string(schedulerChoices.front().size()).length(); if (stateValuationsGiven) { - widthOfStates += model->getStateValuations().getStateInfo(schedulerChoices.front().size() - 1).length() + 5; + widthOfStates += model->getStateValuations().toString(schedulerChoices.front().size() - 1).length() + 5; } widthOfStates = std::max(widthOfStates, (uint_fast64_t)12); uint_fast64_t numOfSkippedStatesWithUniqueChoice = 0; @@ -228,7 +228,7 @@ void Scheduler::printToStream(std::ostream& out, std::shared_ptrgetStateValuations().getStateInfo(state)); + out << std::setw(widthOfStates) << (std::to_string(state) + ": " + model->getStateValuations().toString(state)); } else { out << std::setw(widthOfStates) << state; } diff --git a/src/storm/storage/expressions/ExpressionManager.cpp b/src/storm/storage/expressions/ExpressionManager.cpp index 6dd89b2014..e1a4778a32 100644 --- a/src/storm/storage/expressions/ExpressionManager.cpp +++ b/src/storm/storage/expressions/ExpressionManager.cpp @@ -185,6 +185,10 @@ Variable ExpressionManager::declareArrayVariable(std::string const& name, Type c return this->declareVariable(name, this->getArrayType(elementType), auxiliary); } +Variable ExpressionManager::declareStringVariable(std::string const& name, bool auxiliary) { + return this->declareVariable(name, this->getStringType(), auxiliary); +} + Variable ExpressionManager::declareOrGetVariable(std::string const& name, storm::expressions::Type const& variableType, bool auxiliary) { return declareOrGetVariable(name, variableType, auxiliary, true); } diff --git a/src/storm/storage/expressions/ExpressionManager.h b/src/storm/storage/expressions/ExpressionManager.h index 138831aa5a..c2c667f947 100644 --- a/src/storm/storage/expressions/ExpressionManager.h +++ b/src/storm/storage/expressions/ExpressionManager.h @@ -240,6 +240,14 @@ class ExpressionManager : public std::enable_shared_from_this */ Variable declareArrayVariable(std::string const& name, Type const& elementType, bool auxiliary = false); + /*! + * Declares a new string variable with the given name + * + * @param name The name of the variable. + * @param auxiliary A flag indicating whether the new variable should be tagged as an auxiliary variable. + */ + Variable declareStringVariable(std::string const& name, bool auxiliary = false); + /*! * Declares a variable with the given name if it does not yet exist. * diff --git a/src/storm/storage/expressions/Variable.cpp b/src/storm/storage/expressions/Variable.cpp index c387b1e006..8f1b887bd2 100644 --- a/src/storm/storage/expressions/Variable.cpp +++ b/src/storm/storage/expressions/Variable.cpp @@ -75,5 +75,9 @@ bool Variable::hasRationalType() const { bool Variable::hasNumericalType() const { return this->getType().isNumericalType(); } + +bool Variable::hasStringType() const { + return this->getType().isStringType(); +} } // namespace expressions } // namespace storm diff --git a/src/storm/storage/expressions/Variable.h b/src/storm/storage/expressions/Variable.h index e25c6435ac..475a4c494c 100644 --- a/src/storm/storage/expressions/Variable.h +++ b/src/storm/storage/expressions/Variable.h @@ -124,17 +124,24 @@ class Variable { /*! * Checks whether the variable is of rational type. * - * @return True iff the variable if of rational type. + * @return True iff the variable is of rational type. */ bool hasRationalType() const; /*! * Checks whether the variable is of numerical type. * - * @return True iff the variable if of numerical type. + * @return True iff the variable is of numerical type. */ bool hasNumericalType() const; + /*! + * Checks whether the variable is of string type. + * + * @return True iff the variable is of string type. + */ + bool hasStringType() const; + private: // The manager that is responsible for this variable. ExpressionManager const* manager; diff --git a/src/storm/storage/sparse/ModelComponents.h b/src/storm/storage/sparse/ModelComponents.h index 9f774e22e0..2c92f9bd0a 100644 --- a/src/storm/storage/sparse/ModelComponents.h +++ b/src/storm/storage/sparse/ModelComponents.h @@ -14,7 +14,7 @@ #include "storm/storage/SparseMatrix.h" #include "storm/storage/sparse/ChoiceOrigins.h" #include "storm/storage/sparse/StateType.h" -#include "storm/storage/sparse/StateValuations.h" +#include "storm/storage/valuations/Valuations.h" #include "storm/exceptions/InvalidOperationException.h" #include "storm/utility/macros.h" @@ -64,14 +64,14 @@ struct ModelComponents { // A vector that stores a labeling for each choice. std::optional choiceLabeling; // stores for each state to which variable valuation it belongs - std::optional stateValuations; + std::optional stateValuations; // stores for each choice from which parts of the input model description it originates std::optional> choiceOrigins; // POMDP specific components // The POMDP observations std::optional> observabilityClasses; - std::optional observationValuations; + std::optional observationValuations; // Continuous time specific components (CTMCs, Markov Automata): // True iff the transition values (for Markovian choices) are interpreted as rates. diff --git a/src/storm/storage/sparse/StateValuationTransformer.cpp b/src/storm/storage/sparse/StateValuationTransformer.cpp deleted file mode 100644 index 481fdd9ead..0000000000 --- a/src/storm/storage/sparse/StateValuationTransformer.cpp +++ /dev/null @@ -1,89 +0,0 @@ -#include "storm/storage/sparse/StateValuationTransformer.h" -#include "storm/adapters/RationalNumberAdapter.h" -#include "storm/exceptions/InvalidArgumentException.h" -#include "storm/exceptions/NotSupportedException.h" -#include "storm/storage/expressions/ExpressionEvaluator.h" -#include "storm/storage/expressions/ExpressionManager.h" -#include "storm/utility/constants.h" - -namespace storm::storage::sparse { - -StateValuationTransformer::StateValuationTransformer(StateValuations const& oldStateValuations) : oldStateValuations(oldStateValuations) { - // Intentionally left empty. -} - -void StateValuationTransformer::addBooleanExpression(storm::expressions::Variable const& var, storm::expressions::Expression const& expr) { - STORM_LOG_THROW(var.getType().isBooleanType(), storm::exceptions::InvalidArgumentException, "Variable must have type `Boolean`."); - STORM_LOG_THROW(expr.getType().isBooleanType(), storm::exceptions::InvalidArgumentException, "Expression must have type `Boolean`."); - STORM_LOG_THROW(var.getManager() == oldStateValuations.getManager(), storm::exceptions::InvalidArgumentException, - "All variables must refer to same manager."); - booleanVariables.push_back(var); - booleanExpressions.push_back(expr); -} - -void StateValuationTransformer::addIntegerExpression(storm::expressions::Variable const& var, storm::expressions::Expression const& expr) { - STORM_LOG_THROW(var.getType().isIntegerType(), storm::exceptions::InvalidArgumentException, "Variable must have type `Integer`."); - STORM_LOG_THROW(expr.getType().isIntegerType(), storm::exceptions::InvalidArgumentException, "Expression must have type `Integer`."); - STORM_LOG_THROW(var.getManager() == oldStateValuations.getManager(), storm::exceptions::InvalidArgumentException, - "All variables must refer to same manager."); - integerVariables.push_back(var); - integerExpressions.push_back(expr); -} - -StateValuations StateValuationTransformer::build(bool extend) { - StateValuationsBuilder builder; - if (extend) { - STORM_LOG_ASSERT(oldStateValuations.getNumberOfStates() > 0, "Code assumes that there are states in the state valuations."); - // This assumption can of course be avoided, but 0state statevaluations are a corner case anyway. Probably better to fix once we have updated state - // valuations. - for (auto it = oldStateValuations.at(0).begin(); it != oldStateValuations.at(0).end(); ++it) { - builder.addVariable(it.getVariable()); - } - } - for (auto const& v : booleanVariables) { - builder.addVariable(v); - } - for (auto const& v : integerVariables) { - builder.addVariable(v); - } - - storm::expressions::ExpressionEvaluator evaluator(oldStateValuations.getManager()); - for (uint64_t state = 0; state < oldStateValuations.getNumberOfStates(); ++state) { - std::vector booleanValues{}; - std::vector integerValues{}; - // Copy variables into the new state valuations and setup the expression evaluator for the current state. - for (auto sv = oldStateValuations.at(state).begin(); sv != oldStateValuations.at(state).end(); ++sv) { - if (sv.isVariableAssignment()) { - auto const& var = sv.getVariable(); - if (sv.isBoolean()) { - evaluator.setBooleanValue(var, sv.getBooleanValue()); - if (extend) { - booleanValues.push_back(sv.getBooleanValue()); - } - } else if (sv.isInteger()) { - evaluator.setIntegerValue(var, sv.getIntegerValue()); - if (extend) { - integerValues.push_back(sv.getIntegerValue()); - } - } else { - STORM_LOG_ASSERT(sv.isRational(), "Must be RationalVariable"); - evaluator.setRationalValue(var, sv.getRationalValue()); - STORM_LOG_THROW(!extend, storm::exceptions::NotSupportedException, - "Extending state valuations with rational values is currently not supported."); - } - } else { - STORM_LOG_THROW(!extend, storm::exceptions::NotSupportedException, "Extending state valuations with label values is currently not supported."); - // Label assignments can be safely skipped. - } - } - for (auto const& expr : booleanExpressions) { - booleanValues.push_back(evaluator.asBool(expr)); - } - for (auto const& expr : integerExpressions) { - integerValues.push_back(evaluator.asInt(expr)); - } - builder.addState(state, std::move(booleanValues), std::move(integerValues)); - } - return builder.build(); -} -} // namespace storm::storage::sparse \ No newline at end of file diff --git a/src/storm/storage/sparse/StateValuationTransformer.h b/src/storm/storage/sparse/StateValuationTransformer.h deleted file mode 100644 index eb5621839b..0000000000 --- a/src/storm/storage/sparse/StateValuationTransformer.h +++ /dev/null @@ -1,40 +0,0 @@ -#pragma once -#include "storm/storage/expressions/Expression.h" -#include "storm/storage/sparse/StateValuations.h" - -namespace storm::storage::sparse { - -/*! - * Transforms the given state valuations to a new state valuations over a new variable set. - * The values of the new variables are determined by evaluating the provided expressions w.r.t. the old variable valuation. - * The freshly introduced variables may either replace or extend the existing variable set. - */ -class StateValuationTransformer { - public: - StateValuationTransformer(StateValuations const& oldStateValuations); - /*! - * Add a Boolean variable defined by the given expression. Note that these should all be over the same expression manager. - * @param var A variable with type Bool - * @param expr An expression with type Bool - */ - void addBooleanExpression(storm::expressions::Variable const& var, storm::expressions::Expression const& expr); - /*! - * Add a Integer variable defined by the given expression. See also addBooleanExpression. - */ - void addIntegerExpression(storm::expressions::Variable const& var, storm::expressions::Expression const& expr); - /*! - * Build and export the state valuations. Should be called only once. - * @param extend Whether to maintain also the existing variables. - * @return - */ - StateValuations build(bool extend); - - private: - StateValuations const& oldStateValuations; - std::vector booleanVariables; - std::vector booleanExpressions; - std::vector integerVariables; - std::vector integerExpressions; -}; - -} // namespace storm::storage::sparse \ No newline at end of file diff --git a/src/storm/storage/sparse/StateValuations.cpp b/src/storm/storage/sparse/StateValuations.cpp deleted file mode 100644 index 4cabde9c7a..0000000000 --- a/src/storm/storage/sparse/StateValuations.cpp +++ /dev/null @@ -1,454 +0,0 @@ -#include "storm/storage/sparse/StateValuations.h" - -#include - -#include "storm/adapters/JsonAdapter.h" - -#include "storm/adapters/RationalNumberForward.h" - -#include "storm/storage/BitVector.h" - -#include "storm/exceptions/InvalidTypeException.h" -#include "storm/utility/macros.h" -#include "storm/utility/vector.h" - -namespace storm { -namespace storage { -namespace sparse { - -StateValuations::StateValuation::StateValuation(std::vector&& booleanValues, std::vector&& integerValues, - std::vector&& rationalValues, std::vector&& observationLabelValues) - : booleanValues(std::move(booleanValues)), - integerValues(std::move(integerValues)), - rationalValues(std::move(rationalValues)), - observationLabelValues(std::move(observationLabelValues)) { - // Intentionally left empty -} - -typename StateValuations::StateValuation const& StateValuations::getValuation(storm::storage::sparse::state_type const& stateIndex) const { - STORM_LOG_ASSERT(stateIndex < valuations.size(), "Invalid state index."); - STORM_LOG_ASSERT(assertValuation(valuations[stateIndex]), "Invalid state valuations"); - return valuations[stateIndex]; -} - -StateValuations::StateValueIterator::StateValueIterator(typename std::map::const_iterator variableIt, - typename std::map::const_iterator labelIt, - typename std::map::const_iterator variableBegin, - typename std::map::const_iterator variableEnd, - typename std::map::const_iterator labelBegin, - typename std::map::const_iterator labelEnd, StateValuation const* valuation) - : variableIt(variableIt), - labelIt(labelIt), - variableBegin(variableBegin), - variableEnd(variableEnd), - labelBegin(labelBegin), - labelEnd(labelEnd), - valuation(valuation) { - // Intentionally left empty. -} - -bool StateValuations::StateValueIterator::isVariableAssignment() const { - return variableIt != variableEnd; -} - -bool StateValuations::StateValueIterator::isLabelAssignment() const { - return variableIt == variableEnd; -} - -storm::expressions::Variable const& StateValuations::StateValueIterator::getVariable() const { - STORM_LOG_ASSERT(isVariableAssignment(), "Does not point to a variable"); - return variableIt->first; -} -std::string const& StateValuations::StateValueIterator::getLabel() const { - STORM_LOG_ASSERT(isLabelAssignment(), "Does not point to a label"); - return labelIt->first; -} -bool StateValuations::StateValueIterator::isBoolean() const { - return isVariableAssignment() && getVariable().hasBooleanType(); -} -bool StateValuations::StateValueIterator::isInteger() const { - return isVariableAssignment() && getVariable().hasIntegerType(); -} -bool StateValuations::StateValueIterator::isRational() const { - return isVariableAssignment() && getVariable().hasRationalType(); -} - -std::string const& StateValuations::StateValueIterator::getName() const { - if (isVariableAssignment()) { - return getVariable().getName(); - } else { - return getLabel(); - } -} - -bool StateValuations::StateValueIterator::getBooleanValue() const { - STORM_LOG_ASSERT(isBoolean(), "Variable has no boolean type."); - return valuation->booleanValues[variableIt->second]; -} - -int64_t StateValuations::StateValueIterator::getIntegerValue() const { - STORM_LOG_ASSERT(isInteger(), "Variable has no integer type."); - return valuation->integerValues[variableIt->second]; -} - -int64_t StateValuations::StateValueIterator::getLabelValue() const { - STORM_LOG_ASSERT(isLabelAssignment(), "Not a label assignment"); - STORM_LOG_ASSERT(labelIt->second < valuation->observationLabelValues.size(), - "Label index " << labelIt->second << " larger than number of labels " << valuation->observationLabelValues.size()); - return valuation->observationLabelValues[labelIt->second]; -} - -storm::RationalNumber StateValuations::StateValueIterator::getRationalValue() const { - STORM_LOG_ASSERT(isRational(), "Variable has no rational type."); - return valuation->rationalValues[variableIt->second]; -} - -bool StateValuations::StateValueIterator::operator==(StateValueIterator const& other) const { - STORM_LOG_ASSERT(valuation == valuation, "Comparing iterators for different states"); - return variableIt == other.variableIt && labelIt == other.labelIt; -} -bool StateValuations::StateValueIterator::operator!=(StateValueIterator const& other) const { - return !(*this == other); -} - -typename StateValuations::StateValueIterator& StateValuations::StateValueIterator::operator++() { - if (variableIt != variableEnd) { - ++variableIt; - } else { - ++labelIt; - } - - return *this; -} - -typename StateValuations::StateValueIterator& StateValuations::StateValueIterator::operator--() { - if (labelIt != labelBegin) { - --labelIt; - } else { - --variableIt; - } - return *this; -} - -StateValuations::StateValueIteratorRange::StateValueIteratorRange(std::map const& variableMap, - std::map const& labelMap, StateValuation const* valuation) - : variableMap(variableMap), labelMap(labelMap), valuation(valuation) { - // Intentionally left empty. -} - -StateValuations::StateValueIterator StateValuations::StateValueIteratorRange::begin() const { - return StateValueIterator(variableMap.cbegin(), labelMap.cbegin(), variableMap.cbegin(), variableMap.cend(), labelMap.cbegin(), labelMap.cend(), valuation); -} - -StateValuations::StateValueIterator StateValuations::StateValueIteratorRange::end() const { - return StateValueIterator(variableMap.cend(), labelMap.cend(), variableMap.cbegin(), variableMap.cend(), labelMap.cbegin(), labelMap.cend(), valuation); -} - -bool StateValuations::getBooleanValue(storm::storage::sparse::state_type const& stateIndex, storm::expressions::Variable const& booleanVariable) const { - auto const& valuation = getValuation(stateIndex); - STORM_LOG_ASSERT(variableToIndexMap.count(booleanVariable) > 0, "Variable " << booleanVariable.getName() << " is not part of this valuation."); - STORM_LOG_ASSERT(booleanVariable.hasBooleanType(), "Variable " << booleanVariable.getName() << " has no Boolean type."); - return valuation.booleanValues[variableToIndexMap.at(booleanVariable)]; -} - -int64_t const& StateValuations::getIntegerValue(storm::storage::sparse::state_type const& stateIndex, - storm::expressions::Variable const& integerVariable) const { - auto const& valuation = getValuation(stateIndex); - STORM_LOG_ASSERT(variableToIndexMap.count(integerVariable) > 0, "Variable " << integerVariable.getName() << " is not part of this valuation."); - STORM_LOG_ASSERT(integerVariable.hasIntegerType(), "Variable " << integerVariable.getName() << " has no integer type."); - return valuation.integerValues[variableToIndexMap.at(integerVariable)]; -} - -storm::RationalNumber const& StateValuations::getRationalValue(storm::storage::sparse::state_type const& stateIndex, - storm::expressions::Variable const& rationalVariable) const { - auto const& valuation = getValuation(stateIndex); - STORM_LOG_ASSERT(variableToIndexMap.count(rationalVariable) > 0, "Variable " << rationalVariable.getName() << " is not part of this valuation."); - STORM_LOG_ASSERT(rationalVariable.hasRationalType(), "Variable " << rationalVariable.getName() << " has no rational type."); - return valuation.rationalValues[variableToIndexMap.at(rationalVariable)]; -} - -storm::storage::BitVector StateValuations::getBooleanValues(storm::expressions::Variable const& booleanVariable) const { - STORM_LOG_ASSERT(variableToIndexMap.count(booleanVariable) > 0, "Variable " << booleanVariable.getName() << " is not part of this valuation."); - STORM_LOG_ASSERT(booleanVariable.hasBooleanType(), "Variable " << booleanVariable.getName() << " has no Boolean type."); - auto const varIndex = variableToIndexMap.at(booleanVariable); - storm::storage::BitVector result(getNumberOfStates(), false); - for (uint64_t stateIndex = 0; stateIndex < getNumberOfStates(); ++stateIndex) { - if (getValuation(stateIndex).booleanValues[varIndex]) { - result.set(stateIndex); - } - } - return result; -} - -std::vector StateValuations::getIntegerValues(storm::expressions::Variable const& integerVariable) const { - STORM_LOG_ASSERT(variableToIndexMap.count(integerVariable) > 0, "Variable " << integerVariable.getName() << " is not part of this valuation."); - STORM_LOG_ASSERT(integerVariable.hasIntegerType(), "Variable " << integerVariable.getName() << " has no integer type."); - auto const varIndex = variableToIndexMap.at(integerVariable); - std::vector result; - result.reserve(getNumberOfStates()); - for (uint64_t stateIndex = 0; stateIndex < getNumberOfStates(); ++stateIndex) { - result.push_back(getValuation(stateIndex).integerValues[varIndex]); - } - return result; -} - -std::vector StateValuations::getRationalValues(storm::expressions::Variable const& rationalVariable) const { - STORM_LOG_ASSERT(variableToIndexMap.count(rationalVariable) > 0, "Variable " << rationalVariable.getName() << " is not part of this valuation."); - STORM_LOG_ASSERT(rationalVariable.hasRationalType(), "Variable " << rationalVariable.getName() << " has no rational type."); - auto const varIndex = variableToIndexMap.at(rationalVariable); - std::vector result; - result.reserve(getNumberOfStates()); - for (uint64_t stateIndex = 0; stateIndex < getNumberOfStates(); ++stateIndex) { - result.push_back(getValuation(stateIndex).rationalValues[varIndex]); - } - return result; -} - -bool StateValuations::isEmpty(storm::storage::sparse::state_type const& stateIndex) const { - auto const& valuation = valuations[stateIndex]; // Do not use getValuations, as that is only valid after adding stuff. - return valuation.booleanValues.empty() && valuation.integerValues.empty() && valuation.rationalValues.empty() && valuation.observationLabelValues.empty(); -} - -std::string StateValuations::toString(storm::storage::sparse::state_type const& stateIndex, bool pretty, - boost::optional> const& selectedVariables) const { - auto const& valueAssignment = at(stateIndex); - typename std::set::const_iterator setIt; - if (selectedVariables) { - setIt = selectedVariables->begin(); - } - std::vector assignments; - for (auto valIt = valueAssignment.begin(); valIt != valueAssignment.end(); ++valIt) { - if (selectedVariables && (*setIt != valIt.getVariable())) { - continue; - } - - std::stringstream stream; - if (pretty) { - if (valIt.isBoolean() && !valIt.getBooleanValue()) { - stream << "!"; - } - stream << valIt.getName(); - if (valIt.isInteger()) { - stream << "=" << valIt.getIntegerValue(); - } else if (valIt.isRational()) { - stream << "=" << valIt.getRationalValue(); - } else if (valIt.isLabelAssignment()) { - stream << "=" << valIt.getLabelValue(); - } else { - STORM_LOG_THROW(valIt.isBoolean(), storm::exceptions::InvalidTypeException, "Unexpected variable type."); - } - } else { - if (valIt.isBoolean()) { - stream << std::boolalpha << valIt.getBooleanValue() << std::noboolalpha; - } else if (valIt.isInteger()) { - stream << valIt.getIntegerValue(); - } else if (valIt.isRational()) { - stream << valIt.getRationalValue(); - } else if (valIt.isLabelAssignment()) { - stream << valIt.getLabelValue(); - } - } - assignments.push_back(stream.str()); - - if (selectedVariables) { - // Go to next selected position - ++setIt; - } - } - STORM_LOG_ASSERT(!selectedVariables || setIt == selectedVariables->end(), "Valuation does not consider selected variable " << setIt->getName() << "."); - - if (pretty) { - return "[" + boost::join(assignments, "\t& ") + "]"; - } else { - return "[" + boost::join(assignments, "\t") + "]"; - } -} - -template -storm::json StateValuations::toJson(storm::storage::sparse::state_type const& stateIndex, - boost::optional> const& selectedVariables) const { - auto const& valueAssignment = at(stateIndex); - typename std::set::const_iterator setIt; - if (selectedVariables) { - setIt = selectedVariables->begin(); - } - storm::json result; - for (auto valIt = valueAssignment.begin(); valIt != valueAssignment.end(); ++valIt) { - if (selectedVariables && (*setIt != valIt.getVariable())) { - continue; - } - - if (valIt.isBoolean()) { - result[valIt.getName()] = valIt.getBooleanValue(); - } else if (valIt.isInteger()) { - result[valIt.getName()] = valIt.getIntegerValue(); - } else if (valIt.isLabelAssignment()) { - result[valIt.getLabel()] = valIt.getLabelValue(); - } else { - STORM_LOG_ASSERT(valIt.isRational(), "Unexpected variable type for variable " << valIt.getName()); - result[valIt.getName()] = storm::utility::convertNumber(valIt.getRationalValue()); - } - - if (selectedVariables) { - // Go to next selected position - ++setIt; - } - } - return result; -} - -bool StateValuations::assertValuation(StateValuation const& valuation) const { - storm::storage::BitVector foundBooleanValues(valuation.booleanValues.size(), false); - storm::storage::BitVector foundIntegerValues(valuation.integerValues.size(), false); - storm::storage::BitVector foundRationalValues(valuation.rationalValues.size(), false); - for (auto const& varIndex : variableToIndexMap) { - storm::storage::BitVector* bv; - if (varIndex.first.hasBooleanType()) { - bv = &foundBooleanValues; - } else if (varIndex.first.hasIntegerType()) { - bv = &foundIntegerValues; - } else if (varIndex.first.hasRationalType()) { - bv = &foundRationalValues; - } else { - STORM_LOG_THROW(false, storm::exceptions::InvalidTypeException, "Unexpected variable type."); - } - if (varIndex.second < bv->size()) { - if (bv->get(varIndex.second)) { - STORM_LOG_ERROR("Multiple variables refer to the same value index"); - return false; - } - bv->set(varIndex.second, true); - } else { - STORM_LOG_ERROR("Valuation does not provide a value for variable: " << varIndex.first.getName()); - return false; - } - } - if (!(foundBooleanValues.full() && foundIntegerValues.full() && foundRationalValues.full())) { - STORM_LOG_ERROR("Valuation has too many entries."); - } - return true; -} - -StateValuations::StateValuations(std::map const& variableToIndexMap, std::vector&& valuations) - : variableToIndexMap(variableToIndexMap), valuations(valuations) { - // Intentionally left empty -} - -std::string StateValuations::getStateInfo(state_type const& state) const { - STORM_LOG_ASSERT(state < getNumberOfStates(), "Invalid state index."); - return this->toString(state); -} - -typename StateValuations::StateValueIteratorRange StateValuations::at(state_type const& state) const { - STORM_LOG_ASSERT(state < getNumberOfStates(), "Invalid state index " << state << ", have only " << getNumberOfStates() << " states."); - return StateValueIteratorRange({variableToIndexMap, observationLabels, &(valuations[state])}); -} - -uint_fast64_t StateValuations::getNumberOfStates() const { - return valuations.size(); -} - -std::size_t StateValuations::hash() const { - return 0; -} - -StateValuations StateValuations::selectStates(storm::storage::BitVector const& selectedStates) const { - return StateValuations(variableToIndexMap, storm::utility::vector::filterVector(valuations, selectedStates)); -} - -StateValuations StateValuations::selectStates(std::vector const& selectedStates) const { - std::vector selectedValuations; - selectedValuations.reserve(selectedStates.size()); - for (auto const& selectedState : selectedStates) { - if (selectedState < valuations.size()) { - selectedValuations.push_back(valuations[selectedState]); - } else { - selectedValuations.emplace_back(); - } - } - return StateValuations(variableToIndexMap, std::move(selectedValuations)); -} - -StateValuations StateValuations::blowup(const std::vector& mapNewToOld) const { - std::vector newValuations; - for (auto const& oldState : mapNewToOld) { - newValuations.push_back(valuations[oldState]); - } - return StateValuations(variableToIndexMap, std::move(newValuations)); -} - -storm::expressions::ExpressionManager const& StateValuations::getManager() const { - STORM_LOG_ASSERT(!variableToIndexMap.empty(), "Cannot be called on state valuations without variables."); - return variableToIndexMap.begin()->first.getManager(); -} - -StateValuationsBuilder::StateValuationsBuilder() : booleanVarCount(0), integerVarCount(0), rationalVarCount(0), labelCount(0) { - // Intentionally left empty. -} - -void StateValuationsBuilder::addVariable(storm::expressions::Variable const& variable) { - STORM_LOG_ASSERT(currentStateValuations.valuations.empty(), "Tried to add a variable, although a state has already been added before."); - STORM_LOG_ASSERT(currentStateValuations.variableToIndexMap.count(variable) == 0, "Variable " << variable.getName() << " already added."); - if (variable.hasBooleanType()) { - currentStateValuations.variableToIndexMap[variable] = booleanVarCount++; - } - if (variable.hasIntegerType()) { - currentStateValuations.variableToIndexMap[variable] = integerVarCount++; - } - if (variable.hasRationalType()) { - currentStateValuations.variableToIndexMap[variable] = rationalVarCount++; - } -} - -void StateValuationsBuilder::addObservationLabel(const std::string& label) { - currentStateValuations.observationLabels[label] = labelCount++; -} - -void StateValuationsBuilder::addState(storm::storage::sparse::state_type const& state, std::vector&& booleanValues, - std::vector&& integerValues) { - addState(state, std::move(booleanValues), std::move(integerValues), {}); -} - -void StateValuationsBuilder::addState(storm::storage::sparse::state_type const& state, std::vector&& booleanValues, std::vector&& integerValues, - std::vector&& rationalValues, std::vector&& observationLabelValues) { - if (state > currentStateValuations.valuations.size()) { - currentStateValuations.valuations.resize(state); - } - if (state == currentStateValuations.valuations.size()) { - currentStateValuations.valuations.emplace_back(std::move(booleanValues), std::move(integerValues), std::move(rationalValues), - std::move(observationLabelValues)); - } else { - STORM_LOG_ASSERT(currentStateValuations.isEmpty(state), "Adding a valuation to the same state multiple times."); - currentStateValuations.valuations[state] = typename StateValuations::StateValuation(std::move(booleanValues), std::move(integerValues), - std::move(rationalValues), std::move(observationLabelValues)); - } -} - -uint64_t StateValuationsBuilder::getBooleanVarCount() const { - return booleanVarCount; -} - -uint64_t StateValuationsBuilder::getIntegerVarCount() const { - return integerVarCount; -} - -uint64_t StateValuationsBuilder::getLabelCount() const { - return labelCount; -} - -StateValuations StateValuationsBuilder::build() { - booleanVarCount = 0; - integerVarCount = 0; - rationalVarCount = 0; - labelCount = 0; - return std::move(currentStateValuations); -} - -template storm::json StateValuations::toJson(storm::storage::sparse::state_type const&, - boost::optional> const&) const; -template storm::json StateValuations::toJson( - storm::storage::sparse::state_type const&, boost::optional> const&) const; - -} // namespace sparse -} // namespace storage -} // namespace storm diff --git a/src/storm/storage/sparse/StateValuations.h b/src/storm/storage/sparse/StateValuations.h deleted file mode 100644 index cd50aa57be..0000000000 --- a/src/storm/storage/sparse/StateValuations.h +++ /dev/null @@ -1,215 +0,0 @@ -#pragma once - -#include -#include -#include - -#include "storm/adapters/JsonForward.h" -#include "storm/adapters/RationalNumberForward.h" -#include "storm/models/sparse/StateAnnotation.h" -#include "storm/storage/BitVector.h" -#include "storm/storage/expressions/Variable.h" -#include "storm/storage/sparse/StateType.h" - -namespace storm { -namespace storage { -namespace sparse { - -class StateValuationsBuilder; - -// A structure holding information about the reachable state space that can be retrieved from the outside. -class StateValuations : public storm::models::sparse::StateAnnotation { - public: - friend class StateValuationsBuilder; - - class StateValuation { - public: - friend class StateValuations; - StateValuation() = default; - StateValuation(std::vector&& booleanValues, std::vector&& integerValues, std::vector&& rationalValues, - std::vector&& observationLabelValues = {}); - - private: - std::vector booleanValues; - std::vector integerValues; - std::vector rationalValues; - std::vector observationLabelValues; - }; - - class StateValueIterator { - public: - StateValueIterator(typename std::map::const_iterator variableIt, - typename std::map::const_iterator labelIt, - typename std::map::const_iterator variableBegin, - typename std::map::const_iterator variableEnd, - typename std::map::const_iterator labelBegin, - typename std::map::const_iterator labelEnd, StateValuation const* valuation); - bool operator==(StateValueIterator const& other) const; - bool operator!=(StateValueIterator const& other) const; - StateValueIterator& operator++(); - StateValueIterator& operator--(); - - bool isVariableAssignment() const; - bool isLabelAssignment() const; - storm::expressions::Variable const& getVariable() const; - std::string const& getLabel() const; - bool isBoolean() const; - bool isInteger() const; - bool isRational() const; - - std::string const& getName() const; - - // These shall only be called if the variable has the correct type - bool getBooleanValue() const; - int64_t getIntegerValue() const; - storm::RationalNumber getRationalValue() const; - int64_t getLabelValue() const; - - private: - typename std::map::const_iterator variableIt; - typename std::map::const_iterator labelIt; - typename std::map::const_iterator variableBegin; - typename std::map::const_iterator variableEnd; - typename std::map::const_iterator labelBegin; - typename std::map::const_iterator labelEnd; - - StateValuation const* const valuation; - }; - - class StateValueIteratorRange { - public: - StateValueIteratorRange(std::map const& variableMap, std::map const& labelMap, - StateValuation const* valuation); - StateValueIterator begin() const; - StateValueIterator end() const; - - private: - std::map const& variableMap; - std::map const& labelMap; - StateValuation const* const valuation; - }; - - StateValuations() = default; - virtual ~StateValuations() = default; - virtual std::string getStateInfo(storm::storage::sparse::state_type const& state) const override; - StateValueIteratorRange at(storm::storage::sparse::state_type const& state) const; - - storm::expressions::ExpressionManager const& getManager() const; - - bool getBooleanValue(storm::storage::sparse::state_type const& stateIndex, storm::expressions::Variable const& booleanVariable) const; - int64_t const& getIntegerValue(storm::storage::sparse::state_type const& stateIndex, storm::expressions::Variable const& integerVariable) const; - storm::RationalNumber const& getRationalValue(storm::storage::sparse::state_type const& stateIndex, - storm::expressions::Variable const& rationalVariable) const; - /// Returns true, if this valuation does not contain any value. - bool isEmpty(storm::storage::sparse::state_type const& stateIndex) const; - - /*! - * Returns a vector of size getNumberOfStates() such that the i'th entry is the value of the given variable of state i. - */ - storm::storage::BitVector getBooleanValues(storm::expressions::Variable const& booleanVariable) const; - - /*! - * Returns a vector of size getNumberOfStates() such that the i'th entry is the value of the given variable of state i. - */ - std::vector getIntegerValues(storm::expressions::Variable const& integerVariable) const; - - /*! - * Returns a vector of size getNumberOfStates() such that the i'th entry is the value of the given variable of state i. - */ - std::vector getRationalValues(storm::expressions::Variable const& rationalVariable) const; - - /*! - * Returns a string representation of the valuation. - * - * @param selectedVariables If given, only the informations for the variables in this set are processed. - * @return The string representation. - */ - std::string toString(storm::storage::sparse::state_type const& stateIndex, bool pretty = true, - boost::optional> const& selectedVariables = boost::none) const; - - /*! - * Returns a JSON representation of this valuation - * @param selectedVariables If given, only the informations for the variables in this set are processed. - * @return - */ - template - storm::json toJson(storm::storage::sparse::state_type const& stateIndex, - boost::optional> const& selectedVariables = boost::none) const; - - // Returns the (current) number of states that this object describes. - uint_fast64_t getNumberOfStates() const; - - /* - * Derive new state valuations from this by selecting the given states. - */ - StateValuations selectStates(storm::storage::BitVector const& selectedStates) const; - - /* - * Derive new state valuations from this by selecting the given states. - * If an invalid state index is selected, the corresponding valuation will be empty. - */ - StateValuations selectStates(std::vector const& selectedStates) const; - - StateValuations blowup(std::vector const& mapNewToOld) const; - - virtual std::size_t hash() const; - - private: - StateValuations(std::map const& variableToIndexMap, std::vector&& valuations); - bool assertValuation(StateValuation const& valuation) const; - StateValuation const& getValuation(storm::storage::sparse::state_type const& stateIndex) const; - - std::map variableToIndexMap; - std::map observationLabels; - // A mapping from state indices to their variable valuations. - std::vector valuations; -}; - -class StateValuationsBuilder { - public: - StateValuationsBuilder(); - - /*! Adds a new variable to keep track of for the state valuations. - * All variables need to be added before adding new states. - */ - void addVariable(storm::expressions::Variable const& variable); - - void addObservationLabel(std::string const& label); - - /*! - * Adds a new state. - * The variable values have to be given in the same order as the variables have been added. - * The number of given variable values for each type needs to match the number of added variables. - * After calling this method, no more variables should be added. - */ - void addState(storm::storage::sparse::state_type const& state, std::vector&& booleanValues = {}, std::vector&& integerValues = {}); - - /*! - * Adds a new state including rational values. - * The variable values have to be given in the same order as the variables have been added. - * The number of given variable values for each type needs to match the number of added variables. - * After calling this method, no more variables should be added. - * @note there are two versions of this to allow forward declaration of RationalNumber - */ - void addState(storm::storage::sparse::state_type const& state, std::vector&& booleanValues, std::vector&& integerValues, - std::vector&& rationalValues, std::vector&& observationLabelValues = {}); - - /*! - * Creates the finalized state valuations object. - */ - StateValuations build(); - - uint64_t getBooleanVarCount() const; - uint64_t getIntegerVarCount() const; - uint64_t getLabelCount() const; - - private: - StateValuations currentStateValuations; - uint64_t booleanVarCount; - uint64_t integerVarCount; - uint64_t rationalVarCount; - uint64_t labelCount; -}; -} // namespace sparse -} // namespace storage -} // namespace storm diff --git a/src/storm/storage/sparse/ValuationTransformer.cpp b/src/storm/storage/sparse/ValuationTransformer.cpp new file mode 100644 index 0000000000..54de9b09f4 --- /dev/null +++ b/src/storm/storage/sparse/ValuationTransformer.cpp @@ -0,0 +1,82 @@ +#include "storm/storage/sparse/ValuationTransformer.h" + +#include "storm/adapters/RationalNumberAdapter.h" +#include "storm/exceptions/InvalidArgumentException.h" +#include "storm/exceptions/NotSupportedException.h" +#include "storm/storage/expressions/ExpressionEvaluator.h" +#include "storm/storage/expressions/ExpressionManager.h" +#include "storm/storage/valuations/ValuationDescriptionBuilder.h" +#include "storm/storage/valuations/ValuationsStorage.h" +#include "storm/utility/constants.h" + +namespace storm::storage::sparse { + +ValuationTransformer::ValuationTransformer(Valuations const& oldValuations) : oldValuations(oldValuations) { + // Intentionally left empty. +} + +void ValuationTransformer::addExpression(storm::expressions::Variable const& var, storm::expressions::Expression const& expr) { + STORM_LOG_THROW(var.getType() == expr.getType(), storm::exceptions::InvalidArgumentException, + "Variable " << var.getName() << " and expression " << expr << " must have the same type."); + STORM_LOG_THROW(var.getManager() == expr.getManager(), storm::exceptions::InvalidArgumentException, + "Variable " << var.getName() << " and expression " << expr << " must have the same manager."); + STORM_LOG_THROW(var.getManager() == oldValuations.getManager(), storm::exceptions::InvalidArgumentException, + "Variable " << var.getName() << " and old state valuations must have the same manager."); + STORM_LOG_THROW(var.hasBooleanType() || var.hasIntegerType() || var.hasRationalType(), storm::exceptions::InvalidArgumentException, + "Unsupported variable type " << var.getType() << " for variable " << var.getName() << "."); + variables.push_back(var); + expressions.push_back(expr); +} + +Valuations ValuationTransformer::build(bool extend) { + STORM_LOG_THROW(oldValuations.getStorage().numClasses() == 1, storm::exceptions::NotSupportedException, + "Valuation transformation is only supported for valuations with a single class."); + ValuationsStorage result = [&]() { + ValuationDescriptionBuilder descriptionBuilder(oldValuations.getManager().shared_from_this()); + if (extend) { + descriptionBuilder.addVariables(oldValuations.getStorage().getClassDescription()); + } + for (auto const& v : variables) { + if (v.hasBooleanType()) { + descriptionBuilder.addBooleanVariable(v); + } else if (v.hasIntegerType()) { + descriptionBuilder.addIntegerVariable(v, std::numeric_limits::min(), std::numeric_limits::max()); + } else if (v.hasRationalType()) { + descriptionBuilder.addRationalVariable(v, 128); + } else { + STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, + "Variable " << v.getName() << " has unsupported type " << v.getType() << "."); + } + } + return ValuationsStorage(descriptionBuilder.buildClassDescription(), oldValuations.getManager().shared_from_this()); + }(); + result.resize(oldValuations.getNumberOfEntities()); + + storm::expressions::ExpressionEvaluator evaluator(oldValuations.getManager()); + for (uint64_t entity = 0; entity < oldValuations.getNumberOfEntities(); ++entity) { + if (extend) { + // If requested, we copy variables into the new valuations + oldValuations.getStorage().readCallback(entity, [&result](auto const e, auto const& var, auto const& value) { result.writeValue(e, var, value); }); + } + + // Setup the expression evaluator + oldValuations.setValuesInEvaluator(entity, evaluator); + // Evaluate expressions and write results into the new valuations + for (uint64_t i = 0; i < variables.size(); ++i) { + auto const& var = variables[i]; + auto const& expr = expressions[i]; + if (var.hasBooleanType()) { + result.writeValue(entity, var, evaluator.asBool(expr)); + } else if (var.hasIntegerType()) { + result.writeValue(entity, var, evaluator.asInt(expr)); + } else if (var.hasRationalType()) { + result.writeValue(entity, var, evaluator.asRational(expr)); + } else { + STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, + "Variable " << var.getName() << " has unsupported type " << var.getType() << "."); + } + } + } + return Valuations(std::move(result)); +} +} // namespace storm::storage::sparse \ No newline at end of file diff --git a/src/storm/storage/sparse/ValuationTransformer.h b/src/storm/storage/sparse/ValuationTransformer.h new file mode 100644 index 0000000000..76044fea8a --- /dev/null +++ b/src/storm/storage/sparse/ValuationTransformer.h @@ -0,0 +1,37 @@ +#pragma once +#include "storm/storage/expressions/Expression.h" +#include "storm/storage/valuations/Valuations.h" + +namespace storm::storage::sparse { + +/*! + * Transforms the given state valuations to a new state valuations over a new variable set. + * The values of the new variables are determined by evaluating the provided expressions w.r.t. the old variable valuation. + * The freshly introduced variables may either replace or extend the existing variable set. + */ +class ValuationTransformer { + public: + ValuationTransformer(Valuations const& oldValuations); + + /*! + * Add a variable defined by the given expression. + * Note that these should all be over the same expression manager and both should have the same type. + * @param var A variable + * @param expr An expression + */ + void addExpression(storm::expressions::Variable const& var, storm::expressions::Expression const& expr); + + /*! + * Build and export the state valuations. Should be called only once. + * @param extend Whether to maintain also the existing variables. + * @return + */ + Valuations build(bool extend); + + private: + Valuations const& oldValuations; + std::vector variables; + std::vector expressions; +}; + +} // namespace storm::storage::sparse \ No newline at end of file diff --git a/src/storm/storage/umb/Umb.h b/src/storm/storage/umb/Umb.h index cab662d678..6afa75754e 100644 --- a/src/storm/storage/umb/Umb.h +++ b/src/storm/storage/umb/Umb.h @@ -14,6 +14,11 @@ enum class ModelType; class ModelBase; } // namespace models +/*! + * Import and export of umb files. + * @see https://pmc-tools.github.io/umb/spec + * @see https://arxiv.org/abs/2606.17811 + */ namespace umb { template diff --git a/src/storm/storage/umb/export/SparseModelToUmb.cpp b/src/storm/storage/umb/export/SparseModelToUmb.cpp index 12dd54923c..59b64d5f63 100644 --- a/src/storm/storage/umb/export/SparseModelToUmb.cpp +++ b/src/storm/storage/umb/export/SparseModelToUmb.cpp @@ -15,6 +15,7 @@ #include "storm/models/sparse/Pomdp.h" #include "storm/models/sparse/Smg.h" #include "storm/storage/sparse/ChoiceOrigins.h" +#include "storm/storage/valuations/ValuationsStorage.h" #include "storm/transformer/MakePOMDPCanonic.h" #include "storm/utility/macros.h" #include "storm/utility/vector.h" @@ -385,6 +386,31 @@ void setIndexInformation(storm::models::sparse::Model const& model, s apIndex.appliesTo.push_back(storm::umb::ModelIndex::Annotation::AppliesTo::States); } } + + // valuations: + auto createDescription = [](storm::storage::sparse::ValuationsStorage const& valuations) { + storm::storage::sparse::ValuationDescription descr; + for (uint64_t classIndex = 0; classIndex < valuations.numClasses(); ++classIndex) { + descr.classes.push_back(valuations.getClassDescription(classIndex)); + } + if (valuations.hasStrings()) { + descr.numStrings = valuations.numStrings(); + } + return descr; + }; + if (model.hasStateValuations()) { + index.valuations.emplace().states = createDescription(model.getStateValuations().getStorage()); + } + if (model.isPartiallyObservable()) { + STORM_LOG_ASSERT(model.isOfType(storm::models::ModelType::Pomdp), "Only POMDPs are supported as partially observable models."); + auto pomdp = model.template as>(); + if (pomdp->hasObservationValuations()) { + if (!index.valuations.has_value()) { + index.valuations.emplace(); + } + index.valuations->observations = createDescription(pomdp->getObservationValuations().getStorage()); + } + } } template @@ -421,9 +447,16 @@ void sparseModelToUmb(storm::models::sparse::Model const& model, UmbM umbModel.index.transitionSystem.numChoiceActions = numActions; } - // State valuations + // Valuations if (model.hasStateValuations()) { - STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "State valuations are not yet supported for UMB export."); + umbModel.valuations.states = model.getStateValuations().getStorage().getRawUmbData(); + } + if (model.isPartiallyObservable()) { + STORM_LOG_ASSERT(model.isOfType(storm::models::ModelType::Pomdp), "Only POMDPs are supported as partially observable models."); + auto pomdp = model.template as>(); + if (pomdp->hasObservationValuations()) { + umbModel.valuations.observations = pomdp->getObservationValuations().getStorage().getRawUmbData(); + } } // Transition matrix diff --git a/src/storm/storage/umb/import/ImportOptions.h b/src/storm/storage/umb/import/ImportOptions.h index a5e110ed61..eaaa2d0bb3 100644 --- a/src/storm/storage/umb/import/ImportOptions.h +++ b/src/storm/storage/umb/import/ImportOptions.h @@ -22,5 +22,11 @@ struct ImportOptions { * State valuations will only be built if this is set to true *and* the umb model contains appropriate information. */ bool buildStateValuations{true}; + + /*! + * Controls building of observation valuations. + * Observation valuations will only be built if this is set to true *and* the umb model contains appropriate information. + */ + bool buildObservationValuations{true}; }; } // namespace storm::umb diff --git a/src/storm/storage/umb/import/SparseModelFromUmb.cpp b/src/storm/storage/umb/import/SparseModelFromUmb.cpp index 8f2152c9e8..1a14c89238 100644 --- a/src/storm/storage/umb/import/SparseModelFromUmb.cpp +++ b/src/storm/storage/umb/import/SparseModelFromUmb.cpp @@ -4,7 +4,7 @@ #include #include "storm/storage/umb/model/UmbModel.h" -#include "storm/storage/umb/model/Valuations.h" +#include "storm/storage/valuations/ValuationsStorage.h" #include "storm/models/ModelType.h" #include "storm/storage/BitVector.h" @@ -252,15 +252,24 @@ std::shared_ptr> constructSparseModel(st auto transitionMatrix = constructTransitionMatrix(umbModel); storm::storage::sparse::ModelComponents components(std::move(transitionMatrix), std::move(stateLabelling), constructRewardModels(umbModel)); + // choice labeling if (options.buildChoiceLabeling && umbModel.index.transitionSystem.numChoiceActions > 0) { STORM_LOG_THROW(umbModel.choiceActions.has_value() && umbModel.choiceActions->values.has_value(), storm::exceptions::WrongFormatException, "Choice actions mentioned in the index but no files given."); components.choiceLabeling = constructChoiceLabeling(umbModel); } + // state valuations if (options.buildStateValuations && umbModel.index.valuations.has_value() && umbModel.index.valuations->states.has_value()) { STORM_LOG_THROW(umbModel.valuations.states.has_value() && umbModel.valuations.states->valuations.has_value(), storm::exceptions::WrongFormatException, "State valuations mentioned in the index but no files given."); - STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "State valuations for UMB models are not yet supported."); + auto const& svIndex = umbModel.index.valuations->states.value(); + auto const& svData = umbModel.valuations.states.value(); + STORM_LOG_ASSERT(svIndex.numStrings.has_value() == svData.stringMapping.has_value() && svIndex.numStrings.has_value() == svData.strings.has_value(), + "String mapping and strings must be given iff there are #strings mentioned in index."); + storm::storage::sparse::ValuationsStorage val(umbModel.index.transitionSystem.numStates, svIndex.classes, svData.valuations.value(), + svData.stringMapping.value_or(std::vector()), svData.strings.value_or(std::vector()), + svData.valuationToClass); + components.stateValuations.emplace(std::move(val)); } else { STORM_LOG_WARN_COND(!options.buildStateValuations, "State valuations requested but the UMB model does not have any."); } @@ -288,6 +297,21 @@ std::shared_ptr> constructSparseModel(st STORM_LOG_THROW(umbModel.stateObservations.has_value(), storm::exceptions::WrongFormatException, "State observations are required for POMDP models but not present in the UMB model."); components.observabilityClasses.emplace(umbModel.stateObservations->values->begin(), umbModel.stateObservations->values->end()); + // observation valuations + if (options.buildObservationValuations && umbModel.index.valuations.has_value() && umbModel.index.valuations->observations.has_value()) { + STORM_LOG_THROW(umbModel.valuations.observations.has_value() && umbModel.valuations.observations->valuations.has_value(), + storm::exceptions::WrongFormatException, "Observation valuations mentioned in the index but no files given."); + auto const& ovIndex = umbModel.index.valuations->observations.value(); + auto const& ovData = umbModel.valuations.observations.value(); + STORM_LOG_ASSERT(ovIndex.numStrings.has_value() == ovData.stringMapping.has_value() && ovIndex.numStrings.has_value() == ovData.strings.has_value(), + "String mapping and strings must be given iff there are #strings mentioned in index."); + storm::storage::sparse::ValuationsStorage val(umbModel.index.transitionSystem.numObservations, ovIndex.classes, ovData.valuations.value(), + ovData.stringMapping.value_or(std::vector()), ovData.strings.value_or(std::vector()), + ovData.valuationToClass); + components.observationValuations.emplace(std::move(val)); + } else { + STORM_LOG_WARN_COND(!options.buildStateValuations, "State valuations requested but the UMB model does not have any."); + } } else if (modelType == Smg) { if (umbModel.stateToPlayer.has_value()) { auto const& stateToPlayer = umbModel.stateToPlayer.value(); diff --git a/src/storm/storage/umb/model/ModelIndex.h b/src/storm/storage/umb/model/ModelIndex.h index 064201b54d..5de1e1de86 100644 --- a/src/storm/storage/umb/model/ModelIndex.h +++ b/src/storm/storage/umb/model/ModelIndex.h @@ -7,7 +7,7 @@ #include "storm/adapters/JsonAdapter.h" #include "storm/adapters/JsonSerializationAdapter.h" #include "storm/storage/umb/model/Type.h" -#include "storm/storage/umb/model/ValuationDescription.h" +#include "storm/storage/valuations/ValuationDescription.h" #include "storm/utility/OptionalRef.h" namespace storm::umb { @@ -109,7 +109,7 @@ struct ModelIndex { std::optional> annotations; struct Valuations { - std::optional states, choices, branches, observations, players; + std::optional states, choices, branches, observations, players; auto static constexpr JsonKeys = {"states", "choices", "branches", "observations", "players"}; using JsonSerialization = storm::JsonSerialization; }; diff --git a/src/storm/storage/umb/model/StringEncoding.h b/src/storm/storage/umb/model/StringEncoding.h index 65d7a423e5..46c849bdb0 100644 --- a/src/storm/storage/umb/model/StringEncoding.h +++ b/src/storm/storage/umb/model/StringEncoding.h @@ -7,15 +7,22 @@ namespace storm::umb { +auto inline stringVectorView(SEQ::value_type const& strings, CSR::value_type const& stringMapping) { + STORM_LOG_ASSERT(stringMapping.size() > 0, "stringMapping CSR must not be empty."); + auto const numEntries = stringMapping.size() - 1; + return std::ranges::iota_view(0ull, numEntries) | std::ranges::views::transform([&strings, &stringMapping](auto i) -> std::string_view { + return std::string_view(strings.data() + stringMapping[i], stringMapping[i + 1] - stringMapping[i]); + }); +} + auto inline stringVectorView(SEQ const& strings, CSR const& stringMapping) { STORM_LOG_ASSERT(!stringMapping.has_value() || std::ranges::size(stringMapping.value()) > 0, "stringMapping CSR must not be empty."); STORM_LOG_ASSERT(stringMapping.has_value() == strings.has_value(), "stringMapping must be present iff strings is present."); auto const numEntries = stringMapping.has_value() ? std::ranges::size(stringMapping.value()) - 1 : 0; - return std::ranges::iota_view(0ull, numEntries) | - std::ranges::views::transform([stringPtr = strings.has_value() ? strings.value().data() : nullptr, &stringMapping](auto i) -> std::string_view { + return std::ranges::iota_view(0ull, numEntries) | std::ranges::views::transform([&strings, &stringMapping](auto i) -> std::string_view { // Note: this is only executed if numEntries is positive, i.e., if there actually are strings - STORM_LOG_ASSERT(stringPtr != nullptr, "Expected strings to be present if there are entries in the string mapping."); - return std::string_view(stringPtr + stringMapping.value()[i], stringMapping.value()[i + 1] - stringMapping.value()[i]); + STORM_LOG_ASSERT(strings.has_value(), "Expected strings to be present if there are entries in the string mapping."); + return std::string_view(strings->data() + stringMapping.value()[i], stringMapping.value()[i + 1] - stringMapping.value()[i]); }); } diff --git a/src/storm/storage/umb/model/Validation.cpp b/src/storm/storage/umb/model/Validation.cpp index 0e2d27f4db..f15b9af447 100644 --- a/src/storm/storage/umb/model/Validation.cpp +++ b/src/storm/storage/umb/model/Validation.cpp @@ -201,8 +201,8 @@ bool validate(storm::umb::UmbModel const& umbModel, std::ostream& err) { } for (auto const& descr : description->classes) { for (auto const& var : descr.variables) { - if (std::holds_alternative(var)) { - auto const& variable = std::get(var); + if (std::holds_alternative(var)) { + auto const& variable = std::get(var); if (variable.name.empty()) { err << "A valuation description has a variable with an empty name.\n"; isValid = false; @@ -496,7 +496,7 @@ bool validate(storm::umb::UmbModel const& umbModel, std::ostream& err) { // Valuations auto validateValuation = [&isValid, &err](storm::umb::UmbModel::Valuation const& v, auto const& entityName, uint64_t const numEntity, - storm::umb::ValuationDescription const& descr) { + storm::storage::sparse::ValuationDescription const& descr) { auto const context = std::string("valuations/") + entityName; if (v.valuationToClass.has_value() && v.valuationToClass->size() != numEntity) { err << context << "/valuation-to-class has invalid size: " << v.valuationToClass->size() << " != #" << entityName << "=" << numEntity << ".\n"; diff --git a/src/storm/storage/umb/model/Valuations.h b/src/storm/storage/umb/model/Valuations.h deleted file mode 100644 index 32ba95a82c..0000000000 --- a/src/storm/storage/umb/model/Valuations.h +++ /dev/null @@ -1,422 +0,0 @@ -#pragma once - -#include -#include -#include -#include -#include -#include -#include -#include - -#include "storm/storage/expressions/ExpressionManager.h" -#include "storm/storage/expressions/Variable.h" -#include "storm/storage/umb/model/StringEncoding.h" -#include "storm/storage/umb/model/ValuationDescription.h" -#include "storm/storage/umb/model/ValueEncoding.h" -#include "storm/utility/bitoperations.h" - -#include "storm/exceptions/NotSupportedException.h" -#include "storm/exceptions/UnexpectedException.h" - -namespace storm::umb { - -class Valuations { - public: - Valuations(std::vector const& descriptions, std::vector valuations, std::vector stringMapping, - std::vector strings, std::optional> classes = {}, - std::vector> expressionManagers = {}) - : valuations(std::move(valuations)), stringMapping(std::move(stringMapping)), strings(std::move(strings)) { - if (expressionManagers.empty()) { - expressionManagers.emplace_back(std::make_shared()); - } - STORM_LOG_ASSERT(descriptions.size() == expressionManagers.size() || expressionManagers.size() == 1, - "Mismatch between number of descriptions and expression managers."); - for (uint64_t i = 0; i < descriptions.size(); ++i) { - // We either have a separate manager for each class or all classes share the same manager. - // In the latter case, variable (names,types) pairs need to be unique among all possible classes - auto& manager = expressionManagers.size() == 1 ? *expressionManagers.front() : *expressionManagers[i]; - variableClasses.push_back(createVariablesInformation(manager, descriptions[i])); - } - if (classes.has_value()) { - STORM_LOG_ASSERT(classes->size() == descriptions.size(), "Mismatch between number of descriptions and class mapping."); - uniqueSizeInBytes = std::numeric_limits::max(); // not unique - this->classes = {std::move(*classes), std::vector{1, 0}}; - std::vector classSizesInBytes; - for (auto const& descr : descriptions) { - classSizesInBytes.push_back(descr.sizeInBits() / 8); - } - uint64_t pos = 0; - this->classes->toValuationsMapping.reserve(this->classes->toClassMapping.size() + 1); - for (uint64_t entity = 0; entity < this->classes->toClassMapping.size(); ++entity) { - pos += classSizesInBytes[this->classes->toClassMapping[entity]]; - this->classes->toValuationsMapping.push_back(pos); - } - STORM_LOG_ASSERT(valuations.size() == pos, "Valuation data size does not match class mapping."); - } else { - STORM_LOG_ASSERT(descriptions.size() == 1, "Valuation descriptions must be unique if no class mapping is given."); - uniqueSizeInBytes = descriptions.front().sizeInBits() / 8; - STORM_LOG_ASSERT(valuations.size() % uniqueSizeInBytes == 0, "Valuation data size is not a multiple of the unique valuation size."); - } - } - - Valuations(std::vector descriptions, std::vector valuations, std::optional> classes = {}, - std::vector> expressionManagers = {}) - : Valuations(std::move(descriptions), std::move(valuations), {}, {}, std::move(classes), std::move(expressionManagers)) { - // Intentionally empty - } - - uint64_t size() const { - if (classes) { - return classes->toClassMapping.size(); - } else { - return valuations.size() / uniqueSizeInBytes; - } - } - - uint64_t numStrings() const { - return stringMapping.size() > 0 ? stringMapping.size() - 1 : 0; - } - - void read(uint64_t entity, auto const& callback) const { - for (auto const& varInfo : info(entity).variables) { - read(entity, varInfo, callback); - } - } - - void read(auto const& callback) const { - for (uint64_t entity = 0; entity < size(); ++entity) { - read(entity, callback); - } - } - - private: - using Integer = storm::NumberTraits::IntegerType; - - // Variable information - struct VariableInformation { - storm::expressions::Variable const expressionVariable; - ValuationClassDescription::Variable const description; - uint64_t const bitOffset; // The first bit holding the variable's data within the valuation. - // If the variable is optional, the optional bit is located at bitOffset - 1 - bool const fits64Bit; - }; - struct VariablesInformation { - std::vector variables; - std::shared_ptr expressionManager; - }; - std::vector variableClasses; - - // Classes information - struct ClassData { - std::vector toClassMapping; - std::vector toValuationsMapping; - }; - std::optional classes; // present iff there are multiple classes - uint64_t uniqueSizeInBytes; // if there is only a single class, this is the size of the valuation in bytes. 2^64-1 iff classes are present. - - // Data - std::vector valuations; - std::vector stringMapping; - std::vector strings; - - /*! - * Return true if the variable representation and potential offset addition all fit inside a standard 64 bit number representation - * @return - */ - static bool fits64Bit(ValuationClassDescription::Variable const& varDesc) { - using enum storm::umb::Type; - if (varDesc.type.bitSize() > 64) { - return false; - } - switch (varDesc.type.type) { - case Bool: - return true; - case Uint: { - if (varDesc.offset.value_or(0) == 0) { - return true; - } - // check if adding the (non-zero) offset still fits into 64 bits - uint64_t const maxValue = varDesc.upper.has_value() ? static_cast(varDesc.upper.value()) - : (varDesc.type.bitSize() == 64) ? std::numeric_limits::max() - : (static_cast(1) << varDesc.type.bitSize()) - 1; - // the minValue equals the offset (given as int64_t and therefore always fits into 64 bits - if (varDesc.offset.value() < 0) { - // maxValue + offset = maxValue - (-offset) must fit into output type int64_t - return maxValue - static_cast(-varDesc.offset.value()) <= static_cast(std::numeric_limits::max()); - } else { // positive offset - // maxValue + offset must fit into output type uint64_t - return maxValue <= std::numeric_limits::max() - static_cast(varDesc.offset.value()); - } - } - case Int: { - if (varDesc.offset.value_or(0) == 0) { - return true; - } - // check if adding the (non-zero) offset still fits into 64 bits - int64_t const maxValue = varDesc.upper.value_or(varDesc.type.bitSize() == 64 ? std::numeric_limits::max() - : (static_cast(1) << (varDesc.type.bitSize() - 1)) - 1); - int64_t const minValue = varDesc.lower.value_or(varDesc.type.bitSize() == 64 ? std::numeric_limits::min() - : -(static_cast(1) << (varDesc.type.bitSize() - 1))); - if (varDesc.offset.value() < 0) { - // minValue + offset must fit into output type int64_t - return minValue >= std::numeric_limits::min() - varDesc.offset.value(); - } else { // positive offset - // maxValue + offset must fit into output type int64_t - return maxValue <= std::numeric_limits::max() - varDesc.offset.value(); - } - } - case Double: - return true; // double values are always stored as 64 bit IEEE 754 values - case Rational: - return false; // - case String: - return true; // string indices are always stored as uint64_t - default: - STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, - "Valuations for variable type '" << varDesc.type.toString() << "' are not supported."); - } - } - - static VariablesInformation createVariablesInformation(storm::expressions::ExpressionManager& expressionManager, - ValuationClassDescription const& description) { - VariablesInformation result{.variables = {}, .expressionManager = expressionManager.shared_from_this()}; - uint64_t currentOffset = 0; - for (auto const& varVariant : description.variables) { - if (std::holds_alternative(varVariant)) { - auto const& varDesc = std::get(varVariant); - storm::expressions::Type variableType; - using enum storm::umb::Type; - switch (varDesc.type.type) { - case Bool: - variableType = expressionManager.getBooleanType(); - break; - case Uint: - case Int: - variableType = expressionManager.getIntegerType(); - break; - case Double: - case Rational: - variableType = expressionManager.getRationalType(); - break; - case String: - variableType = expressionManager.getStringType(); - break; - default: - STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, - "Valuations for variable type '" << varDesc.type.toString() << "' are not supported."); - } - if (varDesc.isOptional.value_or(false)) { - ++currentOffset; // optional variables have a preceding presence bit - } - result.variables.emplace_back(VariableInformation{.expressionVariable = expressionManager.declareOrGetVariable(varDesc.name, variableType), - .description = varDesc, - .bitOffset = currentOffset, - .fits64Bit = fits64Bit(varDesc)}); - currentOffset += result.variables.back().description.type.bitSize(); - } else { - auto const& padding = std::get(varVariant); - currentOffset += padding.padding; - } - } - STORM_LOG_ASSERT(currentOffset == description.sizeInBits(), "Computed size does not match description size."); - STORM_LOG_ASSERT(currentOffset % 8 == 0, "Invalid valuation description detected: size in bits must be a multiple of 8."); - return result; - } - - VariablesInformation const& info(uint64_t entity) const { - STORM_LOG_ASSERT(entity < size(), "Entity index out of bounds: " << entity << " >= " << size() << "."); - if (classes) { - return variableClasses[classes->toClassMapping[entity]]; - } else { - return variableClasses.front(); - } - } - - std::span bytes(uint64_t entity) const { - STORM_LOG_ASSERT(entity < size(), "Entity index out of bounds: " << entity << " >= " << size() << "."); - if (classes) { - auto const start = classes->toValuationsMapping[entity]; - auto const end = classes->toValuationsMapping[entity + 1]; - return std::span(&valuations[start], end - start); - } else { - auto const start = entity * uniqueSizeInBytes; - return std::span(&valuations[start], uniqueSizeInBytes); - } - } - - std::span bytes(uint64_t entity) { - if (classes) { - auto const start = classes->toValuationsMapping[entity]; - auto const end = classes->toValuationsMapping[entity + 1]; - return std::span(&valuations[start], end - start); - } else { - auto const start = entity * uniqueSizeInBytes; - return std::span(&valuations[start], uniqueSizeInBytes); - } - } - - uint64_t readUint64(std::span bytes, uint64_t const bitOffset, uint64_t const bitSize) const { - STORM_LOG_ASSERT(bitOffset < bytes.size() * 8, "Variable offset exceeds valuation size."); - STORM_LOG_ASSERT(bitSize <= 64, "Invalid bit range."); - auto const firstByte = bitOffset / 8; - auto const bitOffsetWithinByte = bitOffset % 8; - auto const numBytes = (bitOffsetWithinByte + bitSize + 7) / 8; - STORM_LOG_ASSERT(numBytes <= 9, "Invalid number of bytes computed: " << numBytes); - uint64_t result; - // set the first (up to) 8 bytes - std::memcpy(&result, &bytes[firstByte], std::min(numBytes, 8ull)); - result >>= bitOffsetWithinByte; - // if necessary, set the most significant bits by reading a 9th byte - if (numBytes == 9ull) { - uint64_t upperBits = std::bit_cast(bytes[firstByte + 8]); - upperBits <<= (64 - bitOffsetWithinByte); - result |= upperBits; - } - // Set irrelevant bits to zero - if (bitSize < 64) { - uint64_t const relevantBitMask = (1ull << bitSize) - 1; - result &= relevantBitMask; - } - return result; - } - - template - Integer readInteger(std::span bytes, uint64_t const bitOffset, uint64_t const bitSize) const { - auto const num64BitChunks = (bitSize + 63) / 64; - auto chunksView = - std::ranges::iota_view(0ull, num64BitChunks) | std::ranges::views::transform([this, &bytes, &bitOffset, &bitSize](auto i) -> uint64_t { - return readUint64(bytes, bitOffset + i * 64, std::min(64, bitSize - i * 64)); - }); - Integer result = ValueEncoding::decodeArbitraryPrecisionInteger(chunksView); - if constexpr (Signed) { - // Check if this number is supposed to be negative - if (result >= storm::utility::pow(2, bitSize - 1)) { - return result - storm::utility::pow(2, bitSize); - } - } - return result; - } - - template - void read(uint64_t entity, VariableInformation const& varInfo, auto const& callback) const { - bool constexpr allowAny = (sizeof...(AllowedTypes) == 0); - bool constexpr allowNullopt = allowAny || std::disjunction_v...>; - bool constexpr allowBool = allowAny || std::disjunction_v...>; - bool constexpr allowUint64 = allowAny || std::disjunction_v...>; - bool constexpr allowInt64 = allowAny || std::disjunction_v...>; - bool constexpr allowDouble = allowAny || std::disjunction_v...>; - bool constexpr allowRational = allowAny || std::disjunction_v...>; - bool constexpr allowInteger = allowAny || std::disjunction_v...>; - bool constexpr allowString = allowAny || std::disjunction_v...>; - - if (varInfo.description.isOptional.value_or(false)) { - if constexpr (allowNullopt) { - callback(entity, varInfo.expressionVariable, std::nullopt); - } - } - auto const bitSize = varInfo.description.type.bitSize(); - using enum storm::umb::Type; - if (varInfo.fits64Bit) { - STORM_LOG_ASSERT(bitSize <= 64, "Invalid bit size for 64 bit fast path."); - uint64_t rawContent = readUint64(bytes(entity), varInfo.bitOffset, bitSize); - switch (varInfo.description.type.type) { - case Bool: - if constexpr (allowBool) { - callback(entity, varInfo.expressionVariable, rawContent != 0); - return; - } - case Uint: - if (int64_t offset = varInfo.description.offset.value_or(0); offset < 0) { - // negative offset, output type is int64_t - if constexpr (allowInt64) { - callback(entity, varInfo.expressionVariable, static_cast(rawContent) + offset); - return; - } - } else { - // non-negative offset, output type is uint64_t - uint64_t value = rawContent + offset; - if constexpr (allowUint64) { - callback(entity, varInfo.expressionVariable, value); - return; - } else if constexpr (allowInt64) { - if (value <= static_cast(std::numeric_limits::max())) { - callback(entity, varInfo.expressionVariable, static_cast(value)); - return; - } - } - } - case Int: - if constexpr (allowInt64) { - uint64_t const mostSignificantBitMask = 1ull << (bitSize - 1); - if (rawContent & mostSignificantBitMask) { - // Negative value: Two's complement (e.g. 1111...1101 is -3) - callback(entity, varInfo.expressionVariable, -static_cast(~rawContent & (mostSignificantBitMask - 1)) - 1); - return; - } else { - // Positive value - callback(entity, varInfo.expressionVariable, static_cast(rawContent)); - return; - } - } - case Double: - if constexpr (allowDouble) { - callback(entity, varInfo.expressionVariable, static_cast(std::bit_cast(rawContent))); - return; - } - case Rational: - // Reaching this part should not be possible as varInfo.fits64Bit would be false - STORM_LOG_ASSERT(false, "Handling of rational values in 64 bit fast path is not implemented."); - case String: - if constexpr (allowString) { - callback(entity, varInfo.expressionVariable, stringVectorView(strings, stringMapping)[rawContent]); - return; - } - default: - STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, - "Valuations for variable type '" << varInfo.description.type.toString() << "' are not supported."); - } - } - // reaching this point means that we could not handle the value in the fast path - switch (varInfo.description.type.type) { - case Bool: - if constexpr (allowBool) { - // Bools could be encoded with more than 64 bits (which is not reasonable, but possible..) - callback(entity, varInfo.expressionVariable, readInteger(bytes(entity), varInfo.bitOffset, bitSize) != Integer(0)); - return; - } - case Uint: - case Int: - if constexpr (allowInteger) { - Integer value = varInfo.description.type.type == Int ? readInteger(bytes(entity), varInfo.bitOffset, bitSize) - : readInteger(bytes(entity), varInfo.bitOffset, bitSize); - value += storm::utility::convertNumber(varInfo.description.offset.value_or(0)); - callback(entity, varInfo.expressionVariable, value); - return; - } - case Double: - // Reaching this part should not be possible as varInfo.fits64Bit would be true - STORM_LOG_ASSERT(false, "double variables with more than 64 bits are not compliant."); - case Rational: - if constexpr (allowRational) { - STORM_LOG_ASSERT(bitSize % 2 == 0, "Rational number bit size must be even."); - uint64_t b = bitSize / 2; - storm::RationalNumber numerator = readInteger(bytes(entity), varInfo.bitOffset, b); - storm::RationalNumber denominator = readInteger(bytes(entity), varInfo.bitOffset + b, b); - callback(entity, varInfo.expressionVariable, storm::RationalNumber(numerator / denominator)); - return; - } - case String: { - // Reaching this part should not be possible as varInfo.fits64Bit would be true - STORM_LOG_ASSERT(false, "String variables with more than 64 bits are not compliant."); - } - default: - STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, - "Valuations for variable type '" << varInfo.description.type.toString() << "' are not supported."); - } - - STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, - "Variable " << varInfo.description.name << " of type " << varInfo.description.type.toString() << " is not handled."); - } -}; -} // namespace storm::umb \ No newline at end of file diff --git a/src/storm/storage/umb/model/ValueEncoding.h b/src/storm/storage/umb/model/ValueEncoding.h index 52ea658d1a..7ffabdebc1 100644 --- a/src/storm/storage/umb/model/ValueEncoding.h +++ b/src/storm/storage/umb/model/ValueEncoding.h @@ -127,7 +127,11 @@ class ValueEncoding { template static void appendEncodedInteger(std::vector& result, typename storm::NumberTraits::IntegerType const& value, uint64_t uint64BucketsPerInteger) { - if constexpr (Signed) { + using IntegerType = typename storm::NumberTraits::IntegerType; + if (uint64BucketsPerInteger == 0) { + STORM_LOG_ASSERT(value == storm::utility::zero(), "Unexpected non-zero value for zero bucket size."); + // nothing to do + } else if constexpr (Signed) { if (value < 0) { // Two's complement representation (e.g. -3 is 1111...1101) // We encode the corresponding positive value and then invert the bits. @@ -144,7 +148,6 @@ class ValueEncoding { "Encoding error for positive signed integer: most significant bit is set. Not enough uint64 buckets allocated?"); } } else { - using IntegerType = typename storm::NumberTraits::IntegerType; auto const twoTo64 = storm::utility::pow(2, 64); // We assume a little endian representation, so we start with the least significant bits. @@ -158,6 +161,9 @@ class ValueEncoding { ++buckets; } // fill remaining buckets with zeros + STORM_LOG_ASSERT(uint64BucketsPerInteger >= buckets, "Not enough uint64 buckets allocated for encoding integer value " + << value << " (" << uint64BucketsPerInteger << " buckets allocated but " << buckets + << " needed)."); result.resize(result.size() + (uint64BucketsPerInteger - buckets), 0ull); } } diff --git a/src/storm/storage/umb/model/ValuationDescription.cpp b/src/storm/storage/valuations/ValuationDescription.cpp similarity index 53% rename from src/storm/storage/umb/model/ValuationDescription.cpp rename to src/storm/storage/valuations/ValuationDescription.cpp index 5ba5490d6c..f9e4195818 100644 --- a/src/storm/storage/umb/model/ValuationDescription.cpp +++ b/src/storm/storage/valuations/ValuationDescription.cpp @@ -1,6 +1,6 @@ -#include "storm/storage/umb/model/ValuationDescription.h" +#include "storm/storage/valuations/ValuationDescription.h" -namespace storm::umb { +namespace storm::storage::sparse { uint64_t ValuationClassDescription::sizeInBits() const { uint64_t totalSize = 0; for (auto const& variable : variables) { @@ -17,4 +17,16 @@ uint64_t ValuationClassDescription::sizeInBits() const { return totalSize; } -} // namespace storm::umb +bool ValuationClassDescription::hasStringVariable() const { + for (auto const& variable : variables) { + if (std::holds_alternative(variable)) { + auto const& var = std::get(variable); + if (isStringType(var.type.type)) { + return true; + } + } + } + return false; +} + +} // namespace storm::storage::sparse diff --git a/src/storm/storage/umb/model/ValuationDescription.h b/src/storm/storage/valuations/ValuationDescription.h similarity index 58% rename from src/storm/storage/umb/model/ValuationDescription.h rename to src/storm/storage/valuations/ValuationDescription.h index e051fa9de7..957d973656 100644 --- a/src/storm/storage/umb/model/ValuationDescription.h +++ b/src/storm/storage/valuations/ValuationDescription.h @@ -8,7 +8,14 @@ #include "storm/adapters/JsonSerializationAdapter.h" #include "storm/storage/umb/model/Type.h" -namespace storm::umb { +namespace storm::storage::sparse { +/*! + * Describes the layout of a class of valuations (e.g. the variables of a state class) as specified by the + * UMB (Unified Markov Binary) format. The structure and JSON keys of this type must stay compliant with + * the UMB specification, since it is (de-)serialized directly to/from the "classes" entry of a UMB index file. + * @see https://pmc-tools.github.io/umb/spec + * @see https://arxiv.org/abs/2606.17811 + */ struct ValuationClassDescription { struct Padding { uint64_t padding{0}; @@ -18,7 +25,7 @@ struct ValuationClassDescription { struct Variable { std::string name; std::optional isOptional; - SizedType type; + storm::umb::SizedType type; std::optional lower, upper, offset; static auto constexpr JsonKeys = {"name", "is-optional", "type", "lower", "upper", "offset"}; using JsonSerialization = storm::JsonSerialization; @@ -32,8 +39,18 @@ struct ValuationClassDescription { * The size is the sum of all padding and size values plus 1 for each variable where isOptional is true. */ uint64_t sizeInBits() const; + + /*! + * @return true iff there is at least one variable of type String in this class description. + */ + bool hasStringVariable() const; }; +/*! + * Describes all valuation classes for a set of entities (e.g. states / observations) as specified by the + * UMB format. The structure and JSON keys of this type must stay compliant with + * the UMB specification, since it is (de-)serialized directly to/from a UMB index file. + */ struct ValuationDescription { bool unique{false}; std::optional numStrings; @@ -41,4 +58,4 @@ struct ValuationDescription { static auto constexpr JsonKeys = {"unique", "#strings", "classes"}; using JsonSerialization = storm::JsonSerialization; }; -} // namespace storm::umb +} // namespace storm::storage::sparse diff --git a/src/storm/storage/valuations/ValuationDescriptionBuilder.cpp b/src/storm/storage/valuations/ValuationDescriptionBuilder.cpp new file mode 100644 index 0000000000..e2d0008e93 --- /dev/null +++ b/src/storm/storage/valuations/ValuationDescriptionBuilder.cpp @@ -0,0 +1,115 @@ +#include "storm/storage/valuations/ValuationDescriptionBuilder.h" + +#include +#include "storm/storage/expressions/ExpressionManager.h" +#include "storm/storage/expressions/Variable.h" +#include "storm/storage/valuations/ValuationsStorage.h" +#include "storm/utility/macros.h" + +namespace storm::storage::sparse { + +ValuationDescriptionBuilder::ValuationDescriptionBuilder(std::shared_ptr const& expressionManager) + : manager(expressionManager) { + STORM_LOG_ASSERT(this->manager != nullptr, "Initilization with empty expression manager is not allowed."); +} + +storm::expressions::ExpressionManager const& ValuationDescriptionBuilder::getManager() const { + return *manager; +} + +void ValuationDescriptionBuilder::addBooleanVariable(storm::expressions::Variable const& variable, bool optional) { + STORM_LOG_ASSERT(*manager == variable.getManager(), "Variable " << variable.getName() << " has a different manager than previously specified."); + descr.variables.emplace_back(ValuationClassDescription::Variable{.name{variable.getName()}, + .isOptional{optional ? std::optional(true) : std::nullopt}, + .type{.type = storm::umb::Type::Bool, .size = 1}, + .lower{}, + .upper{}, + .offset{}}); +} + +void ValuationDescriptionBuilder::addIntegerVariable(storm::expressions::Variable const& variable, int64_t const lowerBound, int64_t const upperBound, + bool optional) { + STORM_LOG_ASSERT(*manager == variable.getManager(), "Variable " << variable.getName() << " has a different manager than previously specified."); + STORM_LOG_ASSERT(lowerBound <= upperBound, "Lower bound " << lowerBound << " must not be above upper bound" << upperBound << "."); + // Cast to uint64_t *before* subtracting to avoid signed overflow UB. + uint64_t const bitSize = storm::utility::bitsize(static_cast(upperBound) - static_cast(lowerBound)); + storm::umb::SizedType const t{.type{storm::umb::Type::Uint}, .size{std::max(1, bitSize)}}; + descr.variables.emplace_back(ValuationClassDescription::Variable{.name{variable.getName()}, + .isOptional{optional ? std::optional(true) : std::nullopt}, + .type{t}, + .lower{lowerBound}, + .upper{upperBound}, + .offset{lowerBound}}); +} + +void ValuationDescriptionBuilder::addIntegerVariable(storm::expressions::Variable const& variable, Integer const lowerBound, Integer const upperBound, + bool optional) { + STORM_LOG_ASSERT(*manager == variable.getManager(), "Variable " << variable.getName() << " has a different manager than previously specified."); + STORM_LOG_ASSERT(lowerBound <= upperBound, "Lower bound " << lowerBound << " must not be above upper bound" << upperBound << "."); + if (lowerBound >= storm::utility::convertNumber(std::numeric_limits::min()) && + upperBound <= storm::utility::convertNumber(std::numeric_limits::max())) { + // If the values fit into int64_t, we use that. + addIntegerVariable(variable, storm::utility::convertNumber(lowerBound), storm::utility::convertNumber(upperBound)); + } else { + uint64_t const bitSize = storm::utility::bitsize(upperBound - lowerBound); + storm::umb::SizedType const t{.type{lowerBound < 0 ? storm::umb::Type::Int : storm::umb::Type::Uint}, .size{std::max(1, bitSize)}}; + descr.variables.emplace_back(ValuationClassDescription::Variable{ + .name{variable.getName()}, .isOptional{optional ? std::optional(true) : std::nullopt}, .type{t}, .lower{}, .upper{}, .offset{}}); + } +} + +void ValuationDescriptionBuilder::addDoubleVariable(storm::expressions::Variable const& variable, bool optional) { + STORM_LOG_ASSERT(*manager == variable.getManager(), "Variable " << variable.getName() << " has a different manager than previously specified."); + descr.variables.emplace_back(ValuationClassDescription::Variable{.name{variable.getName()}, + .isOptional{optional ? std::optional(true) : std::nullopt}, + .type{storm::umb::Type::Double, std::nullopt}, + .lower{}, + .upper{}, + .offset{}}); +} + +void ValuationDescriptionBuilder::addRationalVariable(storm::expressions::Variable const& variable, uint64_t bitSize, bool optional) { + STORM_LOG_ASSERT(*manager == variable.getManager(), "Variable " << variable.getName() << " has a different manager than previously specified."); + STORM_LOG_ASSERT(bitSize % 2 == 0, "Bit size for rational variables must be a multiple of 2."); + storm::umb::SizedType const t{.type{storm::umb::Type::Rational}, .size{std::max(2, bitSize)}}; + descr.variables.emplace_back(ValuationClassDescription::Variable{ + .name{variable.getName()}, .isOptional{optional ? std::optional(true) : std::nullopt}, .type{t}, .lower{}, .upper{}, .offset{}}); +} + +void ValuationDescriptionBuilder::addStringVariable(storm::expressions::Variable const& variable, bool optional) { + STORM_LOG_ASSERT(*manager == variable.getManager(), "Variable " << variable.getName() << " has a different manager than previously specified."); + descr.variables.emplace_back(ValuationClassDescription::Variable{.name{variable.getName()}, + .isOptional{optional ? std::optional(true) : std::nullopt}, + .type{storm::umb::Type::String, std::nullopt}, + .lower{}, + .upper{}, + .offset{}}); +} + +void ValuationDescriptionBuilder::addVariable(ValuationClassDescription::Variable const& variable) { + STORM_LOG_ASSERT(manager->hasVariable(variable.name), "Variable " << variable.name << " is not declared in the expression manager."); + descr.variables.push_back(variable); +} +void ValuationDescriptionBuilder::addVariables(ValuationClassDescription const& description, bool addPadding) { + for (auto const& varVariant : description.variables) { + if (std::holds_alternative(varVariant)) { + addVariable(std::get(varVariant)); + } else if (addPadding && std::holds_alternative(varVariant)) { + descr.variables.push_back(varVariant); + } + } +} + +void ValuationDescriptionBuilder::finalize() { + if (uint64_t const padding = descr.sizeInBits() % 8; padding > 0) { + descr.variables.emplace_back(ValuationClassDescription::Padding{.padding = 8 - padding}); + } +} + +ValuationClassDescription ValuationDescriptionBuilder::buildClassDescription() { + STORM_LOG_ASSERT(!descr.variables.empty(), "At least one variable must be added to the valuation description."); + finalize(); + return descr; +} + +} // namespace storm::storage::sparse diff --git a/src/storm/storage/valuations/ValuationDescriptionBuilder.h b/src/storm/storage/valuations/ValuationDescriptionBuilder.h new file mode 100644 index 0000000000..976b25fa10 --- /dev/null +++ b/src/storm/storage/valuations/ValuationDescriptionBuilder.h @@ -0,0 +1,81 @@ +#pragma once + +#include +#include "storm/storage/valuations/ValuationDescription.h" +#include "storm/utility/NumberTraits.h" + +namespace storm { +namespace expressions { +class Variable; +class ExpressionManager; +} // namespace expressions + +namespace storage::sparse { +/*! + * Helper to incrementally build a ValuationClassDescription, i.e. the description of a class of valuations + * as specified by the UMB (Unified Markov Binary) format. The resulting ValuationClassDescription must + * stay compliant with the UMB specification. + * @see https://pmc-tools.github.io/umb/spec + * @see https://arxiv.org/abs/2606.17811 + */ +class ValuationDescriptionBuilder { + public: + using Integer = storm::NumberTraits::IntegerType; + + ValuationDescriptionBuilder(std::shared_ptr const& expressionManager); + + storm::expressions::ExpressionManager const& getManager() const; + + /*! + * Adds a new boolean variable to the builder. + */ + void addBooleanVariable(storm::expressions::Variable const& variable, bool optional = false); + + /*! + * Adds a new integer variable to the builder. + */ + void addIntegerVariable(storm::expressions::Variable const& variable, int64_t const lowerBound, int64_t const upperBound, bool optional = false); + + /*! + * Adds a new integer variable to the builder. + */ + void addIntegerVariable(storm::expressions::Variable const& variable, Integer const lowerBound, Integer const upperBound, bool optional = false); + + /*! + * Adds a new double variable to the builder. + */ + void addDoubleVariable(storm::expressions::Variable const& variable, bool optional = false); + + /*! + * Adds a new rational variable to the builder. + */ + void addRationalVariable(storm::expressions::Variable const& variable, uint64_t bitSize, bool optional = false); + + /*! + * Adds a new string variable to the builder. + */ + void addStringVariable(storm::expressions::Variable const& variable, bool optional = false); + + /*! + * Adds the given variable. + */ + void addVariable(ValuationClassDescription::Variable const& variable); + + /*! Adds all variables from the given description. + * If addPadding is true, padding entries in the description are added, otherwise they are ignored. + */ + void addVariables(ValuationClassDescription const& description, bool addPadding = false); + + /*! + * Creates the finalized state valuations object. + */ + ValuationClassDescription buildClassDescription(); + + private: + void finalize(); + std::shared_ptr const manager; + ValuationClassDescription descr; +}; + +} // namespace storage::sparse +} // namespace storm diff --git a/src/storm/storage/valuations/Valuations.cpp b/src/storm/storage/valuations/Valuations.cpp new file mode 100644 index 0000000000..645862bc87 --- /dev/null +++ b/src/storm/storage/valuations/Valuations.cpp @@ -0,0 +1,281 @@ +#include "storm/storage/valuations/Valuations.h" + +#include + +#include "storm/adapters/JsonAdapter.h" +#include "storm/adapters/RationalNumberAdapter.h" +#include "storm/storage/expressions/ExpressionEvaluator.h" +#include "storm/storage/valuations/ValuationsStorage.h" + +namespace storm::storage::sparse { + +Valuations::Valuations(ValuationClassDescription const umbValuationDescription, std::shared_ptr const& manager, + uint64_t const numEntities) + : umbValuations(std::make_unique(umbValuationDescription, manager)) { + umbValuations->resize(numEntities); +} + +Valuations::Valuations(ValuationsStorage&& umbValuations) : umbValuations(std::make_unique(std::move(umbValuations))) { + // Intentionally empty +} + +// The type ValuationsStorage is incomplete (forward declared) in the header file and complete in this cpp file. +// The member variable Valuations::umbValuations is of type std::unique_ptr. +// To re-assign or destruct umbValuations, the type ValuationsStorage must be complete (because ValuationsStorage::~ValuationsStorage must be invoked). +// We therefore must define the following destructors / constructors / assignment operators in the .cpp file, not the header file. +Valuations::~Valuations() = default; +Valuations::Valuations(Valuations&& other) = default; +Valuations& Valuations::operator=(Valuations&& other) = default; + +Valuations::Valuations(Valuations const& other) { + if (other.umbValuations) { + // Create a deep copy + umbValuations = std::make_unique(*other.umbValuations); + } +} + +Valuations& Valuations::operator=(Valuations const& other) { + if (this != &other) { + if (other.umbValuations) { + // Create a deep copy + umbValuations = std::make_unique(*other.umbValuations); + } else { + umbValuations.reset(); + } + } + return *this; +} + +storm::expressions::ExpressionManager const& Valuations::getManager() const { + return umbValuations->getManager(); +} + +ValuationsStorage const& Valuations::getStorage() const { + return *umbValuations; +} +ValuationsStorage& Valuations::getStorage() { + return *umbValuations; +} + +uint64_t Valuations::getNumberOfEntities() const { + return umbValuations->size(); +} + +std::set Valuations::getAllVariables() const { + return umbValuations->getAllVariables(); +} + +bool Valuations::entityHasVariable(uint64_t entity, const storm::expressions::Variable& variable) const { + return umbValuations->entityHasVariable(entity, variable); +} + +bool Valuations::getBooleanValue(uint64_t const entity, storm::expressions::Variable const& booleanVariable) const { + return umbValuations->readValue(entity, booleanVariable); +} + +std::optional Valuations::getOptionalBooleanValue(uint64_t const entity, storm::expressions::Variable const& booleanVariable) const { + if (!entityHasVariable(entity, booleanVariable)) { + return std::nullopt; + } + std::optional result; + umbValuations->readCallback(entity, booleanVariable, [&result](auto, auto const&, auto&& value) { + using T = std::remove_cvref_t; + if constexpr (std::is_same_v) { + result = value; + } + // std::nullopt_t means the optional variable's presence bit is unset → result stays std::nullopt + }); + return result; +} + +int64_t Valuations::getInt64Value(uint64_t const entity, storm::expressions::Variable const& integerVariable) const { + return umbValuations->readValue(entity, integerVariable); +} + +std::optional Valuations::getOptionalInt64Value(uint64_t const entity, storm::expressions::Variable const& integerVariable) const { + if (!entityHasVariable(entity, integerVariable)) { + return std::nullopt; + } + std::optional result; + umbValuations->readCallback(entity, integerVariable, [&result](auto, auto const&, auto&& value) { + using T = std::remove_cvref_t; + if constexpr (std::is_same_v) { + result = value; + } + }); + return result; +} + +double Valuations::getDoubleValue(uint64_t const entity, storm::expressions::Variable const& doubleVariable) const { + return umbValuations->readValue(entity, doubleVariable); +} + +std::optional Valuations::getOptionalDoubleValue(uint64_t const entity, storm::expressions::Variable const& doubleVariable) const { + if (!entityHasVariable(entity, doubleVariable)) { + return std::nullopt; + } + std::optional result; + umbValuations->readCallback(entity, doubleVariable, [&result](auto, auto const&, auto&& value) { + using T = std::remove_cvref_t; + if constexpr (std::is_same_v) { + result = value; + } + }); + return result; +} + +storm::RationalNumber Valuations::getRationalValue(uint64_t const entity, storm::expressions::Variable const& rationalVariable) const { + return umbValuations->readValue(entity, rationalVariable); +} + +std::optional Valuations::getOptionalRationalValue(uint64_t const entity, storm::expressions::Variable const& rationalVariable) const { + if (!entityHasVariable(entity, rationalVariable)) { + return std::nullopt; + } + std::optional result; + umbValuations->readCallback(entity, rationalVariable, [&result](auto, auto const&, auto&& value) { + using T = std::remove_cvref_t; + if constexpr (std::is_same_v) { + result = std::move(value); + } + }); + return result; +} + +std::string Valuations::getStringValue(uint64_t const entity, storm::expressions::Variable const& stringVariable) const { + return umbValuations->readValue(entity, stringVariable); +} + +std::optional Valuations::getOptionalStringValue(uint64_t const entity, storm::expressions::Variable const& stringVariable) const { + if (!entityHasVariable(entity, stringVariable)) { + return std::nullopt; + } + std::optional result; + umbValuations->readCallback(entity, stringVariable, [&result](auto, auto const&, auto&& value) { + using T = std::remove_cvref_t; + if constexpr (std::is_same_v) { + result = std::move(value); + } + }); + return result; +} + +template +void Valuations::setValuesInEvaluator(uint64_t entity, storm::expressions::ExpressionEvaluator& evaluator) const { + umbValuations->setValuesInEvaluator(entity, evaluator); +} +template void Valuations::setValuesInEvaluator(uint64_t entity, storm::expressions::ExpressionEvaluator& evaluator) const; +template void Valuations::setValuesInEvaluator(uint64_t entity, storm::expressions::ExpressionEvaluator& evaluator) const; + +storm::storage::BitVector Valuations::getBooleanValues(storm::expressions::Variable const& booleanVariable) const { + STORM_LOG_ASSERT(booleanVariable.hasBooleanType(), "Variable " << booleanVariable.getName() << " is not of boolean type."); + storm::storage::BitVector result(getNumberOfEntities(), false); + umbValuations->readCallback(booleanVariable, [&result](auto const entity, auto, bool value) { + if (value) { + result.set(entity); + } + }); + return result; +} + +std::vector Valuations::getInt64Values(storm::expressions::Variable const& integerVariable) const { + STORM_LOG_ASSERT(integerVariable.hasIntegerType(), "Variable " << integerVariable.getName() << " is not of integer type."); + std::vector result; + result.reserve(getNumberOfEntities()); + umbValuations->readCallback(integerVariable, [&result](auto const entity, auto, int64_t value) { + STORM_LOG_ASSERT(entity == result.size(), "entities processed in unexpected order."); + result.push_back(value); + }); + return result; +} + +std::vector Valuations::getDoubleValues(storm::expressions::Variable const& doubleVariable) const { + STORM_LOG_ASSERT(doubleVariable.hasRationalType(), "Variable " << doubleVariable.getName() << " is not of rational type."); + std::vector result; + result.reserve(getNumberOfEntities()); + umbValuations->readCallback(doubleVariable, [&result](auto const entity, auto, double value) { + STORM_LOG_ASSERT(entity == result.size(), "entities processed in unexpected order."); + result.push_back(value); + }); + return result; +} + +std::vector Valuations::getRationalValues(storm::expressions::Variable const& rationalVariable) const { + STORM_LOG_ASSERT(rationalVariable.hasRationalType(), "Variable " << rationalVariable.getName() << " is not of rational type."); + std::vector result; + result.reserve(getNumberOfEntities()); + umbValuations->readCallback(rationalVariable, [&result](auto const entity, auto, storm::RationalNumber value) { + STORM_LOG_ASSERT(entity == result.size(), "entities processed in unexpected order."); + result.push_back(std::move(value)); + }); + return result; +} + +std::vector Valuations::getStringValues(storm::expressions::Variable const& stringVariable) const { + STORM_LOG_ASSERT(stringVariable.hasStringType(), "Variable " << stringVariable.getName() << " is not of rational type."); + std::vector result; + result.reserve(getNumberOfEntities()); + umbValuations->readCallback(stringVariable, [&result](auto const entity, auto, std::string&& value) { + STORM_LOG_ASSERT(entity == result.size(), "entities processed in unexpected order."); + result.push_back(std::move(value)); + }); + return result; +} + +std::string Valuations::toString(uint64_t const entity, bool const pretty, + std::optional> const& selectedVariables) const { + std::vector assignments; + umbValuations->readCallback(entity, [pretty, &selectedVariables, &assignments](auto, auto const& var, auto&& value) { + if (selectedVariables && !selectedVariables->contains(var)) { + return; + } + using ValueType = std::remove_cvref_t; + if constexpr (std::is_same_v) { + assignments.push_back(pretty ? (var.getName() + "=none") : "none"); + } else if constexpr (std::is_same_v) { + if (pretty) { + assignments.push_back(value ? "" : "!" + var.getName()); + } else { + assignments.push_back(value ? "true" : "false"); + } + } else { + std::stringstream stream; + if (pretty) { + stream << var.getName() << "="; + } + stream << value; + assignments.push_back(stream.str()); + } + }); + return "[" + boost::join(assignments, pretty ? "\t& " : "\t") + "]"; +} + +template +storm::json Valuations::toJson(uint64_t const entity, std::optional> const& selectedVariables) const { + storm::json result; + umbValuations->readCallback(entity, [&selectedVariables, &result](auto, auto const& var, auto&& value) { + if (selectedVariables && !selectedVariables->contains(var)) { + return; + } + result[var.getName()] = value; + }); + return result; +} + +Valuations Valuations::selectEntities(storm::storage::BitVector const& selectedEntities) const { + return Valuations(umbValuations->selectEntities(selectedEntities)); +} + +Valuations Valuations::selectEntities(std::vector const& selectedEntities) const { + return Valuations(umbValuations->selectEntities(selectedEntities)); +} + +std::size_t Valuations::hash() const { + return umbValuations->hash(); +} + +template storm::json Valuations::toJson(uint64_t const, std::optional> const&) const; +template storm::json Valuations::toJson(uint64_t const, + std::optional> const&) const; + +} // namespace storm::storage::sparse diff --git a/src/storm/storage/valuations/Valuations.h b/src/storm/storage/valuations/Valuations.h new file mode 100644 index 0000000000..97bf43641e --- /dev/null +++ b/src/storm/storage/valuations/Valuations.h @@ -0,0 +1,139 @@ +#pragma once + +#include +#include + +#include "storm/adapters/JsonForward.h" +#include "storm/adapters/RationalNumberForward.h" +#include "storm/storage/BitVector.h" +#include "storm/storage/expressions/Variable.h" +#include "storm/utility/NumberTraits.h" + +namespace storm { + +namespace expressions { +template +class ExpressionEvaluator; +} + +namespace storage::sparse { + +struct ValuationClassDescription; +class ValuationsStorage; + +/*! + * Provides access to valuations of variables for a set of entities (e.g. states / observations). + * This class serves as a wrapper around the more low-level storm::storage::sparse::ValuationsStorage class + */ +class Valuations { + public: + Valuations(ValuationClassDescription const valuationClassDescription, std::shared_ptr const& manager = {}, + uint64_t const numEntities = 0); + Valuations(ValuationsStorage&& umbValuations); + Valuations(Valuations const& other); + Valuations(Valuations&& other); + ~Valuations(); + Valuations& operator=(Valuations&& other); + Valuations& operator=(Valuations const& other); + + storm::expressions::ExpressionManager const& getManager() const; + ValuationsStorage const& getStorage() const; + ValuationsStorage& getStorage(); + + /*! + * @return the numer of entities that this object describes + */ + uint64_t getNumberOfEntities() const; + + /*! + * @return the variables that this stores valuations for + */ + std::set getAllVariables() const; + + /*! + * Returns true iff the variable is relevant for the given entity + */ + bool entityHasVariable(uint64_t entity, storm::expressions::Variable const& variable) const; + + // optional variants have no value iff either entityHasVariable(entity, variable) is false or the value is of optional type and not set. + bool getBooleanValue(uint64_t const entity, storm::expressions::Variable const& booleanVariable) const; + std::optional getOptionalBooleanValue(uint64_t const entity, storm::expressions::Variable const& booleanVariable) const; + int64_t getInt64Value(uint64_t const entity, storm::expressions::Variable const& integerVariable) const; + std::optional getOptionalInt64Value(uint64_t const entity, storm::expressions::Variable const& integerVariable) const; + double getDoubleValue(uint64_t const entity, storm::expressions::Variable const& doubleVariable) const; + std::optional getOptionalDoubleValue(uint64_t const entity, storm::expressions::Variable const& doubleVariable) const; + storm::RationalNumber getRationalValue(uint64_t const entity, storm::expressions::Variable const& rationalVariable) const; + std::optional getOptionalRationalValue(uint64_t const entity, storm::expressions::Variable const& rationalVariable) const; + std::string getStringValue(uint64_t const entity, storm::expressions::Variable const& stringVariable) const; + std::optional getOptionalStringValue(uint64_t const entity, storm::expressions::Variable const& stringVariable) const; + + /*! + * Reads the variable values for the given entity and sets them into the given expression evaluator. + * @tparam RationalValueType The value type of rationals as stored by the evaluator (e.g. double or storm::RationalNumber). + * @param entity Entity index; must be less than size(). + * @param evaluator The expression evaluator to set the variable values into. + */ + template + void setValuesInEvaluator(uint64_t entity, storm::expressions::ExpressionEvaluator& evaluator) const; + + /*! + * Returns a vector of size getNumberOfEntities() such that the i'th entry is the value of the given variable of entity i. + */ + storm::storage::BitVector getBooleanValues(storm::expressions::Variable const& booleanVariable) const; + + /*! + * Returns a vector of size getNumberOfEntities() such that the i'th entry is the value of the given variable of entity i. + */ + std::vector getInt64Values(storm::expressions::Variable const& integerVariable) const; + + /*! + * Returns a vector of size getNumberOfEntities() such that the i'th entry is the value of the given variable of entity i. + */ + std::vector getDoubleValues(storm::expressions::Variable const& doubleVariable) const; + + /*! + * Returns a vector of size getNumberOfEntities() such that the i'th entry is the value of the given variable of entity i. + */ + std::vector getRationalValues(storm::expressions::Variable const& rationalVariable) const; + + /*! + * Returns a vector of size getNumberOfEntities() such that the i'th entry is the value of the given variable of entity i. + */ + std::vector getStringValues(storm::expressions::Variable const& stringVariable) const; + + /*! + * Returns a string representation of the valuation. + * + * @param selectedVariables If given, only the informations for the variables in this set are processed. + * @return The string representation. + */ + std::string toString(uint64_t const entity, bool const pretty = true, + std::optional> const& selectedVariables = {}) const; + + /*! + * Returns a JSON representation of this valuation + * @param selectedVariables If given, only the informations for the variables in this set are processed. + * @return the json representation + */ + template + storm::json toJson(uint64_t const entity, std::optional> const& selectedVariables = {}) const; + + /*! + * Derive new valuations from this by selecting the given entities. + */ + Valuations selectEntities(storm::storage::BitVector const& selectedEntities) const; + + /*! + * Derive new valuations from this by selecting the given entities. + * Requires that the selectedEntities are valid indices, i.e., < getNumberOfEntities() + */ + Valuations selectEntities(std::vector const& selectedEntities) const; + + std::size_t hash() const; + + private: + std::unique_ptr umbValuations; +}; + +} // namespace storage::sparse +} // namespace storm \ No newline at end of file diff --git a/src/storm/storage/valuations/ValuationsStorage.cpp b/src/storm/storage/valuations/ValuationsStorage.cpp new file mode 100644 index 0000000000..264357e946 --- /dev/null +++ b/src/storm/storage/valuations/ValuationsStorage.cpp @@ -0,0 +1,633 @@ +#include "storm/storage/valuations/ValuationsStorage.h" + +#include +#include +#include + +#include + +#include "storm/storage/BitVector.h" +#include "storm/storage/expressions/ExpressionEvaluator.h" +#include "storm/storage/umb/model/ValueEncoding.h" +#include "storm/utility/bitoperations.h" + +#include "storm/exceptions/IllegalFunctionCallException.h" +#include "storm/exceptions/NotSupportedException.h" +#include "storm/exceptions/OutOfRangeException.h" + +namespace storm::storage::sparse { +namespace detail { + +bool fits64Bit(ValuationClassDescription::Variable const& varDesc) { + using enum storm::umb::Type; + if (varDesc.type.bitSize() > 64) { + return false; + } + switch (varDesc.type.type) { + case Bool: + return true; + case Uint: { + // The smallest possible value is 0 + offset. As the offset is given as int64_t, it always fits into 64 bits. + // We have to check if the largest possible value also fits. + if (varDesc.offset.value_or(0) == 0) { + // The offset is 0 and the bitSize is <= 64, so this always fits + return true; + } else if (varDesc.upper.has_value()) { + // If the upper bound is given (as int64_t), then the largest value to represent is max(upper, upper - offset). + // Since all numbers involved are given as int64_t, the max value will fit into 64 bits as well. + return true; + } else if (varDesc.type.bitSize() == 64) { + // The largest actual value is 2^64 - 1 + offset. + // This never fits into 64 bits for positive offset. + // For negative offsets, the actual value type would be int64_t. Then the above number only fits if offset = -2^63 + // Since offset != 0 in this branch, that is the only valid case where the values fit into 64 bits. + return varDesc.offset.value() == std::numeric_limits::min(); + } else { + // The largest actual value is at most 2^63 - 1 + offset + // For positive offset, the actual type is uint64_t and we can upper bound the above number by 2^63 - 1 + 2^63 - 1 = 2^64 - 2 < uint64_t max + // For negative offset, the actual type is int64_t and we can upper bound the above number by 2^63 - 1 <= int64_t max + return true; + } + } + case Int: { + if (varDesc.offset.value_or(0) == 0) { + return true; + } else if (varDesc.offset.value() < 0) { + // negative offset. We might have trouble representing the smallest actual value + int64_t const minValueStored = + varDesc.type.bitSize() == 64 ? std::numeric_limits::min() : -(static_cast(1) << (varDesc.type.bitSize() - 1)); + return varDesc.lower.has_value() || minValueStored >= std::numeric_limits::min() - varDesc.offset.value(); + } else { + // positive offset. We might have trouble representing the largest actual value + int64_t const maxValueStored = + varDesc.type.bitSize() == 64 ? std::numeric_limits::max() : (static_cast(1) << (varDesc.type.bitSize() - 1)) - 1; + return varDesc.upper.has_value() || maxValueStored <= std::numeric_limits::max() - varDesc.offset.value(); + } + } + case Double: + return true; // double values are always stored as 64 bit IEEE 754 values + case Rational: + return false; + case String: + return true; // string indices are always stored as uint64_t + default: + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, + "ValuationsStorage for variable type '" << varDesc.type.toString() << "' are not supported."); + } +} + +template +ValuationsStorage::VariablesInformation createVariablesInformation(ManagerType& expressionManager, ValuationClassDescription const& description) { + std::vector variables; + uint64_t currentOffset = 0; + for (auto const& varVariant : description.variables) { + if (std::holds_alternative(varVariant)) { + auto const& varDesc = std::get(varVariant); + storm::expressions::Variable exprVar; + if constexpr (std::is_const_v) { + exprVar = expressionManager.getVariable(varDesc.name); + } else { + storm::expressions::Type variableType; + using enum storm::umb::Type; + switch (varDesc.type.type) { + case Bool: + variableType = expressionManager.getBooleanType(); + break; + case Uint: + case Int: + variableType = expressionManager.getIntegerType(); + break; + case Double: + case Rational: + variableType = expressionManager.getRationalType(); + break; + case String: + variableType = expressionManager.getStringType(); + break; + default: + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, + "ValuationsStorage for variable type '" << varDesc.type.toString() << "' are not supported."); + } + exprVar = expressionManager.declareOrGetVariable(varDesc.name, variableType); + } + if (varDesc.isOptional.value_or(false)) { + ++currentOffset; // optional variables have a preceding presence bit + } + variables.emplace_back(typename ValuationsStorage::VariableInformation{ + .expressionVariable = exprVar, .description = varDesc, .bitOffset = currentOffset, .fits64Bit = fits64Bit(varDesc)}); + currentOffset += variables.back().description.type.bitSize(); + } else { + auto const& padding = std::get(varVariant); + currentOffset += padding.padding; + } + } + STORM_LOG_ASSERT(currentOffset == description.sizeInBits(), "Computed size does not match description size."); + STORM_LOG_ASSERT(currentOffset % 8 == 0, "Invalid valuation description detected: size in bits must be a multiple of 8."); + return typename ValuationsStorage::VariablesInformation{ + .variables = std::move(variables), .expressionManager = expressionManager.shared_from_this(), .sizeInBytes = currentOffset / 8}; +} + +} // namespace detail + +ValuationsStorage::ValuationsStorage(uint64_t const numEntities, std::vector const& descriptions, std::vector valuations, + std::vector stringMapping, std::vector strings, std::optional> classes, + std::vector> expressionManagers) + : numEntities(numEntities), valuations(std::move(valuations)), stringMapping(std::move(stringMapping)), strings(std::move(strings)) { + STORM_LOG_ASSERT(descriptions.size() == expressionManagers.size() || expressionManagers.size() <= 1, + "Mismatch between number of descriptions and expression managers."); + // First set up the variable classes. + // We either have a separate manager for each class or all classes share the same manager. + // Furthermore, we might create a new manager for a class, if no manager was given explicitly. + auto sharedManager = std::make_shared(); + for (uint64_t i = 0; i < descriptions.size(); ++i) { + if (expressionManagers.empty() || (expressionManagers.size() == 1 && expressionManagers.front() == nullptr)) { + // Shared manager for all classes, not given explicitly + variableClasses.push_back(detail::createVariablesInformation(*sharedManager, descriptions[i])); + } else if (expressionManagers.size() == 1) { + // Shared manager for all classes, given explicitly + variableClasses.push_back(detail::createVariablesInformation(*expressionManagers.front(), descriptions[i])); + } else if (expressionManagers[i] == nullptr) { + // Separate manager for each class, not given explicitly + auto manager = std::make_shared(); + variableClasses.push_back(detail::createVariablesInformation(*manager, descriptions[i])); + } else { + // Separate manager for each class, given explicitly + variableClasses.push_back(detail::createVariablesInformation(*expressionManagers[i], descriptions[i])); + } + } + // Initialize string mappings. It should be given iff there is a string variable + bool const hasStringVariable = std::any_of(descriptions.begin(), descriptions.end(), [](auto const& classDescr) { return classDescr.hasStringVariable(); }); + if (hasStringVariable && this->stringMapping.empty()) { + this->stringMapping.push_back(0); + } + STORM_LOG_ASSERT(hasStringVariable || this->stringMapping.empty(), "Non-empty string mapping given but there is no string variable."); + STORM_LOG_ASSERT(stringMapping.empty() || this->stringMapping.back() == strings.size(), + "String mapping should end with the total size of the string data."); + + // Enable quick access to the right byte span for each entity. + if (classes.has_value() && this->variableClasses.size() > 1) { + STORM_LOG_ASSERT(numEntities == classes->size(), "Number of entities does not match class mapping size."); + this->entityClassMappings = {std::move(*classes), std::vector({0ull})}; + uint64_t pos = 0; + this->entityClassMappings->toValuationsMapping.reserve(this->entityClassMappings->toClassMapping.size() + 1); + for (uint64_t entity = 0; entity < this->entityClassMappings->toClassMapping.size(); ++entity) { + STORM_LOG_ASSERT( + this->entityClassMappings->toClassMapping[entity] < this->variableClasses.size(), + "Class index " << this->entityClassMappings->toClassMapping[entity] << " out of bounds. Only " << descriptions.size() << "classes known."); + pos += this->variableClasses[this->entityClassMappings->toClassMapping[entity]].sizeInBytes; + this->entityClassMappings->toValuationsMapping.push_back(pos); + } + STORM_LOG_ASSERT(this->valuations.size() == pos, "Valuation data size does not match class mapping."); + } else { + STORM_LOG_ASSERT(this->variableClasses.size() == 1, "Valuation descriptions must be unique if no class mapping is given."); + STORM_LOG_ASSERT(!classes.has_value() || std::all_of(classes->begin(), classes->end(), [&](auto classIndex) { return classIndex == 0; }), + "A single description is given but the class mapping is not unique."); + STORM_LOG_ASSERT(this->variableClasses.front().sizeInBytes == 0 || this->valuations.size() % this->variableClasses.front().sizeInBytes == 0, + "Valuation data size is not a multiple of the unique valuation size."); + STORM_LOG_ASSERT(numEntities * this->variableClasses.front().sizeInBytes == this->valuations.size(), + "Valuation data size (" << valuations.size() << ") does not match number of entities (" << this->numEntities + << ") times valuation size (" << this->variableClasses.front().sizeInBytes << ")."); + } +} + +ValuationsStorage::ValuationsStorage(uint64_t const numEntities, ValuationClassDescription const& description, std::vector valuations, + std::shared_ptr expressionManager) + : ValuationsStorage(numEntities, {description}, std::move(valuations), {}, {}, std::nullopt, {expressionManager}) { + STORM_LOG_ASSERT(!description.hasStringVariable(), "String mapping must be given for descriptions with string variables."); +} + +ValuationsStorage::ValuationsStorage(std::vector const& descriptions, + std::vector> expressionManagers) + : ValuationsStorage(0, descriptions, {}, {}, {}, std::vector{}, std::move(expressionManagers)) {} + +ValuationsStorage::ValuationsStorage(ValuationClassDescription const& description, + std::shared_ptr expressionManager) + : ValuationsStorage(0, {description}, {}, {}, {}, std::nullopt, {expressionManager}) {} + +ValuationsStorage::ValuationsStorage(std::vector const& variableClasses) : numEntities(0), variableClasses(variableClasses) {} + +uint64_t ValuationsStorage::size() const { + return numEntities; +} + +uint64_t ValuationsStorage::numClasses() const { + return variableClasses.size(); +} + +uint64_t ValuationsStorage::numStrings() const { + return stringMapping.size() > 0 ? stringMapping.size() - 1 : 0; +} + +bool ValuationsStorage::hasStrings() const { + return !stringMapping.empty(); +} + +uint64_t ValuationsStorage::getClassOfEntity(uint64_t entity) const { + STORM_LOG_ASSERT(entity < size(), "Entity index out of bounds: " << entity << " >= " << size() << "."); + if (entityClassMappings) { + return entityClassMappings->toClassMapping[entity]; + } else { + STORM_LOG_ASSERT(variableClasses.size() == 1, "No class mapping given but multiple classes exist."); + return 0; + } +} + +ValuationClassDescription ValuationsStorage::getClassDescription(uint64_t classIndex) const { + STORM_LOG_ASSERT(classIndex < numClasses(), "Class index " << classIndex << " out of bounds. Only " << variableClasses.size() << "classes known."); + ValuationClassDescription res; + uint64_t currBit = 0; + for (auto const& varInfo : variableClasses[classIndex].variables) { + uint64_t padding = varInfo.bitOffset - currBit; + if (varInfo.description.isOptional.value_or(false)) { + STORM_LOG_ASSERT(padding >= 1, "Optional variables must have at least 1 bit preceding its offset."); + --padding; + } + if (padding > 0) { + res.variables.push_back(ValuationClassDescription::Padding{.padding = padding}); + } + res.variables.push_back(varInfo.description); + currBit = varInfo.bitOffset + varInfo.description.type.bitSize(); + STORM_LOG_ASSERT(currBit == res.sizeInBits(), "Unexpected bit offset for variable " << varInfo.description.name << " in class " << classIndex + << ". Expected " << res.sizeInBits() << ", got " + << varInfo.bitOffset << "."); + } + if (uint64_t padding = currBit % 8; padding > 0) { + res.variables.push_back(ValuationClassDescription::Padding{.padding = 8 - padding}); + } + return res; +} + +storm::expressions::ExpressionManager const& ValuationsStorage::getManager() const { + STORM_LOG_ASSERT(!variableClasses.empty(), "No variable classes given, cannot determine expression manager."); + auto const& manager = variableClasses.front().expressionManager; + STORM_LOG_THROW( + std::all_of(variableClasses.begin() + 1, variableClasses.end(), [&manager](auto const& varClass) { return varClass.expressionManager == manager; }), + storm::exceptions::IllegalFunctionCallException, "Expression manager is not unique."); + return *manager; +} + +storm::expressions::ExpressionManager const& ValuationsStorage::getManager(uint64_t classIndex) const { + STORM_LOG_ASSERT(classIndex < variableClasses.size(), + "Class index " << classIndex << " out of bounds. Only " << variableClasses.size() << "classes known."); + return *variableClasses[classIndex].expressionManager; +} + +ValuationsStorage::VariableInformation const& ValuationsStorage::getVariableInformation(uint64_t entity, storm::expressions::Variable const& variable) const { + auto const& vars = info(entity).variables; + auto varInfoIt = std::find_if(vars.begin(), vars.end(), [&variable](auto const& varInfo) { return varInfo.expressionVariable == variable; }); + STORM_LOG_ASSERT(varInfoIt != vars.end(), "Can not find unknown variable " << variable.getName() << "."); + return *varInfoIt; +} + +ValuationsStorage::VariableInformation const& ValuationsStorage::getVariableInformation(storm::expressions::Variable const& variable) const { + STORM_LOG_ASSERT(numClasses() == 1, "Trying to get variable information but the class is not unique among entities."); + return getVariableInformation(0, variable); +} + +std::set ValuationsStorage::getAllVariables() const { + [[maybe_unused]] auto const& manager = getManager(); + std::set result; + for (auto const& varClass : variableClasses) { + for (auto const& varInfo : varClass.variables) { + STORM_LOG_ASSERT(varInfo.expressionVariable.getManager() == manager, + "Expression manager of variable " << varInfo.expressionVariable.getName() << " does not match the one of the valuation."); + result.insert(varInfo.expressionVariable); + } + } + return result; +} + +bool ValuationsStorage::entityHasVariable(uint64_t entity, storm::expressions::Variable const& variable) const { + auto const& vars = info(entity).variables; + return std::any_of(vars.begin(), vars.end(), [&variable](auto const& varInfo) { return varInfo.expressionVariable == variable; }); +} + +storm::umb::UmbModel::Valuation ValuationsStorage::getRawUmbData() const { + storm::umb::UmbModel::Valuation result; + if (entityClassMappings.has_value()) { + result.valuationToClass = entityClassMappings->toClassMapping; + } + result.valuations = valuations; + if (hasStrings()) { + result.stringMapping = stringMapping; + result.strings = strings; + } + return result; +} + +void ValuationsStorage::resize(uint64_t newEntityCount, uint64_t const classIndex) { + if (newEntityCount > size()) { + // Initialize one new entity with default values. This is required to ensure that valuation data is consistent (e.g. avoid 0/0 for rationals). + emplaceBack(classIndex, [](auto&&...) {}); + // For the remaining entities, we can be a bit quicker by copying the values of the last initialized entity. + if (newEntityCount > size()) { + uint64_t const classSize = variableClasses[classIndex].sizeInBytes; + valuations.resize(valuations.size() + (newEntityCount - size()) * classSize); + if (entityClassMappings) { + entityClassMappings->toClassMapping.resize(newEntityCount, classIndex); + for (uint64_t valEnd = entityClassMappings->toValuationsMapping.back() + classSize; valEnd < valuations.size(); valEnd += classSize) { + entityClassMappings->toValuationsMapping.push_back(valEnd); + } + } + auto const srcBytes = getRawBytes(numEntities); // the bytes of the entry we initialized using emplaceBack + for (uint64_t newEntityIndex = numEntities + 1; newEntityIndex < newEntityCount; ++newEntityIndex) { + auto destBytes = getRawBytes(newEntityIndex); + std::copy(srcBytes.begin(), srcBytes.end(), destBytes.begin()); + } + numEntities = newEntityCount; + } + } else if (newEntityCount < size()) { + uint64_t const newValuationsSize = + entityClassMappings.has_value() ? entityClassMappings->toValuationsMapping[newEntityCount] : newEntityCount * variableClasses.front().sizeInBytes; + valuations.resize(newValuationsSize); + if (entityClassMappings) { + entityClassMappings->toClassMapping.resize(newEntityCount); + entityClassMappings->toValuationsMapping.resize(newEntityCount + 1); + } + numEntities = newEntityCount; + } +} + +template +void ValuationsStorage::setValuesInEvaluator(uint64_t entity, storm::expressions::ExpressionEvaluator& evaluator) const { + readCallback(entity, [&evaluator](auto, auto const& var, auto const& value) { + using ValueType = std::remove_cvref_t; + if constexpr (std::is_same_v) { + evaluator.setBooleanValue(var, value); + } else if constexpr (std::is_same_v || std::is_same_v) { + evaluator.setIntegerValue(var, value); + // evaluator has no support for arbitrary-precision integers. + } else if constexpr (std::is_same_v || std::is_same_v) { + evaluator.setRationalValue(var, storm::utility::convertNumber(value)); + } else { + STORM_LOG_THROW( + (std::is_same_v || std::is_same_v || std::is_same_v), + storm::exceptions::NotSupportedException, "Unsupported variable value type when reading state values: " << typeid(ValueType).name()); + } + }); +} + +template void ValuationsStorage::setValuesInEvaluator(uint64_t entity, storm::expressions::ExpressionEvaluator& evaluator) const; +template void ValuationsStorage::setValuesInEvaluator(uint64_t entity, + storm::expressions::ExpressionEvaluator& evaluator) const; + +ValuationsStorage::VariablesInformation const& ValuationsStorage::info(uint64_t entity) const { + return variableClasses[getClassOfEntity(entity)]; +} + +std::span ValuationsStorage::getRawBytes(uint64_t entity) const { + STORM_LOG_ASSERT(entity < size(), "Entity index out of bounds: " << entity << " >= " << size() << "."); + if (entityClassMappings) { + auto const start = entityClassMappings->toValuationsMapping[entity]; + auto const end = entityClassMappings->toValuationsMapping[entity + 1]; + return std::span(&valuations[start], end - start); + } else { + auto const start = entity * variableClasses.front().sizeInBytes; + return std::span(&valuations[start], variableClasses.front().sizeInBytes); + } +} + +std::span ValuationsStorage::getRawBytes(uint64_t entity) { + if (entityClassMappings) { + auto const start = entityClassMappings->toValuationsMapping[entity]; + auto const end = entityClassMappings->toValuationsMapping[entity + 1]; + return std::span(&valuations[start], end - start); + } else { + auto const start = entity * variableClasses.front().sizeInBytes; + return std::span(&valuations[start], variableClasses.front().sizeInBytes); + } +} + +bool ValuationsStorage::readBit(std::span bytes, uint64_t const position) const { + STORM_LOG_ASSERT(position < bytes.size() * 8, "Bit position exceeds valuation size."); + return bytes[position / 8] & (1 << (position % 8)); +} + +void ValuationsStorage::writeBit(std::span bytes, uint64_t const position, bool value) const { + STORM_LOG_ASSERT(position < bytes.size() * 8, "Bit position exceeds valuation size."); + char& byte = bytes[position / 8]; + char const pos = (1 << (position % 8)); + if (value) { + byte |= pos; + } else { + byte &= ~pos; + } +} + +uint64_t ValuationsStorage::readUint64(std::span bytes, uint64_t const bitOffset, uint64_t const bitSize) const { + STORM_LOG_ASSERT(bitOffset < bytes.size() * 8, "Variable offset exceeds valuation size."); + STORM_LOG_ASSERT(bitSize <= 64, "Invalid bit range."); + auto const firstByte = bitOffset / 8; + auto const bitOffsetWithinByte = bitOffset % 8; + auto const numBytes = (bitOffsetWithinByte + bitSize + 7) / 8; + STORM_LOG_ASSERT(numBytes <= 9, "Invalid number of bytes computed: " << numBytes); + uint64_t result; + // set the first (up to) 8 bytes + std::memcpy(&result, &bytes[firstByte], std::min(numBytes, 8ull)); + result >>= bitOffsetWithinByte; + // if necessary, set the most significant bits by reading a 9th byte + if (numBytes == 9ull) { + uint64_t upperBits = std::bit_cast(bytes[firstByte + 8]); + upperBits <<= (64 - bitOffsetWithinByte); + result |= upperBits; + } + // Set irrelevant bits to zero + if (bitSize < 64) { + uint64_t const relevantBitMask = (1ull << bitSize) - 1; + result &= relevantBitMask; + } + return result; +} + +void ValuationsStorage::writeUint64(std::span bytes, uint64_t const bitOffset, uint64_t const bitSize, uint64_t const value) const { + STORM_LOG_ASSERT(bitOffset < bytes.size() * 8, "Variable offset exceeds valuation size."); + STORM_LOG_ASSERT(bitSize <= 64, "Invalid bit range."); + STORM_LOG_THROW(bitSize == 64 || value < (1ull << bitSize), storm::exceptions::OutOfRangeException, + "Invalid value " << value << " for bit size " << bitSize); + uint64_t const firstByte = bitOffset / 8; + uint8_t const bitOffsetWithinByte = bitOffset % 8; + uint8_t const numBytes = (bitOffsetWithinByte + bitSize + 7) / 8; + uint8_t const numFullBytes = (bitOffsetWithinByte + bitSize) / 8; + STORM_LOG_ASSERT(numBytes <= 9, "Invalid number of bytes computed: " << numBytes); + if (numFullBytes == 0) { + // We only have to write into a single byte + char& byte = bytes[firstByte]; + uint8_t const relevantBitsMask = ((1 << bitSize) - 1) << bitOffsetWithinByte; // e.g. 0000 1110 for bitOffsetWithinByte=1 and bitSize=3 + byte &= static_cast(~relevantBitsMask); // set relevant bits to zero + byte |= static_cast((value << bitOffsetWithinByte) & relevantBitsMask); // set relevant bits to the value bits + } else { + // First write all full bytes + if (bitOffsetWithinByte == 0) { + // Fast path: variable is byte-aligned, so we can directly write all full bytes without bit shifts + std::memcpy(&bytes[firstByte], &value, numFullBytes); + } else { + uint64_t const shiftedValue = (static_cast(bytes[firstByte]) & ((1ull << bitOffsetWithinByte) - 1)) | (value << bitOffsetWithinByte); + std::memcpy(&bytes[firstByte], &shiftedValue, numFullBytes); + } + // Then write the last byte if necessary + if (numFullBytes != numBytes) { + // we have to write a partial byte at the end, so we need to read the existing byte and only overwrite the relevant bits + char& lastByte = bytes[firstByte + numFullBytes]; + uint8_t const numBitsUsedInLastByte = (bitOffsetWithinByte + bitSize) % 8; + lastByte &= static_cast((1 << numBitsUsedInLastByte) - 1); // set relevant bits to zero + lastByte |= static_cast(value >> (numFullBytes * 8 - bitOffsetWithinByte)); // set relevant bits to the value bits + } + } +} + +template +ValuationsStorage::Integer ValuationsStorage::readInteger(std::span bytes, uint64_t const bitOffset, uint64_t const bitSize) const { + auto const num64BitChunks = (bitSize + 63) / 64; + auto chunksView = std::ranges::iota_view(0ull, num64BitChunks) | std::ranges::views::transform([this, &bytes, &bitOffset, &bitSize](auto i) -> uint64_t { + return readUint64(bytes, bitOffset + i * 64, std::min(64, bitSize - i * 64)); + }); + Integer result = storm::umb::ValueEncoding::decodeArbitraryPrecisionInteger(chunksView); + if constexpr (Signed) { + // Check if this number is supposed to be negative + if (result >= storm::utility::pow(2, bitSize - 1)) { + return result - storm::utility::pow(2, bitSize); + } + } + return result; +} + +template ValuationsStorage::Integer ValuationsStorage::readInteger(std::span, uint64_t, uint64_t) const; +template ValuationsStorage::Integer ValuationsStorage::readInteger(std::span, uint64_t, uint64_t) const; + +template +void ValuationsStorage::writeInteger(std::span bytes, uint64_t bitOffset, uint64_t bitSize, Integer const& value) const { + STORM_LOG_THROW(storm::umb::ValueEncoding::getSizeOfIntegerEncoding(value) <= bitSize, storm::exceptions::OutOfRangeException, + "Value " << value << " cannot be encoded in " << bitSize << " bits."); + auto const num64BitChunks = (bitSize + 63) / 64; + std::vector uint64Encoding; + storm::umb::ValueEncoding::appendEncodedInteger(uint64Encoding, value, num64BitChunks); + STORM_LOG_ASSERT(uint64Encoding.size() == num64BitChunks, "Encoding does not fit into the specified bit size."); + for (auto v : uint64Encoding) { + if (bitSize >= 64) { + writeUint64(bytes, bitOffset, 64, v); + bitOffset += 64; + bitSize -= 64; + } else { + uint64_t const relevantBitMask = (1ull << bitSize) - 1; + // Check if the number is negative by looking at the sign bit + if (Signed && ((v & (1ull << (bitSize - 1))) != 0)) { + STORM_LOG_ASSERT(value < 0, "Value " << value << " is non-negative but the sign bit is set."); + // Assert that all irrelevant bits are set + STORM_LOG_ASSERT((~relevantBitMask & v) == ~relevantBitMask, + "Value " << value << " does not fit into the specified bit size of " << bitSize << " bits."); + // For negative numbers, we clear the upper (unused) bits, so that the resulting (unsigned) value fits into + // the specified bit size. For example, -3 with bitSize=3 would be represented as 101. We get the 64 bit + // value 1...1101 which (interpreted as unsigned value) doesn't fit into 3 bits. We need 0...0101. + v &= relevantBitMask; // set upper bits to zero + } else { + // Assert that all irrelevant bits are not set + STORM_LOG_ASSERT((~relevantBitMask & v) == 0, "Value " << value << " does not fit into the specified bit size of " << bitSize << " bits."); + } + writeUint64(bytes, bitOffset, bitSize, v); + bitSize = 0; + break; + } + } + STORM_LOG_ASSERT(bitSize == 0, "Unexpected integer encoding. Not all bits were written."); +} + +template void ValuationsStorage::writeInteger(std::span, uint64_t, uint64_t, Integer const&) const; +template void ValuationsStorage::writeInteger(std::span, uint64_t, uint64_t, Integer const&) const; + +template +void ValuationsStorage::writeValue(std::span bytes, uint64_t bitOffset, uint64_t bitSize, ValueType const& value) { + if constexpr (std::is_same_v) { + writeUint64(bytes, bitOffset, bitSize, value ? 1ul : 0ul); + } else if constexpr (std::is_same_v) { + writeUint64(bytes, bitOffset, bitSize, value); + } else if constexpr (std::is_same_v) { + if (value < 0) { + // For negative value, take the two's complement (e.g. 1111...1101 is -3) + uint64_t v = ~static_cast(-(value + 1)); + // Clear upper bits + if (bitSize < 64) { + v &= (1ull << bitSize) - 1; + } + writeUint64(bytes, bitOffset, bitSize, v); + } else { + // For positive value, the binary representation is the same as for unsigned values + writeUint64(bytes, bitOffset, bitSize, static_cast(value)); + } + } else if constexpr (std::is_same_v) { + writeUint64(bytes, bitOffset, bitSize, std::bit_cast(value)); + } else if constexpr (std::is_same_v) { + if (value < 0) { + writeInteger(bytes, bitOffset, bitSize, value); + } else { + writeInteger(bytes, bitOffset, bitSize, value); + } + } else if constexpr (std::is_same_v) { + STORM_LOG_ASSERT(bitSize % 2 == 0, "Uneven bitsize for rational number not expected."); + auto const numDenSize = bitSize / 2; + writeInteger(bytes, bitOffset, numDenSize, storm::utility::numerator(value)); + static_assert(storm::RationalNumberDenominatorAlwaysPositive); + writeInteger(bytes, bitOffset + numDenSize, numDenSize, storm::utility::denominator(value)); + } else { + // Note: overwriting the string does not erase the old string from the strings vector as it might still be in use elsewhere + static_assert(std::is_same_v || std::is_same_v); + uint64_t const index = storm::umb::StringsBuilder(strings, stringMapping).findOrPushBack(value); + writeUint64(bytes, bitOffset, bitSize, index); + } +} + +template void ValuationsStorage::writeValue(std::span, uint64_t, uint64_t, bool const&); +template void ValuationsStorage::writeValue(std::span, uint64_t, uint64_t, uint64_t const&); +template void ValuationsStorage::writeValue(std::span, uint64_t, uint64_t, int64_t const&); +template void ValuationsStorage::writeValue(std::span, uint64_t, uint64_t, double const&); +template void ValuationsStorage::writeValue(std::span, uint64_t, uint64_t, ValuationsStorage::Integer const&); +template void ValuationsStorage::writeValue(std::span, uint64_t, uint64_t, storm::RationalNumber const&); +template void ValuationsStorage::writeValue(std::span, uint64_t, uint64_t, std::string_view const&); +template void ValuationsStorage::writeValue(std::span, uint64_t, uint64_t, std::string const&); + +template +ValuationsStorage ValuationsStorage::selectEntities(T const& selectedEntities) const { + ValuationsStorage result(variableClasses); + result.numEntities = [&selectedEntities]() { + if constexpr (std::is_same_v) { + return selectedEntities.getNumberOfSetBits(); + } else { + return std::ranges::distance(selectedEntities); + } + }(); + result.stringMapping = stringMapping; + result.strings = strings; + + if (entityClassMappings) { + result.entityClassMappings.emplace(); + result.entityClassMappings->toValuationsMapping.reserve(result.numEntities + 1); + result.entityClassMappings->toValuationsMapping.push_back(0); // first entry of toValuationsMapping must be 0 + result.entityClassMappings->toClassMapping.reserve(result.numEntities); + } else { + result.valuations.reserve(result.numEntities * result.variableClasses.front().sizeInBytes); + } + for (auto const oldEntityIndex : selectedEntities) { + STORM_LOG_ASSERT(oldEntityIndex < size(), "Selected entity index " << oldEntityIndex << " out of bounds. Only " << size() << " entities known."); + auto const bytes = getRawBytes(oldEntityIndex); + result.valuations.insert(result.valuations.end(), bytes.begin(), bytes.end()); + if (entityClassMappings) { + result.entityClassMappings->toValuationsMapping.push_back(result.valuations.size()); + result.entityClassMappings->toClassMapping.push_back(entityClassMappings->toClassMapping[oldEntityIndex]); + } + } + return result; +} + +template ValuationsStorage ValuationsStorage::selectEntities(storm::storage::BitVector const&) const; +template ValuationsStorage ValuationsStorage::selectEntities>(std::vector const&) const; + +std::size_t ValuationsStorage::hash() const { + // As the valuations are stored as a sequence of chars, we can pretend that this is a string and use efficient string_view hashing + auto const hashBytes = std::hash{}; + + std::size_t seed = hashBytes(std::string_view(valuations.data(), valuations.size())); + boost::hash_combine(seed, hashBytes(std::string_view(strings.data(), strings.size()))); + + return seed; +} + +} // namespace storm::storage::sparse diff --git a/src/storm/storage/valuations/ValuationsStorage.h b/src/storm/storage/valuations/ValuationsStorage.h new file mode 100644 index 0000000000..6268533ff1 --- /dev/null +++ b/src/storm/storage/valuations/ValuationsStorage.h @@ -0,0 +1,770 @@ +#pragma once + +#include +#include +#include +#include +#include +#include +#include + +#include "storm/storage/expressions/ExpressionManager.h" +#include "storm/storage/expressions/Variable.h" +#include "storm/storage/umb/model/StringEncoding.h" +#include "storm/storage/umb/model/UmbModel.h" +#include "storm/storage/valuations/ValuationDescription.h" +#include "storm/utility/macros.h" + +#include "storm/exceptions/NotSupportedException.h" +#include "storm/exceptions/OutOfRangeException.h" +#include "storm/exceptions/UnexpectedException.h" + +namespace storm::expressions { +template +class ExpressionEvaluator; +} + +namespace storm::storage::sparse { + +/*! + * Concept for a callback used in readCallback / readValue. + * The callback is invoked as callback(entity, variable, value) where value is one of the + * supported value types (bool, int64_t, uint64_t, double, RationalNumber, string_view, string, + * or std::nullopt_t for unset optional variables). + */ +template +concept ValuationReadCallback = + std::invocable || std::invocable || + std::invocable || std::invocable || + std::invocable || + std::invocable::IntegerType> || + std::invocable || + std::invocable || + std::invocable; + +/*! + * Concept for a callback used in writeCallback / writeValue. + * The callback is invoked as callback(entity, variable, value) where value is passed by + * (non-const) lvalue reference so the callback can assign the new value. + * For optional variables (AllowOptional=true), value is wrapped in std::optional&. + */ +template +concept ValuationWriteCallback = + std::invocable || std::invocable || + std::invocable || std::invocable || + std::invocable || + std::invocable::IntegerType&> || + std::invocable; + +/*! + * Stores valuations of variables for a set of entities (e.g. states / observations) in the packed, + * bit-level binary layout defined by the UMB (Unified Markov Binary) format. The in-memory layout of + * this class must therefore stay compliant with the UMB specification so that the raw data obtained via + * getRawUmbData() can be written to / read from a UMB file without further conversion. + * @see https://pmc-tools.github.io/umb/spec + * @see https://arxiv.org/abs/2606.17811 + */ +class ValuationsStorage { + public: + using Integer = storm::NumberTraits::IntegerType; + + /*! + * Compiled information about a single variable within a valuation class. + * Derived from the ValuationClassDescription at construction time and cached here to avoid + * recomputing bit offsets and type properties on every read/write. + */ + struct VariableInformation { + storm::expressions::Variable const expressionVariable; + ValuationClassDescription::Variable const description; + uint64_t const bitOffset; // The first bit holding the variable's data within the valuation. + // If the variable is optional, the optional bit is located at bitOffset - 1 + bool const fits64Bit; + }; + + /*! + * Compiled information about all variables belonging to one valuation class. + * Holds the per-variable information list, the owning ExpressionManager, and the total + * size in bytes of one entity's packed valuation data for this class. + */ + struct VariablesInformation { + std::vector const variables; + std::shared_ptr const expressionManager; + uint64_t const sizeInBytes; + }; + + ValuationsStorage(ValuationsStorage const&) = default; + ValuationsStorage(ValuationsStorage&&) = default; + ValuationsStorage& operator=(ValuationsStorage const&) = default; + ValuationsStorage& operator=(ValuationsStorage&&) = default; + + /*! + * Full constructor. Creates a ValuationsStorage object from pre-existing packed data. + * @param numEntities Number of entities whose valuations are stored. + * @param descriptions One ValuationClassDescription per class. + * @param valuations Packed valuation bytes for all entities. + * @param stringMapping CSR offsets into @p strings; must end with strings.size(). + * Pass empty when there are no string variables. + * @param strings Concatenated string data referenced by @p stringMapping. + * @param classes Per-entity class index vector. If omitted (or all zeros), all entities + * are assumed to belong to class 0. Required when @p descriptions has + * more than one entry and entities differ in class. + * @param expressionManagers Expression managers to use for variable lookup. If empty or a + * single nullptr, a fresh shared manager is created for all classes. + * If a single non-null pointer is given, it is shared across all classes. + * If one pointer per class is given, each class gets its own manager. + */ + ValuationsStorage(uint64_t numEntities, std::vector const& descriptions, std::vector valuations, + std::vector stringMapping, std::vector strings, std::optional> classes = {}, + std::vector> expressionManagers = {}); + + /*! + * Convenience constructor for a single-class ValuationsStorage with pre-existing packed data. + * Equivalent to the full constructor with a single description, no class mapping, and no + * string data. Asserts that @p description contains no string variables. + * @param numEntities Number of entities. + * @param description The single valuation class description. + * @param valuations Packed valuation bytes. + * @param expressionManager Expression manager to use; a fresh one is created if null. + */ + ValuationsStorage(uint64_t numEntities, ValuationClassDescription const& description, std::vector valuations, + std::shared_ptr expressionManager = {}); + + /*! + * Constructs an empty (zero-entity) ValuationsStorage ready to receive multiple classes via + * emplaceBack / resize. + * @param descriptions One ValuationClassDescription per class. + * @param expressionManagers See full constructor for semantics. + */ + ValuationsStorage(std::vector const& descriptions, + std::vector> expressionManagers = {}); + + /*! + * Constructs an empty (zero-entity) single-class ValuationsStorage ready to receive entities via + * emplaceBack / resize. + * @param description The single valuation class description. + * @param expressionManager Expression manager to use; a fresh one is created if null. + */ + ValuationsStorage(ValuationClassDescription const& description, std::shared_ptr expressionManager = {}); + + /*! + * @return The number of entities (e.g. states) that this ValuationsStorage assigns values for. + */ + uint64_t size() const; + + /*! + * @return The number of distinct valuation classes (i.e. the number of ValuationClassDescriptions + * this object was constructed with). + */ + uint64_t numClasses() const; + + /*! + * @return The number of distinct string values stored across all string variables. + */ + uint64_t numStrings() const; + + /*! + * @return True iff this ValuationsStorage contains at least one string variable (and therefore + * maintains a non-empty string table). + */ + bool hasStrings() const; + + /*! + * Returns the class index of the given entity. + * When all entities share a single class this always returns 0. + * @param entity Entity index; must be less than size(). + */ + uint64_t getClassOfEntity(uint64_t entity) const; + + /*! + * Reconstructs the ValuationClassDescription for the given class from the stored compiled + * variable information, including any padding entries. + * @param classIndex Class index; must be less than numClasses(). Defaults to 0. + */ + ValuationClassDescription getClassDescription(uint64_t classIndex = 0) const; + + /*! + * Returns the expression manager shared by all classes. + * @throws IllegalFunctionCallException if different classes use different managers. + */ + storm::expressions::ExpressionManager const& getManager() const; + + /*! + * Returns the expression manager for the given class. + * @param classIndex Class index; must be less than numClasses(). + */ + storm::expressions::ExpressionManager const& getManager(uint64_t classIndex) const; + + /*! + * Returns all expression variables that this valuation assigns values to for at least one class. + */ + std::set getAllVariables() const; + + /*! + * Returns true iff the variable is relevant for the given entity's class, i.e. it is listed in the class description + */ + bool entityHasVariable(uint64_t entity, storm::expressions::Variable const& variable) const; + + /*! + * Looks up compiled variable information for the given entity and variable. + * The lookup is performed in the class that @p entity belongs to. + * @param entity Entity index; must be less than size(). + * @param variable An expression variable registered in the corresponding ExpressionManager. + */ + VariableInformation const& getVariableInformation(uint64_t entity, storm::expressions::Variable const& variable) const; + + /*! + * Looks up compiled variable information for the given variable. + * Only valid when numClasses() == 1 (asserts otherwise); uses entity 0 for the lookup. + * @param variable An expression variable registered in the ExpressionManager. + */ + VariableInformation const& getVariableInformation(storm::expressions::Variable const& variable) const; + + /*! + * Exports a snapshot of the raw UMB model valuation data (packed bytes, optional class + * mapping, and string table) in the format expected by UmbModel::Valuation. + */ + typename storm::umb::UmbModel::Valuation getRawUmbData() const; + + /*! + * Resizes the entity count to @p newEntityCount. + * When growing, new entities are appended to @p classIndex and initialized with default + * values (lower bound for integers, false for booleans, etc.). When shrinking, the trailing + * entities are removed. No-op if newEntityCount == size(). + * @param newEntityCount Desired number of entities after the call. + * @param classIndex Class to use for newly appended entities. Defaults to 0. + */ + void resize(uint64_t newEntityCount, uint64_t classIndex = 0); + + /*! + * Appends a new entity of the given class and populates its variables via @p callback. + * The callback is invoked once per variable with the entity index, the variable, and a + * mutable reference to the (default-initialized) value to be written. + * @tparam AllowOptional If true, the callback receives std::optional& for + * optional variables, allowing them to be left unset (std::nullopt). + * @tparam AllowedTypes If non-empty, only variables whose natural type is in this list + * will be passed to the callback; others are silently skipped. + * @tparam Callback A type satisfying ValuationWriteCallback. + * @param classIndex The class index for the new entity. + * @param callback Callable invoked as callback(entity, variable, value). + */ + template + void emplaceBack(uint64_t classIndex, Callback const& callback) { + STORM_LOG_ASSERT(classIndex < variableClasses.size(), + "Class index " << classIndex << " out of bounds. Only " << variableClasses.size() << "classes known."); + valuations.resize(valuations.size() + variableClasses[classIndex].sizeInBytes, 0); + if (entityClassMappings) { + entityClassMappings->toClassMapping.push_back(classIndex); + entityClassMappings->toValuationsMapping.push_back(valuations.size()); + } + ++numEntities; + writeCallback(size() - 1, callback); + } + + /*! + * Convenience overload of emplaceBack for single-class ValuationsStorage (asserts numClasses() == 1). + * @tparam AllowOptional See emplaceBack(classIndex, callback). + * @tparam AllowedTypes See emplaceBack(classIndex, callback). + * @tparam Callback A type satisfying ValuationWriteCallback. + * @param callback Callable invoked as callback(entity, variable, value). + */ + template + void emplaceBack(Callback const& callback) { + STORM_LOG_ASSERT(variableClasses.size() == 1, "Trying to add a valuation but the class is not unique."); + emplaceBack(0, callback); + } + + /*! + * Constructs a new ValuationsStorage containing only the selected entities, in the order they + * appear in @p selectedEntities. The string table is shared (copied) verbatim. + * @tparam T Either storm::storage::BitVector or any range of uint64_t entity indices. + * @param selectedEntities The set or sequence of entity indices to include. + * @return A new ValuationsStorage with size() equal to the number of selected entities. + */ + template + ValuationsStorage selectEntities(T const& selectedEntities) const; + + /*! + * Reads all variables of the given entity and invokes @p callback for each one. + * @tparam AllowedTypes If non-empty, the callback is only invoked for variables whose + * natural value type is among these types. + * @tparam Callback A type satisfying ValuationReadCallback. + * @param entity Entity index; must be less than size(). + * @param callback Callable invoked as callback(entity, variable, value). + */ + template + void readCallback(uint64_t entity, Callback const& callback) const { + for (auto const& varInfo : info(entity).variables) { + read(entity, varInfo, callback); + } + } + + /*! + * Reads a single variable of the given entity and invokes @p callback with its value. + * @tparam AllowedTypes See readCallback(entity, callback). + * @tparam Callback A type satisfying ValuationReadCallback. + * @param entity Entity index; must be less than size(). + * @param variable The variable to read. + * @param callback Callable invoked as callback(entity, variable, value). + */ + template + void readCallback(uint64_t entity, storm::expressions::Variable const& variable, Callback const& callback) const { + read(entity, getVariableInformation(entity, variable), callback); + } + + /*! + * Reads the given variable for every entity and invokes @p callback for each one. + * When numClasses() == 1, the variable information is looked up only once for efficiency. + * @tparam AllowedTypes See readCallback(entity, callback). + * @tparam Callback A type satisfying ValuationReadCallback. + * @param variable The variable to read across all entities. + * @param callback Callable invoked as callback(entity, variable, value). + */ + template + void readCallback(storm::expressions::Variable const& variable, Callback const& callback) const { + if (numClasses() == 1) { + // We have only one class, so we can look up the variable info once and use it for all entities + auto const& varInfo = getVariableInformation(variable); + for (uint64_t entity = 0; entity < size(); ++entity) { + read(entity, varInfo, callback); + } + } else { + for (uint64_t entity = 0; entity < size(); ++entity) { + readCallback(entity, variable, callback); + } + } + } + + /*! + * Reads all variables of every entity and invokes @p callback for each (entity, variable) + * pair. + * @tparam AllowedTypes See readCallback(entity, callback). + * @tparam Callback A type satisfying ValuationReadCallback. + * @param callback Callable invoked as callback(entity, variable, value). + */ + template + void readCallback(Callback const& callback) const { + for (uint64_t entity = 0; entity < size(); ++entity) { + readCallback(entity, callback); + } + } + + /*! + * Reads a single variable of the given entity and returns its value directly. + * The callback type must accept exactly the concrete type of the variable; an incorrect + * ValueType will result in a default-initialized return value. + * @tparam ValueType The expected C++ type of the variable (e.g. bool, int64_t, double). + * @param entity Entity index; must be less than size(). + * @param variable The variable to read. + * @return The current value of @p variable for @p entity. + */ + template + ValueType readValue(uint64_t entity, storm::expressions::Variable const& variable) const { + ValueType result; + readCallback(entity, variable, [&](auto, auto, ValueType value) { result = std::move(value); }); + return result; + } + + /*! + * Reads the variable values for the given entity and sets them into the given expression evaluator. + * @tparam RationalValueType The value type of rationals as stored by the evaluator (e.g. double or storm::RationalNumber). + * @param entity Entity index; must be less than size(). + * @param evaluator The expression evaluator to set the variable values into. + */ + template + void setValuesInEvaluator(uint64_t entity, storm::expressions::ExpressionEvaluator& evaluator) const; + + /*! + * Writes all variables of the given entity by invoking @p callback for each one. + * The callback receives a mutable reference to the current (or default) value and may + * overwrite it with the desired new value. + * @tparam InitializeWithCurrent If true, the reference passed to the callback is + * pre-initialized with the variable's current stored value + * instead of the type's default. + * @tparam AllowOptional If true, optional variables are exposed as std::optional& + * so the callback can leave them unset. + * @tparam AllowedTypes If non-empty, only variables with a matching natural type are passed + * to the callback; others are silently skipped. + * @tparam Callback A type satisfying ValuationWriteCallback. + * @param entity Entity index; must be less than size(). + * @param callback Callable invoked as callback(entity, variable, value). + */ + template + void writeCallback(uint64_t entity, Callback const& callback) { + for (auto const& varInfo : info(entity).variables) { + write(entity, varInfo, callback); + } + } + + /*! + * Writes a single variable of the given entity by invoking @p callback. + * @tparam InitializeWithCurrent See writeCallback(entity, callback). + * @tparam AllowOptional See writeCallback(entity, callback). + * @tparam AllowedTypes See writeCallback(entity, callback). + * @tparam Callback A type satisfying ValuationWriteCallback. + * @param entity Entity index; must be less than size(). + * @param variable The variable to write. + * @param callback Callable invoked as callback(entity, variable, value). + */ + template + void writeCallback(uint64_t entity, storm::expressions::Variable const& variable, Callback const& callback) { + write(entity, getVariableInformation(entity, variable), callback); + } + + /*! + * Writes all variables of every entity by invoking @p callback for each (entity, variable) + * pair. + * @tparam InitializeWithCurrent See writeCallback(entity, callback). + * @tparam AllowOptional See writeCallback(entity, callback). + * @tparam AllowedTypes See writeCallback(entity, callback). + * @tparam Callback A type satisfying ValuationWriteCallback. + * @param callback Callable invoked as callback(entity, variable, value). + */ + template + void writeCallback(Callback const& callback) { + for (uint64_t entity = 0; entity < size(); ++entity) { + writeCallback(entity, callback); + } + } + + /*! + * Directly writes @p value to the given variable of @p entity. + * Passing std::nullopt marks an optional variable as unset. + * Passing std::string_view is converted to std::string internally. + * @tparam ValueType The C++ type of the value to write. + * @param entity Entity index; must be less than size(). + * @param variable The variable to write. + * @param value The value to store. + */ + template + void writeValue(uint64_t entity, storm::expressions::Variable const& variable, ValueType const& value) { + if constexpr (std::is_same_v) { + writeCallback(entity, variable, [](auto, auto, auto&) { /* intentionally empty */ }); + } else if constexpr (std::is_same_v) { + writeCallback(entity, variable, [&value](auto, auto, std::string& val) { val = value; }); + } else { + writeCallback(entity, variable, [&value](auto, auto, ValueType& val) { val = value; }); + } + } + + /*! + * Computes a hash of the entire valuation data. + * Two ValuationsStorage objects with the same entities and identical variable values will produce + * the same hash. + */ + std::size_t hash() const; + + private: + uint64_t numEntities; + std::vector variableClasses; + + struct ClassData { + std::vector toClassMapping; // mapping from entity index to class index (size equals number of entities) + std::vector toValuationsMapping; // CSR mapping from entity index to valuations + }; + std::optional entityClassMappings; // present iff there are multiple classes + + std::vector valuations; + std::vector stringMapping; + std::vector strings; + + explicit ValuationsStorage(std::vector const& variableClasses); + + VariablesInformation const& info(uint64_t entity) const; + std::span getRawBytes(uint64_t entity) const; + std::span getRawBytes(uint64_t entity); + + bool readBit(std::span bytes, uint64_t position) const; + void writeBit(std::span bytes, uint64_t position, bool value) const; + uint64_t readUint64(std::span bytes, uint64_t bitOffset, uint64_t bitSize) const; + void writeUint64(std::span bytes, uint64_t bitOffset, uint64_t bitSize, uint64_t value) const; + + template + Integer readInteger(std::span bytes, uint64_t bitOffset, uint64_t bitSize) const; + + template + void writeInteger(std::span bytes, uint64_t bitOffset, uint64_t bitSize, Integer const& value) const; + + template + void writeValue(std::span bytes, uint64_t bitOffset, uint64_t bitSize, ValueType const& value); + + /*! + * Reads the given variable for the given entity and calls the callback with the read value. + * @tparam AllowedTypes either empty (allowing all types) or a list of types that are handled in the callback. + * @param entity the entity (state/choice/branch/observation index) + * @param varInfo The info for the given variable + * @param callback The callback. + */ + template + void read(uint64_t entity, VariableInformation const& varInfo, Callback const& callback) const { + auto invokeCallback = [&entity, &varInfo, &callback](auto&& value) -> bool { + using ValueType = std::remove_cvref_t; + bool constexpr IsAllowed = (sizeof...(AllowedTypes) == 0) || std::disjunction_v...>; + if constexpr (IsAllowed) { + callback(entity, varInfo.expressionVariable, std::move(value)); + } + return IsAllowed; + }; + + if (varInfo.description.isOptional.value_or(false)) { + STORM_LOG_ASSERT(varInfo.bitOffset > 0, "Invalid variable information: optional variable must have a preceding presence bit."); + if (bool const hasValue = readBit(getRawBytes(entity), varInfo.bitOffset - 1); !hasValue) { + if (invokeCallback(std::nullopt)) { + return; + } + } + } + auto const bitSize = varInfo.description.type.bitSize(); + using enum storm::umb::Type; + if (varInfo.fits64Bit) { + STORM_LOG_ASSERT(bitSize <= 64, "Invalid bit size for 64 bit fast path."); + uint64_t const rawContent = readUint64(getRawBytes(entity), varInfo.bitOffset, bitSize); + switch (varInfo.description.type.type) { + case Bool: + if (invokeCallback(rawContent != 0)) { + return; + } + break; + case Uint: + if (int64_t offset = varInfo.description.offset.value_or(0); offset < 0) { + // negative offset, output type is int64_t + if (invokeCallback(static_cast(rawContent) + offset)) { + return; + } + } else { + // non-negative offset, output type is uint64_t but we also try int64_t if uint64_t is not allowed + uint64_t const value = rawContent + offset; + uint64_t constexpr maxInt64 = std::numeric_limits::max(); + if (invokeCallback(value) || (value <= maxInt64 && invokeCallback(static_cast(value)))) { + return; + } + } + break; + case Int: { + uint64_t const mostSignificantBitMask = 1ull << (bitSize - 1); + bool const isNegative = rawContent & mostSignificantBitMask; + // For negative value, take the two's complement (e.g. 1111...1101 is -3) + int64_t const value = + isNegative ? (-static_cast(~rawContent & (mostSignificantBitMask - 1)) - 1) : static_cast(rawContent); + if (invokeCallback(value)) { + return; + } + break; + } + case Double: + if (invokeCallback(std::bit_cast(rawContent))) { + return; + } + break; + case Rational: + // Reaching this part should not be possible as varInfo.fits64Bit would be false + STORM_LOG_ASSERT(false, "Handling of rational values in 64 bit fast path is not implemented."); + break; + case String: + STORM_LOG_ASSERT(rawContent < numStrings(), "String index " << rawContent << " out of bounds (> " << numStrings() << ")."); + // Prefer the string_view callback + if (std::string_view const sv = storm::umb::stringVectorView(strings, stringMapping)[rawContent]; + invokeCallback(sv) || invokeCallback(std::string(sv))) { + return; + } + break; + default: + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, + "ValuationsStorage for variable type '" << varInfo.description.type.toString() << "' are not supported."); + } + } + // reaching this point means that we could not handle the value in the fast path + switch (varInfo.description.type.type) { + case Bool: + // Bools could be encoded with more than 64 bits (which is not reasonable, but possible..) + if (invokeCallback(readInteger(getRawBytes(entity), varInfo.bitOffset, bitSize) != Integer(0))) { + return; + } + break; + case Uint: + case Int: { + Integer value = varInfo.description.type.type == Int ? readInteger(getRawBytes(entity), varInfo.bitOffset, bitSize) + : readInteger(getRawBytes(entity), varInfo.bitOffset, bitSize); + value += storm::utility::convertNumber(varInfo.description.offset.value_or(0)); + if (invokeCallback(value)) { + return; + } + break; + } + case Double: + // Reaching this part should not be possible as varInfo.fits64Bit would be true + STORM_LOG_ASSERT(false, "double variables with more than 64 bits are not compliant."); + break; + case Rational: { + STORM_LOG_ASSERT(bitSize % 2 == 0, "Rational number bit size must be even."); + uint64_t const b = bitSize / 2; + storm::RationalNumber const numerator = readInteger(getRawBytes(entity), varInfo.bitOffset, b); + storm::RationalNumber const denominator = readInteger(getRawBytes(entity), varInfo.bitOffset + b, b); + if (invokeCallback(storm::RationalNumber(numerator / denominator))) { + return; + } + break; + } + case String: { + // Reaching this part should not be possible as varInfo.fits64Bit would be true + STORM_LOG_ASSERT(false, "String variables with more than 64 bits are not compliant."); + break; + } + default: + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, + "ValuationsStorage for variable type '" << varInfo.description.type.toString() << "' are not supported."); + } + + STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, + "Variable " << varInfo.description.name << " of type " << varInfo.description.type.toString() << " is not handled."); + } + + template + void write(uint64_t entity, VariableInformation const& varInfo, Callback const& callback) { + auto invokeCallback = [this, &entity, &varInfo, &callback]() -> bool { + bool constexpr IsAllowed = (sizeof...(AllowedTypes) == 0) || std::disjunction_v...>; + if constexpr (IsAllowed) { + ValueType value; + bool isOptional = varInfo.description.isOptional.value_or(false); + bool initializeAsUnsetOptional = false; + if constexpr (InitializeWithCurrent) { + // Initialize with current value (if requested) + read(entity, varInfo, [&value, &initializeAsUnsetOptional](auto..., auto&& currentValue) { + using CurrentVT = std::remove_cvref_t; + if constexpr (std::is_same_v) { + value = currentValue; + } else { + static_assert(std::is_same_v); + initializeAsUnsetOptional = true; + } + }); + } else { + initializeAsUnsetOptional = isOptional; + if constexpr (std::is_same_v || std::is_same_v || std::is_same_v) { + // Explicitly initialize integer values to the lower bound, 0, or the upper bound (in that order) + if (varInfo.description.lower && (!std::is_same_v || varInfo.description.lower.value() >= 0)) { + value = storm::utility::convertNumber(varInfo.description.lower.value()); + } else if (!varInfo.description.upper || varInfo.description.upper >= 0) { + value = storm::utility::zero(); + } else { + value = storm::utility::convertNumber(varInfo.description.upper.value()); + } + } + } + // Invoke the callback. Determine if we need to write a value and ensure that `value` holds the value to write. + bool haveToWriteValue = false; + if (isOptional) { + if constexpr (AllowOptional) { + std::optional optionalValue = initializeAsUnsetOptional ? std::optional() : value; + callback(entity, varInfo.expressionVariable, optionalValue); + if (optionalValue.has_value()) { + value = std::move(optionalValue.value()); + haveToWriteValue = true; + } + STORM_LOG_ASSERT(varInfo.bitOffset > 0, "Invalid variable information: optional variable must have a preceding presence bit."); + writeBit(getRawBytes(entity), varInfo.bitOffset - 1, optionalValue.has_value()); + } else { + STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, + "Writing to optional variable " << varInfo.description.name << " was not expected."); + } + } else { + callback(entity, varInfo.expressionVariable, value); + haveToWriteValue = true; + } + if (haveToWriteValue) { + // Check bounds and apply the offset for integer variables + if constexpr (std::is_same_v || std::is_same_v || std::is_same_v) { + if constexpr (std::is_same_v || std::is_same_v) { + STORM_LOG_THROW(!varInfo.description.lower || std::cmp_greater_equal(value, varInfo.description.lower.value()), + storm::exceptions::OutOfRangeException, + "Value " << value << " is out of range for variable " << varInfo.description.name + << ": value is smaller than lower bound " << varInfo.description.lower.value() << "."); + STORM_LOG_THROW(!varInfo.description.upper || std::cmp_less_equal(value, varInfo.description.upper.value()), + storm::exceptions::OutOfRangeException, + "Value " << value << " is out of range for variable " << varInfo.description.name + << ": value is greater than upper bound " << varInfo.description.upper.value() << "."); + } else { + if (varInfo.description.lower) { + STORM_LOG_THROW(value >= storm::utility::convertNumber(varInfo.description.lower.value()), + storm::exceptions::OutOfRangeException, + "Value " << value << " is out of range for variable " << varInfo.description.name + << ": value is smaller than lower bound " << varInfo.description.lower.value() << "."); + } + if (varInfo.description.upper) { + STORM_LOG_THROW(value <= storm::utility::convertNumber(varInfo.description.upper.value()), + storm::exceptions::OutOfRangeException, + "Value " << value << " is out of range for variable " << varInfo.description.name + << ": value is greater than upper bound " << varInfo.description.upper.value() << "."); + } + } + if (auto offset = varInfo.description.offset.value_or(0); offset != 0) { + if constexpr (std::is_same_v) { + STORM_LOG_ASSERT(std::cmp_greater_equal(value, offset), + "Set negative value " << value << "-" << offset << " to unsigned variable."); + value -= offset; + } else { + value -= storm::utility::convertNumber(offset); + } + } + } + // Write the value + writeValue(getRawBytes(entity), varInfo.bitOffset, varInfo.description.type.bitSize(), value); + } + } + return IsAllowed; + }; + + using enum storm::umb::Type; + switch (varInfo.description.type.type) { + case Bool: + if (invokeCallback.template operator()()) { + return; + } + break; + case Uint: + if (varInfo.fits64Bit) { + if (varInfo.description.offset.value_or(0) >= 0) { + // non-negative offset, default output type is uint64_t + if (invokeCallback.template operator()()) { + return; + } + } + // take int64_t if uint64_t is not allowed or we have a negative offset + if (invokeCallback.template operator()()) { + return; + } + } + // finally take Integer if the 64 bit types are not allowed or insufficient + if (invokeCallback.template operator()()) { + return; + } + break; + case Int: + // Prefer int64_t if it fits and is allowed. + if ((varInfo.fits64Bit && invokeCallback.template operator()()) || invokeCallback.template operator()()) { + return; + } + break; + case Double: + if (invokeCallback.template operator()()) { + return; + } + break; + case Rational: + if (invokeCallback.template operator()()) { + return; + } + break; + case String: + if (invokeCallback.template operator()()) { + return; + } + break; + default: + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, + "ValuationsStorage for variable type '" << varInfo.description.type.toString() << "' are not supported."); + } + STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, + "Variable " << varInfo.description.name << " of type " << varInfo.description.type.toString() << " is not handled."); + } +}; +} // namespace storm::storage::sparse diff --git a/src/storm/transformer/MakePOMDPCanonic.cpp b/src/storm/transformer/MakePOMDPCanonic.cpp index 3050b0136f..008c41c905 100644 --- a/src/storm/transformer/MakePOMDPCanonic.cpp +++ b/src/storm/transformer/MakePOMDPCanonic.cpp @@ -151,7 +151,7 @@ std::shared_ptr> MakePOMDPCanonic std::string MakePOMDPCanonic::getStateInformation(uint64_t state) const { if (pomdp.hasStateValuations()) { - return std::to_string(state) + " " + pomdp.getStateValuations().getStateInfo(state); + return std::to_string(state) + " " + pomdp.getStateValuations().toString(state); } else { return std::to_string(state); } @@ -160,7 +160,7 @@ std::string MakePOMDPCanonic::getStateInformation(uint64_t state) con template std::string MakePOMDPCanonic::getObservationInformation(uint32_t obs) const { if (pomdp.hasObservationValuations()) { - return std::to_string(obs) + " " + pomdp.getObservationValuations().getStateInfo(obs); + return std::to_string(obs) + " " + pomdp.getObservationValuations().toString(obs); } else { return std::to_string(obs); } diff --git a/src/storm/transformer/SubsystemBuilder.cpp b/src/storm/transformer/SubsystemBuilder.cpp index c19983994e..a13a592379 100644 --- a/src/storm/transformer/SubsystemBuilder.cpp +++ b/src/storm/transformer/SubsystemBuilder.cpp @@ -150,7 +150,7 @@ SubsystemBuilderReturnType internalBuildSubsystem(st components.choiceLabeling = originalModel.getChoiceLabeling().getSubLabeling(keptActions); } if (originalModel.hasStateValuations()) { - components.stateValuations = originalModel.getStateValuations().selectStates(subsystemStates); + components.stateValuations = originalModel.getStateValuations().selectEntities(subsystemStates); } if (originalModel.hasChoiceOrigins()) { components.choiceOrigins = originalModel.getChoiceOrigins()->selectChoices(keptActions); diff --git a/src/storm/utility/constants.cpp b/src/storm/utility/constants.cpp index 602960f572..018bc609f2 100644 --- a/src/storm/utility/constants.cpp +++ b/src/storm/utility/constants.cpp @@ -423,6 +423,11 @@ ClnRationalNumber convertNumber(uint_fast64_t const& number) { return carl::rationalize(static_cast(number)); } +template<> +int64_t convertNumber(NumberTraits::IntegerType const& number) { + return carl::toInt(number); +} + template<> typename NumberTraits::IntegerType convertNumber(uint_fast64_t const& number) { STORM_LOG_ASSERT(static_cast(number) == number, "Conversion failed, because the number is too large."); @@ -648,6 +653,11 @@ GmpRationalNumber convertNumber(NumberTraits::IntegerType con return GmpRationalNumber(number); } +template<> +int64_t convertNumber(NumberTraits::IntegerType const& number) { + return carl::toInt(number); +} + template<> typename NumberTraits::IntegerType convertNumber(uint_fast64_t const& number) { STORM_LOG_ASSERT(static_cast(number) == number, "Conversion failed, because the number is too large."); @@ -1228,6 +1238,11 @@ template bool isBetween(storm::storage::sparse::state_type const& a, storm::stor bool strict); template uint64_t bitsize(storm::storage::sparse::state_type const& number); +// int64_t +template int64_t zero(); +template int64_t one(); +template int64_t convertNumber(int64_t const&); + // other instantiations template unsigned long convertNumber(long const&); template double convertNumber(long const&); @@ -1237,6 +1252,7 @@ template double convertNumber(long const&); template storm::ClnRationalNumber one(); template NumberTraits::IntegerType one(); template storm::ClnRationalNumber zero(); +template NumberTraits::IntegerType zero(); template bool isZero(NumberTraits::IntegerType const& value); template bool isConstant(storm::ClnRationalNumber const& value); template bool isPositive(storm::ClnRationalNumber const& value); @@ -1268,6 +1284,7 @@ template uint64_t bitsize(storm::ClnIntegerNumber const& number); template storm::GmpRationalNumber one(); template NumberTraits::IntegerType one(); template storm::GmpRationalNumber zero(); +template NumberTraits::IntegerType zero(); template bool isZero(NumberTraits::IntegerType const& value); template bool isConstant(storm::GmpRationalNumber const& value); template bool isPositive(storm::GmpRationalNumber const& value); diff --git a/src/test/storm/storage/StateValuationTest.cpp b/src/test/storm/storage/StateValuationTest.cpp deleted file mode 100644 index 134b9ebcca..0000000000 --- a/src/test/storm/storage/StateValuationTest.cpp +++ /dev/null @@ -1,79 +0,0 @@ -#include "storm-config.h" -#include "test/storm_gtest.h" - -#include "storm-parsers/parser/PrismParser.h" -#include "storm/builder/ExplicitModelBuilder.h" -#include "storm/exceptions/WrongFormatException.h" -#include "storm/generator/PrismNextStateGenerator.h" -#include "storm/models/sparse/MarkovAutomaton.h" -#include "storm/models/sparse/StandardRewardModel.h" -#include "storm/storage/expressions/ExpressionManager.h" -#include "storm/storage/sparse/StateValuationTransformer.h" - -class StateValuationTest : public ::testing::Test { - protected: - void SetUp() override { -#ifndef STORM_HAVE_Z3 - GTEST_SKIP() << "Z3 not available."; -#endif - } -}; - -TEST_F(StateValuationTest, StateValuationConstruction) { - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/die.pm"); - storm::generator::NextStateGeneratorOptions generatorOptions; - generatorOptions.setBuildStateValuations(); - auto builder = storm::builder::ExplicitModelBuilder(program, generatorOptions); - std::shared_ptr> model = builder.build(); - ASSERT_TRUE(model->hasStateValuations()); - auto const& sv = model->getStateValuations(); - ASSERT_EQ(sv.getNumberOfStates(), model->getNumberOfStates()); - auto val = sv.at(0).begin(); - ASSERT_EQ(val.getName(), "s"); - val.operator++(); - ASSERT_EQ(val.getName(), "d"); - val.operator++(); - ASSERT_TRUE(val == sv.at(0).end()); -} - -TEST_F(StateValuationTest, StateValuationTransformation) { - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/die.pm"); - storm::generator::NextStateGeneratorOptions generatorOptions; - generatorOptions.setBuildStateValuations(); - auto builder = storm::builder::ExplicitModelBuilder(program, generatorOptions); - std::shared_ptr> model = builder.build(); - ASSERT_TRUE(model->hasStateValuations()); - auto const& sv = model->getStateValuations(); - - storm::storage::sparse::StateValuationTransformer notransformer(sv); - auto newsv = notransformer.build(true); - ASSERT_EQ(newsv.getNumberOfStates(), sv.getNumberOfStates()); - storm::storage::sparse::StateValuationTransformer transformer(sv); - auto svar = program.getManager().getVariable("s"); - auto dvar = program.getManager().getVariable("d"); - auto sgt3Var = program.getManager().declareBooleanVariable("sGT3"); - auto alwaysTrueVar = program.getManager().declareBooleanVariable("alwaysTrue"); - auto alwaysFalseVar = program.getManager().declareBooleanVariable("alwaysFalse"); - transformer.addBooleanExpression(sgt3Var, svar.getExpression() > program.getManager().integer(3)); - transformer.addBooleanExpression(alwaysTrueVar, svar.getExpression() == svar.getExpression()); - transformer.addBooleanExpression(alwaysFalseVar, dvar.getExpression() < dvar.getExpression()); - newsv = transformer.build(true); - auto val = newsv.at(0).begin(); - ASSERT_EQ(val.getName(), "sGT3"); - val.operator++(); - ASSERT_EQ(val.getName(), "alwaysTrue"); - val.operator++(); - ASSERT_EQ(val.getName(), "alwaysFalse"); - val.operator++(); - ASSERT_EQ(val.getName(), "s"); - val.operator++(); - ASSERT_EQ(val.getName(), "d"); - val.operator++(); - ASSERT_TRUE(val == newsv.at(0).end()); - for (uint64_t state = 0; state < newsv.getNumberOfStates(); ++state) { - ASSERT_TRUE(newsv.getBooleanValue(state, alwaysTrueVar)); - ASSERT_FALSE(newsv.getBooleanValue(state, alwaysFalseVar)); - ASSERT_EQ(sv.getIntegerValue(state, svar), newsv.getIntegerValue(state, svar)); - ASSERT_EQ(newsv.getBooleanValue(state, sgt3Var), newsv.getIntegerValue(state, svar) > 3); - } -} diff --git a/src/test/storm/storage/UmbTest.cpp b/src/test/storm/storage/UmbTest.cpp index 4ea6d72a5b..2309ac2876 100644 --- a/src/test/storm/storage/UmbTest.cpp +++ b/src/test/storm/storage/UmbTest.cpp @@ -9,12 +9,14 @@ #include "storm/adapters/IntervalAdapter.h" #include "storm/adapters/RationalNumberAdapter.h" #include "storm/builder/ExplicitModelBuilder.h" +#include "storm/models/sparse/Pomdp.h" #include "storm/storage/umb/export/SparseModelToUmb.h" #include "storm/storage/umb/export/UmbExport.h" #include "storm/storage/umb/import/SparseModelFromUmb.h" #include "storm/storage/umb/import/UmbImport.h" #include "storm/storage/umb/model/UmbModel.h" #include "storm/storage/umb/model/ValueEncoding.h" +#include "storm/storage/valuations/ValuationsStorage.h" #include "storm/utility/constants.h" #include "test/storm_gtest.h" /*! @@ -53,7 +55,8 @@ class UmbRoundTripTest : public ::testing::Test { generatorOptions.setBuildChoiceOrigins(exportOptions.allowChoiceOriginsAsActions); generatorOptions.setBuildAllRewardModels(); generatorOptions.setBuildAllLabels(); - // TODO: valuations + generatorOptions.setBuildStateValuations(true); + generatorOptions.setBuildObservationValuations(true); // build model from prism file storm::prism::Program program = storm::parser::PrismParser::parse(prismfile, true); @@ -93,6 +96,33 @@ class UmbRoundTripTest : public ::testing::Test { EXPECT_EQ(rewardModel.getTransitionRewardMatrix(), otherRewardModel.getTransitionRewardMatrix()); } } + auto assertEqualValuations = [](auto const& v, auto const& other_v) { + ASSERT_EQ(v.size(), other_v.size()); + EXPECT_EQ(0, v.numStrings()); + EXPECT_EQ(0, other_v.numStrings()); + ASSERT_EQ(1, v.numClasses()); + ASSERT_EQ(1, other_v.numClasses()); + ASSERT_EQ(v.getClassDescription().sizeInBits(), other_v.getClassDescription().sizeInBits()); + storm::umb::UmbModel::Valuation data = v.getRawUmbData(); + storm::umb::UmbModel::Valuation other_data = other_v.getRawUmbData(); + EXPECT_EQ(data.valuations, other_data.valuations); + EXPECT_EQ(data.stringMapping, other_data.stringMapping); + EXPECT_EQ(data.strings == other_data.strings, true); + EXPECT_EQ(data.valuationToClass, other_data.valuationToClass); + }; + ASSERT_TRUE(model->hasStateValuations()); + ASSERT_TRUE(otherModelPtr->hasStateValuations()); + assertEqualValuations(model->getStateValuations().getStorage(), otherModelPtr->getStateValuations().getStorage()); + // POMDP specific things + if (model->isPartiallyObservable()) { + ASSERT_TRUE(model->isOfType(storm::models::ModelType::Pomdp)); + auto pomdp = model->template as>(); + auto otherPomdp = otherModelPtr->template as>(); + EXPECT_EQ(pomdp->getObservations(), otherPomdp->getObservations()); + ASSERT_TRUE(pomdp->hasObservationValuations()); + ASSERT_TRUE(otherPomdp->hasObservationValuations()); + assertEqualValuations(pomdp->getObservationValuations().getStorage(), otherPomdp->getObservationValuations().getStorage()); + } }; // Short round trip: model -> umb -> model diff --git a/src/test/storm/storage/ValuationsTest.cpp b/src/test/storm/storage/ValuationsTest.cpp new file mode 100644 index 0000000000..8c61972404 --- /dev/null +++ b/src/test/storm/storage/ValuationsTest.cpp @@ -0,0 +1,394 @@ +#include "storm-config.h" +#include "test/storm_gtest.h" + +#include "storm-parsers/parser/PrismParser.h" +#include "storm/adapters/JsonAdapter.h" +#include "storm/builder/ExplicitModelBuilder.h" +#include "storm/generator/PrismNextStateGenerator.h" +#include "storm/storage/expressions/ExpressionManager.h" +#include "storm/storage/sparse/ValuationTransformer.h" +#include "storm/storage/valuations/ValuationDescriptionBuilder.h" +#include "storm/storage/valuations/Valuations.h" +#include "storm/storage/valuations/ValuationsStorage.h" + +TEST(ValuationTest, StateValuationConstruction) { +#ifndef STORM_HAVE_Z3 + GTEST_SKIP() << "Z3 not available."; +#endif + storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/die.pm"); + storm::generator::NextStateGeneratorOptions generatorOptions; + generatorOptions.setBuildStateValuations(); + generatorOptions.setBuildAllLabels(); + auto builder = storm::builder::ExplicitModelBuilder(program, generatorOptions); + std::shared_ptr> model = builder.build(); + ASSERT_TRUE(model->hasStateValuations()); + auto const& sv = model->getStateValuations(); + ASSERT_EQ(sv.getNumberOfEntities(), model->getNumberOfStates()); + ASSERT_TRUE(sv.getManager().hasVariable("s")); + ASSERT_TRUE(sv.getManager().hasVariable("d")); + auto const s = sv.getManager().getVariable("s"); + auto const d = sv.getManager().getVariable("d"); + auto const vars = sv.getAllVariables(); + ASSERT_EQ(2, vars.size()); + ASSERT_TRUE(vars.contains(s)); + ASSERT_TRUE(vars.contains(d)); + // reading values at sinit + uint64_t const sinit = *model->getInitialStates().begin(); + ASSERT_TRUE(sv.entityHasVariable(sinit, s)); + ASSERT_TRUE(sv.entityHasVariable(sinit, d)); + EXPECT_EQ(0, sv.getInt64Value(sinit, s)); + EXPECT_EQ(0, sv.getOptionalInt64Value(sinit, s).value()); + EXPECT_EQ(0, sv.getOptionalInt64Value(sinit, d).value()); + // reading json at sinit + auto js = sv.toJson(sinit); + EXPECT_EQ(2, js.size()); + EXPECT_TRUE(js.contains("s")); + EXPECT_TRUE(js.contains("d")); + EXPECT_EQ(0, js["s"].get()); + EXPECT_EQ(0, js["d"].get()); + // reading values at "three" state + ASSERT_TRUE(model->getStateLabeling().containsLabel("three")); + ASSERT_TRUE(model->getStates("three").hasUniqueSetBit()); + uint64_t const three = *model->getStates("three").begin(); + EXPECT_EQ(7, sv.getInt64Value(three, s)); + EXPECT_EQ(3, sv.getInt64Value(three, d)); + // reading all values for d + auto dValues = sv.getInt64Values(d); + ASSERT_EQ(sv.getNumberOfEntities(), dValues.size()); + EXPECT_EQ(3, dValues[three]); + int64_t const sum = std::accumulate(dValues.begin(), dValues.end(), 0ll); + EXPECT_EQ(1 + 2 + 3 + 4 + 5 + 6, sum); +} + +TEST(ValuationTest, StateValuationTransformation) { +#ifndef STORM_HAVE_Z3 + GTEST_SKIP() << "Z3 not available."; +#endif + storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/die.pm"); + storm::generator::NextStateGeneratorOptions generatorOptions; + generatorOptions.setBuildStateValuations(); + auto builder = storm::builder::ExplicitModelBuilder(program, generatorOptions); + std::shared_ptr> model = builder.build(); + ASSERT_TRUE(model->hasStateValuations()); + auto const& sv = model->getStateValuations(); + storm::storage::sparse::ValuationTransformer notransformer(sv); + auto newsv = notransformer.build(true); + ASSERT_EQ(newsv.getNumberOfEntities(), sv.getNumberOfEntities()); + storm::storage::sparse::ValuationTransformer transformer(sv); + auto const svar = program.getManager().getVariable("s"); + auto const dvar = program.getManager().getVariable("d"); + auto const sgt3Var = program.getManager().declareBooleanVariable("sGT3"); + auto const alwaysTrueVar = program.getManager().declareBooleanVariable("alwaysTrue"); + auto const alwaysFalseVar = program.getManager().declareBooleanVariable("alwaysFalse"); + transformer.addExpression(sgt3Var, svar.getExpression() > program.getManager().integer(3)); + transformer.addExpression(alwaysTrueVar, svar.getExpression() == svar.getExpression()); + transformer.addExpression(alwaysFalseVar, dvar.getExpression() < dvar.getExpression()); + newsv = transformer.build(true); + auto const vars = newsv.getAllVariables(); + ASSERT_EQ(5, vars.size()); + ASSERT_TRUE(vars.contains(svar)); + ASSERT_TRUE(vars.contains(dvar)); + ASSERT_TRUE(vars.contains(sgt3Var)); + ASSERT_TRUE(vars.contains(alwaysTrueVar)); + ASSERT_TRUE(vars.contains(alwaysFalseVar)); + uint64_t const sinit = *model->getInitialStates().begin(); + EXPECT_EQ(0, newsv.getInt64Value(sinit, svar)); + EXPECT_EQ(0, newsv.getInt64Value(sinit, dvar)); + EXPECT_FALSE(newsv.getBooleanValue(sinit, sgt3Var)); + EXPECT_TRUE(newsv.getBooleanValue(sinit, alwaysTrueVar)); + EXPECT_FALSE(newsv.getBooleanValue(sinit, alwaysFalseVar)); + + for (uint64_t state = 0; state < newsv.getNumberOfEntities(); ++state) { + ASSERT_TRUE(newsv.getBooleanValue(state, alwaysTrueVar)); + ASSERT_FALSE(newsv.getBooleanValue(state, alwaysFalseVar)); + ASSERT_EQ(sv.getInt64Value(state, svar), newsv.getInt64Value(state, svar)); + ASSERT_EQ(newsv.getBooleanValue(state, sgt3Var), newsv.getInt64Value(state, svar) > 3); + } +} + +TEST(ValuationTest, Valuations2classes) { + auto manager = std::make_shared(); + auto const b = manager->declareBooleanVariable("b"); + auto const i = manager->declareIntegerVariable("i"); + auto const s = manager->declareStringVariable("s"); + auto const r = manager->declareRationalVariable("r"); + std::vector classes; + { + storm::storage::sparse::ValuationDescriptionBuilder builder1(manager); + builder1.addBooleanVariable(b, true); // 1 + 1 bit (optional + builder1.addIntegerVariable(i, -4, 12); // 17 different values, therefore 5 bits + builder1.addStringVariable(s, true); // 64 + 1 bits (optional) + builder1.addRationalVariable(r, 166); // 166 bits + classes.push_back(builder1.buildClassDescription()); // adds 2 padding bits to fill a whole number of bytes + EXPECT_EQ(2 + 5 + 65 + 166 + 2, classes.back().sizeInBits()); + EXPECT_TRUE(classes.back().hasStringVariable()); + + storm::storage::sparse::ValuationDescriptionBuilder builder2(manager); + builder2.addDoubleVariable(r); // 64 bits + builder2.addBooleanVariable(b); // 1 bit + builder2.addIntegerVariable(i, -10, -7); // 4 different values, therefore 2 bits + classes.push_back(builder2.buildClassDescription()); // adds 5 padding bits to fill a whole number of bytes + EXPECT_EQ(64 + 1 + 2 + 5, classes.back().sizeInBits()); + EXPECT_FALSE(classes.back().hasStringVariable()); + } + storm::storage::sparse::ValuationsStorage valuations(classes, {manager, manager}); + EXPECT_EQ(0, valuations.numStrings()); + EXPECT_EQ(2, valuations.numClasses()); + EXPECT_EQ(classes[0].sizeInBits(), valuations.getClassDescription(0).sizeInBits()); + EXPECT_EQ(classes[1].sizeInBits(), valuations.getClassDescription(1).sizeInBits()); + auto const vars = valuations.getAllVariables(); + EXPECT_EQ(4, vars.size()); + EXPECT_TRUE(vars.contains(b)); + EXPECT_TRUE(vars.contains(i)); + EXPECT_TRUE(vars.contains(s)); + EXPECT_TRUE(vars.contains(r)); + // Insert 200 entities with alternating classes and some non-trivial values + std::vector> b_values; + std::vector i_values; + std::vector> s_values; + std::vector r_values; + for (uint64_t e = 0; e < 200; ++e) { + if (e % 3 == 0) { + // insert class 0 + valuations.emplaceBack(0, [&](auto entity, auto const& var, auto& value) { + using ValueType = std::remove_cvref_t; + if constexpr (std::is_same_v>) { + EXPECT_EQ(b, var); + if (entity % 2 == 0) { + value = entity % 4 == 0; + } + b_values.push_back(value); + } else if constexpr (std::is_same_v) { + EXPECT_EQ(i, var); + value = static_cast(entity) % 17 - 4; + i_values.push_back(value); + } else if constexpr (std::is_same_v>) { + EXPECT_EQ(s, var); + if (entity % 2 == 1) { + value = "str" + std::to_string(entity); + } + s_values.push_back(value); + } else if constexpr (std::is_same_v) { + EXPECT_EQ(r, var); + auto const uint64max = storm::utility::convertNumber(std::numeric_limits::max()); + value = (uint64max + uint64max + storm::utility::convertNumber(entity)) / (uint64max); + if (entity % 8 == 0) { + value = -value; + } + r_values.push_back(value); + } else { + FAIL() << "Unexpected variable type " << typeid(ValueType).name() << " for variable " << var.getName(); + } + }); + } else { + // insert class 1 + valuations.emplaceBack(1, [&](auto entity, auto const& var, auto& value) { + using ValueType = std::remove_cvref_t; + if constexpr (std::is_same_v) { + EXPECT_EQ(r, var); + value = static_cast(entity) / 3.0; + r_values.push_back(storm::utility::convertNumber(value)); + } else if constexpr (std::is_same_v) { + EXPECT_EQ(b, var); + value = entity % 2 == 0; + b_values.push_back(value); + } else { + static_assert(std::is_same_v); + EXPECT_EQ(i, var); + value = static_cast(entity) % 4 - 10; + i_values.push_back(value); + } + }); + s_values.push_back(std::nullopt); + } + } + // Now check if reading back the values works correctly. + ASSERT_EQ(200, b_values.size()); + ASSERT_EQ(200, i_values.size()); + ASSERT_EQ(200, s_values.size()); + ASSERT_EQ(200, r_values.size()); + valuations.readCallback([&](auto entity, auto const& var, auto const& value) { + using ValueType = std::remove_cvref_t; + if constexpr (std::is_same_v) { + EXPECT_EQ(0, valuations.getClassOfEntity(entity)); + if (var == b) { + EXPECT_FALSE(b_values[entity].has_value()); + } else { + EXPECT_TRUE(var == s); + EXPECT_FALSE(s_values[entity].has_value()); + } + } else if constexpr (std::is_same_v) { + EXPECT_EQ(b, var); + ASSERT_TRUE(b_values[entity].has_value()); + EXPECT_EQ(b_values[entity].value(), value); + } else if constexpr (std::is_same_v) { + EXPECT_EQ(i, var); + EXPECT_EQ(i_values[entity], value); + } else if constexpr (std::is_same_v) { + EXPECT_EQ(s, var); + ASSERT_TRUE(s_values[entity].has_value()); + EXPECT_EQ(s_values[entity].value(), value); + } else if constexpr (std::is_same_v) { + EXPECT_EQ(0, valuations.getClassOfEntity(entity)); + EXPECT_EQ(r, var); + EXPECT_EQ(r_values[entity], value); + } else { + static_assert(std::is_same_v); + EXPECT_EQ(1, valuations.getClassOfEntity(entity)); + EXPECT_EQ(r, var); + EXPECT_EQ(storm::utility::convertNumber(r_values[entity]), storm::utility::convertNumber(value)); + } + }); +} + +TEST(ValuationTest, ValuationsSingleClass) { + // Tests point-access via readValue / writeValue, entityHasVariable, getAllVariables, and resize + // on a simple single-class layout with non-optional variables only. + auto manager = std::make_shared(); + auto const b = manager->declareBooleanVariable("b"); + auto const i = manager->declareIntegerVariable("i"); + auto const d = manager->declareRationalVariable("d"); + + storm::storage::sparse::ValuationDescriptionBuilder builder(manager); + builder.addBooleanVariable(b); // 1 bit + builder.addIntegerVariable(i, -5, 5); // 11 values → 4 bits + builder.addDoubleVariable(d); // 64 bits + auto const desc = builder.buildClassDescription(); + EXPECT_EQ(1 + 4 + 64 + 3, desc.sizeInBits()); + + storm::storage::sparse::ValuationsStorage valuations(desc, manager); + EXPECT_EQ(0u, valuations.size()); + EXPECT_EQ(1u, valuations.numClasses()); + + // getAllVariables should list exactly the three declared variables + auto const vars = valuations.getAllVariables(); + EXPECT_EQ(3u, vars.size()); + EXPECT_TRUE(vars.contains(b)); + EXPECT_TRUE(vars.contains(i)); + EXPECT_TRUE(vars.contains(d)); + + // Insert 6 entities with distinct, easily checkable values + std::vector bVals = {true, false, true, false, true, false}; + std::vector iVals = {-5, -3, 0, 2, 4, 5}; + std::vector dVals = {0.0, 1.5, -2.25, 1e10, -1e-5, 3.14}; + + for (uint64_t e = 0; e < 6; ++e) { + valuations.emplaceBack([&](auto entity, auto const& var, auto& value) { + using ValueType = std::remove_cvref_t; + if constexpr (std::is_same_v) { + value = bVals[entity]; + } else if constexpr (std::is_same_v) { + value = iVals[entity]; + } else { + static_assert(std::is_same_v); + value = dVals[entity]; + } + }); + } + ASSERT_EQ(6u, valuations.size()); + + // entityHasVariable: all variables belong to the single class, so always true + for (uint64_t e = 0; e < 6; ++e) { + EXPECT_TRUE(valuations.entityHasVariable(e, b)); + EXPECT_TRUE(valuations.entityHasVariable(e, i)); + EXPECT_TRUE(valuations.entityHasVariable(e, d)); + } + + // readValue round-trips + for (uint64_t e = 0; e < 6; ++e) { + EXPECT_EQ(bVals[e], valuations.readValue(e, b)) << " at entity " << e; + EXPECT_EQ(iVals[e], valuations.readValue(e, i)) << " at entity " << e; + EXPECT_EQ(dVals[e], valuations.readValue(e, d)) << " at entity " << e; + } + + // writeValue then readValue: overwrite entity 3 and verify neighbours are unaffected + valuations.writeValue(3, b, true); + valuations.writeValue(3, i, int64_t(-1)); + valuations.writeValue(3, d, 99.0); + EXPECT_EQ(true, valuations.readValue(3, b)); + EXPECT_EQ(-1, valuations.readValue(3, i)); + EXPECT_EQ(99.0, valuations.readValue(3, d)); + // neighbours untouched + EXPECT_EQ(bVals[2], valuations.readValue(2, b)); + EXPECT_EQ(iVals[4], valuations.readValue(4, i)); + + // resize: grow to 9 — new entities get default values and the first 6 stay intact + valuations.resize(9); + ASSERT_EQ(9u, valuations.size()); + for (uint64_t e = 0; e < 6; ++e) { + if (e == 3) + continue; // entity 3 was overwritten above + EXPECT_EQ(bVals[e], valuations.readValue(e, b)) << " at entity " << e; + EXPECT_EQ(iVals[e], valuations.readValue(e, i)) << " at entity " << e; + EXPECT_EQ(dVals[e], valuations.readValue(e, d)) << " at entity " << e; + } + + // resize: shrink back to 4 + valuations.resize(4); + EXPECT_EQ(4u, valuations.size()); + EXPECT_EQ(bVals[0], valuations.readValue(0, b)); + EXPECT_EQ(iVals[1], valuations.readValue(1, i)); + EXPECT_EQ(dVals[2], valuations.readValue(2, d)); +} + +TEST(ValuationTest, ValuationsSelectEntities) { + // Tests selectEntities (BitVector and vector overloads) on a single-class + // layout. Verifies that the selection preserves values in the correct order and that the + // original Valuations object is left unchanged. + auto manager = std::make_shared(); + auto const b = manager->declareBooleanVariable("b"); + auto const i = manager->declareIntegerVariable("i"); + + storm::storage::sparse::ValuationDescriptionBuilder builder(manager); + builder.addBooleanVariable(b); // 1 bit + builder.addIntegerVariable(i, 0, 7); // 8 values → 3 bits + auto const desc = builder.buildClassDescription(); + + storm::storage::sparse::ValuationsStorage valuations(desc, manager); + + // Insert 8 entities: b = (entity % 2 == 0), i = entity + for (uint64_t e = 0; e < 8; ++e) { + valuations.emplaceBack([e](auto /*entity*/, auto const& var, auto& value) { + using ValueType = std::remove_cvref_t; + if constexpr (std::is_same_v) { + value = (e % 2 == 0); + } else { + static_assert(std::is_same_v); + value = static_cast(e); + } + }); + } + ASSERT_EQ(8u, valuations.size()); + + // --- BitVector selection: pick entities 1, 3, 5, 7 (odd indices) --- + storm::storage::BitVector bvOdd(8, false); + for (uint64_t e = 1; e < 8; e += 2) { + bvOdd.set(e); + } + auto const selectedBv = valuations.selectEntities(bvOdd); + ASSERT_EQ(4u, selectedBv.size()); + EXPECT_EQ(1u, selectedBv.numClasses()); + for (uint64_t sel = 0; sel < 4; ++sel) { + uint64_t const origEntity = 2 * sel + 1; // 1, 3, 5, 7 + EXPECT_EQ(false, selectedBv.readValue(sel, b)) << " selected entity " << sel; + EXPECT_EQ(static_cast(origEntity), selectedBv.readValue(sel, i)) << " selected entity " << sel; + } + + // --- vector selection: pick entities {6, 0, 4} in that order --- + std::vector const indices = {6, 0, 4}; + auto const selectedVec = valuations.selectEntities(indices); + ASSERT_EQ(3u, selectedVec.size()); + EXPECT_EQ(true, selectedVec.readValue(0, b)); // entity 6: even → true + EXPECT_EQ(6, selectedVec.readValue(0, i)); + EXPECT_EQ(true, selectedVec.readValue(1, b)); // entity 0: even → true + EXPECT_EQ(0, selectedVec.readValue(1, i)); + EXPECT_EQ(true, selectedVec.readValue(2, b)); // entity 4: even → true + EXPECT_EQ(4, selectedVec.readValue(2, i)); + + // Original must be unchanged + ASSERT_EQ(8u, valuations.size()); + for (uint64_t e = 0; e < 8; ++e) { + EXPECT_EQ(e % 2 == 0, valuations.readValue(e, b)) << " at original entity " << e; + EXPECT_EQ(static_cast(e), valuations.readValue(e, i)) << " at original entity " << e; + } +} \ No newline at end of file