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