Showing error 2312

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

Source: 

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