LCOV - code coverage report
Current view: top level - bes/include/mcrl2/bes - boolean_equation_system.h (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 27 29 93.1 %
Date: 2020-10-20 00:45:57 Functions: 12 13 92.3 %
Legend: Lines: hit not hit

          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/bes/boolean_equation_system.h
      10             : /// \brief add your file description here.
      11             : 
      12             : #ifndef MCRL2_BES_BOOLEAN_EQUATION_SYSTEM_H
      13             : #define MCRL2_BES_BOOLEAN_EQUATION_SYSTEM_H
      14             : 
      15             : #include "mcrl2/bes/boolean_equation.h"
      16             : 
      17             : namespace mcrl2
      18             : {
      19             : 
      20             : namespace bes
      21             : {
      22             : 
      23             : // forward declarations
      24             : class boolean_equation_system;
      25             : 
      26             : atermpp::aterm_appl boolean_equation_system_to_aterm(const boolean_equation_system& p);
      27             : 
      28             : /// \brief boolean equation system
      29             : // <BES>          ::= BES(<BooleanEquation>*, <BooleanExpression>)
      30          65 : class boolean_equation_system
      31             : {
      32             :   public:
      33             :     typedef boolean_equation equation_type;
      34             : 
      35             :   protected:
      36             :     /// \brief The equations
      37             :     std::vector<boolean_equation> m_equations;
      38             : 
      39             :     /// \brief The initial state
      40             :     boolean_expression m_initial_state;
      41             : 
      42             :   public:
      43             :     /// \brief Constructor.
      44          23 :     boolean_equation_system()
      45          23 :       : m_initial_state(core::term_traits<boolean_expression>::true_())
      46          23 :     {}
      47             : 
      48             :     /// \brief Constructor.
      49             :     /// \param equations A sequence of boolean equations
      50             :     /// \param initial_state An initial state
      51          23 :     boolean_equation_system(
      52             :       const std::vector<boolean_equation>& equations,
      53             :       boolean_expression initial_state)
      54          23 :       :
      55             :       m_equations(equations),
      56          23 :       m_initial_state(initial_state)
      57          23 :     {}
      58             : 
      59             :     /// \brief Returns the equations.
      60             :     /// \return The equations
      61          82 :     const std::vector<boolean_equation>& equations() const
      62             :     {
      63          82 :       return m_equations;
      64             :     }
      65             : 
      66             :     /// \brief Returns the equations.
      67             :     /// \return The equations
      68          63 :     std::vector<boolean_equation>& equations()
      69             :     {
      70          63 :       return m_equations;
      71             :     }
      72             : 
      73             :     /// \brief Returns the initial state.
      74             :     /// \return The initial state.
      75          39 :     const boolean_expression& initial_state() const
      76             :     {
      77          39 :       return m_initial_state;
      78             :     }
      79             : 
      80             :     /// \brief Returns the initial state.
      81             :     /// \return The initial state.
      82          38 :     boolean_expression& initial_state()
      83             :     {
      84          38 :       return m_initial_state;
      85             :     }
      86             : 
      87             :     /// \brief Returns true.
      88             :     /// Some checks will be added later.
      89             :     /// \return The value true.
      90             :     bool is_well_typed() const
      91             :     {
      92             :       return true;
      93             :     }
      94             : 
      95             :     /// \brief Returns the set of binding variables of the boolean_equation_system, i.e. the
      96             :     /// variables that occur on the left hand side of an equation.
      97             :     /// \return The binding variables of the equation system
      98           2 :     std::set<boolean_variable> binding_variables() const
      99             :     {
     100           2 :       std::set<boolean_variable> result;
     101           7 :       for (const boolean_equation& eqn: equations())
     102             :       {
     103           5 :         result.insert(eqn.variable());
     104             :       }
     105           2 :       return result;
     106             :     }
     107             : 
     108             :     /// \brief Returns the set of occurring variables of the boolean_equation_system, i.e.
     109             :     /// the variables that occur in the right hand side of an equation or in the
     110             :     /// initial state.
     111             :     /// \return The occurring variables of the equation system
     112             :     std::set<boolean_variable> occurring_variables() const;
     113             : 
     114             :     /// \brief Returns true if all occurring variables are binding variables.
     115             :     /// \return True if the equation system is closed
     116           1 :     bool is_closed() const
     117             :     {
     118           2 :       std::set<boolean_variable> bnd = binding_variables();
     119           2 :       std::set<boolean_variable> occ = occurring_variables();
     120           2 :       return std::includes(bnd.begin(), bnd.end(), occ.begin(), occ.end()) && bnd.find(boolean_variable(initial_state())) != bnd.end();
     121             :     }
     122             : };
     123             : 
     124             : //--- start generated class boolean_equation_system ---//
     125             : // prototype declaration
     126             : std::string pp(const boolean_equation_system& x);
     127             : 
     128             : /// \brief Outputs the object to a stream
     129             : /// \param out An output stream
     130             : /// \param x Object x
     131             : /// \return The output stream
     132             : inline
     133           0 : std::ostream& operator<<(std::ostream& out, const boolean_equation_system& x)
     134             : {
     135           0 :   return out << bes::pp(x);
     136             : }
     137             : //--- end generated class boolean_equation_system ---//
     138             : 
     139             : inline
     140           1 : bool operator==(const boolean_equation_system& x, const boolean_equation_system& y)
     141             : {
     142           1 :         return x.equations() == y.equations() && x.initial_state() == y.initial_state();
     143             : }
     144             : 
     145             : } // namespace bes
     146             : 
     147             : } // namespace mcrl2
     148             : 
     149             : #endif // MCRL2_BES_BOOLEAN_EQUATION_SYSTEM_H

Generated by: LCOV version 1.13