Showing error 2332

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