Showing error 2310

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