StaminaIterativeModelBuilder.h

#ifndef STAMINA_BUILDER_ITERATIVEMODELBUILDER_H
#define STAMINA_BUILDER_ITERATIVEMODELBUILDER_H
 
#include "StaminaModelBuilder.h"
 
namespace stamina {
    namespace builder {
        template<typename ValueType, typename RewardModelType = storm::models::sparse::StandardRewardModel<ValueType>, typename StateType = uint32_t>
        class StaminaIterativeModelBuilder : public StaminaModelBuilder<ValueType, RewardModelType, StateType> {
        public:
            StaminaIterativeModelBuilder(
                std::shared_ptr<storm::generator::PrismNextStateGenerator<ValueType, StateType>> const& generator
                , storm::prism::Program const& modulesFile
                , storm::generator::NextStateGeneratorOptions const & options
            );
            StaminaIterativeModelBuilder(
                storm::prism::Program const& program
                , storm::generator::NextStateGeneratorOptions const& generatorOptions = storm::generator::NextStateGeneratorOptions()
            );
            virtual 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;
            StateType getOrAddStateIndex(CompressedState const& state) override;
            storm::storage::sparse::ModelComponents<ValueType, RewardModelType> buildModelComponents() override;
        protected:
            /*
             * 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 flushStatesTerminated();
            void connectAllTerminalStatesToAbsorbing(storm::storage::SparseMatrixBuilder<ValueType>& transitionMatrixBuilder);
            // Dynamic programming improvement: we keep an ordered set of the states terminated
            // during the previous iteration (in an order that prevents needing to use a remapping
            // vector for state indecies.
            std::deque<std::pair<ProbabilityState<StateType> *, CompressedState>> statesTerminatedLastIteration;
            uint64_t numberOfExploredStates;
            uint64_t numberOfExploredStatesSinceLastMessage;
        };
        // "Custom" deleter (which actually is not custom) to allow for polymorphic shared pointers
        template<typename ValueType, typename RewardModelType = storm::models::sparse::StandardRewardModel<ValueType>, typename StateType = uint32_t>
        void __delete_stamina_iterative_model_builder(StaminaIterativeModelBuilder<ValueType, RewardModelType, StateType> * t) { delete t; }
    }
}
#endif // STAMINA_BUILDER_ITERATIVEMODELBUILDER_H