Showing error 281

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.10.BUG.cil.c
Line in file: 8
Project: SV-COMP 2012
Tools: Manual Work
Entered: 2012-11-19 13:47:39 UTC

Source: 

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