Showing error 263

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