TimeTravelling.h

Go to the documentation of this file.

#pragma once
 
#include <cstdint>
#include <set>
#include "storm-pars/utility/parametric.h"
#include "storm/adapters/RationalFunctionAdapter.h"
#include "storm/modelchecker/CheckTask.h"
#include "storm/models/sparse/Dtmc.h"
#include "storm/models/sparse/StateLabeling.h"
#include "storm/storage/FlexibleSparseMatrix.h"
 
namespace storm {
namespace transformer {
 
class TimeTravelling {
   public:
    TimeTravelling() = default;
    models::sparse::Dtmc<RationalFunction> timeTravel(models::sparse::Dtmc<RationalFunction> const& model,
                                                      modelchecker::CheckTask<logic::Formula, RationalFunction> const& checkTask);
 
   private:
    void updateTreeStates(std::map<RationalFunctionVariable, std::map<uint64_t, std::set<uint64_t>>>& treeStates,
                          std::map<RationalFunctionVariable, std::set<uint64_t>>& workingSets, storage::FlexibleSparseMatrix<RationalFunction>& flexibleMatrix,
                          const std::set<carl::Variable>& allParameters, const boost::optional<std::vector<RationalFunction>>& stateRewardVector,
                          const models::sparse::StateLabeling stateLabelling, const std::set<std::string> labelsInFormula);
 
    models::sparse::StateLabeling extendStateLabeling(models::sparse::StateLabeling const& oldLabeling, uint64_t oldSize, uint64_t newSize,
                                                      uint64_t stateWithLabels, const std::set<std::string> labelsInFormula);
    std::vector<storm::storage::MatrixEntry<uint64_t, RationalFunction>> joinDuplicateTransitions(
        std::vector<storm::storage::MatrixEntry<uint64_t, RationalFunction>> const& entries);
    bool collapseConstantTransitions(uint64_t state, storage::FlexibleSparseMatrix<RationalFunction>& matrix, std::map<uint64_t, bool>& alreadyVisited,
                                     const std::map<RationalFunctionVariable, std::map<uint64_t, std::set<uint64_t>>>& treeStates,
                                     const std::set<carl::Variable>& allParameters, const boost::optional<std::vector<RationalFunction>>& stateRewardVector,
                                     const models::sparse::StateLabeling stateLabelling, const std::set<std::string> labelsInFormula);
};
 
}  // namespace transformer
}  // namespace storm