(DA-product) transformer: Product, DAProduct + builders

src/storm/transformer/DAProduct.h

@@ -0,0 +1,27 @@
+#pragma
+
+#include "storm/automata/AcceptanceCondition.h"
+#include "storm/transformer/Product.h"
+#include <memory>
+
+namespace storm {
+    namespace transformer {
+
+        template <typename Model>
+        class DAProduct : public Product<Model> {
+        public:
+            typedef std::shared_ptr<DAProduct<Model>> ptr;
+
+            DAProduct(Product<Model>&& product, storm::automata::AcceptanceCondition::ptr acceptance)
+                : Product<Model>(std::move(product)), acceptance(acceptance) {
+                // Intentionally left blank
+            }
+
+            storm::automata::AcceptanceCondition::ptr getAcceptance() {
+                return acceptance;
+            }
+        private:
+            storm::automata::AcceptanceCondition::ptr acceptance;
+        };
+    }
+}

src/storm/transformer/DAProductBuilder.h

@@ -0,0 +1,55 @@
+#pragma once
+
+#include "storm/storage/BitVector.h"
+#include "storm/automata/DeterministicAutomaton.h"
+#include "storm/transformer/DAProduct.h"
+#include "storm/transformer/Product.h"
+#include "storm/transformer/ProductBuilder.h"
+
+#include <vector>
+
+namespace storm {
+    namespace transformer {
+        class DAProductBuilder {
+        public:
+            DAProductBuilder(const storm::automata::DeterministicAutomaton& da, const std::vector<storm::storage::BitVector>& statesForAP)
+              : da(da), statesForAP(statesForAP) {
+            }
+
+            template <typename Model>
+            typename DAProduct<Model>::ptr build(const Model& originalModel, const storm::storage::BitVector& statesOfInterest) const {
+                typename Product<Model>::ptr product = ProductBuilder<Model>::buildProduct(originalModel, *this, statesOfInterest);
+                storm::automata::AcceptanceCondition::ptr prodAcceptance
+                    = da.getAcceptance()->lift(product->getProductModel().getNumberOfStates(),
+                                               [&product](std::size_t prodState) {return product->getAutomatonState(prodState);});
+
+                return typename DAProduct<Model>::ptr(new DAProduct<Model>(std::move(*product), prodAcceptance));
+            }
+
+            storm::storage::sparse::state_type getInitialState(storm::storage::sparse::state_type modelState) const {
+                return da.getSuccessor(da.getInitialState(), getLabelForState(modelState));
+            }
+
+            storm::storage::sparse::state_type getSuccessor(storm::storage::sparse::state_type modelFrom,
+                                                            storm::storage::sparse::state_type automatonFrom,
+                                                            storm::storage::sparse::state_type modelTo) const {
+                return da.getSuccessor(automatonFrom, getLabelForState(modelTo));
+            }
+
+
+        private:
+            const storm::automata::DeterministicAutomaton& da;
+            const std::vector<storm::storage::BitVector>& statesForAP;
+
+            storm::automata::APSet::alphabet_element getLabelForState(storm::storage::sparse::state_type s) const {
+                storm::automata::APSet::alphabet_element label = da.getAPSet().elementAllFalse();
+                for (unsigned int ap = 0; ap < da.getAPSet().size(); ap++) {
+                    if (statesForAP.at(ap).get(s)) {
+                        label = da.getAPSet().elementAddAP(label, ap);
+                    }
+                }
+                return label;
+            }
+        };
+    }
+}

src/storm/transformer/Product.h

