1 // -*- coding: utf-8 -*- 2 // Copyright (C) 2011, 2012, 2013, 2014, 2016 Laboratoire de Recherche 3 // et Développement 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/twa/twa.hh> 23 #include <spot/twa/twaproduct.hh> 24 #include <spot/misc/fixpool.hh> 25 #include <spot/kripke/kripke.hh> 26 #include <spot/ta/tgta.hh> 27 28 namespace spot 29 { 30 31 /// \brief A lazy product. (States are computed on the fly.) 32 class SPOT_API tgta_product : public twa_product 33 { 34 public: 35 tgta_product(const const_kripke_ptr& left, 36 const const_tgta_ptr& right); 37 38 virtual const state* get_init_state() const override; 39 40 virtual twa_succ_iterator* 41 succ_iter(const state* local_state) const override; 42 }; 43 product(const const_kripke_ptr & left,const const_tgta_ptr & right)44 inline twa_ptr product(const const_kripke_ptr& left, 45 const const_tgta_ptr& right) 46 { 47 return std::make_shared<tgta_product>(left, right); 48 } 49 50 /// \brief Iterate over the successors of a product computed on the fly. 51 class SPOT_API tgta_succ_iterator_product final : public twa_succ_iterator 52 { 53 public: 54 tgta_succ_iterator_product(const state_product* s, 55 const const_kripke_ptr& k, 56 const const_tgta_ptr& tgta, 57 fixed_size_pool<pool_type::Safe>* pool); 58 59 virtual 60 ~tgta_succ_iterator_product(); 61 62 // iteration 63 bool first() override; 64 bool next() override; 65 bool done() const override; 66 67 // inspection 68 state_product* dst() const override; 69 bdd cond() const override; 70 acc_cond::mark_t acc() const override; 71 72 private: 73 //@{ 74 /// Internal routines to advance to the next successor. 75 void 76 step_(); 77 bool find_next_succ_(); 78 79 void 80 next_kripke_dest(); 81 82 //@} 83 84 protected: 85 const state_product* source_; 86 const_tgta_ptr tgta_; 87 const_kripke_ptr kripke_; 88 fixed_size_pool<pool_type::Safe>* pool_; 89 twa_succ_iterator* tgta_succ_it_; 90 twa_succ_iterator* kripke_succ_it_; 91 state_product* current_state_; 92 bdd current_condition_; 93 acc_cond::mark_t current_acceptance_conditions_; 94 bdd kripke_source_condition; 95 const state* kripke_current_dest_state; 96 }; 97 } 98