From 22c92e24854688910442ed7e8de836bb97c5def3 Mon Sep 17 00:00:00 2001 From: Stefan Pranger Date: Fri, 29 Jan 2021 08:12:38 +0100 Subject: [PATCH] buildMatrices handles playerIndices via reference --- src/storm/builder/ExplicitModelBuilder.cpp | 4 ++-- src/storm/builder/ExplicitModelBuilder.h | 18 +++++++++--------- 2 files changed, 11 insertions(+), 11 deletions(-) diff --git a/src/storm/builder/ExplicitModelBuilder.cpp b/src/storm/builder/ExplicitModelBuilder.cpp index b80825d1d..70b68fbce 100644 --- a/src/storm/builder/ExplicitModelBuilder.cpp +++ b/src/storm/builder/ExplicitModelBuilder.cpp @@ -196,7 +196,7 @@ namespace storm { rewardModelBuilder.addStateActionReward(storm::utility::zero()); } } - + // This state shall be Markovian (to not introduce Zeno behavior) if (stateAndChoiceInformationBuilder.isBuildMarkovianStates()) { stateAndChoiceInformationBuilder.addMarkovianState(currentRowGroup); @@ -340,7 +340,7 @@ namespace storm { stateAndChoiceInformationBuilder.setBuildStateValuations(generator->getOptions().isBuildStateValuationsSet()); buildMatrices(transitionMatrixBuilder, rewardModelBuilders, stateAndChoiceInformationBuilder); - + // Initialize the model components with the obtained information. storm::storage::sparse::ModelComponents modelComponents(transitionMatrixBuilder.build(0, transitionMatrixBuilder.getCurrentRowGroupCount()), buildStateLabeling(), std::unordered_map(), !generator->isDiscreteTimeModel()); diff --git a/src/storm/builder/ExplicitModelBuilder.h b/src/storm/builder/ExplicitModelBuilder.h index f33b37ba3..6538c72c1 100644 --- a/src/storm/builder/ExplicitModelBuilder.h +++ b/src/storm/builder/ExplicitModelBuilder.h @@ -35,12 +35,12 @@ namespace storm { namespace utility { template class ConstantsComparator; } - + namespace builder { - + using namespace storm::utility::prism; using namespace storm::generator; - + // Forward-declare classes. template class RewardModelBuilder; class StateAndChoiceInformationBuilder; @@ -59,21 +59,21 @@ namespace storm { VariableInformation varInfo; storm::storage::BitVectorHashMap stateToId; }; - + template, typename StateType = uint32_t> class ExplicitModelBuilder { public: - + struct Options { /*! * Creates an object representing the default building options. */ Options(); - + // The order in which to explore the model. ExplorationOrder explorationOrder; }; - + /*! * 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. */ 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 * 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. */ StateType getOrAddStateIndex(CompressedState const& state); - + /*! * Builds the transition matrix and the transition reward matrix based for the given program. *