ValuationsStorage.h

Go to the documentation of this file.

#pragma once
 
#include <bit>
#include <concepts>
#include <cstdint>
#include <memory>
#include <optional>
#include <set>
#include <span>
#include <sstream>
#include <typeinfo>
 
#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<typename T>
class ExpressionEvaluator;
}
 
namespace storm::storage::sparse {

template<typename F>
concept ValuationReadCallback =
    std::invocable<F, uint64_t, storm::expressions::Variable const&, bool> || std::invocable<F, uint64_t, storm::expressions::Variable const&, int64_t> ||
    std::invocable<F, uint64_t, storm::expressions::Variable const&, uint64_t> || std::invocable<F, uint64_t, storm::expressions::Variable const&, double> ||
    std::invocable<F, uint64_t, storm::expressions::Variable const&, storm::RationalNumber> ||
    std::invocable<F, uint64_t, storm::expressions::Variable const&, storm::NumberTraits<storm::RationalNumber>::IntegerType> ||
    std::invocable<F, uint64_t, storm::expressions::Variable const&, std::string_view> ||
    std::invocable<F, uint64_t, storm::expressions::Variable const&, std::string> ||
    std::invocable<F, uint64_t, storm::expressions::Variable const&, std::nullopt_t>;

template<typename F>
concept ValuationWriteCallback =
    std::invocable<F, uint64_t, storm::expressions::Variable const&, bool&> || std::invocable<F, uint64_t, storm::expressions::Variable const&, int64_t&> ||
    std::invocable<F, uint64_t, storm::expressions::Variable const&, uint64_t&> || std::invocable<F, uint64_t, storm::expressions::Variable const&, double&> ||
    std::invocable<F, uint64_t, storm::expressions::Variable const&, storm::RationalNumber&> ||
    std::invocable<F, uint64_t, storm::expressions::Variable const&, storm::NumberTraits<storm::RationalNumber>::IntegerType&> ||
    std::invocable<F, uint64_t, storm::expressions::Variable const&, std::string&>;

class ValuationsStorage {
   public:
    using Integer = storm::NumberTraits<storm::RationalNumber>::IntegerType;

    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<VariableInformation> const variables;
        std::shared_ptr<storm::expressions::ExpressionManager const> const expressionManager;
        uint64_t const sizeInBytes;
    };
 
    ValuationsStorage(ValuationsStorage const&) = default;
    ValuationsStorage(ValuationsStorage&&) = default;
    ValuationsStorage& operator=(ValuationsStorage const&) = default;
    ValuationsStorage& operator=(ValuationsStorage&&) = default;

    ValuationsStorage(uint64_t numEntities, std::vector<ValuationClassDescription> const& descriptions, std::vector<char> valuations,
                      std::vector<uint64_t> stringMapping, std::vector<char> strings, std::optional<std::vector<uint32_t>> classes = {},
                      std::vector<std::shared_ptr<storm::expressions::ExpressionManager const>> expressionManagers = {});

    ValuationsStorage(uint64_t numEntities, ValuationClassDescription const& description, std::vector<char> valuations,
                      std::shared_ptr<storm::expressions::ExpressionManager const> expressionManager = {});

    ValuationsStorage(std::vector<ValuationClassDescription> const& descriptions,
                      std::vector<std::shared_ptr<storm::expressions::ExpressionManager const>> expressionManagers = {});

    ValuationsStorage(ValuationClassDescription const& description, std::shared_ptr<storm::expressions::ExpressionManager const> expressionManager = {});

    uint64_t size() const;

    uint64_t numClasses() const;

    uint64_t numStrings() const;

    bool hasStrings() const;

    uint64_t getClassOfEntity(uint64_t entity) const;

    ValuationClassDescription getClassDescription(uint64_t classIndex = 0) const;

    storm::expressions::ExpressionManager const& getManager() const;

    storm::expressions::ExpressionManager const& getManager(uint64_t classIndex) const;

    std::set<storm::expressions::Variable> getAllVariables() const;

    bool entityHasVariable(uint64_t entity, storm::expressions::Variable const& variable) const;

    VariableInformation const& getVariableInformation(uint64_t entity, storm::expressions::Variable const& variable) const;

    VariableInformation const& getVariableInformation(storm::expressions::Variable const& variable) const;

    typename storm::umb::UmbModel::Valuation getRawUmbData() const;

    void resize(uint64_t newEntityCount, uint64_t classIndex = 0);

