LCOV - code coverage report
Current view: top level - pbes/include/mcrl2/pbes - remove_equations.h (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 33 40 82.5 %
Date: 2024-03-08 02:52:28 Functions: 2 3 66.7 %
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 mcrl2/pbes/remove_equations.h
      10             : /// \brief add your file description here.
      11             : 
      12             : #ifndef MCRL2_PBES_REMOVE_EQUATIONS_H
      13             : #define MCRL2_PBES_REMOVE_EQUATIONS_H
      14             : 
      15             : #include "mcrl2/pbes/pbes.h"
      16             : 
      17             : namespace mcrl2 {
      18             : 
      19             : namespace pbes_system {
      20             : 
      21             : namespace detail {
      22             : 
      23             : inline
      24           0 : std::string print_removed_equations(const std::vector<propositional_variable>& removed)
      25             : {
      26           0 :   std::ostringstream out;
      27           0 :   out << "\nremoved the following equations:" << std::endl;
      28           0 :   for (const propositional_variable& v: removed)
      29             :   {
      30           0 :     out << "  " << pbes_system::pp(v) << std::endl;
      31             :   }
      32           0 :   return out.str();
      33           0 : }
      34             : 
      35             : } // namespace detail
      36             : 
      37             : inline
      38          20 : std::set<propositional_variable> reachable_variables(const pbes& p)
      39             : {
      40             :   typedef std::vector<pbes_equation>::const_iterator iterator;
      41             : 
      42             :   // create a mapping from variable names to iterators
      43          20 :   std::map<core::identifier_string, iterator> index;
      44          59 :   for (auto i = p.equations().begin(); i != p.equations().end(); ++i)
      45             :   {
      46             :     // index[i->variable().name()] = i;  <-- This leads to a attempt to copy-
      47             :     //                                       construct an iterator from a singular iterator when the toolset
      48             :     //                                       is compiled in maintainer mode.
      49          39 :     index.insert(std::pair<core::identifier_string, iterator>(i->variable().name(),i));
      50             :   }
      51             : 
      52          20 :   std::set<core::identifier_string> visited;
      53          20 :   std::set<core::identifier_string> explored;
      54          20 :   visited.insert(p.initial_state().name());
      55          55 :   while (!visited.empty())
      56             :   {
      57          35 :     core::identifier_string X = *visited.begin();
      58          35 :     visited.erase(visited.begin());
      59          35 :     explored.insert(X);
      60          35 :     pbes_expression phi = index[X]->formula();
      61          35 :     std::set<propositional_variable_instantiation> iocc = pbes_system::find_propositional_variable_instantiations(phi);
      62          80 :     for (const propositional_variable_instantiation& i: iocc)
      63             :     {
      64          45 :       if (explored.find(i.name()) == explored.end())
      65             :       {
      66          17 :         visited.insert(i.name());
      67             :       }
      68             :     }
      69          35 :   }
      70             : 
      71          20 :   std::set<propositional_variable> result;
      72          55 :   for (const core::identifier_string& i: explored)
      73             :   {
      74          35 :     result.insert(index[i]->variable());
      75             :   }
      76          40 :   return result;
      77          20 : }
      78             : 
      79             : /// \brief Removes equations that are not (syntactically) reachable from the initial state of a PBES.
      80             : /// \return The removed variables
      81             : inline
      82          20 : std::vector<propositional_variable> remove_unreachable_variables(pbes& p)
      83             : {
      84          20 :   std::vector<propositional_variable> result;
      85             : 
      86          20 :   std::set<propositional_variable> V = reachable_variables(p);
      87          20 :   std::vector<pbes_equation> equations;
      88          59 :   for (pbes_equation& eqn: p.equations())
      89             :   {
      90          39 :     if (V.find(eqn.variable()) != V.end())
      91             :     {
      92          35 :       equations.push_back(eqn);
      93             :     }
      94             :     else
      95             :     {
      96           4 :       result.push_back(eqn.variable());
      97             :     }
      98             :   }
      99          20 :   p.equations() = equations;
     100          40 :   return result;
     101          20 : }
     102             : 
     103             : } // namespace pbes_system
     104             : 
     105             : } // namespace mcrl2
     106             : 
     107             : #endif // MCRL2_PBES_REMOVE_EQUATIONS_H

Generated by: LCOV version 1.14