LCOV - code coverage report
Current view: top level - modal_formula/source - modal_formula.cpp (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 31 100 31.0 %
Date: 2020-07-11 00:44:39 Functions: 14 61 23.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 modal_formula.cpp
      10             : /// \brief
      11             : 
      12             : #include "mcrl2/modal_formula/algorithms.h"
      13             : #include "mcrl2/modal_formula/is_timed.h"
      14             : #include "mcrl2/modal_formula/normalize.h"
      15             : #include "mcrl2/modal_formula/parse.h"
      16             : #include "mcrl2/modal_formula/parse_impl.h"
      17             : #include "mcrl2/modal_formula/print.h"
      18             : #include "mcrl2/modal_formula/replace.h"
      19             : 
      20             : namespace mcrl2
      21             : {
      22             : 
      23             : namespace action_formulas
      24             : {
      25             : 
      26             : //--- start generated action_formulas overloads ---//
      27           0 : std::string pp(const action_formulas::action_formula& x) { return action_formulas::pp< action_formulas::action_formula >(x); }
      28           0 : std::string pp(const action_formulas::and_& x) { return action_formulas::pp< action_formulas::and_ >(x); }
      29           0 : std::string pp(const action_formulas::at& x) { return action_formulas::pp< action_formulas::at >(x); }
      30           0 : std::string pp(const action_formulas::exists& x) { return action_formulas::pp< action_formulas::exists >(x); }
      31           0 : std::string pp(const action_formulas::false_& x) { return action_formulas::pp< action_formulas::false_ >(x); }
      32           0 : std::string pp(const action_formulas::forall& x) { return action_formulas::pp< action_formulas::forall >(x); }
      33           0 : std::string pp(const action_formulas::imp& x) { return action_formulas::pp< action_formulas::imp >(x); }
      34           0 : std::string pp(const action_formulas::multi_action& x) { return action_formulas::pp< action_formulas::multi_action >(x); }
      35           0 : std::string pp(const action_formulas::not_& x) { return action_formulas::pp< action_formulas::not_ >(x); }
      36           0 : std::string pp(const action_formulas::or_& x) { return action_formulas::pp< action_formulas::or_ >(x); }
      37           0 : std::string pp(const action_formulas::true_& x) { return action_formulas::pp< action_formulas::true_ >(x); }
      38           0 : std::set<data::variable> find_all_variables(const action_formulas::action_formula& x) { return action_formulas::find_all_variables< action_formulas::action_formula >(x); }
      39             : //--- end generated action_formulas overloads ---//
      40             : 
      41             : namespace detail {
      42             : 
      43           0 : action_formula parse_action_formula(const std::string& text)
      44             : {
      45           0 :   core::parser p(parser_tables_mcrl2, core::detail::ambiguity_fn, core::detail::syntax_error_fn);
      46           0 :   unsigned int start_symbol_index = p.start_symbol_index("ActFrm");
      47           0 :   bool partial_parses = false;
      48           0 :   core::parse_node node = p.parse(text, start_symbol_index, partial_parses);
      49           0 :   core::warn_and_or(node);
      50           0 :   action_formula result = action_formula_actions(p).parse_ActFrm(node);
      51           0 :   return result;
      52             : }
      53             : 
      54             : } // namespace detail
      55             : 
      56             : } // namespace action_formulas
      57             : 
      58             : namespace regular_formulas
      59             : {
      60             : 
      61             : //--- start generated regular_formulas overloads ---//
      62           0 : std::string pp(const regular_formulas::alt& x) { return regular_formulas::pp< regular_formulas::alt >(x); }
      63           0 : std::string pp(const regular_formulas::regular_formula& x) { return regular_formulas::pp< regular_formulas::regular_formula >(x); }
      64           0 : std::string pp(const regular_formulas::seq& x) { return regular_formulas::pp< regular_formulas::seq >(x); }
      65           0 : std::string pp(const regular_formulas::trans& x) { return regular_formulas::pp< regular_formulas::trans >(x); }
      66           0 : std::string pp(const regular_formulas::trans_or_nil& x) { return regular_formulas::pp< regular_formulas::trans_or_nil >(x); }
      67           0 : std::string pp(const regular_formulas::untyped_regular_formula& x) { return regular_formulas::pp< regular_formulas::untyped_regular_formula >(x); }
      68             : //--- end generated regular_formulas overloads ---//
      69             : 
      70             : namespace detail
      71             : {
      72             : 
      73           0 : regular_formula parse_regular_formula(const std::string& text)
      74             : {
      75           0 :   core::parser p(parser_tables_mcrl2, core::detail::ambiguity_fn, core::detail::syntax_error_fn);
      76           0 :   unsigned int start_symbol_index = p.start_symbol_index("RegFrm");
      77           0 :   bool partial_parses = false;
      78           0 :   core::parse_node node = p.parse(text, start_symbol_index, partial_parses);
      79           0 :   regular_formula result = regular_formula_actions(p).parse_RegFrm(node);
      80           0 :   return result;
      81             : }
      82             : 
      83             : } // namespace detail
      84             : 
      85             : } // namespace regular_formulas
      86             : 
      87             : namespace state_formulas
      88             : {
      89             : 
      90             : //--- start generated state_formulas overloads ---//
      91           0 : std::string pp(const state_formulas::and_& x) { return state_formulas::pp< state_formulas::and_ >(x); }
      92           0 : std::string pp(const state_formulas::delay& x) { return state_formulas::pp< state_formulas::delay >(x); }
      93           0 : std::string pp(const state_formulas::delay_timed& x) { return state_formulas::pp< state_formulas::delay_timed >(x); }
      94           0 : std::string pp(const state_formulas::exists& x) { return state_formulas::pp< state_formulas::exists >(x); }
      95           0 : std::string pp(const state_formulas::false_& x) { return state_formulas::pp< state_formulas::false_ >(x); }
      96           0 : std::string pp(const state_formulas::forall& x) { return state_formulas::pp< state_formulas::forall >(x); }
      97           0 : std::string pp(const state_formulas::imp& x) { return state_formulas::pp< state_formulas::imp >(x); }
      98           0 : std::string pp(const state_formulas::may& x) { return state_formulas::pp< state_formulas::may >(x); }
      99           0 : std::string pp(const state_formulas::mu& x) { return state_formulas::pp< state_formulas::mu >(x); }
     100           0 : std::string pp(const state_formulas::must& x) { return state_formulas::pp< state_formulas::must >(x); }
     101           0 : std::string pp(const state_formulas::not_& x) { return state_formulas::pp< state_formulas::not_ >(x); }
     102           0 : std::string pp(const state_formulas::nu& x) { return state_formulas::pp< state_formulas::nu >(x); }
     103           0 : std::string pp(const state_formulas::or_& x) { return state_formulas::pp< state_formulas::or_ >(x); }
     104          95 : std::string pp(const state_formulas::state_formula& x) { return state_formulas::pp< state_formulas::state_formula >(x); }
     105           1 : std::string pp(const state_formulas::state_formula_specification& x) { return state_formulas::pp< state_formulas::state_formula_specification >(x); }
     106           0 : std::string pp(const state_formulas::true_& x) { return state_formulas::pp< state_formulas::true_ >(x); }
     107           0 : std::string pp(const state_formulas::variable& x) { return state_formulas::pp< state_formulas::variable >(x); }
     108           0 : std::string pp(const state_formulas::yaled& x) { return state_formulas::pp< state_formulas::yaled >(x); }
     109           0 : std::string pp(const state_formulas::yaled_timed& x) { return state_formulas::pp< state_formulas::yaled_timed >(x); }
     110         169 : state_formulas::state_formula normalize_sorts(const state_formulas::state_formula& x, const data::sort_specification& sortspec) { return state_formulas::normalize_sorts< state_formulas::state_formula >(x, sortspec); }
     111         168 : state_formulas::state_formula translate_user_notation(const state_formulas::state_formula& x) { return state_formulas::translate_user_notation< state_formulas::state_formula >(x); }
     112         168 : std::set<data::sort_expression> find_sort_expressions(const state_formulas::state_formula& x) { return state_formulas::find_sort_expressions< state_formulas::state_formula >(x); }
     113           1 : std::set<data::variable> find_all_variables(const state_formulas::state_formula& x) { return state_formulas::find_all_variables< state_formulas::state_formula >(x); }
     114           1 : std::set<data::variable> find_free_variables(const state_formulas::state_formula& x) { return state_formulas::find_free_variables< state_formulas::state_formula >(x); }
     115         641 : std::set<core::identifier_string> find_identifiers(const state_formulas::state_formula& x) { return state_formulas::find_identifiers< state_formulas::state_formula >(x); }
     116           0 : std::set<process::action_label> find_action_labels(const state_formulas::state_formula& x) { return state_formulas::find_action_labels< state_formulas::state_formula >(x); }
     117             : //--- end generated state_formulas overloads ---//
     118             : 
     119             : namespace detail {
     120             : 
     121         168 : state_formula parse_state_formula(const std::string& text)
     122             : {
     123         336 :   core::parser p(parser_tables_mcrl2, core::detail::ambiguity_fn, core::detail::syntax_error_fn);
     124         168 :   unsigned int start_symbol_index = p.start_symbol_index("StateFrm");
     125         168 :   bool partial_parses = false;
     126         336 :   core::parse_node node = p.parse(text, start_symbol_index, partial_parses);
     127         168 :   core::warn_and_or(node);
     128         168 :   state_formula result = state_formula_actions(p).parse_StateFrm(node);
     129         336 :   return result;
     130             : }
     131             : 
     132           1 : state_formula_specification parse_state_formula_specification(const std::string& text)
     133             : {
     134           2 :   core::parser p(parser_tables_mcrl2, core::detail::ambiguity_fn, core::detail::syntax_error_fn);
     135           1 :   unsigned int start_symbol_index = p.start_symbol_index("StateFrmSpec");
     136           1 :   bool partial_parses = false;
     137           2 :   core::parse_node node = p.parse(text, start_symbol_index, partial_parses);
     138           1 :   core::warn_and_or(node);
     139           1 :   core::warn_left_merge_merge(node);
     140             : 
     141           2 :   untyped_state_formula_specification untyped_statespec = state_formula_actions(p).parse_StateFrmSpec(node);
     142           1 :   state_formula_specification result = untyped_statespec.construct_state_formula_specification();
     143           2 :   return result;
     144             : }
     145             : 
     146             : } // namespace detail
     147             : 
     148             : namespace algorithms {
     149             : 
     150           0 : state_formula parse_state_formula(std::istream& in, lps::specification& lpsspec)
     151             : {
     152           0 :   return state_formulas::parse_state_formula(in, lpsspec);
     153             : }
     154             : 
     155           1 : state_formula parse_state_formula(const std::string& text, lps::specification& lpsspec)
     156             : {
     157           1 :   return state_formulas::parse_state_formula(text, lpsspec);
     158             : }
     159             : 
     160           0 : state_formula_specification parse_state_formula_specification(std::istream& in)
     161             : {
     162           0 :   return state_formulas::parse_state_formula_specification(in);
     163             : }
     164             : 
     165           0 : state_formula_specification parse_state_formula_specification(const std::string& text)
     166             : {
     167           0 :   return state_formulas::parse_state_formula_specification(text);
     168             : }
     169             : 
     170           0 : state_formula_specification parse_state_formula_specification(std::istream& in, lps::specification& lpsspec)
     171             : {
     172           0 :   return state_formulas::parse_state_formula_specification(in, lpsspec);
     173             : }
     174             : 
     175           0 : state_formula_specification parse_state_formula_specification(const std::string& text, lps::specification& lpsspec)
     176             : {
     177           0 :   return state_formulas::parse_state_formula_specification(text, lpsspec);
     178             : }
     179             : 
     180           0 : bool is_monotonous(const state_formula& f)
     181             : {
     182           0 :   return state_formulas::is_monotonous(f);
     183             : }
     184             : 
     185           0 : state_formula normalize(const state_formula& x)
     186             : {
     187           0 :   return state_formulas::normalize(x);
     188             : }
     189             : 
     190           0 : bool is_normalized(const state_formula& x)
     191             : {
     192           0 :   return state_formulas::is_normalized(x);
     193             : }
     194             : 
     195         138 : bool is_timed(const state_formula& x)
     196             : {
     197         138 :   return state_formulas::is_timed(x);
     198             : }
     199             : 
     200           0 : std::set<core::identifier_string> find_state_variable_names(const state_formula& x)
     201             : {
     202           0 :   return state_formulas::find_state_variable_names(x);
     203             : }
     204             : 
     205             : } // namespace algorithms
     206             : 
     207             : } // namespace state_formulas
     208             : 
     209         138 : } // namespace mcrl2

Generated by: LCOV version 1.13