Browse Source

buildMatrices handles playerIndices via reference

tempestpy_adaptions
Stefan Pranger 4 years ago
parent
commit
22c92e2485
  1. 4
      src/storm/builder/ExplicitModelBuilder.cpp
  2. 18
      src/storm/builder/ExplicitModelBuilder.h

4
src/storm/builder/ExplicitModelBuilder.cpp

@ -196,7 +196,7 @@ namespace storm {
rewardModelBuilder.addStateActionReward(storm::utility::zero<ValueType>()); rewardModelBuilder.addStateActionReward(storm::utility::zero<ValueType>());
} }
} }
// This state shall be Markovian (to not introduce Zeno behavior) // This state shall be Markovian (to not introduce Zeno behavior)
if (stateAndChoiceInformationBuilder.isBuildMarkovianStates()) { if (stateAndChoiceInformationBuilder.isBuildMarkovianStates()) {
stateAndChoiceInformationBuilder.addMarkovianState(currentRowGroup); stateAndChoiceInformationBuilder.addMarkovianState(currentRowGroup);
@ -340,7 +340,7 @@ namespace storm {
stateAndChoiceInformationBuilder.setBuildStateValuations(generator->getOptions().isBuildStateValuationsSet()); stateAndChoiceInformationBuilder.setBuildStateValuations(generator->getOptions().isBuildStateValuationsSet());
buildMatrices(transitionMatrixBuilder, rewardModelBuilders, stateAndChoiceInformationBuilder); buildMatrices(transitionMatrixBuilder, rewardModelBuilders, stateAndChoiceInformationBuilder);
// Initialize the model components with the obtained information. // Initialize the model components with the obtained information.
storm::storage::sparse::ModelComponents<ValueType, RewardModelType> modelComponents(transitionMatrixBuilder.build(0, transitionMatrixBuilder.getCurrentRowGroupCount()), buildStateLabeling(), std::unordered_map<std::string, RewardModelType>(), !generator->isDiscreteTimeModel()); storm::storage::sparse::ModelComponents<ValueType, RewardModelType> modelComponents(transitionMatrixBuilder.build(0, transitionMatrixBuilder.getCurrentRowGroupCount()), buildStateLabeling(), std::unordered_map<std::string, RewardModelType>(), !generator->isDiscreteTimeModel());

18
src/storm/builder/ExplicitModelBuilder.h

@ -35,12 +35,12 @@ namespace storm {
namespace utility { namespace utility {
template<typename ValueType> class ConstantsComparator; template<typename ValueType> class ConstantsComparator;
} }
namespace builder { namespace builder {
using namespace storm::utility::prism; using namespace storm::utility::prism;
using namespace storm::generator; using namespace storm::generator;
// Forward-declare classes. // Forward-declare classes.
template <typename ValueType> class RewardModelBuilder; template <typename ValueType> class RewardModelBuilder;
class StateAndChoiceInformationBuilder; class StateAndChoiceInformationBuilder;
@ -59,21 +59,21 @@ namespace storm {
VariableInformation varInfo; VariableInformation varInfo;
storm::storage::BitVectorHashMap<StateType> stateToId; storm::storage::BitVectorHashMap<StateType> stateToId;
}; };
template<typename ValueType, typename RewardModelType = storm::models::sparse::StandardRewardModel<ValueType>, typename StateType = uint32_t> template<typename ValueType, typename RewardModelType = storm::models::sparse::StandardRewardModel<ValueType>, typename StateType = uint32_t>
class ExplicitModelBuilder { class ExplicitModelBuilder {
public: public:
struct Options { struct Options {
/*! /*!
* Creates an object representing the default building options. * Creates an object representing the default building options.
*/ */
Options(); Options();
// The order in which to explore the model. // The order in which to explore the model.
ExplorationOrder explorationOrder; ExplorationOrder explorationOrder;
}; };
/*! /*!
* Creates an explicit model builder that uses the provided generator. * Creates an explicit model builder that uses the provided generator.
* *
@ -94,7 +94,7 @@ namespace storm {
* @param model The JANI model for which to build the model. * @param model The JANI model for which to build the model.
*/ */
ExplicitModelBuilder(storm::jani::Model const& model, storm::generator::NextStateGeneratorOptions const& generatorOptions = storm::generator::NextStateGeneratorOptions(), Options const& builderOptions = Options()); ExplicitModelBuilder(storm::jani::Model const& model, storm::generator::NextStateGeneratorOptions const& generatorOptions = storm::generator::NextStateGeneratorOptions(), Options const& builderOptions = Options());
/*! /*!
* Convert the program given at construction time to an abstract model. The type of the model is the one * Convert the program given at construction time to an abstract model. The type of the model is the one
* specified in the program. The given reward model name selects the rewards that the model will contain. * specified in the program. The given reward model name selects the rewards that the model will contain.
@ -121,7 +121,7 @@ namespace storm {
* @return A pair indicating whether the state was already discovered before and the state id of the state. * @return A pair indicating whether the state was already discovered before and the state id of the state.
*/ */
StateType getOrAddStateIndex(CompressedState const& state); StateType getOrAddStateIndex(CompressedState const& state);
/*! /*!
* Builds the transition matrix and the transition reward matrix based for the given program. * Builds the transition matrix and the transition reward matrix based for the given program.
* *

Loading…
Cancel
Save