Storm
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
ArrayVariableReplacementInformation.cpp
Go to the documentation of this file.
2
5
6namespace storm {
7namespace generator {
8ArrayVariableReplacementInformation::ArrayVariableReplacementInformation(std::vector<ArrayVariableReplacementInformation>&& children)
9 : data(std::move(children)) {
10 // Intentionally left empty
11}
12
13ArrayVariableReplacementInformation::ArrayVariableReplacementInformation(uint64_t informationIndex) : data(std::move(informationIndex)) {
14 // Intentionally left empty
15}
16
18 return data.which() == 0;
19}
20
22 STORM_LOG_ASSERT(isInformationIndex(), "invalid operation.");
23 return boost::get<uint64_t>(data);
24}
25
27 STORM_LOG_ASSERT(!isInformationIndex(), "invalid operation.");
28 return boost::get<std::vector<ArrayVariableReplacementInformation>>(data).size();
29}
30
32 STORM_LOG_ASSERT(!isInformationIndex(), "invalid operation.");
33 return boost::get<std::vector<ArrayVariableReplacementInformation>>(data).at(arrayAccessIndex);
34}
35
36uint64_t ArrayVariableReplacementInformation::getVariableInformationIndex(std::vector<uint64_t> arrayIndexVector) const {
37 auto const* replInfo = this;
38 for (auto const& i : arrayIndexVector) {
39 STORM_LOG_ASSERT(!replInfo->isInformationIndex(), "unexpected array replacement information.");
40 STORM_LOG_THROW(i < replInfo->getNumberOfChildren(), storm::exceptions::OutOfRangeException,
41 "Array access evaluates to array index " << i << " which is out of bounds as the array size is " << replInfo->getNumberOfChildren());
42 replInfo = &replInfo->getChild(i);
43 }
44 STORM_LOG_ASSERT(replInfo->isInformationIndex(), "unexpected array replacement information.");
45 return replInfo->getInformationIndex();
46}
47} // namespace generator
48} // namespace storm
uint64_t getVariableInformationIndex(std::vector< uint64_t > arrayIndexVector) const
ArrayVariableReplacementInformation const & getChild(uint64_t arrayAccessIndex) const
ArrayVariableReplacementInformation(std::vector< ArrayVariableReplacementInformation > &&children)
#define STORM_LOG_ASSERT(cond, message)
Definition macros.h:11
#define STORM_LOG_THROW(cond, exception, message)
Definition macros.h:30
LabParser.cpp.
Definition cli.cpp:18