From 0b4f8995f7b6d0a72d00fe3a136ed102f0bb6008 Mon Sep 17 00:00:00 2001
From: Roman Andriushchenko <iandri@fit.vut.cz>
Date: Tue, 20 Feb 2024 13:32:54 +0100
Subject: [PATCH] export state sub-to-full mapping when constructing sub-POMDP

---
 .../tac24-synthesis/refuel-06-res/._sketch.templ | Bin 4096 -> 0 bytes
 .../synthesis/translation/SubPomdpBuilder.cpp    |   2 ++
 .../src/synthesis/translation/SubPomdpBuilder.h  |   6 ++++++
 payntbind/src/synthesis/translation/bindings.cpp |   1 +
 4 files changed, 9 insertions(+)
 delete mode 100644 models/archive/tac24-synthesis/refuel-06-res/._sketch.templ

diff --git a/models/archive/tac24-synthesis/refuel-06-res/._sketch.templ b/models/archive/tac24-synthesis/refuel-06-res/._sketch.templ
deleted file mode 100644
index 400937d77f8069ca4f16752887b9c965df2bb145..0000000000000000000000000000000000000000
GIT binary patch
literal 0
HcmV?d00001

literal 4096
zcmZQz6=P>$Vqox1Ojhs@R)|o50+1L3ClDJkFz{^v(m+1nBL)UWIUt(=a103vVqjnw
zf#_gZ08}o3riBs6hl)!j=jZAr78K;9>g6OBmy{N#rlcg6q$&plgY?Xwb|n==Yj(C8
zg6L5&8UmvsFd71*Aut*OqaiRF0;3@?8UmvsFd71*Aut*OxIzHb*#u!QkPFGkELJE=
zEzU13N={Ws%P-1S$jmEA%`3^w&r8h7sZ_{GO)F7I%1O-22KI%ax`s4`>VLRbWEkZB
G{|5kzxhe1f

diff --git a/payntbind/src/synthesis/translation/SubPomdpBuilder.cpp b/payntbind/src/synthesis/translation/SubPomdpBuilder.cpp
index d236d3021..652cca8e3 100644
--- a/payntbind/src/synthesis/translation/SubPomdpBuilder.cpp
+++ b/payntbind/src/synthesis/translation/SubPomdpBuilder.cpp
@@ -98,6 +98,8 @@ namespace synthesis {
         observability_classes[translated_initial_state] = pomdp.getNrObservations();
         components.observabilityClasses = observability_classes;
 
+        state_sub_to_full = state_translator.translationToItem();
+
         clearMemory();
         return std::make_shared<storm::models::sparse::Pomdp<ValueType>>(std::move(components));
     }
diff --git a/payntbind/src/synthesis/translation/SubPomdpBuilder.h b/payntbind/src/synthesis/translation/SubPomdpBuilder.h
index 96f1f8245..5317750ad 100644
--- a/payntbind/src/synthesis/translation/SubPomdpBuilder.h
+++ b/payntbind/src/synthesis/translation/SubPomdpBuilder.h
@@ -24,6 +24,12 @@ namespace synthesis {
             std::map<uint64_t,ValueType> const& initial_belief
         );
 
+        /**
+         * Sub-POMDP-to-POMDP state mapping. Fresh states have an invalid value
+         * equal to the number of states in the POMDP.
+         */
+        std::vector<uint64_t> state_sub_to_full;
+
     private:
 
         /** The original POMDP. */
diff --git a/payntbind/src/synthesis/translation/bindings.cpp b/payntbind/src/synthesis/translation/bindings.cpp
index ab8a17963..586c6fc84 100644
--- a/payntbind/src/synthesis/translation/bindings.cpp
+++ b/payntbind/src/synthesis/translation/bindings.cpp
@@ -7,6 +7,7 @@ void bindings_translation(py::module& m) {
     py::class_<synthesis::SubPomdpBuilder<double>, std::shared_ptr<synthesis::SubPomdpBuilder<double>>>(m, "SubPomdpBuilder")
         .def(py::init<storm::models::sparse::Pomdp<double> const&>())
         .def("start_from_belief", &synthesis::SubPomdpBuilder<double>::startFromBelief)
+        .def_property_readonly("state_sub_to_full", [](synthesis::SubPomdpBuilder<double>& b) {return b.state_sub_to_full;} )
         ;
 }