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 : }