Storm
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
StateAndChoiceInformationBuilder.h
Go to the documentation of this file.
1#pragma once
2
3#include <boost/any.hpp>
4#include <memory>
5#include <string>
6#include <unordered_map>
7#include <vector>
8
15
16namespace storm {
17namespace builder {
18
24 public:
26
27 void setBuildChoiceLabels(bool value);
28 bool isBuildChoiceLabels() const;
29 void addChoiceLabel(std::string const& label, uint_fast64_t choiceIndex);
30 storm::models::sparse::ChoiceLabeling buildChoiceLabeling(uint_fast64_t totalNumberOfChoices);
31
32 void setBuildChoiceOrigins(bool value);
33 bool isBuildChoiceOrigins() const;
34 void addChoiceOriginData(boost::any const& originData, uint_fast64_t choiceIndex);
35 std::vector<boost::any> buildDataOfChoiceOrigins(uint_fast64_t totalNumberOfChoices);
36
37 void setBuildStatePlayerIndications(bool value);
42 void addStatePlayerIndication(storm::storage::PlayerIndex player, uint_fast64_t stateIndex);
43 bool hasStatePlayerIndicationBeenSet(storm::storage::PlayerIndex expectedPlayer, uint_fast64_t stateIndex) const;
44 std::vector<storm::storage::PlayerIndex> buildStatePlayerIndications(uint_fast64_t totalNumberOfStates);
45
46 void setBuildMarkovianStates(bool value);
47 bool isBuildMarkovianStates() const;
48 void addMarkovianState(uint_fast64_t markovianStateIndex);
49 storm::storage::BitVector buildMarkovianStates(uint_fast64_t totalNumberOfStates);
50
51 void setBuildStateValuations(bool value);
52 bool isBuildStateValuations() const;
54
55 private:
56 bool _buildChoiceLabels;
57 std::unordered_map<std::string, storm::storage::BitVector> _choiceLabels;
58
59 bool _buildChoiceOrigins;
60 std::vector<boost::any> _dataOfChoiceOrigins;
61
62 bool _buildStatePlayerIndications;
63 std::vector<storm::storage::PlayerIndex> _statePlayerIndications;
64
65 bool _buildMarkovianStates;
66 storm::storage::BitVector _markovianStates;
67
68 bool _buildStateValuations;
70};
71} // namespace builder
72} // namespace storm
This class collects information regarding the states and choices during model building.
std::vector< boost::any > buildDataOfChoiceOrigins(uint_fast64_t totalNumberOfChoices)
storm::storage::sparse::StateValuationsBuilder & stateValuationsBuilder()
storm::storage::BitVector buildMarkovianStates(uint_fast64_t totalNumberOfStates)
bool hasStatePlayerIndicationBeenSet(storm::storage::PlayerIndex expectedPlayer, uint_fast64_t stateIndex) const
void addStatePlayerIndication(storm::storage::PlayerIndex player, uint_fast64_t stateIndex)
storm::models::sparse::ChoiceLabeling buildChoiceLabeling(uint_fast64_t totalNumberOfChoices)
void addChoiceLabel(std::string const &label, uint_fast64_t choiceIndex)
std::vector< storm::storage::PlayerIndex > buildStatePlayerIndications(uint_fast64_t totalNumberOfStates)
void addChoiceOriginData(boost::any const &originData, uint_fast64_t choiceIndex)
This class manages the labeling of the choice space with a number of (atomic) labels.
A bit vector that is internally represented as a vector of 64-bit values.
Definition BitVector.h:18
uint64_t PlayerIndex
Definition PlayerIndex.h:7
LabParser.cpp.
Definition cli.cpp:18