1 // -*- coding: utf-8 -*- 2 // Copyright (C) 2012-2014, 2016, 2018, 2019 Laboratoire de Recherche 3 // et Dévelopment de l'Epita (LRDE). 4 // 5 // This file is part of Spot, a model checking library. 6 // 7 // Spot is free software; you can redistribute it and/or modify it 8 // under the terms of the GNU General Public License as published by 9 // the Free Software Foundation; either version 3 of the License, or 10 // (at your option) any later version. 11 // 12 // Spot is distributed in the hope that it will be useful, but WITHOUT 13 // ANY WARRANTY; without even the implied warranty of MERCHANTABILITY 14 // or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public 15 // License for more details. 16 // 17 // You should have received a copy of the GNU General Public License 18 // along with this program. If not, see <http://www.gnu.org/licenses/>. 19 20 #pragma once 21 22 #include <spot/ta/taproduct.hh> 23 #include <spot/misc/optionmap.hh> 24 #include <spot/twaalgos/emptiness_stats.hh> 25 #include <stack> 26 #include <queue> 27 28 namespace spot 29 { 30 31 namespace 32 { 33 typedef std::pair<const spot::state*, 34 ta_succ_iterator_product*> pair_state_iter; 35 } 36 37 /// \addtogroup ta_emptiness_check Emptiness-checks 38 /// \ingroup ta_algorithms 39 40 /// \ingroup ta_emptiness_check 41 /// \brief Check whether the language of a product (spot::ta_product) between 42 /// a Kripke structure and a TA is empty. It works also for the product 43 /// using Generalized TA (GTA and SGTA). 44 /// 45 /// you should call spot::ta_check::check() to check the product automaton. 46 /// If spot::ta_check::check() returns false, then the product automaton 47 /// was found empty. Otherwise the automaton accepts some run. 48 /// 49 /// This is based on \cite geldenhuys.06.spin . 50 /// 51 /// the implementation of spot::ta_check::check() is inspired from the 52 /// two-pass algorithm of the paper above: 53 /// - the fist-pass detect all Buchi-accepting cycles and includes 54 /// the heuristic proposed in the paper to detect some 55 /// livelock-accepting cycles. 56 /// - the second-pass detect all livelock-accepting cycles. 57 /// In addition, we add some optimizations to the fist pass: 58 /// 1- Detection of all cycles containing a least 59 /// one state that is both livelock and Buchi accepting states 60 /// 2- Detection of all livelock-accepting cycles containing a least 61 /// one state (k,t) such as its "TA component" t is a livelock-accepting 62 /// state that has no successors in the TA automaton. 63 /// 64 /// The implementation of the algorithm of each pass is a SCC-based algorithm 65 /// inspired from spot::gtec.hh. 66 /// @{ 67 68 /// \brief An implementation of the emptiness-check algorithm for a product 69 /// between a TA and a Kripke structure 70 /// 71 /// See the paper cited above. 72 class SPOT_API ta_check : public ec_statistics 73 { 74 typedef state_map<int> hash_type; 75 public: 76 ta_check(const const_ta_product_ptr& a, option_map o = option_map()); 77 virtual 78 ~ta_check(); 79 80 /// \brief Check whether the TA product automaton contains an accepting run: 81 /// it detects the two kinds of accepting runs: Buchi-accepting runs 82 /// and livelock-accepting runs. This emptiness check algorithm can also 83 /// check a product using the generalized form of TA. 84 /// 85 /// Return false if the product automaton accepts no run, otherwise true 86 /// 87 /// \param disable_second_pass is used to disable the second pass when 88 /// when it is not necessary, for example when all the livelock-accepting 89 /// states of the TA automaton have no successors, we call this kind of 90 /// TA as STA (Single-pass Testing Automata) 91 /// (see spot::tgba2ta::add_artificial_livelock_accepting_state() for an 92 /// automatic transformation of any TA automaton into STA automaton 93 /// 94 /// \param disable_heuristic_for_livelock_detection disable the heuristic 95 /// used in the first pass to detect livelock-accepting runs, 96 /// this heuristic is described in the paper cited above 97 bool 98 check(bool disable_second_pass = false, 99 bool disable_heuristic_for_livelock_detection = false); 100 101 /// \brief Check whether the product automaton contains 102 /// a livelock-accepting run 103 /// Return false if the product automaton accepts no livelock-accepting run, 104 /// otherwise true 105 bool 106 livelock_detection(const const_ta_product_ptr& t); 107 108 /// Print statistics, if any. 109 std::ostream& 110 print_stats(std::ostream& os) const; 111 112 protected: 113 void 114 clear(hash_type& h, std::stack<pair_state_iter> todo, std::queue< 115 const spot::state*> init_set); 116 117 void 118 clear(hash_type& h, std::stack<pair_state_iter> todo, 119 spot::ta_succ_iterator* init_states_it); 120 121 /// the heuristic for livelock-accepting runs detection, it's described 122 /// in the paper cited above 123 bool 124 heuristic_livelock_detection(const state * stuttering_succ, 125 hash_type& h, int h_livelock_root, std::set<const state*, 126 state_ptr_less_than> liveset_curr); 127 128 const_ta_product_ptr a_; ///< The automaton. 129 option_map o_; ///< The options 130 131 // Force the second pass 132 bool is_full_2_pass_; 133 134 // scc: a stack of strongly connected components (SCC) 135 scc_stack_ta scc; 136 137 // sscc: a stack of strongly stuttering-connected components (SSCC) 138 scc_stack_ta sscc; 139 140 }; 141 142 /// @} 143 144 } 145