diff --git a/src/storm-pomdp/transformer/ObservationTraceUnfolder.cpp b/src/storm-pomdp/transformer/ObservationTraceUnfolder.cpp new file mode 100644 index 000000000..a300e1880 --- /dev/null +++ b/src/storm-pomdp/transformer/ObservationTraceUnfolder.cpp @@ -0,0 +1,158 @@ +#include "storm/exceptions/InvalidArgumentException.h" +#include "storm-pomdp/transformer/ObservationTraceUnfolder.h" + + +namespace storm { + namespace pomdp { + template + ObservationTraceUnfolder::ObservationTraceUnfolder(storm::models::sparse::Pomdp const& model) : model(model) { + statesPerObservation = std::vector(model.getNrObservations(), storm::storage::BitVector(model.getNumberOfStates())); + for (uint64_t state = 0; state < model.getNumberOfStates(); ++state) { + statesPerObservation[model.getObservation(state)].set(state, true); + } + } + + template + std::shared_ptr> ObservationTraceUnfolder::transform( + const std::vector &observations, std::vector const& risk) { + std::vector modifiedObservations = observations; + // First observation should be special. + // This just makes the algorithm simpler because we do not treat the first step as a special case later. + modifiedObservations[0] = model.getNrObservations(); + + storm::storage::BitVector initialStates = model.getInitialStates(); + storm::storage::BitVector actualInitialStates = initialStates; + for (uint64_t state : initialStates) { + if (model.getObservation(state) != observations[0]) { + actualInitialStates.set(state, false); + } + } + STORM_LOG_THROW(actualInitialStates.getNumberOfSetBits() == 1, storm::exceptions::InvalidArgumentException, "Must have unique initial state matching the observation"); + // + statesPerObservation.resize(model.getNrObservations() + 1); + statesPerObservation[model.getNrObservations()] = actualInitialStates; + + + std::map unfoldedToOld; + std::map unfoldedToOldNextStep; + std::map oldToUnfolded; + + // Add this initial state state: + unfoldedToOldNextStep[0] = actualInitialStates.getNextSetIndex(0); + + storm::storage::SparseMatrixBuilder transitionMatrixBuilder(0,0,0,true,true); + uint64_t newStateIndex = 1; + uint64_t newRowGroupStart = 0; + uint64_t newRowCount = 0; + // Notice that we are going to use a special last step + + for (uint64_t step = 0; step < observations.size() - 1; ++step) { + std::cout << "step " << step << std::endl; + oldToUnfolded.clear(); + unfoldedToOld = unfoldedToOldNextStep; + unfoldedToOldNextStep.clear(); + + for (auto const& unfoldedToOldEntry : unfoldedToOld) { + transitionMatrixBuilder.newRowGroup(newRowGroupStart); + std::cout << "\tconsider new state " << unfoldedToOldEntry.first << std::endl; + assert(step == 0 || newRowCount == transitionMatrixBuilder.getLastRow() + 1); + uint64_t oldRowIndexStart = model.getNondeterministicChoiceIndices()[unfoldedToOldEntry.second]; + uint64_t oldRowIndexEnd = model.getNondeterministicChoiceIndices()[unfoldedToOldEntry.second+1]; + + for (uint64_t oldRowIndex = oldRowIndexStart; oldRowIndex != oldRowIndexEnd; oldRowIndex++) { + std::cout << "\t\tconsider old action " << oldRowIndex << std::endl; + std::cout << "\t\tconsider new row nr " << newRowCount << std::endl; + + ValueType resetProb = storm::utility::zero(); + // We first find the reset probability + for (auto const &oldRowEntry : model.getTransitionMatrix().getRow(oldRowIndex)) { + if (model.getObservation(oldRowEntry.getColumn()) != observations[step + 1]) { + resetProb += oldRowEntry.getValue(); + } + } + std::cout << "\t\t\t add reset" << std::endl; + + // Add the resets + if (resetProb != storm::utility::zero()) { + transitionMatrixBuilder.addNextValue(newRowCount, 0, resetProb); + } + + std::cout << "\t\t\t add other transitions..." << std::endl; + + // Now, we build the outgoing transitions. + for (auto const &oldRowEntry : model.getTransitionMatrix().getRow(oldRowIndex)) { + if (model.getObservation(oldRowEntry.getColumn()) != observations[step + 1]) { + continue;// already handled. + } + uint64_t column = 0; + + auto entryIt = oldToUnfolded.find(oldRowEntry.getColumn()); + if (entryIt == oldToUnfolded.end()) { + column = newStateIndex; + oldToUnfolded[oldRowEntry.getColumn()] = column; + unfoldedToOldNextStep[column] = oldRowEntry.getColumn(); + newStateIndex++; + } else { + column = entryIt->second; + } + std::cout << "\t\t\t\t transition to " << column << std::endl; + transitionMatrixBuilder.addNextValue(newRowCount, column, + oldRowEntry.getValue()); + } + newRowCount++; + } + + newRowGroupStart = transitionMatrixBuilder.getLastRow() + 1; + + } + } + std::cout << "Adding last step..." << std::endl; + // Now, take care of the last step. + uint64_t sinkState = newStateIndex; + uint64_t targetState = newStateIndex + 1; + for (auto const& unfoldedToOldEntry : unfoldedToOldNextStep) { + transitionMatrixBuilder.newRowGroup(newRowGroupStart); + if (!storm::utility::isZero(storm::utility::one() - risk[unfoldedToOldEntry.second])) { + transitionMatrixBuilder.addNextValue(newRowGroupStart, sinkState, + storm::utility::one() - risk[unfoldedToOldEntry.second]); + } + if (!storm::utility::isZero(risk[unfoldedToOldEntry.second])) { + transitionMatrixBuilder.addNextValue(newRowGroupStart, targetState, + risk[unfoldedToOldEntry.second]); + } + newRowGroupStart++; + } + // sink state + transitionMatrixBuilder.newRowGroup(newRowGroupStart); + transitionMatrixBuilder.addNextValue(newRowGroupStart, sinkState, storm::utility::one()); + newRowGroupStart++; + transitionMatrixBuilder.newRowGroup(newRowGroupStart); + // target state + transitionMatrixBuilder.addNextValue(newRowGroupStart, targetState, storm::utility::one()); + + + + storm::storage::sparse::ModelComponents components; + components.transitionMatrix = transitionMatrixBuilder.build(); + std::cout << components.transitionMatrix << std::endl; + + STORM_LOG_ASSERT(components.transitionMatrix.getRowGroupCount() == targetState + 1, "Expect row group count (" << components.transitionMatrix.getRowGroupCount() << ") one more as target state index " << targetState << ")"); + + storm::models::sparse::StateLabeling labeling(components.transitionMatrix.getRowGroupCount()); + labeling.addLabel("_goal"); + labeling.addLabelToState("_goal", targetState); + labeling.addLabel("init"); + labeling.addLabelToState("init", 0); + components.stateLabeling = labeling; + return std::make_shared>(std::move(components)); + + + + + } + + template class ObservationTraceUnfolder; + template class ObservationTraceUnfolder; + + } +} \ No newline at end of file diff --git a/src/storm-pomdp/transformer/ObservationTraceUnfolder.h b/src/storm-pomdp/transformer/ObservationTraceUnfolder.h new file mode 100644 index 000000000..feafe57e2 --- /dev/null +++ b/src/storm-pomdp/transformer/ObservationTraceUnfolder.h @@ -0,0 +1,18 @@ +#include "storm/models/sparse/Pomdp.h" + +namespace storm { + namespace pomdp { + template + class ObservationTraceUnfolder { + + public: + ObservationTraceUnfolder(storm::models::sparse::Pomdp const& model); + std::shared_ptr> transform(std::vector const& observations, std::vector const& risk); + private: + storm::models::sparse::Pomdp const& model; + std::vector statesPerObservation; + + }; + + } +} \ No newline at end of file