Showing error 2331

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.09_unsafe.cil.c
Line in file: 9
Project: SV-COMP 2013
Project version: 2.6.28
Tools: Manual Work
Entered: 2013-01-17 16:57:54 UTC

Source: 

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