StaminaPriorityModelBuilder.h

#ifndef STAMINA_BUILDER_PRIORITYMODELBUILDER_H
#define STAMINA_BUILDER_PRIORITYMODELBUILDER_H
 
#include "StaminaModelBuilder.h"
 
namespace stamina {
    namespace builder {
        template<typename ValueType, typename RewardModelType = storm::models::sparse::StandardRewardModel<ValueType>, typename StateType = uint32_t>
        class StaminaPriorityModelBuilder : public StaminaModelBuilder<ValueType, RewardModelType, StateType> {
        public:
//          typedef typename StaminaModelBuilder<ValueType, RewardModelType, StateType>::ProbabilityState ProbabilityState;
            StaminaPriorityModelBuilder(
                std::shared_ptr<storm::generator::PrismNextStateGenerator<ValueType, StateType>> const& generator
                , storm::prism::Program const& modulesFile
                , storm::generator::NextStateGeneratorOptions const & options
            );
            StaminaPriorityModelBuilder(
                storm::prism::Program const& program
                , storm::generator::NextStateGeneratorOptions const& generatorOptions = storm::generator::NextStateGeneratorOptions()
            );
            StateType getOrAddStateIndex(CompressedState const& state) override;
            storm::storage::sparse::ModelComponents<ValueType, RewardModelType> buildModelComponents() override;
            void buildMatrices(
                storm::storage::SparseMatrixBuilder<ValueType>& transitionMatrixBuilder
                , std::vector<RewardModelBuilder<typename RewardModelType::ValueType>>& rewardModelBuilders
                , StateAndChoiceInformationBuilder& choiceInformationBuilder
                , boost::optional<storm::storage::BitVector>& markovianChoices
                , boost::optional<storm::storage::sparse::StateValuationsBuilder>& stateValuationsBuilder
            ) override;
        private:
            /*
             * Access to data members of parent class
             * */
            using StaminaModelBuilder<ValueType, RewardModelType, StateType>::propertyExpression;
            using StaminaModelBuilder<ValueType, RewardModelType, StateType>::expressionManager;
            using StaminaModelBuilder<ValueType, RewardModelType, StateType>::propertyFormula;
            using StaminaModelBuilder<ValueType, RewardModelType, StateType>::generator;
            using StaminaModelBuilder<ValueType, RewardModelType, StateType>::memoryPool;
            using StaminaModelBuilder<ValueType, RewardModelType, StateType>::statesToExplore;
            using StaminaModelBuilder<ValueType, RewardModelType, StateType>::stateMap;
            using StaminaModelBuilder<ValueType, RewardModelType, StateType>::stateStorage;
            // Options for next state generators
            using StaminaModelBuilder<ValueType, RewardModelType, StateType>::options;
            // The model builder must have access to this to create a fresh next state generator each iteration
            using StaminaModelBuilder<ValueType, RewardModelType, StateType>::modulesFile;
            using StaminaModelBuilder<ValueType, RewardModelType, StateType>::currentProbabilityState;
            using StaminaModelBuilder<ValueType, RewardModelType, StateType>::absorbingState;
            using StaminaModelBuilder<ValueType, RewardModelType, StateType>::absorbingWasSetUp;
            using StaminaModelBuilder<ValueType, RewardModelType, StateType>::isInit;
            using StaminaModelBuilder<ValueType, RewardModelType, StateType>::fresh;
            using StaminaModelBuilder<ValueType, RewardModelType, StateType>::iteration;
            using StaminaModelBuilder<ValueType, RewardModelType, StateType>::firstIteration;
            using StaminaModelBuilder<ValueType, RewardModelType, StateType>::localKappa;
            using StaminaModelBuilder<ValueType, RewardModelType, StateType>::isCtmc;
            using StaminaModelBuilder<ValueType, RewardModelType, StateType>::formulaMatchesExpression;
            using StaminaModelBuilder<ValueType, RewardModelType, StateType>::numberTerminal;
            using StaminaModelBuilder<ValueType, RewardModelType, StateType>::numberStates;
            using StaminaModelBuilder<ValueType, RewardModelType, StateType>::numberTransitions;
            using StaminaModelBuilder<ValueType, RewardModelType, StateType>::currentRowGroup;
            using StaminaModelBuilder<ValueType, RewardModelType, StateType>::currentRow;
            void connectAllTerminalStatesToAbsorbing(storm::storage::SparseMatrixBuilder<ValueType>& transitionMatrixBuilder);
            /* Data members */
            std::priority_queue<
                ProbabilityStatePair<StateType>
                , std::vector<ProbabilityStatePair<StateType>>
                , ProbabilityStatePairComparison<StateType>
            > statePriorityQueue;
            uint64_t numberOfExploredStates;
            uint64_t numberOfExploredStatesSinceLastMessage;
            double piHat;
        };
    }
}
#endif // STAMINA_BUILDER_PRIORITYMODELBUILDER_H