@@ -0,0 +1,89 @@
+#pragma once
+
+#include <memory>
+
+namespace storm {
+    namespace transformer {
+        template <typename Model>
+        class Product {
+        public:
+            typedef std::shared_ptr<Product<Model>> ptr;
+
+            typedef storm::storage::sparse::state_type state_type;
+            typedef std::pair<state_type, state_type> product_state_type;
+            typedef std::map<product_state_type, state_type> product_state_to_product_index_map;
+            typedef std::vector<product_state_type> product_index_to_product_state_vector;
+
+            Product(Model&& productModel,
+                    std::string&& productStateOfInterestLabel,
+                    product_state_to_product_index_map&& productStateToProductIndex,
+                    product_index_to_product_state_vector&& productIndexToProductState)
+                : productModel(productModel),
+                  productStateOfInterestLabel(productStateOfInterestLabel),
+                  productStateToProductIndex(productStateToProductIndex),
+                  productIndexToProductState(productIndexToProductState) {}
+
+            Product(Product<Model>&& product) = default;
+            Product& operator=(Product<Model>&& product) = default;
+
+            Model& getProductModel() {return productModel;}
+
+            state_type getModelState(state_type productStateIndex) const {
+                return productIndexToProductState.at(productStateIndex).first;
+            }
+
+            state_type getAutomatonState(state_type productStateIndex) const {
+                return productIndexToProductState.at(productStateIndex).second;
+            }
+
+            storm::storage::BitVector liftFromAutomaton(const storm::storage::BitVector& vector) const {
+                state_type n = productModel.getNumberOfStates();
+                storm::storage::BitVector lifted(n, false);
+                for (state_type s = 0; s < n; s++) {
+                    if (vector.get(getAutomatonState(s))) {
+                        lifted.set(s);
+                    }
+                }
+                return lifted;
+            }
+
+            storm::storage::BitVector liftFromModel(const storm::storage::BitVector& vector) const {
+                state_type n = productModel.getNumberOfStates();
+                storm::storage::BitVector lifted(n, false);
+                for (state_type s = 0; s < n; s++) {
+                    if (vector.get(getModelState(s))) {
+                        lifted.set(s);
+                    }
+                }
+                return lifted;
+            }
+
+            template <typename ValueType>
+            std::vector<ValueType> projectToOriginalModel(const Model& originalModel, const std::vector<ValueType>& prodValues) {
+                std::vector<ValueType> origValues(originalModel.getNumberOfStates());
+                for (state_type productState : productModel.getStateLabeling().getStates(productStateOfInterestLabel)) {
+                    state_type originalState = getModelState(productState);
+                    origValues.at(originalState) = prodValues.at(productState);
+                }
+                return origValues;
+            }
+
+            const storm::storage::BitVector& getStatesOfInterest() const {
+                return productModel.getStates(productStateOfInterestLabel);
+            }
+
+            void printMapping(std::ostream& out) const {
+                out << "Mapping index -> product state\n";
+                for (std::size_t i = 0; i < productIndexToProductState.size(); i++) {
+                    out << " " << i << ": " << productIndexToProductState.at(i).first << "," << productIndexToProductState.at(i).second << "\n";
+                }
+            }
+
+        private:
+            Model productModel;
+            std::string productStateOfInterestLabel;
+            product_state_to_product_index_map productStateToProductIndex;
+            product_index_to_product_state_vector productIndexToProductState;
+         };
+    }
+}

src/storm/transformer/ProductBuilder.h

