Line data    Source code

       1             : // Author(s): Wieger Wesselink
       2             : // Copyright: see the accompanying file COPYING or copy at
       3             : // https://github.com/mCRL2org/mCRL2/blob/master/COPYING
       4             : //
       5             : // Distributed under the Boost Software License, Version 1.0.
       6             : // (See accompanying file LICENSE_1_0.txt or copy at
       7             : // http://www.boost.org/LICENSE_1_0.txt)
       8             : //
       9             : /// \file mcrl2/modal_formula/state_formula_specification.h
      10             : /// \brief add your file description here.
      11             : 
      12             : #ifndef MCRL2_MODAL_FORMULA_STATE_FORMULA_SPECIFICATION_H
      13             : #define MCRL2_MODAL_FORMULA_STATE_FORMULA_SPECIFICATION_H
      14             : 
      15             : #include "mcrl2/modal_formula/state_formula.h"
      16             : 
      17             : namespace mcrl2 {
      18             : 
      19             : namespace state_formulas {
      20             : 
      21             : class state_formula_specification
      22             : {
      23             :   protected:
      24             :     /// \brief The data specification of the specification
      25             :     data::data_specification m_data;
      26             : 
      27             :     /// \brief The action specification of the specification
      28             :     process::action_label_list m_action_labels;
      29             : 
      30             :     /// \brief The formula of the specification
      31             :     state_formula m_formula;
      32             : 
      33             :   public:
      34             :     /// \brief Constructor.
      35           5 :     state_formula_specification()
      36           5 :     {}
      37             : 
      38             :     /// \brief Constructor of a state formula specification.
      39           4 :     state_formula_specification(const state_formula& formula, const data::data_specification& data = data::data_specification(), const process::action_label_list& action_labels = {})
      40           4 :       : m_data(data),
      41           4 :         m_action_labels(action_labels),
      42           4 :         m_formula(formula)
      43           4 :     {}
      44             : 
      45             :     /// \brief Returns the data specification
      46             :     /// \return The data specification
      47           5 :     const data::data_specification& data() const
      48             :     {
      49           5 :       return m_data;
      50             :     }
      51             : 
      52             :     /// \brief Returns the data specification
      53             :     /// \return The data specification
      54          10 :     data::data_specification& data()
      55             :     {
      56          10 :       return m_data;
      57             :     }
      58             : 
      59             :     /// \brief Returns the action label specification
      60             :     /// \return The action label specification
      61           5 :     const process::action_label_list& action_labels() const
      62             :     {
      63           5 :       return m_action_labels;
      64             :     }
      65             : 
      66             :     /// \brief Returns the action label specification
      67             :     /// \return The action label specification
      68          10 :     process::action_label_list& action_labels()
      69             :     {
      70          10 :       return m_action_labels;
      71             :     }
      72             : 
      73             :     /// \brief Returns the formula of the state formula specification
      74             :     /// \return The formula of the state formula specification
      75           9 :     const state_formula& formula() const
      76             :     {
      77           9 :       return m_formula;
      78             :     }
      79             : 
      80             :     /// \brief Returns the formula of the state formula specification
      81             :     /// \return The formula of the state formula specification
      82          25 :     state_formula& formula()
      83             :     {
      84          25 :       return m_formula;
      85             :     }
      86             : };
      87             : 
      88             : //--- start generated classes ---//
      89             : // prototype declaration
      90             : std::string pp(const state_formula_specification& x);
      91             : 
      92             : /// \\brief Outputs the object to a stream
      93             : /// \\param out An output stream
      94             : /// \\param x Object x
      95             : /// \\return The output stream
      96             : inline
      97             : std::ostream& operator<<(std::ostream& out, const state_formula_specification& x)
      98             : {
      99             :   return out << state_formulas::pp(x);
     100             : }
     101             : //--- end generated classes ---//
     102             : 
     103             : } // namespace state_formulas
     104             : 
     105             : } // namespace mcrl2
     106             : 
     107             : #endif // MCRL2_MODAL_FORMULA_STATE_FORMULA_SPECIFICATION_H