LCOV - code coverage report
Current view: top level - pbes/source - pbes.cpp (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 64 92 69.6 %
Date: 2020-02-28 00:44:21 Functions: 29 48 60.4 %
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 pbes.cpp
      10             : /// \brief
      11             : 
      12             : #include "mcrl2/pbes/detail/has_propositional_variables.h"
      13             : #include "mcrl2/pbes/detail/instantiate_global_variables.h"
      14             : #include "mcrl2/pbes/detail/is_well_typed.h"
      15             : #include "mcrl2/pbes/detail/occurring_variable_visitor.h"
      16             : #include "mcrl2/pbes/index_traits.h"
      17             : #include "mcrl2/pbes/is_bes.h"
      18             : #include "mcrl2/pbes/parse_impl.h"
      19             : #include "mcrl2/pbes/print.h"
      20             : #include "mcrl2/pbes/translate_user_notation.h"
      21             : 
      22             : namespace mcrl2
      23             : {
      24             : 
      25             : namespace pbes_system
      26             : {
      27             : 
      28             : //--- start generated pbes_system overloads ---//
      29           0 : std::string pp(const pbes_system::pbes_equation_vector& x) { return pbes_system::pp< pbes_system::pbes_equation_vector >(x); }
      30           0 : std::string pp(const pbes_system::pbes_expression_list& x) { return pbes_system::pp< pbes_system::pbes_expression_list >(x); }
      31           0 : std::string pp(const pbes_system::pbes_expression_vector& x) { return pbes_system::pp< pbes_system::pbes_expression_vector >(x); }
      32           0 : std::string pp(const pbes_system::propositional_variable_list& x) { return pbes_system::pp< pbes_system::propositional_variable_list >(x); }
      33           0 : std::string pp(const pbes_system::propositional_variable_vector& x) { return pbes_system::pp< pbes_system::propositional_variable_vector >(x); }
      34           0 : std::string pp(const pbes_system::propositional_variable_instantiation_list& x) { return pbes_system::pp< pbes_system::propositional_variable_instantiation_list >(x); }
      35           0 : std::string pp(const pbes_system::propositional_variable_instantiation_vector& x) { return pbes_system::pp< pbes_system::propositional_variable_instantiation_vector >(x); }
      36           0 : std::string pp(const pbes_system::and_& x) { return pbes_system::pp< pbes_system::and_ >(x); }
      37           0 : std::string pp(const pbes_system::exists& x) { return pbes_system::pp< pbes_system::exists >(x); }
      38          88 : std::string pp(const pbes_system::fixpoint_symbol& x) { return pbes_system::pp< pbes_system::fixpoint_symbol >(x); }
      39           0 : std::string pp(const pbes_system::forall& x) { return pbes_system::pp< pbes_system::forall >(x); }
      40           0 : std::string pp(const pbes_system::imp& x) { return pbes_system::pp< pbes_system::imp >(x); }
      41           0 : std::string pp(const pbes_system::not_& x) { return pbes_system::pp< pbes_system::not_ >(x); }
      42           0 : std::string pp(const pbes_system::or_& x) { return pbes_system::pp< pbes_system::or_ >(x); }
      43         190 : std::string pp(const pbes_system::pbes& x) { return pbes_system::pp< pbes_system::pbes >(x); }
      44           0 : std::string pp(const pbes_system::pbes_equation& x) { return pbes_system::pp< pbes_system::pbes_equation >(x); }
      45        6533 : std::string pp(const pbes_system::pbes_expression& x) { return pbes_system::pp< pbes_system::pbes_expression >(x); }
      46          77 : std::string pp(const pbes_system::propositional_variable& x) { return pbes_system::pp< pbes_system::propositional_variable >(x); }
      47          74 : std::string pp(const pbes_system::propositional_variable_instantiation& x) { return pbes_system::pp< pbes_system::propositional_variable_instantiation >(x); }
      48           0 : void normalize_sorts(pbes_system::pbes_equation_vector& x, const data::sort_specification& sortspec) { pbes_system::normalize_sorts< pbes_system::pbes_equation_vector >(x, sortspec); }
      49         471 : void normalize_sorts(pbes_system::pbes& x, const data::sort_specification& /* sortspec */) { pbes_system::normalize_sorts< pbes_system::pbes >(x, x.data()); }
      50           2 : pbes_system::pbes_expression normalize_sorts(const pbes_system::pbes_expression& x, const data::sort_specification& sortspec) { return pbes_system::normalize_sorts< pbes_system::pbes_expression >(x, sortspec); }
      51         469 : void translate_user_notation(pbes_system::pbes& x) { pbes_system::translate_user_notation< pbes_system::pbes >(x); }
      52           1 : pbes_system::pbes_expression translate_user_notation(const pbes_system::pbes_expression& x) { return pbes_system::translate_user_notation< pbes_system::pbes_expression >(x); }
      53         606 : std::set<data::sort_expression> find_sort_expressions(const pbes_system::pbes& x) { return pbes_system::find_sort_expressions< pbes_system::pbes >(x); }
      54           1 : std::set<data::variable> find_all_variables(const pbes_system::pbes& x) { return pbes_system::find_all_variables< pbes_system::pbes >(x); }
      55         163 : std::set<data::variable> find_free_variables(const pbes_system::pbes& x) { return pbes_system::find_free_variables< pbes_system::pbes >(x); }
      56        1247 : std::set<data::variable> find_free_variables(const pbes_system::pbes_expression& x) { return pbes_system::find_free_variables< pbes_system::pbes_expression >(x); }
      57           2 : std::set<data::variable> find_free_variables(const pbes_system::pbes_equation& x) { return pbes_system::find_free_variables< pbes_system::pbes_equation >(x); }
      58          22 : std::set<data::function_symbol> find_function_symbols(const pbes_system::pbes& x) { return pbes_system::find_function_symbols< pbes_system::pbes >(x); }
      59        3718 : std::set<pbes_system::propositional_variable_instantiation> find_propositional_variable_instantiations(const pbes_system::pbes_expression& x) { return pbes_system::find_propositional_variable_instantiations< pbes_system::pbes_expression >(x); }
      60         907 : std::set<core::identifier_string> find_identifiers(const pbes_system::pbes_expression& x) { return pbes_system::find_identifiers< pbes_system::pbes_expression >(x); }
      61           0 : bool search_variable(const pbes_system::pbes_expression& x, const data::variable& v) { return pbes_system::search_variable< pbes_system::pbes_expression >(x, v); }
      62             : //--- end generated pbes_system overloads ---//
      63             : 
      64             : namespace algorithms {
      65             : 
      66          36 : void instantiate_global_variables(pbes& p)
      67             : {
      68          36 :   pbes_system::detail::instantiate_global_variables(p);
      69          36 : }
      70             : 
      71           2 : bool is_bes(const pbes& x)
      72             : {
      73           2 :   return pbes_system::is_bes(x);
      74             : }
      75             : 
      76             : } // namespace algorithms
      77             : 
      78           0 : bool is_well_typed(const pbes_equation& eqn)
      79             : {
      80           0 :   return pbes_system::detail::is_well_typed(eqn);
      81             : }
      82             : 
      83         486 : bool is_well_typed_equation(const pbes_equation& eqn,
      84             :                             const std::set<data::sort_expression>& declared_sorts,
      85             :                             const std::set<data::variable>& declared_global_variables,
      86             :                             const data::data_specification& data_spec
      87             :                            )
      88             : {
      89         486 :   return pbes_system::detail::is_well_typed_equation(eqn, declared_sorts, declared_global_variables, data_spec);
      90             : }
      91             : 
      92         105 : bool is_well_typed_pbes(const std::set<data::sort_expression>& declared_sorts,
      93             :                         const std::set<data::variable>& declared_global_variables,
      94             :                         const std::set<data::variable>& occurring_global_variables,
      95             :                         const std::set<propositional_variable>& declared_variables,
      96             :                         const std::set<propositional_variable_instantiation>& occ,
      97             :                         const propositional_variable_instantiation& init,
      98             :                         const data::data_specification& data_spec
      99             :                        )
     100             : {
     101         105 :   return pbes_system::detail::is_well_typed_pbes(declared_sorts, declared_global_variables, occurring_global_variables, declared_variables, occ, init, data_spec);
     102             : }
     103             : 
     104           0 : bool pbes_equation::is_solved() const
     105             : {
     106           0 :   return !detail::has_propositional_variables(formula());
     107             : }
     108             : 
     109         304 : std::set<propositional_variable_instantiation> pbes::occurring_variable_instantiations() const
     110             : {
     111         304 :   std::set<propositional_variable_instantiation> result;
     112        1371 :   for (const pbes_equation& eqn: equations())
     113             :   {
     114        2134 :     detail::occurring_variable_visitor f;
     115        1067 :     f.apply(eqn.formula());
     116        1067 :     result.insert(f.variables.begin(), f.variables.end());
     117             :   }
     118         304 :   return result;
     119             : }
     120             : 
     121          42 : static bool register_hooks()
     122             : {
     123          42 :   register_propositional_variable_instantiation_hooks();
     124          42 :   return true;
     125             : }
     126          42 : static bool mcrl2_register_pbes(register_hooks());
     127             : 
     128             : namespace detail {
     129             : 
     130           0 : pbes_expression parse_pbes_expression_new(const std::string& text)
     131             : {
     132           0 :   core::parser p(parser_tables_mcrl2, core::detail::ambiguity_fn, core::detail::syntax_error_fn);
     133           0 :   unsigned int start_symbol_index = p.start_symbol_index("PbesExpr");
     134           0 :   bool partial_parses = false;
     135           0 :   core::parse_node node = p.parse(text, start_symbol_index, partial_parses);
     136           0 :   core::warn_and_or(node);
     137           0 :   pbes_expression result = pbes_actions(p).parse_PbesExpr(node);
     138           0 :   return result;
     139             : }
     140             : 
     141         471 : untyped_pbes parse_pbes_new(const std::string& text)
     142             : {
     143         942 :   core::parser p(parser_tables_mcrl2, core::detail::ambiguity_fn, core::detail::syntax_error_fn);
     144         471 :   unsigned int start_symbol_index = p.start_symbol_index("PbesSpec");
     145         471 :   bool partial_parses = false;
     146         942 :   core::parse_node node = p.parse(text, start_symbol_index, partial_parses);
     147         471 :   core::warn_and_or(node);
     148         471 :   untyped_pbes result = pbes_actions(p).parse_PbesSpec(node);
     149         942 :   return result;
     150             : }
     151             : 
     152         469 : void complete_pbes(pbes& x)
     153             : {
     154         469 :   typecheck_pbes(x);
     155         469 :   pbes_system::translate_user_notation(x);
     156         469 :   complete_data_specification(x);
     157         469 : }
     158             : 
     159           2 : propositional_variable parse_propositional_variable(const std::string& text)
     160             : {
     161           4 :   core::parser p(parser_tables_mcrl2, core::detail::ambiguity_fn, core::detail::syntax_error_fn);
     162           2 :   unsigned int start_symbol_index = p.start_symbol_index("PropVarDecl");
     163           2 :   bool partial_parses = false;
     164           4 :   core::parse_node node = p.parse(text, start_symbol_index, partial_parses);
     165           4 :   return detail::pbes_actions(p).parse_PropVarDecl(node);
     166             : }
     167             : 
     168           1 : pbes_expression parse_pbes_expression(const std::string& text)
     169             : {
     170           2 :   core::parser p(parser_tables_mcrl2, core::detail::ambiguity_fn, core::detail::syntax_error_fn);
     171           1 :   unsigned int start_symbol_index = p.start_symbol_index("PbesExpr");
     172           1 :   bool partial_parses = false;
     173           2 :   core::parse_node node = p.parse(text, start_symbol_index, partial_parses);
     174           1 :   core::warn_and_or(node);
     175           2 :   return detail::pbes_actions(p).parse_PbesExpr(node);
     176             : }
     177             : 
     178             : } // namespace detail
     179             : 
     180             : } // namespace pbes_system
     181             : 
     182         126 : } // namespace mcrl2
     183             : 

Generated by: LCOV version 1.13