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