Showing error 266

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.13.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 t13_pc  =    0;
  27int m_st  ;
  28int t1_st  ;
  29int t2_st  ;
  30int t3_st  ;
  31int t4_st  ;
  32int t5_st  ;
  33int t6_st  ;
  34int t7_st  ;
  35int t8_st  ;
  36int t9_st  ;
  37int t10_st  ;
  38int t11_st  ;
  39int t12_st  ;
  40int t13_st  ;
  41int m_i  ;
  42int t1_i  ;
  43int t2_i  ;
  44int t3_i  ;
  45int t4_i  ;
  46int t5_i  ;
  47int t6_i  ;
  48int t7_i  ;
  49int t8_i  ;
  50int t9_i  ;
  51int t10_i  ;
  52int t11_i  ;
  53int t12_i  ;
  54int t13_i  ;
  55int M_E  =    2;
  56int T1_E  =    2;
  57int T2_E  =    2;
  58int T3_E  =    2;
  59int T4_E  =    2;
  60int T5_E  =    2;
  61int T6_E  =    2;
  62int T7_E  =    2;
  63int T8_E  =    2;
  64int T9_E  =    2;
  65int T10_E  =    2;
  66int T11_E  =    2;
  67int T12_E  =    2;
  68int T13_E  =    2;
  69int E_M  =    2;
  70int E_1  =    2;
  71int E_2  =    2;
  72int E_3  =    2;
  73int E_4  =    2;
  74int E_5  =    2;
  75int E_6  =    2;
  76int E_7  =    2;
  77int E_8  =    2;
  78int E_9  =    2;
  79int E_10  =    2;
  80int E_11  =    2;
  81int E_12  =    2;
  82int E_13  =    2;
  83int is_master_triggered(void) ;
  84int is_transmit1_triggered(void) ;
  85int is_transmit2_triggered(void) ;
  86int is_transmit3_triggered(void) ;
  87int is_transmit4_triggered(void) ;
  88int is_transmit5_triggered(void) ;
  89int is_transmit6_triggered(void) ;
  90int is_transmit7_triggered(void) ;
  91int is_transmit8_triggered(void) ;
  92int is_transmit9_triggered(void) ;
  93int is_transmit10_triggered(void) ;
  94int is_transmit11_triggered(void) ;
  95int is_transmit12_triggered(void) ;
  96int is_transmit13_triggered(void) ;
  97void immediate_notify(void) ;
  98int token  ;
  99int __VERIFIER_nondet_int()  ;
 100int local  ;
 101void master(void) 
 102{ 
 103
 104  {
 105  if (m_pc == 0) {
 106    goto M_ENTRY;
 107  } else {
 108    if (m_pc == 1) {
 109      goto M_WAIT;
 110    } else {
 111
 112    }
 113  }
 114  M_ENTRY: ;
 115  {
 116  while (1) {
 117    while_0_continue: /* CIL Label */ ;
 118    {
 119    token = __VERIFIER_nondet_int();
 120    local = token;
 121    E_1 = 1;
 122    immediate_notify();
 123    E_1 = 2;
 124    m_pc = 1;
 125    m_st = 2;
 126    }
 127
 128    goto return_label;
 129    M_WAIT: ;
 130    if (token != local + 13) {
 131      {
 132      error();
 133      }
 134    } else {
 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_12 = 1;
 530    immediate_notify();
 531    E_12 = 2;
 532    }
 533  }
 534  while_11_break: /* CIL Label */ ;
 535  }
 536
 537  return_label: /* CIL Label */ 
 538  return;
 539}
 540}
 541void transmit12(void) 
 542{ 
 543
 544  {
 545  if (t12_pc == 0) {
 546    goto T12_ENTRY;
 547  } else {
 548    if (t12_pc == 1) {
 549      goto T12_WAIT;
 550    } else {
 551
 552    }
 553  }
 554  T12_ENTRY: ;
 555  {
 556  while (1) {
 557    while_12_continue: /* CIL Label */ ;
 558    t12_pc = 1;
 559    t12_st = 2;
 560
 561    goto return_label;
 562    T12_WAIT: 
 563    {
 564    token += 1;
 565    E_13 = 1;
 566    immediate_notify();
 567    E_13 = 2;
 568    }
 569  }
 570  while_12_break: /* CIL Label */ ;
 571  }
 572
 573  return_label: /* CIL Label */ 
 574  return;
 575}
 576}
 577void transmit13(void) 
 578{ 
 579
 580  {
 581  if (t13_pc == 0) {
 582    goto T13_ENTRY;
 583  } else {
 584    if (t13_pc == 1) {
 585      goto T13_WAIT;
 586    } else {
 587
 588    }
 589  }
 590  T13_ENTRY: ;
 591  {
 592  while (1) {
 593    while_13_continue: /* CIL Label */ ;
 594    t13_pc = 1;
 595    t13_st = 2;
 596
 597    goto return_label;
 598    T13_WAIT: 
 599    {
 600    token += 1;
 601    E_M = 1;
 602    immediate_notify();
 603    E_M = 2;
 604    }
 605  }
 606  while_13_break: /* CIL Label */ ;
 607  }
 608
 609  return_label: /* CIL Label */ 
 610  return;
 611}
 612}
 613int is_master_triggered(void) 
 614{ int __retres1 ;
 615
 616  {
 617  if (m_pc == 1) {
 618    if (E_M == 1) {
 619      __retres1 = 1;
 620      goto return_label;
 621    } else {
 622
 623    }
 624  } else {
 625
 626  }
 627  __retres1 = 0;
 628  return_label: /* CIL Label */ 
 629  return (__retres1);
 630}
 631}
 632int is_transmit1_triggered(void) 
 633{ int __retres1 ;
 634
 635  {
 636  if (t1_pc == 1) {
 637    if (E_1 == 1) {
 638      __retres1 = 1;
 639      goto return_label;
 640    } else {
 641
 642    }
 643  } else {
 644
 645  }
 646  __retres1 = 0;
 647  return_label: /* CIL Label */ 
 648  return (__retres1);
 649}
 650}
 651int is_transmit2_triggered(void) 
 652{ int __retres1 ;
 653
 654  {
 655  if (t2_pc == 1) {
 656    if (E_2 == 1) {
 657      __retres1 = 1;
 658      goto return_label;
 659    } else {
 660
 661    }
 662  } else {
 663
 664  }
 665  __retres1 = 0;
 666  return_label: /* CIL Label */ 
 667  return (__retres1);
 668}
 669}
 670int is_transmit3_triggered(void) 
 671{ int __retres1 ;
 672
 673  {
 674  if (t3_pc == 1) {
 675    if (E_3 == 1) {
 676      __retres1 = 1;
 677      goto return_label;
 678    } else {
 679
 680    }
 681  } else {
 682
 683  }
 684  __retres1 = 0;
 685  return_label: /* CIL Label */ 
 686  return (__retres1);
 687}
 688}
 689int is_transmit4_triggered(void) 
 690{ int __retres1 ;
 691
 692  {
 693  if (t4_pc == 1) {
 694    if (E_4 == 1) {
 695      __retres1 = 1;
 696      goto return_label;
 697    } else {
 698
 699    }
 700  } else {
 701
 702  }
 703  __retres1 = 0;
 704  return_label: /* CIL Label */ 
 705  return (__retres1);
 706}
 707}
 708int is_transmit5_triggered(void) 
 709{ int __retres1 ;
 710
 711  {
 712  if (t5_pc == 1) {
 713    if (E_5 == 1) {
 714      __retres1 = 1;
 715      goto return_label;
 716    } else {
 717
 718    }
 719  } else {
 720
 721  }
 722  __retres1 = 0;
 723  return_label: /* CIL Label */ 
 724  return (__retres1);
 725}
 726}
 727int is_transmit6_triggered(void) 
 728{ int __retres1 ;
 729
 730  {
 731  if (t6_pc == 1) {
 732    if (E_6 == 1) {
 733      __retres1 = 1;
 734      goto return_label;
 735    } else {
 736
 737    }
 738  } else {
 739
 740  }
 741  __retres1 = 0;
 742  return_label: /* CIL Label */ 
 743  return (__retres1);
 744}
 745}
 746int is_transmit7_triggered(void) 
 747{ int __retres1 ;
 748
 749  {
 750  if (t7_pc == 1) {
 751    if (E_7 == 1) {
 752      __retres1 = 1;
 753      goto return_label;
 754    } else {
 755
 756    }
 757  } else {
 758
 759  }
 760  __retres1 = 0;
 761  return_label: /* CIL Label */ 
 762  return (__retres1);
 763}
 764}
 765int is_transmit8_triggered(void) 
 766{ int __retres1 ;
 767
 768  {
 769  if (t8_pc == 1) {
 770    if (E_8 == 1) {
 771      __retres1 = 1;
 772      goto return_label;
 773    } else {
 774
 775    }
 776  } else {
 777
 778  }
 779  __retres1 = 0;
 780  return_label: /* CIL Label */ 
 781  return (__retres1);
 782}
 783}
 784int is_transmit9_triggered(void) 
 785{ int __retres1 ;
 786
 787  {
 788  if (t9_pc == 1) {
 789    if (E_9 == 1) {
 790      __retres1 = 1;
 791      goto return_label;
 792    } else {
 793
 794    }
 795  } else {
 796
 797  }
 798  __retres1 = 0;
 799  return_label: /* CIL Label */ 
 800  return (__retres1);
 801}
 802}
 803int is_transmit10_triggered(void) 
 804{ int __retres1 ;
 805
 806  {
 807  if (t10_pc == 1) {
 808    if (E_10 == 1) {
 809      __retres1 = 1;
 810      goto return_label;
 811    } else {
 812
 813    }
 814  } else {
 815
 816  }
 817  __retres1 = 0;
 818  return_label: /* CIL Label */ 
 819  return (__retres1);
 820}
 821}
 822int is_transmit11_triggered(void) 
 823{ int __retres1 ;
 824
 825  {
 826  if (t11_pc == 1) {
 827    if (E_11 == 1) {
 828      __retres1 = 1;
 829      goto return_label;
 830    } else {
 831
 832    }
 833  } else {
 834
 835  }
 836  __retres1 = 0;
 837  return_label: /* CIL Label */ 
 838  return (__retres1);
 839}
 840}
 841int is_transmit12_triggered(void) 
 842{ int __retres1 ;
 843
 844  {
 845  if (t12_pc == 1) {
 846    if (E_12 == 1) {
 847      __retres1 = 1;
 848      goto return_label;
 849    } else {
 850
 851    }
 852  } else {
 853
 854  }
 855  __retres1 = 0;
 856  return_label: /* CIL Label */ 
 857  return (__retres1);
 858}
 859}
 860int is_transmit13_triggered(void) 
 861{ int __retres1 ;
 862
 863  {
 864  if (t13_pc == 1) {
 865    if (E_13 == 1) {
 866      __retres1 = 1;
 867      goto return_label;
 868    } else {
 869
 870    }
 871  } else {
 872
 873  }
 874  __retres1 = 0;
 875  return_label: /* CIL Label */ 
 876  return (__retres1);
 877}
 878}
 879void update_channels(void) 
 880{ 
 881
 882  {
 883
 884  return;
 885}
 886}
 887void init_threads(void) 
 888{ 
 889
 890  {
 891  if (m_i == 1) {
 892    m_st = 0;
 893  } else {
 894    m_st = 2;
 895  }
 896  if (t1_i == 1) {
 897    t1_st = 0;
 898  } else {
 899    t1_st = 2;
 900  }
 901  if (t2_i == 1) {
 902    t2_st = 0;
 903  } else {
 904    t2_st = 2;
 905  }
 906  if (t3_i == 1) {
 907    t3_st = 0;
 908  } else {
 909    t3_st = 2;
 910  }
 911  if (t4_i == 1) {
 912    t4_st = 0;
 913  } else {
 914    t4_st = 2;
 915  }
 916  if (t5_i == 1) {
 917    t5_st = 0;
 918  } else {
 919    t5_st = 2;
 920  }
 921  if (t6_i == 1) {
 922    t6_st = 0;
 923  } else {
 924    t6_st = 2;
 925  }
 926  if (t7_i == 1) {
 927    t7_st = 0;
 928  } else {
 929    t7_st = 2;
 930  }
 931  if (t8_i == 1) {
 932    t8_st = 0;
 933  } else {
 934    t8_st = 2;
 935  }
 936  if (t9_i == 1) {
 937    t9_st = 0;
 938  } else {
 939    t9_st = 2;
 940  }
 941  if (t10_i == 1) {
 942    t10_st = 0;
 943  } else {
 944    t10_st = 2;
 945  }
 946  if (t11_i == 1) {
 947    t11_st = 0;
 948  } else {
 949    t11_st = 2;
 950  }
 951  if (t12_i == 1) {
 952    t12_st = 0;
 953  } else {
 954    t12_st = 2;
 955  }
 956  if (t13_i == 1) {
 957    t13_st = 0;
 958  } else {
 959    t13_st = 2;
 960  }
 961
 962  return;
 963}
 964}
 965int exists_runnable_thread(void) 
 966{ int __retres1 ;
 967
 968  {
 969  if (m_st == 0) {
 970    __retres1 = 1;
 971    goto return_label;
 972  } else {
 973    if (t1_st == 0) {
 974      __retres1 = 1;
 975      goto return_label;
 976    } else {
 977      if (t2_st == 0) {
 978        __retres1 = 1;
 979        goto return_label;
 980      } else {
 981        if (t3_st == 0) {
 982          __retres1 = 1;
 983          goto return_label;
 984        } else {
 985          if (t4_st == 0) {
 986            __retres1 = 1;
 987            goto return_label;
 988          } else {
 989            if (t5_st == 0) {
 990              __retres1 = 1;
 991              goto return_label;
 992            } else {
 993              if (t6_st == 0) {
 994                __retres1 = 1;
 995                goto return_label;
 996              } else {
 997                if (t7_st == 0) {
 998                  __retres1 = 1;
 999                  goto return_label;
1000                } else {
1001                  if (t8_st == 0) {
1002                    __retres1 = 1;
1003                    goto return_label;
1004                  } else {
1005                    if (t9_st == 0) {
1006                      __retres1 = 1;
1007                      goto return_label;
1008                    } else {
1009                      if (t10_st == 0) {
1010                        __retres1 = 1;
1011                        goto return_label;
1012                      } else {
1013                        if (t11_st == 0) {
1014                          __retres1 = 1;
1015                          goto return_label;
1016                        } else {
1017                          if (t12_st == 0) {
1018                            __retres1 = 1;
1019                            goto return_label;
1020                          } else {
1021                            if (t13_st == 0) {
1022                              __retres1 = 1;
1023                              goto return_label;
1024                            } else {
1025
1026                            }
1027                          }
1028                        }
1029                      }
1030                    }
1031                  }
1032                }
1033              }
1034            }
1035          }
1036        }
1037      }
1038    }
1039  }
1040  __retres1 = 0;
1041  return_label: /* CIL Label */ 
1042  return (__retres1);
1043}
1044}
1045void eval(void) 
1046{// int __VERIFIER_nondet_int()___0 ;
1047  int tmp ;
1048
1049  {
1050  {
1051  while (1) {
1052    while_14_continue: /* CIL Label */ ;
1053    {
1054    tmp = exists_runnable_thread();
1055    }
1056    if (tmp) {
1057
1058    } else {
1059      goto while_14_break;
1060    }
1061    if (m_st == 0) {
1062      int tmp_ndt_1;
1063      tmp_ndt_1 = __VERIFIER_nondet_int();
1064      if (tmp_ndt_1) {
1065        {
1066        m_st = 1;
1067        master();
1068        }
1069      } else {
1070
1071      }
1072    } else {
1073
1074    }
1075    if (t1_st == 0) {
1076      int tmp_ndt_2;
1077      tmp_ndt_2 = __VERIFIER_nondet_int();
1078      if (tmp_ndt_2) {
1079        {
1080        t1_st = 1;
1081        transmit1();
1082        }
1083      } else {
1084
1085      }
1086    } else {
1087
1088    }
1089    if (t2_st == 0) {
1090      int tmp_ndt_3;
1091      tmp_ndt_3 = __VERIFIER_nondet_int();
1092      if (tmp_ndt_3) {
1093        {
1094        t2_st = 1;
1095        transmit2();
1096        }
1097      } else {
1098
1099      }
1100    } else {
1101
1102    }
1103    if (t3_st == 0) {
1104      int tmp_ndt_4;
1105      tmp_ndt_4 = __VERIFIER_nondet_int();
1106      if (tmp_ndt_4) {
1107        {
1108        t3_st = 1;
1109        transmit3();
1110        }
1111      } else {
1112
1113      }
1114    } else {
1115
1116    }
1117    if (t4_st == 0) {
1118      int tmp_ndt_5;
1119      tmp_ndt_5 = __VERIFIER_nondet_int();
1120      if (tmp_ndt_5) {
1121        {
1122        t4_st = 1;
1123        transmit4();
1124        }
1125      } else {
1126
1127      }
1128    } else {
1129
1130    }
1131    if (t5_st == 0) {
1132      int tmp_ndt_6;
1133      tmp_ndt_6 = __VERIFIER_nondet_int();
1134      if (tmp_ndt_6) {
1135        {
1136        t5_st = 1;
1137        transmit5();
1138        }
1139      } else {
1140
1141      }
1142    } else {
1143
1144    }
1145    if (t6_st == 0) {
1146      int tmp_ndt_7;
1147      tmp_ndt_7 = __VERIFIER_nondet_int();
1148      if (tmp_ndt_7) {
1149        {
1150        t6_st = 1;
1151        transmit6();
1152        }
1153      } else {
1154
1155      }
1156    } else {
1157
1158    }
1159    if (t7_st == 0) {
1160      int tmp_ndt_8;
1161      tmp_ndt_8 = __VERIFIER_nondet_int();
1162      if (tmp_ndt_8) {
1163        {
1164        t7_st = 1;
1165        transmit7();
1166        }
1167      } else {
1168
1169      }
1170    } else {
1171
1172    }
1173    if (t8_st == 0) {
1174      int tmp_ndt_9;
1175      tmp_ndt_9 = __VERIFIER_nondet_int();
1176      if (tmp_ndt_9) {
1177        {
1178        t8_st = 1;
1179        transmit8();
1180        }
1181      } else {
1182
1183      }
1184    } else {
1185
1186    }
1187    if (t9_st == 0) {
1188      int tmp_ndt_10;
1189      tmp_ndt_10 = __VERIFIER_nondet_int();
1190      if (tmp_ndt_10) {
1191        {
1192        t9_st = 1;
1193        transmit9();
1194        }
1195      } else {
1196
1197      }
1198    } else {
1199
1200    }
1201    if (t10_st == 0) {
1202      int tmp_ndt_11;
1203      tmp_ndt_11 = __VERIFIER_nondet_int();
1204      if (tmp_ndt_11) {
1205        {
1206        t10_st = 1;
1207        transmit10();
1208        }
1209      } else {
1210
1211      }
1212    } else {
1213
1214    }
1215    if (t11_st == 0) {
1216      int tmp_ndt_12;
1217      tmp_ndt_12 = __VERIFIER_nondet_int();
1218      if (tmp_ndt_12) {
1219        {
1220        t11_st = 1;
1221        transmit11();
1222        }
1223      } else {
1224
1225      }
1226    } else {
1227
1228    }
1229    if (t12_st == 0) {
1230      int tmp_ndt_13;
1231      tmp_ndt_13 = __VERIFIER_nondet_int();
1232      if (tmp_ndt_13) {
1233        {
1234        t12_st = 1;
1235        transmit12();
1236        }
1237      } else {
1238
1239      }
1240    } else {
1241
1242    }
1243    if (t13_st == 0) {
1244      int tmp_ndt_14;
1245      tmp_ndt_14 = __VERIFIER_nondet_int();
1246      if (tmp_ndt_14) {
1247        {
1248        t13_st = 1;
1249        transmit13();
1250        }
1251      } else {
1252
1253      }
1254    } else {
1255
1256    }
1257  }
1258  while_14_break: /* CIL Label */ ;
1259  }
1260
1261  return;
1262}
1263}
1264void fire_delta_events(void) 
1265{ 
1266
1267  {
1268  if (M_E == 0) {
1269    M_E = 1;
1270  } else {
1271
1272  }
1273  if (T1_E == 0) {
1274    T1_E = 1;
1275  } else {
1276
1277  }
1278  if (T2_E == 0) {
1279    T2_E = 1;
1280  } else {
1281
1282  }
1283  if (T3_E == 0) {
1284    T3_E = 1;
1285  } else {
1286
1287  }
1288  if (T4_E == 0) {
1289    T4_E = 1;
1290  } else {
1291
1292  }
1293  if (T5_E == 0) {
1294    T5_E = 1;
1295  } else {
1296
1297  }
1298  if (T6_E == 0) {
1299    T6_E = 1;
1300  } else {
1301
1302  }
1303  if (T7_E == 0) {
1304    T7_E = 1;
1305  } else {
1306
1307  }
1308  if (T8_E == 0) {
1309    T8_E = 1;
1310  } else {
1311
1312  }
1313  if (T9_E == 0) {
1314    T9_E = 1;
1315  } else {
1316
1317  }
1318  if (T10_E == 0) {
1319    T10_E = 1;
1320  } else {
1321
1322  }
1323  if (T11_E == 0) {
1324    T11_E = 1;
1325  } else {
1326
1327  }
1328  if (T12_E == 0) {
1329    T12_E = 1;
1330  } else {
1331
1332  }
1333  if (T13_E == 0) {
1334    T13_E = 1;
1335  } else {
1336
1337  }
1338  if (E_M == 0) {
1339    E_M = 1;
1340  } else {
1341
1342  }
1343  if (E_1 == 0) {
1344    E_1 = 1;
1345  } else {
1346
1347  }
1348  if (E_2 == 0) {
1349    E_2 = 1;
1350  } else {
1351
1352  }
1353  if (E_3 == 0) {
1354    E_3 = 1;
1355  } else {
1356
1357  }
1358  if (E_4 == 0) {
1359    E_4 = 1;
1360  } else {
1361
1362  }
1363  if (E_5 == 0) {
1364    E_5 = 1;
1365  } else {
1366
1367  }
1368  if (E_6 == 0) {
1369    E_6 = 1;
1370  } else {
1371
1372  }
1373  if (E_7 == 0) {
1374    E_7 = 1;
1375  } else {
1376
1377  }
1378  if (E_8 == 0) {
1379    E_8 = 1;
1380  } else {
1381
1382  }
1383  if (E_9 == 0) {
1384    E_9 = 1;
1385  } else {
1386
1387  }
1388  if (E_10 == 0) {
1389    E_10 = 1;
1390  } else {
1391
1392  }
1393  if (E_11 == 0) {
1394    E_11 = 1;
1395  } else {
1396
1397  }
1398  if (E_12 == 0) {
1399    E_12 = 1;
1400  } else {
1401
1402  }
1403  if (E_13 == 0) {
1404    E_13 = 1;
1405  } else {
1406
1407  }
1408
1409  return;
1410}
1411}
1412void reset_delta_events(void) 
1413{ 
1414
1415  {
1416  if (M_E == 1) {
1417    M_E = 2;
1418  } else {
1419
1420  }
1421  if (T1_E == 1) {
1422    T1_E = 2;
1423  } else {
1424
1425  }
1426  if (T2_E == 1) {
1427    T2_E = 2;
1428  } else {
1429
1430  }
1431  if (T3_E == 1) {
1432    T3_E = 2;
1433  } else {
1434
1435  }
1436  if (T4_E == 1) {
1437    T4_E = 2;
1438  } else {
1439
1440  }
1441  if (T5_E == 1) {
1442    T5_E = 2;
1443  } else {
1444
1445  }
1446  if (T6_E == 1) {
1447    T6_E = 2;
1448  } else {
1449
1450  }
1451  if (T7_E == 1) {
1452    T7_E = 2;
1453  } else {
1454
1455  }
1456  if (T8_E == 1) {
1457    T8_E = 2;
1458  } else {
1459
1460  }
1461  if (T9_E == 1) {
1462    T9_E = 2;
1463  } else {
1464
1465  }
1466  if (T10_E == 1) {
1467    T10_E = 2;
1468  } else {
1469
1470  }
1471  if (T11_E == 1) {
1472    T11_E = 2;
1473  } else {
1474
1475  }
1476  if (T12_E == 1) {
1477    T12_E = 2;
1478  } else {
1479
1480  }
1481  if (T13_E == 1) {
1482    T13_E = 2;
1483  } else {
1484
1485  }
1486  if (E_M == 1) {
1487    E_M = 2;
1488  } else {
1489
1490  }
1491  if (E_1 == 1) {
1492    E_1 = 2;
1493  } else {
1494
1495  }
1496  if (E_2 == 1) {
1497    E_2 = 2;
1498  } else {
1499
1500  }
1501  if (E_3 == 1) {
1502    E_3 = 2;
1503  } else {
1504
1505  }
1506  if (E_4 == 1) {
1507    E_4 = 2;
1508  } else {
1509
1510  }
1511  if (E_5 == 1) {
1512    E_5 = 2;
1513  } else {
1514
1515  }
1516  if (E_6 == 1) {
1517    E_6 = 2;
1518  } else {
1519
1520  }
1521  if (E_7 == 1) {
1522    E_7 = 2;
1523  } else {
1524
1525  }
1526  if (E_8 == 1) {
1527    E_8 = 2;
1528  } else {
1529
1530  }
1531  if (E_9 == 1) {
1532    E_9 = 2;
1533  } else {
1534
1535  }
1536  if (E_10 == 1) {
1537    E_10 = 2;
1538  } else {
1539
1540  }
1541  if (E_11 == 1) {
1542    E_11 = 2;
1543  } else {
1544
1545  }
1546  if (E_12 == 1) {
1547    E_12 = 2;
1548  } else {
1549
1550  }
1551  if (E_13 == 1) {
1552    E_13 = 2;
1553  } else {
1554
1555  }
1556
1557  return;
1558}
1559}
1560void activate_threads(void) 
1561{ int tmp ;
1562  int tmp___0 ;
1563  int tmp___1 ;
1564  int tmp___2 ;
1565  int tmp___3 ;
1566  int tmp___4 ;
1567  int tmp___5 ;
1568  int tmp___6 ;
1569  int tmp___7 ;
1570  int tmp___8 ;
1571  int tmp___9 ;
1572  int tmp___10 ;
1573  int tmp___11 ;
1574  int tmp___12 ;
1575
1576  {
1577  {
1578  tmp = is_master_triggered();
1579  }
1580  if (tmp) {
1581    m_st = 0;
1582  } else {
1583
1584  }
1585  {
1586  tmp___0 = is_transmit1_triggered();
1587  }
1588  if (tmp___0) {
1589    t1_st = 0;
1590  } else {
1591
1592  }
1593  {
1594  tmp___1 = is_transmit2_triggered();
1595  }
1596  if (tmp___1) {
1597    t2_st = 0;
1598  } else {
1599
1600  }
1601  {
1602  tmp___2 = is_transmit3_triggered();
1603  }
1604  if (tmp___2) {
1605    t3_st = 0;
1606  } else {
1607
1608  }
1609  {
1610  tmp___3 = is_transmit4_triggered();
1611  }
1612  if (tmp___3) {
1613    t4_st = 0;
1614  } else {
1615
1616  }
1617  {
1618  tmp___4 = is_transmit5_triggered();
1619  }
1620  if (tmp___4) {
1621    t5_st = 0;
1622  } else {
1623
1624  }
1625  {
1626  tmp___5 = is_transmit6_triggered();
1627  }
1628  if (tmp___5) {
1629    t6_st = 0;
1630  } else {
1631
1632  }
1633  {
1634  tmp___6 = is_transmit7_triggered();
1635  }
1636  if (tmp___6) {
1637    t7_st = 0;
1638  } else {
1639
1640  }
1641  {
1642  tmp___7 = is_transmit8_triggered();
1643  }
1644  if (tmp___7) {
1645    t8_st = 0;
1646  } else {
1647
1648  }
1649  {
1650  tmp___8 = is_transmit9_triggered();
1651  }
1652  if (tmp___8) {
1653    t9_st = 0;
1654  } else {
1655
1656  }
1657  {
1658  tmp___9 = is_transmit10_triggered();
1659  }
1660  if (tmp___9) {
1661    t10_st = 0;
1662  } else {
1663
1664  }
1665  {
1666  tmp___10 = is_transmit11_triggered();
1667  }
1668  if (tmp___10) {
1669    t11_st = 0;
1670  } else {
1671
1672  }
1673  {
1674  tmp___11 = is_transmit12_triggered();
1675  }
1676  if (tmp___11) {
1677    t12_st = 0;
1678  } else {
1679
1680  }
1681  {
1682  tmp___12 = is_transmit13_triggered();
1683  }
1684  if (tmp___12) {
1685    t13_st = 0;
1686  } else {
1687
1688  }
1689
1690  return;
1691}
1692}
1693void immediate_notify(void) 
1694{ 
1695
1696  {
1697  {
1698  activate_threads();
1699  }
1700
1701  return;
1702}
1703}
1704void fire_time_events(void) 
1705{ 
1706
1707  {
1708  M_E = 1;
1709
1710  return;
1711}
1712}
1713void reset_time_events(void) 
1714{ 
1715
1716  {
1717  if (M_E == 1) {
1718    M_E = 2;
1719  } else {
1720
1721  }
1722  if (T1_E == 1) {
1723    T1_E = 2;
1724  } else {
1725
1726  }
1727  if (T2_E == 1) {
1728    T2_E = 2;
1729  } else {
1730
1731  }
1732  if (T3_E == 1) {
1733    T3_E = 2;
1734  } else {
1735
1736  }
1737  if (T4_E == 1) {
1738    T4_E = 2;
1739  } else {
1740
1741  }
1742  if (T5_E == 1) {
1743    T5_E = 2;
1744  } else {
1745
1746  }
1747  if (T6_E == 1) {
1748    T6_E = 2;
1749  } else {
1750
1751  }
1752  if (T7_E == 1) {
1753    T7_E = 2;
1754  } else {
1755
1756  }
1757  if (T8_E == 1) {
1758    T8_E = 2;
1759  } else {
1760
1761  }
1762  if (T9_E == 1) {
1763    T9_E = 2;
1764  } else {
1765
1766  }
1767  if (T10_E == 1) {
1768    T10_E = 2;
1769  } else {
1770
1771  }
1772  if (T11_E == 1) {
1773    T11_E = 2;
1774  } else {
1775
1776  }
1777  if (T12_E == 1) {
1778    T12_E = 2;
1779  } else {
1780
1781  }
1782  if (T13_E == 1) {
1783    T13_E = 2;
1784  } else {
1785
1786  }
1787  if (E_M == 1) {
1788    E_M = 2;
1789  } else {
1790
1791  }
1792  if (E_1 == 1) {
1793    E_1 = 2;
1794  } else {
1795
1796  }
1797  if (E_2 == 1) {
1798    E_2 = 2;
1799  } else {
1800
1801  }
1802  if (E_3 == 1) {
1803    E_3 = 2;
1804  } else {
1805
1806  }
1807  if (E_4 == 1) {
1808    E_4 = 2;
1809  } else {
1810
1811  }
1812  if (E_5 == 1) {
1813    E_5 = 2;
1814  } else {
1815
1816  }
1817  if (E_6 == 1) {
1818    E_6 = 2;
1819  } else {
1820
1821  }
1822  if (E_7 == 1) {
1823    E_7 = 2;
1824  } else {
1825
1826  }
1827  if (E_8 == 1) {
1828    E_8 = 2;
1829  } else {
1830
1831  }
1832  if (E_9 == 1) {
1833    E_9 = 2;
1834  } else {
1835
1836  }
1837  if (E_10 == 1) {
1838    E_10 = 2;
1839  } else {
1840
1841  }
1842  if (E_11 == 1) {
1843    E_11 = 2;
1844  } else {
1845
1846  }
1847  if (E_12 == 1) {
1848    E_12 = 2;
1849  } else {
1850
1851  }
1852  if (E_13 == 1) {
1853    E_13 = 2;
1854  } else {
1855
1856  }
1857
1858  return;
1859}
1860}
1861void init_model(void) 
1862{ 
1863
1864  {
1865  m_i = 1;
1866  t1_i = 1;
1867  t2_i = 1;
1868  t3_i = 1;
1869  t4_i = 1;
1870  t5_i = 1;
1871  t6_i = 1;
1872  t7_i = 1;
1873  t8_i = 1;
1874  t9_i = 1;
1875  t10_i = 1;
1876  t11_i = 1;
1877  t12_i = 1;
1878  t13_i = 1;
1879
1880  return;
1881}
1882}
1883int stop_simulation(void) 
1884{ int tmp ;
1885  int __retres2 ;
1886
1887  {
1888  {
1889  tmp = exists_runnable_thread();
1890  }
1891  if (tmp) {
1892    __retres2 = 0;
1893    goto return_label;
1894  } else {
1895
1896  }
1897  __retres2 = 1;
1898  return_label: /* CIL Label */ 
1899  return (__retres2);
1900}
1901}
1902void start_simulation(void) 
1903{ int kernel_st ;
1904  int tmp ;
1905  int tmp___0 ;
1906
1907  {
1908  {
1909  kernel_st = 0;
1910  update_channels();
1911  init_threads();
1912  fire_delta_events();
1913  activate_threads();
1914  reset_delta_events();
1915  }
1916  {
1917  while (1) {
1918    while_15_continue: /* CIL Label */ ;
1919    {
1920    kernel_st = 1;
1921    eval();
1922    }
1923    {
1924    kernel_st = 2;
1925    update_channels();
1926    }
1927    {
1928    kernel_st = 3;
1929    fire_delta_events();
1930    activate_threads();
1931    reset_delta_events();
1932    }
1933    {
1934    tmp = exists_runnable_thread();
1935    }
1936    if (tmp == 0) {
1937      {
1938      kernel_st = 4;
1939      fire_time_events();
1940      activate_threads();
1941      reset_time_events();
1942      }
1943    } else {
1944
1945    }
1946    {
1947    tmp___0 = stop_simulation();
1948    }
1949    if (tmp___0) {
1950      goto while_15_break;
1951    } else {
1952
1953    }
1954  }
1955  while_15_break: /* CIL Label */ ;
1956  }
1957
1958  return;
1959}
1960}
1961int main(void) 
1962{ int __retres1 ;
1963
1964  {
1965  {
1966  init_model();
1967  start_simulation();
1968  }
1969  __retres1 = 0;
1970  return (__retres1);
1971}
1972}
↑