JaniScopeChanger.h

Go to the documentation of this file.

#pragma once
 
#include <cstdint>
#include <optional>
#include <vector>
 
#include "storm/utility/OptionalRef.h"
 
namespace storm {
 
namespace expressions {
class Variable;
}
 
namespace jani {
 
class Model;
class Property;
 
class JaniScopeChanger {
   public:
    JaniScopeChanger() = default;
 
    void makeVariableGlobal(storm::expressions::Variable const& variable, Model& model) const;
 
    void makeVariableLocal(storm::expressions::Variable const& variable, Model& model, uint64_t automatonIndex) const;
 
    bool canMakeVariableGlobal(storm::expressions::Variable const& variable, Model const& model) const;
 
    std::pair<bool, uint64_t> canMakeVariableLocal(storm::expressions::Variable const& variable, Model const& model,
                                                   storm::OptionalRef<std::vector<Property> const> properties = storm::NullRef,
                                                   std::optional<uint64_t> automatonIndex = std::nullopt) const;
 
    void makeVariablesGlobal(Model& model) const;
 
    void makeVariablesLocal(Model& model, storm::OptionalRef<std::vector<Property> const> properties = storm::NullRef) const;
};
}  // namespace jani
 
}  // namespace storm