1 // -*- coding: utf-8 -*- 2 // Copyright (C) 2010-2011, 2013-2016, 2018 Laboratoire de 3 // Recherche et Développement de l'Epita (LRDE). 4 // Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), 5 // département Systèmes Répartis Coopératifs (SRC), Université Pierre 6 // et Marie Curie. 7 // 8 // This file is part of Spot, a model checking library. 9 // 10 // Spot is free software; you can redistribute it and/or modify it 11 // under the terms of the GNU General Public License as published by 12 // the Free Software Foundation; either version 3 of the License, or 13 // (at your option) any later version. 14 // 15 // Spot is distributed in the hope that it will be useful, but WITHOUT 16 // ANY WARRANTY; without even the implied warranty of MERCHANTABILITY 17 // or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public 18 // License for more details. 19 // 20 // You should have received a copy of the GNU General Public License 21 // along with this program. If not, see <http://www.gnu.org/licenses/>. 22 23 #include "config.h" 24 #include <spot/twaalgos/gtec/ce.hh> 25 #include <spot/twaalgos/bfssteps.hh> 26 #include <spot/misc/hash.hh> 27 28 namespace spot 29 { 30 namespace 31 { 32 class shortest_path final: public bfs_steps 33 { 34 public: shortest_path(const state_set * t,const std::shared_ptr<const couvreur99_check_status> & ecs,couvreur99_check_result * r)35 shortest_path(const state_set* t, 36 const std::shared_ptr<const couvreur99_check_status>& ecs, 37 couvreur99_check_result* r) 38 : bfs_steps(ecs->aut), target(t), ecs(ecs), r(r) 39 { 40 } 41 42 const state* search(const state * start,twa_run::steps & l)43 search(const state* start, twa_run::steps& l) 44 { 45 return this->bfs_steps::search(filter(start), l); 46 } 47 48 const state* filter(const state * s)49 filter(const state* s) override 50 { 51 r->inc_ars_prefix_states(); 52 auto i = ecs->h.find(s); 53 s->destroy(); 54 // Ignore unknown states ... 55 if (i == ecs->h.end()) 56 return nullptr; 57 // ... as well as dead states. 58 if (i->second == -1) 59 return nullptr; 60 return i->first; 61 } 62 63 bool match(twa_run::step &,const state * dest)64 match(twa_run::step&, const state* dest) override 65 { 66 return target->find(dest) != target->end(); 67 } 68 69 private: 70 state_set seen; 71 const state_set* target; 72 std::shared_ptr<const couvreur99_check_status> ecs; 73 couvreur99_check_result* r; 74 }; 75 } 76 couvreur99_check_result(const std::shared_ptr<const couvreur99_check_status> & ecs,option_map o)77 couvreur99_check_result::couvreur99_check_result 78 (const std::shared_ptr<const couvreur99_check_status>& ecs, 79 option_map o) 80 : emptiness_check_result(ecs->aut, o), ecs_(ecs) 81 { 82 } 83 84 unsigned acss_states() const85 couvreur99_check_result::acss_states() const 86 { 87 int scc_root = ecs_->root.top().index; 88 unsigned count = 0; 89 for (auto i: ecs_->h) 90 if (i.second >= scc_root) 91 ++count; 92 return count; 93 } 94 95 twa_run_ptr accepting_run()96 couvreur99_check_result::accepting_run() 97 { 98 run_ = std::make_shared<twa_run>(ecs_->aut); 99 100 assert(!ecs_->root.empty()); 101 102 // Compute an accepting cycle. 103 accepting_cycle(); 104 105 // Compute the prefix: it's the shortest path from the initial 106 // state of the automata to any state of the cycle. 107 108 // Register all states from the cycle as target of the BFS. 109 state_set ss; 110 for (twa_run::steps::const_iterator i = run_->cycle.begin(); 111 i != run_->cycle.end(); ++i) 112 ss.insert(i->s); 113 shortest_path shpath(&ss, ecs_, this); 114 115 const state* prefix_start = ecs_->aut->get_init_state(); 116 // There are two cases: either the initial state is already on 117 // the cycle, or it is not. If it is, we will have to rotate 118 // the cycle so it begins on this position. Otherwise we will shift 119 // the cycle so it begins on the state that follows the prefix. 120 // cycle_entry_point is that state. 121 const state* cycle_entry_point; 122 state_set::const_iterator ps = ss.find(prefix_start); 123 if (ps != ss.end()) 124 { 125 // The initial state is on the cycle. 126 prefix_start->destroy(); 127 cycle_entry_point = *ps; 128 } 129 else 130 { 131 // This initial state is outside the cycle. Compute the prefix. 132 cycle_entry_point = shpath.search(prefix_start, run_->prefix); 133 } 134 135 // Locate cycle_entry_point on the cycle. 136 twa_run::steps::iterator cycle_ep_it; 137 for (cycle_ep_it = run_->cycle.begin(); 138 cycle_ep_it != run_->cycle.end() 139 && cycle_entry_point->compare(cycle_ep_it->s); ++cycle_ep_it) 140 continue; 141 assert(cycle_ep_it != run_->cycle.end()); 142 143 // Now shift the cycle so it starts on cycle_entry_point. 144 run_->cycle.splice(run_->cycle.end(), run_->cycle, 145 run_->cycle.begin(), cycle_ep_it); 146 147 return run_; 148 } 149 150 void accepting_cycle()151 couvreur99_check_result::accepting_cycle() 152 { 153 acc_cond::mark_t acc_to_traverse = 154 ecs_->aut->acc().accepting_sets(ecs_->root.top().condition); 155 // Compute an accepting cycle using successive BFS that are 156 // restarted from the point reached after we have discovered a 157 // transition with a new acceptance conditions. 158 // 159 // This idea is taken from Product<T>::findWitness in LBTT 1.1.2, 160 // which in turn is probably inspired from 161 // @Article{ latvala.00.fi, 162 // author = {Timo Latvala and Keijo Heljanko}, 163 // title = {Coping With Strong Fairness}, 164 // journal = {Fundamenta Informaticae}, 165 // year = {2000}, 166 // volume = {43}, 167 // number = {1--4}, 168 // pages = {1--19}, 169 // publisher = {IOS Press} 170 // } 171 const state* substart = ecs_->cycle_seed; 172 do 173 { 174 struct scc_bfs final: bfs_steps 175 { 176 const couvreur99_check_status* ecs; 177 couvreur99_check_result* r; 178 acc_cond::mark_t& acc_to_traverse; 179 int scc_root; 180 181 scc_bfs(const couvreur99_check_status* ecs, 182 couvreur99_check_result* r, acc_cond::mark_t& acc_to_traverse) 183 : bfs_steps(ecs->aut), ecs(ecs), r(r), 184 acc_to_traverse(acc_to_traverse), 185 scc_root(ecs->root.top().index) 186 { 187 } 188 189 virtual const state* 190 filter(const state* s) override 191 { 192 auto i = ecs->h.find(s); 193 s->destroy(); 194 // Ignore unknown states. 195 if (i == ecs->h.end()) 196 return nullptr; 197 // Stay in the final SCC. 198 if (i->second < scc_root) 199 return nullptr; 200 r->inc_ars_cycle_states(); 201 return i->first; 202 } 203 204 virtual bool 205 match(twa_run::step& st, const state* s) override 206 { 207 acc_cond::mark_t less_acc = 208 acc_to_traverse - st.acc; 209 if (less_acc != acc_to_traverse 210 || (!acc_to_traverse 211 && s == ecs->cycle_seed)) 212 { 213 acc_to_traverse = less_acc; 214 return true; 215 } 216 return false; 217 } 218 219 } b(ecs_.get(), this, acc_to_traverse); 220 221 substart = b.search(substart, run_->cycle); 222 assert(substart); 223 } 224 while (acc_to_traverse || substart != ecs_->cycle_seed); 225 } 226 227 void print_stats(std::ostream & os) const228 couvreur99_check_result::print_stats(std::ostream& os) const 229 { 230 ecs_->print_stats(os); 231 // FIXME: This is bogusly assuming run_ exists. (Even if we 232 // created it, the user might have deleted it.) 233 os << run_->prefix.size() << " states in run_->prefix" << std::endl; 234 os << run_->cycle.size() << " states in run_->cycle" << std::endl; 235 } 236 237 } 238