User: | Jiri Slaby |
Error type: | Reachable Error Location |
Error type description: | A specified error location is reachable in some program path |
File location: | systemc/token_ring.13.cil.c |
Line in file: | 8 |
Project: | SV-COMP 2012 |
Tools: |
Manual Work
|
Entered: | 2012-11-19 13:47:39 UTC |
1/* Generated by CIL v. 1.3.6 */ 2/* print_CIL_Input is true */ 3 4void error(void) 5{ 6 7 { 8 ERROR: ; 9 goto ERROR; 10 return; 11} 12} 13int m_pc = 0; 14int t1_pc = 0; 15int t2_pc = 0; 16int t3_pc = 0; 17int t4_pc = 0; 18int t5_pc = 0; 19int t6_pc = 0; 20int t7_pc = 0; 21int t8_pc = 0; 22int t9_pc = 0; 23int t10_pc = 0; 24int t11_pc = 0; 25int t12_pc = 0; 26int t13_pc = 0; 27int m_st ; 28int t1_st ; 29int t2_st ; 30int t3_st ; 31int t4_st ; 32int t5_st ; 33int t6_st ; 34int t7_st ; 35int t8_st ; 36int t9_st ; 37int t10_st ; 38int t11_st ; 39int t12_st ; 40int t13_st ; 41int m_i ; 42int t1_i ; 43int t2_i ; 44int t3_i ; 45int t4_i ; 46int t5_i ; 47int t6_i ; 48int t7_i ; 49int t8_i ; 50int t9_i ; 51int t10_i ; 52int t11_i ; 53int t12_i ; 54int t13_i ; 55int M_E = 2; 56int T1_E = 2; 57int T2_E = 2; 58int T3_E = 2; 59int T4_E = 2; 60int T5_E = 2; 61int T6_E = 2; 62int T7_E = 2; 63int T8_E = 2; 64int T9_E = 2; 65int T10_E = 2; 66int T11_E = 2; 67int T12_E = 2; 68int T13_E = 2; 69int E_M = 2; 70int E_1 = 2; 71int E_2 = 2; 72int E_3 = 2; 73int E_4 = 2; 74int E_5 = 2; 75int E_6 = 2; 76int E_7 = 2; 77int E_8 = 2; 78int E_9 = 2; 79int E_10 = 2; 80int E_11 = 2; 81int E_12 = 2; 82int E_13 = 2; 83int is_master_triggered(void) ; 84int is_transmit1_triggered(void) ; 85int is_transmit2_triggered(void) ; 86int is_transmit3_triggered(void) ; 87int is_transmit4_triggered(void) ; 88int is_transmit5_triggered(void) ; 89int is_transmit6_triggered(void) ; 90int is_transmit7_triggered(void) ; 91int is_transmit8_triggered(void) ; 92int is_transmit9_triggered(void) ; 93int is_transmit10_triggered(void) ; 94int is_transmit11_triggered(void) ; 95int is_transmit12_triggered(void) ; 96int is_transmit13_triggered(void) ; 97void immediate_notify(void) ; 98int token ; 99int __VERIFIER_nondet_int() ; 100int local ; 101void master(void) 102{ 103 104 { 105 if (m_pc == 0) { 106 goto M_ENTRY; 107 } else { 108 if (m_pc == 1) { 109 goto M_WAIT; 110 } else { 111 112 } 113 } 114 M_ENTRY: ; 115 { 116 while (1) { 117 while_0_continue: /* CIL Label */ ; 118 { 119 token = __VERIFIER_nondet_int(); 120 local = token; 121 E_1 = 1; 122 immediate_notify(); 123 E_1 = 2; 124 m_pc = 1; 125 m_st = 2; 126 } 127 128 goto return_label; 129 M_WAIT: ; 130 if (token != local + 13) { 131 { 132 error(); 133 } 134 } else { 135 136 } 137 } 138 while_0_break: /* CIL Label */ ; 139 } 140 141 return_label: /* CIL Label */ 142 return; 143} 144} 145void transmit1(void) 146{ 147 148 { 149 if (t1_pc == 0) { 150 goto T1_ENTRY; 151 } else { 152 if (t1_pc == 1) { 153 goto T1_WAIT; 154 } else { 155 156 } 157 } 158 T1_ENTRY: ; 159 { 160 while (1) { 161 while_1_continue: /* CIL Label */ ; 162 t1_pc = 1; 163 t1_st = 2; 164 165 goto return_label; 166 T1_WAIT: 167 { 168 token += 1; 169 E_2 = 1; 170 immediate_notify(); 171 E_2 = 2; 172 } 173 } 174 while_1_break: /* CIL Label */ ; 175 } 176 177 return_label: /* CIL Label */ 178 return; 179} 180} 181void transmit2(void) 182{ 183 184 { 185 if (t2_pc == 0) { 186 goto T2_ENTRY; 187 } else { 188 if (t2_pc == 1) { 189 goto T2_WAIT; 190 } else { 191 192 } 193 } 194 T2_ENTRY: ; 195 { 196 while (1) { 197 while_2_continue: /* CIL Label */ ; 198 t2_pc = 1; 199 t2_st = 2; 200 201 goto return_label; 202 T2_WAIT: 203 { 204 token += 1; 205 E_3 = 1; 206 immediate_notify(); 207 E_3 = 2; 208 } 209 } 210 while_2_break: /* CIL Label */ ; 211 } 212 213 return_label: /* CIL Label */ 214 return; 215} 216} 217void transmit3(void) 218{ 219 220 { 221 if (t3_pc == 0) { 222 goto T3_ENTRY; 223 } else { 224 if (t3_pc == 1) { 225 goto T3_WAIT; 226 } else { 227 228 } 229 } 230 T3_ENTRY: ; 231 { 232 while (1) { 233 while_3_continue: /* CIL Label */ ; 234 t3_pc = 1; 235 t3_st = 2; 236 237 goto return_label; 238 T3_WAIT: 239 { 240 token += 1; 241 E_4 = 1; 242 immediate_notify(); 243 E_4 = 2; 244 } 245 } 246 while_3_break: /* CIL Label */ ; 247 } 248 249 return_label: /* CIL Label */ 250 return; 251} 252} 253void transmit4(void) 254{ 255 256 { 257 if (t4_pc == 0) { 258 goto T4_ENTRY; 259 } else { 260 if (t4_pc == 1) { 261 goto T4_WAIT; 262 } else { 263 264 } 265 } 266 T4_ENTRY: ; 267 { 268 while (1) { 269 while_4_continue: /* CIL Label */ ; 270 t4_pc = 1; 271 t4_st = 2; 272 273 goto return_label; 274 T4_WAIT: 275 { 276 token += 1; 277 E_5 = 1; 278 immediate_notify(); 279 E_5 = 2; 280 } 281 } 282 while_4_break: /* CIL Label */ ; 283 } 284 285 return_label: /* CIL Label */ 286 return; 287} 288} 289void transmit5(void) 290{ 291 292 { 293 if (t5_pc == 0) { 294 goto T5_ENTRY; 295 } else { 296 if (t5_pc == 1) { 297 goto T5_WAIT; 298 } else { 299 300 } 301 } 302 T5_ENTRY: ; 303 { 304 while (1) { 305 while_5_continue: /* CIL Label */ ; 306 t5_pc = 1; 307 t5_st = 2; 308 309 goto return_label; 310 T5_WAIT: 311 { 312 token += 1; 313 E_6 = 1; 314 immediate_notify(); 315 E_6 = 2; 316 } 317 } 318 while_5_break: /* CIL Label */ ; 319 } 320 321 return_label: /* CIL Label */ 322 return; 323} 324} 325void transmit6(void) 326{ 327 328 { 329 if (t6_pc == 0) { 330 goto T6_ENTRY; 331 } else { 332 if (t6_pc == 1) { 333 goto T6_WAIT; 334 } else { 335 336 } 337 } 338 T6_ENTRY: ; 339 { 340 while (1) { 341 while_6_continue: /* CIL Label */ ; 342 t6_pc = 1; 343 t6_st = 2; 344 345 goto return_label; 346 T6_WAIT: 347 { 348 token += 1; 349 E_7 = 1; 350 immediate_notify(); 351 E_7 = 2; 352 } 353 } 354 while_6_break: /* CIL Label */ ; 355 } 356 357 return_label: /* CIL Label */ 358 return; 359} 360} 361void transmit7(void) 362{ 363 364 { 365 if (t7_pc == 0) { 366 goto T7_ENTRY; 367 } else { 368 if (t7_pc == 1) { 369 goto T7_WAIT; 370 } else { 371 372 } 373 } 374 T7_ENTRY: ; 375 { 376 while (1) { 377 while_7_continue: /* CIL Label */ ; 378 t7_pc = 1; 379 t7_st = 2; 380 381 goto return_label; 382 T7_WAIT: 383 { 384 token += 1; 385 E_8 = 1; 386 immediate_notify(); 387 E_8 = 2; 388 } 389 } 390 while_7_break: /* CIL Label */ ; 391 } 392 393 return_label: /* CIL Label */ 394 return; 395} 396} 397void transmit8(void) 398{ 399 400 { 401 if (t8_pc == 0) { 402 goto T8_ENTRY; 403 } else { 404 if (t8_pc == 1) { 405 goto T8_WAIT; 406 } else { 407 408 } 409 } 410 T8_ENTRY: ; 411 { 412 while (1) { 413 while_8_continue: /* CIL Label */ ; 414 t8_pc = 1; 415 t8_st = 2; 416 417 goto return_label; 418 T8_WAIT: 419 { 420 token += 1; 421 E_9 = 1; 422 immediate_notify(); 423 E_9 = 2; 424 } 425 } 426 while_8_break: /* CIL Label */ ; 427 } 428 429 return_label: /* CIL Label */ 430 return; 431} 432} 433void transmit9(void) 434{ 435 436 { 437 if (t9_pc == 0) { 438 goto T9_ENTRY; 439 } else { 440 if (t9_pc == 1) { 441 goto T9_WAIT; 442 } else { 443 444 } 445 } 446 T9_ENTRY: ; 447 { 448 while (1) { 449 while_9_continue: /* CIL Label */ ; 450 t9_pc = 1; 451 t9_st = 2; 452 453 goto return_label; 454 T9_WAIT: 455 { 456 token += 1; 457 E_10 = 1; 458 immediate_notify(); 459 E_10 = 2; 460 } 461 } 462 while_9_break: /* CIL Label */ ; 463 } 464 465 return_label: /* CIL Label */ 466 return; 467} 468} 469void transmit10(void) 470{ 471 472 { 473 if (t10_pc == 0) { 474 goto T10_ENTRY; 475 } else { 476 if (t10_pc == 1) { 477 goto T10_WAIT; 478 } else { 479 480 } 481 } 482 T10_ENTRY: ; 483 { 484 while (1) { 485 while_10_continue: /* CIL Label */ ; 486 t10_pc = 1; 487 t10_st = 2; 488 489 goto return_label; 490 T10_WAIT: 491 { 492 token += 1; 493 E_11 = 1; 494 immediate_notify(); 495 E_11 = 2; 496 } 497 } 498 while_10_break: /* CIL Label */ ; 499 } 500 501 return_label: /* CIL Label */ 502 return; 503} 504} 505void transmit11(void) 506{ 507 508 { 509 if (t11_pc == 0) { 510 goto T11_ENTRY; 511 } else { 512 if (t11_pc == 1) { 513 goto T11_WAIT; 514 } else { 515 516 } 517 } 518 T11_ENTRY: ; 519 { 520 while (1) { 521 while_11_continue: /* CIL Label */ ; 522 t11_pc = 1; 523 t11_st = 2; 524 525 goto return_label; 526 T11_WAIT: 527 { 528 token += 1; 529 E_12 = 1; 530 immediate_notify(); 531 E_12 = 2; 532 } 533 } 534 while_11_break: /* CIL Label */ ; 535 } 536 537 return_label: /* CIL Label */ 538 return; 539} 540} 541void transmit12(void) 542{ 543 544 { 545 if (t12_pc == 0) { 546 goto T12_ENTRY; 547 } else { 548 if (t12_pc == 1) { 549 goto T12_WAIT; 550 } else { 551 552 } 553 } 554 T12_ENTRY: ; 555 { 556 while (1) { 557 while_12_continue: /* CIL Label */ ; 558 t12_pc = 1; 559 t12_st = 2; 560 561 goto return_label; 562 T12_WAIT: 563 { 564 token += 1; 565 E_13 = 1; 566 immediate_notify(); 567 E_13 = 2; 568 } 569 } 570 while_12_break: /* CIL Label */ ; 571 } 572 573 return_label: /* CIL Label */ 574 return; 575} 576} 577void transmit13(void) 578{ 579 580 { 581 if (t13_pc == 0) { 582 goto T13_ENTRY; 583 } else { 584 if (t13_pc == 1) { 585 goto T13_WAIT; 586 } else { 587 588 } 589 } 590 T13_ENTRY: ; 591 { 592 while (1) { 593 while_13_continue: /* CIL Label */ ; 594 t13_pc = 1; 595 t13_st = 2; 596 597 goto return_label; 598 T13_WAIT: 599 { 600 token += 1; 601 E_M = 1; 602 immediate_notify(); 603 E_M = 2; 604 } 605 } 606 while_13_break: /* CIL Label */ ; 607 } 608 609 return_label: /* CIL Label */ 610 return; 611} 612} 613int is_master_triggered(void) 614{ int __retres1 ; 615 616 { 617 if (m_pc == 1) { 618 if (E_M == 1) { 619 __retres1 = 1; 620 goto return_label; 621 } else { 622 623 } 624 } else { 625 626 } 627 __retres1 = 0; 628 return_label: /* CIL Label */ 629 return (__retres1); 630} 631} 632int is_transmit1_triggered(void) 633{ int __retres1 ; 634 635 { 636 if (t1_pc == 1) { 637 if (E_1 == 1) { 638 __retres1 = 1; 639 goto return_label; 640 } else { 641 642 } 643 } else { 644 645 } 646 __retres1 = 0; 647 return_label: /* CIL Label */ 648 return (__retres1); 649} 650} 651int is_transmit2_triggered(void) 652{ int __retres1 ; 653 654 { 655 if (t2_pc == 1) { 656 if (E_2 == 1) { 657 __retres1 = 1; 658 goto return_label; 659 } else { 660 661 } 662 } else { 663 664 } 665 __retres1 = 0; 666 return_label: /* CIL Label */ 667 return (__retres1); 668} 669} 670int is_transmit3_triggered(void) 671{ int __retres1 ; 672 673 { 674 if (t3_pc == 1) { 675 if (E_3 == 1) { 676 __retres1 = 1; 677 goto return_label; 678 } else { 679 680 } 681 } else { 682 683 } 684 __retres1 = 0; 685 return_label: /* CIL Label */ 686 return (__retres1); 687} 688} 689int is_transmit4_triggered(void) 690{ int __retres1 ; 691 692 { 693 if (t4_pc == 1) { 694 if (E_4 == 1) { 695 __retres1 = 1; 696 goto return_label; 697 } else { 698 699 } 700 } else { 701 702 } 703 __retres1 = 0; 704 return_label: /* CIL Label */ 705 return (__retres1); 706} 707} 708int is_transmit5_triggered(void) 709{ int __retres1 ; 710 711 { 712 if (t5_pc == 1) { 713 if (E_5 == 1) { 714 __retres1 = 1; 715 goto return_label; 716 } else { 717 718 } 719 } else { 720 721 } 722 __retres1 = 0; 723 return_label: /* CIL Label */ 724 return (__retres1); 725} 726} 727int is_transmit6_triggered(void) 728{ int __retres1 ; 729 730 { 731 if (t6_pc == 1) { 732 if (E_6 == 1) { 733 __retres1 = 1; 734 goto return_label; 735 } else { 736 737 } 738 } else { 739 740 } 741 __retres1 = 0; 742 return_label: /* CIL Label */ 743 return (__retres1); 744} 745} 746int is_transmit7_triggered(void) 747{ int __retres1 ; 748 749 { 750 if (t7_pc == 1) { 751 if (E_7 == 1) { 752 __retres1 = 1; 753 goto return_label; 754 } else { 755 756 } 757 } else { 758 759 } 760 __retres1 = 0; 761 return_label: /* CIL Label */ 762 return (__retres1); 763} 764} 765int is_transmit8_triggered(void) 766{ int __retres1 ; 767 768 { 769 if (t8_pc == 1) { 770 if (E_8 == 1) { 771 __retres1 = 1; 772 goto return_label; 773 } else { 774 775 } 776 } else { 777 778 } 779 __retres1 = 0; 780 return_label: /* CIL Label */ 781 return (__retres1); 782} 783} 784int is_transmit9_triggered(void) 785{ int __retres1 ; 786 787 { 788 if (t9_pc == 1) { 789 if (E_9 == 1) { 790 __retres1 = 1; 791 goto return_label; 792 } else { 793 794 } 795 } else { 796 797 } 798 __retres1 = 0; 799 return_label: /* CIL Label */ 800 return (__retres1); 801} 802} 803int is_transmit10_triggered(void) 804{ int __retres1 ; 805 806 { 807 if (t10_pc == 1) { 808 if (E_10 == 1) { 809 __retres1 = 1; 810 goto return_label; 811 } else { 812 813 } 814 } else { 815 816 } 817 __retres1 = 0; 818 return_label: /* CIL Label */ 819 return (__retres1); 820} 821} 822int is_transmit11_triggered(void) 823{ int __retres1 ; 824 825 { 826 if (t11_pc == 1) { 827 if (E_11 == 1) { 828 __retres1 = 1; 829 goto return_label; 830 } else { 831 832 } 833 } else { 834 835 } 836 __retres1 = 0; 837 return_label: /* CIL Label */ 838 return (__retres1); 839} 840} 841int is_transmit12_triggered(void) 842{ int __retres1 ; 843 844 { 845 if (t12_pc == 1) { 846 if (E_12 == 1) { 847 __retres1 = 1; 848 goto return_label; 849 } else { 850 851 } 852 } else { 853 854 } 855 __retres1 = 0; 856 return_label: /* CIL Label */ 857 return (__retres1); 858} 859} 860int is_transmit13_triggered(void) 861{ int __retres1 ; 862 863 { 864 if (t13_pc == 1) { 865 if (E_13 == 1) { 866 __retres1 = 1; 867 goto return_label; 868 } else { 869 870 } 871 } else { 872 873 } 874 __retres1 = 0; 875 return_label: /* CIL Label */ 876 return (__retres1); 877} 878} 879void update_channels(void) 880{ 881 882 { 883 884 return; 885} 886} 887void init_threads(void) 888{ 889 890 { 891 if (m_i == 1) { 892 m_st = 0; 893 } else { 894 m_st = 2; 895 } 896 if (t1_i == 1) { 897 t1_st = 0; 898 } else { 899 t1_st = 2; 900 } 901 if (t2_i == 1) { 902 t2_st = 0; 903 } else { 904 t2_st = 2; 905 } 906 if (t3_i == 1) { 907 t3_st = 0; 908 } else { 909 t3_st = 2; 910 } 911 if (t4_i == 1) { 912 t4_st = 0; 913 } else { 914 t4_st = 2; 915 } 916 if (t5_i == 1) { 917 t5_st = 0; 918 } else { 919 t5_st = 2; 920 } 921 if (t6_i == 1) { 922 t6_st = 0; 923 } else { 924 t6_st = 2; 925 } 926 if (t7_i == 1) { 927 t7_st = 0; 928 } else { 929 t7_st = 2; 930 } 931 if (t8_i == 1) { 932 t8_st = 0; 933 } else { 934 t8_st = 2; 935 } 936 if (t9_i == 1) { 937 t9_st = 0; 938 } else { 939 t9_st = 2; 940 } 941 if (t10_i == 1) { 942 t10_st = 0; 943 } else { 944 t10_st = 2; 945 } 946 if (t11_i == 1) { 947 t11_st = 0; 948 } else { 949 t11_st = 2; 950 } 951 if (t12_i == 1) { 952 t12_st = 0; 953 } else { 954 t12_st = 2; 955 } 956 if (t13_i == 1) { 957 t13_st = 0; 958 } else { 959 t13_st = 2; 960 } 961 962 return; 963} 964} 965int exists_runnable_thread(void) 966{ int __retres1 ; 967 968 { 969 if (m_st == 0) { 970 __retres1 = 1; 971 goto return_label; 972 } else { 973 if (t1_st == 0) { 974 __retres1 = 1; 975 goto return_label; 976 } else { 977 if (t2_st == 0) { 978 __retres1 = 1; 979 goto return_label; 980 } else { 981 if (t3_st == 0) { 982 __retres1 = 1; 983 goto return_label; 984 } else { 985 if (t4_st == 0) { 986 __retres1 = 1; 987 goto return_label; 988 } else { 989 if (t5_st == 0) { 990 __retres1 = 1; 991 goto return_label; 992 } else { 993 if (t6_st == 0) { 994 __retres1 = 1; 995 goto return_label; 996 } else { 997 if (t7_st == 0) { 998 __retres1 = 1; 999 goto return_label; 1000 } else { 1001 if (t8_st == 0) { 1002 __retres1 = 1; 1003 goto return_label; 1004 } else { 1005 if (t9_st == 0) { 1006 __retres1 = 1; 1007 goto return_label; 1008 } else { 1009 if (t10_st == 0) { 1010 __retres1 = 1; 1011 goto return_label; 1012 } else { 1013 if (t11_st == 0) { 1014 __retres1 = 1; 1015 goto return_label; 1016 } else { 1017 if (t12_st == 0) { 1018 __retres1 = 1; 1019 goto return_label; 1020 } else { 1021 if (t13_st == 0) { 1022 __retres1 = 1; 1023 goto return_label; 1024 } else { 1025 1026 } 1027 } 1028 } 1029 } 1030 } 1031 } 1032 } 1033 } 1034 } 1035 } 1036 } 1037 } 1038 } 1039 } 1040 __retres1 = 0; 1041 return_label: /* CIL Label */ 1042 return (__retres1); 1043} 1044} 1045void eval(void) 1046{// int __VERIFIER_nondet_int()___0 ; 1047 int tmp ; 1048 1049 { 1050 { 1051 while (1) { 1052 while_14_continue: /* CIL Label */ ; 1053 { 1054 tmp = exists_runnable_thread(); 1055 } 1056 if (tmp) { 1057 1058 } else { 1059 goto while_14_break; 1060 } 1061 if (m_st == 0) { 1062 int tmp_ndt_1; 1063 tmp_ndt_1 = __VERIFIER_nondet_int(); 1064 if (tmp_ndt_1) { 1065 { 1066 m_st = 1; 1067 master(); 1068 } 1069 } else { 1070 1071 } 1072 } else { 1073 1074 } 1075 if (t1_st == 0) { 1076 int tmp_ndt_2; 1077 tmp_ndt_2 = __VERIFIER_nondet_int(); 1078 if (tmp_ndt_2) { 1079 { 1080 t1_st = 1; 1081 transmit1(); 1082 } 1083 } else { 1084 1085 } 1086 } else { 1087 1088 } 1089 if (t2_st == 0) { 1090 int tmp_ndt_3; 1091 tmp_ndt_3 = __VERIFIER_nondet_int(); 1092 if (tmp_ndt_3) { 1093 { 1094 t2_st = 1; 1095 transmit2(); 1096 } 1097 } else { 1098 1099 } 1100 } else { 1101 1102 } 1103 if (t3_st == 0) { 1104 int tmp_ndt_4; 1105 tmp_ndt_4 = __VERIFIER_nondet_int(); 1106 if (tmp_ndt_4) { 1107 { 1108 t3_st = 1; 1109 transmit3(); 1110 } 1111 } else { 1112 1113 } 1114 } else { 1115 1116 } 1117 if (t4_st == 0) { 1118 int tmp_ndt_5; 1119 tmp_ndt_5 = __VERIFIER_nondet_int(); 1120 if (tmp_ndt_5) { 1121 { 1122 t4_st = 1; 1123 transmit4(); 1124 } 1125 } else { 1126 1127 } 1128 } else { 1129 1130 } 1131 if (t5_st == 0) { 1132 int tmp_ndt_6; 1133 tmp_ndt_6 = __VERIFIER_nondet_int(); 1134 if (tmp_ndt_6) { 1135 { 1136 t5_st = 1; 1137 transmit5(); 1138 } 1139 } else { 1140 1141 } 1142 } else { 1143 1144 } 1145 if (t6_st == 0) { 1146 int tmp_ndt_7; 1147 tmp_ndt_7 = __VERIFIER_nondet_int(); 1148 if (tmp_ndt_7) { 1149 { 1150 t6_st = 1; 1151 transmit6(); 1152 } 1153 } else { 1154 1155 } 1156 } else { 1157 1158 } 1159 if (t7_st == 0) { 1160 int tmp_ndt_8; 1161 tmp_ndt_8 = __VERIFIER_nondet_int(); 1162 if (tmp_ndt_8) { 1163 { 1164 t7_st = 1; 1165 transmit7(); 1166 } 1167 } else { 1168 1169 } 1170 } else { 1171 1172 } 1173 if (t8_st == 0) { 1174 int tmp_ndt_9; 1175 tmp_ndt_9 = __VERIFIER_nondet_int(); 1176 if (tmp_ndt_9) { 1177 { 1178 t8_st = 1; 1179 transmit8(); 1180 } 1181 } else { 1182 1183 } 1184 } else { 1185 1186 } 1187 if (t9_st == 0) { 1188 int tmp_ndt_10; 1189 tmp_ndt_10 = __VERIFIER_nondet_int(); 1190 if (tmp_ndt_10) { 1191 { 1192 t9_st = 1; 1193 transmit9(); 1194 } 1195 } else { 1196 1197 } 1198 } else { 1199 1200 } 1201 if (t10_st == 0) { 1202 int tmp_ndt_11; 1203 tmp_ndt_11 = __VERIFIER_nondet_int(); 1204 if (tmp_ndt_11) { 1205 { 1206 t10_st = 1; 1207 transmit10(); 1208 } 1209 } else { 1210 1211 } 1212 } else { 1213 1214 } 1215 if (t11_st == 0) { 1216 int tmp_ndt_12; 1217 tmp_ndt_12 = __VERIFIER_nondet_int(); 1218 if (tmp_ndt_12) { 1219 { 1220 t11_st = 1; 1221 transmit11(); 1222 } 1223 } else { 1224 1225 } 1226 } else { 1227 1228 } 1229 if (t12_st == 0) { 1230 int tmp_ndt_13; 1231 tmp_ndt_13 = __VERIFIER_nondet_int(); 1232 if (tmp_ndt_13) { 1233 { 1234 t12_st = 1; 1235 transmit12(); 1236 } 1237 } else { 1238 1239 } 1240 } else { 1241 1242 } 1243 if (t13_st == 0) { 1244 int tmp_ndt_14; 1245 tmp_ndt_14 = __VERIFIER_nondet_int(); 1246 if (tmp_ndt_14) { 1247 { 1248 t13_st = 1; 1249 transmit13(); 1250 } 1251 } else { 1252 1253 } 1254 } else { 1255 1256 } 1257 } 1258 while_14_break: /* CIL Label */ ; 1259 } 1260 1261 return; 1262} 1263} 1264void fire_delta_events(void) 1265{ 1266 1267 { 1268 if (M_E == 0) { 1269 M_E = 1; 1270 } else { 1271 1272 } 1273 if (T1_E == 0) { 1274 T1_E = 1; 1275 } else { 1276 1277 } 1278 if (T2_E == 0) { 1279 T2_E = 1; 1280 } else { 1281 1282 } 1283 if (T3_E == 0) { 1284 T3_E = 1; 1285 } else { 1286 1287 } 1288 if (T4_E == 0) { 1289 T4_E = 1; 1290 } else { 1291 1292 } 1293 if (T5_E == 0) { 1294 T5_E = 1; 1295 } else { 1296 1297 } 1298 if (T6_E == 0) { 1299 T6_E = 1; 1300 } else { 1301 1302 } 1303 if (T7_E == 0) { 1304 T7_E = 1; 1305 } else { 1306 1307 } 1308 if (T8_E == 0) { 1309 T8_E = 1; 1310 } else { 1311 1312 } 1313 if (T9_E == 0) { 1314 T9_E = 1; 1315 } else { 1316 1317 } 1318 if (T10_E == 0) { 1319 T10_E = 1; 1320 } else { 1321 1322 } 1323 if (T11_E == 0) { 1324 T11_E = 1; 1325 } else { 1326 1327 } 1328 if (T12_E == 0) { 1329 T12_E = 1; 1330 } else { 1331 1332 } 1333 if (T13_E == 0) { 1334 T13_E = 1; 1335 } else { 1336 1337 } 1338 if (E_M == 0) { 1339 E_M = 1; 1340 } else { 1341 1342 } 1343 if (E_1 == 0) { 1344 E_1 = 1; 1345 } else { 1346 1347 } 1348 if (E_2 == 0) { 1349 E_2 = 1; 1350 } else { 1351 1352 } 1353 if (E_3 == 0) { 1354 E_3 = 1; 1355 } else { 1356 1357 } 1358 if (E_4 == 0) { 1359 E_4 = 1; 1360 } else { 1361 1362 } 1363 if (E_5 == 0) { 1364 E_5 = 1; 1365 } else { 1366 1367 } 1368 if (E_6 == 0) { 1369 E_6 = 1; 1370 } else { 1371 1372 } 1373 if (E_7 == 0) { 1374 E_7 = 1; 1375 } else { 1376 1377 } 1378 if (E_8 == 0) { 1379 E_8 = 1; 1380 } else { 1381 1382 } 1383 if (E_9 == 0) { 1384 E_9 = 1; 1385 } else { 1386 1387 } 1388 if (E_10 == 0) { 1389 E_10 = 1; 1390 } else { 1391 1392 } 1393 if (E_11 == 0) { 1394 E_11 = 1; 1395 } else { 1396 1397 } 1398 if (E_12 == 0) { 1399 E_12 = 1; 1400 } else { 1401 1402 } 1403 if (E_13 == 0) { 1404 E_13 = 1; 1405 } else { 1406 1407 } 1408 1409 return; 1410} 1411} 1412void reset_delta_events(void) 1413{ 1414 1415 { 1416 if (M_E == 1) { 1417 M_E = 2; 1418 } else { 1419 1420 } 1421 if (T1_E == 1) { 1422 T1_E = 2; 1423 } else { 1424 1425 } 1426 if (T2_E == 1) { 1427 T2_E = 2; 1428 } else { 1429 1430 } 1431 if (T3_E == 1) { 1432 T3_E = 2; 1433 } else { 1434 1435 } 1436 if (T4_E == 1) { 1437 T4_E = 2; 1438 } else { 1439 1440 } 1441 if (T5_E == 1) { 1442 T5_E = 2; 1443 } else { 1444 1445 } 1446 if (T6_E == 1) { 1447 T6_E = 2; 1448 } else { 1449 1450 } 1451 if (T7_E == 1) { 1452 T7_E = 2; 1453 } else { 1454 1455 } 1456 if (T8_E == 1) { 1457 T8_E = 2; 1458 } else { 1459 1460 } 1461 if (T9_E == 1) { 1462 T9_E = 2; 1463 } else { 1464 1465 } 1466 if (T10_E == 1) { 1467 T10_E = 2; 1468 } else { 1469 1470 } 1471 if (T11_E == 1) { 1472 T11_E = 2; 1473 } else { 1474 1475 } 1476 if (T12_E == 1) { 1477 T12_E = 2; 1478 } else { 1479 1480 } 1481 if (T13_E == 1) { 1482 T13_E = 2; 1483 } else { 1484 1485 } 1486 if (E_M == 1) { 1487 E_M = 2; 1488 } else { 1489 1490 } 1491 if (E_1 == 1) { 1492 E_1 = 2; 1493 } else { 1494 1495 } 1496 if (E_2 == 1) { 1497 E_2 = 2; 1498 } else { 1499 1500 } 1501 if (E_3 == 1) { 1502 E_3 = 2; 1503 } else { 1504 1505 } 1506 if (E_4 == 1) { 1507 E_4 = 2; 1508 } else { 1509 1510 } 1511 if (E_5 == 1) { 1512 E_5 = 2; 1513 } else { 1514 1515 } 1516 if (E_6 == 1) { 1517 E_6 = 2; 1518 } else { 1519 1520 } 1521 if (E_7 == 1) { 1522 E_7 = 2; 1523 } else { 1524 1525 } 1526 if (E_8 == 1) { 1527 E_8 = 2; 1528 } else { 1529 1530 } 1531 if (E_9 == 1) { 1532 E_9 = 2; 1533 } else { 1534 1535 } 1536 if (E_10 == 1) { 1537 E_10 = 2; 1538 } else { 1539 1540 } 1541 if (E_11 == 1) { 1542 E_11 = 2; 1543 } else { 1544 1545 } 1546 if (E_12 == 1) { 1547 E_12 = 2; 1548 } else { 1549 1550 } 1551 if (E_13 == 1) { 1552 E_13 = 2; 1553 } else { 1554 1555 } 1556 1557 return; 1558} 1559} 1560void activate_threads(void) 1561{ int tmp ; 1562 int tmp___0 ; 1563 int tmp___1 ; 1564 int tmp___2 ; 1565 int tmp___3 ; 1566 int tmp___4 ; 1567 int tmp___5 ; 1568 int tmp___6 ; 1569 int tmp___7 ; 1570 int tmp___8 ; 1571 int tmp___9 ; 1572 int tmp___10 ; 1573 int tmp___11 ; 1574 int tmp___12 ; 1575 1576 { 1577 { 1578 tmp = is_master_triggered(); 1579 } 1580 if (tmp) { 1581 m_st = 0; 1582 } else { 1583 1584 } 1585 { 1586 tmp___0 = is_transmit1_triggered(); 1587 } 1588 if (tmp___0) { 1589 t1_st = 0; 1590 } else { 1591 1592 } 1593 { 1594 tmp___1 = is_transmit2_triggered(); 1595 } 1596 if (tmp___1) { 1597 t2_st = 0; 1598 } else { 1599 1600 } 1601 { 1602 tmp___2 = is_transmit3_triggered(); 1603 } 1604 if (tmp___2) { 1605 t3_st = 0; 1606 } else { 1607 1608 } 1609 { 1610 tmp___3 = is_transmit4_triggered(); 1611 } 1612 if (tmp___3) { 1613 t4_st = 0; 1614 } else { 1615 1616 } 1617 { 1618 tmp___4 = is_transmit5_triggered(); 1619 } 1620 if (tmp___4) { 1621 t5_st = 0; 1622 } else { 1623 1624 } 1625 { 1626 tmp___5 = is_transmit6_triggered(); 1627 } 1628 if (tmp___5) { 1629 t6_st = 0; 1630 } else { 1631 1632 } 1633 { 1634 tmp___6 = is_transmit7_triggered(); 1635 } 1636 if (tmp___6) { 1637 t7_st = 0; 1638 } else { 1639 1640 } 1641 { 1642 tmp___7 = is_transmit8_triggered(); 1643 } 1644 if (tmp___7) { 1645 t8_st = 0; 1646 } else { 1647 1648 } 1649 { 1650 tmp___8 = is_transmit9_triggered(); 1651 } 1652 if (tmp___8) { 1653 t9_st = 0; 1654 } else { 1655 1656 } 1657 { 1658 tmp___9 = is_transmit10_triggered(); 1659 } 1660 if (tmp___9) { 1661 t10_st = 0; 1662 } else { 1663 1664 } 1665 { 1666 tmp___10 = is_transmit11_triggered(); 1667 } 1668 if (tmp___10) { 1669 t11_st = 0; 1670 } else { 1671 1672 } 1673 { 1674 tmp___11 = is_transmit12_triggered(); 1675 } 1676 if (tmp___11) { 1677 t12_st = 0; 1678 } else { 1679 1680 } 1681 { 1682 tmp___12 = is_transmit13_triggered(); 1683 } 1684 if (tmp___12) { 1685 t13_st = 0; 1686 } else { 1687 1688 } 1689 1690 return; 1691} 1692} 1693void immediate_notify(void) 1694{ 1695 1696 { 1697 { 1698 activate_threads(); 1699 } 1700 1701 return; 1702} 1703} 1704void fire_time_events(void) 1705{ 1706 1707 { 1708 M_E = 1; 1709 1710 return; 1711} 1712} 1713void reset_time_events(void) 1714{ 1715 1716 { 1717 if (M_E == 1) { 1718 M_E = 2; 1719 } else { 1720 1721 } 1722 if (T1_E == 1) { 1723 T1_E = 2; 1724 } else { 1725 1726 } 1727 if (T2_E == 1) { 1728 T2_E = 2; 1729 } else { 1730 1731 } 1732 if (T3_E == 1) { 1733 T3_E = 2; 1734 } else { 1735 1736 } 1737 if (T4_E == 1) { 1738 T4_E = 2; 1739 } else { 1740 1741 } 1742 if (T5_E == 1) { 1743 T5_E = 2; 1744 } else { 1745 1746 } 1747 if (T6_E == 1) { 1748 T6_E = 2; 1749 } else { 1750 1751 } 1752 if (T7_E == 1) { 1753 T7_E = 2; 1754 } else { 1755 1756 } 1757 if (T8_E == 1) { 1758 T8_E = 2; 1759 } else { 1760 1761 } 1762 if (T9_E == 1) { 1763 T9_E = 2; 1764 } else { 1765 1766 } 1767 if (T10_E == 1) { 1768 T10_E = 2; 1769 } else { 1770 1771 } 1772 if (T11_E == 1) { 1773 T11_E = 2; 1774 } else { 1775 1776 } 1777 if (T12_E == 1) { 1778 T12_E = 2; 1779 } else { 1780 1781 } 1782 if (T13_E == 1) { 1783 T13_E = 2; 1784 } else { 1785 1786 } 1787 if (E_M == 1) { 1788 E_M = 2; 1789 } else { 1790 1791 } 1792 if (E_1 == 1) { 1793 E_1 = 2; 1794 } else { 1795 1796 } 1797 if (E_2 == 1) { 1798 E_2 = 2; 1799 } else { 1800 1801 } 1802 if (E_3 == 1) { 1803 E_3 = 2; 1804 } else { 1805 1806 } 1807 if (E_4 == 1) { 1808 E_4 = 2; 1809 } else { 1810 1811 } 1812 if (E_5 == 1) { 1813 E_5 = 2; 1814 } else { 1815 1816 } 1817 if (E_6 == 1) { 1818 E_6 = 2; 1819 } else { 1820 1821 } 1822 if (E_7 == 1) { 1823 E_7 = 2; 1824 } else { 1825 1826 } 1827 if (E_8 == 1) { 1828 E_8 = 2; 1829 } else { 1830 1831 } 1832 if (E_9 == 1) { 1833 E_9 = 2; 1834 } else { 1835 1836 } 1837 if (E_10 == 1) { 1838 E_10 = 2; 1839 } else { 1840 1841 } 1842 if (E_11 == 1) { 1843 E_11 = 2; 1844 } else { 1845 1846 } 1847 if (E_12 == 1) { 1848 E_12 = 2; 1849 } else { 1850 1851 } 1852 if (E_13 == 1) { 1853 E_13 = 2; 1854 } else { 1855 1856 } 1857 1858 return; 1859} 1860} 1861void init_model(void) 1862{ 1863 1864 { 1865 m_i = 1; 1866 t1_i = 1; 1867 t2_i = 1; 1868 t3_i = 1; 1869 t4_i = 1; 1870 t5_i = 1; 1871 t6_i = 1; 1872 t7_i = 1; 1873 t8_i = 1; 1874 t9_i = 1; 1875 t10_i = 1; 1876 t11_i = 1; 1877 t12_i = 1; 1878 t13_i = 1; 1879 1880 return; 1881} 1882} 1883int stop_simulation(void) 1884{ int tmp ; 1885 int __retres2 ; 1886 1887 { 1888 { 1889 tmp = exists_runnable_thread(); 1890 } 1891 if (tmp) { 1892 __retres2 = 0; 1893 goto return_label; 1894 } else { 1895 1896 } 1897 __retres2 = 1; 1898 return_label: /* CIL Label */ 1899 return (__retres2); 1900} 1901} 1902void start_simulation(void) 1903{ int kernel_st ; 1904 int tmp ; 1905 int tmp___0 ; 1906 1907 { 1908 { 1909 kernel_st = 0; 1910 update_channels(); 1911 init_threads(); 1912 fire_delta_events(); 1913 activate_threads(); 1914 reset_delta_events(); 1915 } 1916 { 1917 while (1) { 1918 while_15_continue: /* CIL Label */ ; 1919 { 1920 kernel_st = 1; 1921 eval(); 1922 } 1923 { 1924 kernel_st = 2; 1925 update_channels(); 1926 } 1927 { 1928 kernel_st = 3; 1929 fire_delta_events(); 1930 activate_threads(); 1931 reset_delta_events(); 1932 } 1933 { 1934 tmp = exists_runnable_thread(); 1935 } 1936 if (tmp == 0) { 1937 { 1938 kernel_st = 4; 1939 fire_time_events(); 1940 activate_threads(); 1941 reset_time_events(); 1942 } 1943 } else { 1944 1945 } 1946 { 1947 tmp___0 = stop_simulation(); 1948 } 1949 if (tmp___0) { 1950 goto while_15_break; 1951 } else { 1952 1953 } 1954 } 1955 while_15_break: /* CIL Label */ ; 1956 } 1957 1958 return; 1959} 1960} 1961int main(void) 1962{ int __retres1 ; 1963 1964 { 1965 { 1966 init_model(); 1967 start_simulation(); 1968 } 1969 __retres1 = 0; 1970 return (__retres1); 1971} 1972}