1 // -*- coding: utf-8 -*- 2 // Copyright (C) 2014-2015, 2018-2020 Laboratoire de Recherche et 3 // 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/misc/common.hh> 23 #include <spot/twa/fwd.hh> 24 #include <spot/twaalgos/powerset.hh> 25 #include <vector> 26 #include <utility> 27 28 namespace spot 29 { 30 /// \brief Automata constructed by product() contain a property 31 /// named "product-states" with this type 32 typedef std::vector<std::pair<unsigned, unsigned>> product_states; 33 34 /// \ingroup twa_algorithms 35 /// \brief Intersect two automata using a synchronous product 36 /// 37 /// The resulting automaton will accept the intersection of both 38 /// languages and have an acceptance condition that is the 39 /// conjunction of the acceptance conditions of the two input 40 /// automata. In case one of the left or right automaton is weak, 41 /// the acceptance condition of the result is made simpler: it 42 /// usually is the acceptance condition of the other argument, 43 /// therefore avoiding the need to introduce new accepting sets. 44 /// 45 /// The algorithm also defines a named property called 46 /// "product-states" with type spot::product_states. This stores 47 /// the pair of original state numbers associated to each state of 48 /// the product. 49 /// 50 /// If an \a aborter is given, the function will return nullptr 51 /// whenever the resulting product would be too large. 52 SPOT_API 53 twa_graph_ptr product(const const_twa_graph_ptr& left, 54 const const_twa_graph_ptr& right, 55 const output_aborter* aborter = nullptr); 56 57 /// \ingroup twa_algorithms 58 /// \brief Intersect two automata using a synchronous product 59 /// 60 /// This variant allows changing the initial state of both automata 61 /// in case you want to start the product at a different place. 62 /// 63 /// The resulting automaton will accept the intersection of the 64 /// languages recognized by each input automaton (with its initial 65 /// state changed) and have an acceptance condition that is the 66 /// conjunction of the acceptance conditions of the two input 67 /// automata. In case one of the left or right automaton is weak, 68 /// the acceptance condition of the result is made simpler: it 69 /// usually is the acceptance condition of the other argument, 70 /// therefore avoiding the need to introduce new accepting sets. 71 /// 72 /// The algorithm also defines a named property called 73 /// "product-states" with type spot::product_states. This stores 74 /// the pair of original state numbers associated to each state of 75 /// the product. 76 /// 77 /// If an \a aborter is given, the function will return nullptr 78 /// whenever the resulting product would be too large. 79 SPOT_API 80 twa_graph_ptr product(const const_twa_graph_ptr& left, 81 const const_twa_graph_ptr& right, 82 unsigned left_state, 83 unsigned right_state, 84 const output_aborter* aborter = nullptr); 85 86 /// \ingroup twa_algorithms 87 /// \brief Sum two automata using a synchronous product 88 /// 89 /// The resulting automaton will accept the union of both 90 /// languages and have an acceptance condition that is the 91 /// disjunction of the acceptance conditions of the two input 92 /// automata. In case one of the left or right automaton is weak, 93 /// the acceptance condition of the result is made simpler: it 94 /// usually is the acceptance condition of the other argument, 95 /// therefore avoiding the need to introduce new accepting sets. 96 /// 97 /// The algorithm also defines a named property called 98 /// "product-states" with type spot::product_states. This stores 99 /// the pair of original state numbers associated to each state of 100 /// the product. 101 SPOT_API 102 twa_graph_ptr product_or(const const_twa_graph_ptr& left, 103 const const_twa_graph_ptr& right); 104 105 /// \ingroup twa_algorithms 106 /// \brief Sum two automata using a synchronous product 107 /// 108 /// This variant allows changing the initial state of both automata 109 /// in case you want to start the product at a different place. 110 /// 111 /// The resulting automaton will accept the sum of the languages 112 /// recognized by each input automaton (with its initial state 113 /// changed) and have an acceptance condition that is the 114 /// disjunction of the acceptance conditions of the two input 115 /// automata. In case one of the left or right automaton is weak, 116 /// the acceptance condition of the result is made simpler: it 117 /// usually is the acceptance condition of the other argument, 118 /// therefore avoiding the need to introduce new accepting sets. 119 /// 120 /// The algorithm also defines a named property called 121 /// "product-states" with type spot::product_states. This stores 122 /// the pair of original state numbers associated to each state of 123 /// the product. 124 SPOT_API 125 twa_graph_ptr product_or(const const_twa_graph_ptr& left, 126 const const_twa_graph_ptr& right, 127 unsigned left_state, 128 unsigned right_state); 129 130 /// \ingroup twa_algorithms 131 /// \brief XOR two deterministic automata using a synchronous product 132 /// 133 /// The two operands must be deterministic. 134 /// 135 /// The resulting automaton will accept the symmetric difference of 136 /// both languages and have an acceptance condition that is the xor 137 /// of the acceptance conditions of the two input automata. In case 138 /// both operands are weak, the acceptance condition of the result 139 /// is made simpler. 140 /// 141 /// The algorithm also defines a named property called 142 /// "product-states" with type spot::product_states. This stores 143 /// the pair of original state numbers associated to each state of 144 /// the product. 145 SPOT_API 146 twa_graph_ptr product_xor(const const_twa_graph_ptr& left, 147 const const_twa_graph_ptr& right); 148 149 /// \ingroup twa_algorithms 150 /// \brief XNOR two automata using a synchronous product 151 /// 152 /// The two operands must be deterministic. 153 /// 154 /// The resulting automaton will accept words that are either in 155 /// both input languages, or not in both languages. (The XNOR gate 156 /// it the logical complement of XOR. XNOR is also known as logical 157 /// equivalence.) The output will have an acceptance condition that 158 /// is the XNOR of the acceptance conditions of the two input 159 /// automata. In case both the operands are weak, the acceptance 160 /// condition of the result is made simpler. 161 /// 162 /// The algorithm also defines a named property called 163 /// "product-states" with type spot::product_states. This stores 164 /// the pair of original state numbers associated to each state of 165 /// the product. 166 SPOT_API 167 twa_graph_ptr product_xnor(const const_twa_graph_ptr& left, 168 const const_twa_graph_ptr& right); 169 170 /// \ingroup twa_algorithms 171 /// \brief Build the product of an automaton with a suspendable 172 /// automaton. 173 /// 174 /// The language of this product is the intersection of the 175 /// languages of both input automata. 176 /// 177 /// This function *assumes* that \a right_susp is a suspendable 178 /// automaton, i.e., its language L satisfies L = Σ*.L. 179 /// Therefore the product between the two automata need only be done 180 /// with the accepting SCCs of left. 181 /// 182 /// If \a left is a weak automaton, the acceptance condition of the 183 /// output will be that of \a right_susp. Otherwise the acceptance 184 /// condition is the conjunction of both acceptances. 185 SPOT_API 186 twa_graph_ptr product_susp(const const_twa_graph_ptr& left, 187 const const_twa_graph_ptr& right_susp); 188 189 /// \ingroup twa_algorithms 190 /// \brief Build the "or" product of an automaton with a suspendable 191 /// automaton. 192 /// 193 /// The language of this product is the union of the languages of 194 /// both input automata. 195 /// 196 /// This function *assumes* that \a right_susp is a suspendable 197 /// automaton, i.e., its language L satisfies L = Σ*.L. 198 /// Therefore, after left has been completed (this will be done by 199 /// product_or_susp) the product between the two automata need only 200 /// be done with the SCCs of left that contains some rejecting cycles. 201 /// 202 /// The current implementation is currently suboptimal as instead of 203 /// looking for SCC with rejecting cycles, it simply loop for 204 /// non-trivial SCC, (or in the case of weak automata, with 205 /// non-trivial and rejecting SCCs). 206 SPOT_API 207 twa_graph_ptr product_or_susp(const const_twa_graph_ptr& left, 208 const const_twa_graph_ptr& right_susp); 209 } 210