Line data Source code
1 : // Author(s): Jan Friso Groote 2 : // Copyright: see the accompanying file COPYING or copy at 3 : // https://github.com/mCRL2org/mCRL2/blob/master/COPYING 4 : // 5 : // Distributed under the Boost Software License, Version 1.0. 6 : // (See accompanying file LICENSE_1_0.txt or copy at 7 : // http://www.boost.org/LICENSE_1_0.txt) 8 : // 9 : 10 : /** \file probabilistic_lts.h 11 : * 12 : * \brief The file containing the core class for transition systems. 13 : * \details This is the LTS library's main header file. It declares all publicly 14 : * accessible data structures that form the interface of the library. 15 : * \author Jan Friso Groote 16 : */ 17 : 18 : #ifndef MCRL2_LTS_PROBABILISTIC_STATE_H 19 : #define MCRL2_LTS_PROBABILISTIC_STATE_H 20 : 21 : #include <sstream> 22 : #include "mcrl2/utilities/exception.h" 23 : #include "mcrl2/lps/state_probability_pair.h" 24 : 25 : 26 : namespace mcrl2 27 : { 28 : 29 : namespace lts 30 : { 31 : 32 : /** \brief A class that contains a probabilistic state. 33 : \details A probabilistic state is essentially a sequence 34 : of pairs of a state and a probability. The probability 35 : indicates the likelyhood with which that particular 36 : state can be reached. The sum of all probabilities 37 : in a probabilistic state is one. 38 : Internally, it is either stored as single state, 39 : or as a vector of states. 40 : When using a probabilistic state, a user should 41 : be aware which of the two internal representations are used. 42 : After calling "construct_internal_vector_representation" 43 : it is guaranteed that the state is stored as a vector, 44 : and iterators over begin/end, and cbegin/cend can be used. 45 : */ 46 : 47 : template < class STATE, class PROBABILITY > 48 : class probabilistic_state 49 : { 50 : public: 51 : 52 : friend std::hash<probabilistic_state>; 53 : 54 : typedef typename lps::state_probability_pair< STATE, PROBABILITY > state_probability_pair; 55 : typedef STATE state_t; 56 : typedef PROBABILITY probability_t; 57 : typedef typename std::vector<state_probability_pair>::iterator iterator; 58 : typedef typename std::vector<state_probability_pair>::const_iterator const_iterator; 59 : typedef typename std::vector<state_probability_pair>::reverse_iterator reverse_iterator; 60 : typedef typename std::vector<state_probability_pair>::const_reverse_iterator const_reverse_iterator; 61 : 62 : protected: 63 : 64 : STATE m_single_state; // If there is only one state, this is stored as 65 : // a base state with implicit probability 1. 66 : std::vector<state_probability_pair> m_probabilistic_state; // A vector with states and their associated probability. 67 : // The sum of all probabilities in the vector must be one. 68 : 69 : public: 70 : 71 : /** \brief Default constructor 72 : **/ 73 2160 : probabilistic_state() 74 2160 : : m_single_state(STATE(-1)) 75 : { 76 2160 : } 77 : 78 : /** \brief Constructor of a probabilistic state from a non probabilistic state. 79 : * \param[in] s A state. 80 : * \return The generated probabilistic state. 81 : **/ 82 1337 : explicit probabilistic_state(const STATE& s) 83 1337 : : m_single_state(s) 84 : { 85 1337 : } 86 : 87 : /** \brief Copy constructor **/ 88 5550 : probabilistic_state(const probabilistic_state& other) 89 5550 : : m_single_state(other.m_single_state), 90 5550 : m_probabilistic_state(other.m_probabilistic_state) 91 : { 92 5550 : shrink_to_fit(); 93 5550 : } 94 : 95 : /** \brief Copy assignment constructor **/ 96 1104 : probabilistic_state& operator=(const probabilistic_state& other) 97 : { 98 1104 : m_single_state= other.m_single_state; 99 1104 : m_probabilistic_state = other.m_probabilistic_state; 100 1104 : shrink_to_fit(); 101 1104 : return *this; 102 : } 103 : 104 : /** \brief Creates a probabilistic state on the basis of state_probability_pairs. 105 : * \param[in] begin Iterator to the first state_probability_pair. 106 : * \param[in] end Iterator to the last state_probability_pair. 107 : * \return Resulting probabilistic state. **/ 108 : template <class STATE_PROBABILITY_PAIR_ITERATOR> 109 112 : probabilistic_state(const STATE_PROBABILITY_PAIR_ITERATOR begin, const STATE_PROBABILITY_PAIR_ITERATOR end) 110 112 : : m_single_state(STATE(-1)), 111 112 : m_probabilistic_state(begin,end) 112 : { 113 112 : assert(begin!=end); 114 112 : shrink_to_fit(); 115 112 : } 116 : 117 : /** \brief Standard equality operator. 118 : * \result Returns true iff the probabilistic states are equal. 119 : */ 120 500 : bool operator==(const probabilistic_state& other) const 121 : { 122 500 : if (m_single_state==STATE(-1)) 123 : { 124 468 : if (other.m_single_state==STATE(-1)) 125 : { 126 468 : assert(m_probabilistic_state.size()>0); 127 468 : assert(other.m_probabilistic_state.size()>0); 128 468 : return m_probabilistic_state==other.m_probabilistic_state; 129 : } 130 : else 131 : { 132 0 : return m_probabilistic_state.size()==1 && 133 0 : other.m_single_state==m_probabilistic_state.front().state(); 134 : } 135 : } 136 : else 137 : { 138 32 : if (other.m_single_state==STATE(-1)) 139 : { 140 4 : return other.m_probabilistic_state.size()==1 && 141 4 : m_single_state==other.m_probabilistic_state.front().state(); 142 : } 143 : else 144 : { 145 30 : assert(m_probabilistic_state.size()==0); 146 30 : assert(other.m_probabilistic_state.size()==0); 147 30 : return m_single_state==other.m_single_state; 148 : } 149 : } 150 : } 151 : 152 : /** \brief Standard equality operator. 153 : * \result Returns true iff the probabilistic states are equal. 154 : */ 155 : bool operator!=(const probabilistic_state& other) const 156 : { 157 : return !(operator==(other)); 158 : } 159 : 160 : /** \brief Swap this probabilistic state. 161 : * \param[in] s A probabilistic state. */ 162 129 : void swap(probabilistic_state& other) 163 : { 164 129 : std::swap(m_single_state,other.m_single_state); 165 129 : m_probabilistic_state.swap(other.m_probabilistic_state); 166 129 : } 167 : 168 : /** \brief Guarantee that this probabilistic state is internally stored as 169 : ** a vector, such that begin/end, cbegin/cend and size are properly 170 : ** defined. */ 171 : void construct_internal_vector_representation() 172 : { 173 : if (m_single_state!=STATE(-1)) 174 : { 175 : assert(m_probabilistic_state.size()==0); 176 : m_probabilistic_state.emplace_back(m_single_state,PROBABILITY::one()); 177 : m_single_state=STATE(-1); 178 : } 179 : } 180 : 181 : /** \brief Set this probabilistic state to a single state with probability one. 182 : * \details It is assumed that the given state probability pair does not have 183 : any element. 184 : * \param[in] s The state. */ 185 715 : void set(const STATE& s) 186 : { 187 715 : assert(m_probabilistic_state.size()==0); 188 715 : m_single_state=s; 189 715 : } 190 : 191 : /** \brief Get a probabilistic state if is is simple, i.e., consists of a single state. 192 : * \details It is assumed that the given state probability pair does not have 193 : any element. 194 : * \param[in] s The state. */ 195 3360 : STATE get() const 196 : { 197 3360 : if (m_probabilistic_state.size()>1) 198 : { 199 0 : throw mcrl2::runtime_error("Probabilistic state is not simple\n"); 200 : } 201 3360 : if (m_probabilistic_state.size()==1) 202 : { 203 0 : assert(m_probabilistic_state.front().state()!=STATE(-1)); 204 0 : return m_probabilistic_state.front().state(); 205 : } 206 3360 : assert(m_single_state!=STATE(-1)); 207 3360 : return m_single_state; 208 : } 209 : 210 : /** \brief Add a state with a probability to the probabilistic state 211 : * \param[in] s The state to be added. 212 : * \param[in] p The probability of this state. 213 : **/ 214 1709 : void add(const STATE& s, const PROBABILITY& p) 215 : { 216 1709 : m_probabilistic_state.emplace_back(s,p); 217 1709 : } 218 : 219 : /** \brief If a probabilistic state is ready, shrinking it to minimal size might be useful 220 : * to reduce its memory usage. A requirement is that the sum of the probabilities must 221 : * be one. 222 : */ 223 6822 : void shrink_to_fit() 224 : { 225 6822 : m_probabilistic_state.shrink_to_fit(); 226 6822 : assert((m_probabilistic_state.size()>1 && m_single_state==std::size_t(-1)) || 227 : (m_probabilistic_state.size()==0 && m_single_state!=std::size_t(-1))); 228 : #ifndef NDEBUG 229 6822 : PROBABILITY sum=PROBABILITY::zero(); 230 12872 : for(const state_probability_pair& p: m_probabilistic_state) 231 : { 232 6050 : assert(p.probability()>PROBABILITY::zero()); 233 6050 : assert(p.probability()<=PROBABILITY::one()); 234 6050 : sum=sum+p.probability(); 235 : } 236 : // SVC studio copies empty probabilistic states. 237 6822 : assert(m_probabilistic_state.size()==0 || sum==PROBABILITY::one()); 238 : #endif 239 6822 : } 240 : 241 : /** \brief Gets the number of probabilistic states in the vector representation of this state. 242 : ** If the state is stored as a simple number this size returns 0. So, 0 means that there 243 : ** is one state, which should then be obtained using get(). If the size is larger than 0 244 : ** the state is stored in a vector, and it must be accessed throught the iterators begin() 245 : ** and n. 246 : * \return The number of probabilistic states, where 0 means there is one simple state. */ 247 6693 : std::size_t size() const 248 : { 249 6693 : return m_probabilistic_state.size(); 250 : } 251 : 252 : /** \brief Makes the probabilistic state empty. 253 : */ 254 453 : void clear() 255 : { 256 453 : m_single_state=STATE(-1); 257 453 : m_probabilistic_state.clear(); 258 453 : } 259 : 260 : /** \brief Gets an iterator over pairs of state and probability. This can only be used when the state is stored 261 : ** internally as a vector. 262 : * \return The iterator pointing at the first state probability pair. */ 263 1388 : const_iterator begin() const 264 : { 265 1388 : return m_probabilistic_state.begin(); 266 : } 267 : 268 : /** \brief Gets the end iterator over pairs of state and probability. 269 : ** \return The iterator pointing beyond the last state probability pair in a probabilistic state. */ 270 1384 : const_iterator end() const 271 : { 272 1384 : return m_probabilistic_state.end(); 273 : } 274 : 275 : /** \brief Gets an iterator over pairs of state and probability. This can only be used if the state is internally stored as a vector. 276 : ** \return The iterator pointing at the first state probability pair. */ 277 992 : iterator begin() 278 : { 279 992 : return m_probabilistic_state.begin(); 280 : } 281 : 282 : /** \brief Gets the end iterator over pairs of state and probability. 283 : ** \return The iterator pointing beyond the last state probability pair in a probabilistic state. */ 284 992 : iterator end() 285 : { 286 992 : return m_probabilistic_state.end(); 287 : } 288 : 289 : /** \brief Gets a reverse iterator over pairs of state and probability. This can only be used when the state is stored 290 : ** internally as a vector. 291 : * \return The iterator pointing at the last state probability pair. */ 292 : const_reverse_iterator rbegin() const 293 : { 294 : return m_probabilistic_state.rbegin(); 295 : } 296 : 297 : /** \brief Gets the reverse end iterator over pairs of state and probability. 298 : ** \return The iterator pointing before the first state probability pair in a probabilistic state. */ 299 : const_reverse_iterator rend() const 300 : { 301 : return m_probabilistic_state.rend(); 302 : } 303 : 304 : /** \brief Gets a reverse iterator over pairs of state and probability. This can only be used if the state is internally stored as a vector. 305 : ** \return The iterator pointing at the last state probability pair. */ 306 : reverse_iterator rbegin() 307 : { 308 : return m_probabilistic_state.rbegin(); 309 : } 310 : 311 : /** \brief Gets the reverse end iterator over pairs of state and probability. 312 : ** \return The iterator pointing before the first state probability pair in a probabilistic state. */ 313 : reverse_iterator rend() 314 : { 315 : return m_probabilistic_state.rend(); 316 : } 317 : }; 318 : 319 : 320 : /* \brief A pretty print operator on action labels, returning it as a string. 321 : * */ 322 : template < class STATE, class PROBABILITY > 323 : inline std::string pp(const probabilistic_state<STATE, PROBABILITY>& l) 324 : { 325 : std::stringstream str; 326 : if (l.size()<=1) 327 : { 328 : str << "[ " << l.get() << ": 1.0 ]"; 329 : } 330 : else 331 : { 332 : str << "[ "; 333 : bool first=true; 334 : for(const lps::state_probability_pair<STATE, PROBABILITY>& p: l) 335 : { 336 : if (first) 337 : { 338 : first=false; 339 : } 340 : else 341 : { 342 : str << "; "; 343 : } 344 : str << p.state() << ": " << p.probability(); 345 : } 346 : str << " ]"; 347 : } 348 : 349 : return str.str(); 350 : } 351 : 352 : /** \brief Pretty print to an outstream. 353 : */ 354 : template < class STATE, class PROBABILITY > 355 : inline 356 : std::ostream& operator<<(std::ostream& out, const probabilistic_state<STATE, PROBABILITY>& l) 357 : { 358 : return out << pp(l); 359 : } 360 : 361 : 362 : 363 : } // namespace lts 364 : } // namespace mcrl2 365 : 366 : namespace std 367 : { 368 : 369 : /// \brief Specialization of the standard std::hash function. 370 : /// \details It is essential that this hash function yields the same has for a singular 371 : /// state in a distribution, stored as a number with implicit probability 1, or 372 : /// as a vector of length 1. 373 : template < class STATE, class PROBABILITY > 374 : struct hash< mcrl2::lts::probabilistic_state<STATE, PROBABILITY> > 375 : { 376 533 : std::size_t operator()(const mcrl2::lts::probabilistic_state<STATE, PROBABILITY>& p) const 377 : { 378 533 : if (p.m_single_state!=STATE(-1)) 379 : { 380 30 : assert(p.m_probabilistic_state.size()==0); 381 : hash<STATE> state_hasher; 382 : hash<PROBABILITY> probability_hasher; 383 36 : return mcrl2::utilities::detail::hash_combine(0, 384 30 : mcrl2::utilities::detail::hash_combine(state_hasher(p.m_single_state), 385 57 : probability_hasher(PROBABILITY::one()))); 386 : } 387 : hash<vector<typename mcrl2::lps::state_probability_pair< STATE, PROBABILITY > > > hasher; 388 503 : return hasher(p.m_probabilistic_state); 389 : } 390 : }; 391 : 392 : } // namespace std 393 : 394 : #endif // MCRL2_LTS_PROBABILISTIC_STATE_H