Showing error 283

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

Source: 

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