LCOV - code coverage report
Current view: top level - bes/include/mcrl2/bes - bes2pbes.h (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 13 13 100.0 %
Date: 2020-10-20 00:45:57 Functions: 3 3 100.0 %
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/bes2pbes.h
      10             : /// \brief Contains functions to transfrom a BES into a PBES.
      11             : 
      12             : #ifndef MCRL2_BES_BES2PBES_H
      13             : #define MCRL2_BES_BES2PBES_H
      14             : 
      15             : #include "mcrl2/bes/detail/boolean_expression2pbes_expression_traverser.h"
      16             : #include "mcrl2/pbes/pbes.h"
      17             : 
      18             : namespace mcrl2
      19             : {
      20             : 
      21             : namespace bes
      22             : {
      23             : 
      24             : /// \brief Converts a boolean variable into a propositional variable
      25             : /// \param v A boolean variable
      26             : inline
      27             : pbes_system::propositional_variable_instantiation bes2pbes(const boolean_variable& v)
      28             : {
      29             :   return pbes_system::propositional_variable_instantiation(v.name(), data::data_expression_list());
      30             : }
      31             : 
      32             : /// \brief Converts a boolean expression into a PBES expression
      33             : /// \param x A boolean expression
      34             : inline
      35           4 : pbes_system::pbes_expression bes2pbes(const boolean_expression& x)
      36             : {
      37           8 :   bes::detail::boolean_expression2pbes_expression_traverser t;
      38           4 :   t.apply(x);
      39           8 :   return t.result();
      40             : }
      41             : 
      42             : /// \brief Converts a boolean equation into a PBES equation
      43             : /// \param eq A boolean equation
      44             : inline
      45           3 : pbes_system::pbes_equation bes2pbes(const boolean_equation& eq)
      46             : {
      47           3 :   return pbes_system::pbes_equation(eq.symbol(), pbes_system::propositional_variable(eq.variable().name(), data::variable_list()), bes2pbes(eq.formula()));
      48             : }
      49             : 
      50             : /// \brief Converts a BES into a PBES
      51             : /// \param x A boolean expression
      52             : inline
      53           1 : pbes_system::pbes bes2pbes(const boolean_equation_system& x)
      54             : {
      55           2 :   data::data_specification data_spec;
      56           2 :   std::vector<pbes_system::pbes_equation> equations;
      57           4 :   for (const boolean_equation& eqn: x.equations())
      58             :   {
      59           3 :     equations.push_back(bes2pbes(eqn));
      60             :   }
      61           2 :   pbes_system::propositional_variable_instantiation initial_state = atermpp::down_cast<pbes_system::propositional_variable_instantiation>(bes2pbes(x.initial_state()));
      62             : 
      63           2 :   return pbes_system::pbes(data_spec, equations, initial_state);
      64             : }
      65             : 
      66             : } // namespace bes
      67             : 
      68             : } // namespace mcrl2
      69             : 
      70             : #endif // MCRL2_BES_BES2PBES_H

Generated by: LCOV version 1.13