LCOV - code coverage report
Current view: top level - pbes/include/mcrl2/pbes - pbesinst_lazy.h (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 110 164 67.1 %
Date: 2024-03-08 02:52:28 Functions: 16 24 66.7 %
Legend: Lines: hit not hit

          Line data    Source code
       1             : // Author(s): Wieger Wesselink 2017-2019
       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/pbesinst_lazy_algorithm.h
      10             : /// \brief A lazy algorithm for instantiating a PBES, ported from bes_deprecated.h.
      11             : 
      12             : #include <thread>
      13             : #include <mutex>
      14             : 
      15             : #include "mcrl2/atermpp/standard_containers/deque.h"
      16             : #include "mcrl2/atermpp/standard_containers/indexed_set.h"
      17             : #include "mcrl2/data/substitution_utility.h"
      18             : #include "mcrl2/pbes/detail/bes_equation_limit.h"
      19             : #include "mcrl2/pbes/detail/instantiate_global_variables.h"
      20             : #include "mcrl2/pbes/pbes_equation_index.h"
      21             : #include "mcrl2/pbes/pbessolve_options.h"
      22             : #include "mcrl2/pbes/remove_equations.h"
      23             : #include "mcrl2/pbes/replace_constants_by_variables.h"
      24             : #include "mcrl2/pbes/rewriters/enumerate_quantifiers_rewriter.h"
      25             : #include "mcrl2/pbes/rewriters/one_point_rule_rewriter.h"
      26             : #include "mcrl2/pbes/rewriters/simplify_quantifiers_rewriter.h"
      27             : #include "mcrl2/pbes/transformation_strategy.h"
      28             : #include "mcrl2/pbes/transformations.h"
      29             : 
      30             : #ifndef MCRL2_PBES_PBESINST_LAZY_H
      31             : #define MCRL2_PBES_PBESINST_LAZY_H
      32             : 
      33             : namespace mcrl2
      34             : {
      35             : 
      36             : namespace pbes_system
      37             : {
      38             : 
      39             : // This todo set maintains elements that were removed by the reset procedure.
      40             : class pbesinst_lazy_todo
      41             : {
      42             :   protected:
      43             :     std::unordered_set<propositional_variable_instantiation> irrelevant;
      44             :     atermpp::deque<propositional_variable_instantiation> todo;
      45             : 
      46             :     // checks some invariants on the internal state
      47             :     bool check_invariants() const
      48             :     {
      49             :       using utilities::detail::contains;
      50             :       for (const auto& X: irrelevant)
      51             :       {
      52             :         if (contains(todo, X))
      53             :         {
      54             :           return false;
      55             :         }
      56             :       }
      57             :       std::unordered_set<propositional_variable_instantiation> tmp(todo.begin(), todo.end());
      58             :       return tmp.size() == todo.size();
      59             :     }
      60             : 
      61             :   public:
      62        3549 :     const propositional_variable_instantiation& front() const
      63             :     {
      64        3549 :       return todo.front();
      65             :     }
      66             : 
      67           0 :     const propositional_variable_instantiation& back() const
      68             :     {
      69           0 :       return todo.back();
      70             :     }
      71             : 
      72             :     bool empty() const
      73             :     {
      74             :       return todo.empty() && irrelevant.empty();
      75             :     }
      76             : 
      77             :     std::size_t size() const
      78             :     {
      79             :       return todo.size();
      80             :     }
      81             : 
      82        3682 :     const atermpp::deque<propositional_variable_instantiation>& elements() const
      83             :     {
      84        3682 :       return todo;
      85             :     }
      86             : 
      87             :     const std::unordered_set<propositional_variable_instantiation>& irrelevant_elements() const
      88             :     {
      89             :       return irrelevant;
      90             :     }
      91             : 
      92             :     std::unordered_set<propositional_variable_instantiation>& irrelevant_elements()
      93             :     {
      94             :       return irrelevant;
      95             :     }
      96             : 
      97        3549 :     void pop_front()
      98             :     {
      99        3549 :       todo.pop_front();
     100        3549 :     }
     101             : 
     102           0 :     void pop_back()
     103             :     {
     104           0 :       todo.pop_back();
     105           0 :     }
     106             : 
     107         133 :     void insert(const propositional_variable_instantiation& x)
     108             :     {
     109         133 :       irrelevant.erase(x);
     110         133 :       todo.push_back(x);
     111         133 :     }
     112             : 
     113             :     template <typename FwdIter, bool ThreadSafe>
     114        3549 :     void insert(FwdIter first, 
     115             :                 FwdIter last, 
     116             :                 const atermpp::indexed_set<propositional_variable_instantiation, ThreadSafe>& discovered,
     117             :                 const std::size_t thread_index)
     118             :     {
     119             :       using utilities::detail::contains;
     120             : 
     121        9140 :       for (FwdIter i = first; i != last; ++i)
     122             :       {
     123        5591 :         auto j = irrelevant.find(*i);
     124        5591 :         if (j != irrelevant.end())
     125             :         {
     126           0 :           todo.push_back(*j);
     127           0 :           irrelevant.erase(j);
     128             :         }
     129        5591 :         else if (!contains(discovered, *i, thread_index))
     130             :         {
     131        3416 :           todo.push_back(*i);
     132             :         }
     133             :       }
     134        3549 :     }
     135             : 
     136             :     void set_todo(atermpp::deque<propositional_variable_instantiation>& new_todo)
     137             :     {
     138             :       using utilities::detail::contains;
     139             :       std::size_t size_before = todo.size() + irrelevant.size();
     140             :       std::unordered_set<propositional_variable_instantiation> new_irrelevant;
     141             :       for (const propositional_variable_instantiation& x: todo)
     142             :       {
     143             :         if (!contains(new_todo, x))
     144             :         {
     145             :           new_irrelevant.insert(x);
     146             :         }
     147             :       } 
     148             :       for (const propositional_variable_instantiation& x: irrelevant)
     149             :       {
     150             :         if (!contains(new_todo, x))
     151             :         {
     152             :           new_irrelevant.insert(x);
     153             :         }
     154             :       } 
     155             :       std::swap(todo, new_todo);
     156             :       std::swap(irrelevant, new_irrelevant);
     157             : 
     158             :       std::size_t size_after = todo.size() + irrelevant.size();
     159             :       if (size_before != size_after)
     160             :       {
     161             :         throw mcrl2::runtime_error("sizes do not match in pbesinst_lazy_todo::set_todo");
     162             :       }
     163             :       assert(check_invariants());
     164             :     }
     165             : };
     166             : 
     167             : inline
     168             : std::ostream& operator<<(std::ostream& out, const pbesinst_lazy_todo& todo)
     169             : {
     170             :   return out << "todo = " << core::detail::print_list(todo.elements()) << " irrelevant = " << core::detail::print_list(todo.irrelevant_elements()) << std::endl;
     171             : }
     172             : 
     173             : /// \brief A PBES instantiation algorithm that uses a lazy strategy
     174             : class pbesinst_lazy_algorithm
     175             : {
     176             :   protected:
     177             :     /// \brief Algorithm options.
     178             :     const pbessolve_options& m_options;
     179             : 
     180             :     /// \brief Data rewriter.
     181             :     data::rewriter datar;
     182             : 
     183             :     /// \brief A PBES.
     184             :     pbes m_pbes;
     185             : 
     186             :     /// \brief A lookup map for PBES equations.
     187             :     pbes_equation_index m_equation_index;
     188             : 
     189             :     /// \brief The propositional variable instantiations that need to be handled.
     190             :     pbesinst_lazy_todo todo;
     191             : 
     192             :     /// \brief The propositional variable instantiations that have been discovered (not necessarily handled).
     193             :     atermpp::indexed_set<propositional_variable_instantiation, true> discovered;
     194             : 
     195             :     /// \brief The initial value (after rewriting).
     196             :     propositional_variable_instantiation init;
     197             : 
     198             :     // \brief The number of iterations
     199             :     std::size_t m_iteration_count = 0;
     200             : 
     201             :     // The data structures that must be separate per thread.
     202             :     /// \brief The rewriter.
     203             :     enumerate_quantifiers_rewriter m_global_R;
     204             : 
     205             :     // Mutexes
     206             :     utilities::mutex m_todo_access;
     207             : 
     208             :     volatile bool m_must_abort = false;
     209             : 
     210             :     // \brief Returns a status message about the progress
     211           0 :     virtual std::string status_message(std::size_t equation_count)
     212             :     {
     213           0 :       if (equation_count > 0 && equation_count % 1000 == 0)
     214             :       {
     215           0 :         std::ostringstream out;
     216           0 :         out << "Generated " << equation_count << " BES equations" << std::endl;
     217           0 :         return out.str();
     218           0 :       }
     219           0 :       return "";
     220             :     }
     221             : 
     222             :     // instantiates global variables
     223             :     // simplifies the pbes
     224         133 :     pbes preprocess(const pbes& x) const
     225             :     {
     226         133 :       pbes p = x;
     227         133 :       pbes_system::detail::instantiate_global_variables(p);
     228             :       pbes_system::one_point_rule_rewriter one_point_rule_rewriter;
     229         133 :       pbes_system::simplify_quantifiers_data_rewriter<mcrl2::data::rewriter> simplify_rewriter(datar);
     230         606 :       for (pbes_equation& eqn: p.equations())
     231             :       {
     232         473 :         eqn.formula() = order_quantified_variables(one_point_rule_rewriter(simplify_rewriter(eqn.formula())), p.data());
     233             :       }
     234         266 :       return p;
     235           0 :     }
     236             : 
     237           0 :     static void rewrite_true_false(pbes_expression& result,
     238             :                                    const fixpoint_symbol& symbol,
     239             :                                    const propositional_variable_instantiation& X,
     240             :                                    const pbes_expression& psi
     241             :                                   )
     242             :     {
     243           0 :       bool changed = false;
     244           0 :       replace_propositional_variables(
     245             :         result,
     246             :         psi,
     247           0 :         [&](const propositional_variable_instantiation& Y) -> pbes_expression
     248             :         {
     249           0 :           if (Y == X)
     250             :           {
     251           0 :             changed = true;
     252           0 :             if (symbol.is_mu())
     253             :             {
     254           0 :               return false_();
     255             :             }
     256             :             else
     257             :             {
     258           0 :               return true_();
     259             :             }
     260             :           }
     261           0 :           return Y;
     262             :         }
     263             :       );
     264           0 :       if (changed)
     265             :       {
     266             :         simplify_rewriter simplify;
     267           0 :         const pbes_expression result1=result;
     268           0 :         simplify(result, result1);
     269           0 :       }
     270           0 :     }
     271             : 
     272         133 :     data::rewriter construct_rewriter(const pbes& pbesspec)
     273             :     {
     274         133 :       if (m_options.remove_unused_rewrite_rules)
     275             :       {
     276             :         return data::rewriter(pbesspec.data(),
     277           0 :                               data::used_data_equation_selector(pbesspec.data(), pbes_system::find_function_symbols(pbesspec), pbesspec.global_variables()),
     278           0 :                               m_options.rewrite_strategy);
     279             :       }
     280             :       else
     281             :       {
     282         133 :         return data::rewriter(pbesspec.data(), m_options.rewrite_strategy);
     283             :       }
     284             :     }
     285             : 
     286             :   public:
     287             : 
     288             :     /// \brief Constructor.
     289             :     /// \param p The pbes used in the exploration algorithm.
     290             :     /// \param rewrite_strategy A strategy for the data rewriter.
     291             :     /// \param search_strategy The search strategy used to explore the pbes, typically depth or breadth first.
     292             :     /// \param optimization An indication of the optimisation level.
     293         133 :     explicit pbesinst_lazy_algorithm(
     294             :       const pbessolve_options& options,
     295             :       const pbes& p
     296             :     )
     297         133 :      : m_options(options),
     298         133 :        datar(construct_rewriter(p)),
     299         133 :        m_pbes(preprocess(p)),
     300         133 :        m_equation_index(p),
     301         133 :        discovered(m_options.number_of_threads),
     302         399 :        m_global_R(datar, p.data())
     303         133 :     { }
     304             : 
     305         133 :     virtual ~pbesinst_lazy_algorithm() = default;
     306             : 
     307             :     /// \brief Reports BES equations that are produced by the algorithm.
     308             :     /// This function is called for every BES equation X = psi with rank k that is produced. By default it does nothing.
     309           0 :     virtual void on_report_equation(const std::size_t /* thread_index */,
     310             :                                     const propositional_variable_instantiation& /* X */,
     311             :                                     const pbes_expression& /* psi */, std::size_t /* k */
     312             :                                    )
     313           0 :     { }
     314             : 
     315             :     /// \brief This function is called when new elements are added to discovered.
     316        3549 :     virtual void on_discovered_elements(const std::set<propositional_variable_instantiation>& /* elements */)
     317        3549 :     { }
     318             : 
     319             :     /// \brief This function is called right after the while loop is finished.
     320         133 :     virtual void on_end_while_loop()
     321         133 :     { }
     322             : 
     323        3549 :     void next_todo(propositional_variable_instantiation& result)
     324             :     {
     325        3549 :       if (m_options.exploration_strategy == breadth_first)
     326             :       {
     327        3549 :         result = todo.front();
     328        3549 :         todo.pop_front();
     329             :       }
     330             :       else
     331             :       {
     332           0 :         result = todo.back();
     333           0 :         todo.pop_back();
     334             :       }
     335        3549 :     }
     336             : 
     337             :     const fixpoint_symbol& symbol(std::size_t i) const
     338             :     {
     339             :       return m_pbes.equations()[i].symbol();
     340             :     }
     341             : 
     342             :     // rewrite the right hand side of the equation X = psi
     343        3549 :     virtual void rewrite_psi(const std::size_t /* thread_index */,
     344             :                              pbes_expression& result,
     345             :                              const fixpoint_symbol& symbol,
     346             :                              const propositional_variable_instantiation& X,
     347             :                              const pbes_expression& psi
     348             :                             )
     349             :     {
     350        3549 :       if (m_options.optimization >= 1)
     351             :       {
     352           0 :         rewrite_true_false(result, symbol, X, psi);
     353             :       }
     354             :       else
     355             :       {
     356        3549 :         result = psi;
     357             :       }
     358        3549 :     }
     359             : 
     360        3549 :     virtual bool solution_found(const propositional_variable_instantiation& /* init */) const
     361             :     {
     362        3549 :       return false;
     363             :     }
     364             : 
     365         133 :     virtual void run_thread(const std::size_t thread_index,
     366             :                             pbesinst_lazy_todo& todo,
     367             :                             std::atomic<std::size_t>& number_of_active_processes,
     368             :                             data::mutable_indexed_substitution<> sigma,
     369             :                             enumerate_quantifiers_rewriter R
     370             :                            )
     371             :     {
     372             :       using utilities::detail::contains;
     373             : 
     374         133 :       if (m_options.number_of_threads > 1) mCRL2log(log::debug) << "Start thread " << thread_index << ".\n";
     375         133 :       R.thread_initialise();
     376             : 
     377         133 :       propositional_variable_instantiation X_e;
     378         133 :       pbes_expression psi_e;
     379             : 
     380         266 :       while (number_of_active_processes > 0)
     381             :       {
     382         133 :         m_todo_access.lock();
     383        3682 :         while (!todo.elements().empty() && !m_must_abort)
     384             :         {
     385        3549 :           ++m_iteration_count;
     386        3549 :           mCRL2log(log::status) << status_message(m_iteration_count);
     387        3549 :           detail::check_bes_equation_limit(m_iteration_count);
     388             : 
     389        3549 :           next_todo(X_e);
     390        3549 :           m_todo_access.unlock();
     391             : 
     392        3549 :           std::size_t index = m_equation_index.index(X_e.name());
     393        3549 :           const pbes_equation& eqn = m_pbes.equations()[index];
     394        3549 :           const auto& phi = eqn.formula();
     395        3549 :           data::add_assignments(sigma, eqn.variable().parameters(), X_e.parameters());
     396        3549 :           R(psi_e, phi, sigma);
     397        3549 :           R.clear_identifier_generator();
     398        3549 :           data::remove_assignments(sigma, eqn.variable().parameters());
     399             : 
     400             :           // optional step
     401        3549 :           m_todo_access.lock();
     402        3549 :           rewrite_psi(thread_index, psi_e, eqn.symbol(), X_e, psi_e);
     403        3549 :           m_todo_access.unlock();
     404             : 
     405        3549 :           std::set<propositional_variable_instantiation> occ = find_propositional_variable_instantiations(psi_e);
     406             : 
     407             :           // report the generated equation
     408        3549 :           std::size_t k = m_equation_index.rank(X_e.name());
     409        3549 :           m_todo_access.lock();
     410        3549 :           mCRL2log(log::debug) << "generated equation " << X_e << " = " << psi_e
     411           0 :                                << " with rank " << k << std::endl;
     412        3549 :           on_report_equation(thread_index, X_e, psi_e, k);
     413        3549 :           todo.insert(occ.begin(), occ.end(), discovered, thread_index);
     414        9140 :           for (auto i = occ.begin(); i != occ.end(); ++i)
     415             :           {
     416        5591 :             discovered.insert(*i, thread_index);
     417             :           }
     418        3549 :           on_discovered_elements(occ);
     419             : 
     420        3549 :           if (solution_found(init))
     421             :           {
     422           0 :             break;
     423             :           }
     424        3549 :         }
     425         133 :         m_todo_access.unlock();
     426             : 
     427             :         // Check whether all processes are ready. If so the
     428             :         // number_of_active_processes becomes 0. Otherwise, this thread becomes
     429             :         // active again, and tries to see whether the todo buffer is not empty,
     430             :         // to take up more work.
     431         133 :         number_of_active_processes--;
     432         133 :         std::this_thread::sleep_for(std::chrono::milliseconds(100));
     433         133 :         if (number_of_active_processes > 0)
     434             :         {
     435           0 :           number_of_active_processes++;
     436             :         }
     437             :       }
     438             : 
     439         133 :       if (m_options.number_of_threads>1) mCRL2log(log::debug) << "Stop thread " << thread_index << ".\n";
     440         133 :     }
     441             : 
     442             :     /// \brief Runs the algorithm. The result is obtained by calling the function \p get_result.
     443         133 :     virtual void run()
     444             :     {
     445         133 :       m_iteration_count = 0;
     446             : 
     447         133 :       const std::size_t number_of_threads = m_options.number_of_threads;
     448         133 :       const std::size_t initialisation_thread_index = (number_of_threads==1?0:1);
     449         133 :       std::atomic<std::size_t> number_of_active_processes = number_of_threads;
     450         133 :       std::vector<std::thread> threads;
     451             : 
     452         133 :       data::mutable_indexed_substitution<> sigma;
     453         133 :       if (m_options.replace_constants_by_variables)
     454             :       {
     455           0 :         pbes_system::replace_constants_by_variables(m_pbes, datar, sigma);
     456             :       }
     457             : 
     458         133 :       init = atermpp::down_cast<propositional_variable_instantiation>(m_global_R(m_pbes.initial_state(), sigma));
     459         133 :       todo.insert(init);
     460         133 :       discovered.insert(init, initialisation_thread_index);
     461             : 
     462         133 :       if (number_of_threads>1)
     463             :       {
     464           0 :         threads.reserve(number_of_threads);
     465           0 :         for (std::size_t i = 1; i <= number_of_threads; ++i)
     466             :         {
     467           0 :           std::thread tr([&, i](){
     468           0 :             run_thread(i,
     469           0 :                        todo,
     470           0 :                        number_of_active_processes,
     471           0 :                        sigma.clone(),
     472           0 :                        m_global_R.clone()
     473             :                       );
     474           0 :           });
     475           0 :           threads.push_back(std::move(tr));
     476           0 :         }
     477             : 
     478           0 :         for (std::size_t i = 1; i <= number_of_threads; ++i)
     479             :         {
     480           0 :           threads[i-1].join();
     481             :         }
     482             :       }
     483             :       else 
     484             :       {
     485             :         // There is only one thread. Run the process in the main thread, without cloning sigma or the rewriter.
     486         133 :         const std::size_t single_thread_index=0;
     487         266 :         run_thread(single_thread_index,
     488         133 :                    todo,
     489             :                    number_of_active_processes,
     490             :                    sigma,
     491         133 :                    m_global_R
     492             :                   );
     493             :       }
     494         133 :       on_end_while_loop();
     495         133 :     }
     496             : 
     497             :     const pbes_equation_index& equation_index() const
     498             :     {
     499             :       return m_equation_index;
     500             :     }
     501             : 
     502             :     enumerate_quantifiers_rewriter& rewriter()
     503             :     {
     504             :       return m_global_R;
     505             :     }
     506             : };
     507             : 
     508             : } // namespace pbes_system
     509             : 
     510             : } // namespace mcrl2
     511             : 
     512             : #endif // MCRL2_PBES_PBESINST_LAZY_H

Generated by: LCOV version 1.14