1extern int __VERIFIER_nondet_int();
2void error(void)
3{
4 {
5 goto ERROR;
6 ERROR: ;
7 return;
8}
9}
10int m_run_st ;
11int m_run_i ;
12int m_run_pc ;
13int s_memory0 ;
14int s_run_st ;
15int s_run_i ;
16int s_run_pc ;
17int c_m_lock ;
18int c_m_ev ;
19int c_req_type ;
20int c_req_a ;
21int c_req_d ;
22int c_rsp_type ;
23int c_rsp_status ;
24int c_rsp_d ;
25int c_empty_req ;
26int c_empty_rsp ;
27int c_read_req_ev ;
28int c_write_req_ev ;
29int c_read_rsp_ev ;
30int c_write_rsp_ev ;
31static int d_t ;
32static int a_t ;
33static int req_t_type ;
34static int req_t_a ;
35static int req_t_d ;
36static int rsp_t_type ;
37static int rsp_t_status ;
38static int rsp_t_d ;
39static int req_tt_type ;
40static int req_tt_a ;
41static int req_tt_d ;
42static int rsp_tt_type ;
43static int rsp_tt_status ;
44static int rsp_tt_d ;
45int s_memory_read(int i)
46{
47 int x;
48 if (i==0)
49 x = s_memory0;
50 else
51 error();
52 return (x);
53}
54void s_memory_write(int i, int v)
55{
56 if (i==0)
57 s_memory0 = v;
58 else
59 error();
60 return;
61}
62void m_run(void)
63{ int d ;
64 int a ;
65 int req_type ;
66 int req_a ;
67 int req_d ;
68 int rsp_type ;
69 int rsp_status ;
70 int rsp_d ;
71 int req_type___0 ;
72 int req_a___0 ;
73 int req_d___0 ;
74 int rsp_type___0 ;
75 int rsp_status___0 ;
76 int rsp_d___0 ;
77 {
78 if ((int )m_run_pc == 0) {
79 goto L_MASTER_RUN_ENTRY;
80 } else {
81 if ((int )m_run_pc == 1) {
82 goto L_MASTER_RUN_MUTEX;
83 } else {
84 if ((int )m_run_pc == 2) {
85 goto L_MASTER_RUN_PUT;
86 } else {
87 if ((int )m_run_pc == 3) {
88 goto L_MASTER_RUN_GET;
89 } else {
90 if ((int )m_run_pc == 4) {
91 goto L_MASTER_RUN_MUTEX2;
92 } else {
93 if ((int )m_run_pc == 5) {
94 goto L_MASTER_RUN_PUT2;
95 } else {
96 if ((int )m_run_pc == 6) {
97 goto L_MASTER_RUN_GET2;
98 } else {
99 }
100 }
101 }
102 }
103 }
104 }
105 }
106 L_MASTER_RUN_ENTRY:
107 a = 0;
108 {
109 while (1) {
110 while_0_continue: ;
111 if (a < 1) {
112 } else {
113 goto while_0_break;
114 }
115 req_type = 1;
116 req_a = a;
117 req_d = a + 50;
118 {
119 while (1) {
120 while_1_continue: ;
121 if (c_m_lock == 1) {
122 } else {
123 goto while_1_break;
124 }
125 m_run_st = 2;
126 m_run_pc = 1;
127 req_t_type = req_type;
128 req_t_a = req_a;
129 req_t_d = req_d;
130 rsp_t_type = rsp_type;
131 rsp_t_status = rsp_status;
132 rsp_t_d = rsp_d;
133 d_t = d;
134 a_t = a;
135 goto return_label;
136 L_MASTER_RUN_MUTEX:
137 req_type = req_t_type;
138 req_a = req_t_a;
139 req_d = req_t_d;
140 rsp_type = rsp_t_type;
141 rsp_status = rsp_t_status;
142 rsp_d = rsp_t_d;
143 d = d_t;
144 a = a_t;
145 }
146 while_1_break: ;
147 }
148 c_m_lock = 1;
149 {
150 while (1) {
151 while_2_continue: ;
152 if ((int )c_empty_req == 0) {
153 } else {
154 goto while_2_break;
155 }
156 m_run_st = 2;
157 m_run_pc = 2;
158 req_t_type = req_type;
159 req_t_a = req_a;
160 req_t_d = req_d;
161 rsp_t_type = rsp_type;
162 rsp_t_status = rsp_status;
163 rsp_t_d = rsp_d;
164 d_t = d;
165 a_t = a;
166 goto return_label;
167 L_MASTER_RUN_PUT:
168 req_type = req_t_type;
169 req_a = req_t_a;
170 req_d = req_t_d;
171 rsp_type = rsp_t_type;
172 rsp_status = rsp_t_status;
173 rsp_d = rsp_t_d;
174 a = a_t;
175 d = d_t;
176 }
177 while_2_break: ;
178 }
179 c_req_type = req_type;
180 c_req_a = req_a;
181 c_req_d = req_d;
182 c_empty_req = 0;
183 c_write_req_ev = 1;
184 if ((int )m_run_pc == 1) {
185 if ((int )c_m_ev == 1) {
186 m_run_st = 0;
187 } else {
188 goto _L___3;
189 }
190 } else {
191 _L___3:
192 if ((int )m_run_pc == 2) {
193 if ((int )c_read_req_ev == 1) {
194 m_run_st = 0;
195 } else {
196 goto _L___2;
197 }
198 } else {
199 _L___2:
200 if ((int )m_run_pc == 3) {
201 if ((int )c_write_rsp_ev == 1) {
202 m_run_st = 0;
203 } else {
204 goto _L___1;
205 }
206 } else {
207 _L___1:
208 if ((int )m_run_pc == 4) {
209 if ((int )c_m_ev == 1) {
210 m_run_st = 0;
211 } else {
212 goto _L___0;
213 }
214 } else {
215 _L___0:
216 if ((int )m_run_pc == 5) {
217 if ((int )c_read_req_ev == 1) {
218 m_run_st = 0;
219 } else {
220 goto _L;
221 }
222 } else {
223 _L:
224 if ((int )m_run_pc == 6) {
225 if ((int )c_write_rsp_ev == 1) {
226 m_run_st = 0;
227 } else {
228 }
229 } else {
230 }
231 }
232 }
233 }
234 }
235 }
236 if ((int )s_run_pc == 2) {
237 if ((int )c_write_req_ev == 1) {
238 s_run_st = 0;
239 } else {
240 goto _L___4;
241 }
242 } else {
243 _L___4:
244 if ((int )s_run_pc == 1) {
245 if ((int )c_read_rsp_ev == 1) {
246 s_run_st = 0;
247 } else {
248 }
249 } else {
250 }
251 }
252 c_write_req_ev = 2;
253 {
254 while (1) {
255 while_3_continue: ;
256 if ((int )c_empty_rsp == 1) {
257 } else {
258 goto while_3_break;
259 }
260 m_run_st = 2;
261 m_run_pc = 3;
262 req_t_type = req_type;
263 req_t_a = req_a;
264 req_t_d = req_d;
265 rsp_t_type = rsp_type;
266 rsp_t_status = rsp_status;
267 rsp_t_d = rsp_d;
268 d_t = d;
269 a_t = a;
270 goto return_label;
271 L_MASTER_RUN_GET:
272 req_type = req_t_type;
273 req_a = req_t_a;
274 req_d = req_t_d;
275 rsp_type = rsp_t_type;
276 rsp_status = rsp_t_status;
277 rsp_d = rsp_t_d;
278 d = d_t;
279 a = a_t;
280 }
281 while_3_break: ;
282 }
283 rsp_type = c_rsp_type;
284 rsp_status = c_rsp_status;
285 rsp_d = c_rsp_d;
286 c_empty_rsp = 1;
287 c_read_rsp_ev = 1;
288 if ((int )m_run_pc == 1) {
289 if ((int )c_m_ev == 1) {
290 m_run_st = 0;
291 } else {
292 goto _L___9;
293 }
294 } else {
295 _L___9:
296 if ((int )m_run_pc == 2) {
297 if ((int )c_read_req_ev == 1) {
298 m_run_st = 0;
299 } else {
300 goto _L___8;
301 }
302 } else {
303 _L___8:
304 if ((int )m_run_pc == 3) {
305 if ((int )c_write_rsp_ev == 1) {
306 m_run_st = 0;
307 } else {
308 goto _L___7;
309 }
310 } else {
311 _L___7:
312 if ((int )m_run_pc == 4) {
313 if ((int )c_m_ev == 1) {
314 m_run_st = 0;
315 } else {
316 goto _L___6;
317 }
318 } else {
319 _L___6:
320 if ((int )m_run_pc == 5) {
321 if ((int )c_read_req_ev == 1) {
322 m_run_st = 0;
323 } else {
324 goto _L___5;
325 }
326 } else {
327 _L___5:
328 if ((int )m_run_pc == 6) {
329 if ((int )c_write_rsp_ev == 1) {
330 m_run_st = 0;
331 } else {
332 }
333 } else {
334 }
335 }
336 }
337 }
338 }
339 }
340 if ((int )s_run_pc == 2) {
341 if ((int )c_write_req_ev == 1) {
342 s_run_st = 0;
343 } else {
344 goto _L___10;
345 }
346 } else {
347 _L___10:
348 if ((int )s_run_pc == 1) {
349 if ((int )c_read_rsp_ev == 1) {
350 s_run_st = 0;
351 } else {
352 }
353 } else {
354 }
355 }
356 c_read_rsp_ev = 2;
357 if (c_m_lock == 0) {
358 {
359 error();
360 }
361 } else {
362 }
363 c_m_lock = 0;
364 c_m_ev = 1;
365 if ((int )m_run_pc == 1) {
366 if ((int )c_m_ev == 1) {
367 m_run_st = 0;
368 } else {
369 goto _L___15;
370 }
371 } else {
372 _L___15:
373 if ((int )m_run_pc == 2) {
374 if ((int )c_read_req_ev == 1) {
375 m_run_st = 0;
376 } else {
377 goto _L___14;
378 }
379 } else {
380 _L___14:
381 if ((int )m_run_pc == 3) {
382 if ((int )c_write_rsp_ev == 1) {
383 m_run_st = 0;
384 } else {
385 goto _L___13;
386 }
387 } else {
388 _L___13:
389 if ((int )m_run_pc == 4) {
390 if ((int )c_m_ev == 1) {
391 m_run_st = 0;
392 } else {
393 goto _L___12;
394 }
395 } else {
396 _L___12:
397 if ((int )m_run_pc == 5) {
398 if ((int )c_read_req_ev == 1) {
399 m_run_st = 0;
400 } else {
401 goto _L___11;
402 }
403 } else {
404 _L___11:
405 if ((int )m_run_pc == 6) {
406 if ((int )c_write_rsp_ev == 1) {
407 m_run_st = 0;
408 } else {
409 }
410 } else {
411 }
412 }
413 }
414 }
415 }
416 }
417 if ((int )s_run_pc == 2) {
418 if ((int )c_write_req_ev == 1) {
419 s_run_st = 0;
420 } else {
421 goto _L___16;
422 }
423 } else {
424 _L___16:
425 if ((int )s_run_pc == 1) {
426 if ((int )c_read_rsp_ev == 1) {
427 s_run_st = 0;
428 } else {
429 }
430 } else {
431 }
432 }
433 c_m_ev = 2;
434 a += 1;
435 }
436 while_0_break: ;
437 }
438 a = 0;
439 {
440 while (1) {
441 while_4_continue: ;
442 if (a < 1) {
443 } else {
444 goto while_4_break;
445 }
446 req_type___0 = 0;
447 req_a___0 = a;
448 {
449 while (1) {
450 while_5_continue: ;
451 if (c_m_lock == 1) {
452 } else {
453 goto while_5_break;
454 }
455 m_run_st = 2;
456 m_run_pc = 4;
457 req_tt_type = req_type___0;
458 req_tt_a = req_a___0;
459 req_tt_d = req_d___0;
460 rsp_tt_type = rsp_type___0;
461 rsp_tt_status = rsp_status___0;
462 rsp_tt_d = rsp_d___0;
463 d_t = d;
464 a_t = a;
465 goto return_label;
466 L_MASTER_RUN_MUTEX2:
467 req_type___0 = req_tt_type;
468 req_a___0 = req_tt_a;
469 req_d___0 = req_tt_d;
470 rsp_type___0 = rsp_tt_type;
471 rsp_status___0 = rsp_tt_status;
472 rsp_d___0 = rsp_tt_d;
473 d = d_t;
474 a = a_t;
475 }
476 while_5_break: ;
477 }
478 c_m_lock = 1;
479 {
480 while (1) {
481 while_6_continue: ;
482 if ((int )c_empty_req == 0) {
483 } else {
484 goto while_6_break;
485 }
486 m_run_st = 2;
487 m_run_pc = 5;
488 req_tt_type = req_type___0;
489 req_tt_a = req_a___0;
490 req_tt_d = req_d___0;
491 rsp_tt_type = rsp_type___0;
492 rsp_tt_status = rsp_status___0;
493 rsp_tt_d = rsp_d___0;
494 d_t = d;
495 a_t = a;
496 goto return_label;
497 L_MASTER_RUN_PUT2:
498 req_type___0 = req_tt_type;
499 req_a___0 = req_tt_a;
500 req_d___0 = req_tt_d;
501 rsp_type___0 = rsp_tt_type;
502 rsp_status___0 = rsp_tt_status;
503 rsp_d___0 = rsp_tt_d;
504 d = d_t;
505 a = a_t;
506 }
507 while_6_break: ;
508 }
509 c_req_type = req_type___0;
510 c_req_a = req_a___0;
511 c_req_d = req_d___0;
512 c_empty_req = 0;
513 c_write_req_ev = 1;
514 if ((int )m_run_pc == 1) {
515 if ((int )c_m_ev == 1) {
516 m_run_st = 0;
517 } else {
518 goto _L___21;
519 }
520 } else {
521 _L___21:
522 if ((int )m_run_pc == 2) {
523 if ((int )c_read_req_ev == 1) {
524 m_run_st = 0;
525 } else {
526 goto _L___20;
527 }
528 } else {
529 _L___20:
530 if ((int )m_run_pc == 3) {
531 if ((int )c_write_rsp_ev == 1) {
532 m_run_st = 0;
533 } else {
534 goto _L___19;
535 }
536 } else {
537 _L___19:
538 if ((int )m_run_pc == 4) {
539 if ((int )c_m_ev == 1) {
540 m_run_st = 0;
541 } else {
542 goto _L___18;
543 }
544 } else {
545 _L___18:
546 if ((int )m_run_pc == 5) {
547 if ((int )c_read_req_ev == 1) {
548 m_run_st = 0;
549 } else {
550 goto _L___17;
551 }
552 } else {
553 _L___17:
554 if ((int )m_run_pc == 6) {
555 if ((int )c_write_rsp_ev == 1) {
556 m_run_st = 0;
557 } else {
558 }
559 } else {
560 }
561 }
562 }
563 }
564 }
565 }
566 if ((int )s_run_pc == 2) {
567 if ((int )c_write_req_ev == 1) {
568 s_run_st = 0;
569 } else {
570 goto _L___22;
571 }
572 } else {
573 _L___22:
574 if ((int )s_run_pc == 1) {
575 if ((int )c_read_rsp_ev == 1) {
576 s_run_st = 0;
577 } else {
578 }
579 } else {
580 }
581 }
582 c_write_req_ev = 2;
583 {
584 while (1) {
585 while_7_continue: ;
586 if ((int )c_empty_rsp == 1) {
587 } else {
588 goto while_7_break;
589 }
590 m_run_st = 2;
591 m_run_pc = 6;
592 req_tt_type = req_type___0;
593 req_tt_a = req_a___0;
594 req_tt_d = req_d___0;
595 rsp_tt_type = rsp_type___0;
596 rsp_tt_status = rsp_status___0;
597 rsp_tt_d = rsp_d___0;
598 d_t = d;
599 a_t = a;
600 goto return_label;
601 L_MASTER_RUN_GET2:
602 req_type___0 = req_tt_type;
603 req_a___0 = req_tt_a;
604 req_d___0 = req_tt_d;
605 rsp_type___0 = rsp_tt_type;
606 rsp_status___0 = rsp_tt_status;
607 rsp_d___0 = rsp_tt_d;
608 d = d_t;
609 a = a_t;
610 }
611 while_7_break: ;
612 }
613 rsp_type___0 = c_rsp_type;
614 rsp_status___0 = c_rsp_status;
615 rsp_d___0 = c_rsp_d;
616 c_empty_rsp = 1;
617 c_read_rsp_ev = 1;
618 if ((int )m_run_pc == 1) {
619 if ((int )c_m_ev == 1) {
620 m_run_st = 0;
621 } else {
622 goto _L___27;
623 }
624 } else {
625 _L___27:
626 if ((int )m_run_pc == 2) {
627 if ((int )c_read_req_ev == 1) {
628 m_run_st = 0;
629 } else {
630 goto _L___26;
631 }
632 } else {
633 _L___26:
634 if ((int )m_run_pc == 3) {
635 if ((int )c_write_rsp_ev == 1) {
636 m_run_st = 0;
637 } else {
638 goto _L___25;
639 }
640 } else {
641 _L___25:
642 if ((int )m_run_pc == 4) {
643 if ((int )c_m_ev == 1) {
644 m_run_st = 0;
645 } else {
646 goto _L___24;
647 }
648 } else {
649 _L___24:
650 if ((int )m_run_pc == 5) {
651 if ((int )c_read_req_ev == 1) {
652 m_run_st = 0;
653 } else {
654 goto _L___23;
655 }
656 } else {
657 _L___23:
658 if ((int )m_run_pc == 6) {
659 if ((int )c_write_rsp_ev == 1) {
660 m_run_st = 0;
661 } else {
662 }
663 } else {
664 }
665 }
666 }
667 }
668 }
669 }
670 if ((int )s_run_pc == 2) {
671 if ((int )c_write_req_ev == 1) {
672 s_run_st = 0;
673 } else {
674 goto _L___28;
675 }
676 } else {
677 _L___28:
678 if ((int )s_run_pc == 1) {
679 if ((int )c_read_rsp_ev == 1) {
680 s_run_st = 0;
681 } else {
682 }
683 } else {
684 }
685 }
686 c_read_rsp_ev = 2;
687 if (c_m_lock == 0) {
688 {
689 error();
690 }
691 } else {
692 }
693 c_m_lock = 0;
694 c_m_ev = 1;
695 if ((int )m_run_pc == 1) {
696 if ((int )c_m_ev == 1) {
697 m_run_st = 0;
698 } else {
699 goto _L___33;
700 }
701 } else {
702 _L___33:
703 if ((int )m_run_pc == 2) {
704 if ((int )c_read_req_ev == 1) {
705 m_run_st = 0;
706 } else {
707 goto _L___32;
708 }
709 } else {
710 _L___32:
711 if ((int )m_run_pc == 3) {
712 if ((int )c_write_rsp_ev == 1) {
713 m_run_st = 0;
714 } else {
715 goto _L___31;
716 }
717 } else {
718 _L___31:
719 if ((int )m_run_pc == 4) {
720 if ((int )c_m_ev == 1) {
721 m_run_st = 0;
722 } else {
723 goto _L___30;
724 }
725 } else {
726 _L___30:
727 if ((int )m_run_pc == 5) {
728 if ((int )c_read_req_ev == 1) {
729 m_run_st = 0;
730 } else {
731 goto _L___29;
732 }
733 } else {
734 _L___29:
735 if ((int )m_run_pc == 6) {
736 if ((int )c_write_rsp_ev == 1) {
737 m_run_st = 0;
738 } else {
739 }
740 } else {
741 }
742 }
743 }
744 }
745 }
746 }
747 if ((int )s_run_pc == 2) {
748 if ((int )c_write_req_ev == 1) {
749 s_run_st = 0;
750 } else {
751 goto _L___34;
752 }
753 } else {
754 _L___34:
755 if ((int )s_run_pc == 1) {
756 if ((int )c_read_rsp_ev == 1) {
757 s_run_st = 0;
758 } else {
759 }
760 } else {
761 }
762 }
763 c_m_ev = 2;
764 if (! (req_a___0 + 50 == rsp_d___0)) {
765 {
766 error();
767 }
768 } else {
769 }
770 a += 1;
771 }
772 while_4_break: ;
773 }
774 return_label:
775 return;
776}
777}
778static int req_t_type___0 ;
779static int req_t_a___0 ;
780static int req_t_d___0 ;
781static int rsp_t_type___0 ;
782static int rsp_t_status___0 ;
783static int rsp_t_d___0 ;
784void s_run(void)
785{ int req_type ;
786 int req_a ;
787 int req_d ;
788 int rsp_type ;
789 int rsp_status ;
790 int rsp_d ;
791 int dummy ;
792 {
793 if ((int )s_run_pc == 0) {
794 goto L_SLAVE_RUN_ENTRY;
795 } else {
796 if ((int )s_run_pc == 1) {
797 goto L_SLAVE_RUN_PUT;
798 } else {
799 if ((int )s_run_pc == 2) {
800 goto L_SLAVE_RUN_GET;
801 } else {
802 }
803 }
804 }
805 L_SLAVE_RUN_ENTRY:
806 {
807 while (1) {
808 while_8_continue: ;
809 {
810 while (1) {
811 while_9_continue: ;
812 if ((int )c_empty_req == 1) {
813 } else {
814 goto while_9_break;
815 }
816 s_run_st = 2;
817 s_run_pc = 2;
818 req_t_type___0 = req_type;
819 req_t_a___0 = req_a;
820 req_t_d___0 = req_d;
821 rsp_t_type___0 = rsp_type;
822 rsp_t_status___0 = rsp_status;
823 rsp_t_d___0 = rsp_d;
824 goto return_label;
825 L_SLAVE_RUN_GET:
826 req_type = req_t_type___0;
827 req_a = req_t_a___0;
828 req_d = req_t_d___0;
829 rsp_type = rsp_t_type___0;
830 rsp_status = rsp_t_status___0;
831 rsp_d = rsp_t_d___0;
832 }
833 while_9_break: ;
834 }
835 req_type = c_req_type;
836 req_a = c_req_a;
837 req_d = c_req_d;
838 c_empty_req = 1;
839 c_read_req_ev = 1;
840 if ((int )m_run_pc == 1) {
841 if ((int )c_m_ev == 1) {
842 m_run_st = 0;
843 } else {
844 goto _L___3;
845 }
846 } else {
847 _L___3:
848 if ((int )m_run_pc == 2) {
849 if ((int )c_read_req_ev == 1) {
850 m_run_st = 0;
851 } else {
852 goto _L___2;
853 }
854 } else {
855 _L___2:
856 if ((int )m_run_pc == 3) {
857 if ((int )c_write_rsp_ev == 1) {
858 m_run_st = 0;
859 } else {
860 goto _L___1;
861 }
862 } else {
863 _L___1:
864 if ((int )m_run_pc == 4) {
865 if ((int )c_m_ev == 1) {
866 m_run_st = 0;
867 } else {
868 goto _L___0;
869 }
870 } else {
871 _L___0:
872 if ((int )m_run_pc == 5) {
873 if ((int )c_read_req_ev == 1) {
874 m_run_st = 0;
875 } else {
876 goto _L;
877 }
878 } else {
879 _L:
880 if ((int )m_run_pc == 6) {
881 if ((int )c_write_rsp_ev == 1) {
882 m_run_st = 0;
883 } else {
884 }
885 } else {
886 }
887 }
888 }
889 }
890 }
891 }
892 if ((int )s_run_pc == 2) {
893 if ((int )c_write_req_ev == 1) {
894 s_run_st = 0;
895 } else {
896 goto _L___4;
897 }
898 } else {
899 _L___4:
900 if ((int )s_run_pc == 1) {
901 if ((int )c_read_rsp_ev == 1) {
902 s_run_st = 0;
903 } else {
904 }
905 } else {
906 }
907 }
908 c_read_req_ev = 2;
909 rsp_type = req_type;
910 if ((int )req_type == 0) {
911 rsp_d = s_memory_read(req_a);
912 rsp_status = 1;
913 } else {
914 if ((int )req_type == 1) {
915 s_memory_write(req_a,req_d);
916 rsp_status = 1;
917 } else {
918 rsp_status = 0;
919 }
920 }
921 {
922 while (1) {
923 while_10_continue: ;
924 if ((int )c_empty_rsp == 0) {
925 } else {
926 goto while_10_break;
927 }
928 s_run_st = 2;
929 s_run_pc = 1;
930 req_t_type___0 = req_type;
931 req_t_a___0 = req_a;
932 req_t_d___0 = req_d;
933 rsp_t_type___0 = rsp_type;
934 rsp_t_status___0 = rsp_status;
935 rsp_t_d___0 = rsp_d;
936 goto return_label;
937 L_SLAVE_RUN_PUT:
938 req_type = req_t_type___0;
939 req_a = req_t_a___0;
940 req_d = req_t_d___0;
941 rsp_type = rsp_t_type___0;
942 rsp_status = rsp_t_status___0;
943 rsp_d = rsp_t_d___0;
944 }
945 while_10_break: ;
946 }
947 c_rsp_type = rsp_type;
948 c_rsp_status = rsp_status;
949 c_rsp_d = rsp_d;
950 c_empty_rsp = 0;
951 c_write_rsp_ev = 1;
952 if ((int )m_run_pc == 1) {
953 if ((int )c_m_ev == 1) {
954 m_run_st = 0;
955 } else {
956 goto _L___9;
957 }
958 } else {
959 _L___9:
960 if ((int )m_run_pc == 2) {
961 if ((int )c_read_req_ev == 1) {
962 m_run_st = 0;
963 } else {
964 goto _L___8;
965 }
966 } else {
967 _L___8:
968 if ((int )m_run_pc == 3) {
969 if ((int )c_write_rsp_ev == 1) {
970 m_run_st = 0;
971 } else {
972 goto _L___7;
973 }
974 } else {
975 _L___7:
976 if ((int )m_run_pc == 4) {
977 if ((int )c_m_ev == 1) {
978 m_run_st = 0;
979 } else {
980 goto _L___6;
981 }
982 } else {
983 _L___6:
984 if ((int )m_run_pc == 5) {
985 if ((int )c_read_req_ev == 1) {
986 m_run_st = 0;
987 } else {
988 goto _L___5;
989 }
990 } else {
991 _L___5:
992 if ((int )m_run_pc == 6) {
993 if ((int )c_write_rsp_ev == 1) {
994 m_run_st = 0;
995 } else {
996 }
997 } else {
998 }
999 }
1000 }
1001 }
1002 }
1003 }
1004 if ((int )s_run_pc == 2) {
1005 if ((int )c_write_req_ev == 1) {
1006 s_run_st = 0;
1007 } else {
1008 goto _L___10;
1009 }
1010 } else {
1011 _L___10:
1012 if ((int )s_run_pc == 1) {
1013 if ((int )c_read_rsp_ev == 1) {
1014 s_run_st = 0;
1015 } else {
1016 }
1017 } else {
1018 }
1019 }
1020 c_write_rsp_ev = 2;
1021 }
1022 while_8_break: ;
1023 }
1024 return_label:
1025 return;
1026}
1027}
1028void eval(void)
1029{ int tmp ;
1030 int tmp___0 ;
1031 {
1032 {
1033 while (1) {
1034 while_11_continue: ;
1035 if ((int )m_run_st == 0) {
1036 } else {
1037 if ((int )s_run_st == 0) {
1038 } else {
1039 goto while_11_break;
1040 }
1041 }
1042 if ((int )m_run_st == 0) {
1043 {
1044 tmp = __VERIFIER_nondet_int();
1045 }
1046 if (tmp) {
1047 {
1048 m_run_st = 1;
1049 m_run();
1050 }
1051 } else {
1052 }
1053 } else {
1054 }
1055 if ((int )s_run_st == 0) {
1056 {
1057 tmp___0 = __VERIFIER_nondet_int();
1058 }
1059 if (tmp___0) {
1060 {
1061 s_run_st = 1;
1062 s_run();
1063 }
1064 } else {
1065 }
1066 } else {
1067 }
1068 }
1069 while_11_break: ;
1070 }
1071 return;
1072}
1073}
1074void start_simulation(void)
1075{ int kernel_st ;
1076 {
1077 kernel_st = 0;
1078 if ((int )m_run_i == 1) {
1079 m_run_st = 0;
1080 } else {
1081 m_run_st = 2;
1082 }
1083 if ((int )s_run_i == 1) {
1084 s_run_st = 0;
1085 } else {
1086 s_run_st = 2;
1087 }
1088 if ((int )m_run_pc == 1) {
1089 if ((int )c_m_ev == 1) {
1090 m_run_st = 0;
1091 } else {
1092 goto _L___3;
1093 }
1094 } else {
1095 _L___3:
1096 if ((int )m_run_pc == 2) {
1097 if ((int )c_read_req_ev == 1) {
1098 m_run_st = 0;
1099 } else {
1100 goto _L___2;
1101 }
1102 } else {
1103 _L___2:
1104 if ((int )m_run_pc == 3) {
1105 if ((int )c_write_rsp_ev == 1) {
1106 m_run_st = 0;
1107 } else {
1108 goto _L___1;
1109 }
1110 } else {
1111 _L___1:
1112 if ((int )m_run_pc == 4) {
1113 if ((int )c_m_ev == 1) {
1114 m_run_st = 0;
1115 } else {
1116 goto _L___0;
1117 }
1118 } else {
1119 _L___0:
1120 if ((int )m_run_pc == 5) {
1121 if ((int )c_read_req_ev == 1) {
1122 m_run_st = 0;
1123 } else {
1124 goto _L;
1125 }
1126 } else {
1127 _L:
1128 if ((int )m_run_pc == 6) {
1129 if ((int )c_write_rsp_ev == 1) {
1130 m_run_st = 0;
1131 } else {
1132 }
1133 } else {
1134 }
1135 }
1136 }
1137 }
1138 }
1139 }
1140 if ((int )s_run_pc == 2) {
1141 if ((int )c_write_req_ev == 1) {
1142 s_run_st = 0;
1143 } else {
1144 goto _L___4;
1145 }
1146 } else {
1147 _L___4:
1148 if ((int )s_run_pc == 1) {
1149 if ((int )c_read_rsp_ev == 1) {
1150 s_run_st = 0;
1151 } else {
1152 }
1153 } else {
1154 }
1155 }
1156 {
1157 while (1) {
1158 while_12_continue: ;
1159 {
1160 kernel_st = 1;
1161 eval();
1162 }
1163 kernel_st = 2;
1164 kernel_st = 3;
1165 if ((int )m_run_pc == 1) {
1166 if ((int )c_m_ev == 1) {
1167 m_run_st = 0;
1168 } else {
1169 goto _L___9;
1170 }
1171 } else {
1172 _L___9:
1173 if ((int )m_run_pc == 2) {
1174 if ((int )c_read_req_ev == 1) {
1175 m_run_st = 0;
1176 } else {
1177 goto _L___8;
1178 }
1179 } else {
1180 _L___8:
1181 if ((int )m_run_pc == 3) {
1182 if ((int )c_write_rsp_ev == 1) {
1183 m_run_st = 0;
1184 } else {
1185 goto _L___7;
1186 }
1187 } else {
1188 _L___7:
1189 if ((int )m_run_pc == 4) {
1190 if ((int )c_m_ev == 1) {
1191 m_run_st = 0;
1192 } else {
1193 goto _L___6;
1194 }
1195 } else {
1196 _L___6:
1197 if ((int )m_run_pc == 5) {
1198 if ((int )c_read_req_ev == 1) {
1199 m_run_st = 0;
1200 } else {
1201 goto _L___5;
1202 }
1203 } else {
1204 _L___5:
1205 if ((int )m_run_pc == 6) {
1206 if ((int )c_write_rsp_ev == 1) {
1207 m_run_st = 0;
1208 } else {
1209 }
1210 } else {
1211 }
1212 }
1213 }
1214 }
1215 }
1216 }
1217 if ((int )s_run_pc == 2) {
1218 if ((int )c_write_req_ev == 1) {
1219 s_run_st = 0;
1220 } else {
1221 goto _L___10;
1222 }
1223 } else {
1224 _L___10:
1225 if ((int )s_run_pc == 1) {
1226 if ((int )c_read_rsp_ev == 1) {
1227 s_run_st = 0;
1228 } else {
1229 }
1230 } else {
1231 }
1232 }
1233 if ((int )m_run_st == 0) {
1234 } else {
1235 if ((int )s_run_st == 0) {
1236 } else {
1237 goto while_12_break;
1238 }
1239 }
1240 }
1241 while_12_break: ;
1242 }
1243 return;
1244}
1245}
1246int main(void)
1247{ int __retres1 ;
1248 {
1249 {
1250 c_m_lock = 0;
1251 c_m_ev = 2;
1252 m_run_i = 1;
1253 m_run_pc = 0;
1254 s_run_i = 1;
1255 s_run_pc = 0;
1256 c_empty_req = 1;
1257 c_empty_rsp = 1;
1258 c_read_req_ev = 2;
1259 c_write_req_ev = 2;
1260 c_read_rsp_ev = 2;
1261 c_write_rsp_ev = 2;
1262 c_m_lock = 0;
1263 c_m_ev = 2;
1264 start_simulation();
1265 }
1266 __retres1 = 0;
1267 return (__retres1);
1268}
1269}