@@ -0,0 +1,105 @@
+#pragma once
+
+#include "storm/models/sparse/StateLabeling.h"
+#include "storm/storage/SparseMatrix.h"
+#include "storm/storage/BitVector.h"
+
+#include <vector>
+#include <deque>
+#include <map>
+
+namespace storm {
+    namespace transformer {
+
+        template <typename Model>
+        class ProductBuilder {
+        public:
+            typedef storm::storage::SparseMatrix<typename Model::ValueType> matrix_type;
+
+            template <typename ProductOperator>
+            static typename Product<Model>::ptr buildProduct(const Model& originalModel, ProductOperator& prodOp, const storm::storage::BitVector& statesOfInterest) {
+                const matrix_type& originalMatrix = originalModel.getTransitionMatrix();
+                bool deterministic = originalMatrix.hasTrivialRowGrouping();
+
+                typedef storm::storage::sparse::state_type state_type;
+                typedef std::pair<state_type, state_type> product_state_type;
+
+                state_type nextState = 0;
+                std::map<product_state_type, state_type> productStateToProductIndex;
+                std::vector<product_state_type> productIndexToProductState;
+                std::vector<state_type> prodInitial;
+
+                // use deque for todo so that the states are handled in the order
+                // of their index in the product model, which is required due to the
+                // use of the SparseMatrixBuilder that can only handle linear addNextValue
+                // calls
+                std::deque<state_type> todo;
+
+                for (state_type s_0 : statesOfInterest) {
+                    state_type q_0 = prodOp.getInitialState(s_0);
+
+                    // std::cout << "Initial: " << s_0 << ", " << q_0 << " = " << nextState << "\n";
+
+                    product_state_type s_q(s_0, q_0);
+                    state_type index = nextState++;
+                    productStateToProductIndex[s_q] = index;
+                    productIndexToProductState.push_back(s_q);
+                    prodInitial.push_back(index);
+                    todo.push_back(index);
+                }
+
+                storm::storage::SparseMatrixBuilder<typename Model::ValueType> builder(0, 0, 0, false, deterministic ? false : true, 0);
+                while (!todo.empty()) {
+                    state_type prodIndexFrom = todo.front();
+                    todo.pop_front();
+
+                    product_state_type from = productIndexToProductState.at(prodIndexFrom);
+                    // std::cout << "Handle " << from.first << "," << from.second << " (prodIndexFrom = " << prodIndexFrom << "):\n";
+                    if (deterministic) {
+                        typename matrix_type::const_rows row = originalMatrix.getRow(from.first);
+                        for (auto const& entry : row) {
+                            state_type t = entry.getColumn();
+                            state_type p = prodOp.getSuccessor(from.first, from.second, t);
+                            // std::cout << " p = " << p << "\n";
+                            product_state_type t_p(t, p);
+                            state_type prodIndexTo;
+                            auto it = productStateToProductIndex.find(t_p);
+                            if (it == productStateToProductIndex.end()) {
+                                prodIndexTo = nextState++;
+                                todo.push_back(prodIndexTo);
+                                productIndexToProductState.push_back(t_p);
+                                productStateToProductIndex[t_p] = prodIndexTo;
+                                // std::cout << " Adding " << t_p.first << "," << t_p.second << " as " << prodIndexTo << "\n";
+                            } else {
+                                prodIndexTo = it->second;
+                            }
+                            // std::cout << " " << t_p.first << "," << t_p.second << ": to = " << prodIndexTo << "\n";
+
+                            // std::cout << " addNextValue(" << prodIndexFrom << "," << prodIndexTo << "," << entry.getValue() << ")\n";
+                            builder.addNextValue(prodIndexFrom, prodIndexTo, entry.getValue());
+                        }
+                    } else {
+                        throw std::runtime_error("nondeterministic product not yet supported");
+                    }
+                }
+
+                state_type numberOfProductStates = nextState;
+
+                Model product(builder.build(), storm::models::sparse::StateLabeling(numberOfProductStates));
+                storm::storage::BitVector productStatesOfInterest(product.getNumberOfStates());
+                for (auto& s : prodInitial) {
+                    productStatesOfInterest.set(s);
+                }
+                std::string prodSoiLabel = product.getStateLabeling().addUniqueLabel("soi", productStatesOfInterest);
+
+                // const storm::models::sparse::StateLabeling& orignalLabels = dtmc->getStateLabeling();
+                // for (originalLabels.)
+
+                return typename Product<Model>::ptr(new Product<Model>(std::move(product),
+                                                                       std::move(prodSoiLabel),
+                                                                       std::move(productStateToProductIndex),
+                                                                       std::move(productIndexToProductState)));
+            }
+        };
+    }
+}