CompressedState.h

Go to the documentation of this file.

#ifndef STORM_GENERATOR_COMPRESSEDSTATE_H_
#define STORM_GENERATOR_COMPRESSEDSTATE_H_
 
#include <map>
#include <unordered_map>
#include "storm/adapters/JsonForward.h"
#include "storm/storage/BitVector.h"
 
namespace storm {
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 extractVariableValues(CompressedState const& state, VariableInformation const& variableInformation, std::vector<int64_t>& locationValues,
                           std::vector<bool>& booleanValues, std::vector<int64_t>& integerValues);
 
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
 
#endif /* STORM_GENERATOR_COMPRESSEDSTATE_H_ */