Showing error 264

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

Source: 

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