Revised State and observation valuations

src/storm-cli-utilities/model-handling.h

@@ -612,6 +612,7 @@ std::shared_ptr<storm::models::ModelBase> 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<ValueType, storm::RationalFunction>) {
             STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "RationalFunction currently not supported for UMB models.");
         } else if constexpr (std::is_same_v<ValueType, storm::RationalNumber>) {

src/storm-counterexamples/counterexamples/PathCounterexample.cpp

@@ -26,7 +26,7 @@ void PathCounterexample<ValueType>::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);

src/storm-pars/transformer/BinaryDtmcTransformer.cpp

@@ -24,7 +24,7 @@ std::shared_ptr<storm::models::sparse::Dtmc<RationalFunction>> 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<storm::models::sparse::Dtmc<RationalFunction>>(std::move(components.transitionMatrix), std::move(components.stateLabeling),

src/storm-pomdp/analysis/IterativePolicySearch.cpp

@@ -863,7 +863,7 @@ void IterativePolicySearch<ValueType>::coveredStatesToStream(std::ostream& os, s
             }
             std::cout << state;
             if (pomdp.hasStateValuations()) {
-                os << ":" << pomdp.getStateValuations().getStateInfo(state);
+                os << ":" << pomdp.getStateValuations().toString(state);
             }
         }
     }

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/sparse/Valuations.h"
+#include "storm/storage/umb/model/Valuations.h"
+#include "storm/storage/umb/utility/ValuationDescriptionBuilder.h"
 #include "storm/utility/constants.h"
 #include "storm/utility/macros.h"
 
@@ -331,82 +334,42 @@ std::shared_ptr<MonitorVerifier<ValueType>> GenerateMonitorVerifier<ValueType>::
 
     if (mc.hasStateValuations()) {
         // Add state valuations
-        storm::storage::sparse::StateValuationsBuilder svBuilder;
-        svBuilder.addVariable(monvar);
-        svBuilder.addVariable(mcvar);
-        std::set<expressions::Variable> 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().getUmbValuations();
+        storm::umb::Valuations stateValuations = [this, &oldValuations]() {
+            storm::umb::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::umb::Valuations(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);
                 if (!prodToIndexMap.contains(s))
                     continue;
 
-                std::vector<bool> booleanValues;
-                std::vector<int64_t> integerValues;
-                std::vector<storm::RationalNumber> 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;
+                stateValuations.writeCallback(prodToIndexMap[std::make_pair(i, j)], [this, &oldValuations, i, j](auto, auto const& var, auto& value) {
+                    if (var == monvar || var == mcvar) {
+                        if constexpr (std::is_same_v<std::remove_cvref_t<decltype(value)>, int64_t>) {
+                            value = var == monvar ? j : i;
+                        } else {
+                            STORM_LOG_ASSERT(false, "Unexpected type.");
                         }
+                    } else {
+                        value = oldValuations.template readValue<std::remove_cvref_t<decltype(value)>>(i, var);
                     }
-                }
-                svBuilder.addState(prodToIndexMap[std::make_pair(i, j)], std::move(booleanValues), std::move(integerValues), std::move(rationalValues));
-            }
-        }
-
-        std::vector<bool> goalBooleanValues;
-        std::vector<int64_t> goalIntegerValues(2, -1);
-        std::vector<storm::RationalNumber> 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<bool> stopBooleanValues;
-        std::vector<int64_t> stopIntegerValues(2, -1);
-        std::vector<storm::RationalNumber> 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<int64_t>(goalIndex, monvar, -1);
+        stateValuations.writeValue<int64_t>(goalIndex, mcvar, -1);
+        stateValuations.writeValue<int64_t>(stopIndex, monvar, -1);
+        stateValuations.writeValue<int64_t>(stopIndex, mcvar, -1);
+        components.stateValuations.emplace(std::move(stateValuations));
     }
 
     // Store model

src/storm-pomdp/storage/BeliefManager.cpp

@@ -787,7 +787,7 @@ uint64_t BeliefManager<PomdpType, BeliefValueType, StateType>::getRepresentative
 template<typename PomdpType, typename BeliefValueType, typename StateType>
 std::string BeliefManager<PomdpType, BeliefValueType, StateType>::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 "";

src/storm-pomdp/transformer/BinaryPomdpTransformer.cpp

@@ -27,7 +27,7 @@ PomdpTransformationResult<ValueType> BinaryPomdpTransformer<ValueType>::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<ValueType> result;
     result.transformedPomdp = std::make_shared<storm::models::sparse::Pomdp<ValueType>>(std::move(components), true);

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/sparse/Valuations.h"
+#include "storm/storage/umb/model/Valuations.h"
+#include "storm/storage/umb/utility/ValuationDescriptionBuilder.h"
 #include "storm/utility/ConstantsComparator.h"
 
 #undef _VERBOSE_OBSERVATION_UNFOLDING
@@ -42,9 +45,15 @@ std::shared_ptr<storm::models::sparse::Mdp<ValueType>> ObservationTraceUnfolder<
 #ifdef _VERBOSE_OBSERVATION_UNFOLDING
     std::cout << "build valution builder..\n";
 #endif
