CompressedState.h

Go to the documentation of this file.

#pragma once
 
#include <map>
#include <unordered_map>
#include "storm/adapters/JsonForward.h"
#include "storm/storage/BitVector.h"
 
namespace storm {
namespace storage::sparse {
class ValuationsStorage;
}
namespace expressions {
template<typename ValueType>
class ExpressionEvaluator;
 
class ExpressionManager;
class SimpleValuation;
class Variable;
class Expression;
}  // namespace expressions
 
namespace generator {
typedef storm::storage::BitVector CompressedState;
 
struct VariableInformation;

template<typename ValueType>
void unpackStateIntoEvaluator(CompressedState const& state, VariableInformation const& variableInformation,
                              storm::expressions::ExpressionEvaluator<ValueType>& evaluator);

storm::expressions::SimpleValuation unpackStateIntoValuation(CompressedState const& state, VariableInformation const& variableInformation,
                                                             storm::expressions::ExpressionManager const& manager);

template<typename ValueType>
storm::json<ValueType> unpackStateIntoJson(CompressedState const& state, VariableInformation const& variableInformation, bool onlyObservable);

void unpackStateAppendToValuations(CompressedState const& state, VariableInformation const& variableInformation,
                                   storm::storage::sparse::ValuationsStorage& valuations);

void unpackObservationClassIntoValuations(CompressedState const& observationClass, uint64_t const observationClassIndex,
                                          VariableInformation const& variableInformation, storm::storage::sparse::ValuationsStorage& valuations);

std::string toString(CompressedState const& state, VariableInformation const& variableInformation);

storm::storage::BitVector computeObservabilityMask(VariableInformation const& variableInformation);
uint32_t unpackStateToObservabilityClass(CompressedState const& state, storm::storage::BitVector const& observationVector,
                                         std::unordered_map<storm::storage::BitVector, uint32_t>& observabilityMap, storm::storage::BitVector const& mask);
CompressedState createOutOfBoundsState(VariableInformation const& varInfo, bool roundTo64Bit = true);
 
CompressedState createCompressedState(VariableInformation const& varInfo,
                                      std::map<storm::expressions::Variable, storm::expressions::Expression> const& stateDescription, bool checkOutOfBounds);
 
CompressedState packStateFromValuation(expressions::SimpleValuation const& valuation, VariableInformation const& variableInformation,
                                       bool checkOutOfBounds = false);
 
}  // namespace generator
}  // namespace storm