diff --git a/src/storm/transformer/DAProduct.h b/src/storm/transformer/DAProduct.h new file mode 100644 index 000000000..ac3e46926 --- /dev/null +++ b/src/storm/transformer/DAProduct.h @@ -0,0 +1,27 @@ +#pragma + +#include "storm/automata/AcceptanceCondition.h" +#include "storm/transformer/Product.h" +#include + +namespace storm { + namespace transformer { + + template + class DAProduct : public Product { + public: + typedef std::shared_ptr> ptr; + + DAProduct(Product&& product, storm::automata::AcceptanceCondition::ptr acceptance) + : Product(std::move(product)), acceptance(acceptance) { + // Intentionally left blank + } + + storm::automata::AcceptanceCondition::ptr getAcceptance() { + return acceptance; + } + private: + storm::automata::AcceptanceCondition::ptr acceptance; + }; + } +} diff --git a/src/storm/transformer/DAProductBuilder.h b/src/storm/transformer/DAProductBuilder.h new file mode 100644 index 000000000..9e903e058 --- /dev/null +++ b/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 + +namespace storm { + namespace transformer { + class DAProductBuilder { + public: + DAProductBuilder(const storm::automata::DeterministicAutomaton& da, const std::vector& statesForAP) + : da(da), statesForAP(statesForAP) { + } + + template + typename DAProduct::ptr build(const Model& originalModel, const storm::storage::BitVector& statesOfInterest) const { + typename Product::ptr product = ProductBuilder::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::ptr(new DAProduct(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& 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; + } + }; + } +} diff --git a/src/storm/transformer/Product.h b/src/storm/transformer/Product.h new file mode 100644 index 000000000..d0d826d0f --- /dev/null +++ b/src/storm/transformer/Product.h @@ -0,0 +1,89 @@ +#pragma once + +#include + +namespace storm { + namespace transformer { + template + class Product { + public: + typedef std::shared_ptr> ptr; + + typedef storm::storage::sparse::state_type state_type; + typedef std::pair product_state_type; + typedef std::map product_state_to_product_index_map; + typedef std::vector 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&& product) = default; + Product& operator=(Product&& 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 + std::vector projectToOriginalModel(const Model& originalModel, const std::vector& prodValues) { + std::vector 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; + }; + } +} diff --git a/src/storm/transformer/ProductBuilder.h b/src/storm/transformer/ProductBuilder.h new file mode 100644 index 000000000..bf047db14 --- /dev/null +++ b/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 +#include +#include + +namespace storm { + namespace transformer { + + template + class ProductBuilder { + public: + typedef storm::storage::SparseMatrix matrix_type; + + template + static typename Product::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 product_state_type; + + state_type nextState = 0; + std::map productStateToProductIndex; + std::vector productIndexToProductState; + std::vector 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 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 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::ptr(new Product(std::move(product), + std::move(prodSoiLabel), + std::move(productStateToProductIndex), + std::move(productIndexToProductState))); + } + }; + } +}