Showing error 2336

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.15_unsafe.cil.c
Line in file: 9
Project: SV-COMP 2013
Project version: 2.6.28
Tools: Manual Work
Entered: 2013-01-17 16:57:54 UTC

Source: 

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