VariableSet.h

Go to the documentation of this file.

#pragma once
 
#include <set>
#include <vector>
 
#include "storm/adapters/DereferenceIteratorAdapter.h"
 
#include "storm/storage/jani/Variable.h"
 
namespace storm {
namespace jani {
 
namespace detail {
template<typename VariableType>
using Variables = storm::adapters::DereferenceIteratorAdapter<std::vector<std::shared_ptr<VariableType>>>;
 
template<typename VariableType>
using ConstVariables = storm::adapters::DereferenceIteratorAdapter<std::vector<std::shared_ptr<VariableType>> const>;
}  // namespace detail
 
class VariableSet {
   public:
    VariableSet();
 
    detail::Variables<Variable> getBooleanVariables();
 
    detail::ConstVariables<Variable> getBooleanVariables() const;
 
    detail::Variables<Variable> getBoundedIntegerVariables();
 
    detail::ConstVariables<Variable> getBoundedIntegerVariables() const;
 
    detail::Variables<Variable> getUnboundedIntegerVariables();
 
    detail::ConstVariables<Variable> getUnboundedIntegerVariables() const;
 
    detail::Variables<Variable> getRealVariables();
 
    detail::ConstVariables<Variable> getRealVariables() const;
 
    detail::Variables<Variable> getArrayVariables();
 
    detail::ConstVariables<Variable> getArrayVariables() const;
 
    detail::Variables<Variable> getClockVariables();
 
    detail::ConstVariables<Variable> getClockVariables() const;
 
    detail::Variables<Variable> getContinuousVariables();
 
    detail::ConstVariables<Variable> getContinuousVariables() const;
 
    Variable const& addVariable(Variable const& variable);
 
    std::vector<std::shared_ptr<Variable>> dropAllArrayVariables();
 
    bool hasVariable(std::string const& name) const;
 
    Variable const& getVariable(std::string const& name) const;
 
    bool hasVariable(storm::jani::Variable const& variable) const;
 
    bool hasVariable(storm::expressions::Variable const& variable) const;
 
    Variable const& getVariable(storm::expressions::Variable const& variable) const;
 
    std::shared_ptr<Variable> eraseVariable(storm::expressions::Variable const& variable);
 
    bool hasTransientVariable() const;
 
    typename detail::Variables<Variable>::iterator begin();
 
    typename detail::ConstVariables<Variable>::iterator begin() const;
 
    typename detail::Variables<Variable>::iterator end();
 
    typename detail::ConstVariables<Variable>::iterator end() const;
 
    bool containsBooleanVariable() const;
 
    bool containsBoundedIntegerVariable() const;
 
    bool containsUnboundedIntegerVariables() const;
 
    bool containsRealVariables() const;
 
    bool containsArrayVariables() const;
 
    bool containsClockVariables() const;
 
    bool containsContinuousVariables() const;
 
    bool containsNonTransientRealVariables() const;
 
    bool containsNonTransientUnboundedIntegerVariables() const;
 
    bool empty() const;
 
    uint64_t getNumberOfVariables() const;
 
    /*
     * Total number of nontransient variables
     */
    uint64_t getNumberOfNontransientVariables() const;
 
    uint64_t getNumberOfTransientVariables() const;
 
    uint64_t getNumberOfRealTransientVariables() const;
 
    uint64_t getNumberOfUnboundedIntegerTransientVariables() const;
 
    uint64_t getNumberOfNumericalTransientVariables() const;
 
    typename detail::ConstVariables<Variable> getTransientVariables() const;
 
    bool containsVariablesInBoundExpressionsOrInitialValues(std::set<storm::expressions::Variable> const& variables) const;
 
    std::map<std::string, std::reference_wrapper<Variable const>> getNameToVariableMap() const;
 
    void substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution, bool const substituteTranscendentalNumbers);
 
    void substituteExpressionVariables(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution);
 
   private:
    std::vector<std::shared_ptr<Variable>>& getVariableVectorForType(JaniType const& type);
 
    std::vector<std::shared_ptr<Variable>> variables;
 
    std::vector<std::shared_ptr<Variable>> booleanVariables;
 
    std::vector<std::shared_ptr<Variable>> boundedIntegerVariables;
 
    std::vector<std::shared_ptr<Variable>> unboundedIntegerVariables;
 
    std::vector<std::shared_ptr<Variable>> realVariables;
 
    std::vector<std::shared_ptr<Variable>> arrayVariables;
 
    std::vector<std::shared_ptr<Variable>> clockVariables;
 
    std::vector<std::shared_ptr<Variable>> continuousVariables;
 
    std::vector<std::shared_ptr<Variable>> transientVariables;
 
    std::map<std::string, storm::expressions::Variable> nameToVariable;
 
    std::map<storm::expressions::Variable, std::shared_ptr<Variable>> variableToVariable;
};
 
}  // namespace jani
}  // namespace storm