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/pbessolve_attractors.h
      10             : /// \brief add your file description here.
      11             : 
      12             : #ifndef MCRL2_PBES_PBESSOLVE_ATTRACTORS_H
      13             : #define MCRL2_PBES_PBESSOLVE_ATTRACTORS_H
      14             : 
      15             : #include "mcrl2/pbes/pbessolve_vertex_set.h"
      16             : 
      17             : namespace mcrl2 {
      18             : 
      19             : namespace pbes_system {
      20             : 
      21             : // Does not set a strategy
      22             : struct no_strategy
      23             : {
      24             :   static void set_strategy(structure_graph::index_type /* u */, structure_graph::index_type /* v */)
      25             :   {}
      26             : };
      27             : 
      28             : // Puts strategy annotations in the strategy attributes of the nodes of graph G
      29             : template <typename StructureGraph>
      30             : struct global_strategy
      31             : {
      32             :   const StructureGraph& G;
      33             : 
      34         232 :   explicit global_strategy(const StructureGraph& G_)
      35         232 :    : G(G_)
      36         232 :   {}
      37             : 
      38        2603 :   void set_strategy(structure_graph::index_type u, structure_graph::index_type v)
      39             :   {
      40        2603 :     if (v == undefined_vertex())
      41             :     {
      42           0 :       mCRL2log(log::debug) << "Error: undefined strategy for node " << u << std::endl;
      43             :     }
      44        2603 :     mCRL2log(log::debug) << "  set tau[" << u << "] = " << v << std::endl;
      45        2603 :     G.find_vertex(u).strategy = v;
      46        2603 :   }
      47             : };
      48             : 
      49             : // Puts strategy annotations in tau[alpha]
      50             : struct local_strategy
      51             : {
      52             :   std::array<strategy_vector, 2>& tau;
      53             :   std::size_t alpha;
      54             : 
      55             :   local_strategy(std::array<strategy_vector, 2>& tau_, std::size_t alpha_)
      56             :     : tau(tau_), alpha(alpha_)
      57             :   {}
      58             : 
      59             :   void set_strategy(structure_graph::index_type u, structure_graph::index_type v)
      60             :   {
      61             :     if (v == undefined_vertex())
      62             :     {
      63             :       mCRL2log(log::debug) << "Error: undefined strategy for node " << u << std::endl;
      64             :     }
      65             :     mCRL2log(log::debug) << "  set tau" << alpha << "[" << u << "] = " << v << std::endl;
      66             :     tau[alpha][u] = v;
      67             :   }
      68             : };
      69             : 
      70             : // Combination of global and local strategy
      71             : template <typename StructureGraph>
      72             : struct global_local_strategy
      73             : {
      74             :   global_strategy<StructureGraph> global;
      75             :   local_strategy local;
      76             : 
      77             :   global_local_strategy(const StructureGraph& G, std::array<strategy_vector, 2>& tau, std::size_t alpha)
      78             :    : global(G), local(tau, alpha)
      79             :   {}
      80             : 
      81             :   void set_strategy(structure_graph::index_type u, structure_graph::index_type v)
      82             :   {
      83             :     global.set_strategy(u, v);
      84             :     local.set_strategy(u, v);
      85             :   }
      86             : };
      87             : 
      88             : // Returns true if succ(u) \subseteq A
      89             : template <typename StructureGraph, typename VertexSet>
      90        2066 : bool includes_successors(const StructureGraph& G, typename StructureGraph::index_type u, const VertexSet& A)
      91             : {
      92        8492 :   for (auto v: G.successors(u))
      93             :   {
      94        3072 :     if (!A.contains(v))
      95             :     {
      96         644 :       return false;
      97             :     }
      98             :   }
      99        1422 :   return true;
     100             : }
     101             : 
     102             : // Returns pred(A) \ A
     103             : template <typename StructureGraph>
     104         231 : deque_vertex_set exclusive_predecessors(const StructureGraph& G, const vertex_set& A)
     105             : {
     106             :   // put all predecessors of elements in A in todo
     107         231 :   deque_vertex_set todo(G.all_vertices().size());
     108        1778 :   for (auto u: A.vertices())
     109             :   {
     110        5447 :     for (auto v: G.predecessors(u))
     111             :     {
     112        2353 :       if (!A.contains(v))
     113             :       {
     114        1860 :         todo.insert(v);
     115             :       }
     116             :     }
     117             :   }
     118         231 :   return todo;
     119           0 : }
     120             : 
     121             : // Inserts pred(u) \ A into todo
     122             : template <typename StructureGraph>
     123        2602 : void insert_predecessors(const StructureGraph& G, structure_graph::index_type u, const vertex_set& A, deque_vertex_set& todo)
     124             : {
     125        8889 :   for (auto v: G.predecessors(u))
     126             :   {
     127        3685 :     if (!A.contains(v))
     128             :     {
     129        2182 :       todo.insert(v);
     130             :     }
     131             :   }
     132        2602 : }
     133             : 
     134             : // Computes an attractor set, by extending A.
     135             : // alpha = 0: disjunctive
     136             : // alpha = 1: conjunctive
     137             : // StructureGraph is either structure_graph or simple_structure_graph
     138             : // Strategy is either no_strategy, global_strategy, local_strategy or global_local_strategy
     139             : template <typename StructureGraph, typename Strategy>
     140         231 : vertex_set attr_default_generic(const StructureGraph& G, vertex_set A, std::size_t alpha, Strategy tau)
     141             : {
     142         231 :   deque_vertex_set todo = exclusive_predecessors(G, A);
     143             : 
     144        3477 :   while (!todo.is_empty())
     145             :   {
     146             :     // N.B. Use a breadth first search, to minimize counter examples
     147        3246 :     auto u = todo.pop_front();
     148             : 
     149        3246 :     if (G.decoration(u) == alpha || includes_successors(G, u, A))
     150             :     {
     151        2602 :       tau.set_strategy(u, find_successor_in(G, u, A));
     152        2602 :       A.insert(u);
     153        2602 :       insert_predecessors(G, u, A, todo);
     154             :     }
     155             :   }
     156             : 
     157         462 :   return A;
     158         231 : }
     159             : 
     160             : // Computes an attractor set, by extending A.
     161             : // alpha = 0: disjunctive
     162             : // alpha = 1: conjunctive
     163             : // StructureGraph is either structure_graph or simple_structure_graph
     164             : template <typename StructureGraph>
     165         231 : vertex_set attr_default(const StructureGraph& G, vertex_set A, std::size_t alpha)
     166             : {
     167         231 :   return attr_default_generic(G, A, alpha, global_strategy<StructureGraph>(G));
     168             : }
     169             : 
     170             : // Variant of attr_default that does not set any strategies.
     171             : template <typename StructureGraph>
     172             : vertex_set attr_default_no_strategy(const StructureGraph& G, vertex_set A, std::size_t alpha)
     173             : {
     174             :   return attr_default_generic(G, A, alpha, no_strategy());
     175             : }
     176             : 
     177             : // Computes an attractor set, by extending A.
     178             : // alpha = 0: disjunctive
     179             : // alpha = 1: conjunctive
     180             : // StructureGraph is either structure_graph or simple_structure_graph
     181             : template <typename StructureGraph>
     182             : vertex_set attr_default_with_tau(const StructureGraph& G, vertex_set A, std::size_t alpha, std::array<strategy_vector, 2>& tau)
     183             : {
     184             :   return attr_default_generic(G, A, alpha, global_local_strategy<StructureGraph>(G, tau, alpha));
     185             : }
     186             : 
     187             : } // namespace pbes_system
     188             : 
     189             : } // namespace mcrl2
     190             : 
     191             : #endif // MCRL2_PBES_PBESSOLVE_ATTRACTORS_H