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/is_bes.h"
      17             : #include "mcrl2/pbes/parse_impl.h"
      18             : #include "mcrl2/pbes/print.h"
      19             : #include "mcrl2/pbes/translate_user_notation.h"
      20             : 
      21             : namespace mcrl2
      22             : {
      23             : 
      24             : namespace pbes_system
      25             : {
      26             : 
      27             : //--- start generated pbes_system overloads ---//
      28           0 : std::string pp(const pbes_system::pbes_equation_vector& x) { return pbes_system::pp< pbes_system::pbes_equation_vector >(x); }
      29           0 : std::string pp(const pbes_system::pbes_expression_list& x) { return pbes_system::pp< pbes_system::pbes_expression_list >(x); }
      30           0 : std::string pp(const pbes_system::pbes_expression_vector& x) { return pbes_system::pp< pbes_system::pbes_expression_vector >(x); }
      31           0 : std::string pp(const pbes_system::propositional_variable_list& x) { return pbes_system::pp< pbes_system::propositional_variable_list >(x); }
      32           0 : std::string pp(const pbes_system::propositional_variable_vector& x) { return pbes_system::pp< pbes_system::propositional_variable_vector >(x); }
      33           0 : std::string pp(const pbes_system::propositional_variable_instantiation_list& x) { return pbes_system::pp< pbes_system::propositional_variable_instantiation_list >(x); }
      34           0 : std::string pp(const pbes_system::propositional_variable_instantiation_vector& x) { return pbes_system::pp< pbes_system::propositional_variable_instantiation_vector >(x); }
      35           0 : std::string pp(const pbes_system::and_& x) { return pbes_system::pp< pbes_system::and_ >(x); }
      36           0 : std::string pp(const pbes_system::exists& x) { return pbes_system::pp< pbes_system::exists >(x); }
      37          88 : std::string pp(const pbes_system::fixpoint_symbol& x) { return pbes_system::pp< pbes_system::fixpoint_symbol >(x); }
      38           0 : std::string pp(const pbes_system::forall& x) { return pbes_system::pp< pbes_system::forall >(x); }
      39           0 : std::string pp(const pbes_system::imp& x) { return pbes_system::pp< pbes_system::imp >(x); }
      40           0 : std::string pp(const pbes_system::not_& x) { return pbes_system::pp< pbes_system::not_ >(x); }
      41           0 : std::string pp(const pbes_system::or_& x) { return pbes_system::pp< pbes_system::or_ >(x); }
      42         205 : std::string pp(const pbes_system::pbes& x) { return pbes_system::pp< pbes_system::pbes >(x); }
      43           0 : std::string pp(const pbes_system::pbes_equation& x) { return pbes_system::pp< pbes_system::pbes_equation >(x); }
      44        6546 : std::string pp(const pbes_system::pbes_expression& x) { return pbes_system::pp< pbes_system::pbes_expression >(x); }
      45          77 : std::string pp(const pbes_system::propositional_variable& x) { return pbes_system::pp< pbes_system::propositional_variable >(x); }
      46          74 : std::string pp(const pbes_system::propositional_variable_instantiation& x) { return pbes_system::pp< pbes_system::propositional_variable_instantiation >(x); }
      47           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); }
      48         467 : void normalize_sorts(pbes_system::pbes& x, const data::sort_specification& /* sortspec */) { pbes_system::normalize_sorts< pbes_system::pbes >(x, x.data()); }
      49           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); }
      50         465 : void translate_user_notation(pbes_system::pbes& x) { pbes_system::translate_user_notation< pbes_system::pbes >(x); }
      51           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); }
      52         606 : std::set<data::sort_expression> find_sort_expressions(const pbes_system::pbes& x) { return pbes_system::find_sort_expressions< pbes_system::pbes >(x); }
      53           1 : std::set<data::variable> find_all_variables(const pbes_system::pbes& x) { return pbes_system::find_all_variables< pbes_system::pbes >(x); }
      54         350 : std::set<data::variable> find_free_variables(const pbes_system::pbes& x) { return pbes_system::find_free_variables< pbes_system::pbes >(x); }
      55        3832 : std::set<data::variable> find_free_variables(const pbes_system::pbes_expression& x) { return pbes_system::find_free_variables< pbes_system::pbes_expression >(x); }
      56           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); }
      57          22 : std::set<data::function_symbol> find_function_symbols(const pbes_system::pbes& x) { return pbes_system::find_function_symbols< pbes_system::pbes >(x); }
      58        3808 : 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); }
      59         925 : std::set<core::identifier_string> find_identifiers(const pbes_system::pbes_expression& x) { return pbes_system::find_identifiers< pbes_system::pbes_expression >(x); }
      60           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); }
      61             : //--- end generated pbes_system overloads ---//
      62             : 
      63             : namespace algorithms {
      64             : 
      65          36 : void instantiate_global_variables(pbes& p)
      66             : {
      67          36 :   pbes_system::detail::instantiate_global_variables(p);
      68          36 : }
      69             : 
      70           0 : bool is_bes(const pbes& x)
      71             : {
      72           0 :   return pbes_system::is_bes(x);
      73             : }
      74             : 
      75             : } // namespace algorithms
      76             : 
      77           0 : bool is_well_typed(const pbes_equation& eqn)
      78             : {
      79           0 :   return pbes_system::detail::is_well_typed(eqn);
      80             : }
      81             : 
      82        1144 : bool is_well_typed_equation(const pbes_equation& eqn,
      83             :                             const std::set<data::sort_expression>& declared_sorts,
      84             :                             const std::set<data::variable>& declared_global_variables,
      85             :                             const data::data_specification& data_spec
      86             :                            )
      87             : {
      88        1144 :   return pbes_system::detail::is_well_typed_equation(eqn, declared_sorts, declared_global_variables, data_spec);
      89             : }
      90             : 
      91         284 : bool is_well_typed_pbes(const std::set<data::sort_expression>& declared_sorts,
      92             :                         const std::set<data::variable>& declared_global_variables,
      93             :                         const std::set<data::variable>& occurring_global_variables,
      94             :                         const std::set<propositional_variable>& declared_variables,
      95             :                         const std::set<propositional_variable_instantiation>& occ,
      96             :                         const propositional_variable_instantiation& init,
      97             :                         const data::data_specification& data_spec
      98             :                        )
      99             : {
     100         284 :   return pbes_system::detail::is_well_typed_pbes(declared_sorts, declared_global_variables, occurring_global_variables, declared_variables, occ, init, data_spec);
     101             : }
     102             : 
     103           0 : bool pbes_equation::is_solved() const
     104             : {
     105           0 :   return !detail::has_propositional_variables(formula());
     106             : }
     107             : 
     108         489 : std::set<propositional_variable_instantiation> pbes::occurring_variable_instantiations() const
     109             : {
     110         489 :   std::set<propositional_variable_instantiation> result;
     111        2228 :   for (const pbes_equation& eqn: equations())
     112             :   {
     113        1739 :     detail::occurring_variable_visitor f;
     114        1739 :     f.apply(eqn.formula());
     115        1739 :     result.insert(f.variables.begin(), f.variables.end());
     116        1739 :   }
     117         489 :   return result;
     118           0 : }
     119             : 
     120             : namespace detail {
     121             : 
     122           0 : pbes_expression parse_pbes_expression_new(const std::string& text)
     123             : {
     124           0 :   core::parser p(parser_tables_mcrl2, core::detail::ambiguity_fn, core::detail::syntax_error_fn);
     125           0 :   unsigned int start_symbol_index = p.start_symbol_index("PbesExpr");
     126           0 :   bool partial_parses = false;
     127           0 :   core::parse_node node = p.parse(text, start_symbol_index, partial_parses);
     128           0 :   core::warn_and_or(node);
     129           0 :   pbes_expression result = pbes_actions(p).parse_PbesExpr(node);
     130           0 :   return result;
     131           0 : }
     132             : 
     133         467 : untyped_pbes parse_pbes_new(const std::string& text)
     134             : {
     135         467 :   core::parser p(parser_tables_mcrl2, core::detail::ambiguity_fn, core::detail::syntax_error_fn);
     136         467 :   unsigned int start_symbol_index = p.start_symbol_index("PbesSpec");
     137         467 :   bool partial_parses = false;
     138         467 :   core::parse_node node = p.parse(text, start_symbol_index, partial_parses);
     139         467 :   core::warn_and_or(node);
     140         467 :   untyped_pbes result = pbes_actions(p).parse_PbesSpec(node);
     141         934 :   return result;
     142         467 : }
     143             : 
     144         465 : void complete_pbes(pbes& x)
     145             : {
     146         465 :   typecheck_pbes(x);
     147         465 :   pbes_system::translate_user_notation(x);
     148         465 :   complete_data_specification(x);
     149         465 : }
     150             : 
     151           2 : propositional_variable parse_propositional_variable(const std::string& text)
     152             : {
     153           2 :   core::parser p(parser_tables_mcrl2, core::detail::ambiguity_fn, core::detail::syntax_error_fn);
     154           2 :   unsigned int start_symbol_index = p.start_symbol_index("PropVarDecl");
     155           2 :   bool partial_parses = false;
     156           2 :   core::parse_node node = p.parse(text, start_symbol_index, partial_parses);
     157           4 :   return detail::pbes_actions(p).parse_PropVarDecl(node);
     158           2 : }
     159             : 
     160           1 : pbes_expression parse_pbes_expression(const std::string& text)
     161             : {
     162           1 :   core::parser p(parser_tables_mcrl2, core::detail::ambiguity_fn, core::detail::syntax_error_fn);
     163           1 :   unsigned int start_symbol_index = p.start_symbol_index("PbesExpr");
     164           1 :   bool partial_parses = false;
     165           1 :   core::parse_node node = p.parse(text, start_symbol_index, partial_parses);
     166           1 :   core::warn_and_or(node);
     167           2 :   return detail::pbes_actions(p).parse_PbesExpr(node);
     168           1 : }
     169             : 
     170             : } // namespace detail
     171             : 
     172             : } // namespace pbes_system
     173             : 
     174             : } // namespace mcrl2
     175             :