StaminaModelChecker.h

#ifndef STAMINA_CORE_STAMINAMODELCHECKER_H
#define STAMINA_CORE_STAMINAMODELCHECKER_H
 
#include "Options.h"
#include "builder/StaminaModelBuilder.h"
#include "builder/StaminaIterativeModelBuilder.h"
// #include "builder/StaminaPriorityModelBuilder.h"
#include "builder/StaminaReExploringModelBuilder.h"
 
#include <sstream>
#include <string>
#include <unordered_set>
 
#include "__storm_needed_for_checker.h"
 
namespace stamina {
    namespace core {
        using namespace stamina::builder;
        const uint32_t absorbingStateIndex = 0;
        class StaminaModelChecker {
        public:
            StaminaModelChecker(
                std::shared_ptr<storm::prism::Program> modulesFile = nullptr
                , std::shared_ptr<std::vector<storm::jani::Property>> propertiesVector = nullptr
            );
            ~StaminaModelChecker();
            void initialize(
                std::shared_ptr<storm::prism::Program> modulesFile = nullptr
                , std::shared_ptr<std::vector<storm::jani::Property>> propertiesVector = nullptr
            );
            std::unique_ptr<storm::modelchecker::CheckResult> modelCheckProperty(
                storm::jani::Property propMin
                , storm::jani::Property propMax
                , storm::prism::Program const& modulesFile
            );
        private:
            class Result {
            public:
                Result()
                    : result(0.0)
                    , explanation("")
                {
                    // Intentionally left empty
                }
                operator std::string() const {
                    std::stringstream str;
                    str << result << " (" << explanation << ")";
                    return str.str();
                }
                friend std::ostream & operator<<(std::ostream & stream, StaminaModelChecker::Result const & r) {
                    stream << r.result << " (" << r.explanation << ")";
                    return stream;
                }
 
                double result;
                std::string explanation;
 
            };
            bool terminateModelCheck();
            void writePerimeterStates(int numRefineIteration);
            void printTransitionActions(std::string const & filename);
            void writeToOutput(std::string filename);
            void modifyState(bool isMin);
            /* Data Members */
            std::shared_ptr<StaminaModelChecker::Result> min_results;
            std::shared_ptr<StaminaModelChecker::Result> max_results;
            std::shared_ptr<StaminaModelBuilder<double>> builder;
            std::shared_ptr<storm::prism::Program> modulesFile;
            std::shared_ptr<std::vector<storm::jani::Property>> propertiesVector;
            storm::expressions::ExpressionManager expressionManager;
            storm::models::sparse::StateLabeling * labeling;
            std::string preUntilLabel;
        };
    } // namespace core
} // namespace stamina
 
#endif // STAMINA_CORE_STAMINAMODELCHECKER_H