Showing error 282

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

Source: 

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