diff --git a/src/storm-pomdp-cli/storm-pomdp.cpp b/src/storm-pomdp-cli/storm-pomdp.cpp index dd1776149..96be00668 100644 --- a/src/storm-pomdp-cli/storm-pomdp.cpp +++ b/src/storm-pomdp-cli/storm-pomdp.cpp @@ -34,6 +34,7 @@ #include "storm-cli-utilities/cli.h" #include "storm-cli-utilities/model-handling.h" +#include "storm-pomdp/transformer/KnownProbabilityTransformer.h" #include "storm-pomdp/transformer/ApplyFiniteSchedulerToPomdp.h" #include "storm-pomdp/transformer/GlobalPOMDPSelfLoopEliminator.h" #include "storm-pomdp/transformer/GlobalPomdpMecChoiceEliminator.h" @@ -134,6 +135,8 @@ int main(const int argc, const char** argv) { if (formula) { if (formula->isProbabilityOperatorFormula()) { + boost::optional prob1States; + boost::optional prob0States; if (pomdpSettings.isSelfloopReductionSet() && !storm::solver::minimize(formula->asProbabilityOperatorFormula().getOptimalityType())) { STORM_PRINT_AND_LOG("Eliminating self-loop choices ..."); uint64_t oldChoiceCount = pomdp->getNumberOfChoices(); @@ -144,12 +147,16 @@ int main(const int argc, const char** argv) { if (pomdpSettings.isQualitativeReductionSet()) { storm::analysis::QualitativeAnalysis qualitativeAnalysis(*pomdp); STORM_PRINT_AND_LOG("Computing states with probability 0 ..."); - std::cout << qualitativeAnalysis.analyseProb0(formula->asProbabilityOperatorFormula()) << std::endl; + prob0States = qualitativeAnalysis.analyseProb0(formula->asProbabilityOperatorFormula()); + std::cout << *prob0States << std::endl; STORM_PRINT_AND_LOG(" done." << std::endl); STORM_PRINT_AND_LOG("Computing states with probability 1 ..."); - std::cout << qualitativeAnalysis.analyseProb1(formula->asProbabilityOperatorFormula()) << std::endl; + prob1States = qualitativeAnalysis.analyseProb1(formula->asProbabilityOperatorFormula()); + std::cout << *prob1States << std::endl; STORM_PRINT_AND_LOG(" done." << std::endl); - std::cout << "actual reduction not yet implemented..." << std::endl; + //std::cout << "actual reduction not yet implemented..." << std::endl; + storm::pomdp::transformer::KnownProbabilityTransformer kpt = storm::pomdp::transformer::KnownProbabilityTransformer(); + pomdp = kpt.transform(*pomdp, *prob0States, *prob1States); } if (pomdpSettings.isGridApproximationSet()) { storm::logic::ProbabilityOperatorFormula const &probFormula = formula->asProbabilityOperatorFormula(); diff --git a/src/storm-pomdp/transformer/KnownProbabilityTransformer.cpp b/src/storm-pomdp/transformer/KnownProbabilityTransformer.cpp new file mode 100644 index 000000000..c5d225d02 --- /dev/null +++ b/src/storm-pomdp/transformer/KnownProbabilityTransformer.cpp @@ -0,0 +1,121 @@ +#include "KnownProbabilityTransformer.h" + +namespace storm { + namespace pomdp { + namespace transformer { + + template + KnownProbabilityTransformer::KnownProbabilityTransformer() { + // Intentionally left empty + } + + template + std::shared_ptr> + KnownProbabilityTransformer::transform(storm::models::sparse::Pomdp const &pomdp, storm::storage::BitVector &prob0States, + storm::storage::BitVector &prob1States) { + std::map stateMap; + std::map observationMap; + + storm::models::sparse::StateLabeling newLabeling(pomdp.getNumberOfStates() - prob0States.getNumberOfSetBits() - prob1States.getNumberOfSetBits() + 2); + + std::vector newObservations; + + // New state 0 represents all states with probability 1 + for (auto const &iter : prob1States) { + stateMap[iter] = 0; + + std::set labelSet = pomdp.getStateLabeling().getLabelsOfState(iter); + for (auto const &label : labelSet) { + if (!newLabeling.containsLabel(label)) { + newLabeling.addLabel(label); + } + newLabeling.addLabelToState(label, 0); + } + } + // New state 1 represents all states with probability 0 + for (auto const &iter : prob0States) { + stateMap[iter] = 1; + for (auto const &label : pomdp.getStateLabeling().getLabelsOfState(iter)) { + if (!newLabeling.containsLabel(label)) { + newLabeling.addLabel(label); + } + newLabeling.addLabelToState(label, 1); + } + } + + storm::storage::BitVector unknownStates = ~(prob1States | prob0States); + //If there are no states with probability 0 we set the next new state id to be 1, otherwise 2 + uint64_t newId = prob0States.empty() ? 1 : 2; + uint64_t nextObservation = prob0States.empty() ? 1 : 2; + for (auto const &iter : unknownStates) { + stateMap[iter] = newId; + if (observationMap.count(pomdp.getObservation(iter)) == 0) { + observationMap[pomdp.getObservation(iter)] = nextObservation; + ++nextObservation; + } + for (auto const &label : pomdp.getStateLabeling().getLabelsOfState(iter)) { + if (!newLabeling.containsLabel(label)) { + newLabeling.addLabel(label); + } + newLabeling.addLabelToState(label, newId); + } + ++newId; + } + + uint64_t newNrOfStates = pomdp.getNumberOfStates() - (prob1States.getNumberOfSetBits() + prob0States.getNumberOfSetBits()); + + uint64_t currentRow = 0; + uint64_t currentRowGroup = 0; + storm::storage::SparseMatrixBuilder smb(0, 0, 0, false, true); + //new row for prob 1 state + smb.newRowGroup(currentRow); + smb.addNextValue(currentRow, 0, storm::utility::one()); + newObservations.push_back(0); + ++currentRowGroup; + ++currentRow; + if (!prob0States.empty()) { + smb.newRowGroup(currentRow); + smb.addNextValue(currentRow, 1, storm::utility::one()); + ++currentRowGroup; + ++currentRow; + newObservations.push_back(1); + } + + auto transitionMatrix = pomdp.getTransitionMatrix(); + + for (auto const &iter : unknownStates) { + smb.newRowGroup(currentRow); + // First collect all transitions + //auto rowGroup = transitionMatrix.getRowGroup(iter); + for (uint64_t row = 0; row < transitionMatrix.getRowGroupSize(iter); ++row) { + std::map transitionsInAction; + for (auto const &entry : transitionMatrix.getRow(iter, row)) { + // here we use the state mapping to collect all probabilities to get to a state with prob 0/1 + transitionsInAction[stateMap[entry.getColumn()]] += entry.getValue(); + } + for (auto const &transition : transitionsInAction) { + smb.addNextValue(currentRow, transition.first, transition.second); + } + ++currentRow; + } + ++currentRowGroup; + newObservations.push_back(observationMap[pomdp.getObservation(iter)]); + } + + auto newTransitionMatrix = smb.build(currentRow, newNrOfStates, currentRowGroup); + //STORM_PRINT(newTransitionMatrix) + storm::storage::sparse::ModelComponents components(newTransitionMatrix, newLabeling); + components.observabilityClasses = newObservations; + + auto newPomdp = storm::models::sparse::Pomdp(components); + + newPomdp.printModelInformationToStream(std::cout); + + return std::make_shared>(newPomdp); + } + + template + class KnownProbabilityTransformer; + } + } +} \ No newline at end of file diff --git a/src/storm-pomdp/transformer/KnownProbabilityTransformer.h b/src/storm-pomdp/transformer/KnownProbabilityTransformer.h new file mode 100644 index 000000000..e043c3f99 --- /dev/null +++ b/src/storm-pomdp/transformer/KnownProbabilityTransformer.h @@ -0,0 +1,17 @@ +#include "storm/api/storm.h" +#include "storm/models/sparse/Pomdp.h" + +namespace storm { + namespace pomdp { + namespace transformer { + template + class KnownProbabilityTransformer { + public: + KnownProbabilityTransformer(); + + std::shared_ptr> + transform(storm::models::sparse::Pomdp const &pomdp, storm::storage::BitVector &prob0States, storm::storage::BitVector &prob1States); + }; + } + } +}