Showing error 267

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

Source: 

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