diff --git a/CHANGELOG.md b/CHANGELOG.md index c2df7e656..f3b2e2a87 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -8,9 +8,13 @@ The releases of major and minor versions contain an overview of changes since th Version 1.6.x ------------- -## Version 1.6.3 (??) +## Version 1.6.3 (20xx/xx) - Added support for multi-objective model checking of long-run average objectives including mixtures with other kinds of objectives. - Added support for generating optimal schedulers for globally formulae +- Simulator supports exact arithmetic +- `storm-pomdp`: States can be labelled with values for observable predicates +- `storm-pomdp`: (Only API) Track state estimates +- `storm-pomdp`: (Only API) Reduce computation of state estimates to computation on unrolled MDP ## Version 1.6.2 (2020/09) - Prism program simplification improved. diff --git a/src/storm-pomdp/generator/BeliefSupportTracker.cpp b/src/storm-pomdp/generator/BeliefSupportTracker.cpp index be2138121..3ee6195ef 100644 --- a/src/storm-pomdp/generator/BeliefSupportTracker.cpp +++ b/src/storm-pomdp/generator/BeliefSupportTracker.cpp @@ -30,6 +30,8 @@ namespace storm { } template class BeliefSupportTracker; + template class BeliefSupportTracker; + } } \ No newline at end of file diff --git a/src/storm-pomdp/generator/NondeterministicBeliefTracker.cpp b/src/storm-pomdp/generator/NondeterministicBeliefTracker.cpp new file mode 100644 index 000000000..c02074a6b --- /dev/null +++ b/src/storm-pomdp/generator/NondeterministicBeliefTracker.cpp @@ -0,0 +1,517 @@ + +#include "storm-pomdp/generator/NondeterministicBeliefTracker.h" +#include "storm/utility/ConstantsComparator.h" +#include "storm/storage/geometry/nativepolytopeconversion/QuickHull.h" +#include "storm/storage/geometry/ReduceVertexCloud.h" +#include "storm/utility/vector.h" +#include "storm/utility/Stopwatch.h" + +namespace storm { + namespace generator { + + template + BeliefStateManager::BeliefStateManager(storm::models::sparse::Pomdp const& pomdp) + : pomdp(pomdp) + { + numberActionsPerObservation = std::vector(pomdp.getNrObservations(), 0); + statePerObservationAndOffset = std::vector>(pomdp.getNrObservations(), std::vector()); + for (uint64_t state = 0; state < pomdp.getNumberOfStates(); ++state) { + numberActionsPerObservation[pomdp.getObservation(state)] = pomdp.getNumberOfChoices(state); + statePerObservationAndOffset[pomdp.getObservation(state)].push_back(state); + observationOffsetId.push_back(statePerObservationAndOffset[pomdp.getObservation(state)].size() - 1); + } + } + + template + uint32_t BeliefStateManager::getObservation(uint64_t state) const { + return pomdp.getObservation(state); + } + + template + uint64_t BeliefStateManager::getNumberOfStates() const { + return pomdp.getNumberOfStates(); + } + + template + uint64_t BeliefStateManager::getActionsForObservation(uint32_t observation) const { + return numberActionsPerObservation[observation]; + } + + template + ValueType BeliefStateManager::getRisk(uint64_t state) const { + return riskPerState.at(state); + } + + template + storm::models::sparse::Pomdp const& BeliefStateManager::getPomdp() const { + return pomdp; + } + + template + void BeliefStateManager::setRiskPerState(std::vector const& risk) { + riskPerState = risk; + } + + template + uint64_t BeliefStateManager::getFreshId() { + beliefIdCounter++; + return beliefIdCounter; + } + + template + uint64_t BeliefStateManager::getObservationOffset(uint64_t state) const { + STORM_LOG_ASSERT(state < observationOffsetId.size(), "State " << state << " not a state id"); + return observationOffsetId[state]; + } + + template + uint64_t BeliefStateManager::numberOfStatesPerObservation(uint32_t observation) const { + STORM_LOG_ASSERT(observation < observationOffsetId.size(), "Observation " << observation << " not an observation id"); + return statePerObservationAndOffset[observation].size(); + } + + template + uint64_t BeliefStateManager::getState(uint32_t obs, uint64_t offset) const { + STORM_LOG_ASSERT(obs < statePerObservationAndOffset.size(), "Obs " << obs << " not a known observatoin"); + STORM_LOG_ASSERT(offset < statePerObservationAndOffset[obs].size(), "Offset " << offset << " too high for observation " << obs); + return statePerObservationAndOffset[obs][offset]; + } + + template + SparseBeliefState::SparseBeliefState(std::shared_ptr> const& manager, uint64_t state) + : manager(manager), belief(), id(0), prevId(0) + { + id = manager->getFreshId(); + belief[state] = storm::utility::one(); + risk = manager->getRisk(state); + } + + template + SparseBeliefState::SparseBeliefState(std::shared_ptr> const& manager, std::map const& belief, + std::size_t hash, ValueType const& risk, uint64_t prevId) + : manager(manager), belief(belief), prestoredhash(hash), risk(risk), id(0), prevId(prevId) + { + id = manager->getFreshId(); + } + + template + ValueType SparseBeliefState::get(uint64_t state) const { + return belief.at(state); + } + + template + ValueType SparseBeliefState::getRisk() const { + return risk; + } + + template + std::size_t SparseBeliefState::hash() const noexcept { + return prestoredhash; + } + + template + bool SparseBeliefState::isValid() const { + return !belief.empty(); + } + + template + std::string SparseBeliefState::toString() const { + std::stringstream sstr; + sstr << "id: " << id << "; "; + bool first = true; + for (auto const& beliefentry : belief) { + if (!first) { + sstr << ", "; + } else { + first = false; + } + sstr << beliefentry.first << " : " << beliefentry.second; + } + sstr << " (from " << prevId << ")"; + return sstr.str(); + } + + template + bool operator==(SparseBeliefState const& lhs, SparseBeliefState const& rhs) { + if (lhs.hash() != rhs.hash()) { + return false; + } + if (lhs.belief.size() != rhs.belief.size()) { + return false; + } + storm::utility::ConstantsComparator cmp(0.00001, true); + auto lhsIt = lhs.belief.begin(); + auto rhsIt = rhs.belief.begin(); + while(lhsIt != lhs.belief.end()) { + if (lhsIt->first != rhsIt->first || !cmp.isEqual(lhsIt->second, rhsIt->second)) { + return false; + } + ++lhsIt; + ++rhsIt; + } + return true; + //return std::equal(lhs.belief.begin(), lhs.belief.end(), rhs.belief.begin()); + } + + + template + void SparseBeliefState::update(uint32_t newObservation, std::unordered_set>& previousBeliefs) const { + updateHelper({{}}, {storm::utility::zero()}, belief.begin(), newObservation, previousBeliefs); + } + + template + uint64_t SparseBeliefState::getSupportSize() const { + return manager->getNumberOfStates(); + } + + template + std::map const& SparseBeliefState::getBeliefMap() const { + return belief; + } + + + template + void SparseBeliefState::setSupport(storm::storage::BitVector& support) const { + for(auto const& entry : belief) { + support.set(entry.first, true); + } + } + + template + void SparseBeliefState::updateHelper(std::vector> const& partialBeliefs, std::vector const& sums, typename std::map::const_iterator nextStateIt, uint32_t newObservation, std::unordered_set>& previousBeliefs) const { + if(nextStateIt == belief.end()) { + for (uint64_t i = 0; i < partialBeliefs.size(); ++i) { + auto const& partialBelief = partialBeliefs[i]; + auto const& sum = sums[i]; + if (storm::utility::isZero(sum)) { + continue; + } + std::size_t newHash = 0; + ValueType risk = storm::utility::zero(); + std::map finalBelief; + for (auto &entry : partialBelief) { + assert(!storm::utility::isZero(sum)); + finalBelief[entry.first] = entry.second / sum; + //boost::hash_combine(newHash, std::hash()(entry.second)); + boost::hash_combine(newHash, entry.first); + risk += entry.second / sum * manager->getRisk(entry.first); + } + previousBeliefs.insert(SparseBeliefState(manager, finalBelief, newHash, risk, id)); + } + } else { + uint64_t state = nextStateIt->first; + auto newNextStateIt = nextStateIt; + newNextStateIt++; + std::vector> newPartialBeliefs; + std::vector newSums; + for (uint64_t i = 0; i < partialBeliefs.size(); ++i) { + + for (auto row = manager->getPomdp().getNondeterministicChoiceIndices()[state]; + row < manager->getPomdp().getNondeterministicChoiceIndices()[state + 1]; ++row) { + std::map newPartialBelief = partialBeliefs[i]; + ValueType newSum = sums[i]; + for (auto const &transition : manager->getPomdp().getTransitionMatrix().getRow(row)) { + if (newObservation != manager->getPomdp().getObservation(transition.getColumn())) { + continue; + } + + if (newPartialBelief.count(transition.getColumn()) == 0) { + newPartialBelief[transition.getColumn()] = transition.getValue() * nextStateIt->second; + } else { + newPartialBelief[transition.getColumn()] += transition.getValue() * nextStateIt->second; + } + newSum += transition.getValue() * nextStateIt->second; + + } + newPartialBeliefs.push_back(newPartialBelief); + newSums.push_back(newSum); + } + } + updateHelper(newPartialBeliefs, newSums, newNextStateIt, newObservation, previousBeliefs); + + } + } + + template + bool operator==(ObservationDenseBeliefState const& lhs, ObservationDenseBeliefState const& rhs) { + if (lhs.hash() != rhs.hash()) { + return false; + } + if (lhs.observation != rhs.observation) { + return false; + } + storm::utility::ConstantsComparator cmp(0.00001, true); + auto lhsIt = lhs.belief.begin(); + auto rhsIt = rhs.belief.begin(); + while(lhsIt != lhs.belief.end()) { + if (!cmp.isEqual(*lhsIt, *rhsIt)) { + return false; + } + ++lhsIt; + ++rhsIt; + } + return true; + //return std::equal(lhs.belief.begin(), lhs.belief.end(), rhs.belief.begin()); + } + + template + ObservationDenseBeliefState::ObservationDenseBeliefState(std::shared_ptr> const& manager, uint64_t state) + : manager(manager), belief(manager->numberOfStatesPerObservation(manager->getObservation(state))) + { + observation = manager->getObservation(state); + belief[manager->getObservationOffset(state)] = storm::utility::one(); + } + + template + ObservationDenseBeliefState::ObservationDenseBeliefState(std::shared_ptr> const& manager, uint32_t observation, std::vector const& belief, std::size_t newHash, ValueType const& risk, uint64_t prevId) + : manager(manager), belief(belief), observation(observation), prestoredhash(newHash), risk(risk), id(manager->getFreshId()), prevId(prevId) + { + // Intentionally left empty. + } + + + template + void ObservationDenseBeliefState::update(uint32_t newObservation, std::unordered_set& previousBeliefs) const { + updateHelper({{}}, {storm::utility::zero()}, 0, newObservation, previousBeliefs); + } + + template + void ObservationDenseBeliefState::updateHelper(std::vector> const& partialBeliefs, std::vector const& sums, uint64_t currentEntry, uint32_t newObservation, std::unordered_set>& previousBeliefs) const { + while(currentEntry != belief.size() && storm::utility::isZero(belief[currentEntry])) { + currentEntry++; + } + if(currentEntry == belief.size()) { + for (uint64_t i = 0; i < partialBeliefs.size(); ++i) { + auto const& partialBelief = partialBeliefs[i]; + auto const& sum = sums[i]; + if (storm::utility::isZero(sum)) { + continue; + } + std::size_t newHash = 0; + ValueType risk = storm::utility::zero(); + std::vector finalBelief(manager->numberOfStatesPerObservation(observation), storm::utility::zero()); + for (auto &entry : partialBelief) { + assert(!storm::utility::isZero(sum)); + finalBelief[manager->getObservationOffset(entry.first)] = (entry.second / sum); + //boost::hash_combine(newHash, std::hash()(entry.second)); + boost::hash_combine(newHash, entry.first); + risk += entry.second / sum * manager->getRisk(entry.first); + } + previousBeliefs.insert(ObservationDenseBeliefState(manager, newObservation, finalBelief, newHash, risk, id)); + } + } else { + uint64_t state = manager->getState(observation,currentEntry); + uint64_t nextEntry = currentEntry + 1; + std::vector> newPartialBeliefs; + std::vector newSums; + for (uint64_t i = 0; i < partialBeliefs.size(); ++i) { + + for (auto row = manager->getPomdp().getNondeterministicChoiceIndices()[state]; + row < manager->getPomdp().getNondeterministicChoiceIndices()[state + 1]; ++row) { + std::map newPartialBelief = partialBeliefs[i]; + ValueType newSum = sums[i]; + for (auto const &transition : manager->getPomdp().getTransitionMatrix().getRow(row)) { + if (newObservation != manager->getPomdp().getObservation(transition.getColumn())) { + continue; + } + + if (newPartialBelief.count(transition.getColumn()) == 0) { + newPartialBelief[transition.getColumn()] = transition.getValue() * belief[currentEntry]; + } else { + newPartialBelief[transition.getColumn()] += transition.getValue() * belief[currentEntry]; + } + newSum += transition.getValue() * belief[currentEntry]; + + } + newPartialBeliefs.push_back(newPartialBelief); + newSums.push_back(newSum); + } + } + updateHelper(newPartialBeliefs, newSums, nextEntry, newObservation, previousBeliefs); + } + } + + template + std::size_t ObservationDenseBeliefState::hash() const noexcept { + return prestoredhash; + } + + template + ValueType ObservationDenseBeliefState::get(uint64_t state) const { + if (manager->getObservation(state) != state) { + return storm::utility::zero(); + } + return belief[manager->getObservationOffset(state)]; + } + + template + ValueType ObservationDenseBeliefState::getRisk() const { + return risk; + } + + template + uint64_t ObservationDenseBeliefState::getSupportSize() const { + return belief.size(); + } + + template + void ObservationDenseBeliefState::setSupport(storm::storage::BitVector& support) const { + storm::utility::vector::setNonzeroIndices(belief, support); + } + + + template + std::string ObservationDenseBeliefState::toString() const { + std::stringstream sstr; + sstr << "id: " << id << "; "; + bool first = true; + uint64_t i = 0; + for (auto const& beliefentry : belief) { + + if (!storm::utility::isZero(beliefentry)) { + if (!first) { + sstr << ", "; + } else { + first = false; + } + + sstr << manager->getState(observation, i) << " : " << beliefentry; + } + i++; + } + sstr << " (from " << prevId << ")"; + return sstr.str(); + } + + + template + NondeterministicBeliefTracker::NondeterministicBeliefTracker(storm::models::sparse::Pomdp const& pomdp, typename NondeterministicBeliefTracker::Options options ) : + pomdp(pomdp), manager(std::make_shared>(pomdp)), beliefs(), options(options) { + // + } + + template + bool NondeterministicBeliefTracker::reset(uint32_t observation) { + bool hit = false; + for (auto state : pomdp.getInitialStates()) { + if (observation == pomdp.getObservation(state)) { + hit = true; + beliefs.emplace(manager, state); + } + } + lastObservation = observation; + return hit; + } + + template + bool NondeterministicBeliefTracker::track(uint64_t newObservation) { + STORM_LOG_THROW(!beliefs.empty(), storm::exceptions::InvalidOperationException, "Cannot track without a belief (need to reset)."); + std::unordered_set newBeliefs; + storm::utility::Stopwatch trackTimer(true); + for (auto const& belief : beliefs) { + belief.update(newObservation, newBeliefs); + if (options.trackTimeOut > 0 && trackTimer.getTimeInMilliseconds() > options.trackTimeOut) { + return false; + } + } + beliefs = newBeliefs; + lastObservation = newObservation; + return !beliefs.empty(); + } + + template + ValueType NondeterministicBeliefTracker::getCurrentRisk(bool max) { + STORM_LOG_THROW(!beliefs.empty(), storm::exceptions::InvalidOperationException, "Risk is only defined for beliefs (run reset() first)."); + ValueType result = beliefs.begin()->getRisk(); + if (max) { + for (auto const& belief : beliefs) { + if (belief.getRisk() > result) { + result = belief.getRisk(); + } + } + } else { + for (auto const& belief : beliefs) { + if (belief.getRisk() < result) { + result = belief.getRisk(); + } + } + } + return result; + } + + template + void NondeterministicBeliefTracker::setRisk(std::vector const& risk) { + manager->setRiskPerState(risk); + } + + template + std::unordered_set const& NondeterministicBeliefTracker::getCurrentBeliefs() const { + return beliefs; + } + + template + uint32_t NondeterministicBeliefTracker::getCurrentObservation() const { + return lastObservation; + } + + template + uint64_t NondeterministicBeliefTracker::getNumberOfBeliefs() const { + return beliefs.size(); + } + + template + uint64_t NondeterministicBeliefTracker::getCurrentDimension() const { + storm::storage::BitVector support(beliefs.begin()->getSupportSize()); + for(auto const& belief : beliefs) { + belief.setSupport(support); + } + return support.getNumberOfSetBits(); + } + + + +// + template + uint64_t NondeterministicBeliefTracker::reduce() { + reductionTimedOut = false; + std::shared_ptr solverFactory = std::make_shared(); + storm::storage::geometry::ReduceVertexCloud rvc(solverFactory, options.wiggle, options.timeOut); + std::vector> points; + std::vector::iterator> iterators; + for (auto it = beliefs.begin(); it != beliefs.end(); ++it) { + // TODO get rid of the getBeliefMap function. + points.push_back(it->getBeliefMap()); + iterators.push_back(it); + } + auto res = rvc.eliminate(points, pomdp.getNumberOfStates()); + storm::storage::BitVector eliminate = ~res.first; + if (res.second) { + reductionTimedOut = true; + } + + auto selectedIterators = storm::utility::vector::filterVector(iterators, eliminate); + for (auto iter : selectedIterators) { + beliefs.erase(iter); + } + return eliminate.getNumberOfSetBits(); + } + + template + bool NondeterministicBeliefTracker::hasTimedOut() const { + return reductionTimedOut; + } + + + template class SparseBeliefState; + template bool operator==(SparseBeliefState const&, SparseBeliefState const&); + template class NondeterministicBeliefTracker>; + //template class ObservationDenseBeliefState; + //template bool operator==(ObservationDenseBeliefState const&, ObservationDenseBeliefState const&); + //template class NondeterministicBeliefTracker>; + + template class SparseBeliefState; + template bool operator==(SparseBeliefState const&, SparseBeliefState const&); + template class NondeterministicBeliefTracker>; + + } +} diff --git a/src/storm-pomdp/generator/NondeterministicBeliefTracker.h b/src/storm-pomdp/generator/NondeterministicBeliefTracker.h new file mode 100644 index 000000000..ad5b87143 --- /dev/null +++ b/src/storm-pomdp/generator/NondeterministicBeliefTracker.h @@ -0,0 +1,215 @@ +#pragma once +#include "storm/models/sparse/Pomdp.h" + +namespace storm { + namespace generator { + /** + * This class keeps track of common information of a set of beliefs. + * It also keeps a reference to the POMDP. The manager is referenced by all beliefs. + */ + template + class BeliefStateManager { + public: + BeliefStateManager(storm::models::sparse::Pomdp const& pomdp); + storm::models::sparse::Pomdp const& getPomdp() const; + uint64_t getActionsForObservation(uint32_t observation) const; + ValueType getRisk(uint64_t) const; + void setRiskPerState(std::vector const& risk); + uint64_t getFreshId(); + uint32_t getObservation(uint64_t state) const; + uint64_t getObservationOffset(uint64_t state) const; + uint64_t getState(uint32_t obs, uint64_t offset) const; + uint64_t getNumberOfStates() const; + uint64_t numberOfStatesPerObservation(uint32_t observation) const; + + private: + storm::models::sparse::Pomdp const& pomdp; + std::vector riskPerState; + std::vector numberActionsPerObservation; + uint64_t beliefIdCounter = 0; + std::vector observationOffsetId; + std::vector> statePerObservationAndOffset; + }; + + + template + class SparseBeliefState; + template + bool operator==(SparseBeliefState const& lhs, SparseBeliefState const& rhs); + + /** + * SparseBeliefState stores beliefs in a sparse format. + */ + template + class SparseBeliefState { + public: + SparseBeliefState(std::shared_ptr> const& manager, uint64_t state); + /** + * Update the belief using the new observation + * @param newObservation + * @param previousBeliefs put the new belief in this set + */ + void update(uint32_t newObservation, std::unordered_set& previousBeliefs) const; + std::size_t hash() const noexcept; + /** + * Get the estimate to be in the given state + * @param state + * @return + */ + ValueType get(uint64_t state) const; + /** + * Get the weighted risk + * @return + */ + ValueType getRisk() const; + + // Various getters + std::string toString() const; + bool isValid() const; + uint64_t getSupportSize() const; + void setSupport(storm::storage::BitVector&) const; + std::map const& getBeliefMap() const; + + friend bool operator==<>(SparseBeliefState const& lhs, SparseBeliefState const& rhs); + private: + void updateHelper(std::vector> const& partialBeliefs, std::vector const& sums, typename std::map::const_iterator nextStateIt, uint32_t newObservation, std::unordered_set>& previousBeliefs) const; + SparseBeliefState(std::shared_ptr> const& manager, std::map const& belief, std::size_t newHash, ValueType const& risk, uint64_t prevId); + std::shared_ptr> manager; + + std::map belief; // map is ordered for unique hashing. + std::size_t prestoredhash = 0; + ValueType risk; + uint64_t id; + uint64_t prevId; + }; + + /** + * ObservationDenseBeliefState stores beliefs in a dense format (per observation). + */ + template + class ObservationDenseBeliefState; + template + bool operator==(ObservationDenseBeliefState const& lhs, ObservationDenseBeliefState const& rhs); + + template + class ObservationDenseBeliefState { + public: + ObservationDenseBeliefState(std::shared_ptr> const& manager, uint64_t state); + void update(uint32_t newObservation, std::unordered_set& previousBeliefs) const; + std::size_t hash() const noexcept; + ValueType get(uint64_t state) const; + ValueType getRisk() const; + std::string toString() const; + uint64_t getSupportSize() const; + void setSupport(storm::storage::BitVector&) const; + friend bool operator==<>(ObservationDenseBeliefState const& lhs, ObservationDenseBeliefState const& rhs); + private: + void updateHelper(std::vector> const& partialBeliefs, std::vector const& sums, uint64_t currentEntry, uint32_t newObservation, std::unordered_set>& previousBeliefs) const; + ObservationDenseBeliefState(std::shared_ptr> const& manager, uint32_t observation, std::vector const& belief, std::size_t newHash, ValueType const& risk, uint64_t prevId); + std::shared_ptr> manager; + + std::vector belief; + uint64_t observation = 0; + std::size_t prestoredhash = 0; + ValueType risk; + uint64_t id; + uint64_t prevId; + }; + + /** + * This tracker implements state estimation for POMDPs. + * This corresponds to forward filtering in Junges, Torfah, Seshia. + * + * @tparam ValueType How are probabilities stored + * @tparam BeliefState What format to use for beliefs + */ + template + class NondeterministicBeliefTracker { + public: + struct Options { + uint64_t trackTimeOut = 0; + uint64_t timeOut = 0; // for reduction, in milliseconds, 0 is no timeout + ValueType wiggle; // tolerance, anything above 0 means that we are incomplete. + }; + NondeterministicBeliefTracker(storm::models::sparse::Pomdp const& pomdp, typename NondeterministicBeliefTracker::Options options = Options()); + /** + * Start with a new trace. + * @param observation The initial observation to start with. + * @return + */ + bool reset(uint32_t observation); + /** + * Extend the observed trace with the new observation + * @param newObservation + * @return + */ + bool track(uint64_t newObservation); + /** + * Provides access to the current beliefs. + * @return + */ + std::unordered_set const& getCurrentBeliefs() const; + /** + * What was the last obervation that we made? + * @return + */ + uint32_t getCurrentObservation() const; + /** + * How many beliefs are we currently tracking? + * @return + */ + uint64_t getNumberOfBeliefs() const; + /** + * What is the (worst-case/best-case) risk over all beliefs + * @param max Should we take the max or the min? + * @return + */ + ValueType getCurrentRisk(bool max=true); + /** + * Sets the state-risk to use for all beliefs. + * @param risk + */ + void setRisk(std::vector const& risk); + /** + * What is the dimension of the current set of beliefs, i.e., + * what is the number of states we could possibly be in? + * @return + */ + uint64_t getCurrentDimension() const; + /** + * Apply reductions to the belief state + * @return + */ + uint64_t reduce(); + /** + * Did we time out during the computation? + * @return + */ + bool hasTimedOut() const; + + private: + storm::models::sparse::Pomdp const& pomdp; + std::shared_ptr> manager; + std::unordered_set beliefs; + bool reductionTimedOut = false; + Options options; + uint32_t lastObservation; + }; + } +} + +// +namespace std { + template + struct hash> { + std::size_t operator()(storm::generator::SparseBeliefState const& s) const noexcept { + return s.hash(); + } + }; + template + struct hash> { + std::size_t operator()(storm::generator::ObservationDenseBeliefState const& s) const noexcept { + return s.hash(); + } + }; +} diff --git a/src/storm-pomdp/transformer/MakePOMDPCanonic.cpp b/src/storm-pomdp/transformer/MakePOMDPCanonic.cpp index 28f0d8c30..601ce6699 100644 --- a/src/storm-pomdp/transformer/MakePOMDPCanonic.cpp +++ b/src/storm-pomdp/transformer/MakePOMDPCanonic.cpp @@ -151,6 +151,7 @@ namespace storm { modelcomponents.stateValuations = pomdp.getOptionalStateValuations(); modelcomponents.choiceLabeling = pomdp.getChoiceLabeling(); modelcomponents.choiceLabeling->permuteItems(permutation); + modelcomponents.observationValuations = pomdp.getOptionalObservationValuations(); return std::make_shared>(modelcomponents, true); } diff --git a/src/storm-pomdp/transformer/ObservationTraceUnfolder.cpp b/src/storm-pomdp/transformer/ObservationTraceUnfolder.cpp new file mode 100644 index 000000000..36901c3e9 --- /dev/null +++ b/src/storm-pomdp/transformer/ObservationTraceUnfolder.cpp @@ -0,0 +1,202 @@ +#include "storm/exceptions/InvalidArgumentException.h" +#include "storm-pomdp/transformer/ObservationTraceUnfolder.h" +#include "storm/storage/expressions/ExpressionManager.h" +#include "storm/utility/ConstantsComparator.h" + +#undef _VERBOSE_OBSERVATION_UNFOLDING + +namespace storm { + namespace pomdp { + template + ObservationTraceUnfolder::ObservationTraceUnfolder(storm::models::sparse::Pomdp const& model, std::vector const& risk, + std::shared_ptr& exprManager) : model(model), risk(risk), exprManager(exprManager) { + 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); + } + svvar = exprManager->declareFreshIntegerVariable(false, "_s"); + } + + template + std::shared_ptr> ObservationTraceUnfolder::transform( + const std::vector &observations) { + 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; + +#ifdef _VERBOSE_OBSERVATION_UNFOLDING + std::cout << "build valution builder.." << std::endl; +#endif + storm::storage::sparse::StateValuationsBuilder svbuilder; + svbuilder.addVariable(svvar); + + std::map unfoldedToOld; + std::map unfoldedToOldNextStep; + std::map oldToUnfolded; + +#ifdef _VERBOSE_OBSERVATION_UNFOLDING + std::cout << "start buildiing matrix..." << std::endl; +#endif + + // 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) { + oldToUnfolded.clear(); + unfoldedToOld = unfoldedToOldNextStep; + unfoldedToOldNextStep.clear(); + + for (auto const& unfoldedToOldEntry : unfoldedToOld) { + transitionMatrixBuilder.newRowGroup(newRowGroupStart); +#ifdef _VERBOSE_OBSERVATION_UNFOLDING + std::cout << "\tconsider new state " << unfoldedToOldEntry.first << std::endl; +#endif + assert(step == 0 || newRowCount == transitionMatrixBuilder.getLastRow() + 1); + svbuilder.addState(unfoldedToOldEntry.first, {}, {static_cast(unfoldedToOldEntry.second)}); + uint64_t oldRowIndexStart = model.getNondeterministicChoiceIndices()[unfoldedToOldEntry.second]; + uint64_t oldRowIndexEnd = model.getNondeterministicChoiceIndices()[unfoldedToOldEntry.second+1]; + + for (uint64_t oldRowIndex = oldRowIndexStart; oldRowIndex != oldRowIndexEnd; oldRowIndex++) { +#ifdef _VERBOSE_OBSERVATION_UNFOLDING + std::cout << "\t\tconsider old action " << oldRowIndex << std::endl; + std::cout << "\t\tconsider new row nr " << newRowCount << std::endl; +#endif + + 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(); + } + } +#ifdef _VERBOSE_OBSERVATION_UNFOLDING + std::cout << "\t\t\t add reset with probability " << resetProb << std::endl; +#endif + + // Add the resets + if (resetProb != storm::utility::zero()) { + transitionMatrixBuilder.addNextValue(newRowCount, 0, resetProb); + } +#ifdef _VERBOSE_OBSERVATION_UNFOLDING + std::cout << "\t\t\t add other transitions..." << std::endl; +#endif + + // 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; + } +#ifdef _VERBOSE_OBSERVATION_UNFOLDING + std::cout << "\t\t\t\t transition to " << column << "with probability " << oldRowEntry.getValue() << std::endl; +#endif + transitionMatrixBuilder.addNextValue(newRowCount, column, + oldRowEntry.getValue()); + } + newRowCount++; + } + + newRowGroupStart = transitionMatrixBuilder.getLastRow() + 1; + + } + } + // Now, take care of the last step. + uint64_t sinkState = newStateIndex; + uint64_t targetState = newStateIndex + 1; + auto cc = storm::utility::ConstantsComparator(); + for (auto const& unfoldedToOldEntry : unfoldedToOldNextStep) { + svbuilder.addState(unfoldedToOldEntry.first, {}, {static_cast(unfoldedToOldEntry.second)}); + + transitionMatrixBuilder.newRowGroup(newRowGroupStart); + STORM_LOG_ASSERT(risk.size() > unfoldedToOldEntry.second, "Must be a state"); + STORM_LOG_ASSERT(!cc.isLess(storm::utility::one(), risk[unfoldedToOldEntry.second]), "Risk must be a probability"); + STORM_LOG_ASSERT(!cc.isLess(risk[unfoldedToOldEntry.second], storm::utility::zero()), "Risk must be a probability"); + //std::cout << "risk is" << risk[unfoldedToOldEntry.second] << std::endl; + if (!storm::utility::isOne(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()); + svbuilder.addState(sinkState, {}, {-1}); + + newRowGroupStart++; + transitionMatrixBuilder.newRowGroup(newRowGroupStart); + // target state + transitionMatrixBuilder.addNextValue(newRowGroupStart, targetState, storm::utility::one()); + svbuilder.addState(targetState, {}, {-1}); +#ifdef _VERBOSE_OBSERVATION_UNFOLDING + std::cout << "build matrix..." << std::endl; +#endif + + storm::storage::sparse::ModelComponents components; + components.transitionMatrix = transitionMatrixBuilder.build(); +#ifdef _VERBOSE_OBSERVATION_UNFOLDING + std::cout << components.transitionMatrix << std::endl; +#endif + 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; + components.stateValuations = svbuilder.build( components.transitionMatrix.getRowGroupCount()); + return std::make_shared>(std::move(components)); + + } + + template + std::shared_ptr> ObservationTraceUnfolder::extend(uint32_t observation) { + traceSoFar.push_back(observation); + return transform(traceSoFar); + } + + template + void ObservationTraceUnfolder::reset(uint32_t observation) { + traceSoFar = {observation}; + } + + template class ObservationTraceUnfolder; + template class ObservationTraceUnfolder; + template class ObservationTraceUnfolder; + + } +} diff --git a/src/storm-pomdp/transformer/ObservationTraceUnfolder.h b/src/storm-pomdp/transformer/ObservationTraceUnfolder.h new file mode 100644 index 000000000..68a4f73c5 --- /dev/null +++ b/src/storm-pomdp/transformer/ObservationTraceUnfolder.h @@ -0,0 +1,49 @@ +#include "storm/models/sparse/Pomdp.h" + +namespace storm { + namespace pomdp { + /** + * Observation-trace unrolling to allow model checking for monitoring. + * This approach is outlined in Junges, Hazem, Seshia -- Runtime Monitoring for Markov Decision Processes + * @tparam ValueType ValueType for probabilities + */ + template + class ObservationTraceUnfolder { + + public: + /** + * Initialize + * @param model the MDP with state-based observations + * @param risk the state risk + * @param exprManager an Expression Manager + */ + ObservationTraceUnfolder(storm::models::sparse::Pomdp const& model, std::vector const& risk, std::shared_ptr& exprManager); + /** + * Transform in one shot + * @param observations + * @return + */ + std::shared_ptr> transform(std::vector const& observations); + /** + * Transform incrementaly + * @param observation + * @return + */ + std::shared_ptr> extend(uint32_t observation); + /** + * When using the incremental approach, reset the observations made so far. + * @param observation The new initial observation + */ + void reset(uint32_t observation); + private: + storm::models::sparse::Pomdp const& model; + std::vector risk; // TODO reconsider holding this as a reference, but there were some strange bugs + std::shared_ptr& exprManager; + std::vector statesPerObservation; + std::vector traceSoFar; + storm::expressions::Variable svvar; + + }; + + } +} \ No newline at end of file diff --git a/src/storm/builder/BuilderOptions.cpp b/src/storm/builder/BuilderOptions.cpp index 9831040c3..17de90355 100644 --- a/src/storm/builder/BuilderOptions.cpp +++ b/src/storm/builder/BuilderOptions.cpp @@ -130,10 +130,14 @@ namespace storm { bool BuilderOptions::isBuildChoiceLabelsSet() const { return buildChoiceLabels; } - - bool BuilderOptions::isBuildStateValuationsSet() const { + + bool BuilderOptions::isBuildStateValuationsSet() const { return buildStateValuations; } + + bool BuilderOptions::isBuildObservationValuationsSet() const { + return buildObservationValuations; + } bool BuilderOptions::isBuildChoiceOriginsSet() const { return buildChoiceOrigins; @@ -237,6 +241,11 @@ namespace storm { buildStateValuations = newValue; return *this; } + + BuilderOptions& BuilderOptions::setBuildObservationValuations(bool newValue) { + buildObservationValuations = newValue; + return *this; + } BuilderOptions& BuilderOptions::setBuildChoiceOrigins(bool newValue) { buildChoiceOrigins = newValue; diff --git a/src/storm/builder/BuilderOptions.h b/src/storm/builder/BuilderOptions.h index a06817816..af424497a 100644 --- a/src/storm/builder/BuilderOptions.h +++ b/src/storm/builder/BuilderOptions.h @@ -106,6 +106,7 @@ namespace storm { bool isApplyMaximalProgressAssumptionSet() const; bool isBuildChoiceLabelsSet() const; bool isBuildStateValuationsSet() const; + bool isBuildObservationValuationsSet() const; bool isBuildChoiceOriginsSet() const; bool isBuildAllRewardModelsSet() const; bool isBuildAllLabelsSet() const; @@ -159,6 +160,14 @@ namespace storm { * @return this */ BuilderOptions& setBuildStateValuations(bool newValue = true); + + /** + * Should a observation valuation mapping be built? + * @param newValue The new value (default true) + * @return this + */ + BuilderOptions& setBuildObservationValuations(bool newValue = true); + /** * Should the origins the different choices be built? * @param newValue The new value (default true) @@ -236,6 +245,9 @@ namespace storm { /// A flag indicating whether or not to build for each state the variable valuation from which it originates. bool buildStateValuations; + + /// A flag indicating whether or not to build observation valuations + bool buildObservationValuations; // A flag that indicates whether or not to generate the information from which parts of the model specification // each choice originates. diff --git a/src/storm/builder/ExplicitModelBuilder.cpp b/src/storm/builder/ExplicitModelBuilder.cpp index 9f5c7d298..8fedf075b 100644 --- a/src/storm/builder/ExplicitModelBuilder.cpp +++ b/src/storm/builder/ExplicitModelBuilder.cpp @@ -358,69 +358,17 @@ namespace storm { } if (generator->isPartiallyObservable()) { std::vector classes; - uint32_t newObservation = 0; classes.resize(stateStorage.getNumberOfStates()); std::unordered_map, uint32_t>>> observationActions; for (auto const& bitVectorIndexPair : stateStorage.stateToId) { uint32_t varObservation = generator->observabilityClass(bitVectorIndexPair.first); - uint32_t observation = -1; // Is replaced later on. - bool checkActionNames = false; - if (checkActionNames) { - bool foundActionSet = false; - std::vector actionNames; - bool addedAnonymousAction = false; - for (uint64_t choice = modelComponents.transitionMatrix.getRowGroupIndices()[bitVectorIndexPair.second]; - choice < modelComponents.transitionMatrix.getRowGroupIndices()[bitVectorIndexPair.second + - 1]; ++choice) { - if (modelComponents.choiceLabeling.get().getLabelsOfChoice(choice).empty()) { - STORM_LOG_THROW(!addedAnonymousAction, storm::exceptions::WrongFormatException, - "Cannot have multiple anonymous actions, as these cannot be mapped correctly."); - actionNames.push_back(""); - addedAnonymousAction = true; - } else { - STORM_LOG_ASSERT( - modelComponents.choiceLabeling.get().getLabelsOfChoice(choice).size() == 1, - "Expect choice labelling to contain exactly one label at this point, but found " - << modelComponents.choiceLabeling.get().getLabelsOfChoice( - choice).size()); - actionNames.push_back( - *modelComponents.choiceLabeling.get().getLabelsOfChoice(choice).begin()); - } - } - STORM_LOG_TRACE("VarObservation: " << varObservation << " Action Names: " - << storm::utility::vector::toString(actionNames)); - auto it = observationActions.find(varObservation); - if (it == observationActions.end()) { - observationActions.emplace(varObservation, - std::vector, uint32_t>>()); - } else { - for (auto const &entries : it->second) { - STORM_LOG_TRACE(storm::utility::vector::toString(entries.first)); - if (entries.first == actionNames) { - observation = entries.second; - foundActionSet = true; - break; - } - } - - STORM_LOG_THROW( - generator->getOptions().isInferObservationsFromActionsSet() || foundActionSet, - storm::exceptions::WrongFormatException, - "Two states with the same observation have a different set of enabled actions, this is only allowed with a special option."); - - } - if (!foundActionSet) { - observation = newObservation; - observationActions.find(varObservation)->second.emplace_back(actionNames, newObservation); - ++newObservation; - } - - classes[bitVectorIndexPair.second] = observation; - } else { - classes[bitVectorIndexPair.second] = varObservation; - } + classes[bitVectorIndexPair.second] = varObservation; } + modelComponents.observabilityClasses = classes; + if(generator->getOptions().isBuildObservationValuationsSet()) { + modelComponents.observationValuations = generator->makeObservationValuation(); + } } return modelComponents; } diff --git a/src/storm/generator/NextStateGenerator.cpp b/src/storm/generator/NextStateGenerator.cpp index eb681382b..e62825d17 100644 --- a/src/storm/generator/NextStateGenerator.cpp +++ b/src/storm/generator/NextStateGenerator.cpp @@ -61,6 +61,25 @@ namespace storm { } return result; } + + template + storm::storage::sparse::StateValuationsBuilder NextStateGenerator::initializeObservationValuationsBuilder() const { + storm::storage::sparse::StateValuationsBuilder result; + for (auto const& v : variableInformation.booleanVariables) { + if(v.observable) { + result.addVariable(v.variable); + } + } + for (auto const& v : variableInformation.integerVariables) { + if(v.observable) { + result.addVariable(v.variable); + } + } + for (auto const& l : variableInformation.observationLabels) { + result.addObservationLabel(l.name); + } + return result; + } template void NextStateGenerator::load(CompressedState const& state) { @@ -93,7 +112,42 @@ namespace storm { extractVariableValues(*this->state, variableInformation, integerValues, booleanValues, integerValues); valuationsBuilder.addState(currentStateIndex, std::move(booleanValues), std::move(integerValues)); } - + + template + storm::storage::sparse::StateValuations NextStateGenerator::makeObservationValuation() const { + storm::storage::sparse::StateValuationsBuilder valuationsBuilder = initializeObservationValuationsBuilder(); + for (auto const& observationEntry : observabilityMap) { + std::vector booleanValues; + booleanValues.reserve( + variableInformation.booleanVariables.size()); // TODO: use number of observable boolean variables + std::vector integerValues; + integerValues.reserve(variableInformation.locationVariables.size() + + variableInformation.integerVariables.size()); // TODO: use number of observable integer variables + std::vector observationLabelValues; + observationLabelValues.reserve(variableInformation.observationLabels.size()); + expressions::SimpleValuation val = unpackStateIntoValuation(observationEntry.first, variableInformation, *expressionManager); + for (auto const& v : variableInformation.booleanVariables) { + if (v.observable) { + booleanValues.push_back(val.getBooleanValue(v.variable)); + } + } + for (auto const& v : variableInformation.integerVariables) { + if (v.observable) { + integerValues.push_back(val.getIntegerValue(v.variable)); + } + } + for(uint64_t labelStart = variableInformation.getTotalBitOffset(true); labelStart < observationEntry.first.size(); labelStart += 64) { + observationLabelValues.push_back(observationEntry.first.getAsInt(labelStart, 64)); + } + valuationsBuilder.addState(observationEntry.second, std::move(booleanValues), std::move(integerValues), {}, std::move(observationLabelValues)); + } + return valuationsBuilder.build(observabilityMap.size()); + + } + + + + template storm::models::sparse::StateLabeling NextStateGenerator::label(storm::storage::sparse::StateStorage const& stateStorage, std::vector const& initialStateIndices, std::vector const& deadlockStateIndices, std::vector> labelsAndExpressions) { @@ -213,7 +267,8 @@ namespace storm { if (this->mask.size() == 0) { this->mask = computeObservabilityMask(variableInformation); } - return unpackStateToObservabilityClass(state, evaluateObservationLabels(state), observabilityMap, mask); + uint32_t classId = unpackStateToObservabilityClass(state, evaluateObservationLabels(state), observabilityMap, mask); + return classId; } template diff --git a/src/storm/generator/NextStateGenerator.h b/src/storm/generator/NextStateGenerator.h index b782ad908..59f50843e 100644 --- a/src/storm/generator/NextStateGenerator.h +++ b/src/storm/generator/NextStateGenerator.h @@ -64,7 +64,9 @@ namespace storm { /// Adds the valuation for the currently loaded state to the given builder virtual void addStateValuation(storm::storage::sparse::state_type const& currentStateIndex, storm::storage::sparse::StateValuationsBuilder& valuationsBuilder) const; - + /// Adds the valuation for the currently loaded state + virtual storm::storage::sparse::StateValuations makeObservationValuation() const; + virtual std::size_t getNumberOfRewardModels() const = 0; virtual storm::builder::RewardModelInformation getRewardModelInformation(uint64_t const& index) const = 0; @@ -95,6 +97,8 @@ namespace storm { virtual storm::storage::BitVector evaluateObservationLabels(CompressedState const& state) const =0; + virtual storm::storage::sparse::StateValuationsBuilder initializeObservationValuationsBuilder() const; + void postprocess(StateBehavior& result); /// The options to be used for next-state generation. diff --git a/src/storm/generator/VariableInformation.cpp b/src/storm/generator/VariableInformation.cpp index 72a351250..91dcf30ee 100644 --- a/src/storm/generator/VariableInformation.cpp +++ b/src/storm/generator/VariableInformation.cpp @@ -29,6 +29,10 @@ namespace storm { LocationVariableInformation::LocationVariableInformation(storm::expressions::Variable const& variable, uint64_t highestValue, uint_fast64_t bitOffset, uint_fast64_t bitWidth, bool observable) : variable(variable), highestValue(highestValue), bitOffset(bitOffset), bitWidth(bitWidth), observable(observable) { // Intentionally left empty. } + + ObservationLabelInformation::ObservationLabelInformation(const std::string &name) : name(name) { + // Intentionally left empty. + } VariableInformation::VariableInformation(storm::prism::Program const& program, bool outOfBoundsState) : totalBitOffset(0) { if (outOfBoundsState) { @@ -64,6 +68,9 @@ namespace storm { totalBitOffset += bitwidth; } } + for (auto const& oblab : program.getObservationLabels()) { + observationLabels.emplace_back(oblab.getName()); + } sortVariables(); } diff --git a/src/storm/generator/VariableInformation.h b/src/storm/generator/VariableInformation.h index b7be52200..be97290f8 100644 --- a/src/storm/generator/VariableInformation.h +++ b/src/storm/generator/VariableInformation.h @@ -89,6 +89,12 @@ namespace storm { bool observable; }; + + struct ObservationLabelInformation { + ObservationLabelInformation(std::string const& name); + std::string name; + bool deterministic = true; + }; // A structure storing information about the used variables of the program. struct VariableInformation { @@ -113,7 +119,10 @@ namespace storm { /// The integer variables. std::vector integerVariables; - + + /// The observation labels + std::vector observationLabels; + /// Replacements for each array variable std::unordered_map> arrayVariableToElementInformations; diff --git a/src/storm/models/ModelBase.cpp b/src/storm/models/ModelBase.cpp index 7bf753ab8..37ef5c80d 100644 --- a/src/storm/models/ModelBase.cpp +++ b/src/storm/models/ModelBase.cpp @@ -35,6 +35,10 @@ namespace storm { } return false; } + + bool ModelBase::isPartiallyObservable() const { + return false; + } bool ModelBase::supportsParameters() const { return false; diff --git a/src/storm/models/ModelBase.h b/src/storm/models/ModelBase.h index ca275ed92..95bfdc9e5 100644 --- a/src/storm/models/ModelBase.h +++ b/src/storm/models/ModelBase.h @@ -140,7 +140,12 @@ namespace storm { * @return True iff the model is exact. */ virtual bool isExact() const; - + + /* + * Checks whether the model is partially observable + */ + virtual bool isPartiallyObservable() const; + /*! * Converts the transition rewards of all reward models to state-based rewards. For deterministic models, * this reduces the rewards to state rewards only. For nondeterminstic models, the reward models will diff --git a/src/storm/models/sparse/Pomdp.cpp b/src/storm/models/sparse/Pomdp.cpp index dc5461120..a304a1898 100644 --- a/src/storm/models/sparse/Pomdp.cpp +++ b/src/storm/models/sparse/Pomdp.cpp @@ -15,12 +15,12 @@ namespace storm { } template - Pomdp::Pomdp(storm::storage::sparse::ModelComponents const &components, bool canonicFlag) : Mdp(components, storm::models::ModelType::Pomdp), observations(components.observabilityClasses.get()), canonicFlag(canonicFlag) { + Pomdp::Pomdp(storm::storage::sparse::ModelComponents const &components, bool canonicFlag) : Mdp(components, storm::models::ModelType::Pomdp), observations(components.observabilityClasses.get()), canonicFlag(canonicFlag) , observationValuations(components.observationValuations) { computeNrObservations(); } template - Pomdp::Pomdp(storm::storage::sparse::ModelComponents &&components, bool canonicFlag): Mdp(components, storm::models::ModelType::Pomdp), observations(components.observabilityClasses.get()), canonicFlag(canonicFlag) { + Pomdp::Pomdp(storm::storage::sparse::ModelComponents &&components, bool canonicFlag): Mdp(components, storm::models::ModelType::Pomdp), observations(components.observabilityClasses.get()), canonicFlag(canonicFlag) , observationValuations(components.observationValuations) { computeNrObservations(); } @@ -100,6 +100,21 @@ namespace storm { return result; } + template + bool Pomdp::hasObservationValuations() const { + return static_cast(observationValuations); + } + + template + storm::storage::sparse::StateValuations const& Pomdp::getObservationValuations() const { + return observationValuations.get(); + } + + template + boost::optional const& Pomdp::getOptionalObservationValuations() const { + return observationValuations; + } + template bool Pomdp::isCanonic() const { return canonicFlag; @@ -110,6 +125,11 @@ namespace storm { this->canonicFlag = newValue; } + template + bool Pomdp::isPartiallyObservable() const { + return true; + } + template std::size_t Pomdp::hash() const { diff --git a/src/storm/models/sparse/Pomdp.h b/src/storm/models/sparse/Pomdp.h index cacee0953..1589ac49e 100644 --- a/src/storm/models/sparse/Pomdp.h +++ b/src/storm/models/sparse/Pomdp.h @@ -78,12 +78,20 @@ namespace storm { std::vector getStatesWithObservation(uint32_t observation) const; + bool hasObservationValuations() const; + + storm::storage::sparse::StateValuations const& getObservationValuations() const; + + boost::optional const& getOptionalObservationValuations() const; + bool isCanonic() const; void setIsCanonic(bool newValue = true); virtual std::size_t hash() const override; + virtual bool isPartiallyObservable() const override; + protected: /*! * Return a string that is additonally added to the state information in the dot stream. @@ -94,11 +102,13 @@ namespace storm { // TODO: consider a bitvector based presentation (depending on our needs). std::vector observations; - uint64_t nrObservations; - bool canonicFlag = false; + boost::optional observationValuations; + + + void computeNrObservations(); }; } diff --git a/src/storm/simulator/DiscreteTimeSparseModelSimulator.cpp b/src/storm/simulator/DiscreteTimeSparseModelSimulator.cpp index ba6ad778b..9822e8a71 100644 --- a/src/storm/simulator/DiscreteTimeSparseModelSimulator.cpp +++ b/src/storm/simulator/DiscreteTimeSparseModelSimulator.cpp @@ -18,7 +18,7 @@ namespace storm { template void DiscreteTimeSparseModelSimulator::setSeed(uint64_t seed) { - generator = storm::utility::RandomProbabilityGenerator(seed); + generator = storm::utility::RandomProbabilityGenerator(seed); } template @@ -89,5 +89,7 @@ namespace storm { } template class DiscreteTimeSparseModelSimulator; + template class DiscreteTimeSparseModelSimulator; + } } diff --git a/src/storm/solver/helper/OptimisticValueIterationHelper.cpp b/src/storm/solver/helper/OptimisticValueIterationHelper.cpp index fe5e2ddc3..c756463a9 100644 --- a/src/storm/solver/helper/OptimisticValueIterationHelper.cpp +++ b/src/storm/solver/helper/OptimisticValueIterationHelper.cpp @@ -279,6 +279,9 @@ namespace storm { bool cancelGuess = false; while (status == SolverStatus::InProgress && overallIterations < maxOverallIterations) { + if (storm::utility::resources::isTerminate()) { + status = SolverStatus::Aborted; + } ++overallIterations; ++currentVerificationIterations; // Perform value iteration stepwise for lower bound and guessed upper bound diff --git a/src/storm/storage/expressions/ExpressionManager.cpp b/src/storm/storage/expressions/ExpressionManager.cpp index 07a44dd3b..777f4b9c7 100644 --- a/src/storm/storage/expressions/ExpressionManager.cpp +++ b/src/storm/storage/expressions/ExpressionManager.cpp @@ -296,7 +296,7 @@ namespace storm { Type const& ExpressionManager::getVariableType(uint_fast64_t index) const { auto indexTypePair = indexToTypeMapping.find(index); - STORM_LOG_ASSERT(indexTypePair != indexToTypeMapping.end(), "Unable to retrieve type of unknown variable index."); + STORM_LOG_ASSERT(indexTypePair != indexToTypeMapping.end(), "Unable to retrieve type of unknown variable index '" << index << "'."); return indexTypePair->second; } diff --git a/src/storm/storage/geometry/ReduceVertexCloud.cpp b/src/storm/storage/geometry/ReduceVertexCloud.cpp new file mode 100644 index 000000000..e3042ccaf --- /dev/null +++ b/src/storm/storage/geometry/ReduceVertexCloud.cpp @@ -0,0 +1,138 @@ +#include "storm/storage/geometry/ReduceVertexCloud.h" +#include "storm/utility/Stopwatch.h" +#undef _DEBUG_REDUCE_VERTEX_CLOUD + + +namespace storm { + namespace storage { + namespace geometry { + + template + std::string toString(std::map const& point) { + std::stringstream sstr; + bool first = true; + for (auto const& entry : point) { + if (first) { + first = false; + } else { + sstr << ", "; + } + sstr << entry.first << " : " << entry.second; + } + return sstr.str(); + } + + template + std::pair ReduceVertexCloud::eliminate(std::vector> const& input, uint64_t maxdimension) { + std::shared_ptr expressionManager = std::make_shared(); + std::vector supports; + std::vector weightVariables; + std::vector weightVariableExpressions; + + for (uint64_t pointIndex = 0; pointIndex < input.size(); ++pointIndex) { + + // Compute the support vectors to quickly determine which input points could be relevant. + supports.push_back(storm::storage::BitVector(maxdimension)); + for (auto const& entry : input[pointIndex]) { + supports.back().set(entry.first, true); + } + // Add a weight variable for each input point + weightVariables.push_back(expressionManager->declareRationalVariable("w_"+ std::to_string(pointIndex))); + // For convenience and performance, obtain the expression. + weightVariableExpressions.push_back(weightVariables.back().getExpression()); + } + + std::unique_ptr smtSolver = smtSolverFactory->create(*expressionManager); + for (auto const& weightVariableExpr : weightVariableExpressions) { + //smtSolver->add((weightVariableExpr == expressionManager->rational(0.0)) || (weightVariableExpr > expressionManager->rational(0.00001))); + smtSolver->add((weightVariableExpr >= expressionManager->rational(0.0))); + smtSolver->add(weightVariableExpr < expressionManager->rational(1.0)); + } + if (storm::utility::isZero(wiggle)) { + smtSolver->add(storm::expressions::sum(weightVariableExpressions) <= + expressionManager->rational(1)); + } else { + smtSolver->add(storm::expressions::sum(weightVariableExpressions) <= + expressionManager->rational(1.0 + wiggle)); + smtSolver->add(storm::expressions::sum(weightVariableExpressions) >= + expressionManager->rational(1 - wiggle)); + } + + storm::utility::Stopwatch solverTime; + storm::utility::Stopwatch totalTime(true); + storm::storage::BitVector vertices(input.size()); + for (uint64_t pointIndex = 0; pointIndex < input.size(); ++pointIndex) { +#ifdef _DEBUG_REUCE_VERTEX_CLOUD + std::cout << pointIndex << " out of " << input.size() << std::endl; +#endif + smtSolver->push(); + std::map> dimensionTerms; + for (auto const& entry : input[pointIndex]) { + dimensionTerms[entry.first] = {expressionManager->rational(-entry.second)}; + } + for (uint64_t potentialSupport = 0; potentialSupport < input.size(); ++potentialSupport) { + if (pointIndex == potentialSupport) { + smtSolver->add(weightVariableExpressions[potentialSupport] == expressionManager->rational(0.0)); + } else if (potentialSupport < pointIndex && !vertices.get(potentialSupport)) { + smtSolver->add(weightVariableExpressions[potentialSupport] == expressionManager->rational(0.0)); + } else if (supports[potentialSupport].isSubsetOf(supports[pointIndex])) { + for (auto const& entry : input[potentialSupport]) { + dimensionTerms[entry.first].push_back(weightVariableExpressions[potentialSupport] * expressionManager->rational(entry.second)); + } + } else { + smtSolver->add(weightVariableExpressions[potentialSupport] == expressionManager->rational(0.0)); + } + } + for (auto const& entry : dimensionTerms) { + smtSolver->add(storm::expressions::sum(entry.second) == expressionManager->rational(0.0)); + } + + solverTime.start(); + auto result = smtSolver->check(); + solverTime.stop(); + if (result == storm::solver::SmtSolver::CheckResult::Unsat) { +#ifdef _DEBUG_REDUCE_VERTEX_CLOUD + if (input[pointIndex].size() == 2) { + std::cout << "point " << toString(input[pointIndex]) << " is a vertex:"; + std::cout << smtSolver->getSmtLibString() << std::endl; + } +#endif + vertices.set(pointIndex, true); + } +#ifdef _DEBUG_REDUCE_VERTEX_CLOUD + else + { + std::cout << "point " << toString(input[pointIndex]) << " is a convex combination of "; + auto val = smtSolver->getModelAsValuation(); + uint64_t varIndex = 0; + for (auto const& wvar : weightVariables) { + if (!storm::utility::isZero(val.getRationalValue(wvar))) { + std::cout << toString(input[varIndex]) << " (weight: " << val.getRationalValue(wvar) << ")"; + } + varIndex++; + } + std::cout << std::endl; + } + if (timeOut > ) +#endif + if (timeOut > 0 && totalTime.getTimeInMilliseconds() > timeOut) { + for (uint64_t remainingPoint = pointIndex + 1; remainingPoint < input.size(); ++remainingPoint) { + vertices.set(remainingPoint); + } + return {vertices, true}; + } + smtSolver->pop(); +#ifdef _DEBUG_REDUCE_VERTEX_CLOUD + std::cout << "Solver time " << solverTime.getTimeInMilliseconds() << std::endl; + std::cout << "Total time " << totalTime.getTimeInMilliseconds() << std::endl; +#endif + } + return {vertices, false}; + + } + + template class ReduceVertexCloud; + template class ReduceVertexCloud; + } + } +} \ No newline at end of file diff --git a/src/storm/storage/geometry/ReduceVertexCloud.h b/src/storm/storage/geometry/ReduceVertexCloud.h new file mode 100644 index 000000000..0877d2933 --- /dev/null +++ b/src/storm/storage/geometry/ReduceVertexCloud.h @@ -0,0 +1,36 @@ +#pragma once + +#include "storm/storage/BitVector.h" +#include "storm/solver/SmtSolver.h" +#include "storm/utility/solver.h" + +namespace storm { + namespace storage { + namespace geometry { + template + class ReduceVertexCloud { + public: + /*! + * + * @param smtSolverFactory + * @param wiggle + * @param timeout: Maximal time in milliseconds, 0 is no timeout + */ + ReduceVertexCloud(std::shared_ptr& smtSolverFactory, ValueType wiggle = storm::utility::convertNumber(0.0), uint64_t timeout = 0) + : smtSolverFactory(smtSolverFactory), wiggle(wiggle), timeOut(timeout) + { + + } + + std::pair eliminate(std::vector> const& input, uint64_t maxdimension); + + private: + std::shared_ptr& smtSolverFactory; + ValueType wiggle; + uint64_t timeOut; + + }; + + } + } +} \ No newline at end of file diff --git a/src/storm/storage/sparse/ModelComponents.h b/src/storm/storage/sparse/ModelComponents.h index f71037f1a..ca325b73c 100644 --- a/src/storm/storage/sparse/ModelComponents.h +++ b/src/storm/storage/sparse/ModelComponents.h @@ -67,6 +67,8 @@ namespace storm { // The POMDP observations boost::optional> observabilityClasses; + boost::optional observationValuations; + // Continuous time specific components (CTMCs, Markov Automata): // True iff the transition values (for Markovian choices) are interpreted as rates. bool rateTransitions; diff --git a/src/storm/storage/sparse/StateValuations.cpp b/src/storm/storage/sparse/StateValuations.cpp index 271e8aee9..95cc3368a 100644 --- a/src/storm/storage/sparse/StateValuations.cpp +++ b/src/storm/storage/sparse/StateValuations.cpp @@ -10,7 +10,7 @@ namespace storm { namespace storage { namespace sparse { - StateValuations::StateValuation::StateValuation(std::vector&& booleanValues, std::vector&& integerValues, std::vector&& rationalValues) : booleanValues(std::move(booleanValues)), integerValues(std::move(integerValues)), rationalValues(std::move(rationalValues)) { + StateValuations::StateValuation::StateValuation(std::vector&& booleanValues, std::vector&& integerValues, std::vector&& rationalValues, std::vector&& observationLabelValues) : booleanValues(std::move(booleanValues)), integerValues(std::move(integerValues)), rationalValues(std::move(rationalValues)), observationLabelValues(std::move(observationLabelValues)) { // Intentionally left empty } @@ -20,15 +20,46 @@ namespace storm { return valuations[stateIndex]; } - StateValuations::StateValueIterator::StateValueIterator(typename std::map::const_iterator variableIt, StateValuation const* valuation) : variableIt(variableIt), valuation(valuation) { + StateValuations::StateValueIterator::StateValueIterator(typename std::map::const_iterator variableIt, + typename std::map::const_iterator labelIt, + typename std::map::const_iterator variableBegin , + typename std::map::const_iterator variableEnd, + typename std::map::const_iterator labelBegin, + typename std::map::const_iterator labelEnd, + StateValuation const* valuation) : variableIt(variableIt), labelIt(labelIt), + variableBegin(variableBegin), variableEnd(variableEnd), + labelBegin(labelBegin), labelEnd(labelEnd), valuation(valuation) { // Intentionally left empty. } - storm::expressions::Variable const& StateValuations::StateValueIterator::getVariable() const { return variableIt->first; } - bool StateValuations::StateValueIterator::isBoolean() const { return getVariable().hasBooleanType(); } - bool StateValuations::StateValueIterator::isInteger() const { return getVariable().hasIntegerType(); } - bool StateValuations::StateValueIterator::isRational() const { return getVariable().hasRationalType(); } - + bool StateValuations::StateValueIterator::isVariableAssignment() const { + return variableIt != variableEnd; + } + + bool StateValuations::StateValueIterator::isLabelAssignment() const { + return variableIt == variableEnd; + } + + storm::expressions::Variable const& StateValuations::StateValueIterator::getVariable() const { + STORM_LOG_ASSERT(isVariableAssignment(), "Does not point to a variable"); + return variableIt->first; + } + std::string const& StateValuations::StateValueIterator::getLabel() const { + STORM_LOG_ASSERT(isLabelAssignment(), "Does not point to a label"); + return labelIt->first; + } + bool StateValuations::StateValueIterator::isBoolean() const { return isVariableAssignment() && getVariable().hasBooleanType(); } + bool StateValuations::StateValueIterator::isInteger() const { return isVariableAssignment() && getVariable().hasIntegerType(); } + bool StateValuations::StateValueIterator::isRational() const { return isVariableAssignment() && getVariable().hasRationalType(); } + + std::string const& StateValuations::StateValueIterator::getName() const { + if(isVariableAssignment()) { + return getVariable().getName(); + } else { + return getLabel(); + } + } + bool StateValuations::StateValueIterator::getBooleanValue() const { STORM_LOG_ASSERT(isBoolean(), "Variable has no boolean type."); return valuation->booleanValues[variableIt->second]; @@ -38,7 +69,13 @@ namespace storm { STORM_LOG_ASSERT(isInteger(), "Variable has no integer type."); return valuation->integerValues[variableIt->second]; } - + + int64_t StateValuations::StateValueIterator::getLabelValue() const { + STORM_LOG_ASSERT(isLabelAssignment(), "Not a label assignment"); + STORM_LOG_ASSERT(labelIt->second < valuation->observationLabelValues.size(), "Label index " << labelIt->second << " larger than number of labels " << valuation->observationLabelValues.size()); + return valuation->observationLabelValues[labelIt->second]; + } + storm::RationalNumber StateValuations::StateValueIterator::getRationalValue() const { STORM_LOG_ASSERT(isRational(), "Variable has no rational type."); return valuation->rationalValues[variableIt->second]; @@ -46,33 +83,41 @@ namespace storm { bool StateValuations::StateValueIterator::operator==(StateValueIterator const& other) { STORM_LOG_ASSERT(valuation == valuation, "Comparing iterators for different states"); - return variableIt == other.variableIt; + return variableIt == other.variableIt && labelIt == other.labelIt; } bool StateValuations::StateValueIterator::operator!=(StateValueIterator const& other) { - STORM_LOG_ASSERT(valuation == valuation, "Comparing iterators for different states"); - return variableIt != other.variableIt; + return !(*this == other); } typename StateValuations::StateValueIterator& StateValuations::StateValueIterator::operator++() { - ++variableIt; + if(variableIt != variableEnd ) { + ++variableIt; + } else { + ++labelIt; + } + return *this; } typename StateValuations::StateValueIterator& StateValuations::StateValueIterator::operator--() { - --variableIt; + if (labelIt != labelBegin) { + --labelIt; + } else { + --variableIt; + } return *this; } - StateValuations::StateValueIteratorRange::StateValueIteratorRange(std::map const& variableMap, StateValuation const* valuation) : variableMap(variableMap), valuation(valuation) { + StateValuations::StateValueIteratorRange::StateValueIteratorRange(std::map const& variableMap, std::map const& labelMap, StateValuation const* valuation) : variableMap(variableMap), labelMap(labelMap), valuation(valuation) { // Intentionally left empty. } StateValuations::StateValueIterator StateValuations::StateValueIteratorRange::begin() const { - return StateValueIterator(variableMap.cbegin(), valuation); + return StateValueIterator(variableMap.cbegin(), labelMap.cbegin(), variableMap.cbegin(), variableMap.cend(), labelMap.cbegin(), labelMap.cend(), valuation); } StateValuations::StateValueIterator StateValuations::StateValueIteratorRange::end() const { - return StateValueIterator(variableMap.cend(), valuation); + return StateValueIterator(variableMap.cend(), labelMap.cend(), variableMap.cbegin(), variableMap.cend(), labelMap.cbegin(), labelMap.cend(), valuation); } bool StateValuations::getBooleanValue(storm::storage::sparse::state_type const& stateIndex, storm::expressions::Variable const& booleanVariable) const { @@ -94,8 +139,8 @@ namespace storm { } bool StateValuations::isEmpty(storm::storage::sparse::state_type const& stateIndex) const { - auto const& valuation = getValuation(stateIndex); - return valuation.booleanValues.empty() && valuation.integerValues.empty() && valuation.rationalValues.empty(); + auto const& valuation = valuations[stateIndex]; // Do not use getValuations, as that is only valid after adding stuff. + return valuation.booleanValues.empty() && valuation.integerValues.empty() && valuation.rationalValues.empty() && valuation.observationLabelValues.empty(); } std::string StateValuations::toString(storm::storage::sparse::state_type const& stateIndex, bool pretty, boost::optional> const& selectedVariables) const { @@ -115,11 +160,13 @@ namespace storm { if (valIt.isBoolean() && !valIt.getBooleanValue()) { stream << "!"; } - stream << valIt.getVariable().getName(); + stream << valIt.getName(); if (valIt.isInteger()) { stream << "=" << valIt.getIntegerValue(); } else if (valIt.isRational()) { stream << "=" << valIt.getRationalValue(); + } else if (valIt.isLabelAssignment()) { + stream << "=" << valIt.getLabelValue(); } else { STORM_LOG_THROW(valIt.isBoolean(), storm::exceptions::InvalidTypeException, "Unexpected variable type."); } @@ -130,6 +177,8 @@ namespace storm { stream << valIt.getIntegerValue(); } else if (valIt.isRational()) { stream << valIt.getRationalValue(); + } else if (valIt.isLabelAssignment()) { + stream << valIt.getLabelValue(); } } assignments.push_back(stream.str()); @@ -161,12 +210,12 @@ namespace storm { } if (valIt.isBoolean()) { - result[valIt.getVariable().getName()] = valIt.getBooleanValue(); + result[valIt.getName()] = valIt.getBooleanValue(); } else if (valIt.isInteger()) { - result[valIt.getVariable().getName()] = valIt.getIntegerValue(); + result[valIt.getName()] = valIt.getIntegerValue(); } else { STORM_LOG_ASSERT(valIt.isRational(), "Unexpected variable type."); - result[valIt.getVariable().getName()] = valIt.getRationalValue(); + result[valIt.getName()] = valIt.getRationalValue(); } if (selectedVariables) { @@ -220,7 +269,7 @@ namespace storm { typename StateValuations::StateValueIteratorRange StateValuations::at(state_type const& state) const { STORM_LOG_ASSERT(state < getNumberOfStates(), "Invalid state index."); - return StateValueIteratorRange({variableToIndexMap, &(valuations[state])}); + return StateValueIteratorRange({variableToIndexMap, observationLabels, &(valuations[state])}); } uint_fast64_t StateValuations::getNumberOfStates() const { @@ -256,7 +305,7 @@ namespace storm { return StateValuations(variableToIndexMap, std::move(newValuations)); } - StateValuationsBuilder::StateValuationsBuilder() : booleanVarCount(0), integerVarCount(0), rationalVarCount(0) { + StateValuationsBuilder::StateValuationsBuilder() : booleanVarCount(0), integerVarCount(0), rationalVarCount(0), labelCount(0) { // Intentionally left empty. } @@ -273,24 +322,41 @@ namespace storm { currentStateValuations.variableToIndexMap[variable] = rationalVarCount++; } } + + void StateValuationsBuilder::addObservationLabel(const std::string &label) { + currentStateValuations.observationLabels[label] = labelCount++; + } - void StateValuationsBuilder::addState(storm::storage::sparse::state_type const& state, std::vector&& booleanValues, std::vector&& integerValues, std::vector&& rationalValues) { + void StateValuationsBuilder::addState(storm::storage::sparse::state_type const& state, std::vector&& booleanValues, std::vector&& integerValues, std::vector&& rationalValues,std::vector&& observationLabelValues) { if (state > currentStateValuations.valuations.size()) { currentStateValuations.valuations.resize(state); } if (state == currentStateValuations.valuations.size()) { - currentStateValuations.valuations.emplace_back(std::move(booleanValues), std::move(integerValues), std::move(rationalValues)); + currentStateValuations.valuations.emplace_back(std::move(booleanValues), std::move(integerValues), std::move(rationalValues), std::move(observationLabelValues)); } else { STORM_LOG_ASSERT(currentStateValuations.isEmpty(state), "Adding a valuation to the same state multiple times."); - currentStateValuations.valuations[state] = typename StateValuations::StateValuation(std::move(booleanValues), std::move(integerValues), std::move(rationalValues)); + currentStateValuations.valuations[state] = typename StateValuations::StateValuation(std::move(booleanValues), std::move(integerValues), std::move(rationalValues), std::move(observationLabelValues)); } } + + uint64_t StateValuationsBuilder::getBooleanVarCount() const { + return booleanVarCount; + } + + uint64_t StateValuationsBuilder::getIntegerVarCount() const { + return integerVarCount; + } + + uint64_t StateValuationsBuilder::getLabelCount() const { + return labelCount; + } StateValuations StateValuationsBuilder::build(std::size_t totalStateCount) { return std::move(currentStateValuations); booleanVarCount = 0; integerVarCount = 0; rationalVarCount = 0; + labelCount = 0; } } } diff --git a/src/storm/storage/sparse/StateValuations.h b/src/storm/storage/sparse/StateValuations.h index 4199a69a3..ac78ce816 100644 --- a/src/storm/storage/sparse/StateValuations.h +++ b/src/storm/storage/sparse/StateValuations.h @@ -26,45 +26,65 @@ namespace storm { public: friend class StateValuations; StateValuation() = default; - StateValuation(std::vector&& booleanValues, std::vector&& integerValues, std::vector&& rationalValues); + StateValuation(std::vector&& booleanValues, std::vector&& integerValues, std::vector&& rationalValues, std::vector&& observationLabelValues = {}); private: std::vector booleanValues; std::vector integerValues; std::vector rationalValues; + std::vector observationLabelValues; }; class StateValueIterator { public: - StateValueIterator(typename std::map::const_iterator variableIt, StateValuation const* valuation); + StateValueIterator(typename std::map::const_iterator variableIt, + typename std::map::const_iterator labelIt, + typename std::map::const_iterator variableBegin , + typename std::map::const_iterator variableEnd, + typename std::map::const_iterator labelBegin, + typename std::map::const_iterator labelEnd, + StateValuation const* valuation); bool operator==(StateValueIterator const& other); bool operator!=(StateValueIterator const& other); StateValueIterator& operator++(); StateValueIterator& operator--(); - + + bool isVariableAssignment() const; + bool isLabelAssignment() const; storm::expressions::Variable const& getVariable() const; + std::string const& getLabel() const; bool isBoolean() const; bool isInteger() const; bool isRational() const; - + + std::string const& getName() const; + // These shall only be called if the variable has the correct type bool getBooleanValue() const; int64_t getIntegerValue() const; storm::RationalNumber getRationalValue() const; + int64_t getLabelValue() const; private: typename std::map::const_iterator variableIt; + typename std::map::const_iterator labelIt; + typename std::map::const_iterator variableBegin; + typename std::map::const_iterator variableEnd; + typename std::map::const_iterator labelBegin; + typename std::map::const_iterator labelEnd; + StateValuation const* const valuation; }; class StateValueIteratorRange { public: - StateValueIteratorRange(std::map const& variableMap, StateValuation const* valuation); + StateValueIteratorRange(std::map const& variableMap, std::map const& labelMap, StateValuation const* valuation); StateValueIterator begin() const; StateValueIterator end() const; private: std::map const& variableMap; + std::map const& labelMap; StateValuation const* const valuation; }; @@ -119,6 +139,7 @@ namespace storm { StateValuation const& getValuation(storm::storage::sparse::state_type const& stateIndex) const; std::map variableToIndexMap; + std::map observationLabels; // A mapping from state indices to their variable valuations. std::vector valuations; @@ -129,28 +150,35 @@ namespace storm { StateValuationsBuilder(); /*! Adds a new variable to keep track of for the state valuations. - *! All variables need to be added before adding new states. + * All variables need to be added before adding new states. */ void addVariable(storm::expressions::Variable const& variable); - + + void addObservationLabel(std::string const& label); + /*! * Adds a new state. * The variable values have to be given in the same order as the variables have been added. * The number of given variable values for each type needs to match the number of added variables. * After calling this method, no more variables should be added. */ - void addState(storm::storage::sparse::state_type const& state, std::vector&& booleanValues = {}, std::vector&& integerValues = {}, std::vector&& rationalValues = {}); + void addState(storm::storage::sparse::state_type const& state, std::vector&& booleanValues = {}, std::vector&& integerValues = {}, std::vector&& rationalValues = {}, std::vector&& observationLabelValues = {}); /*! * Creates the finalized state valuations object. */ StateValuations build(std::size_t totalStateCount); + uint64_t getBooleanVarCount() const; + uint64_t getIntegerVarCount() const; + uint64_t getLabelCount() const; + private: StateValuations currentStateValuations; uint64_t booleanVarCount; uint64_t integerVarCount; uint64_t rationalVarCount; + uint64_t labelCount; }; } } diff --git a/src/storm/utility/SignalHandler.h b/src/storm/utility/SignalHandler.h index 1050dfcad..bcae6d7ed 100644 --- a/src/storm/utility/SignalHandler.h +++ b/src/storm/utility/SignalHandler.h @@ -103,6 +103,12 @@ namespace storm { int lastSignal; }; + + inline void resetTimeoutAlarm() { + SignalInformation::infos().setTerminate(false); + alarm(0); + } + /*! * Check whether the program should terminate (due to some abort signal). * diff --git a/src/storm/utility/random.cpp b/src/storm/utility/random.cpp index f13d403cd..9e2d0ae35 100644 --- a/src/storm/utility/random.cpp +++ b/src/storm/utility/random.cpp @@ -1,5 +1,7 @@ #include "storm/utility/random.h" +#include + namespace storm { namespace utility { RandomProbabilityGenerator::RandomProbabilityGenerator() @@ -23,6 +25,28 @@ namespace storm { return std::uniform_int_distribution(min, max)(engine); } + RandomProbabilityGenerator::RandomProbabilityGenerator() + : distribution(0, std::numeric_limits::max()) + { + std::random_device rd; + engine = std::mt19937(rd()); + } + + RandomProbabilityGenerator::RandomProbabilityGenerator(uint64_t seed) + : distribution(0, std::numeric_limits::max()), engine(seed) + { + + } + + RationalNumber RandomProbabilityGenerator::random() { + return carl::rationalize(distribution(engine)) / carl::rationalize(std::numeric_limits::max()); + + } + + uint64_t RandomProbabilityGenerator::random_uint(uint64_t min, uint64_t max) { + return std::uniform_int_distribution(min, max)(engine); + } + } } diff --git a/src/storm/utility/random.h b/src/storm/utility/random.h index 93bfad20c..7e6e015be 100644 --- a/src/storm/utility/random.h +++ b/src/storm/utility/random.h @@ -1,4 +1,5 @@ #include +#include "storm/adapters/RationalNumberAdapter.h" namespace storm { namespace utility { @@ -26,6 +27,20 @@ namespace storm { }; + template<> + class RandomProbabilityGenerator { + public: + RandomProbabilityGenerator(); + RandomProbabilityGenerator(uint64_t seed); + RationalNumber random(); + uint64_t random_uint(uint64_t min, uint64_t max); + private: + std::uniform_int_distribution distribution; + std::mt19937 engine; + + }; + + } } \ No newline at end of file diff --git a/src/storm/utility/vector.h b/src/storm/utility/vector.h index b70453aaa..28c267223 100644 --- a/src/storm/utility/vector.h +++ b/src/storm/utility/vector.h @@ -84,6 +84,16 @@ namespace storm { } } + template + void setNonzeroIndices(std::vector const& vec, storm::storage::BitVector& bv) { + STORM_LOG_ASSERT(bv.size() == vec.size(), "Bitvector size should match vector size"); + for (uint64_t i = 0; i < vec.size(); ++i) { + if(!storm::utility::isZero(vec[i])) { + bv.set(i, true); + } + } + } + /*! * Iota function as a helper for efficient creating a range in a vector. * See also http://stackoverflow.com/questions/11965732/set-stdvectorint-to-a-range