.. index:: pbesabstract
.. _tool-pbesabstract:
pbesabstract
============
Under- or overapproximate the solution of a PBES, by abstracting from variables.
Example
-------
Consider the following PBES:
.. code-block:: mcrl2
nu X(n:Nat) = val(n > 1000000) || X(n+1)
Computing ``X(0)`` depends on the computation of equations for all ``X(i)``,
for ``i <= 1000000``. After pbesabstract, for variable ``n``, the equation is
reduced to:
.. code-block:: mcrl2
nu X(n:Nat) = false || X(n+1)
Now, an application of pbesparelm can detect the redundancy of variable
``n``, allowing one to rewrite the above equation to the equivalent PBES:
.. code-block:: mcrl2
nu X = false || X
The latter is readily seen to have solution ``true``. As a result, also the
original equation systems have result ``true``.