Common functionality ==================== The mCRL2 Library contains some algorithms that are applicable to several libraries. The most prominent example is a traversal framework and a family of find functions that has been implemented on top of that. This chapter discusses some of these algorithms. Traversal functions ------------------- The mCRL2 Library contains a range of generic traversal functions. There are different types of travelsals possible: .. table Traversal types ======================= ==================================================================== Type Meaning ======================= ==================================================================== normal traversal Traverse an object completely binding aware traversal Traverse an object completely, while maintaining the bound variables sort traversal Traverses only the parts of an object that contain sorts ======================= ==================================================================== Each library defines classes that support these traversal types, namely `traverser`, `binding_aware_traverser` and `builder`. They are the most commonly occurring traversals. When writing an algorithm that needs to traverse an object, one can usually implement it using one of the predefined traversal classes. When deriving from a traverser class, the `enter` and `leave` functions must be made visible using .. code-block:: c++ using super::enter; using super::leave; .. note:: For Visual C++ the following workaround must be applied as well, otherwise it will complain about ambiguities of `operator()`. .. code-block:: c++ #if BOOST_MSVC // Workaround for malfunctioning MSVC 2008 overload resolution template < typename Container > void operator()(Container const& a) { super::operator()(a); } #endif .. note:: It is possible to change the way an object is traversed by overriding member functions. How that works exactly needs be figured out. Implementation details ^^^^^^^^^^^^^^^^^^^^^^ The traverser classes have the following structure: .. code-block:: c++ template < typename Derived > class traverser { public: void operator()(function_symbol const& e); void operator()(data_expression const& e); ... }; template < typename Derived > class binding_aware_traverser : public traverser< Derived >; template < typename Derived > class sort_traverser : public traverser< Derived >; The default implementation for `operator()` calls the function `enter` upon entering and `leave` upon leaving an object. By default these functions have an empty body, so they can be optimized away by the compiler. The user can override these functions in a base class to add behavior. If an object has any sub objects, they can be visited by applying the `operator()` function to them. In the example below this is done with the `name()` attribute of a `variable`. .. code-block:: c++ void operator()(variable const& e) { ... static_cast< Derived& >(*this).enter(e); static_cast< Derived& >(*this)(e.name()); static_cast< Derived& >(*this).leave(e); ... } Note that the `Curiously recurring template pattern `_ needs to be applied in the implementation of `traverser`, since it needs access to protected interfaces of derived classes. The traversal framework can be reused in other libraries. The LPS Library defines classes `lps_data_traverser` and `lps_binding_aware_traverser` like this: .. code-block:: c++ template < typename Derived, template < class > class Traverser = mcrl2::data::detail::traverser > class lps_data_traverser : public Traverser< Derived > { public: void operator()(const multi_action& a); void operator()(const linear_process& p); ... }; template < typename Derived > struct lps_binding_aware_traverser : public lps::detail::lps_data_traverser< Derived, data::detail::binding_aware_traverser > .. warning:: The traversal classes have only been partly defined for the LPS Library and not yet for the Process and PBES Library. Examples ^^^^^^^^ The following are three examples of applications of traversers and builders. The first example shows a traverser that computes the sum of all integers. Applied to a vector of integers, this will compute the sum of all integers in the vector. .. literalinclude:: examples/traverser1.cpp The example is extended with different traversers, and again applied to a vector of integers in the following example. .. literalinclude:: examples/traverser2.cpp Traversers are read only, i.e. they do not modify a term. The following example shows a builder, that increments each integer. .. literalinclude:: examples/builder1.cpp Applications ^^^^^^^^^^^^ The Traversal Framework is a collection of classes that support traversal over hierarchical mCRL2 data structures. Many algorithms are built on top of this library. The most important examples are the find and replace functions. The goal of the traversal framework is to provide algorithms with a uniform interface, and to prevent repetitive code for traversing mCRL2 data structures. Find functions """""""""""""" The mCRL2 Library contains a wide range of algorithms built on top of the traversers and builders. An overview of the most commonly used traverser based functions is given below. The mCRL2 Library contains a range of generic find functions. These are: .. table:: Generic find functions ======================= =============================================== Function Meaning ======================= =============================================== `find_basic_sorts` Finds basic sorts that occur in an object `find_data_expressions` Finds data expressions that occur in an object `find_free_variables` Finds free variables that occur in an object `find_identifiers` Finds identifiers that occur in an object `find_sort_expressions` Finds sort expressions that occur in an object `find_variables` Finds variables that occur in an object ======================= =============================================== These functions can be applied to a wide range of objects in the mCRL2 Library, ranging from `data_expression` to `action_summand`. .. table:: Find functions for data specifications ================== =================================================================== Function Meaning ================== =================================================================== `find_constructor` Finds a constructor `find_equations` Finds equations with a given expression as head on one of its sides `find_mapping` Finds a mapping `find_sort` Finds a sort ================== =================================================================== .. table:: Generic replace functions ================================= ================================================================================================================================== Function Meaning ================================= ================================================================================================================================== `replace_sort_expressions` Applies a substitution to sort expressions that occur in an object. Optionally it can be applied to nested expressions. `replace_variables` Applies a substitution to variables that occur in an object within the context of a data expression. `replace_free_variables` Applies a substitution to free variables that occur in an object within the context of a data expression. `replace_data_expressions` Applies a substitution to data expressions that occur in an object. Optionally it can be applied to nested expressions. `replace_propositional_variables` Applies a substitution to propositional variable instantiations that occur in an object within the context of a pbes expression. ================================= ================================================================================================================================== .. table:: Other generic traverser based functions ========================= ========================================================================================== Function Meaning ========================= ========================================================================================== `translate_user_notation` Applies a transformation to numbers, sets and bags that is needed after parsing. `normalize_sorts` Brings embedded sorts into normal form. `rewrite` Applies a rewriter to embedded expressions, optionally in combination with a substitution. ========================= ========================================================================================== These functions can be applied to a wide range of objects in the mCRL2 Library, ranging from `data::data_expression` to `lps::action_summand`. Each library has it's own overloads of these functions. For example to find data variables in an object of the LPS library, the function `lps::find_variables` must be used. .. warning:: It is important to choose the right overload of generic traverser functions. Failing to do so may result in compilation errors, or runtime exceptions. Implementation details """""""""""""""""""""" The implementation of find functions is not finished yet. It has to be figured out how to extend the functionality of the Data Library to other libraries. The file `mcrl2/lps/find.h` currently contains this: .. code-block:: c++ /// \brief Returns all data variables that occur in a range of expressions /// \param[in] container a container with expressions /// \return All data variables that occur in the term t template void find_free_variables(Container const& container, OutputIterator o) { data::detail::make_free_variable_find_helper< lps::detail::lps_binding_aware_traverser >(o)(container); } /// \brief Returns all data variables that occur in a range of expressions /// \param[in] container a container with expressions /// \return All data variables that occur in the term t /// TODO replace uses by data::find_free_variables template std::set< data::variable > find_free_variables(Container const& container) { ... } Generic programming techniques ------------------------------ The file =mcrl2/data/detail/container_utility.h= contains two utility functions `enable_if_container` and `disable_if_container` for determining if a type is a container type. It can be used to create an interface that does different things for containers and for other types: .. code-block:: c++ template void operator()(const Container& t, typename data::detail::enable_if_container::type* = 0) { traverse_container(t); } template void operator()(const Term& t, typename data::detail::disable_if_container::type* = 0) { traverse(t); } Static polymorphism ------------------- For the traversal functions in mCRL2 a technique called `static polymorphism `_ is used. Below an example is given how static polymorphism can in principle be used to implement find functions in the mCRL2 Library. In this case, A models data::detail::traverser, B models lps::detail::traverser and C models data::detail::find_helper. .. code-block:: c++ #include // base class template struct A { void a() { std::cout << "A::a()" << std::endl; } }; // extended class template struct B: public A { void b() { std::cout << "B::b()" << std::endl; static_cast(*this).a(); } }; // override the a() function template