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/utility/OptionalRef.h"
 
#include "storm/builder/TerminalStatesGetter.h"
#include "storm/logic/Formula.h"
 
namespace storm {
class Environment;
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, storm::OptionalRef<std::vector<storm::jani::Property> const> properties = storm::NullRef);
 
    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;
 
        // A flag that indicates whether deadlock states should be fixed by inserting a self-loop. If not set,
        // an error is raised whenever a deadlock state is encountered.
        bool fixDeadlocks = true;
    };

    std::shared_ptr<storm::models::symbolic::Model<Type, ValueType>> build(storm::Environment const& env, storm::jani::Model const& model,
                                                                           Options const& options = Options());
};
 
}  // namespace builder
}  // namespace storm