digraph "dekker.lsts"
{
margin=0;rankdir=LR;{rank=same;206;58;1;}
1[style=bold];
3[label="3\nscheduler_2"];
5[label="5\nwait_set_b_i_2"];
8[label="8\nwait_set_b_i_2\nscheduler_1"];
11[label="11\nwait_set_b_i_1\nwait_set_b_i_2"];
15[label="15\nwait_set_b_i_1\nwait_set_b_i_2\nscheduler_1"];
20[label="20\nwait_set_b_i_2"];
25[label="25\nwait_set_b_i_2\nscheduler_1"];
32[label="32\nwait_set_b_i_2"];
39[label="39\nwait_set_b_i_2\nscheduler_2"];
_58[label="58\nscheduler_1"];
58[label="58\nscheduler_1"];
84[label="84\nscheduler_1"];
102[label="102\nwait_set_k_1"];
114[label="114\nwait_set_k_1\nscheduler_1"];
143[label="143\nscheduler_1"];
169[label="169\nscheduler_2"];
193[label="193\nscheduler_2"];
219[label="219\nscheduler_1"];
235[label="235\nwait_set_b_i_1"];
252[label="252\nwait_set_b_i_1\nscheduler_1"];
285[label="285\nscheduler_1"];
315[label="315\nscheduler_1"];
340[label="340\nscheduler_1"];
359[label="359\nscheduler_1"];
_206[label=206];
1->3[label="choose_i$i$2"];
3->5[label="desire$i$2"];
5->8[label="choose_i$i$1"];
8->11[label="desire$i$1"];
11->15[label="choose_i$i$1"];
15->20[label="set_b_i$i$1"];
20->25[label="choose_i$i$1"];
25->32[label="read_b_j_false$i$1"];
32->39[label="choose_i$i$2"];
39->48[label="set_b_i$i$2"];
48->_58[label="choose_i$i$1"];
58->72[label="enter$i$1"];
72->84[label="choose_i$i$1"];
84->102[label="exit$i$1"];
102->114[label="choose_i$i$1"];
114->132[label="set_k$i$1$z$1"];
132->143[label="choose_i$i$1"];
143->159[label="clear_b_i_again$i$1"];
159->169[label="choose_i$i$2"];
169->181[label="read_b_j_false$i$2"];
181->193[label="choose_i$i$2"];
193->_206[label="enter$i$2"];
206->219[label="choose_i$i$1"];
219->235[label="desire$i$1"];
235->252[label="choose_i$i$1"];
252->268[label="set_b_i$i$1"];
268->285[label="choose_i$i$1"];
285->300[label="read_b_j_true$i$1"];
300->315[label="choose_i$i$1"];
315->328[label="read_k_eq_j$i$1"];
328->340[label="choose_i$i$1"];
340->352[label="clear_b_i$i$1"];
352->359[label="choose_i$i$1"];
359->352[label="read_k_again_eq_j$i$1"];
}