Showing error 2334

User: Jiri Slaby
Error type: Reachable Error Location
Error type description: A specified error location is reachable in some program path
File location: systemc/transmitter.12_unsafe.cil.c
Line in file: 9
Project: SV-COMP 2013
Project version: 2.6.28
Tools: Manual Work
Entered: 2013-01-17 16:57:54 UTC

Source: 

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