    template<bool AllowOptional = false, typename... AllowedTypes, ValuationWriteCallback Callback>
    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<false, AllowOptional, AllowedTypes...>(size() - 1, callback);
    }

    template<bool AllowOptional = false, typename... AllowedTypes, ValuationWriteCallback Callback>
    void emplaceBack(Callback const& callback) {
        STORM_LOG_ASSERT(variableClasses.size() == 1, "Trying to add a valuation but the class is not unique.");
        emplaceBack<AllowOptional, AllowedTypes...>(0, callback);
    }

    template<typename T>
    ValuationsStorage selectEntities(T const& selectedEntities) const;

    template<typename... AllowedTypes, ValuationReadCallback Callback>
    void readCallback(uint64_t entity, Callback const& callback) const {
        for (auto const& varInfo : info(entity).variables) {
            read<AllowedTypes...>(entity, varInfo, callback);
        }
    }

    template<typename... AllowedTypes, ValuationReadCallback Callback>
    void readCallback(uint64_t entity, storm::expressions::Variable const& variable, Callback const& callback) const {
        read<AllowedTypes...>(entity, getVariableInformation(entity, variable), callback);
    }

    template<typename... AllowedTypes, ValuationReadCallback Callback>
    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<AllowedTypes...>(entity, varInfo, callback);
            }
        } else {
            for (uint64_t entity = 0; entity < size(); ++entity) {
                readCallback<AllowedTypes...>(entity, variable, callback);
            }
        }
    }

    template<typename... AllowedTypes, ValuationReadCallback Callback>
    void readCallback(Callback const& callback) const {
        for (uint64_t entity = 0; entity < size(); ++entity) {
            readCallback<AllowedTypes...>(entity, callback);
        }
    }

    template<typename ValueType>
    ValueType readValue(uint64_t entity, storm::expressions::Variable const& variable) const {
        ValueType result;
        readCallback<ValueType>(entity, variable, [&](auto, auto, ValueType value) { result = std::move(value); });
        return result;
    }

    template<typename RationalValueType>
    void setValuesInEvaluator(uint64_t entity, storm::expressions::ExpressionEvaluator<RationalValueType>& evaluator) const;

    template<bool InitializeWithCurrent = false, bool AllowOptional = false, typename... AllowedTypes, ValuationWriteCallback Callback>
    void writeCallback(uint64_t entity, Callback const& callback) {
        for (auto const& varInfo : info(entity).variables) {
            write<InitializeWithCurrent, AllowOptional, AllowedTypes...>(entity, varInfo, callback);
        }
    }

    template<bool InitializeWithCurrent = false, bool AllowOptional = false, typename... AllowedTypes, ValuationWriteCallback Callback>
    void writeCallback(uint64_t entity, storm::expressions::Variable const& variable, Callback const& callback) {
        write<InitializeWithCurrent, AllowOptional, AllowedTypes...>(entity, getVariableInformation(entity, variable), callback);
    }

    template<bool InitializeWithCurrent = false, bool AllowOptional = false, typename... AllowedTypes, ValuationWriteCallback Callback>
    void writeCallback(Callback const& callback) {
        for (uint64_t entity = 0; entity < size(); ++entity) {
            writeCallback<InitializeWithCurrent, AllowOptional, AllowedTypes...>(entity, callback);
        }
    }

    template<typename ValueType>
    void writeValue(uint64_t entity, storm::expressions::Variable const& variable, ValueType const& value) {
        if constexpr (std::is_same_v<ValueType, std::nullopt_t>) {
            writeCallback<false, true>(entity, variable, [](auto, auto, auto&) { /* intentionally empty */ });
        } else if constexpr (std::is_same_v<ValueType, std::string_view>) {
            writeCallback<false, false, std::string>(entity, variable, [&value](auto, auto, std::string& val) { val = value; });
        } else {
            writeCallback<false, false, ValueType>(entity, variable, [&value](auto, auto, ValueType& val) { val = value; });
        }
    }

    std::size_t hash() const;
 
   private:
    template<typename T>
    static std::string typeName() {
        if constexpr (std::is_same_v<T, bool>) {
            return "bool";
        } else if constexpr (std::is_same_v<T, int64_t>) {
            return "int64_t";
        } else if constexpr (std::is_same_v<T, uint64_t>) {
            return "uint64_t";
        } else if constexpr (std::is_same_v<T, double>) {
            return "double";
        } else if constexpr (std::is_same_v<T, storm::RationalNumber>) {
            return "storm::RationalNumber";
        } else if constexpr (std::is_same_v<T, Integer>) {
            return "Integer (arbitrary-precision)";
        } else if constexpr (std::is_same_v<T, std::string>) {
            return "std::string";
        } else if constexpr (std::is_same_v<T, std::string_view>) {
            return "std::string_view";
        } else if constexpr (std::is_same_v<T, std::nullopt_t>) {
            return "std::nullopt_t";
        } else {
            return typeid(T).name();
        }
    }

    template<typename... Types>
    static std::string typeNames() {
        std::ostringstream oss;
        [[maybe_unused]] bool first = true;
        ((oss << (first ? "" : ", ") << typeName<Types>(), first = false), ...);
        return oss.str();
    }
 
    uint64_t numEntities;
    std::vector<VariablesInformation> variableClasses;
 
    struct ClassData {
        std::vector<uint32_t> toClassMapping;       // mapping from entity index to class index (size equals number of entities)
        std::vector<uint64_t> toValuationsMapping;  // CSR mapping from entity index to valuations
    };
    std::optional<ClassData> entityClassMappings;  // present iff there are multiple classes
 
    std::vector<char> valuations;
    std::vector<uint64_t> stringMapping;
    std::vector<char> strings;
 
    explicit ValuationsStorage(std::vector<VariablesInformation> const& variableClasses);
 
    VariablesInformation const& info(uint64_t entity) const;
    std::span<char const> getRawBytes(uint64_t entity) const;
    std::span<char> getRawBytes(uint64_t entity);
 
    bool readBit(std::span<char const> bytes, uint64_t position) const;
    void writeBit(std::span<char> bytes, uint64_t position, bool value) const;
    uint64_t readUint64(std::span<char const> bytes, uint64_t bitOffset, uint64_t bitSize) const;
    void writeUint64(std::span<char> bytes, uint64_t bitOffset, uint64_t bitSize, uint64_t value) const;
 
    template<bool Signed>
    Integer readInteger(std::span<char const> bytes, uint64_t bitOffset, uint64_t bitSize) const;
 
    template<bool Signed>
    void writeInteger(std::span<char> bytes, uint64_t bitOffset, uint64_t bitSize, Integer const& value) const;
 
    template<typename ValueType>
    void writeValue(std::span<char> bytes, uint64_t bitOffset, uint64_t bitSize, ValueType const& value);

    template<typename... AllowedTypes, ValuationReadCallback Callback>
    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<decltype(value)>;
            bool constexpr IsAllowed = (sizeof...(AllowedTypes) == 0) || std::disjunction_v<std::is_same<ValueType, AllowedTypes>...>;
            if constexpr (IsAllowed) {
                callback(entity, varInfo.expressionVariable, std::forward<decltype(value)>(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<int64_t>(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<int64_t>::max();
                        if (invokeCallback(value) || (value <= maxInt64 && invokeCallback(static_cast<int64_t>(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<int64_t>(~rawContent & (mostSignificantBitMask - 1)) - 1) : static_cast<int64_t>(rawContent);
                    if (invokeCallback(value)) {
                        return;
                    }
                    break;
                }
                case Double:
                    if (invokeCallback(std::bit_cast<double>(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<false>(getRawBytes(entity), varInfo.bitOffset, bitSize) != Integer(0))) {
                    return;
                }
                break;
            case Uint:
            case Int: {
                Integer value = varInfo.description.type.type == Int ? readInteger<true>(getRawBytes(entity), varInfo.bitOffset, bitSize)
                                                                     : readInteger<false>(getRawBytes(entity), varInfo.bitOffset, bitSize);
                value += storm::utility::convertNumber<Integer>(varInfo.description.offset.value_or(0));
                if (invokeCallback(value)) {
                    return;
                }
                break;
            }
            case Double:
                // Reaching this line happens for two different reasons that are otherwise indistinguishable
                // here: (a) the field is a compliant 64-bit double but the caller's AllowedTypes didn't
                // include double (a type mismatch, e.g. reading a double-encoded variable via
                // getRationalValue/getInt64Value/...) -- fits64Bit is true in this case, and we fall through
                // to the "not handled" throw below, matching how a mismatched read of any other type is
                // handled; or (b) the field's declared bit size exceeds 64, which violates the UMB spec for
                // Double and should be impossible: ValuationDescriptionBuilder::addVariable rejects such
                // descriptions at construction time (see validateTypeDeclaration).
                STORM_LOG_ASSERT(varInfo.fits64Bit, "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<true>(getRawBytes(entity), varInfo.bitOffset, b);
                storm::RationalNumber const denominator = readInteger<false>(getRawBytes(entity), varInfo.bitOffset + b, b);
                if (invokeCallback(storm::RationalNumber(numerator / denominator))) {
                    return;
                }
                break;
            }
            case String:
                // Same reasoning as the Double case above: fits64Bit distinguishes a type mismatch (falls
                // through to the "not handled" throw below) from a genuine >64-bit violation (asserted
                // against here, since construction-time validation should now make it impossible).
                STORM_LOG_ASSERT(varInfo.fits64Bit, "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 << " is stored as " << varInfo.description.type.toString()
                                    << ", which cannot be read as any of the requested C++ type(s) [" << typeNames<AllowedTypes...>()
                                    << "]. Check that you are using the accessor matching the variable's declared storage type (e.g. "
                                       "getDoubleValue instead of getRationalValue for a variable added via addDoubleVariable).");
    }
 
    template<bool InitializeWithCurrent = false, bool AllowOptional = false, typename... AllowedTypes, ValuationWriteCallback Callback>
    void write(uint64_t entity, VariableInformation const& varInfo, Callback const& callback) {
        auto invokeCallback = [this, &entity, &varInfo, &callback]<typename ValueType>() -> bool {
            bool constexpr IsAllowed = (sizeof...(AllowedTypes) == 0) || std::disjunction_v<std::is_same<ValueType, AllowedTypes>...>;
            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<std::nullopt_t, ValueType>(entity, varInfo, [&value, &initializeAsUnsetOptional](auto..., auto&& currentValue) {
                        using CurrentVT = std::remove_cvref_t<decltype(currentValue)>;
                        if constexpr (std::is_same_v<CurrentVT, ValueType>) {
                            value = currentValue;
                        } else {
                            static_assert(std::is_same_v<CurrentVT, std::nullopt_t>);
                            initializeAsUnsetOptional = true;
                        }
                    });
                } else {
                    initializeAsUnsetOptional = isOptional;
                    if constexpr (std::is_same_v<ValueType, uint64_t> || std::is_same_v<ValueType, int64_t> || std::is_same_v<ValueType, Integer>) {
                        // Explicitly initialize integer values to the lower bound, 0, or the upper bound (in that order)
                        if (varInfo.description.lower && (!std::is_same_v<ValueType, uint64_t> || varInfo.description.lower.value() >= 0)) {
                            value = storm::utility::convertNumber<ValueType>(varInfo.description.lower.value());
                        } else if (!varInfo.description.upper || varInfo.description.upper >= 0) {
                            value = storm::utility::zero<ValueType>();
                        } else {
                            value = storm::utility::convertNumber<ValueType>(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<ValueType> optionalValue = initializeAsUnsetOptional ? std::optional<ValueType>() : 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<ValueType, uint64_t> || std::is_same_v<ValueType, int64_t> || std::is_same_v<ValueType, Integer>) {
                        if constexpr (std::is_same_v<ValueType, uint64_t> || std::is_same_v<ValueType, int64_t>) {
                            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<Integer>(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<Integer>(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<ValueType, uint64_t>) {
                                STORM_LOG_ASSERT(std::cmp_greater_equal(value, offset),
                                                 "Set negative value " << value << "-" << offset << " to unsigned variable.");
                                value -= offset;
                            } else {
                                value -= storm::utility::convertNumber<ValueType>(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()<bool>()) {
                    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()<uint64_t>()) {
                            return;
                        }
                    }
                    // take int64_t if uint64_t is not allowed or we have a negative offset
                    if (invokeCallback.template operator()<int64_t>()) {
                        return;
                    }
                }
                // finally take Integer if the 64 bit types are not allowed or insufficient
                if (invokeCallback.template operator()<Integer>()) {
                    return;
                }
                break;
            case Int:
                // Prefer int64_t if it fits and is allowed.
                if ((varInfo.fits64Bit && invokeCallback.template operator()<int64_t>()) || invokeCallback.template operator()<Integer>()) {
                    return;
                }
                break;
            case Double:
                if (invokeCallback.template operator()<double>()) {
                    return;
                }
                break;
            case Rational:
                if (invokeCallback.template operator()<storm::RationalNumber>()) {
                    return;
                }
                break;
            case String:
                if (invokeCallback.template operator()<std::string>()) {
                    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 << " is stored as " << varInfo.description.type.toString()
                                    << ", which cannot be written as any of the requested C++ type(s) [" << typeNames<AllowedTypes...>()
                                    << "]. Check that you are using the accessor matching the variable's declared storage type (e.g. "
                                       "writeDoubleValue instead of writeRationalValue for a variable added via addDoubleVariable).");
    }
};
}  // namespace storm::storage::sparse