Browse Source

CompressedStateType as template argument for NextStateGenerator

Former-commit-id: 145182a918
main
Mavo 9 years ago
parent
commit
662bbd73d7
  1. 2
      src/builder/ExplicitDFTModelBuilder.h
  2. 6
      src/generator/NextStateGenerator.h
  3. 4
      src/generator/PrismNextStateGenerator.h

2
src/builder/ExplicitDFTModelBuilder.h

@ -60,7 +60,7 @@ namespace storm {
size_t initialStateIndex = 0;
public:
struct LabelOptions {
struct LabelOptions {
bool buildFailLabel = true;
bool buildFailSafeLabel = false;
std::set<std::string> beLabels = {};

6
src/generator/NextStateGenerator.h

@ -11,15 +11,15 @@
namespace storm {
namespace generator {
template<typename ValueType, typename StateType = uint32_t>
template<typename ValueType, typename CompressedStateType, typename StateType = uint32_t>
class NextStateGenerator {
public:
typedef std::function<StateType (CompressedState const&)> StateToIdCallback;
typedef std::function<StateType (CompressedStateType const&)> StateToIdCallback;
virtual bool isDeterministicModel() const = 0;
virtual std::vector<StateType> getInitialStates(StateToIdCallback const& stateToIdCallback) = 0;
virtual void load(CompressedState const& state) = 0;
virtual void load(CompressedStateType const& state) = 0;
virtual StateBehavior<ValueType, StateType> expand(StateToIdCallback const& stateToIdCallback) = 0;
virtual bool satisfies(storm::expressions::Expression const& expression) const = 0;
};

4
src/generator/PrismNextStateGenerator.h

@ -13,9 +13,9 @@ namespace storm {
namespace generator {
template<typename ValueType, typename StateType = uint32_t>
class PrismNextStateGenerator : public NextStateGenerator<ValueType, StateType> {
class PrismNextStateGenerator : public NextStateGenerator<ValueType, CompressedState, StateType> {
public:
typedef typename NextStateGenerator<ValueType, StateType>::StateToIdCallback StateToIdCallback;
typedef typename NextStateGenerator<ValueType, CompressedState, StateType>::StateToIdCallback StateToIdCallback;
PrismNextStateGenerator(storm::prism::Program const& program, VariableInformation const& variableInformation, bool buildChoiceLabeling);

Loading…
Cancel
Save