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           0 : }
      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           0 : }
      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::const_multiply& x) { return state_formulas::pp< state_formulas::const_multiply >(x); }
      93           0 : std::string pp(const state_formulas::const_multiply_alt& x) { return state_formulas::pp< state_formulas::const_multiply_alt >(x); }
      94           0 : std::string pp(const state_formulas::delay& x) { return state_formulas::pp< state_formulas::delay >(x); }
      95           0 : std::string pp(const state_formulas::delay_timed& x) { return state_formulas::pp< state_formulas::delay_timed >(x); }
      96           0 : std::string pp(const state_formulas::exists& x) { return state_formulas::pp< state_formulas::exists >(x); }
      97           0 : std::string pp(const state_formulas::false_& x) { return state_formulas::pp< state_formulas::false_ >(x); }
      98           0 : std::string pp(const state_formulas::forall& x) { return state_formulas::pp< state_formulas::forall >(x); }
      99           0 : std::string pp(const state_formulas::imp& x) { return state_formulas::pp< state_formulas::imp >(x); }
     100           0 : std::string pp(const state_formulas::infimum& x) { return state_formulas::pp< state_formulas::infimum >(x); }
     101           0 : std::string pp(const state_formulas::may& x) { return state_formulas::pp< state_formulas::may >(x); }
     102           0 : std::string pp(const state_formulas::minus& x) { return state_formulas::pp< state_formulas::minus >(x); }
     103           0 : std::string pp(const state_formulas::mu& x) { return state_formulas::pp< state_formulas::mu >(x); }
     104           0 : std::string pp(const state_formulas::must& x) { return state_formulas::pp< state_formulas::must >(x); }
     105           0 : std::string pp(const state_formulas::not_& x) { return state_formulas::pp< state_formulas::not_ >(x); }
     106           0 : std::string pp(const state_formulas::nu& x) { return state_formulas::pp< state_formulas::nu >(x); }
     107           0 : std::string pp(const state_formulas::or_& x) { return state_formulas::pp< state_formulas::or_ >(x); }
     108           0 : std::string pp(const state_formulas::plus& x) { return state_formulas::pp< state_formulas::plus >(x); }
     109         143 : std::string pp(const state_formulas::state_formula& x) { return state_formulas::pp< state_formulas::state_formula >(x); }
     110           5 : std::string pp(const state_formulas::state_formula_specification& x) { return state_formulas::pp< state_formulas::state_formula_specification >(x); }
     111           0 : std::string pp(const state_formulas::sum& x) { return state_formulas::pp< state_formulas::sum >(x); }
     112           0 : std::string pp(const state_formulas::supremum& x) { return state_formulas::pp< state_formulas::supremum >(x); }
     113           0 : std::string pp(const state_formulas::true_& x) { return state_formulas::pp< state_formulas::true_ >(x); }
     114           0 : std::string pp(const state_formulas::variable& x) { return state_formulas::pp< state_formulas::variable >(x); }
     115           0 : std::string pp(const state_formulas::yaled& x) { return state_formulas::pp< state_formulas::yaled >(x); }
     116           0 : std::string pp(const state_formulas::yaled_timed& x) { return state_formulas::pp< state_formulas::yaled_timed >(x); }
     117         179 : 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); }
     118         178 : state_formulas::state_formula translate_user_notation(const state_formulas::state_formula& x) { return state_formulas::translate_user_notation< state_formulas::state_formula >(x); }
     119         174 : 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); }
     120           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); }
     121           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); }
     122         673 : std::set<core::identifier_string> find_identifiers(const state_formulas::state_formula& x) { return state_formulas::find_identifiers< state_formulas::state_formula >(x); }
     123           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); }
     124             : //--- end generated state_formulas overloads ---//
     125             : 
     126             : namespace detail {
     127             : 
     128         174 : state_formula parse_state_formula(const std::string& text)
     129             : {
     130         174 :   core::parser p(parser_tables_mcrl2, core::detail::ambiguity_fn, core::detail::syntax_error_fn);
     131         174 :   unsigned int start_symbol_index = p.start_symbol_index("StateFrm");
     132         174 :   bool partial_parses = false;
     133         174 :   core::parse_node node = p.parse(text, start_symbol_index, partial_parses);
     134         174 :   core::warn_and_or(node);
     135         174 :   state_formula result = state_formula_actions(p).parse_StateFrm(node);
     136         348 :   return result;
     137         174 : }
     138             : 
     139           5 : state_formula_specification parse_state_formula_specification(const std::string& text)
     140             : {
     141           5 :   core::parser p(parser_tables_mcrl2, core::detail::ambiguity_fn, core::detail::syntax_error_fn);
     142           5 :   unsigned int start_symbol_index = p.start_symbol_index("StateFrmSpec");
     143           5 :   bool partial_parses = false;
     144           5 :   core::parse_node node = p.parse(text, start_symbol_index, partial_parses);
     145           5 :   core::warn_and_or(node);
     146           5 :   core::warn_left_merge_merge(node);
     147             : 
     148           5 :   untyped_state_formula_specification untyped_statespec = state_formula_actions(p).parse_StateFrmSpec(node);
     149           5 :   state_formula_specification result = untyped_statespec.construct_state_formula_specification();
     150          10 :   return result;
     151           5 : }
     152             : 
     153             : } // namespace detail
     154             : 
     155             : namespace algorithms {
     156             : 
     157           2 : state_formula parse_state_formula(std::istream& in, lps::stochastic_specification& lpsspec, const bool formula_is_quantitative)
     158             : {
     159           2 :   return state_formulas::parse_state_formula(in, lpsspec, formula_is_quantitative);
     160             : }
     161             : 
     162           1 : state_formula parse_state_formula(const std::string& text, lps::stochastic_specification& lpsspec, const bool formula_is_quantitative)
     163             : {
     164           1 :   return state_formulas::parse_state_formula(text, lpsspec, formula_is_quantitative);
     165             : }
     166             : 
     167           0 : state_formula_specification parse_state_formula_specification(std::istream& in, const bool formula_is_quantitative)
     168             : {
     169           0 :   return state_formulas::parse_state_formula_specification(in, formula_is_quantitative);
     170             : }
     171             : 
     172           0 : state_formula_specification parse_state_formula_specification(const std::string& text, const bool formula_is_quantitative)
     173             : {
     174           0 :   return state_formulas::parse_state_formula_specification(text, formula_is_quantitative);
     175             : }
     176             : 
     177           0 : state_formula_specification parse_state_formula_specification(std::istream& in, lps::stochastic_specification& lpsspec, const bool formula_is_quantitative)
     178             : {
     179           0 :   return state_formulas::parse_state_formula_specification(in, lpsspec, formula_is_quantitative);
     180             : }
     181             : 
     182           0 : state_formula_specification parse_state_formula_specification(const std::string& text, lps::stochastic_specification& lpsspec, const bool formula_is_quantitative)
     183             : {
     184           0 :   return state_formulas::parse_state_formula_specification(text, lpsspec, formula_is_quantitative);
     185             : }
     186             : 
     187           0 : bool is_monotonous(const state_formula& f)
     188             : {
     189           0 :   return state_formulas::is_monotonous(f);
     190             : }
     191             : 
     192           0 : state_formula normalize(const state_formula& x, bool quantitative=false, bool negated=false)
     193             : {
     194           0 :   return state_formulas::normalize(x, quantitative, negated);
     195             : }
     196             : 
     197           0 : bool is_normalized(const state_formula& x)
     198             : {
     199           0 :   return state_formulas::is_normalized(x);
     200             : }
     201             : 
     202         143 : bool is_timed(const state_formula& x)
     203             : {
     204         143 :   return state_formulas::is_timed(x);
     205             : }
     206             : 
     207           0 : std::set<core::identifier_string> find_state_variable_names(const state_formula& x)
     208             : {
     209           0 :   return state_formulas::find_state_variable_names(x);
     210             : }
     211             : 
     212             : } // namespace algorithms
     213             : 
     214             : } // namespace state_formulas
     215             : 
     216             : } // namespace mcrl2