model.prism (0.02 MB)
property.props (0.01 MB)
model.jani (0.25 MB)

Taken from QVBS (January 2026).
The given benchmark (including parameter instantiation and property) has been considered in QComp 2019 and QComp 2020.

Original Prism model and property files have been adapted for compatibility and simplicity:
- Constants: All open constants are now explicitly set within model.prism (no need to set them via command line)
- Properties: The properties only refer to labels and rewards as defined in the model.prism file. No variables or constants are used in the property.
- Formulas: some PRISM formula declarations have been renamed so that their identify does not crash with a label.

// bluetooth model for one node in inquiry scan and one in inquiry
// constants taken from standard
// mxd/gxn/dxp 22/06/04

dtmc

// removed time spent in sleep (turned into one big time transition)
// and combined this with scan (only go to sleep if do not hear anything in scan)
// also numbered frequencies from 1..16 and used extra variable to say what train 
// (i.e. 1..16 train 0 and 17..32 train 1)


// PARAMETERS OF THE RECEIVER
// scan window: time to scan a frequency 11.25ms  [36 slots]
// scan interval: time between scans 0.64 seconds (less than 1.28 so we can have a smaller random choice) [2048 slots]
// phase - time until frequency changes 1.28 seconds (as specified in the standard) [4096 slots]

//----------------------------------------------------------------------------------------------------------------------------
// CONSTANTS (from the standard)
const int phase = 4096; // length of a phase (one frequency for the receiver) [1.28s]
const int maxr = 127; // maximum random delay
const int mrep = 128; //number of times a train is repeated before switching

//----------------------------------------------------------------------------------------------------------------------------
// FORMULAE 

// we combine together scan and sleep when the receiver scans and hears nothing
// the following formula is true in a state if and only if the receiver will hear something if it immediately starts scanning 
// (receiver scans for 32 slots so one loop of a train plus 4 more steps)
formula swap  = (((c=2)|(c=4)|(c=6)|(c=8)|(c=10)|(c=12)|(c=14)|(c=16))); // receiver swaps trains at end of sequence only when c is even
formula swap2  = ((((c=2)|(c=4)|(c=6)|(c=8)|(c=10)|(c=12)|(c=14))) & freq=c+1) | (c=16 & freq=1) | ((((c=1)|(c=3)|(c=5)|(c=7)|(c=9)|(c=11)|(c=13)|(c=15))) & freq!=c+1); // receiver swaps trains when changing frequency set (when receiver sleeps)
formula sleep = (receiver=0 & y1=1); // state where reciever's next time step corresponds to the whole of scan and sleep (scan interval)
formula hear  = (freq1=freq & train1=train & send=1); // when the receiver hears something

formula success = 
	// will see on current set of frequencies and there is time to complete a whole cycle
	((repc)))
	// will see on current set of frequencies and there is not time to complete a whole cycle
	| (rep=mrep & ((send=1 & freq<=f1) | (send>1 & freqc))) 
	// will see on next set of frequencies and at least a whole cycle to to
	| (rep=mrep-1 & c<16 & swap  & ((t1=((freq<=c)?train:1-train) & f1<=c+1) | (t1=((freq<=c)?1-train:train) & f1>c+1)) & ((f1=1 & freq>=15) | (f1=2 & freq=16))) 
	| (rep=mrep-1 & c<16 & !swap & ((t1=((freq<=c)?1-train:train) & f1<=c+1) | (t1=((freq<=c)?train:1-train) & f1>c+1)) & ((f1=1 & freq>=15) | (f1=2 & freq=16)))
	| (rep=mrep-1 & c=16 & (t1=((f1=1)?1-train:train)) & ((f1=1 & freq>=15) | (f1=2 & freq=16)))
	// will see on next set of frequencies and less than a whole cycle to do
	| (rep=mrep & c<16 & swap  & ((t1=((freq<=c)?train:1-train) & f1<=c+1) | (t1=((freq<=c)?1-train:train) & f1>c+1)) & f1<=freq+2)
	| (rep=mrep & c<16 & !swap & ((t1=((freq<=c)?1-train:train) & f1<=c+1) | (t1=((freq<=c)?train:1-train) & f1>c+1)) & f1<=freq+2)
	| (rep=mrep & c=16 & (t1=((f1=1)?1-train:train)) & f1<=freq+2 & c=16));

