LCOV - code coverage report
Current view: top level - pg/source - FocusListLiftingStrategy.cpp (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 0 59 0.0 %
Date: 2020-09-16 00:45:56 Functions: 0 8 0.0 %
Legend: Lines: hit not hit

          Line data    Source code
       1             : // Copyright (c) 2009-2013 University of Twente
       2             : // Copyright (c) 2009-2013 Michael Weber <michaelw@cs.utwente.nl>
       3             : // Copyright (c) 2009-2013 Maks Verver <maksverver@geocities.com>
       4             : // Copyright (c) 2009-2013 Eindhoven University of Technology
       5             : //
       6             : // Distributed under the Boost Software License, Version 1.0.
       7             : // (See accompanying file LICENSE_1_0.txt or copy at
       8             : // http://www.boost.org/LICENSE_1_0.txt)
       9             : 
      10             : #include "mcrl2/pg/FocusListLiftingStrategy.h"
      11             : 
      12             : /*! Credit for a vertex when it is put on the focus list. */
      13             : static const unsigned initial_credit  = 2;
      14             : 
      15             : /*! Credit increase when a vertex on the focus list is successfully lifted. */
      16             : static const unsigned credit_increase = 2;
      17             : 
      18             : 
      19           0 : FocusListLiftingStrategy::FocusListLiftingStrategy( const ParityGame &game,
      20           0 :     bool alternate, verti max_size, std::size_t max_lifts )
      21           0 :     : LiftingStrategy(), V_(game.graph().V()), max_lift_attempts_(max_lifts),
      22           0 :       phase_(1), num_lift_attempts_(0), lls_(game, alternate)
      23             : {
      24           0 :     focus_list_.reserve(max_size);
      25           0 : }
      26             : 
      27           0 : void FocusListLiftingStrategy::lifted(verti vertex)
      28             : {
      29           0 :     if (phase_ == 1)
      30             :     {
      31           0 :         lls_.lifted(vertex);
      32           0 :         if (focus_list_.size() < focus_list_.capacity())
      33             :         {
      34           0 :             focus_list_.push_back(std::make_pair(vertex, initial_credit));
      35             :         }
      36             :     }
      37             :     else /* phase_ == 2 */
      38             :     {
      39           0 :         if (vertex == read_pos_->first) prev_lifted_ = true;
      40             :     }
      41           0 : }
      42             : 
      43           0 : verti FocusListLiftingStrategy::next()
      44             : {
      45           0 :     verti res =  phase_ == 1 ? phase1() : phase2();
      46           0 :     ++num_lift_attempts_;
      47           0 :     return res;
      48             : }
      49             : 
      50           0 : verti FocusListLiftingStrategy::phase1()
      51             : {
      52           0 :     if (focus_list_.size() == focus_list_.capacity() ||
      53           0 :         num_lift_attempts_ >= V_)
      54             :     {
      55           0 :         if (focus_list_.empty())
      56             :         {
      57             :             /* This can only happen if lls_.num_failed >= V too */
      58           0 :             assert(lls_.next() == NO_VERTEX);
      59           0 :             return NO_VERTEX;
      60             :         }
      61             : 
      62             :         /* Switch to phase 2: */
      63           0 :         phase_ = 2;
      64           0 :         num_lift_attempts_ = 0;
      65           0 :         read_pos_ = write_pos_ = focus_list_.begin();
      66           0 :         mCRL2log(mcrl2::log::verbose) << "Switching to focus list of size " << focus_list_.size() << std::endl;
      67           0 :         return phase2();
      68             :     }
      69             : 
      70           0 :     return lls_.next();
      71             : }
      72             : 
      73           0 : verti FocusListLiftingStrategy::phase2()
      74             : {
      75           0 :     if (num_lift_attempts_ > 0)
      76             :     {
      77             :         // Adjust previous vertex credit and move to next position
      78           0 :         focus_list::value_type prev = *read_pos_++;
      79           0 :         if (prev_lifted_)
      80             :         {
      81           0 :             prev.second += credit_increase;
      82           0 :             *write_pos_++ = prev;
      83             :         }
      84             :         else
      85           0 :         if (prev.second > 0)
      86             :         {
      87           0 :             prev.second /= 2;
      88           0 :             *write_pos_++ = prev;
      89             :         }
      90             :         // else, drop from list.
      91             :     }
      92             : 
      93             :     // Check if we've reached the end of the focus list; if so, restart:
      94           0 :     if (read_pos_ == focus_list_.end())
      95             :     {
      96           0 :         focus_list_.erase(write_pos_, focus_list_.end());
      97           0 :         read_pos_ = write_pos_ = focus_list_.begin();
      98             :     }
      99             : 
     100           0 :     if (focus_list_.empty() || num_lift_attempts_ >= max_lift_attempts_)
     101             :     {
     102           0 :         if (focus_list_.empty())
     103             :         {
     104           0 :             mCRL2log(mcrl2::log::verbose) << "Focus list exhausted." << std::endl;
     105             :         }
     106             :         else
     107             :         {
     108           0 :             mCRL2log(mcrl2::log::verbose) << "Maximum lift attempts (" << max_lift_attempts_ << ") on focus list reached." << std::endl;
     109           0 :             focus_list_.clear();
     110             :         }
     111             : 
     112             :         /* Switch to phase 1 */
     113           0 :         phase_ = 1;
     114           0 :         num_lift_attempts_ = 0;
     115           0 :         return phase1();
     116             :     }
     117             : 
     118             :     // Return current item on the focus list
     119           0 :     prev_lifted_ = false;
     120           0 :     return read_pos_->first;
     121             : }
     122             : 
     123           0 : LiftingStrategy *FocusListLiftingStrategyFactory::create(
     124             :     const ParityGame &game, const SmallProgressMeasures &spm )
     125             : {
     126             :     (void)spm;  // unused
     127             : 
     128             :     /* Ratio is absolute value if >1, or a fraction of the size of the game's
     129             :        vertex set if <= 1. */
     130           0 :     verti V = game.graph().V();
     131           0 :     verti max_size  = (size_ratio_ > 1) ? static_cast<verti>(size_ratio_) : static_cast<verti>(size_ratio_*V); // XXX Ugly casting here
     132           0 :     if (max_size == 0) max_size = 1;
     133           0 :     if (max_size >  V) max_size = V;
     134           0 :     verti max_lifts = (verti)(lift_ratio_ * max_size);
     135             :     return new FocusListLiftingStrategy(
     136           0 :         game, alternate_, max_size, max_lifts );
     137           0 : }

Generated by: LCOV version 1.13