DdJaniModelBuilder.h

Go to the documentation of this file.

#pragma once
 
#include <boost/optional.hpp>
 
#include "storm/storage/dd/DdType.h"
#include "storm/storage/expressions/Variable.h"
#include "storm/storage/jani/Property.h"
 
#include "storm/builder/TerminalStatesGetter.h"
#include "storm/logic/Formula.h"
 
namespace storm {
namespace models {
namespace symbolic {
template<storm::dd::DdType Type, typename ValueType>
class Model;
}
}  // namespace models
namespace jani {
class Model;
class ModelFeatures;
}  // namespace jani
 
namespace builder {
 
template<storm::dd::DdType Type, typename ValueType = double>
class DdJaniModelBuilder {
   public:
    static storm::jani::ModelFeatures getSupportedJaniFeatures();
 
    static bool canHandle(storm::jani::Model const& model, boost::optional<std::vector<storm::jani::Property>> const& properties = boost::none);
 
    struct Options {
        Options(bool buildAllLabels = false, bool buildAllRewardModels = false, bool applyMaximumProgressAssumption = true);
 
        Options(storm::logic::Formula const& formula);
 
        Options(std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas);
 
        void preserveFormula(storm::logic::Formula const& formula);
 
        void setTerminalStatesFromFormula(storm::logic::Formula const& formula);
 
        std::set<std::string> const& getRewardModelNames() const;
 
        void addLabel(std::string const& labelName);
 
        bool isBuildAllLabelsSet() const;
 
        bool buildAllLabels;
 
        bool isBuildAllRewardModelsSet() const;
 
        // A flag that indicates whether or not all reward models are to be build.
        bool buildAllRewardModels;
 
        bool applyMaximumProgressAssumption;
 
        std::set<std::string> labelNames;
 
        // A list of reward models to be build in case not all reward models are to be build.
        std::set<std::string> rewardModelsToBuild;
 
        // An optional mapping that, if given, contains defining expressions for undefined constants.
        boost::optional<std::map<storm::expressions::Variable, storm::expressions::Expression>> constantDefinitions;
 
        // An optional set of expression or labels that characterizes (a subset of) the terminal states of the model.
        // If this is set, the outgoing transitions of these states are replaced with a self-loop.
        storm::builder::TerminalStates terminalStates;
    };
 
    std::shared_ptr<storm::models::symbolic::Model<Type, ValueType>> build(storm::jani::Model const& model, Options const& options = Options());
};
 
}  // namespace builder
}  // namespace storm