//----------------------------------------------------------------------------------------------------------------------------
// module for first receiver
module receiver1
	
	y1 : [0..2*maxr+1]; //clock of the receiver
	receiver : [0..3];
	// 0 - next state scan
	// 1 listeninging on frequencies
	// 2 sending and computing the random delay
	// 3 wait random delay
	freq1 : [0..16]; // frequency of the receiver (use 0 for no frequency set)
	train1 : [0..1]; // train of the receiver
	
	[time] receiver=0 & y1=1 -> (y1'=y1-1); // time passes (2048 time slots pass)
	[]          receiver=0 & y1=0 & success  -> (receiver'=1) & (freq1'=f1) & (train1'=t1); // move to scan
	[]          receiver=0 & y1=0 & !success -> (receiver'=0) & (y1'=1); // will not hear anything so scan then sleep
	// scanning (will hear something - unless I have done something wrong)
	[time] receiver=1 & !hear -> (y1'=y1); // hear nothing: stay in scan and let 1 slot pass
	[]       receiver=1 & hear  -> (receiver'=2) & (y1'=2) & (freq1'=0) & (train1'=0); // hear something: get ready to send reply and let time pass
	// replying
	[time] receiver=2 & y1>0 -> (y1'=y1-1); // let time pass (1 slot)
	[reply]  receiver=2 & y1=0 -> 1/(maxr+1) : (receiver'=3) & (y1'=0) // reply and make random choice
	                  + 1/(maxr+1) : (receiver'=3) & (y1'=2*1)
	                  + 1/(maxr+1) : (receiver'=3) & (y1'=2*2)
	                  + 1/(maxr+1) : (receiver'=3) & (y1'=2*3)
	                  + 1/(maxr+1) : (receiver'=3) & (y1'=2*4)
	                  + 1/(maxr+1) : (receiver'=3) & (y1'=2*5)
	                  + 1/(maxr+1) : (receiver'=3) & (y1'=2*6)
	                  + 1/(maxr+1) : (receiver'=3) & (y1'=2*7)
	                  + 1/(maxr+1) : (receiver'=3) & (y1'=2*8)
	                  + 1/(maxr+1) : (receiver'=3) & (y1'=2*9)
	                  + 1/(maxr+1) : (receiver'=3) & (y1'=2*10)
	                  + 1/(maxr+1) : (receiver'=3) & (y1'=2*11)
	                  + 1/(maxr+1) : (receiver'=3) & (y1'=2*12)
	                  + 1/(maxr+1) : (receiver'=3) & (y1'=2*13)
	                  + 1/(maxr+1) : (receiver'=3) & (y1'=2*14)
	                  + 1/(maxr+1) : (receiver'=3) & (y1'=2*15)
	                  + 1/(maxr+1) : (receiver'=3) & (y1'=2*16)
	                  + 1/(maxr+1) : (receiver'=3) & (y1'=2*17)
	                  + 1/(maxr+1) : (receiver'=3) & (y1'=2*18)
	                  + 1/(maxr+1) : (receiver'=3) & (y1'=2*19)
	                  + 1/(maxr+1) : (receiver'=3) & (y1'=2*20)
	                  + 1/(maxr+1) : (receiver'=3) & (y1'=2*21)
	                  + 1/(maxr+1) : (receiver'=3) & (y1'=2*22)
	                  + 1/(maxr+1) : (receiver'=3) & (y1'=2*23)
	                  + 1/(maxr+1) : (receiver'=3) & (y1'=2*24)
	                  + 1/(maxr+1) : (receiver'=3) & (y1'=2*25)
	                  + 1/(maxr+1) : (receiver'=3) & (y1'=2*26)
	                  + 1/(maxr+1) : (receiver'=3) & (y1'=2*27)
	                  + 1/(maxr+1) : (receiver'=3) & (y1'=2*28)
	                  + 1/(maxr+1) : (receiver'=3) & (y1'=2*29)
	                  + 1/(maxr+1) : (receiver'=3) & (y1'=2*30)
	                  + 1/(maxr+1) : (receiver'=3) & (y1'=2*31)
	                  + 1/(maxr+1) : (receiver'=3) & (y1'=2*32)
	                  + 1/(maxr+1) : (receiver'=3) & (y1'=2*33)
	                  + 1/(maxr+1) : (receiver'=3) & (y1'=2*34)
	                  + 1/(maxr+1) : (receiver'=3) & (y1'=2*35)
	                  + 1/(maxr+1) : (receiver'=3) & (y1'=2*36)
	                  + 1/(maxr+1) : (receiver'=3) & (y1'=2*37)
	                  + 1/(maxr+1) : (receiver'=3) & (y1'=2*38)
	                  + 1/(maxr+1) : (receiver'=3) & (y1'=2*39)
	                  + 1/(maxr+1) : (receiver'=3) & (y1'=2*40)
	                  + 1/(maxr+1) : (receiver'=3) & (y1'=2*41)
	                  + 1/(maxr+1) : (receiver'=3) & (y1'=2*42)
	                  + 1/(maxr+1) : (receiver'=3) & (y1'=2*43)
	                  + 1/(maxr+1) : (receiver'=3) & (y1'=2*44)
	                  + 1/(maxr+1) : (receiver'=3) & (y1'=2*45)
	                  + 1/(maxr+1) : (receiver'=3) & (y1'=2*46)
	                  + 1/(maxr+1) : (receiver'=3) & (y1'=2*47)
	                  + 1/(maxr+1) : (receiver'=3) & (y1'=2*48)
	                  + 1/(maxr+1) : (receiver'=3) & (y1'=2*49)
	                  + 1/(maxr+1) : (receiver'=3) & (y1'=2*50)
	                  + 1/(maxr+1) : (receiver'=3) & (y1'=2*51)
	                  + 1/(maxr+1) : (receiver'=3) & (y1'=2*52)
	                  + 1/(maxr+1) : (receiver'=3) & (y1'=2*53)
	                  + 1/(maxr+1) : (receiver'=3) & (y1'=2*54)
	                  + 1/(maxr+1) : (receiver'=3) & (y1'=2*55)
	                  + 1/(maxr+1) : (receiver'=3) & (y1'=2*56)
	                  + 1/(maxr+1) : (receiver'=3) & (y1'=2*57)
	                  + 1/(maxr+1) : (receiver'=3) & (y1'=2*58)
	                  + 1/(maxr+1) : (receiver'=3) & (y1'=2*59)
	                  + 1/(maxr+1) : (receiver'=3) & (y1'=2*60)
	                  + 1/(maxr+1) : (receiver'=3) & (y1'=2*61)
	                  + 1/(maxr+1) : (receiver'=3) & (y1'=2*62)
	                  + 1/(maxr+1) : (receiver'=3) & (y1'=2*63)
	                  + 1/(maxr+1) : (receiver'=3) & (y1'=2*64)
	                  + 1/(maxr+1) : (receiver'=3) & (y1'=2*65)
	                  + 1/(maxr+1) : (receiver'=3) & (y1'=2*66)
	                  + 1/(maxr+1) : (receiver'=3) & (y1'=2*67)
	                  + 1/(maxr+1) : (receiver'=3) & (y1'=2*68)
	                  + 1/(maxr+1) : (receiver'=3) & (y1'=2*69)
	                  + 1/(maxr+1) : (receiver'=3) & (y1'=2*70)
	                  + 1/(maxr+1) : (receiver'=3) & (y1'=2*71)
	                  + 1/(maxr+1) : (receiver'=3) & (y1'=2*72)
	                  + 1/(maxr+1) : (receiver'=3) & (y1'=2*73)
	                  + 1/(maxr+1) : (receiver'=3) & (y1'=2*74)
	                  + 1/(maxr+1) : (receiver'=3) & (y1'=2*75)
	                  + 1/(maxr+1) : (receiver'=3) & (y1'=2*76)
	                  + 1/(maxr+1) : (receiver'=3) & (y1'=2*77)
	                  + 1/(maxr+1) : (receiver'=3) & (y1'=2*78)
	                  + 1/(maxr+1) : (receiver'=3) & (y1'=2*79)
	                  + 1/(maxr+1) : (receiver'=3) & (y1'=2*80)
	                  + 1/(maxr+1) : (receiver'=3) & (y1'=2*81)
	                  + 1/(maxr+1) : (receiver'=3) & (y1'=2*82)
	                  + 1/(maxr+1) : (receiver'=3) & (y1'=2*83)
	                  + 1/(maxr+1) : (receiver'=3) & (y1'=2*84)
	                  + 1/(maxr+1) : (receiver'=3) & (y1'=2*85)
	                  + 1/(maxr+1) : (receiver'=3) & (y1'=2*86)
	                  + 1/(maxr+1) : (receiver'=3) & (y1'=2*87)
	                  + 1/(maxr+1) : (receiver'=3) & (y1'=2*88)
	                  + 1/(maxr+1) : (receiver'=3) & (y1'=2*89)
	                  + 1/(maxr+1) : (receiver'=3) & (y1'=2*90)
	                  + 1/(maxr+1) : (receiver'=3) & (y1'=2*91)
	                  + 1/(maxr+1) : (receiver'=3) & (y1'=2*92)
	                  + 1/(maxr+1) : (receiver'=3) & (y1'=2*93)
	                  + 1/(maxr+1) : (receiver'=3) & (y1'=2*94)
	                  + 1/(maxr+1) : (receiver'=3) & (y1'=2*95)
	                  + 1/(maxr+1) : (receiver'=3) & (y1'=2*96)
	                  + 1/(maxr+1) : (receiver'=3) & (y1'=2*97)
	                  + 1/(maxr+1) : (receiver'=3) & (y1'=2*98)
	                  + 1/(maxr+1) : (receiver'=3) & (y1'=2*99)
	                  + 1/(maxr+1) : (receiver'=3) & (y1'=2*100)
	                  + 1/(maxr+1) : (receiver'=3) & (y1'=2*101)
	                  + 1/(maxr+1) : (receiver'=3) & (y1'=2*102)
	                  + 1/(maxr+1) : (receiver'=3) & (y1'=2*103)
	                  + 1/(maxr+1) : (receiver'=3) & (y1'=2*104)
	                  + 1/(maxr+1) : (receiver'=3) & (y1'=2*105)
	                  + 1/(maxr+1) : (receiver'=3) & (y1'=2*106)
	                  + 1/(maxr+1) : (receiver'=3) & (y1'=2*107)
	                  + 1/(maxr+1) : (receiver'=3) & (y1'=2*108)
	                  + 1/(maxr+1) : (receiver'=3) & (y1'=2*109)
	                  + 1/(maxr+1) : (receiver'=3) & (y1'=2*110)
	                  + 1/(maxr+1) : (receiver'=3) & (y1'=2*111)
	                  + 1/(maxr+1) : (receiver'=3) & (y1'=2*112)
	                  + 1/(maxr+1) : (receiver'=3) & (y1'=2*113)
	                  + 1/(maxr+1) : (receiver'=3) & (y1'=2*114)
	                  + 1/(maxr+1) : (receiver'=3) & (y1'=2*115)
	                  + 1/(maxr+1) : (receiver'=3) & (y1'=2*116)
	                  + 1/(maxr+1) : (receiver'=3) & (y1'=2*117)
	                  + 1/(maxr+1) : (receiver'=3) & (y1'=2*118)
	                  + 1/(maxr+1) : (receiver'=3) & (y1'=2*119)
	                  + 1/(maxr+1) : (receiver'=3) & (y1'=2*120)
	                  + 1/(maxr+1) : (receiver'=3) & (y1'=2*121)
	                  + 1/(maxr+1) : (receiver'=3) & (y1'=2*122)
	                  + 1/(maxr+1) : (receiver'=3) & (y1'=2*123)
	                  + 1/(maxr+1) : (receiver'=3) & (y1'=2*124)
	                  + 1/(maxr+1) : (receiver'=3) & (y1'=2*125)
	                  + 1/(maxr+1) : (receiver'=3) & (y1'=2*126)
	                  + 1/(maxr+1) : (receiver'=3) & (y1'=2*127);
	// waiting random delay
	[time] receiver=3 & y1>0 -> (y1'=y1-1); // let time pass (1 slot)
	// finished waiting random delay (listen again)
	[] receiver=3 & y1=0 & success  -> (receiver'=1) & (freq1'=f1) & (train1'=t1); // move to scan
	[] receiver=3 & y1=0 & !success -> (receiver'=0) & (y1'=1); // will not hear anything (combine scan and sleep)
	
endmodule

//----------------------------------------------------------------------------------------------------------------------------
// frequency for first receiver
module frequency1
	
	z1 : [1..phase];// clock for phase
	f1 : [1..16]; // frequency of receiver
	t1 : [0..1]; // train of receiver
	
	// update frequency (1 slot passes)
	[time] !sleep & z1 (z1'=z1+1);
	[time] !sleep & z1=phase & f1<16 -> (z1'=1) & (f1'=f1+1);
	[time] !sleep & z1=phase & f1=16 -> (z1'=1) & (f1'=1) & (t1'=1-t1);
	// update frequency (2048 slots pass)
	[time] sleep & z1<=2048         -> (z1'=z1+2048);
	[time] sleep & z1>2048 & f1<16  -> (z1'=z1-2048) & (f1'=f1+1);
	[time] sleep & z1>2048 & f1=16  -> (z1'=z1-2048) & (f1'=1) & (t1'=1-t1);
	// update frequency: something is sent by the receiver (cannot be sleeping here)
	[reply] true -> (f1'=(f1<16)?f1+1:1) & (t1'=(f1<16)?t1:1-t1);
	
endmodule

//----------------------------------------------------------------------------------------------------------------------------

// frequency of sender
// note to make things easier we do not change the frequency for receiving
// will only work if the delays are divisible by 4 otherwise it will cause problems
// frequency of sender
module sender_frequency
	
	// still should try some different orderings?
	
	send : [1..3];   // 1 sending and 2,3 receiving
	freq  : [1..16]; // current frequency mod 16 freq+train*16
	train : [0..1];  // used to work out the frequency (actual frequency equals freq+train*16)
	c : [1..16]; // used to work out the trains
	rep : [1..mrep]; // no of repetitions of a train
	
	// sending
	[time] !sleep & send=1 & (((freq=1)|(freq=3)|(freq=5)|(freq=7)|(freq=9)|(freq=11)|(freq=13)|(freq=15))) & freq!=c -> (freq'=freq+1);
	[time] !sleep & send=1 & (((freq=1)|(freq=3)|(freq=5)|(freq=7)|(freq=9)|(freq=11)|(freq=13)|(freq=15))) & freq=c  -> (freq'=freq+1) & (train'=1-train);
	[time] !sleep & send=1 & (((freq=2)|(freq=4)|(freq=6)|(freq=8)|(freq=10)|(freq=12)|(freq=14)|(freq=16))) -> (send'=2);
	// receiving
	[time] !sleep & send=2 -> (send'=3);
	[time] !sleep & send=3 & freq<16 & freq!=c          -> (send'=1) & (freq'=freq+1);
	[time] !sleep & send=3 & freq<16 & freq=c           -> (send'=1) & (freq'=freq+1) & (train'=1-train);
	[time] !sleep & send=3 & freq=16 & rep (send'=1) & (freq'=1) & (train'=1-train) & (rep'=rep+1); 
	[time] !sleep & send=3 & freq=16 & rep (send'=1) & (freq'=1) & (rep'=rep+1);
	[time] !sleep & send=3 & freq=16 & rep=mrep         -> (send'=1) & (freq'=1) & (train'=swap?1-train:train) & (c'=c=16?1:c+1) & (rep'=1);
	// big time step (2048 slots = 64 repetitions)
	[time] sleep & rep<=64 -> (rep'=rep+64); // sleeping does not change frequency set
	[time] sleep & rep>64  -> (rep'=rep-64) & (c'=c=16?1:c+1) & (train'=swap2?1-train:train); // sleeping changes current frequency set
	
endmodule


//----------------------------------------------------------------------------------------------------------------------------
const int mrec = 1; // after receiving mrec messages the inquiry is stopped

// counts the number of replies received
module replies
	
	// no of non garbled received messages
	rec : [0..mrec];
	
	[time] rec (rec'=rec);
	[reply]  rec (rec'=min(rec+1,mrec));
	[] rec=mrec -> (rec'=rec);
	
endmodule

//----------------------------------------------------------------------------------------------------------------------------

// specify initial state (only that receiver starts scanning and nothing sent)
// note as changed the sender so that for freq to be odd send must equal 1 we need the extra condition
// init rec=0 & y1=0 & receiver=0 & freq1=0 & train1=0 & (send=1 | freq=2,4,6,8,10,12,14,16) endinit
const int k = 1; // frequency the sender starts on
const int T = 0; // train that the sender starts on

init 
	receiver=0 & y1=0 & freq1=0 & train1=0 & // initial state of the receiver 
	rec=0 & // nothing received yet
	f1=k & t1=T & // initial frequency of the receiver (based on its clock)
	(send=1 |((freq=2)|(freq=4)|(freq=6)|(freq=8)|(freq=10)|(freq=12)|(freq=14)|(freq=16)))  // condition required on the sender
endinit

//----------------------------------------------------------------------------------------------------------------------------

// rewards - to compute expected time
rewards "time"
	[time] receiver=0 & y1=1 :2048;
	[time] receiver>0 : 1;
endrewards

label "target" = rec=mrec;

// Expected time to complete the inquiry phase
"time": filter(max, R=? [ F "target" ], "init");

{
    "actions": [
        {
            "name": "reply"
        },
        {
            "name": "time"
        }
    ],
    "automata": [
        {
            "edges": [
                {
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "receiver <- 1",
                                    "ref": "receiver",
                                    "value": 1
                                },
                                {
                                    "comment": "freq1 <- f1",
                                    "ref": "freq1",
                                    "value": "f1"
                                },
                                {
                                    "comment": "train1 <- t1",
                                    "ref": "train1",
                                    "value": "t1"
                                }
                            ],
                            "location": "l"
                        }
                    ],
                    "guard": {
                        "comment": "(((receiver = 0) & (y1 = 0)) & success)",
                        "exp": {
                            "left": {
                                "left": {
                                    "left": "receiver",
                                    "op": "=",
                                    "right": 0
                                },
                                "op": "∧",
                                "right": {
                                    "left": "y1",
                                    "op": "=",
                                    "right": 0
                                }
                            },
                            "op": "∧",
                            "right": {
                                "args": [],
                                "function": "success",
                                "op": "call"
                            }
                        }
                    },
                    "location": "l"
                },
                {
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "y1 <- 1",
                                    "ref": "y1",
                                    "value": 1
                                },
                                {
                                    "comment": "receiver <- 0",
                                    "ref": "receiver",
                                    "value": 0
                                }
                            ],
                            "location": "l"
                        }
                    ],
                    "guard": {
                        "comment": "(((receiver = 0) & (y1 = 0)) & !(success))",
                        "exp": {
                            "left": {
                                "left": {
                                    "left": "receiver",
                                    "op": "=",
                                    "right": 0
                                },
                                "op": "∧",
                                "right": {
                                    "left": "y1",
                                    "op": "=",
                                    "right": 0
                                }
                            },
                            "op": "∧",
                            "right": {
                                "exp": {
                                    "args": [],
                                    "function": "success",
                                    "op": "call"
                                },
                                "op": "¬"
                            }
                        }
                    },
                    "location": "l"
                },
                {
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "y1 <- 2",
                                    "ref": "y1",
                                    "value": 2
                                },
                                {
                                    "comment": "receiver <- 2",
                                    "ref": "receiver",
                                    "value": 2
                                },
                                {
                                    "comment": "freq1 <- 0",
                                    "ref": "freq1",
                                    "value": 0
                                },
                                {
                                    "comment": "train1 <- 0",
                                    "ref": "train1",
                                    "value": 0
                                }
                            ],
                            "location": "l"
                        }
                    ],
                    "guard": {
                        "comment": "((receiver = 1) & hear)",
                        "exp": {
                            "left": {
                                "left": "receiver",
                                "op": "=",
                                "right": 1
                            },
                            "op": "∧",
                            "right": {
                                "args": [],
                                "function": "hear",
                                "op": "call"
                            }
                        }
                    },
                    "location": "l"
                },
                {
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "receiver <- 1",
                                    "ref": "receiver",
                                    "value": 1
                                },
                                {
                                    "comment": "freq1 <- f1",
                                    "ref": "freq1",
                                    "value": "f1"
                                },
                                {
                                    "comment": "train1 <- t1",
                                    "ref": "train1",
                                    "value": "t1"
                                }
                            ],
                            "location": "l"
                        }
                    ],
                    "guard": {
                        "comment": "(((receiver = 3) & (y1 = 0)) & success)",
                        "exp": {
                            "left": {
                                "left": {
                                    "left": "receiver",
                                    "op": "=",
                                    "right": 3
                                },
                                "op": "∧",
                                "right": {
                                    "left": "y1",
                                    "op": "=",
                                    "right": 0
                                }
                            },
                            "op": "∧",
                            "right": {
                                "args": [],
                                "function": "success",
                                "op": "call"
                            }
                        }
                    },
                    "location": "l"
                },
                {
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "y1 <- 1",
                                    "ref": "y1",
                                    "value": 1
                                },
                                {
                                    "comment": "receiver <- 0",
                                    "ref": "receiver",
                                    "value": 0
                                }
                            ],
                            "location": "l"
                        }
                    ],
                    "guard": {
                        "comment": "(((receiver = 3) & (y1 = 0)) & !(success))",
                        "exp": {
                            "left": {
                                "left": {
                                    "left": "receiver",
                                    "op": "=",
                                    "right": 3
                                },
                                "op": "∧",
                                "right": {
                                    "left": "y1",
                                    "op": "=",
                                    "right": 0
                                }
                            },
                            "op": "∧",
                            "right": {
                                "exp": {
                                    "args": [],
                                    "function": "success",
                                    "op": "call"
                                },
                                "op": "¬"
                            }
                        }
                    },
                    "location": "l"
                },
                {
                    "action": "reply",
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "y1 <- 0",
                                    "ref": "y1",
                                    "value": 0
                                },
                                {
                                    "comment": "receiver <- 3",
                                    "ref": "receiver",
                                    "value": 3
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / (127 + 1))",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 128
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "y1 <- 2",
                                    "ref": "y1",
                                    "value": 2
                                },
                                {
                                    "comment": "receiver <- 3",
                                    "ref": "receiver",
                                    "value": 3
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / (127 + 1))",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 128
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "y1 <- 4",
                                    "ref": "y1",
                                    "value": 4
                                },
                                {
                                    "comment": "receiver <- 3",
                                    "ref": "receiver",
                                    "value": 3
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / (127 + 1))",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 128
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "y1 <- 6",
                                    "ref": "y1",
                                    "value": 6
                                },
                                {
                                    "comment": "receiver <- 3",
                                    "ref": "receiver",
                                    "value": 3
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / (127 + 1))",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 128
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "y1 <- 8",
                                    "ref": "y1",
                                    "value": 8
                                },
                                {
                                    "comment": "receiver <- 3",
                                    "ref": "receiver",
                                    "value": 3
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / (127 + 1))",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 128
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "y1 <- 10",
                                    "ref": "y1",
                                    "value": 10
                                },
                                {
                                    "comment": "receiver <- 3",
                                    "ref": "receiver",
                                    "value": 3
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / (127 + 1))",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 128
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "y1 <- 12",
                                    "ref": "y1",
                                    "value": 12
                                },
                                {
                                    "comment": "receiver <- 3",
                                    "ref": "receiver",
                                    "value": 3
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / (127 + 1))",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 128
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "y1 <- 14",
                                    "ref": "y1",
                                    "value": 14
                                },
                                {
                                    "comment": "receiver <- 3",
                                    "ref": "receiver",
                                    "value": 3
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / (127 + 1))",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 128
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "y1 <- 16",
                                    "ref": "y1",
                                    "value": 16
                                },
                                {
                                    "comment": "receiver <- 3",
                                    "ref": "receiver",
                                    "value": 3
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / (127 + 1))",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 128
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "y1 <- 18",
                                    "ref": "y1",
                                    "value": 18
                                },
                                {
                                    "comment": "receiver <- 3",
                                    "ref": "receiver",
                                    "value": 3
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / (127 + 1))",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 128
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "y1 <- 20",
                                    "ref": "y1",
                                    "value": 20
                                },
                                {
                                    "comment": "receiver <- 3",
                                    "ref": "receiver",
                                    "value": 3
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / (127 + 1))",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 128
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "y1 <- 22",
                                    "ref": "y1",
                                    "value": 22
                                },
                                {
                                    "comment": "receiver <- 3",
                                    "ref": "receiver",
                                    "value": 3
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / (127 + 1))",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 128
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "y1 <- 24",
                                    "ref": "y1",
                                    "value": 24
                                },
                                {
                                    "comment": "receiver <- 3",
                                    "ref": "receiver",
                                    "value": 3
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / (127 + 1))",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 128
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "y1 <- 26",
                                    "ref": "y1",
                                    "value": 26
                                },
                                {
                                    "comment": "receiver <- 3",
                                    "ref": "receiver",
                                    "value": 3
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / (127 + 1))",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 128
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "y1 <- 28",
                                    "ref": "y1",
                                    "value": 28
                                },
                                {
                                    "comment": "receiver <- 3",
                                    "ref": "receiver",
                                    "value": 3
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / (127 + 1))",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 128
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "y1 <- 30",
                                    "ref": "y1",
                                    "value": 30
                                },
                                {
                                    "comment": "receiver <- 3",
                                    "ref": "receiver",
                                    "value": 3
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / (127 + 1))",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 128
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "y1 <- 32",
                                    "ref": "y1",
                                    "value": 32
                                },
                                {
                                    "comment": "receiver <- 3",
                                    "ref": "receiver",
                                    "value": 3
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / (127 + 1))",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 128
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "y1 <- 34",
                                    "ref": "y1",
                                    "value": 34
                                },
                                {
                                    "comment": "receiver <- 3",
                                    "ref": "receiver",
                                    "value": 3
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / (127 + 1))",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 128
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "y1 <- 36",
                                    "ref": "y1",
                                    "value": 36
                                },
                                {
                                    "comment": "receiver <- 3",
                                    "ref": "receiver",
                                    "value": 3
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / (127 + 1))",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 128
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "y1 <- 38",
                                    "ref": "y1",
                                    "value": 38
                                },
                                {
                                    "comment": "receiver <- 3",
                                    "ref": "receiver",
                                    "value": 3
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / (127 + 1))",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 128
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "y1 <- 40",
                                    "ref": "y1",
                                    "value": 40
                                },
                                {
                                    "comment": "receiver <- 3",
                                    "ref": "receiver",
                                    "value": 3
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / (127 + 1))",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 128
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "y1 <- 42",
                                    "ref": "y1",
                                    "value": 42
                                },
                                {
                                    "comment": "receiver <- 3",
                                    "ref": "receiver",
                                    "value": 3
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / (127 + 1))",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 128
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "y1 <- 44",
                                    "ref": "y1",
                                    "value": 44
                                },
                                {
                                    "comment": "receiver <- 3",
                                    "ref": "receiver",
                                    "value": 3
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / (127 + 1))",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 128
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "y1 <- 46",
                                    "ref": "y1",
                                    "value": 46
                                },
                                {
                                    "comment": "receiver <- 3",
                                    "ref": "receiver",
                                    "value": 3
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / (127 + 1))",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 128
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "y1 <- 48",
                                    "ref": "y1",
                                    "value": 48
                                },
                                {
                                    "comment": "receiver <- 3",
                                    "ref": "receiver",
                                    "value": 3
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / (127 + 1))",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 128
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "y1 <- 50",
                                    "ref": "y1",
                                    "value": 50
                                },
                                {
                                    "comment": "receiver <- 3",
                                    "ref": "receiver",
                                    "value": 3
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / (127 + 1))",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 128
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "y1 <- 52",
                                    "ref": "y1",
                                    "value": 52
                                },
                                {
                                    "comment": "receiver <- 3",
                                    "ref": "receiver",
                                    "value": 3
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / (127 + 1))",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 128
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "y1 <- 54",
                                    "ref": "y1",
                                    "value": 54
                                },
                                {
                                    "comment": "receiver <- 3",
                                    "ref": "receiver",
                                    "value": 3
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / (127 + 1))",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 128
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "y1 <- 56",
                                    "ref": "y1",
                                    "value": 56
                                },
                                {
                                    "comment": "receiver <- 3",
                                    "ref": "receiver",
                                    "value": 3
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / (127 + 1))",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 128
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "y1 <- 58",
                                    "ref": "y1",
                                    "value": 58
                                },
                                {
                                    "comment": "receiver <- 3",
                                    "ref": "receiver",
                                    "value": 3
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / (127 + 1))",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 128
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "y1 <- 60",
                                    "ref": "y1",
                                    "value": 60
                                },
                                {
                                    "comment": "receiver <- 3",
                                    "ref": "receiver",
                                    "value": 3
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / (127 + 1))",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 128
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "y1 <- 62",
                                    "ref": "y1",
                                    "value": 62
                                },
                                {
                                    "comment": "receiver <- 3",
                                    "ref": "receiver",
                                    "value": 3
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / (127 + 1))",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 128
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "y1 <- 64",
                                    "ref": "y1",
                                    "value": 64
                                },
                                {
                                    "comment": "receiver <- 3",
                                    "ref": "receiver",
                                    "value": 3
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / (127 + 1))",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 128
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "y1 <- 66",
                                    "ref": "y1",
                                    "value": 66
                                },
                                {
                                    "comment": "receiver <- 3",
                                    "ref": "receiver",
                                    "value": 3
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / (127 + 1))",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 128
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "y1 <- 68",
                                    "ref": "y1",
                                    "value": 68
                                },
                                {
                                    "comment": "receiver <- 3",
                                    "ref": "receiver",
                                    "value": 3
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / (127 + 1))",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 128
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "y1 <- 70",
                                    "ref": "y1",
                                    "value": 70
                                },
                                {
                                    "comment": "receiver <- 3",
                                    "ref": "receiver",
                                    "value": 3
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / (127 + 1))",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 128
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "y1 <- 72",
                                    "ref": "y1",
                                    "value": 72
                                },
                                {
                                    "comment": "receiver <- 3",
                                    "ref": "receiver",
                                    "value": 3
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / (127 + 1))",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 128
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "y1 <- 74",
                                    "ref": "y1",
                                    "value": 74
                                },
                                {
                                    "comment": "receiver <- 3",
                                    "ref": "receiver",
                                    "value": 3
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / (127 + 1))",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 128
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "y1 <- 76",
                                    "ref": "y1",
                                    "value": 76
                                },
                                {
                                    "comment": "receiver <- 3",
                                    "ref": "receiver",
                                    "value": 3
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / (127 + 1))",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 128
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "y1 <- 78",
                                    "ref": "y1",
                                    "value": 78
                                },
                                {
                                    "comment": "receiver <- 3",
                                    "ref": "receiver",
                                    "value": 3
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / (127 + 1))",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 128
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "y1 <- 80",
                                    "ref": "y1",
                                    "value": 80
                                },
                                {
                                    "comment": "receiver <- 3",
                                    "ref": "receiver",
                                    "value": 3
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / (127 + 1))",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 128
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "y1 <- 82",
                                    "ref": "y1",
                                    "value": 82
                                },
                                {
                                    "comment": "receiver <- 3",
                                    "ref": "receiver",
                                    "value": 3
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / (127 + 1))",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 128
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "y1 <- 84",
                                    "ref": "y1",
                                    "value": 84
                                },
                                {
                                    "comment": "receiver <- 3",
                                    "ref": "receiver",
                                    "value": 3
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / (127 + 1))",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 128
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "y1 <- 86",
                                    "ref": "y1",
                                    "value": 86
                                },
                                {
                                    "comment": "receiver <- 3",
                                    "ref": "receiver",
                                    "value": 3
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / (127 + 1))",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 128
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "y1 <- 88",
                                    "ref": "y1",
                                    "value": 88
                                },
                                {
                                    "comment": "receiver <- 3",
                                    "ref": "receiver",
                                    "value": 3
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / (127 + 1))",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 128
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "y1 <- 90",
                                    "ref": "y1",
                                    "value": 90
                                },
                                {
                                    "comment": "receiver <- 3",
                                    "ref": "receiver",
                                    "value": 3
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / (127 + 1))",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 128
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "y1 <- 92",
                                    "ref": "y1",
                                    "value": 92
                                },
                                {
                                    "comment": "receiver <- 3",
                                    "ref": "receiver",
                                    "value": 3
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / (127 + 1))",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 128
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "y1 <- 94",
                                    "ref": "y1",
                                    "value": 94
                                },
                                {
                                    "comment": "receiver <- 3",
                                    "ref": "receiver",
                                    "value": 3
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / (127 + 1))",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 128
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "y1 <- 96",
                                    "ref": "y1",
                                    "value": 96
                                },
                                {
                                    "comment": "receiver <- 3",
                                    "ref": "receiver",
                                    "value": 3
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / (127 + 1))",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 128
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "y1 <- 98",
                                    "ref": "y1",
                                    "value": 98
                                },
                                {
                                    "comment": "receiver <- 3",
                                    "ref": "receiver",
                                    "value": 3
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / (127 + 1))",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 128
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "y1 <- 100",
                                    "ref": "y1",
                                    "value": 100
                                },
                                {
                                    "comment": "receiver <- 3",
                                    "ref": "receiver",
                                    "value": 3
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / (127 + 1))",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 128
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "y1 <- 102",
                                    "ref": "y1",
                                    "value": 102
                                },
                                {
                                    "comment": "receiver <- 3",
                                    "ref": "receiver",
                                    "value": 3
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / (127 + 1))",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 128
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "y1 <- 104",
                                    "ref": "y1",
                                    "value": 104
                                },
                                {
                                    "comment": "receiver <- 3",
                                    "ref": "receiver",
                                    "value": 3
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / (127 + 1))",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 128
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "y1 <- 106",
                                    "ref": "y1",
                                    "value": 106
                                },
                                {
                                    "comment": "receiver <- 3",
                                    "ref": "receiver",
                                    "value": 3
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / (127 + 1))",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 128
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "y1 <- 108",
                                    "ref": "y1",
                                    "value": 108
                                },
                                {
                                    "comment": "receiver <- 3",
                                    "ref": "receiver",
                                    "value": 3
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / (127 + 1))",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 128
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "y1 <- 110",
                                    "ref": "y1",
                                    "value": 110
                                },
                                {
                                    "comment": "receiver <- 3",
                                    "ref": "receiver",
                                    "value": 3
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / (127 + 1))",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 128
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "y1 <- 112",
                                    "ref": "y1",
                                    "value": 112
                                },
                                {
                                    "comment": "receiver <- 3",
                                    "ref": "receiver",
                                    "value": 3
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / (127 + 1))",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 128
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "y1 <- 114",
                                    "ref": "y1",
                                    "value": 114
                                },
                                {
                                    "comment": "receiver <- 3",
                                    "ref": "receiver",
                                    "value": 3
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / (127 + 1))",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 128
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "y1 <- 116",
                                    "ref": "y1",
                                    "value": 116
                                },
                                {
                                    "comment": "receiver <- 3",
                                    "ref": "receiver",
                                    "value": 3
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / (127 + 1))",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 128
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "y1 <- 118",
                                    "ref": "y1",
                                    "value": 118
                                },
                                {
                                    "comment": "receiver <- 3",
                                    "ref": "receiver",
                                    "value": 3
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / (127 + 1))",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 128
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "y1 <- 120",
                                    "ref": "y1",
                                    "value": 120
                                },
                                {
                                    "comment": "receiver <- 3",
                                    "ref": "receiver",
                                    "value": 3
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / (127 + 1))",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 128
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "y1 <- 122",
                                    "ref": "y1",
                                    "value": 122
                                },
                                {
                                    "comment": "receiver <- 3",
                                    "ref": "receiver",
                                    "value": 3
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / (127 + 1))",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 128
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "y1 <- 124",
                                    "ref": "y1",
                                    "value": 124
                                },
                                {
                                    "comment": "receiver <- 3",
                                    "ref": "receiver",
                                    "value": 3
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / (127 + 1))",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 128
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "y1 <- 126",
                                    "ref": "y1",
                                    "value": 126
                                },
                                {
                                    "comment": "receiver <- 3",
                                    "ref": "receiver",
                                    "value": 3
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / (127 + 1))",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 128
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "y1 <- 128",
                                    "ref": "y1",
                                    "value": 128
                                },
                                {
                                    "comment": "receiver <- 3",
                                    "ref": "receiver",
                                    "value": 3
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / (127 + 1))",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 128
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "y1 <- 130",
                                    "ref": "y1",
                                    "value": 130
                                },
                                {
                                    "comment": "receiver <- 3",
                                    "ref": "receiver",
                                    "value": 3
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / (127 + 1))",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 128
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "y1 <- 132",
                                    "ref": "y1",
                                    "value": 132
                                },
                                {
                                    "comment": "receiver <- 3",
                                    "ref": "receiver",
                                    "value": 3
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / (127 + 1))",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 128
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "y1 <- 134",
                                    "ref": "y1",
                                    "value": 134
                                },
                                {
                                    "comment": "receiver <- 3",
                                    "ref": "receiver",
                                    "value": 3
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / (127 + 1))",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 128
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "y1 <- 136",
                                    "ref": "y1",
                                    "value": 136
                                },
                                {
                                    "comment": "receiver <- 3",
                                    "ref": "receiver",
                                    "value": 3
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / (127 + 1))",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 128
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "y1 <- 138",
                                    "ref": "y1",
                                    "value": 138
                                },
                                {
                                    "comment": "receiver <- 3",
                                    "ref": "receiver",
                                    "value": 3
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / (127 + 1))",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 128
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "y1 <- 140",
                                    "ref": "y1",
                                    "value": 140
                                },
                                {
                                    "comment": "receiver <- 3",
                                    "ref": "receiver",
                                    "value": 3
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / (127 + 1))",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 128
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "y1 <- 142",
                                    "ref": "y1",
                                    "value": 142
                                },
                                {
                                    "comment": "receiver <- 3",
                                    "ref": "receiver",
                                    "value": 3
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / (127 + 1))",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 128
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "y1 <- 144",
                                    "ref": "y1",
                                    "value": 144
                                },
                                {
                                    "comment": "receiver <- 3",
                                    "ref": "receiver",
                                    "value": 3
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / (127 + 1))",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 128
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "y1 <- 146",
                                    "ref": "y1",
                                    "value": 146
                                },
                                {
                                    "comment": "receiver <- 3",
                                    "ref": "receiver",
                                    "value": 3
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / (127 + 1))",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 128
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "y1 <- 148",
                                    "ref": "y1",
                                    "value": 148
                                },
                                {
                                    "comment": "receiver <- 3",
                                    "ref": "receiver",
                                    "value": 3
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / (127 + 1))",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 128
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "y1 <- 150",
                                    "ref": "y1",
                                    "value": 150
                                },
                                {
                                    "comment": "receiver <- 3",
                                    "ref": "receiver",
                                    "value": 3
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / (127 + 1))",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 128
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "y1 <- 152",
                                    "ref": "y1",
                                    "value": 152
                                },
                                {
                                    "comment": "receiver <- 3",
                                    "ref": "receiver",
                                    "value": 3
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / (127 + 1))",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 128
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "y1 <- 154",
                                    "ref": "y1",
                                    "value": 154
                                },
                                {
                                    "comment": "receiver <- 3",
                                    "ref": "receiver",
                                    "value": 3
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / (127 + 1))",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 128
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "y1 <- 156",
                                    "ref": "y1",
                                    "value": 156
                                },
                                {
                                    "comment": "receiver <- 3",
                                    "ref": "receiver",
                                    "value": 3
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / (127 + 1))",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 128
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "y1 <- 158",
                                    "ref": "y1",
                                    "value": 158
                                },
                                {
                                    "comment": "receiver <- 3",
                                    "ref": "receiver",
                                    "value": 3
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / (127 + 1))",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 128
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "y1 <- 160",
                                    "ref": "y1",
                                    "value": 160
                                },
                                {
                                    "comment": "receiver <- 3",
                                    "ref": "receiver",
                                    "value": 3
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / (127 + 1))",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 128
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "y1 <- 162",
                                    "ref": "y1",
                                    "value": 162
                                },
                                {
                                    "comment": "receiver <- 3",
                                    "ref": "receiver",
                                    "value": 3
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / (127 + 1))",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 128
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "y1 <- 164",
                                    "ref": "y1",
                                    "value": 164
                                },
                                {
                                    "comment": "receiver <- 3",
                                    "ref": "receiver",
                                    "value": 3
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / (127 + 1))",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 128
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "y1 <- 166",
                                    "ref": "y1",
                                    "value": 166
                                },
                                {
                                    "comment": "receiver <- 3",
                                    "ref": "receiver",
                                    "value": 3
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / (127 + 1))",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 128
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "y1 <- 168",
                                    "ref": "y1",
                                    "value": 168
                                },
                                {
                                    "comment": "receiver <- 3",
                                    "ref": "receiver",
                                    "value": 3
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / (127 + 1))",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 128
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "y1 <- 170",
                                    "ref": "y1",
                                    "value": 170
                                },
                                {
                                    "comment": "receiver <- 3",
                                    "ref": "receiver",
                                    "value": 3
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / (127 + 1))",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 128
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "y1 <- 172",
                                    "ref": "y1",
                                    "value": 172
                                },
                                {
                                    "comment": "receiver <- 3",
                                    "ref": "receiver",
                                    "value": 3
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / (127 + 1))",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 128
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "y1 <- 174",
                                    "ref": "y1",
                                    "value": 174
                                },
                                {
                                    "comment": "receiver <- 3",
                                    "ref": "receiver",
                                    "value": 3
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / (127 + 1))",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 128
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "y1 <- 176",
                                    "ref": "y1",
                                    "value": 176
                                },
                                {
                                    "comment": "receiver <- 3",
                                    "ref": "receiver",
                                    "value": 3
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / (127 + 1))",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 128
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "y1 <- 178",
                                    "ref": "y1",
                                    "value": 178
                                },
                                {
                                    "comment": "receiver <- 3",
                                    "ref": "receiver",
                                    "value": 3
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / (127 + 1))",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 128
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "y1 <- 180",
                                    "ref": "y1",
                                    "value": 180
                                },
                                {
                                    "comment": "receiver <- 3",
                                    "ref": "receiver",
                                    "value": 3
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / (127 + 1))",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 128
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "y1 <- 182",
                                    "ref": "y1",
                                    "value": 182
                                },
                                {
                                    "comment": "receiver <- 3",
                                    "ref": "receiver",
                                    "value": 3
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / (127 + 1))",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 128
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "y1 <- 184",
                                    "ref": "y1",
                                    "value": 184
                                },
                                {
                                    "comment": "receiver <- 3",
                                    "ref": "receiver",
                                    "value": 3
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / (127 + 1))",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 128
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "y1 <- 186",
                                    "ref": "y1",
                                    "value": 186
                                },
                                {
                                    "comment": "receiver <- 3",
                                    "ref": "receiver",
                                    "value": 3
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / (127 + 1))",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 128
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "y1 <- 188",
                                    "ref": "y1",
                                    "value": 188
                                },
                                {
                                    "comment": "receiver <- 3",
                                    "ref": "receiver",
                                    "value": 3
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / (127 + 1))",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 128
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "y1 <- 190",
                                    "ref": "y1",
                                    "value": 190
                                },
                                {
                                    "comment": "receiver <- 3",
                                    "ref": "receiver",
                                    "value": 3
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / (127 + 1))",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 128
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "y1 <- 192",
                                    "ref": "y1",
                                    "value": 192
                                },
                                {
                                    "comment": "receiver <- 3",
                                    "ref": "receiver",
                                    "value": 3
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / (127 + 1))",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 128
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "y1 <- 194",
                                    "ref": "y1",
                                    "value": 194
                                },
                                {
                                    "comment": "receiver <- 3",
                                    "ref": "receiver",
                                    "value": 3
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / (127 + 1))",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 128
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "y1 <- 196",
                                    "ref": "y1",
                                    "value": 196
                                },
                                {
                                    "comment": "receiver <- 3",
                                    "ref": "receiver",
                                    "value": 3
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / (127 + 1))",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 128
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "y1 <- 198",
                                    "ref": "y1",
                                    "value": 198
                                },
                                {
                                    "comment": "receiver <- 3",
                                    "ref": "receiver",
                                    "value": 3
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / (127 + 1))",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 128
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "y1 <- 200",
                                    "ref": "y1",
                                    "value": 200
                                },
                                {
                                    "comment": "receiver <- 3",
                                    "ref": "receiver",
                                    "value": 3
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / (127 + 1))",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 128
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "y1 <- 202",
                                    "ref": "y1",
                                    "value": 202
                                },
                                {
                                    "comment": "receiver <- 3",
                                    "ref": "receiver",
                                    "value": 3
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / (127 + 1))",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 128
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "y1 <- 204",
                                    "ref": "y1",
                                    "value": 204
                                },
                                {
                                    "comment": "receiver <- 3",
                                    "ref": "receiver",
                                    "value": 3
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / (127 + 1))",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 128
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "y1 <- 206",
                                    "ref": "y1",
                                    "value": 206
                                },
                                {
                                    "comment": "receiver <- 3",
                                    "ref": "receiver",
                                    "value": 3
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / (127 + 1))",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 128
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "y1 <- 208",
                                    "ref": "y1",
                                    "value": 208
                                },
                                {
                                    "comment": "receiver <- 3",
                                    "ref": "receiver",
                                    "value": 3
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / (127 + 1))",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 128
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "y1 <- 210",
                                    "ref": "y1",
                                    "value": 210
                                },
                                {
                                    "comment": "receiver <- 3",
                                    "ref": "receiver",
                                    "value": 3
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / (127 + 1))",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 128
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "y1 <- 212",
                                    "ref": "y1",
                                    "value": 212
                                },
                                {
                                    "comment": "receiver <- 3",
                                    "ref": "receiver",
                                    "value": 3
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / (127 + 1))",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 128
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "y1 <- 214",
                                    "ref": "y1",
                                    "value": 214
                                },
                                {
                                    "comment": "receiver <- 3",
                                    "ref": "receiver",
                                    "value": 3
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / (127 + 1))",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 128
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "y1 <- 216",
                                    "ref": "y1",
                                    "value": 216
                                },
                                {
                                    "comment": "receiver <- 3",
                                    "ref": "receiver",
                                    "value": 3
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / (127 + 1))",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 128
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "y1 <- 218",
                                    "ref": "y1",
                                    "value": 218
                                },
                                {
                                    "comment": "receiver <- 3",
                                    "ref": "receiver",
                                    "value": 3
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / (127 + 1))",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 128
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "y1 <- 220",
                                    "ref": "y1",
                                    "value": 220
                                },
                                {
                                    "comment": "receiver <- 3",
                                    "ref": "receiver",
                                    "value": 3
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / (127 + 1))",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 128
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "y1 <- 222",
                                    "ref": "y1",
                                    "value": 222
                                },
                                {
                                    "comment": "receiver <- 3",
                                    "ref": "receiver",
                                    "value": 3
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / (127 + 1))",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 128
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "y1 <- 224",
                                    "ref": "y1",
                                    "value": 224
                                },
                                {
                                    "comment": "receiver <- 3",
                                    "ref": "receiver",
                                    "value": 3
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / (127 + 1))",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 128
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "y1 <- 226",
                                    "ref": "y1",
                                    "value": 226
                                },
                                {
                                    "comment": "receiver <- 3",
                                    "ref": "receiver",
                                    "value": 3
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / (127 + 1))",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 128
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "y1 <- 228",
                                    "ref": "y1",
                                    "value": 228
                                },
                                {
                                    "comment": "receiver <- 3",
                                    "ref": "receiver",
                                    "value": 3
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / (127 + 1))",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 128
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "y1 <- 230",
                                    "ref": "y1",
                                    "value": 230
                                },
                                {
                                    "comment": "receiver <- 3",
                                    "ref": "receiver",
                                    "value": 3
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / (127 + 1))",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 128
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "y1 <- 232",
                                    "ref": "y1",
                                    "value": 232
                                },
                                {
                                    "comment": "receiver <- 3",
                                    "ref": "receiver",
                                    "value": 3
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / (127 + 1))",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 128
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "y1 <- 234",
                                    "ref": "y1",
                                    "value": 234
                                },
                                {
                                    "comment": "receiver <- 3",
                                    "ref": "receiver",
                                    "value": 3
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / (127 + 1))",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 128
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "y1 <- 236",
                                    "ref": "y1",
                                    "value": 236
                                },
                                {
                                    "comment": "receiver <- 3",
                                    "ref": "receiver",
                                    "value": 3
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / (127 + 1))",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 128
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "y1 <- 238",
                                    "ref": "y1",
                                    "value": 238
                                },
                                {
                                    "comment": "receiver <- 3",
                                    "ref": "receiver",
                                    "value": 3
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / (127 + 1))",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 128
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "y1 <- 240",
                                    "ref": "y1",
                                    "value": 240
                                },
                                {
                                    "comment": "receiver <- 3",
                                    "ref": "receiver",
                                    "value": 3
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / (127 + 1))",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 128
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "y1 <- 242",
                                    "ref": "y1",
                                    "value": 242
                                },
                                {
                                    "comment": "receiver <- 3",
                                    "ref": "receiver",
                                    "value": 3
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / (127 + 1))",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 128
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "y1 <- 244",
                                    "ref": "y1",
                                    "value": 244
                                },
                                {
                                    "comment": "receiver <- 3",
                                    "ref": "receiver",
                                    "value": 3
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / (127 + 1))",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 128
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "y1 <- 246",
                                    "ref": "y1",
                                    "value": 246
                                },
                                {
                                    "comment": "receiver <- 3",
                                    "ref": "receiver",
                                    "value": 3
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / (127 + 1))",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 128
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "y1 <- 248",
                                    "ref": "y1",
                                    "value": 248
                                },
                                {
                                    "comment": "receiver <- 3",
                                    "ref": "receiver",
                                    "value": 3
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / (127 + 1))",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 128
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "y1 <- 250",
                                    "ref": "y1",
                                    "value": 250
                                },
                                {
                                    "comment": "receiver <- 3",
                                    "ref": "receiver",
                                    "value": 3
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / (127 + 1))",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 128
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "y1 <- 252",
                                    "ref": "y1",
                                    "value": 252
                                },
                                {
                                    "comment": "receiver <- 3",
                                    "ref": "receiver",
                                    "value": 3
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / (127 + 1))",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 128
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "y1 <- 254",
                                    "ref": "y1",
                                    "value": 254
                                },
                                {
                                    "comment": "receiver <- 3",
                                    "ref": "receiver",
                                    "value": 3
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / (127 + 1))",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 128
                                }
                            }
                        }
                    ],
                    "guard": {
                        "comment": "((receiver = 2) & (y1 = 0))",
                        "exp": {
                            "left": {
                                "left": "receiver",
                                "op": "=",
                                "right": 2
                            },
                            "op": "∧",
                            "right": {
                                "left": "y1",
                                "op": "=",
                                "right": 0
                            }
                        }
                    },
                    "location": "l"
                },
                {
                    "action": "time",
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "y1 <- (y1 - 1)",
                                    "ref": "y1",
                                    "value": {
                                        "left": "y1",
                                        "op": "-",
                                        "right": 1
                                    }
                                },
                                {
                                    "comment": "time <- ((((receiver = 0) & (y1 = 1)) ? 2048 : 0) + ((receiver > 0) ? 1 : 0))",
                                    "ref": "time",
                                    "value": {
                                        "left": {
                                            "else": 0.0,
                                            "if": {
                                                "left": {
                                                    "left": "receiver",
                                                    "op": "=",
                                                    "right": 0
                                                },
                                                "op": "∧",
                                                "right": {
                                                    "left": "y1",
                                                    "op": "=",
                                                    "right": 1
                                                }
                                            },
                                            "op": "ite",
                                            "then": 2048
                                        },
                                        "op": "+",
                                        "right": {
                                            "else": 0.0,
                                            "if": {
                                                "left": "receiver",
                                                "op": ">",
                                                "right": 0
                                            },
                                            "op": "ite",
                                            "then": 1
                                        }
                                    }
                                }
                            ],
                            "location": "l"
                        }
                    ],
                    "guard": {
                        "comment": "((receiver = 0) & (y1 = 1))",
                        "exp": {
                            "left": {
                                "left": "receiver",
                                "op": "=",
                                "right": 0
                            },
                            "op": "∧",
                            "right": {
                                "left": "y1",
                                "op": "=",
                                "right": 1
                            }
                        }
                    },
                    "location": "l"
                },
                {
                    "action": "time",
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "y1 <- y1",
                                    "ref": "y1",
                                    "value": "y1"
                                },
                                {
                                    "comment": "time <- ((((receiver = 0) & (y1 = 1)) ? 2048 : 0) + ((receiver > 0) ? 1 : 0))",
                                    "ref": "time",
                                    "value": {
                                        "left": {
                                            "else": 0.0,
                                            "if": {
                                                "left": {
                                                    "left": "receiver",
                                                    "op": "=",
                                                    "right": 0
                                                },
                                                "op": "∧",
                                                "right": {
                                                    "left": "y1",
                                                    "op": "=",
                                                    "right": 1
                                                }
                                            },
                                            "op": "ite",
                                            "then": 2048
                                        },
                                        "op": "+",
                                        "right": {
                                            "else": 0.0,
                                            "if": {
                                                "left": "receiver",
                                                "op": ">",
                                                "right": 0
                                            },
                                            "op": "ite",
                                            "then": 1
                                        }
                                    }
                                }
                            ],
                            "location": "l"
                        }
                    ],
                    "guard": {
                        "comment": "((receiver = 1) & !(hear))",
                        "exp": {
                            "left": {
                                "left": "receiver",
                                "op": "=",
                                "right": 1
                            },
                            "op": "∧",
                            "right": {
                                "exp": {
                                    "args": [],
                                    "function": "hear",
                                    "op": "call"
                                },
                                "op": "¬"
                            }
                        }
                    },
                    "location": "l"
                },
                {
                    "action": "time",
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "y1 <- (y1 - 1)",
                                    "ref": "y1",
                                    "value": {
                                        "left": "y1",
                                        "op": "-",
                                        "right": 1
                                    }
                                },
                                {
                                    "comment": "time <- ((((receiver = 0) & (y1 = 1)) ? 2048 : 0) + ((receiver > 0) ? 1 : 0))",
                                    "ref": "time",
                                    "value": {
                                        "left": {
                                            "else": 0.0,
                                            "if": {
                                                "left": {
                                                    "left": "receiver",
                                                    "op": "=",
                                                    "right": 0
                                                },
                                                "op": "∧",
                                                "right": {
                                                    "left": "y1",
                                                    "op": "=",
                                                    "right": 1
                                                }
                                            },
                                            "op": "ite",
                                            "then": 2048
                                        },
                                        "op": "+",
                                        "right": {
                                            "else": 0.0,
                                            "if": {
                                                "left": "receiver",
                                                "op": ">",
                                                "right": 0
                                            },
                                            "op": "ite",
                                            "then": 1
                                        }
                                    }
                                }
                            ],
                            "location": "l"
                        }
                    ],
                    "guard": {
                        "comment": "((receiver = 2) & (y1 > 0))",
                        "exp": {
                            "left": {
                                "left": "receiver",
                                "op": "=",
                                "right": 2
                            },
                            "op": "∧",
                            "right": {
                                "left": "y1",
                                "op": ">",
                                "right": 0
                            }
                        }
                    },
                    "location": "l"
                },
                {
                    "action": "time",
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "y1 <- (y1 - 1)",
                                    "ref": "y1",
                                    "value": {
                                        "left": "y1",
                                        "op": "-",
                                        "right": 1
                                    }
                                },
                                {
                                    "comment": "time <- ((((receiver = 0) & (y1 = 1)) ? 2048 : 0) + ((receiver > 0) ? 1 : 0))",
                                    "ref": "time",
                                    "value": {
                                        "left": {
                                            "else": 0.0,
                                            "if": {
                                                "left": {
                                                    "left": "receiver",
                                                    "op": "=",
                                                    "right": 0
                                                },
                                                "op": "∧",
                                                "right": {
                                                    "left": "y1",
                                                    "op": "=",
                                                    "right": 1
                                                }
                                            },
                                            "op": "ite",
                                            "then": 2048
                                        },
                                        "op": "+",
                                        "right": {
                                            "else": 0.0,
                                            "if": {
                                                "left": "receiver",
                                                "op": ">",
                                                "right": 0
                                            },
                                            "op": "ite",
                                            "then": 1
                                        }
                                    }
                                }
                            ],
                            "location": "l"
                        }
                    ],
                    "guard": {
                        "comment": "((receiver = 3) & (y1 > 0))",
                        "exp": {
                            "left": {
                                "left": "receiver",
                                "op": "=",
                                "right": 3
                            },
                            "op": "∧",
                            "right": {
                                "left": "y1",
                                "op": ">",
                                "right": 0
                            }
                        }
                    },
                    "location": "l"
                }
            ],
            "initial-locations": [
                "l"
            ],
            "locations": [
                {
                    "name": "l",
                    "transient-values": [
                        {
                            "comment": "target <- (rec = 1)",
                            "ref": "target",
                            "value": {
                                "left": "rec",
                                "op": "=",
                                "right": 1
                            }
                        }
                    ]
                }
            ],
            "name": "receiver1",
            "variables": []
        },
        {
            "edges": [
                {
                    "action": "reply",
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "f1 <- ((f1 < 16) ? (f1 + 1) : 1)",
                                    "ref": "f1",
                                    "value": {
                                        "else": 1,
                                        "if": {
                                            "left": "f1",
                                            "op": "<",
                                            "right": 16
                                        },
                                        "op": "ite",
                                        "then": {
                                            "left": "f1",
                                            "op": "+",
                                            "right": 1
                                        }
                                    }
                                },
                                {
                                    "comment": "t1 <- ((f1 < 16) ? t1 : (1 - t1))",
                                    "ref": "t1",
                                    "value": {
                                        "else": {
                                            "left": 1,
                                            "op": "-",
                                            "right": "t1"
                                        },
                                        "if": {
                                            "left": "f1",
                                            "op": "<",
                                            "right": 16
                                        },
                                        "op": "ite",
                                        "then": "t1"
                                    }
                                }
                            ],
                            "location": "l"
                        }
                    ],
                    "location": "l"
                },
                {
                    "action": "time",
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "z1 <- (z1 + 1)",
                                    "ref": "z1",
                                    "value": {
                                        "left": "z1",
                                        "op": "+",
                                        "right": 1
                                    }
                                }
                            ],
                            "location": "l"
                        }
                    ],
                    "guard": {
                        "comment": "(!(sleep) & (z1 < 4096))",
                        "exp": {
                            "left": {
                                "exp": {
                                    "args": [],
                                    "function": "sleep",
                                    "op": "call"
                                },
                                "op": "¬"
                            },
                            "op": "∧",
                            "right": {
                                "left": "z1",
                                "op": "<",
                                "right": 4096
                            }
                        }
                    },
                    "location": "l"
                },
                {
                    "action": "time",
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "z1 <- 1",
                                    "ref": "z1",
                                    "value": 1
                                },
                                {
                                    "comment": "f1 <- (f1 + 1)",
                                    "ref": "f1",
                                    "value": {
                                        "left": "f1",
                                        "op": "+",
                                        "right": 1
                                    }
                                }
                            ],
                            "location": "l"
                        }
                    ],
                    "guard": {
                        "comment": "((!(sleep) & (z1 = 4096)) & (f1 < 16))",
                        "exp": {
                            "left": {
                                "left": {
                                    "exp": {
                                        "args": [],
                                        "function": "sleep",
                                        "op": "call"
                                    },
                                    "op": "¬"
                                },
                                "op": "∧",
                                "right": {
                                    "left": "z1",
                                    "op": "=",
                                    "right": 4096
                                }
                            },
                            "op": "∧",
                            "right": {
                                "left": "f1",
                                "op": "<",
                                "right": 16
                            }
                        }
                    },
                    "location": "l"
                },
                {
                    "action": "time",
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "z1 <- 1",
                                    "ref": "z1",
                                    "value": 1
                                },
                                {
                                    "comment": "f1 <- 1",
                                    "ref": "f1",
                                    "value": 1
                                },
                                {
                                    "comment": "t1 <- (1 - t1)",
                                    "ref": "t1",
                                    "value": {
                                        "left": 1,
                                        "op": "-",
                                        "right": "t1"
                                    }
                                }
                            ],
                            "location": "l"
                        }
                    ],
                    "guard": {
                        "comment": "((!(sleep) & (z1 = 4096)) & (f1 = 16))",
                        "exp": {
                            "left": {
                                "left": {
                                    "exp": {
                                        "args": [],
                                        "function": "sleep",
                                        "op": "call"
                                    },
                                    "op": "¬"
                                },
                                "op": "∧",
                                "right": {
                                    "left": "z1",
                                    "op": "=",
                                    "right": 4096
                                }
                            },
                            "op": "∧",
                            "right": {
                                "left": "f1",
                                "op": "=",
                                "right": 16
                            }
                        }
                    },
                    "location": "l"
                },
                {
                    "action": "time",
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "z1 <- (z1 + 2048)",
                                    "ref": "z1",
                                    "value": {
                                        "left": "z1",
                                        "op": "+",
                                        "right": 2048
                                    }
                                }
                            ],
                            "location": "l"
                        }
                    ],
                    "guard": {
                        "comment": "(sleep & (z1 <= 2048))",
                        "exp": {
                            "left": {
                                "args": [],
                                "function": "sleep",
                                "op": "call"
                            },
                            "op": "∧",
                            "right": {
                                "left": "z1",
                                "op": "≤",
                                "right": 2048
                            }
                        }
                    },
                    "location": "l"
                },
                {
                    "action": "time",
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "z1 <- (z1 - 2048)",
                                    "ref": "z1",
                                    "value": {
                                        "left": "z1",
                                        "op": "-",
                                        "right": 2048
                                    }
                                },
                                {
                                    "comment": "f1 <- (f1 + 1)",
                                    "ref": "f1",
                                    "value": {
                                        "left": "f1",
                                        "op": "+",
                                        "right": 1
                                    }
                                }
                            ],
                            "location": "l"
                        }
                    ],
                    "guard": {
                        "comment": "((sleep & (z1 > 2048)) & (f1 < 16))",
                        "exp": {
                            "left": {
                                "left": {
                                    "args": [],
                                    "function": "sleep",
                                    "op": "call"
                                },
                                "op": "∧",
                                "right": {
                                    "left": "z1",
                                    "op": ">",
                                    "right": 2048
                                }
                            },
                            "op": "∧",
                            "right": {
                                "left": "f1",
                                "op": "<",
                                "right": 16
                            }
                        }
                    },
                    "location": "l"
                },
                {
                    "action": "time",
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "z1 <- (z1 - 2048)",
                                    "ref": "z1",
                                    "value": {
                                        "left": "z1",
                                        "op": "-",
                                        "right": 2048
                                    }
                                },
                                {
                                    "comment": "f1 <- 1",
                                    "ref": "f1",
                                    "value": 1
                                },
                                {
                                    "comment": "t1 <- (1 - t1)",
                                    "ref": "t1",
                                    "value": {
                                        "left": 1,
                                        "op": "-",
                                        "right": "t1"
                                    }
                                }
                            ],
                            "location": "l"
                        }
                    ],
                    "guard": {
                        "comment": "((sleep & (z1 > 2048)) & (f1 = 16))",
                        "exp": {
                            "left": {
                                "left": {
                                    "args": [],
                                    "function": "sleep",
                                    "op": "call"
                                },
                                "op": "∧",
                                "right": {
                                    "left": "z1",
                                    "op": ">",
                                    "right": 2048
                                }
                            },
                            "op": "∧",
                            "right": {
                                "left": "f1",
                                "op": "=",
                                "right": 16
                            }
                        }
                    },
                    "location": "l"
                }
            ],
            "initial-locations": [
                "l"
            ],
            "locations": [
                {
                    "name": "l"
                }
            ],
            "name": "frequency1",
            "variables": [
                {
                    "name": "z1",
                    "type": {
                        "base": "int",
                        "kind": "bounded",
                        "lower-bound": 1,
                        "upper-bound": 4096
                    }
                }
            ]
        },
        {
            "edges": [
                {
                    "action": "time",
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "freq <- (freq + 1)",
                                    "ref": "freq",
                                    "value": {
                                        "left": "freq",
                                        "op": "+",
                                        "right": 1
                                    }
                                }
                            ],
                            "location": "l"
                        }
                    ],
                    "guard": {
                        "comment": "(((!(sleep) & (send = 1)) & ((((((((freq = 1) | (freq = 3)) | (freq = 5)) | (freq = 7)) | (freq = 9)) | (freq = 11)) | (freq = 13)) | (freq = 15))) & (freq != c))",
                        "exp": {
                            "left": {
                                "left": {
                                    "left": "freq",
                                    "op": "≠",
                                    "right": "c"
                                },
                                "op": "∧",
                                "right": {
                                    "left": "send",
                                    "op": "=",
                                    "right": 1
                                }
                            },
                            "op": "∧",
                            "right": {
                                "left": {
                                    "left": {
                                        "left": {
                                            "left": {
                                                "left": "freq",
                                                "op": "=",
                                                "right": 15
                                            },
                                            "op": "∨",
                                            "right": {
                                                "left": "freq",
                                                "op": "=",
                                                "right": 3
                                            }
                                        },
                                        "op": "∨",
                                        "right": {
                                            "left": {
                                                "left": "freq",
                                                "op": "=",
                                                "right": 9
                                            },
                                            "op": "∨",
                                            "right": {
                                                "left": "freq",
                                                "op": "=",
                                                "right": 7
                                            }
                                        }
                                    },
                                    "op": "∨",
                                    "right": {
                                        "left": {
                                            "left": {
                                                "left": "freq",
                                                "op": "=",
                                                "right": 13
                                            },
                                            "op": "∨",
                                            "right": {
                                                "left": "freq",
                                                "op": "=",
                                                "right": 1
                                            }
                                        },
                                        "op": "∨",
                                        "right": {
                                            "left": {
                                                "left": "freq",
                                                "op": "=",
                                                "right": 11
                                            },
                                            "op": "∨",
                                            "right": {
                                                "left": "freq",
                                                "op": "=",
                                                "right": 5
                                            }
                                        }
                                    }
                                },
                                "op": "∧",
                                "right": {
                                    "exp": {
                                        "args": [],
                                        "function": "sleep",
                                        "op": "call"
                                    },
                                    "op": "¬"
                                }
                            }
                        }
                    },
                    "location": "l"
                },
                {
                    "action": "time",
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "freq <- (freq + 1)",
                                    "ref": "freq",
                                    "value": {
                                        "left": "freq",
                                        "op": "+",
                                        "right": 1
                                    }
                                },
                                {
                                    "comment": "train <- (1 - train)",
                                    "ref": "train",
                                    "value": {
                                        "left": 1,
                                        "op": "-",
                                        "right": "train"
                                    }
                                }
                            ],
                            "location": "l"
                        }
                    ],
                    "guard": {
                        "comment": "(((!(sleep) & (send = 1)) & ((((((((freq = 1) | (freq = 3)) | (freq = 5)) | (freq = 7)) | (freq = 9)) | (freq = 11)) | (freq = 13)) | (freq = 15))) & (freq = c))",
                        "exp": {
                            "left": {
                                "left": {
                                    "left": "freq",
                                    "op": "=",
                                    "right": "c"
                                },
                                "op": "∧",
                                "right": {
                                    "left": "send",
                                    "op": "=",
                                    "right": 1
                                }
                            },
                            "op": "∧",
                            "right": {
                                "left": {
                                    "left": {
                                        "left": {
                                            "left": {
                                                "left": "freq",
                                                "op": "=",
                                                "right": 15
                                            },
                                            "op": "∨",
                                            "right": {
                                                "left": "freq",
                                                "op": "=",
                                                "right": 3
                                            }
                                        },
                                        "op": "∨",
                                        "right": {
                                            "left": {
                                                "left": "freq",
                                                "op": "=",
                                                "right": 9
                                            },
                                            "op": "∨",
                                            "right": {
                                                "left": "freq",
                                                "op": "=",
                                                "right": 7
                                            }
                                        }
                                    },
                                    "op": "∨",
                                    "right": {
                                        "left": {
                                            "left": {
                                                "left": "freq",
                                                "op": "=",
                                                "right": 13
                                            },
                                            "op": "∨",
                                            "right": {
                                                "left": "freq",
                                                "op": "=",
                                                "right": 1
                                            }
                                        },
                                        "op": "∨",
                                        "right": {
                                            "left": {
                                                "left": "freq",
                                                "op": "=",
                                                "right": 11
                                            },
                                            "op": "∨",
                                            "right": {
                                                "left": "freq",
                                                "op": "=",
                                                "right": 5
                                            }
                                        }
                                    }
                                },
                                "op": "∧",
                                "right": {
                                    "exp": {
                                        "args": [],
                                        "function": "sleep",
                                        "op": "call"
                                    },
                                    "op": "¬"
                                }
                            }
                        }
                    },
                    "location": "l"
                },
                {
                    "action": "time",
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "send <- 2",
                                    "ref": "send",
                                    "value": 2
                                }
                            ],
                            "location": "l"
                        }
                    ],
                    "guard": {
                        "comment": "((!(sleep) & (send = 1)) & ((((((((freq = 2) | (freq = 4)) | (freq = 6)) | (freq = 8)) | (freq = 10)) | (freq = 12)) | (freq = 14)) | (freq = 16)))",
                        "exp": {
                            "left": {
                                "left": {
                                    "exp": {
                                        "args": [],
                                        "function": "sleep",
                                        "op": "call"
                                    },
                                    "op": "¬"
                                },
                                "op": "∧",
                                "right": {
                                    "left": "send",
                                    "op": "=",
                                    "right": 1
                                }
                            },
                            "op": "∧",
                            "right": {
                                "left": {
                                    "left": {
                                        "left": {
                                            "left": "freq",
                                            "op": "=",
                                            "right": 16
                                        },
                                        "op": "∨",
                                        "right": {
                                            "left": "freq",
                                            "op": "=",
                                            "right": 4
                                        }
                                    },
                                    "op": "∨",
                                    "right": {
                                        "left": {
                                            "left": "freq",
                                            "op": "=",
                                            "right": 10
                                        },
                                        "op": "∨",
                                        "right": {
                                            "left": "freq",
                                            "op": "=",
                                            "right": 8
                                        }
                                    }
                                },
                                "op": "∨",
                                "right": {
                                    "left": {
                                        "left": {
                                            "left": "freq",
                                            "op": "=",
                                            "right": 14
                                        },
                                        "op": "∨",
                                        "right": {
                                            "left": "freq",
                                            "op": "=",
                                            "right": 2
                                        }
                                    },
                                    "op": "∨",
                                    "right": {
                                        "left": {
                                            "left": "freq",
                                            "op": "=",
                                            "right": 12
                                        },
                                        "op": "∨",
                                        "right": {
                                            "left": "freq",
                                            "op": "=",
                                            "right": 6
                                        }
                                    }
                                }
                            }
                        }
                    },
                    "location": "l"
                },
                {
                    "action": "time",
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "send <- 3",
                                    "ref": "send",
                                    "value": 3
                                }
                            ],
                            "location": "l"
                        }
                    ],
                    "guard": {
                        "comment": "(!(sleep) & (send = 2))",
                        "exp": {
                            "left": {
                                "exp": {
                                    "args": [],
                                    "function": "sleep",
                                    "op": "call"
                                },
                                "op": "¬"
                            },
                            "op": "∧",
                            "right": {
                                "left": "send",
                                "op": "=",
                                "right": 2
                            }
                        }
                    },
                    "location": "l"
                },
                {
                    "action": "time",
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "send <- 1",
                                    "ref": "send",
                                    "value": 1
                                },
                                {
                                    "comment": "freq <- (freq + 1)",
                                    "ref": "freq",
                                    "value": {
                                        "left": "freq",
                                        "op": "+",
                                        "right": 1
                                    }
                                }
                            ],
                            "location": "l"
                        }
                    ],
                    "guard": {
                        "comment": "(((!(sleep) & (send = 3)) & (freq < 16)) & (freq != c))",
                        "exp": {
                            "left": {
                                "left": {
                                    "left": "freq",
                                    "op": "≠",
                                    "right": "c"
                                },
                                "op": "∧",
                                "right": {
                                    "left": "send",
                                    "op": "=",
                                    "right": 3
                                }
                            },
                            "op": "∧",
                            "right": {
                                "left": {
                                    "left": "freq",
                                    "op": "<",
                                    "right": 16
                                },
                                "op": "∧",
                                "right": {
                                    "exp": {
                                        "args": [],
                                        "function": "sleep",
                                        "op": "call"
                                    },
                                    "op": "¬"
                                }
                            }
                        }
                    },
                    "location": "l"
                },
                {
                    "action": "time",
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "send <- 1",
                                    "ref": "send",
                                    "value": 1
                                },
                                {
                                    "comment": "freq <- (freq + 1)",
                                    "ref": "freq",
                                    "value": {
                                        "left": "freq",
                                        "op": "+",
                                        "right": 1
                                    }
                                },
                                {
                                    "comment": "train <- (1 - train)",
                                    "ref": "train",
                                    "value": {
                                        "left": 1,
                                        "op": "-",
                                        "right": "train"
                                    }
                                }
                            ],
                            "location": "l"
                        }
                    ],
                    "guard": {
                        "comment": "(((!(sleep) & (send = 3)) & (freq < 16)) & (freq = c))",
                        "exp": {
                            "left": {
                                "left": {
                                    "left": "freq",
                                    "op": "=",
                                    "right": "c"
                                },
                                "op": "∧",
                                "right": {
                                    "left": "send",
                                    "op": "=",
                                    "right": 3
                                }
                            },
                            "op": "∧",
                            "right": {
                                "left": {
                                    "left": "freq",
                                    "op": "<",
                                    "right": 16
                                },
                                "op": "∧",
                                "right": {
                                    "exp": {
                                        "args": [],
                                        "function": "sleep",
                                        "op": "call"
                                    },
                                    "op": "¬"
                                }
                            }
                        }
                    },
                    "location": "l"
                },
                {
                    "action": "time",
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "send <- 1",
                                    "ref": "send",
                                    "value": 1
                                },
                                {
                                    "comment": "freq <- 1",
                                    "ref": "freq",
                                    "value": 1
                                },
                                {
                                    "comment": "train <- (1 - train)",
                                    "ref": "train",
                                    "value": {
                                        "left": 1,
                                        "op": "-",
                                        "right": "train"
                                    }
                                },
                                {
                                    "comment": "rep <- (rep + 1)",
                                    "ref": "rep",
                                    "value": {
                                        "left": "rep",
                                        "op": "+",
                                        "right": 1
                                    }
                                }
                            ],
                            "location": "l"
                        }
                    ],
                    "guard": {
                        "comment": "((((!(sleep) & (send = 3)) & (freq = 16)) & (rep < 128)) & (c != 16))",
                        "exp": {
                            "left": {
                                "left": {
                                    "left": {
                                        "left": "c",
                                        "op": "≠",
                                        "right": 16
                                    },
                                    "op": "∧",
                                    "right": {
                                        "left": "send",
                                        "op": "=",
                                        "right": 3
                                    }
                                },
                                "op": "∧",
                                "right": {
                                    "left": "freq",
                                    "op": "=",
                                    "right": 16
                                }
                            },
                            "op": "∧",
                            "right": {
                                "left": {
                                    "left": "rep",
                                    "op": "<",
                                    "right": 128
                                },
                                "op": "∧",
                                "right": {
                                    "exp": {
                                        "args": [],
                                        "function": "sleep",
                                        "op": "call"
                                    },
                                    "op": "¬"
                                }
                            }
                        }
                    },
                    "location": "l"
                },
                {
                    "action": "time",
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "send <- 1",
                                    "ref": "send",
                                    "value": 1
                                },
                                {
                                    "comment": "freq <- 1",
                                    "ref": "freq",
                                    "value": 1
                                },
                                {
                                    "comment": "rep <- (rep + 1)",
                                    "ref": "rep",
                                    "value": {
                                        "left": "rep",
                                        "op": "+",
                                        "right": 1
                                    }
                                }
                            ],
                            "location": "l"
                        }
                    ],
                    "guard": {
                        "comment": "((((!(sleep) & (send = 3)) & (freq = 16)) & (rep < 128)) & (c = 16))",
                        "exp": {
                            "left": {
                                "left": {
                                    "left": {
                                        "left": "c",
                                        "op": "=",
                                        "right": 16
                                    },
                                    "op": "∧",
                                    "right": {
                                        "left": "send",
                                        "op": "=",
                                        "right": 3
                                    }
                                },
                                "op": "∧",
                                "right": {
                                    "left": "freq",
                                    "op": "=",
                                    "right": 16
                                }
                            },
                            "op": "∧",
                            "right": {
                                "left": {
                                    "left": "rep",
                                    "op": "<",
                                    "right": 128
                                },
                                "op": "∧",
                                "right": {
                                    "exp": {
                                        "args": [],
                                        "function": "sleep",
                                        "op": "call"
                                    },
                                    "op": "¬"
                                }
                            }
                        }
                    },
                    "location": "l"
                },
                {
                    "action": "time",
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "send <- 1",
                                    "ref": "send",
                                    "value": 1
                                },
                                {
                                    "comment": "freq <- 1",
                                    "ref": "freq",
                                    "value": 1
                                },
                                {
                                    "comment": "train <- (swap ? (1 - train) : train)",
                                    "ref": "train",
                                    "value": {
                                        "else": "train",
                                        "if": {
                                            "args": [],
                                            "function": "swap",
                                            "op": "call"
                                        },
                                        "op": "ite",
                                        "then": {
                                            "left": 1,
                                            "op": "-",
                                            "right": "train"
                                        }
                                    }
                                },
                                {
                                    "comment": "c <- ((c = 16) ? 1 : (c + 1))",
                                    "ref": "c",
                                    "value": {
                                        "else": {
                                            "left": "c",
                                            "op": "+",
                                            "right": 1
                                        },
                                        "if": {
                                            "left": "c",
                                            "op": "=",
                                            "right": 16
                                        },
                                        "op": "ite",
                                        "then": 1
                                    }
                                },
                                {
                                    "comment": "rep <- 1",
                                    "ref": "rep",
                                    "value": 1
                                }
                            ],
                            "location": "l"
                        }
                    ],
                    "guard": {
                        "comment": "(((!(sleep) & (send = 3)) & (freq = 16)) & (rep = 128))",
                        "exp": {
                            "left": {
                                "left": {
                                    "left": "rep",
                                    "op": "=",
                                    "right": 128
                                },
                                "op": "∧",
                                "right": {
                                    "left": "send",
                                    "op": "=",
                                    "right": 3
                                }
                            },
                            "op": "∧",
                            "right": {
                                "left": {
                                    "left": "freq",
                                    "op": "=",
                                    "right": 16
                                },
                                "op": "∧",
                                "right": {
                                    "exp": {
                                        "args": [],
                                        "function": "sleep",
                                        "op": "call"
                                    },
                                    "op": "¬"
                                }
                            }
                        }
                    },
                    "location": "l"
                },
                {
                    "action": "time",
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "rep <- (rep + 64)",
                                    "ref": "rep",
                                    "value": {
                                        "left": "rep",
                                        "op": "+",
                                        "right": 64
                                    }
                                }
                            ],
                            "location": "l"
                        }
                    ],
                    "guard": {
                        "comment": "(sleep & (rep <= 64))",
                        "exp": {
                            "left": {
                                "args": [],
                                "function": "sleep",
                                "op": "call"
                            },
                            "op": "∧",
                            "right": {
                                "left": "rep",
                                "op": "≤",
                                "right": 64
                            }
                        }
                    },
                    "location": "l"
                },
                {
                    "action": "time",
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "train <- (swap2 ? (1 - train) : train)",
                                    "ref": "train",
                                    "value": {
                                        "else": "train",
                                        "if": {
                                            "args": [],
                                            "function": "swap2",
                                            "op": "call"
                                        },
                                        "op": "ite",
                                        "then": {
                                            "left": 1,
                                            "op": "-",
                                            "right": "train"
                                        }
                                    }
                                },
                                {
                                    "comment": "c <- ((c = 16) ? 1 : (c + 1))",
                                    "ref": "c",
                                    "value": {
                                        "else": {
                                            "left": "c",
                                            "op": "+",
                                            "right": 1
                                        },
                                        "if": {
                                            "left": "c",
                                            "op": "=",
                                            "right": 16
                                        },
                                        "op": "ite",
                                        "then": 1
                                    }
                                },
                                {
                                    "comment": "rep <- (rep - 64)",
                                    "ref": "rep",
                                    "value": {
                                        "left": "rep",
                                        "op": "-",
                                        "right": 64
                                    }
                                }
                            ],
                            "location": "l"
                        }
                    ],
                    "guard": {
                        "comment": "(sleep & (rep > 64))",
                        "exp": {
                            "left": {
                                "args": [],
                                "function": "sleep",
                                "op": "call"
                            },
                            "op": "∧",
                            "right": {
                                "left": "rep",
                                "op": ">",
                                "right": 64
                            }
                        }
                    },
                    "location": "l"
                }
            ],
            "initial-locations": [
                "l"
            ],
            "locations": [
                {
                    "name": "l"
                }
            ],
            "name": "sender_frequency",
            "variables": []
        },
        {
            "edges": [
                {
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "rec <- rec",
                                    "ref": "rec",
                                    "value": "rec"
                                }
                            ],
                            "location": "l"
                        }
                    ],
                    "guard": {
                        "comment": "(rec = 1)",
                        "exp": {
                            "left": "rec",
                            "op": "=",
                            "right": 1
                        }
                    },
                    "location": "l"
                },
                {
                    "action": "reply",
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "rec <- (min((rec + 1), 1))",
                                    "ref": "rec",
                                    "value": {
                                        "left": {
                                            "left": "rec",
                                            "op": "+",
                                            "right": 1
                                        },
                                        "op": "min",
                                        "right": 1
                                    }
                                }
                            ],
                            "location": "l"
                        }
                    ],
                    "guard": {
                        "comment": "(rec < 1)",
                        "exp": {
                            "left": "rec",
                            "op": "<",
                            "right": 1
                        }
                    },
                    "location": "l"
                },
                {
                    "action": "time",
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "rec <- rec",
                                    "ref": "rec",
                                    "value": "rec"
                                }
                            ],
                            "location": "l"
                        }
                    ],
                    "guard": {
                        "comment": "(rec < 1)",
                        "exp": {
                            "left": "rec",
                            "op": "<",
                            "right": 1
                        }
                    },
                    "location": "l"
                }
            ],
            "initial-locations": [
                "l"
            ],
            "locations": [
                {
                    "name": "l"
                }
            ],
            "name": "replies",
            "variables": []
        }
    ],
    "constants": [
        {
            "name": "phase",
            "type": "int",
            "value": 4096
        },
        {
            "name": "maxr",
            "type": "int",
            "value": 127
        },
        {
            "name": "mrep",
            "type": "int",
            "value": 128
        },
        {
            "name": "mrec",
            "type": "int",
            "value": 1
        },
        {
            "name": "k",
            "type": "int",
            "value": 1
        },
        {
            "name": "T",
            "type": "int",
            "value": 0
        }
    ],
    "features": [
        "derived-operators",
        "functions"
    ],
    "functions": [
        {
            "body": {
                "left": {
                    "left": "receiver",
                    "op": "=",
                    "right": 0
                },
                "op": "∧",
                "right": {
                    "left": "y1",
                    "op": "=",
                    "right": 1
                }
            },
            "name": "sleep",
            "parameters": [],
            "type": "bool"
        },
        {
            "body": {
                "left": {
                    "left": {
                        "left": {
                            "left": "c",
                            "op": "=",
                            "right": 16
                        },
                        "op": "∨",
                        "right": {
                            "left": "c",
                            "op": "=",
                            "right": 4
                        }
                    },
                    "op": "∨",
                    "right": {
                        "left": {
                            "left": "c",
                            "op": "=",
                            "right": 10
                        },
                        "op": "∨",
                        "right": {
                            "left": "c",
                            "op": "=",
                            "right": 8
                        }
                    }
                },
                "op": "∨",
                "right": {
                    "left": {
                        "left": {
                            "left": "c",
                            "op": "=",
                            "right": 14
                        },
                        "op": "∨",
                        "right": {
                            "left": "c",
                            "op": "=",
                            "right": 2
                        }
                    },
                    "op": "∨",
                    "right": {
                        "left": {
                            "left": "c",
                            "op": "=",
                            "right": 12
                        },
                        "op": "∨",
                        "right": {
                            "left": "c",
                            "op": "=",
                            "right": 6
                        }
                    }
                }
            },
            "name": "swap",
            "parameters": [],
            "type": "bool"
        },
        {
            "body": {
                "left": {
                    "left": {
                        "left": {
                            "left": {
                                "left": {
                                    "left": {
                                        "left": "c",
                                        "op": "=",
                                        "right": 16
                                    },
                                    "op": "∧",
                                    "right": {
                                        "left": "c",
                                        "op": "=",
                                        "right": 16
                                    }
                                },
                                "op": "∧",
                                "right": {
                                    "left": "t1",
                                    "op": "=",
                                    "right": {
                                        "else": "train",
                                        "if": {
                                            "left": "f1",
                                            "op": "=",
                                            "right": 1
                                        },
                                        "op": "ite",
                                        "then": {
                                            "left": 1,
                                            "op": "-",
                                            "right": "train"
                                        }
                                    }
                                }
                            },
                            "op": "∧",
                            "right": {
                                "left": {
                                    "left": "f1",
                                    "op": "≤",
                                    "right": {
                                        "left": "freq",
                                        "op": "+",
                                        "right": 2
                                    }
                                },
                                "op": "∧",
                                "right": {
                                    "left": "rep",
                                    "op": "=",
                                    "right": 128
                                }
                            }
                        },
                        "op": "∨",
                        "right": {
                            "left": {
                                "left": {
                                    "left": "rep",
                                    "op": "=",
                                    "right": 128
                                },
                                "op": "∧",
                                "right": {
                                    "left": {
                                        "left": {
                                            "left": "send",
                                            "op": "=",
                                            "right": 1
                                        },
                                        "op": "∧",
                                        "right": {
                                            "left": "freq",
                                            "op": "≤",
                                            "right": "f1"
                                        }
                                    },
                                    "op": "∨",
                                    "right": {
                                        "left": {
                                            "left": "send",
                                            "op": ">",
                                            "right": 1
                                        },
                                        "op": "∧",
                                        "right": {
                                            "left": "freq",
                                            "op": "<",
                                            "right": "f1"
                                        }
                                    }
                                }
                            },
                            "op": "∧",
                            "right": {
                                "left": {
                                    "left": {
                                        "left": "t1",
                                        "op": "=",
                                        "right": {
                                            "else": {
                                                "left": 1,
                                                "op": "-",
                                                "right": "train"
                                            },
                                            "if": {
                                                "left": "freq",
                                                "op": "≤",
                                                "right": "c"
                                            },
                                            "op": "ite",
                                            "then": "train"
                                        }
                                    },
                                    "op": "∧",
                                    "right": {
                                        "left": "f1",
                                        "op": "≤",
                                        "right": "c"
                                    }
                                },
                                "op": "∨",
                                "right": {
                                    "left": {
                                        "left": "t1",
                                        "op": "=",
                                        "right": {
                                            "else": "train",
                                            "if": {
                                                "left": "freq",
                                                "op": "≤",
                                                "right": "c"
                                            },
                                            "op": "ite",
                                            "then": {
                                                "left": 1,
                                                "op": "-",
                                                "right": "train"
                                            }
                                        }
                                    },
                                    "op": "∧",
                                    "right": {
                                        "left": "f1",
                                        "op": ">",
                                        "right": "c"
                                    }
                                }
                            }
                        }
                    },
                    "op": "∨",
                    "right": {
                        "left": {
                            "left": {
                                "left": {
                                    "left": {
                                        "left": {
                                            "left": "f1",
                                            "op": "=",
                                            "right": 1
                                        },
                                        "op": "∧",
                                        "right": {
                                            "left": "freq",
                                            "op": "≥",
                                            "right": 15
                                        }
                                    },
                                    "op": "∨",
                                    "right": {
                                        "left": {
                                            "left": "f1",
                                            "op": "=",
                                            "right": 2
                                        },
                                        "op": "∧",
                                        "right": {
                                            "left": "freq",
                                            "op": "=",
                                            "right": 16
                                        }
                                    }
                                },
                                "op": "∧",
                                "right": {
                                    "left": "c",
                                    "op": "=",
                                    "right": 16
                                }
                            },
                            "op": "∧",
                            "right": {
                                "left": {
                                    "left": "t1",
                                    "op": "=",
                                    "right": {
                                        "else": "train",
                                        "if": {
                                            "left": "f1",
                                            "op": "=",
                                            "right": 1
                                        },
                                        "op": "ite",
                                        "then": {
                                            "left": 1,
                                            "op": "-",
                                            "right": "train"
                                        }
                                    }
                                },
                                "op": "∧",
                                "right": {
                                    "left": "rep",
                                    "op": "=",
                                    "right": 127
                                }
                            }
                        },
                        "op": "∨",
                        "right": {
                            "left": {
                                "left": {
                                    "left": {
                                        "left": {
                                            "left": {
                                                "left": "f1",
                                                "op": "=",
                                                "right": 1
                                            },
                                            "op": "∧",
                                            "right": {
                                                "left": "freq",
                                                "op": "≥",
                                                "right": 15
                                            }
                                        },
                                        "op": "∨",
                                        "right": {
                                            "left": {
                                                "left": "f1",
                                                "op": "=",
                                                "right": 2
                                            },
                                            "op": "∧",
                                            "right": {
                                                "left": "freq",
                                                "op": "=",
                                                "right": 16
                                            }
                                        }
                                    },
                                    "op": "∧",
                                    "right": {
                                        "left": "c",
                                        "op": "<",
                                        "right": 16
                                    }
                                },
                                "op": "∧",
                                "right": {
                                    "exp": {
                                        "args": [],
                                        "function": "swap",
                                        "op": "call"
                                    },
                                    "op": "¬"
                                }
                            },
                            "op": "∧",
                            "right": {
                                "left": {
                                    "left": {
                                        "left": {
                                            "left": "t1",
                                            "op": "=",
                                            "right": {
                                                "else": "train",
                                                "if": {
                                                    "left": "freq",
                                                    "op": "≤",
                                                    "right": "c"
                                                },
                                                "op": "ite",
                                                "then": {
                                                    "left": 1,
                                                    "op": "-",
                                                    "right": "train"
                                                }
                                            }
                                        },
                                        "op": "∧",
                                        "right": {
                                            "left": "f1",
                                            "op": "≤",
                                            "right": {
                                                "left": "c",
                                                "op": "+",
                                                "right": 1
                                            }
                                        }
                                    },
                                    "op": "∨",
                                    "right": {
                                        "left": {
                                            "left": "t1",
                                            "op": "=",
                                            "right": {
                                                "else": {
                                                    "left": 1,
                                                    "op": "-",
                                                    "right": "train"
                                                },
                                                "if": {
                                                    "left": "freq",
                                                    "op": "≤",
                                                    "right": "c"
                                                },
                                                "op": "ite",
                                                "then": "train"
                                            }
                                        },
                                        "op": "∧",
                                        "right": {
                                            "left": "f1",
                                            "op": ">",
                                            "right": {
                                                "left": "c",
                                                "op": "+",
                                                "right": 1
                                            }
                                        }
                                    }
                                },
                                "op": "∧",
                                "right": {
                                    "left": "rep",
                                    "op": "=",
                                    "right": 127
                                }
                            }
                        }
                    }
                },
                "op": "∨",
                "right": {
                    "left": {
                        "left": {
                            "left": {
                                "left": {
                                    "left": {
                                        "left": "f1",
                                        "op": "≤",
                                        "right": {
                                            "left": "freq",
                                            "op": "+",
                                            "right": 2
                                        }
                                    },
                                    "op": "∧",
                                    "right": {
                                        "left": "c",
                                        "op": "<",
                                        "right": 16
                                    }
                                },
                                "op": "∧",
                                "right": {
                                    "exp": {
                                        "args": [],
                                        "function": "swap",
                                        "op": "call"
                                    },
                                    "op": "¬"
                                }
                            },
                            "op": "∧",
                            "right": {
                                "left": {
                                    "left": {
                                        "left": {
                                            "left": "t1",
                                            "op": "=",
                                            "right": {
                                                "else": "train",
                                                "if": {
                                                    "left": "freq",
                                                    "op": "≤",
                                                    "right": "c"
                                                },
                                                "op": "ite",
                                                "then": {
                                                    "left": 1,
                                                    "op": "-",
                                                    "right": "train"
                                                }
                                            }
                                        },
                                        "op": "∧",
                                        "right": {
                                            "left": "f1",
                                            "op": "≤",
                                            "right": {
                                                "left": "c",
                                                "op": "+",
                                                "right": 1
                                            }
                                        }
                                    },
                                    "op": "∨",
                                    "right": {
                                        "left": {
                                            "left": "t1",
                                            "op": "=",
                                            "right": {
                                                "else": {
                                                    "left": 1,
                                                    "op": "-",
                                                    "right": "train"
                                                },
                                                "if": {
                                                    "left": "freq",
                                                    "op": "≤",
                                                    "right": "c"
                                                },
                                                "op": "ite",
                                                "then": "train"
                                            }
                                        },
                                        "op": "∧",
                                        "right": {
                                            "left": "f1",
                                            "op": ">",
                                            "right": {
                                                "left": "c",
                                                "op": "+",
                                                "right": 1
                                            }
                                        }
                                    }
                                },
                                "op": "∧",
                                "right": {
                                    "left": "rep",
                                    "op": "=",
                                    "right": 128
                                }
                            }
                        },
                        "op": "∨",
                        "right": {
                            "left": {
                                "left": "rep",
                                "op": "<",
                                "right": 128
                            },
                            "op": "∧",
                            "right": {
                                "left": {
                                    "left": {
                                        "left": "t1",
                                        "op": "=",
                                        "right": {
                                            "else": {
                                                "left": 1,
                                                "op": "-",
                                                "right": "train"
                                            },
                                            "if": {
                                                "left": "freq",
                                                "op": "≤",
                                                "right": "c"
                                            },
                                            "op": "ite",
                                            "then": "train"
                                        }
                                    },
                                    "op": "∧",
                                    "right": {
                                        "left": "f1",
                                        "op": "≤",
                                        "right": "c"
                                    }
                                },
                                "op": "∨",
                                "right": {
                                    "left": {
                                        "left": "t1",
                                        "op": "=",
                                        "right": {
                                            "else": "train",
                                            "if": {
                                                "left": "freq",
                                                "op": "≤",
                                                "right": "c"
                                            },
                                            "op": "ite",
                                            "then": {
                                                "left": 1,
                                                "op": "-",
                                                "right": "train"
                                            }
                                        }
                                    },
                                    "op": "∧",
                                    "right": {
                                        "left": "f1",
                                        "op": ">",
                                        "right": "c"
                                    }
                                }
                            }
                        }
                    },
                    "op": "∨",
                    "right": {
                        "left": {
                            "left": {
                                "left": {
                                    "left": {
                                        "left": "f1",
                                        "op": "≤",
                                        "right": {
                                            "left": "freq",
                                            "op": "+",
                                            "right": 2
                                        }
                                    },
                                    "op": "∧",
                                    "right": {
                                        "left": "c",
                                        "op": "<",
                                        "right": 16
                                    }
                                },
                                "op": "∧",
                                "right": {
                                    "args": [],
                                    "function": "swap",
                                    "op": "call"
                                }
                            },
                            "op": "∧",
                            "right": {
                                "left": {
                                    "left": {
                                        "left": {
                                            "left": "t1",
                                            "op": "=",
                                            "right": {
                                                "else": {
                                                    "left": 1,
                                                    "op": "-",
                                                    "right": "train"
                                                },
                                                "if": {
                                                    "left": "freq",
                                                    "op": "≤",
                                                    "right": "c"
                                                },
                                                "op": "ite",
                                                "then": "train"
                                            }
                                        },
                                        "op": "∧",
                                        "right": {
                                            "left": "f1",
                                            "op": "≤",
                                            "right": {
                                                "left": "c",
                                                "op": "+",
                                                "right": 1
                                            }
                                        }
                                    },
                                    "op": "∨",
                                    "right": {
                                        "left": {
                                            "left": "t1",
                                            "op": "=",
                                            "right": {
                                                "else": "train",
                                                "if": {
                                                    "left": "freq",
                                                    "op": "≤",
                                                    "right": "c"
                                                },
                                                "op": "ite",
                                                "then": {
                                                    "left": 1,
                                                    "op": "-",
                                                    "right": "train"
                                                }
                                            }
                                        },
                                        "op": "∧",
                                        "right": {
                                            "left": "f1",
                                            "op": ">",
                                            "right": {
                                                "left": "c",
                                                "op": "+",
                                                "right": 1
                                            }
                                        }
                                    }
                                },
                                "op": "∧",
                                "right": {
                                    "left": "rep",
                                    "op": "=",
                                    "right": 128
                                }
                            }
                        },
                        "op": "∨",
                        "right": {
                            "left": {
                                "left": {
                                    "left": {
                                        "left": {
                                            "left": {
                                                "left": "f1",
                                                "op": "=",
                                                "right": 1
                                            },
                                            "op": "∧",
                                            "right": {
                                                "left": "freq",
                                                "op": "≥",
                                                "right": 15
                                            }
                                        },
                                        "op": "∨",
                                        "right": {
                                            "left": {
                                                "left": "f1",
                                                "op": "=",
                                                "right": 2
                                            },
                                            "op": "∧",
                                            "right": {
                                                "left": "freq",
                                                "op": "=",
                                                "right": 16
                                            }
                                        }
                                    },
                                    "op": "∧",
                                    "right": {
                                        "left": "c",
                                        "op": "<",
                                        "right": 16
                                    }
                                },
                                "op": "∧",
                                "right": {
                                    "args": [],
                                    "function": "swap",
                                    "op": "call"
                                }
                            },
                            "op": "∧",
                            "right": {
                                "left": {
                                    "left": {
                                        "left": {
                                            "left": "t1",
                                            "op": "=",
                                            "right": {
                                                "else": {
                                                    "left": 1,
                                                    "op": "-",
                                                    "right": "train"
                                                },
                                                "if": {
                                                    "left": "freq",
                                                    "op": "≤",
                                                    "right": "c"
                                                },
                                                "op": "ite",
                                                "then": "train"
                                            }
                                        },
                                        "op": "∧",
                                        "right": {
                                            "left": "f1",
                                            "op": "≤",
                                            "right": {
                                                "left": "c",
                                                "op": "+",
                                                "right": 1
                                            }
                                        }
                                    },
                                    "op": "∨",
                                    "right": {
                                        "left": {
                                            "left": "t1",
                                            "op": "=",
                                            "right": {
                                                "else": "train",
                                                "if": {
                                                    "left": "freq",
                                                    "op": "≤",
                                                    "right": "c"
                                                },
                                                "op": "ite",
                                                "then": {
                                                    "left": 1,
                                                    "op": "-",
                                                    "right": "train"
                                                }
                                            }
                                        },
                                        "op": "∧",
                                        "right": {
                                            "left": "f1",
                                            "op": ">",
                                            "right": {
                                                "left": "c",
                                                "op": "+",
                                                "right": 1
                                            }
                                        }
                                    }
                                },
                                "op": "∧",
                                "right": {
                                    "left": "rep",
                                    "op": "=",
                                    "right": 127
                                }
                            }
                        }
                    }
                }
            },
            "name": "success",
            "parameters": [],
            "type": "bool"
        },
        {
            "body": {
                "left": {
                    "left": {
                        "left": "freq1",
                        "op": "=",
                        "right": "freq"
                    },
                    "op": "∧",
                    "right": {
                        "left": "train1",
                        "op": "=",
                        "right": "train"
                    }
                },
                "op": "∧",
                "right": {
                    "left": "send",
                    "op": "=",
                    "right": 1
                }
            },
            "name": "hear",
            "parameters": [],
            "type": "bool"
        },
        {
            "body": {
                "left": {
                    "left": {
                        "left": {
                            "left": {
                                "left": {
                                    "left": {
                                        "left": "c",
                                        "op": "=",
                                        "right": 14
                                    },
                                    "op": "∨",
                                    "right": {
                                        "left": "c",
                                        "op": "=",
                                        "right": 4
                                    }
                                },
                                "op": "∨",
                                "right": {
                                    "left": "c",
                                    "op": "=",
                                    "right": 8
                                }
                            },
                            "op": "∨",
                            "right": {
                                "left": {
                                    "left": {
                                        "left": "c",
                                        "op": "=",
                                        "right": 12
                                    },
                                    "op": "∨",
                                    "right": {
                                        "left": "c",
                                        "op": "=",
                                        "right": 2
                                    }
                                },
                                "op": "∨",
                                "right": {
                                    "left": {
                                        "left": "c",
                                        "op": "=",
                                        "right": 10
                                    },
                                    "op": "∨",
                                    "right": {
                                        "left": "c",
                                        "op": "=",
                                        "right": 6
                                    }
                                }
                            }
                        },
                        "op": "∧",
                        "right": {
                            "left": "freq",
                            "op": "=",
                            "right": {
                                "left": "c",
                                "op": "+",
                                "right": 1
                            }
                        }
                    },
                    "op": "∨",
                    "right": {
                        "left": {
                            "left": "c",
                            "op": "=",
                            "right": 16
                        },
                        "op": "∧",
                        "right": {
                            "left": "freq",
                            "op": "=",
                            "right": 1
                        }
                    }
                },
                "op": "∨",
                "right": {
                    "left": {
                        "left": {
                            "left": {
                                "left": {
                                    "left": "c",
                                    "op": "=",
                                    "right": 15
                                },
                                "op": "∨",
                                "right": {
                                    "left": "c",
                                    "op": "=",
                                    "right": 3
                                }
                            },
                            "op": "∨",
                            "right": {
                                "left": {
                                    "left": "c",
                                    "op": "=",
                                    "right": 9
                                },
                                "op": "∨",
                                "right": {
                                    "left": "c",
                                    "op": "=",
                                    "right": 7
                                }
                            }
                        },
                        "op": "∨",
                        "right": {
                            "left": {
                                "left": {
                                    "left": "c",
                                    "op": "=",
                                    "right": 13
                                },
                                "op": "∨",
                                "right": {
                                    "left": "c",
                                    "op": "=",
                                    "right": 1
                                }
                            },
                            "op": "∨",
                            "right": {
                                "left": {
                                    "left": "c",
                                    "op": "=",
                                    "right": 11
                                },
                                "op": "∨",
                                "right": {
                                    "left": "c",
                                    "op": "=",
                                    "right": 5
                                }
                            }
                        }
                    },
                    "op": "∧",
                    "right": {
                        "left": "freq",
                        "op": "≠",
                        "right": {
                            "left": "c",
                            "op": "+",
                            "right": 1
                        }
                    }
                }
            },
            "name": "swap2",
            "parameters": [],
            "type": "bool"
        }
    ],
    "jani-version": 1,
    "name": "model",
    "properties": [
        {
            "expression": {
                "fun": "max",
                "op": "filter",
                "states": {
                    "op": "initial"
                },
                "values": {
                    "accumulate": [
                        "steps"
                    ],
                    "exp": "time",
                    "op": "Emin",
                    "reach": "target"
                }
            },
            "name": "time"
        }
    ],
    "restrict-initial": {
        "exp": {
            "left": {
                "left": {
                    "left": {
                        "left": {
                            "left": {
                                "left": {
                                    "left": {
                                        "left": "send",
                                        "op": "=",
                                        "right": 1
                                    },
                                    "op": "∨",
                                    "right": {
                                        "left": "freq",
                                        "op": "=",
                                        "right": 4
                                    }
                                },
                                "op": "∨",
                                "right": {
                                    "left": "freq",
                                    "op": "=",
                                    "right": 10
                                }
                            },
                            "op": "∨",
                            "right": {
                                "left": {
                                    "left": "freq",
                                    "op": "=",
                                    "right": 14
                                },
                                "op": "∨",
                                "right": {
                                    "left": "freq",
                                    "op": "=",
                                    "right": 6
                                }
                            }
                        },
                        "op": "∨",
                        "right": {
                            "left": {
                                "left": {
                                    "left": "freq",
                                    "op": "=",
                                    "right": 16
                                },
                                "op": "∨",
                                "right": {
                                    "left": "freq",
                                    "op": "=",
                                    "right": 2
                                }
                            },
                            "op": "∨",
                            "right": {
                                "left": {
                                    "left": "freq",
                                    "op": "=",
                                    "right": 12
                                },
                                "op": "∨",
                                "right": {
                                    "left": "freq",
                                    "op": "=",
                                    "right": 8
                                }
                            }
                        }
                    },
                    "op": "∧",
                    "right": {
                        "left": "y1",
                        "op": "=",
                        "right": 0
                    }
                },
                "op": "∧",
                "right": {
                    "left": {
                        "left": "rec",
                        "op": "=",
                        "right": 0
                    },
                    "op": "∧",
                    "right": {
                        "left": "train1",
                        "op": "=",
                        "right": 0
                    }
                }
            },
            "op": "∧",
            "right": {
                "left": {
                    "left": {
                        "left": "t1",
                        "op": "=",
                        "right": 0
                    },
                    "op": "∧",
                    "right": {
                        "left": "receiver",
                        "op": "=",
                        "right": 0
                    }
                },
                "op": "∧",
                "right": {
                    "left": {
                        "left": "f1",
                        "op": "=",
                        "right": 1
                    },
                    "op": "∧",
                    "right": {
                        "left": "freq1",
                        "op": "=",
                        "right": 0
                    }
                }
            }
        }
    },
    "system": {
        "elements": [
            {
                "automaton": "receiver1"
            },
            {
                "automaton": "frequency1"
            },
            {
                "automaton": "sender_frequency"
            },
            {
                "automaton": "replies"
            }
        ],
        "syncs": [
            {
                "result": "reply",
                "synchronise": [
                    "reply",
                    "reply",
                    null,
                    "reply"
                ]
            },
            {
                "result": "time",
                "synchronise": [
                    "time",
                    "time",
                    "time",
                    "time"
                ]
            }
        ]
    },
    "type": "dtmc",
    "variables": [
        {
            "initial-value": false,
            "name": "target",
            "transient": true,
            "type": "bool"
        },
        {
            "initial-value": 0.0,
            "name": "time",
            "transient": true,
            "type": "real"
        },
        {
            "name": "y1",
            "type": {
                "base": "int",
                "kind": "bounded",
                "lower-bound": 0,
                "upper-bound": 255
            }
        },
        {
            "name": "receiver",
            "type": {
                "base": "int",
                "kind": "bounded",
                "lower-bound": 0,
                "upper-bound": 3
            }
        },
        {
            "name": "freq1",
            "type": {
                "base": "int",
                "kind": "bounded",
                "lower-bound": 0,
                "upper-bound": 16
            }
        },
        {
            "name": "train1",
            "type": {
                "base": "int",
                "kind": "bounded",
                "lower-bound": 0,
                "upper-bound": 1
            }
        },
        {
            "name": "f1",
            "type": {
                "base": "int",
                "kind": "bounded",
                "lower-bound": 1,
                "upper-bound": 16
            }
        },
        {
            "name": "t1",
            "type": {
                "base": "int",
                "kind": "bounded",
                "lower-bound": 0,
                "upper-bound": 1
            }
        },
        {
            "name": "send",
            "type": {
                "base": "int",
                "kind": "bounded",
                "lower-bound": 1,
                "upper-bound": 3
            }
        },
        {
            "name": "freq",
            "type": {
                "base": "int",
                "kind": "bounded",
                "lower-bound": 1,
                "upper-bound": 16
            }
        },
        {
            "name": "train",
            "type": {
                "base": "int",
                "kind": "bounded",
                "lower-bound": 0,
                "upper-bound": 1
            }
        },
        {
            "name": "c",
            "type": {
                "base": "int",
                "kind": "bounded",
                "lower-bound": 1,
                "upper-bound": 16
            }
        },
        {
            "name": "rep",
            "type": {
                "base": "int",
                "kind": "bounded",
                "lower-bound": 1,
                "upper-bound": 128
            }
        },
        {
            "name": "rec",
            "type": {
                "base": "int",
                "kind": "bounded",
                "lower-bound": 0,
                "upper-bound": 1
            }
        }
    ]
}