-    storm::storage::sparse::StateValuationsBuilder svbuilder;
-    svbuilder.addVariable(svvar);
-    svbuilder.addVariable(tsvar);
+    storm::umb::Valuations stateValuations = [this, &observations]() {
+        storm::umb::ValuationDescriptionBuilder svBuilder(exprManager);
+        svBuilder.addIntegerVariable(svvar, -1, static_cast<int64_t>(model.getNumberOfStates()) - 1);
+        svBuilder.addIntegerVariable(tsvar, -1, observations.size() - 1);
+        return storm::umb::Valuations(svBuilder.buildClassDescription(), exprManager);
+    }();
+    auto addStateValuation = [this, &stateValuations](int64_t s, int64_t t) {
+        stateValuations.emplaceBack<false, int64_t>([this, s, t](auto, auto const& var, auto& value) { value = var == svvar ? s : t; });
+    };
 
     std::unordered_map<uint64_t, uint64_t> unfoldedToOld;
     std::unordered_map<uint64_t, uint64_t> unfoldedToOldNextStep;
@@ -73,7 +82,7 @@ std::shared_ptr<storm::models::sparse::Mdp<ValueType>> ObservationTraceUnfolder<
         // the violated state (only used when no rejection sampling) is a sink state
         transitionMatrixBuilder.newRowGroup(violatedState);
         transitionMatrixBuilder.addNextValue(violatedState, violatedState, storm::utility::one<ValueType>());
-        svbuilder.addState(violatedState, {}, {-1, -1});
+        addStateValuation(-1, -1);
     }
 
     // Now we are starting to build the MDP from the initial state onwards.
@@ -93,7 +102,7 @@ std::shared_ptr<storm::models::sparse::Mdp<ValueType>> ObservationTraceUnfolder<
 #endif
             STORM_LOG_ASSERT(step == 0 || newRowCount == transitionMatrixBuilder.getLastRow() + 1,
                              "step " << step << " newRowCount " << newRowCount << " lastRow " << transitionMatrixBuilder.getLastRow());
-            svbuilder.addState(unfoldedToOldEntry.first, {}, {static_cast<int64_t>(unfoldedToOldEntry.second), static_cast<int64_t>(step)});
+            addStateValuation(unfoldedToOldEntry.second, step);
             uint64_t oldRowIndexStart = model.getNondeterministicChoiceIndices()[unfoldedToOldEntry.second];
             uint64_t oldRowIndexEnd = model.getNondeterministicChoiceIndices()[unfoldedToOldEntry.second + 1];
 
@@ -159,8 +168,7 @@ std::shared_ptr<storm::models::sparse::Mdp<ValueType>> ObservationTraceUnfolder<
     uint64_t sinkState = newStateIndex;
     uint64_t targetState = newStateIndex + 1;
     for (auto const& unfoldedToOldEntry : unfoldedToOldNextStep) {
-        svbuilder.addState(unfoldedToOldEntry.first, {}, {static_cast<int64_t>(unfoldedToOldEntry.second), static_cast<int64_t>(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<ValueType>(), risk[unfoldedToOldEntry.second], storm::utility::one<ValueType>()),
@@ -177,13 +185,14 @@ std::shared_ptr<storm::models::sparse::Mdp<ValueType>> ObservationTraceUnfolder<
     // sink state
     transitionMatrixBuilder.newRowGroup(newRowGroupStart);
     transitionMatrixBuilder.addNextValue(newRowGroupStart, sinkState, storm::utility::one<ValueType>());
-    svbuilder.addState(sinkState, {}, {-1, -1});
+    addStateValuation(-1, -1);
 
     newRowGroupStart++;
     transitionMatrixBuilder.newRowGroup(newRowGroupStart);
     // target state
     transitionMatrixBuilder.addNextValue(newRowGroupStart, targetState, storm::utility::one<ValueType>());
-    svbuilder.addState(targetState, {}, {-1, -1});
+    addStateValuation(-1, -1);
+
 #ifdef _VERBOSE_OBSERVATION_UNFOLDING
     std::cout << "build matrix...\n";
 #endif
@@ -207,7 +216,7 @@ std::shared_ptr<storm::models::sparse::Mdp<ValueType>> ObservationTraceUnfolder<
     labeling.addLabel("init");
     labeling.addLabelToState("init", initialState);
     components.stateLabeling = labeling;
-    components.stateValuations = svbuilder.build();
+    components.stateValuations = std::move(stateValuations);
     return std::make_shared<storm::models::sparse::Mdp<ValueType>>(std::move(components));
 }
 

src/storm-pomdp/transformer/PomdpMemoryUnfolder.cpp

@@ -39,7 +39,7 @@ std::shared_ptr<storm::models::sparse::Pomdp<ValueType>> PomdpMemoryUnfolder<Val
             for (uint64_t newState = 0; newState < newToOldStates.size(); newState++) {
                 newToOldStates[newState] = getModelState(newState);
             }
-            components.stateValuations = pomdp.getStateValuations().blowup(newToOldStates).selectStates(reachableStates);
+            components.stateValuations = pomdp.getStateValuations().selectEntities(newToOldStates).selectEntities(reachableStates);
         }
     }
 

src/storm/builder/ExplicitModelBuilder.cpp

@@ -134,7 +134,7 @@ void ExplicitModelBuilder<ValueType, RewardModelType, StateType>::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<ValueType, RewardModelType, StateType>::buildMatrices(
 
         generator->load(currentState);
         if (stateAndChoiceInformationBuilder.isBuildStateValuations()) {
-            generator->addStateValuation(currentIndex, stateAndChoiceInformationBuilder.stateValuationsBuilder());
+            generator->addStateValuation(currentIndex, stateAndChoiceInformationBuilder.stateValuations());
         }
 
         storm::generator::StateBehavior<ValueType, StateType> behavior;
@@ -396,7 +396,7 @@ storm::storage::sparse::ModelComponents<ValueType, RewardModelType> 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);

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

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/sparse/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<storm::storage::sparse::Valuations> _stateValuations;
 };
 }  // namespace builder
 }  // namespace storm