Showing error 258

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