Line data Source code
1 : // Author(s): Wieger Wesselink 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 : /// \file mcrl2/pbes/traverser.h 10 : /// \brief add your file description here. 11 : 12 : #ifndef MCRL2_PBES_TRAVERSER_H 13 : #define MCRL2_PBES_TRAVERSER_H 14 : 15 : #include "mcrl2/pbes/pbes.h" 16 : 17 : namespace mcrl2 18 : { 19 : 20 : namespace pbes_system 21 : { 22 : 23 : /// \brief Traversal class for pbes_expressions. Used as a base class for pbes_expression_traverser. 24 : template <typename Derived> 25 : struct pbes_expression_traverser_base: public core::traverser<Derived> 26 : { 27 : typedef core::traverser<Derived> super; 28 : using super::apply; 29 : using super::enter; 30 : using super::leave; 31 : 32 : void apply(pbes_expression& result, const data::data_expression& x) 33 : { 34 : static_cast<Derived&>(*this).enter(x); 35 : // skip 36 : static_cast<Derived&>(*this).leave(x); 37 : result=x; 38 : } 39 : }; 40 : 41 : //--- start generated add_traverser_sort_expressions code ---// 42 : template <template <class> class Traverser, class Derived> 43 : struct add_traverser_sort_expressions: public Traverser<Derived> 44 : { 45 : typedef Traverser<Derived> super; 46 : using super::enter; 47 : using super::leave; 48 : using super::apply; 49 : 50 3075 : void apply(const pbes_system::propositional_variable& x) 51 : { 52 3075 : static_cast<Derived&>(*this).enter(x); 53 3075 : static_cast<Derived&>(*this).apply(x.parameters()); 54 3075 : static_cast<Derived&>(*this).leave(x); 55 3075 : } 56 : 57 3075 : void apply(const pbes_system::pbes_equation& x) 58 : { 59 3075 : static_cast<Derived&>(*this).enter(x); 60 3075 : static_cast<Derived&>(*this).apply(x.variable()); 61 3075 : static_cast<Derived&>(*this).apply(x.formula()); 62 3075 : static_cast<Derived&>(*this).leave(x); 63 3075 : } 64 : 65 621 : void apply(const pbes_system::pbes& x) 66 : { 67 621 : static_cast<Derived&>(*this).enter(x); 68 621 : static_cast<Derived&>(*this).apply(x.global_variables()); 69 621 : static_cast<Derived&>(*this).apply(x.equations()); 70 621 : static_cast<Derived&>(*this).apply(x.initial_state()); 71 621 : static_cast<Derived&>(*this).leave(x); 72 621 : } 73 : 74 1801 : void apply(const pbes_system::propositional_variable_instantiation& x) 75 : { 76 1801 : static_cast<Derived&>(*this).enter(x); 77 1801 : static_cast<Derived&>(*this).apply(x.parameters()); 78 1801 : static_cast<Derived&>(*this).leave(x); 79 1801 : } 80 : 81 143 : void apply(const pbes_system::not_& x) 82 : { 83 143 : static_cast<Derived&>(*this).enter(x); 84 143 : static_cast<Derived&>(*this).apply(x.operand()); 85 143 : static_cast<Derived&>(*this).leave(x); 86 143 : } 87 : 88 772 : void apply(const pbes_system::and_& x) 89 : { 90 772 : static_cast<Derived&>(*this).enter(x); 91 772 : static_cast<Derived&>(*this).apply(x.left()); 92 772 : static_cast<Derived&>(*this).apply(x.right()); 93 772 : static_cast<Derived&>(*this).leave(x); 94 772 : } 95 : 96 792 : void apply(const pbes_system::or_& x) 97 : { 98 792 : static_cast<Derived&>(*this).enter(x); 99 792 : static_cast<Derived&>(*this).apply(x.left()); 100 792 : static_cast<Derived&>(*this).apply(x.right()); 101 792 : static_cast<Derived&>(*this).leave(x); 102 792 : } 103 : 104 176 : void apply(const pbes_system::imp& x) 105 : { 106 176 : static_cast<Derived&>(*this).enter(x); 107 176 : static_cast<Derived&>(*this).apply(x.left()); 108 176 : static_cast<Derived&>(*this).apply(x.right()); 109 176 : static_cast<Derived&>(*this).leave(x); 110 176 : } 111 : 112 353 : void apply(const pbes_system::forall& x) 113 : { 114 353 : static_cast<Derived&>(*this).enter(x); 115 353 : static_cast<Derived&>(*this).apply(x.variables()); 116 353 : static_cast<Derived&>(*this).apply(x.body()); 117 353 : static_cast<Derived&>(*this).leave(x); 118 353 : } 119 : 120 190 : void apply(const pbes_system::exists& x) 121 : { 122 190 : static_cast<Derived&>(*this).enter(x); 123 190 : static_cast<Derived&>(*this).apply(x.variables()); 124 190 : static_cast<Derived&>(*this).apply(x.body()); 125 190 : static_cast<Derived&>(*this).leave(x); 126 190 : } 127 : 128 30058 : void apply(const pbes_system::pbes_expression& x) 129 : { 130 30058 : static_cast<Derived&>(*this).enter(x); 131 30058 : if (data::is_data_expression(x)) 132 : { 133 8733 : static_cast<Derived&>(*this).apply(atermpp::down_cast<data::data_expression>(x)); 134 : } 135 21325 : else if (data::is_variable(x)) 136 : { 137 0 : static_cast<Derived&>(*this).apply(atermpp::down_cast<data::variable>(x)); 138 : } 139 21325 : else if (data::is_untyped_data_parameter(x)) 140 : { 141 0 : static_cast<Derived&>(*this).apply(atermpp::down_cast<data::untyped_data_parameter>(x)); 142 : } 143 21325 : else if (pbes_system::is_propositional_variable_instantiation(x)) 144 : { 145 10796 : static_cast<Derived&>(*this).apply(atermpp::down_cast<pbes_system::propositional_variable_instantiation>(x)); 146 : } 147 10529 : else if (pbes_system::is_not(x)) 148 : { 149 165 : static_cast<Derived&>(*this).apply(atermpp::down_cast<pbes_system::not_>(x)); 150 : } 151 10364 : else if (pbes_system::is_and(x)) 152 : { 153 3996 : static_cast<Derived&>(*this).apply(atermpp::down_cast<pbes_system::and_>(x)); 154 : } 155 6368 : else if (pbes_system::is_or(x)) 156 : { 157 5320 : static_cast<Derived&>(*this).apply(atermpp::down_cast<pbes_system::or_>(x)); 158 : } 159 1048 : else if (pbes_system::is_imp(x)) 160 : { 161 194 : static_cast<Derived&>(*this).apply(atermpp::down_cast<pbes_system::imp>(x)); 162 : } 163 854 : else if (pbes_system::is_forall(x)) 164 : { 165 567 : static_cast<Derived&>(*this).apply(atermpp::down_cast<pbes_system::forall>(x)); 166 : } 167 287 : else if (pbes_system::is_exists(x)) 168 : { 169 287 : static_cast<Derived&>(*this).apply(atermpp::down_cast<pbes_system::exists>(x)); 170 : } 171 30058 : static_cast<Derived&>(*this).leave(x); 172 30058 : } 173 : 174 : }; 175 : 176 : /// \\brief Traverser class 177 : template <typename Derived> 178 : struct sort_expression_traverser: public add_traverser_sort_expressions<data::sort_expression_traverser, Derived> 179 : { 180 : }; 181 : //--- end generated add_traverser_sort_expressions code ---// 182 : 183 : //--- start generated add_traverser_data_expressions code ---// 184 : template <template <class> class Traverser, class Derived> 185 : struct add_traverser_data_expressions: public Traverser<Derived> 186 : { 187 : typedef Traverser<Derived> super; 188 : using super::enter; 189 : using super::leave; 190 : using super::apply; 191 : 192 1479 : void apply(const pbes_system::pbes_equation& x) 193 : { 194 1479 : static_cast<Derived&>(*this).enter(x); 195 1479 : static_cast<Derived&>(*this).apply(x.formula()); 196 1479 : static_cast<Derived&>(*this).leave(x); 197 1479 : } 198 : 199 364 : void apply(const pbes_system::pbes& x) 200 : { 201 364 : static_cast<Derived&>(*this).enter(x); 202 364 : static_cast<Derived&>(*this).apply(x.equations()); 203 364 : static_cast<Derived&>(*this).apply(x.initial_state()); 204 364 : static_cast<Derived&>(*this).leave(x); 205 364 : } 206 : 207 6120 : void apply(const pbes_system::propositional_variable_instantiation& x) 208 : { 209 6120 : static_cast<Derived&>(*this).enter(x); 210 6120 : static_cast<Derived&>(*this).apply(x.parameters()); 211 6120 : static_cast<Derived&>(*this).leave(x); 212 6120 : } 213 : 214 67 : void apply(const pbes_system::not_& x) 215 : { 216 67 : static_cast<Derived&>(*this).enter(x); 217 67 : static_cast<Derived&>(*this).apply(x.operand()); 218 67 : static_cast<Derived&>(*this).leave(x); 219 67 : } 220 : 221 4544 : void apply(const pbes_system::and_& x) 222 : { 223 4544 : static_cast<Derived&>(*this).enter(x); 224 4544 : static_cast<Derived&>(*this).apply(x.left()); 225 4544 : static_cast<Derived&>(*this).apply(x.right()); 226 4544 : static_cast<Derived&>(*this).leave(x); 227 4544 : } 228 : 229 2487 : void apply(const pbes_system::or_& x) 230 : { 231 2487 : static_cast<Derived&>(*this).enter(x); 232 2487 : static_cast<Derived&>(*this).apply(x.left()); 233 2487 : static_cast<Derived&>(*this).apply(x.right()); 234 2487 : static_cast<Derived&>(*this).leave(x); 235 2487 : } 236 : 237 1097 : void apply(const pbes_system::imp& x) 238 : { 239 1097 : static_cast<Derived&>(*this).enter(x); 240 1097 : static_cast<Derived&>(*this).apply(x.left()); 241 1097 : static_cast<Derived&>(*this).apply(x.right()); 242 1097 : static_cast<Derived&>(*this).leave(x); 243 1097 : } 244 : 245 429 : void apply(const pbes_system::forall& x) 246 : { 247 429 : static_cast<Derived&>(*this).enter(x); 248 429 : static_cast<Derived&>(*this).apply(x.body()); 249 429 : static_cast<Derived&>(*this).leave(x); 250 429 : } 251 : 252 888 : void apply(const pbes_system::exists& x) 253 : { 254 888 : static_cast<Derived&>(*this).enter(x); 255 888 : static_cast<Derived&>(*this).apply(x.body()); 256 888 : static_cast<Derived&>(*this).leave(x); 257 888 : } 258 : 259 23196 : void apply(const pbes_system::pbes_expression& x) 260 : { 261 23196 : static_cast<Derived&>(*this).enter(x); 262 23196 : if (data::is_data_expression(x)) 263 : { 264 7784 : static_cast<Derived&>(*this).apply(atermpp::down_cast<data::data_expression>(x)); 265 : } 266 15412 : else if (data::is_variable(x)) 267 : { 268 0 : static_cast<Derived&>(*this).apply(atermpp::down_cast<data::variable>(x)); 269 : } 270 15412 : else if (data::is_untyped_data_parameter(x)) 271 : { 272 0 : static_cast<Derived&>(*this).apply(atermpp::down_cast<data::untyped_data_parameter>(x)); 273 : } 274 15412 : else if (pbes_system::is_propositional_variable_instantiation(x)) 275 : { 276 5900 : static_cast<Derived&>(*this).apply(atermpp::down_cast<pbes_system::propositional_variable_instantiation>(x)); 277 : } 278 9512 : else if (pbes_system::is_not(x)) 279 : { 280 67 : static_cast<Derived&>(*this).apply(atermpp::down_cast<pbes_system::not_>(x)); 281 : } 282 9445 : else if (pbes_system::is_and(x)) 283 : { 284 4544 : static_cast<Derived&>(*this).apply(atermpp::down_cast<pbes_system::and_>(x)); 285 : } 286 4901 : else if (pbes_system::is_or(x)) 287 : { 288 2487 : static_cast<Derived&>(*this).apply(atermpp::down_cast<pbes_system::or_>(x)); 289 : } 290 2414 : else if (pbes_system::is_imp(x)) 291 : { 292 1097 : static_cast<Derived&>(*this).apply(atermpp::down_cast<pbes_system::imp>(x)); 293 : } 294 1317 : else if (pbes_system::is_forall(x)) 295 : { 296 429 : static_cast<Derived&>(*this).apply(atermpp::down_cast<pbes_system::forall>(x)); 297 : } 298 888 : else if (pbes_system::is_exists(x)) 299 : { 300 888 : static_cast<Derived&>(*this).apply(atermpp::down_cast<pbes_system::exists>(x)); 301 : } 302 23196 : static_cast<Derived&>(*this).leave(x); 303 23196 : } 304 : 305 : }; 306 : 307 : /// \\brief Traverser class 308 : template <typename Derived> 309 : struct data_expression_traverser: public add_traverser_data_expressions<data::data_expression_traverser, Derived> 310 : { 311 : }; 312 : //--- end generated add_traverser_data_expressions code ---// 313 : 314 : //--- start generated add_traverser_pbes_expressions code ---// 315 : template <template <class> class Traverser, class Derived> 316 : struct add_traverser_pbes_expressions: public Traverser<Derived> 317 : { 318 : typedef Traverser<Derived> super; 319 : using super::enter; 320 : using super::leave; 321 : using super::apply; 322 : 323 336 : void apply(const pbes_system::pbes_equation& x) 324 : { 325 336 : static_cast<Derived&>(*this).enter(x); 326 336 : static_cast<Derived&>(*this).apply(x.formula()); 327 336 : static_cast<Derived&>(*this).leave(x); 328 336 : } 329 : 330 172 : void apply(const pbes_system::pbes& x) 331 : { 332 172 : static_cast<Derived&>(*this).enter(x); 333 172 : static_cast<Derived&>(*this).apply(x.equations()); 334 172 : static_cast<Derived&>(*this).leave(x); 335 172 : } 336 : 337 4642 : void apply(const pbes_system::propositional_variable_instantiation& x) 338 : { 339 4642 : static_cast<Derived&>(*this).enter(x); 340 : // skip 341 4642 : static_cast<Derived&>(*this).leave(x); 342 4642 : } 343 : 344 385 : void apply(const pbes_system::not_& x) 345 : { 346 385 : static_cast<Derived&>(*this).enter(x); 347 385 : static_cast<Derived&>(*this).apply(x.operand()); 348 385 : static_cast<Derived&>(*this).leave(x); 349 385 : } 350 : 351 10328 : void apply(const pbes_system::and_& x) 352 : { 353 10328 : static_cast<Derived&>(*this).enter(x); 354 10328 : static_cast<Derived&>(*this).apply(x.left()); 355 10328 : static_cast<Derived&>(*this).apply(x.right()); 356 10328 : static_cast<Derived&>(*this).leave(x); 357 10328 : } 358 : 359 5781 : void apply(const pbes_system::or_& x) 360 : { 361 5781 : static_cast<Derived&>(*this).enter(x); 362 5781 : static_cast<Derived&>(*this).apply(x.left()); 363 5781 : static_cast<Derived&>(*this).apply(x.right()); 364 5781 : static_cast<Derived&>(*this).leave(x); 365 5781 : } 366 : 367 2104 : void apply(const pbes_system::imp& x) 368 : { 369 2104 : static_cast<Derived&>(*this).enter(x); 370 2104 : static_cast<Derived&>(*this).apply(x.left()); 371 2104 : static_cast<Derived&>(*this).apply(x.right()); 372 2104 : static_cast<Derived&>(*this).leave(x); 373 2104 : } 374 : 375 1097 : void apply(const pbes_system::forall& x) 376 : { 377 1097 : static_cast<Derived&>(*this).enter(x); 378 1097 : static_cast<Derived&>(*this).apply(x.body()); 379 1097 : static_cast<Derived&>(*this).leave(x); 380 1097 : } 381 : 382 1535 : void apply(const pbes_system::exists& x) 383 : { 384 1535 : static_cast<Derived&>(*this).enter(x); 385 1535 : static_cast<Derived&>(*this).apply(x.body()); 386 1535 : static_cast<Derived&>(*this).leave(x); 387 1535 : } 388 : 389 47134 : void apply(const pbes_system::pbes_expression& x) 390 : { 391 47134 : static_cast<Derived&>(*this).enter(x); 392 47134 : if (data::is_data_expression(x)) 393 : { 394 11340 : static_cast<Derived&>(*this).apply(atermpp::down_cast<data::data_expression>(x)); 395 : } 396 35794 : else if (data::is_variable(x)) 397 : { 398 0 : static_cast<Derived&>(*this).apply(atermpp::down_cast<data::variable>(x)); 399 : } 400 35794 : else if (data::is_untyped_data_parameter(x)) 401 : { 402 0 : static_cast<Derived&>(*this).apply(atermpp::down_cast<data::untyped_data_parameter>(x)); 403 : } 404 35794 : else if (pbes_system::is_propositional_variable_instantiation(x)) 405 : { 406 14728 : static_cast<Derived&>(*this).apply(atermpp::down_cast<pbes_system::propositional_variable_instantiation>(x)); 407 : } 408 21066 : else if (pbes_system::is_not(x)) 409 : { 410 385 : static_cast<Derived&>(*this).apply(atermpp::down_cast<pbes_system::not_>(x)); 411 : } 412 20681 : else if (pbes_system::is_and(x)) 413 : { 414 10260 : static_cast<Derived&>(*this).apply(atermpp::down_cast<pbes_system::and_>(x)); 415 : } 416 10421 : else if (pbes_system::is_or(x)) 417 : { 418 5681 : static_cast<Derived&>(*this).apply(atermpp::down_cast<pbes_system::or_>(x)); 419 : } 420 4740 : else if (pbes_system::is_imp(x)) 421 : { 422 2104 : static_cast<Derived&>(*this).apply(atermpp::down_cast<pbes_system::imp>(x)); 423 : } 424 2636 : else if (pbes_system::is_forall(x)) 425 : { 426 1097 : static_cast<Derived&>(*this).apply(atermpp::down_cast<pbes_system::forall>(x)); 427 : } 428 1539 : else if (pbes_system::is_exists(x)) 429 : { 430 1539 : static_cast<Derived&>(*this).apply(atermpp::down_cast<pbes_system::exists>(x)); 431 : } 432 47134 : static_cast<Derived&>(*this).leave(x); 433 47134 : } 434 : 435 : }; 436 : 437 : /// \\brief Traverser class 438 : template <typename Derived> 439 : struct pbes_expression_traverser: public add_traverser_pbes_expressions<pbes_system::pbes_expression_traverser_base, Derived> 440 : { 441 : }; 442 : //--- end generated add_traverser_pbes_expressions code ---// 443 : 444 : //--- start generated add_traverser_variables code ---// 445 : template <template <class> class Traverser, class Derived> 446 : struct add_traverser_variables: public Traverser<Derived> 447 : { 448 : typedef Traverser<Derived> super; 449 : using super::enter; 450 : using super::leave; 451 : using super::apply; 452 : 453 1 : void apply(const pbes_system::propositional_variable& x) 454 : { 455 1 : static_cast<Derived&>(*this).enter(x); 456 1 : static_cast<Derived&>(*this).apply(x.parameters()); 457 1 : static_cast<Derived&>(*this).leave(x); 458 1 : } 459 : 460 1 : void apply(const pbes_system::pbes_equation& x) 461 : { 462 1 : static_cast<Derived&>(*this).enter(x); 463 1 : static_cast<Derived&>(*this).apply(x.variable()); 464 1 : static_cast<Derived&>(*this).apply(x.formula()); 465 1 : static_cast<Derived&>(*this).leave(x); 466 1 : } 467 : 468 1 : void apply(const pbes_system::pbes& x) 469 : { 470 1 : static_cast<Derived&>(*this).enter(x); 471 1 : static_cast<Derived&>(*this).apply(x.global_variables()); 472 1 : static_cast<Derived&>(*this).apply(x.equations()); 473 1 : static_cast<Derived&>(*this).apply(x.initial_state()); 474 1 : static_cast<Derived&>(*this).leave(x); 475 1 : } 476 : 477 4 : void apply(const pbes_system::propositional_variable_instantiation& x) 478 : { 479 4 : static_cast<Derived&>(*this).enter(x); 480 4 : static_cast<Derived&>(*this).apply(x.parameters()); 481 4 : static_cast<Derived&>(*this).leave(x); 482 4 : } 483 : 484 0 : void apply(const pbes_system::not_& x) 485 : { 486 0 : static_cast<Derived&>(*this).enter(x); 487 0 : static_cast<Derived&>(*this).apply(x.operand()); 488 0 : static_cast<Derived&>(*this).leave(x); 489 0 : } 490 : 491 2 : void apply(const pbes_system::and_& x) 492 : { 493 2 : static_cast<Derived&>(*this).enter(x); 494 2 : static_cast<Derived&>(*this).apply(x.left()); 495 2 : static_cast<Derived&>(*this).apply(x.right()); 496 2 : static_cast<Derived&>(*this).leave(x); 497 2 : } 498 : 499 0 : void apply(const pbes_system::or_& x) 500 : { 501 0 : static_cast<Derived&>(*this).enter(x); 502 0 : static_cast<Derived&>(*this).apply(x.left()); 503 0 : static_cast<Derived&>(*this).apply(x.right()); 504 0 : static_cast<Derived&>(*this).leave(x); 505 0 : } 506 : 507 0 : void apply(const pbes_system::imp& x) 508 : { 509 0 : static_cast<Derived&>(*this).enter(x); 510 0 : static_cast<Derived&>(*this).apply(x.left()); 511 0 : static_cast<Derived&>(*this).apply(x.right()); 512 0 : static_cast<Derived&>(*this).leave(x); 513 0 : } 514 : 515 0 : void apply(const pbes_system::forall& x) 516 : { 517 0 : static_cast<Derived&>(*this).enter(x); 518 0 : static_cast<Derived&>(*this).apply(x.variables()); 519 0 : static_cast<Derived&>(*this).apply(x.body()); 520 0 : static_cast<Derived&>(*this).leave(x); 521 0 : } 522 : 523 1 : void apply(const pbes_system::exists& x) 524 : { 525 1 : static_cast<Derived&>(*this).enter(x); 526 1 : static_cast<Derived&>(*this).apply(x.variables()); 527 1 : static_cast<Derived&>(*this).apply(x.body()); 528 1 : static_cast<Derived&>(*this).leave(x); 529 1 : } 530 : 531 7 : void apply(const pbes_system::pbes_expression& x) 532 : { 533 7 : static_cast<Derived&>(*this).enter(x); 534 7 : if (data::is_data_expression(x)) 535 : { 536 1 : static_cast<Derived&>(*this).apply(atermpp::down_cast<data::data_expression>(x)); 537 : } 538 6 : else if (data::is_variable(x)) 539 : { 540 0 : static_cast<Derived&>(*this).apply(atermpp::down_cast<data::variable>(x)); 541 : } 542 6 : else if (data::is_untyped_data_parameter(x)) 543 : { 544 0 : static_cast<Derived&>(*this).apply(atermpp::down_cast<data::untyped_data_parameter>(x)); 545 : } 546 6 : else if (pbes_system::is_propositional_variable_instantiation(x)) 547 : { 548 3 : static_cast<Derived&>(*this).apply(atermpp::down_cast<pbes_system::propositional_variable_instantiation>(x)); 549 : } 550 3 : else if (pbes_system::is_not(x)) 551 : { 552 0 : static_cast<Derived&>(*this).apply(atermpp::down_cast<pbes_system::not_>(x)); 553 : } 554 3 : else if (pbes_system::is_and(x)) 555 : { 556 2 : static_cast<Derived&>(*this).apply(atermpp::down_cast<pbes_system::and_>(x)); 557 : } 558 1 : else if (pbes_system::is_or(x)) 559 : { 560 0 : static_cast<Derived&>(*this).apply(atermpp::down_cast<pbes_system::or_>(x)); 561 : } 562 1 : else if (pbes_system::is_imp(x)) 563 : { 564 0 : static_cast<Derived&>(*this).apply(atermpp::down_cast<pbes_system::imp>(x)); 565 : } 566 1 : else if (pbes_system::is_forall(x)) 567 : { 568 0 : static_cast<Derived&>(*this).apply(atermpp::down_cast<pbes_system::forall>(x)); 569 : } 570 1 : else if (pbes_system::is_exists(x)) 571 : { 572 1 : static_cast<Derived&>(*this).apply(atermpp::down_cast<pbes_system::exists>(x)); 573 : } 574 7 : static_cast<Derived&>(*this).leave(x); 575 7 : } 576 : 577 : }; 578 : 579 : /// \\brief Traverser class 580 : template <typename Derived> 581 : struct variable_traverser: public add_traverser_variables<data::variable_traverser, Derived> 582 : { 583 : }; 584 : //--- end generated add_traverser_variables code ---// 585 : 586 : //--- start generated add_traverser_identifier_strings code ---// 587 : template <template <class> class Traverser, class Derived> 588 : struct add_traverser_identifier_strings: public Traverser<Derived> 589 : { 590 : typedef Traverser<Derived> super; 591 : using super::enter; 592 : using super::leave; 593 : using super::apply; 594 : 595 0 : void apply(const pbes_system::propositional_variable& x) 596 : { 597 0 : static_cast<Derived&>(*this).enter(x); 598 0 : static_cast<Derived&>(*this).apply(x.name()); 599 0 : static_cast<Derived&>(*this).apply(x.parameters()); 600 0 : static_cast<Derived&>(*this).leave(x); 601 0 : } 602 : 603 0 : void apply(const pbes_system::pbes_equation& x) 604 : { 605 0 : static_cast<Derived&>(*this).enter(x); 606 0 : static_cast<Derived&>(*this).apply(x.variable()); 607 0 : static_cast<Derived&>(*this).apply(x.formula()); 608 0 : static_cast<Derived&>(*this).leave(x); 609 0 : } 610 : 611 0 : void apply(const pbes_system::pbes& x) 612 : { 613 0 : static_cast<Derived&>(*this).enter(x); 614 0 : static_cast<Derived&>(*this).apply(x.global_variables()); 615 0 : static_cast<Derived&>(*this).apply(x.equations()); 616 0 : static_cast<Derived&>(*this).apply(x.initial_state()); 617 0 : static_cast<Derived&>(*this).leave(x); 618 0 : } 619 : 620 487 : void apply(const pbes_system::propositional_variable_instantiation& x) 621 : { 622 487 : static_cast<Derived&>(*this).enter(x); 623 487 : static_cast<Derived&>(*this).apply(x.name()); 624 487 : static_cast<Derived&>(*this).apply(x.parameters()); 625 487 : static_cast<Derived&>(*this).leave(x); 626 487 : } 627 : 628 50 : void apply(const pbes_system::not_& x) 629 : { 630 50 : static_cast<Derived&>(*this).enter(x); 631 50 : static_cast<Derived&>(*this).apply(x.operand()); 632 50 : static_cast<Derived&>(*this).leave(x); 633 50 : } 634 : 635 139 : void apply(const pbes_system::and_& x) 636 : { 637 139 : static_cast<Derived&>(*this).enter(x); 638 139 : static_cast<Derived&>(*this).apply(x.left()); 639 139 : static_cast<Derived&>(*this).apply(x.right()); 640 139 : static_cast<Derived&>(*this).leave(x); 641 139 : } 642 : 643 61 : void apply(const pbes_system::or_& x) 644 : { 645 61 : static_cast<Derived&>(*this).enter(x); 646 61 : static_cast<Derived&>(*this).apply(x.left()); 647 61 : static_cast<Derived&>(*this).apply(x.right()); 648 61 : static_cast<Derived&>(*this).leave(x); 649 61 : } 650 : 651 3 : void apply(const pbes_system::imp& x) 652 : { 653 3 : static_cast<Derived&>(*this).enter(x); 654 3 : static_cast<Derived&>(*this).apply(x.left()); 655 3 : static_cast<Derived&>(*this).apply(x.right()); 656 3 : static_cast<Derived&>(*this).leave(x); 657 3 : } 658 : 659 30 : void apply(const pbes_system::forall& x) 660 : { 661 30 : static_cast<Derived&>(*this).enter(x); 662 30 : static_cast<Derived&>(*this).apply(x.variables()); 663 30 : static_cast<Derived&>(*this).apply(x.body()); 664 30 : static_cast<Derived&>(*this).leave(x); 665 30 : } 666 : 667 28 : void apply(const pbes_system::exists& x) 668 : { 669 28 : static_cast<Derived&>(*this).enter(x); 670 28 : static_cast<Derived&>(*this).apply(x.variables()); 671 28 : static_cast<Derived&>(*this).apply(x.body()); 672 28 : static_cast<Derived&>(*this).leave(x); 673 28 : } 674 : 675 1439 : void apply(const pbes_system::pbes_expression& x) 676 : { 677 1439 : static_cast<Derived&>(*this).enter(x); 678 1439 : if (data::is_data_expression(x)) 679 : { 680 641 : static_cast<Derived&>(*this).apply(atermpp::down_cast<data::data_expression>(x)); 681 : } 682 798 : else if (data::is_variable(x)) 683 : { 684 0 : static_cast<Derived&>(*this).apply(atermpp::down_cast<data::variable>(x)); 685 : } 686 798 : else if (data::is_untyped_data_parameter(x)) 687 : { 688 0 : static_cast<Derived&>(*this).apply(atermpp::down_cast<data::untyped_data_parameter>(x)); 689 : } 690 798 : else if (pbes_system::is_propositional_variable_instantiation(x)) 691 : { 692 487 : static_cast<Derived&>(*this).apply(atermpp::down_cast<pbes_system::propositional_variable_instantiation>(x)); 693 : } 694 311 : else if (pbes_system::is_not(x)) 695 : { 696 50 : static_cast<Derived&>(*this).apply(atermpp::down_cast<pbes_system::not_>(x)); 697 : } 698 261 : else if (pbes_system::is_and(x)) 699 : { 700 139 : static_cast<Derived&>(*this).apply(atermpp::down_cast<pbes_system::and_>(x)); 701 : } 702 122 : else if (pbes_system::is_or(x)) 703 : { 704 61 : static_cast<Derived&>(*this).apply(atermpp::down_cast<pbes_system::or_>(x)); 705 : } 706 61 : else if (pbes_system::is_imp(x)) 707 : { 708 3 : static_cast<Derived&>(*this).apply(atermpp::down_cast<pbes_system::imp>(x)); 709 : } 710 58 : else if (pbes_system::is_forall(x)) 711 : { 712 30 : static_cast<Derived&>(*this).apply(atermpp::down_cast<pbes_system::forall>(x)); 713 : } 714 28 : else if (pbes_system::is_exists(x)) 715 : { 716 28 : static_cast<Derived&>(*this).apply(atermpp::down_cast<pbes_system::exists>(x)); 717 : } 718 1439 : static_cast<Derived&>(*this).leave(x); 719 1439 : } 720 : 721 : }; 722 : 723 : /// \\brief Traverser class 724 : template <typename Derived> 725 : struct identifier_string_traverser: public add_traverser_identifier_strings<data::identifier_string_traverser, Derived> 726 : { 727 : }; 728 : //--- end generated add_traverser_identifier_strings code ---// 729 : 730 : } // namespace pbes_system 731 : 732 : } // namespace mcrl2 733 : 734 : #endif // MCRL2_PBES_TRAVERSER_H