StaminaModelBuilder.h

 
#ifndef STAMINA_BUILDER_STAMINAMODELBUILDER_H
#define STAMINA_BUILDER_STAMINAMODELBUILDER_H
 
#include <memory>
#include <utility>
#include <vector>
#include <deque>
#include <queue>
#include <cstdint>
#include <functional>
 
#include "core/Options.h"
#include "core/StaminaMessages.h"
 
#include "util/StateIndexArray.h"
#include "util/StateMemoryPool.h"
 
#include "builder/threads/ExplorationThread.h"
#include "builder/threads/ControlThread.h"
 
#include "builder/ProbabilityState.h"
 
#include <boost/functional/hash.hpp>
#include <boost/container/flat_map.hpp>
#include <boost/variant.hpp>
 
#include "__storm_needed_for_builder.h"
 
// Frequency for info/debug messages in terms of number of states explored.
#define MSG_FREQUENCY 100000
// #define MSG_FREQUENCY 4000
 
namespace stamina {
    namespace builder {
 
        using namespace storm::builder;
        using namespace storm::utility::prism;
        using namespace storm::generator;
 
        using namespace core;
 
        typedef storm::models::sparse::Ctmc<double> Ctmc;
        typedef storm::modelchecker::SparseCtmcCslModelChecker<Ctmc> CtmcModelChecker;
 
 
 
        template<typename ValueType, typename RewardModelType = storm::models::sparse::StandardRewardModel<ValueType>, typename StateType = uint32_t>
        class StaminaModelBuilder {
        public:
 
            typedef typename threads::ControlThread<StateType, RewardModelType, ValueType>::StateAndThreadIndex StateThreadIndex;
            class TransitionInfo {
            public:
                TransitionInfo(StateType from, StateType to, double transition) :
                    from(from), to(to), transition(transition) { /* Intentionally left empty */ }
                StateType from;
                StateType to;
                double transition;
            };
            struct TransitionInfoComparison {
                bool operator() (
                    const TransitionInfo * first
                    , const TransitionInfo * second
                ) const {
                    return first->to > second->to;
                }
            };
 
            StaminaModelBuilder(
                std::shared_ptr<storm::generator::PrismNextStateGenerator<ValueType, StateType>> const& generator
                , storm::prism::Program const& modulesFile
                , storm::generator::NextStateGeneratorOptions const & options
            );
            StaminaModelBuilder(
                storm::prism::Program const& program
                , storm::generator::NextStateGeneratorOptions const& generatorOptions
            );
            std::shared_ptr<storm::models::sparse::Model<ValueType, RewardModelType>> build();
            StateType getStateIndexIfKnown(CompressedState const& state);
            double accumulateProbabilities();
            void reset();
            void setGenerator(
                std::shared_ptr<storm::generator::PrismNextStateGenerator<ValueType, StateType>> generator
            );
            std::vector<StateType> getPerimeterStates();
            void setLocalKappaToGlobal();
            void printStateSpaceInformation();
            storm::expressions::Expression * getPropertyExpression();
            void setPropertyFormula(
                std::shared_ptr<const storm::logic::Formula> formula
                , const storm::prism::Program & modulesFile
            );
            virtual StateType getOrAddStateIndex(CompressedState const& state);
            StateType getStateIndexOrAbsorbing(CompressedState const& state);
            double getLocalKappa();
        protected:
            storm::storage::sparse::StateStorage<StateType> getStateStorage();
            void loadPropertyExpressionFromFormula();
            void connectTerminalStatesToAbsorbing(
                storm::storage::SparseMatrixBuilder<ValueType>& transitionMatrixBuilder
                , CompressedState & terminalState
                , StateType stateId
                , std::function<StateType (CompressedState const&)> stateToIdCallback
            );
            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
            ) = 0;
            void flushToTransitionMatrix(storm::storage::SparseMatrixBuilder<ValueType>& transitionMatrixBuilder);
            void createTransition(StateType from, StateType to, ValueType probability);
            void createTransition(TransitionInfo transitionInfo);
            virtual storm::storage::sparse::ModelComponents<ValueType, RewardModelType> buildModelComponents() = 0;
            storm::models::sparse::StateLabeling buildStateLabeling();
            void setUpAbsorbingState(
                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
            );
 
            /* Data Members */
            std::shared_ptr<threads::ControlThread<StateType, RewardModelType, ValueType>> controlThread;
            std::vector<std::shared_ptr<threads::ExplorationThread<StateType, RewardModelType, ValueType>>> explorationThreads;
 
            std::function<StateType (CompressedState const&)> terminalStateToIdCallback;
 
            storm::expressions::Expression * propertyExpression;
            storm::expressions::ExpressionManager * expressionManager;
            std::shared_ptr<const storm::logic::Formula> propertyFormula;
 
            std::shared_ptr<storm::generator::PrismNextStateGenerator<ValueType, StateType>> generator;
 
            util::StateMemoryPool<ProbabilityState<StateType>> memoryPool;
 
            std::deque<std::pair<ProbabilityState<StateType> *, CompressedState> > statesToExplore;
 
            // The following data members must be accessible to threads
            util::StateIndexArray<StateType, ProbabilityState<StateType>> stateMap;
            storm::storage::sparse::StateStorage<
                StateType
            >& stateStorage;
 
            // Remapping (not used by STAMINA)
            boost::optional<std::vector<uint_fast64_t>> stateRemapping;
 
            // Transitions which we must add
            std::vector<std::vector<TransitionInfo>> transitionsToAdd;
            // Options for next state generators
            storm::generator::NextStateGeneratorOptions const & options;
            // The model builder must have access to this to create a fresh next state generator each iteration
            storm::prism::Program const& modulesFile;
            ProbabilityState<StateType> * currentProbabilityState;
            CompressedState absorbingState;
            bool absorbingWasSetUp;
            bool isInit;
            bool fresh;
            uint8_t iteration;
            bool firstIteration;
            double localKappa;
            bool isCtmc;
            bool formulaMatchesExpression;
            uint64_t numberTerminal;
            uint64_t numberStates;
            uint64_t numberTransitions;
            uint_fast64_t currentRowGroup;
            uint_fast64_t currentRow;
 
        };
 
        // Helper method to find in unordered_set
        template <typename StateType>
        bool set_contains(std::unordered_set<StateType> current_set, StateType value);
    }
}
#endif // STAMINA_BUILDER_STAMINAMODELBUILDER_H