Showing error 284

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