Showing error 261

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