You can not select more than 25 topics Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.

104 lines
3.7 KiB

  1. #ifndef STORM_GENERATOR_VARIABLEINFORMATION_H_
  2. #define STORM_GENERATOR_VARIABLEINFORMATION_H_
  3. #include <vector>
  4. #include <boost/container/flat_map.hpp>
  5. #include "storm/storage/expressions/Variable.h"
  6. namespace storm {
  7. namespace prism {
  8. class Program;
  9. }
  10. namespace jani {
  11. class Model;
  12. }
  13. namespace generator {
  14. // A structure storing information about the boolean variables of the model.
  15. struct BooleanVariableInformation {
  16. BooleanVariableInformation(storm::expressions::Variable const& variable, uint_fast64_t bitOffset, bool global = false);
  17. // The boolean variable.
  18. storm::expressions::Variable variable;
  19. // Its bit offset in the compressed state.
  20. uint_fast64_t bitOffset;
  21. // A flag indicating whether the variable is a global one.
  22. bool global;
  23. };
  24. // A structure storing information about the integer variables of the model.
  25. struct IntegerVariableInformation {
  26. IntegerVariableInformation(storm::expressions::Variable const& variable, int_fast64_t lowerBound, int_fast64_t upperBound, uint_fast64_t bitOffset, uint_fast64_t bitWidth, bool global = false);
  27. // The integer variable.
  28. storm::expressions::Variable variable;
  29. // The lower bound of its range.
  30. int_fast64_t lowerBound;
  31. // The upper bound of its range.
  32. int_fast64_t upperBound;
  33. // Its bit offset in the compressed state.
  34. uint_fast64_t bitOffset;
  35. // Its bit width in the compressed state.
  36. uint_fast64_t bitWidth;
  37. // A flag indicating whether the variable is a global one.
  38. bool global;
  39. };
  40. // A structure storing information about the location variables of the model.
  41. struct LocationVariableInformation {
  42. LocationVariableInformation(storm::expressions::Variable const& variable, uint64_t highestValue, uint_fast64_t bitOffset, uint_fast64_t bitWidth);
  43. // The expression variable for this location.
  44. storm::expressions::Variable variable;
  45. // The highest possible location value.
  46. uint64_t highestValue;
  47. // Its bit offset in the compressed state.
  48. uint_fast64_t bitOffset;
  49. // Its bit width in the compressed state.
  50. uint_fast64_t bitWidth;
  51. };
  52. // A structure storing information about the used variables of the program.
  53. struct VariableInformation {
  54. VariableInformation(storm::prism::Program const& program);
  55. VariableInformation(storm::jani::Model const& model);
  56. VariableInformation() = default;
  57. uint_fast64_t getTotalBitOffset(bool roundTo64Bit = false) const;
  58. /// The total bit offset over all variables.
  59. uint_fast64_t totalBitOffset;
  60. /// The location variables.
  61. std::vector<LocationVariableInformation> locationVariables;
  62. /// The boolean variables.
  63. std::vector<BooleanVariableInformation> booleanVariables;
  64. /// The integer variables.
  65. std::vector<IntegerVariableInformation> integerVariables;
  66. private:
  67. /*!
  68. * Sorts the variables to establish a known ordering.
  69. */
  70. void sortVariables();
  71. };
  72. }
  73. }
  74. #endif /* STORM_GENERATOR_VARIABLEINFORMATION_H_ */