1		:- dynamic parserVersionNum/1, parserVersionStr/1, parseResult/5.
2		:- dynamic module/4.
3		'parserVersionStr'('0.6.2.1').
4		'parseResult'('ok','',0,0,0).
5		:- dynamic channel/2, bindval/3, agent/3.
6		:- dynamic agent_curry/3, symbol/4.
7		:- dynamic dataTypeDef/2, subTypeDef/2, nameType/2.
8		:- dynamic cspTransparent/1.
9		:- dynamic cspPrint/1.
10		:- dynamic pragma/1.
11		:- dynamic comment/2.
12		:- dynamic assertBool/1, assertRef/5, assertTauPrio/6.
13		:- dynamic assertModelCheckExt/4, assertModelCheck/3.
14		:- dynamic assertLtl/4, assertCtl/4.
15		'parserVersionNum'([0,11,1,1]).
16		'parserVersionStr'('CSPM-Frontent-0.11.1.1').
17		'bindval'('N','int'(3),'src_span'(11,1,11,4,260,3)).
18		'bindval'('T1','int'(1),'src_span'(13,1,13,7,265,6)).
19		'bindval'('T2','int'(3),'src_span'(14,1,14,7,272,6)).
20		'bindval'('TS','int'(7),'src_span'(15,1,15,7,279,6)).
21		'bindval'('Proc1','setExp'('rangeClosed'('int'(0),'-'('val_of'('N','src_span'(17,13,17,14,299,1)),'int'(1)))),'src_span'(17,1,17,17,287,16)).
22		'agent'('above'(_n),'setExp'('rangeEnum'([_k]),['comprehensionGenerator'(_k,'val_of'('Proc1','src_span'(22,22,22,27,457,5))),'comprehensionGuard'('>'(_k,_n))]),'src_span'(22,12,22,33,447,21)).
23		'agent'('below'(_n2),'setExp'('rangeEnum'([_k2]),['comprehensionGenerator'(_k2,'val_of'('Proc1','src_span'(23,22,23,27,490,5))),'comprehensionGuard'('<'(_k2,_n2))]),'src_span'(23,12,23,33,480,21)).
24		'channel'('election','type'('dotTupleType'(['val_of'('Proc1','src_span'(27,18,27,23,568,5)),'val_of'('Proc1','src_span'(27,24,27,29,574,5))]))).
25		'channel'('answer','type'('dotTupleType'(['val_of'('Proc1','src_span'(29,16,29,21,596,5)),'val_of'('Proc1','src_span'(29,22,29,27,602,5))]))).
26		'channel'('coordinator','type'('dotTupleType'(['val_of'('Proc1','src_span'(31,21,31,26,629,5)),'val_of'('Proc1','src_span'(31,27,31,32,635,5))]))).
27		'channel'('fail','type'('dotTupleType'(['val_of'('Proc1','src_span'(33,22,33,27,663,5))]))).
28		'channel'('revive','type'('dotTupleType'(['val_of'('Proc1','src_span'(33,22,33,27,663,5))]))).
29		'channel'('test','type'('dotTupleType'(['val_of'('Proc1','src_span'(35,17,35,22,686,5)),'val_of'('Proc1','src_span'(35,23,35,28,692,5))]))).
30		'channel'('ok','type'('dotTupleType'(['val_of'('Proc1','src_span'(35,17,35,22,686,5)),'val_of'('Proc1','src_span'(35,23,35,28,692,5))]))).
31		'channel'('leader','type'('dotTupleType'(['val_of'('Proc1','src_span'(37,16,37,21,714,5)),'val_of'('Proc1','src_span'(37,22,37,27,720,5))]))).
32		'channel'('tock','type'('dotUnitType')).
33		'agent'('BeginElection'(_n3),'agent_call'('src_span'(44,20,44,33,868,13),'SendElections',['-'('val_of'('N','src_span'(44,34,44,35,882,1)),'int'(1)),_n3]),'src_span'(44,20,44,40,868,20)).
34		'agent'('SendElections'(_k3,_n4),'[]'('[]'('[]'('[]'('[]'('[]'('ifte'('<='(_k3,_n4),'agent_call'('src_span'(50,36,50,48,1111,12),'AwaitAnswers',['val_of'('T1','src_span'(50,49,50,51,1124,2)),_n4]),'prefix'('src_span'(51,27,51,39,1156,12),[],'dotTuple'(['election',_n4,_k3]),'agent_call'('src_span'(51,43,51,56,1172,13),'SendElections',['-'(_k3,'int'(1)),_n4]),'src_span'(51,40,51,42,1168,36)),'no_loc_info_available','no_loc_info_available','src_span'(50,55,51,26,1129,81)),'prefix'('src_span'(52,24,52,32,1217,8),['inGuard'(_k_quote,'agent_call'('src_span'(52,36,52,41,1229,5),'below',[_n4])),'out'(_n4)],'election','prefix'('src_span'(52,49,52,60,1242,11),[],'dotTuple'(['answer',_n4,_k_quote]),'agent_call'('src_span'(52,63,52,76,1256,13),'SendElections',[_k3,_n4]),'src_span'(52,61,52,62,1253,32)),'src_span'(52,47,52,48,1239,37)),'src_span_operator'('no_loc_info_available','src_span'(52,21,52,23,1214,2))),'prefix'('src_span'(53,24,53,30,1298,6),['inGuard'(_k4,'agent_call'('src_span'(53,33,53,38,1307,5),'above',[_n4])),'out'(_n4)],'answer','agent_call'('src_span'(53,47,53,63,1321,16),'AwaitCoordinator',['val_of'('T2','src_span'(53,64,53,66,1338,2)),_n4]),'src_span'(53,44,53,46,1317,28)),'src_span_operator'('no_loc_info_available','src_span'(53,21,53,23,1295,2))),'prefix'('src_span'(54,24,54,26,1367,2),['inGuard'(_k_quote2,'agent_call'('src_span'(54,30,54,35,1373,5),'above',[_n4])),'out'(_n4)],'ok','agent_call'('src_span'(54,44,54,57,1387,13),'SendElections',[_k3,_n4]),'src_span'(54,41,54,43,1383,24)),'src_span_operator'('no_loc_info_available','src_span'(54,21,54,23,1364,2))),'prefix'('src_span'(55,24,55,35,1429,11),['inGuard'(_k5,'agent_call'('src_span'(55,38,55,43,1443,5),'above',[_n4])),'out'(_n4)],'coordinator','agent_call'('src_span'(55,52,55,60,1457,8),'Running\x27\',[_n4,_k5]),'src_span'(55,49,55,51,1453,19)),'src_span_operator'('no_loc_info_available','src_span'(55,21,55,23,1426,2))),'prefix'('src_span'(56,10,56,16,1480,6),[],'dotTuple'(['fail',_n4]),'agent_call'('src_span'(56,20,56,26,1490,6),'Failed',[_n4]),'src_span'(56,17,56,19,1486,19)),'src_span_operator'('no_loc_info_available','src_span'(56,7,56,9,1477,2))),'prefix'('src_span'(57,24,57,28,1523,4),['inGuard'(_k_quote3,'agent_call'('src_span'(57,32,57,37,1531,5),'below',[_n4])),'out'(_n4)],'test','agent_call'('src_span'(57,48,57,61,1547,13),'SendElections',[_k3,_n4]),'src_span'(57,43,57,47,1541,26)),'src_span_operator'('no_loc_info_available','src_span'(57,21,57,23,1520,2))),'no_loc_info_available').
35		'agent'('AwaitAnswers'(_t,_n5),'ifte'('=='(_t,'int'(0)),'agent_call'('src_span'(62,34,62,51,1743,17),'BecomeCoordinator',[_n5]),'[]'('[]'('[]'('[]'('[]'('[]'('prefix'('src_span'(64,21,64,25,1817,4),[],'tock','agent_call'('src_span'(64,29,64,41,1825,12),'AwaitAnswers',['-'(_t,'int'(1)),_n5]),'src_span'(64,26,64,28,1821,27)),'prefix'('src_span'(65,21,65,27,1865,6),['inGuard'(_k6,'agent_call'('src_span'(65,30,65,35,1874,5),'above',[_n5])),'out'(_n5)],'answer','agent_call'('src_span'(65,44,65,60,1888,16),'AwaitCoordinator',['val_of'('T2','src_span'(65,61,65,63,1905,2)),_n5]),'src_span'(65,41,65,43,1884,28)),'src_span_operator'('no_loc_info_available','src_span'(65,18,65,20,1862,2))),'prefix'('src_span'(66,21,66,23,1931,2),['inGuard'(_k7,'agent_call'('src_span'(66,26,66,31,1936,5),'above',[_n5])),'out'(_n5)],'ok','agent_call'('src_span'(66,40,66,52,1950,12),'AwaitAnswers',[_t,_n5]),'src_span'(66,37,66,39,1946,23)),'src_span_operator'('no_loc_info_available','src_span'(66,18,66,20,1928,2))),'prefix'('src_span'(67,21,67,29,1988,8),['inGuard'(_k8,'agent_call'('src_span'(67,32,67,37,1999,5),'below',[_n5])),'out'(_n5)],'election','prefix'('src_span'(67,46,67,56,2013,10),[],'dotTuple'(['answer',_n5,_k8]),'agent_call'('src_span'(67,60,67,72,2027,12),'AwaitAnswers',[_t,_n5]),'src_span'(67,57,67,59,2023,31)),'src_span'(67,43,67,45,2009,37)),'src_span_operator'('no_loc_info_available','src_span'(67,18,67,20,1985,2))),'prefix'('src_span'(68,21,68,32,2065,11),['inGuard'(_k9,'agent_call'('src_span'(68,35,68,40,2079,5),'above',[_n5])),'out'(_n5)],'coordinator','agent_call'('src_span'(68,49,68,57,2093,8),'Running\x27\',[_n5,_k9]),'src_span'(68,46,68,48,2089,19)),'src_span_operator'('no_loc_info_available','src_span'(68,18,68,20,2062,2))),'prefix'('src_span'(69,10,69,16,2116,6),[],'dotTuple'(['fail',_n5]),'agent_call'('src_span'(69,20,69,26,2126,6),'Failed',[_n5]),'src_span'(69,17,69,19,2122,19)),'src_span_operator'('no_loc_info_available','src_span'(69,7,69,9,2113,2))),'prefix'('src_span'(70,24,70,28,2159,4),['inGuard'(_k73,'agent_call'('src_span'(70,31,70,36,2166,5),'below',[_n5])),'out'(_n5)],'test','agent_call'('src_span'(70,47,70,59,2182,12),'AwaitAnswers',[_t,_n5]),'src_span'(70,42,70,46,2176,25)),'src_span_operator'('no_loc_info_available','src_span'(70,21,70,23,2156,2))),'no_loc_info_available','no_loc_info_available','no_loc_info_available'),'src_span'(62,21,70,64,1730,469)).
36		'agent'('AwaitCoordinator'(_t2,_n6),'ifte'('=='(_t2,'int'(0)),'agent_call'('src_span'(77,38,77,51,2428,13),'BeginElection',[_n6]),'[]'('[]'('[]'('[]'('[]'('[]'('prefix'('src_span'(79,25,79,29,2506,4),[],'tock','agent_call'('src_span'(79,32,79,48,2513,16),'AwaitCoordinator',['-'(_t2,'int'(1)),_n6]),'src_span'(79,30,79,31,2510,30)),'prefix'('src_span'(80,25,80,36,2561,11),['inGuard'(_k76,'agent_call'('src_span'(80,39,80,44,2575,5),'above',[_n6])),'out'(_n6)],'coordinator','agent_call'('src_span'(80,53,80,61,2589,8),'Running\x27\',[_n6,_k76]),'src_span'(80,50,80,52,2585,19)),'src_span_operator'('no_loc_info_available','src_span'(80,21,80,23,2557,2))),'prefix'('src_span'(81,24,81,30,2626,6),['inGuard'(_k77,'agent_call'('src_span'(81,33,81,38,2635,5),'above',[_n6])),'out'(_n6)],'answer','agent_call'('src_span'(81,47,81,63,2649,16),'AwaitCoordinator',[_t2,_n6]),'src_span'(81,44,81,46,2645,27)),'src_span_operator'('no_loc_info_available','src_span'(81,21,81,23,2623,2))),'prefix'('src_span'(82,24,82,26,2694,2),['inGuard'(_k78,'agent_call'('src_span'(82,29,82,34,2699,5),'above',[_n6])),'out'(_n6)],'ok','agent_call'('src_span'(82,43,82,59,2713,16),'AwaitCoordinator',[_t2,_n6]),'src_span'(82,40,82,42,2709,27)),'src_span_operator'('no_loc_info_available','src_span'(82,21,82,23,2691,2))),'prefix'('src_span'(83,24,83,32,2758,8),['inGuard'(_k79,'agent_call'('src_span'(83,35,83,40,2769,5),'below',[_n6])),'out'(_n6)],'election','prefix'('src_span'(83,49,83,59,2783,10),[],'dotTuple'(['answer',_n6,_k79]),'agent_call'('src_span'(84,43,84,59,2840,16),'AwaitCoordinator',[_t2,_n6]),'src_span'(83,60,84,42,2793,78)),'src_span'(83,46,83,48,2779,84)),'src_span_operator'('no_loc_info_available','src_span'(83,21,83,23,2755,2))),'prefix'('src_span'(85,10,85,16,2871,6),[],'dotTuple'(['fail',_n6]),'agent_call'('src_span'(85,20,85,26,2881,6),'Failed',[_n6]),'src_span'(85,17,85,19,2877,19)),'src_span_operator'('no_loc_info_available','src_span'(85,7,85,9,2868,2))),'prefix'('src_span'(86,24,86,28,2914,4),['inGuard'(_k80,'agent_call'('src_span'(86,31,86,36,2921,5),'below',[_n6])),'out'(_n6)],'test','agent_call'('src_span'(86,47,86,63,2937,16),'AwaitCoordinator',[_t2,_n6]),'src_span'(86,42,86,46,2931,29)),'src_span_operator'('no_loc_info_available','src_span'(86,21,86,23,2911,2))),'no_loc_info_available','no_loc_info_available','no_loc_info_available'),'src_span'(77,25,86,68,2415,543)).
37		'agent'('BecomeCoordinator'(_n7),'agent_call'('src_span'(91,24,91,34,3100,10),'SendCoords',['-'(_n7,'int'(1)),_n7]),'src_span'(91,24,91,41,3100,17)).
38		'agent'('SendCoords'(_j,_n8),'ifte'('<'(_j,'int'(0)),'agent_call'('src_span'(97,31,97,41,3325,10),'RunAsCoord',[_n8]),'[]'('[]'('[]'('[]'('prefix'('src_span'(98,24,98,39,3362,15),[],'dotTuple'(['coordinator',_n8,_j]),'agent_call'('src_span'(98,43,98,53,3381,10),'SendCoords',['-'(_j,'int'(1)),_n8]),'src_span'(98,40,98,42,3377,36)),'prefix'('src_span'(99,22,99,30,3420,8),['inGuard'(_k84,'agent_call'('src_span'(99,33,99,38,3431,5),'below',[_n8])),'out'(_n8)],'election','prefix'('src_span'(99,47,99,62,3445,15),[],'dotTuple'(['coordinator',_n8,_k84]),'agent_call'('src_span'(99,66,99,76,3464,10),'SendCoords',[_j,_n8]),'src_span'(99,63,99,65,3460,34)),'src_span'(99,44,99,46,3441,40)),'src_span_operator'('no_loc_info_available','src_span'(99,19,99,21,3417,2))),'prefix'('src_span'(100,22,100,33,3501,11),['inGuard'(_k85,'agent_call'('src_span'(100,36,100,41,3515,5),'above',[_n8])),'out'(_n8)],'coordinator','agent_call'('src_span'(100,50,100,58,3529,8),'Running\x27\',[_n8,_k85]),'src_span'(100,47,100,49,3525,19)),'src_span_operator'('no_loc_info_available','src_span'(100,19,100,21,3498,2))),'prefix'('src_span'(101,22,101,28,3564,6),[],'dotTuple'(['fail',_n8]),'agent_call'('src_span'(101,32,101,38,3574,6),'Failed',[_n8]),'src_span'(101,29,101,31,3570,19)),'src_span_operator'('no_loc_info_available','src_span'(101,19,101,21,3561,2))),'prefix'('src_span'(102,22,102,26,3605,4),['inGuard'(_k86,'agent_call'('src_span'(102,29,102,34,3612,5),'below',[_n8])),'out'(_n8)],'test','prefix'('src_span'(102,44,102,50,3627,6),[],'dotTuple'(['ok',_n8,_k86]),'agent_call'('src_span'(102,54,102,64,3637,10),'SendCoords',[_j,_n8]),'src_span'(102,51,102,53,3633,25)),'src_span'(102,40,102,43,3622,32)),'src_span_operator'('no_loc_info_available','src_span'(102,19,102,21,3602,2))),'no_loc_info_available','no_loc_info_available','no_loc_info_available'),'src_span'(97,19,102,69,3313,339)).
39		'agent'('RunAsCoord'(_n9),'[]'('[]'('[]'('prefix'('src_span'(108,22,108,26,3797,4),['inGuard'(_k88,'agent_call'('src_span'(108,29,108,34,3804,5),'below',[_n9])),'out'(_n9)],'test','prefix'('src_span'(108,43,108,49,3818,6),[],'dotTuple'(['ok',_n9,_k88]),'agent_call'('src_span'(108,53,108,63,3828,10),'RunAsCoord',[_n9]),'src_span'(108,50,108,52,3824,23)),'src_span'(108,40,108,42,3814,29)),'prefix'('src_span'(109,22,109,33,3863,11),['inGuard'(_k89,'agent_call'('src_span'(109,36,109,41,3877,5),'above',[_n9])),'out'(_n9)],'coordinator','agent_call'('src_span'(109,50,109,58,3891,8),'Running\x27\',[_n9,_k89]),'src_span'(109,47,109,49,3887,19)),'src_span_operator'('no_loc_info_available','src_span'(109,19,109,21,3860,2))),'prefix'('src_span'(110,22,110,30,3926,8),['inGuard'(_k90,'agent_call'('src_span'(110,33,110,38,3937,5),'below',[_n9])),'out'(_n9)],'election','prefix'('src_span'(110,47,110,57,3951,10),[],'dotTuple'(['answer',_n9,_k90]),'agent_call'('src_span'(110,61,110,74,3965,13),'BeginElection',[_n9]),'src_span'(110,58,110,60,3961,30)),'src_span'(110,44,110,46,3947,36)),'src_span_operator'('no_loc_info_available','src_span'(110,19,110,21,3923,2))),'prefix'('src_span'(111,22,111,28,4003,6),[],'dotTuple'(['fail',_n9]),'agent_call'('src_span'(111,32,111,38,4013,6),'Failed',[_n9]),'src_span'(111,29,111,31,4009,19)),'src_span_operator'('no_loc_info_available','src_span'(111,19,111,21,4000,2))),'no_loc_info_available').
40		'agent'('Running'(_n91,_k92),'[]'('[]'('[]'('[]'('[]'('prefix'('src_span'(116,19,116,27,4129,8),[],'dotTuple'(['test',_n91,_k92]),'agent_call'('src_span'(116,31,116,38,4141,7),'Testing',[_n91,_k92]),'src_span'(116,28,116,30,4137,24)),'prefix'('src_span'(118,22,118,33,4219,11),['inGuard'(_k93,'agent_call'('src_span'(118,36,118,41,4233,5),'above',[_n91])),'out'(_n91)],'coordinator','agent_call'('src_span'(118,50,118,58,4247,8),'Running\x27\',[_n91,_k93]),'src_span'(118,47,118,49,4243,19)),'src_span_operator'('no_loc_info_available','src_span'(118,19,118,21,4216,2))),'prefix'('src_span'(119,22,119,28,4282,6),['inGuard'(_j2,'agent_call'('src_span'(119,31,119,36,4291,5),'above',[_n91])),'out'(_n91)],'answer','agent_call'('src_span'(119,46,119,53,4306,7),'Running',[_n91,_k92]),'src_span'(119,42,119,45,4301,19)),'src_span_operator'('no_loc_info_available','src_span'(119,19,119,21,4279,2))),'prefix'('src_span'(121,22,121,30,4376,8),['inGuard'(_k95,'agent_call'('src_span'(121,33,121,38,4387,5),'below',[_n91])),'out'(_n91)],'election','prefix'('src_span'(121,47,121,57,4401,10),[],'dotTuple'(['answer',_n91,_k95]),'agent_call'('src_span'(121,61,121,74,4415,13),'BeginElection',[_n91]),'src_span'(121,58,121,60,4411,30)),'src_span'(121,44,121,46,4397,36)),'src_span_operator'('no_loc_info_available','src_span'(121,19,121,21,4373,2))),'prefix'('src_span'(122,22,122,26,4453,4),['inGuard'(_j3,'agent_call'('src_span'(122,29,122,34,4460,5),'below',[_n91])),'out'(_n91)],'test','agent_call'('src_span'(122,44,122,51,4475,7),'Running',[_n91,_k92]),'src_span'(122,40,122,43,4470,19)),'src_span_operator'('no_loc_info_available','src_span'(122,19,122,21,4450,2))),'prefix'('src_span'(123,22,123,28,4509,6),[],'dotTuple'(['fail',_n91]),'agent_call'('src_span'(123,32,123,38,4519,6),'Failed',[_n91]),'src_span'(123,29,123,31,4515,19)),'src_span_operator'('no_loc_info_available','src_span'(123,19,123,21,4506,2))),'no_loc_info_available').
41		'agent'('Testing'(_n97,_k98),'[]'('[]'('[]'('[]'('[]'('[]'('prefix'('src_span'(129,22,129,28,4730,6),[],'dotTuple'(['ok',_k98,_n97]),'agent_call'('src_span'(129,32,129,40,4740,8),'Running\x27\',[_n97,_k98]),'src_span'(129,29,129,31,4736,23)),'prefix'('src_span'(130,22,130,26,4775,4),[],'tock','agent_call'('src_span'(130,30,130,43,4783,13),'BeginElection',[_n97]),'src_span'(130,27,130,29,4779,24)),'src_span_operator'('no_loc_info_available','src_span'(130,19,130,21,4772,2))),'prefix'('src_span'(131,22,131,28,4821,6),['inGuard'(_j4,'agent_call'('src_span'(131,31,131,36,4830,5),'above',[_n97])),'out'(_n97)],'answer','agent_call'('src_span'(131,46,131,53,4845,7),'Testing',[_n97,_k98]),'src_span'(131,42,131,45,4840,19)),'src_span_operator'('no_loc_info_available','src_span'(131,19,131,21,4818,2))),'prefix'('src_span'(132,22,132,33,4879,11),['inGuard'(_k100,'agent_call'('src_span'(132,36,132,41,4893,5),'above',[_n97])),'out'(_n97)],'coordinator','agent_call'('src_span'(132,50,132,58,4907,8),'Running\x27\',[_n97,_k100]),'src_span'(132,47,132,49,4903,19)),'src_span_operator'('no_loc_info_available','src_span'(132,19,132,21,4876,2))),'prefix'('src_span'(133,22,133,30,4942,8),['inGuard'(_k101,'agent_call'('src_span'(133,33,133,38,4953,5),'below',[_n97])),'out'(_n97)],'election','prefix'('src_span'(133,47,133,57,4967,10),[],'dotTuple'(['answer',_n97,_k101]),'agent_call'('src_span'(133,61,133,74,4981,13),'BeginElection',[_n97]),'src_span'(133,58,133,60,4977,30)),'src_span'(133,44,133,46,4963,36)),'src_span_operator'('no_loc_info_available','src_span'(133,19,133,21,4939,2))),'prefix'('src_span'(134,22,134,28,5019,6),[],'dotTuple'(['fail',_n97]),'agent_call'('src_span'(134,32,134,38,5029,6),'Failed',[_n97]),'src_span'(134,29,134,31,5025,19)),'src_span_operator'('no_loc_info_available','src_span'(134,19,134,21,5016,2))),'prefix'('src_span'(135,22,135,26,5060,4),['inGuard'(_j5,'agent_call'('src_span'(135,29,135,34,5067,5),'below',[_n97])),'out'(_n97)],'test','agent_call'('src_span'(135,44,135,51,5082,7),'Testing',[_n97,_k98]),'src_span'(135,40,135,43,5077,19)),'src_span_operator'('no_loc_info_available','src_span'(135,19,135,21,5057,2))),'no_loc_info_available').
42		'agent'('Running\x27\'(_n103,_k104),'[]'('[]'('[]'('[]'('[]'('[]'('prefix'('src_span'(142,19,142,23,5341,4),[],'tock','agent_call'('src_span'(142,27,142,34,5349,7),'Running',[_n103,_k104]),'src_span'(142,24,142,26,5345,20)),'prefix'('src_span'(143,22,143,33,5383,11),['inGuard'(_k105,'agent_call'('src_span'(143,36,143,41,5397,5),'above',[_n103])),'out'(_n103)],'coordinator','agent_call'('src_span'(143,50,143,58,5411,8),'Running\x27\',[_n103,_k105]),'src_span'(143,47,143,49,5407,19)),'src_span_operator'('no_loc_info_available','src_span'(143,19,143,21,5380,2))),'prefix'('src_span'(144,22,144,28,5446,6),['inGuard'(_j6,'agent_call'('src_span'(144,31,144,36,5455,5),'above',[_n103])),'out'(_n103)],'answer','agent_call'('src_span'(144,46,144,54,5470,8),'Running\x27\',[_n103,_k104]),'src_span'(144,42,144,45,5465,20)),'src_span_operator'('no_loc_info_available','src_span'(144,19,144,21,5443,2))),'prefix'('src_span'(145,22,145,30,5505,8),['inGuard'(_k107,'agent_call'('src_span'(145,33,145,38,5516,5),'below',[_n103])),'out'(_n103)],'election','prefix'('src_span'(145,47,145,57,5530,10),[],'dotTuple'(['answer',_n103,_k107]),'agent_call'('src_span'(145,61,145,74,5544,13),'BeginElection',[_n103]),'src_span'(145,58,145,60,5540,30)),'src_span'(145,44,145,46,5526,36)),'src_span_operator'('no_loc_info_available','src_span'(145,19,145,21,5502,2))),'prefix'('src_span'(146,22,146,28,5582,6),[],'dotTuple'(['fail',_n103]),'agent_call'('src_span'(146,32,146,38,5592,6),'Failed',[_n103]),'src_span'(146,29,146,31,5588,19)),'src_span_operator'('no_loc_info_available','src_span'(146,19,146,21,5579,2))),'prefix'('src_span'(148,22,148,26,5660,4),['inGuard'(_j7,'agent_call'('src_span'(148,29,148,34,5667,5),'below',[_n103])),'out'(_n103)],'test','agent_call'('src_span'(148,44,148,52,5682,8),'Running\x27\',[_n103,_k104]),'src_span'(148,40,148,43,5677,20)),'src_span_operator'('no_loc_info_available','src_span'(148,19,148,21,5657,2))),'prefix'('src_span'(149,22,149,24,5717,2),['inGuard'(_j8,'agent_call'('src_span'(149,27,149,32,5722,5),'above',[_n103])),'out'(_n103)],'ok','agent_call'('src_span'(149,41,149,49,5736,8),'Running\x27\',[_n103,_k104]),'src_span'(149,38,149,40,5732,19)),'src_span_operator'('no_loc_info_available','src_span'(149,19,149,21,5714,2))),'no_loc_info_available').
43		'agent'('Failed'(_n110),'[]'('[]'('[]'('[]'('[]'('[]'('prefix'('src_span'(153,13,153,17,5813,4),[],'tock','agent_call'('src_span'(153,21,153,28,5821,7),'Failed\x27\',[_n110]),'src_span'(153,18,153,20,5817,18)),'prefix'('src_span'(154,16,154,27,5847,11),['inGuard'(_k111,'agent_call'('src_span'(154,30,154,35,5861,5),'above',[_n110])),'out'(_n110)],'coordinator','agent_call'('src_span'(154,44,154,50,5875,6),'Failed',[_n110]),'src_span'(154,41,154,43,5871,15)),'src_span_operator'('no_loc_info_available','src_span'(154,13,154,15,5844,2))),'prefix'('src_span'(155,16,155,24,5900,8),['inGuard'(_k112,'agent_call'('src_span'(155,27,155,32,5911,5),'below',[_n110])),'out'(_n110)],'election','agent_call'('src_span'(155,41,155,47,5925,6),'Failed',[_n110]),'src_span'(155,38,155,40,5921,15)),'src_span_operator'('no_loc_info_available','src_span'(155,13,155,15,5897,2))),'prefix'('src_span'(156,16,156,20,5950,4),['inGuard'(_k113,'agent_call'('src_span'(156,23,156,28,5957,5),'below',[_n110])),'out'(_n110)],'test','agent_call'('src_span'(156,38,156,44,5972,6),'Failed',[_n110]),'src_span'(156,34,156,37,5967,16)),'src_span_operator'('no_loc_info_available','src_span'(156,13,156,15,5947,2))),'prefix'('src_span'(157,16,157,18,5997,2),['inGuard'(_k114,'agent_call'('src_span'(157,21,157,26,6002,5),'above',[_n110])),'out'(_n110)],'ok','agent_call'('src_span'(157,36,157,42,6017,6),'Failed',[_n110]),'src_span'(157,32,157,35,6012,16)),'src_span_operator'('no_loc_info_available','src_span'(157,13,157,15,5994,2))),'prefix'('src_span'(158,16,158,22,6042,6),['inGuard'(_k115,'agent_call'('src_span'(158,25,158,30,6051,5),'above',[_n110])),'out'(_n110)],'answer','agent_call'('src_span'(158,40,158,46,6066,6),'Failed',[_n110]),'src_span'(158,36,158,39,6061,16)),'src_span_operator'('no_loc_info_available','src_span'(158,13,158,15,6039,2))),'prefix'('src_span'(159,16,159,22,6091,6),[],'dotTuple'(['fail',_n110]),'agent_call'('src_span'(159,26,159,32,6101,6),'Failed',[_n110]),'src_span'(159,23,159,25,6097,19)),'src_span_operator'('no_loc_info_available','src_span'(159,13,159,15,6088,2))),'no_loc_info_available').
44		'agent'('Failed\x27\'(_n116),'[]'('[]'('[]'('[]'('[]'('[]'('prefix'('src_span'(165,16,165,27,6235,11),['inGuard'(_k117,'agent_call'('src_span'(165,30,165,35,6249,5),'above',[_n116])),'out'(_n116)],'coordinator','agent_call'('src_span'(165,44,165,51,6263,7),'Failed\x27\',[_n116]),'src_span'(165,41,165,43,6259,16)),'prefix'('src_span'(166,16,166,24,6289,8),['inGuard'(_k118,'agent_call'('src_span'(166,27,166,32,6300,5),'below',[_n116])),'out'(_n116)],'election','agent_call'('src_span'(166,41,166,48,6314,7),'Failed\x27\',[_n116]),'src_span'(166,38,166,40,6310,16)),'src_span_operator'('no_loc_info_available','src_span'(166,13,166,15,6286,2))),'prefix'('src_span'(167,16,167,20,6340,4),['inGuard'(_k119,'agent_call'('src_span'(167,23,167,28,6347,5),'below',[_n116])),'out'(_n116)],'test','agent_call'('src_span'(167,38,167,45,6362,7),'Failed\x27\',[_n116]),'src_span'(167,34,167,37,6357,17)),'src_span_operator'('no_loc_info_available','src_span'(167,13,167,15,6337,2))),'prefix'('src_span'(168,16,168,18,6388,2),['inGuard'(_k120,'agent_call'('src_span'(168,21,168,26,6393,5),'above',[_n116])),'out'(_n116)],'ok','agent_call'('src_span'(168,36,168,43,6408,7),'Failed\x27\',[_n116]),'src_span'(168,32,168,35,6403,17)),'src_span_operator'('no_loc_info_available','src_span'(168,13,168,15,6385,2))),'prefix'('src_span'(169,16,169,22,6434,6),['inGuard'(_k121,'agent_call'('src_span'(169,25,169,30,6443,5),'above',[_n116])),'out'(_n116)],'answer','agent_call'('src_span'(169,40,169,47,6458,7),'Failed\x27\',[_n116]),'src_span'(169,36,169,39,6453,17)),'src_span_operator'('no_loc_info_available','src_span'(169,13,169,15,6431,2))),'prefix'('src_span'(170,16,170,22,6484,6),[],'dotTuple'(['fail',_n116]),'agent_call'('src_span'(170,26,170,32,6494,6),'Failed',[_n116]),'src_span'(170,23,170,25,6490,19)),'src_span_operator'('no_loc_info_available','src_span'(170,13,170,15,6481,2))),'prefix'('src_span'(171,16,171,24,6519,8),[],'dotTuple'(['revive',_n116]),'ifte'('=='(_n116,'-'('val_of'('N','src_span'(171,35,171,36,6538,1)),'int'(1))),'agent_call'('src_span'(171,44,171,61,6547,17),'BecomeCoordinator',[_n116]),'agent_call'('src_span'(172,37,172,50,6604,13),'BeginElection',[_n116]),'no_loc_info_available','no_loc_info_available','src_span'(171,65,172,36,6567,73)),'src_span'(171,25,171,27,6527,102)),'src_span_operator'('no_loc_info_available','src_span'(171,13,171,15,6516,2))),'no_loc_info_available').
45		'cspTransparent'(['normal']).
46		'agent'('Alpha'(_n122),'agent_call'('src_span'(180,12,180,17,6770,5),'union',['closure'(['tock','dotTuple'(['fail',_n122]),'dotTuple'(['revive',_n122]),'dotTuple'(['election',_n122]),'dotTuple'(['coordinator',_n122]),'dotTuple'(['test',_n122]),'dotTuple'(['answer',_n122]),'dotTuple'(['leader',_n122]),'dotTuple'(['ok',_n122])]),'setExp'('rangeEnum'(['dotTuple'(['election',_k123,_n122]),'dotTuple'(['coordinator',_k123,_n122]),'dotTuple'(['test',_k123,_n122]),'dotTuple'(['answer',_k123,_n122]),'dotTuple'(['ok',_k123,_n122])]),['comprehensionGenerator'(_k123,'val_of'('Proc1','src_span'(183,40,183,45,6960,5)))])]),'src_span'(180,12,183,47,6770,197)).
47		'agent'('Node'(_n124),'agent_call'('src_span'(185,11,185,17,6979,6),'normal',['ifte'('=='(_n124,'-'('val_of'('N','src_span'(185,24,185,25,6992,1)),'int'(1))),'agent_call'('src_span'(185,33,185,43,7001,10),'RunAsCoord',[_n124]),'agent_call'('src_span'(185,52,185,59,7020,7),'Running',[_n124,'-'('val_of'('N','src_span'(185,62,185,63,7030,1)),'int'(1))]),'no_loc_info_available','no_loc_info_available','src_span'(185,47,185,51,7014,33))]),'src_span'(185,11,185,67,6979,56)).
48		'bindval'('Network','procRepAParallel'(['comprehensionGenerator'(_n125,'val_of'('Proc1','src_span'(187,16,187,21,7052,5)))],'pair'('agent_call'('src_span'(187,25,187,30,7061,5),'Alpha',[_n125]),'agent_call'('src_span'(187,35,187,39,7071,4),'Node',[_n125])),'src_span'(187,14,187,23,7050,9)),'src_span'(187,1,187,42,7037,41)).
49		'assertLtl'('False','val_of'('Network','src_span'(189,8,189,15,7087,7)),'WEF => G ([fail.2] => F [coordinator.1.2])','src_span'(189,1,189,68,7080,67)).
50		'assertLtl'('False','val_of'('Network','src_span'(191,8,191,15,7156,7)),'SEF => G ([fail.2] => F [coordinator.1.2])','src_span'(191,1,191,68,7149,67)).
51		'bindval'('Delayable','closure'(['fail','revive','leader','test']),'src_span'(199,1,199,43,7540,42)).
52		'bindval'('Urgent','agent_call'('src_span'(200,10,200,14,7592,4),'diff',['Events','agent_call'('src_span'(200,22,200,27,7604,5),'union',['setExp'('rangeEnum'(['tock'])),'val_of'('Delayable','src_span'(200,35,200,44,7617,9))])]),'src_span'(200,1,200,46,7583,45)).
53		'bindval'('TOCKS','prefix'('src_span'(212,9,212,13,8052,4),[],'tock','val_of'('TOCKS','src_span'(212,17,212,22,8060,5)),'src_span'(212,14,212,16,8056,13)),'src_span'(212,1,212,22,8044,21)).
54		'agent'('max'(_S),'let'(['agent'('pick'('singleSetPat'([_x])),_x,'src_span'(217,26,217,27,8232,1))],'agent_call'('src_span'(218,10,218,14,8250,4),'pick',['setExp'('rangeEnum'([_x2]),['comprehensionGenerator'(_x2,_S),'comprehensionGuard'('=='('setExp'('rangeEnum'([_y]),['comprehensionGenerator'(_y,_S),'comprehensionGuard'('>'(_y,_x2))]),'setExp'('rangeEnum'([]))))])])),'src_span'(217,10,218,55,8216,79)).
55		'agent'('AGREEBY'('int'(0),_alive),'[]'('[]'('[]'('[]'('&'('!='(_alive,'setExp'('rangeEnum'([]))),'prefix'('src_span'(228,34,228,40,8682,6),['inGuard'(_m,_alive),'out'('agent_call'('src_span'(228,49,228,52,8697,3),'max',[_alive]))],'leader','agent_call'('src_span'(228,63,228,70,8711,7),'AGREEBY',['int'(0),_alive]),'src_span'(228,60,228,62,8707,31))),'prefix'('src_span'(229,16,229,20,8743,4),[],'tock','agent_call'('src_span'(229,24,229,31,8751,7),'AGREEBY',['int'(0),_alive]),'src_span'(229,21,229,23,8747,24)),'src_span_operator'('no_loc_info_available','src_span'(229,13,229,15,8740,2))),'prefix'('src_span'(230,9,230,13,8776,4),['in'(_k133)],'fail','agent_call'('src_span'(230,19,230,27,8786,8),'AGREEBY\x27\',['agent_call'('src_span'(230,28,230,32,8795,4),'diff',[_alive,'setExp'('rangeEnum'([_k133]))])]),'src_span'(230,16,230,18,8782,31)),'src_span_operator'('no_loc_info_available','src_span'(230,6,230,8,8773,2))),'prefix'('src_span'(231,9,231,15,8820,6),['in'(_k134)],'revive','agent_call'('src_span'(231,21,231,28,8832,7),'AGREEBY',['val_of'('TS','src_span'(231,29,231,31,8840,2)),'agent_call'('src_span'(231,32,231,37,8843,5),'union',[_alive,'setExp'('rangeEnum'([_k134]))])]),'src_span'(231,18,231,20,8828,34)),'src_span_operator'('no_loc_info_available','src_span'(231,6,231,8,8817,2))),'prefix'('src_span'(232,16,232,20,8876,4),['in'(_n135),'in'(_k136)],'test','agent_call'('src_span'(232,28,232,35,8888,7),'AGREEBY',['int'(0),_alive]),'src_span'(232,25,232,27,8884,22)),'src_span_operator'('no_loc_info_available','src_span'(232,13,232,15,8873,2))),'no_loc_info_available').
56		'agent'('AGREEBY'(_n137,_alive2),'[]'('[]'('[]'('[]'('prefix'('src_span'(237,21,237,27,9011,6),['in'(_m2),'in'(_k140)],'leader','agent_call'('src_span'(237,35,237,42,9025,7),'AGREEBY',[_n137,_alive2]),'src_span'(237,32,237,34,9021,22)),'prefix'('src_span'(238,16,238,20,9058,4),[],'tock','agent_call'('src_span'(238,24,238,31,9066,7),'AGREEBY',['-'(_n137,'int'(1)),_alive2]),'src_span'(238,21,238,23,9062,26)),'src_span_operator'('no_loc_info_available','src_span'(238,13,238,15,9055,2))),'prefix'('src_span'(239,9,239,13,9093,4),['in'(_k141)],'fail','agent_call'('src_span'(239,19,239,27,9103,8),'AGREEBY\x27\',['agent_call'('src_span'(239,28,239,32,9112,4),'diff',[_alive2,'setExp'('rangeEnum'([_k141]))])]),'src_span'(239,16,239,18,9099,31)),'src_span_operator'('no_loc_info_available','src_span'(239,6,239,8,9090,2))),'prefix'('src_span'(240,9,240,15,9137,6),['in'(_k142)],'revive','agent_call'('src_span'(240,21,240,28,9149,7),'AGREEBY',['val_of'('TS','src_span'(240,29,240,31,9157,2)),'agent_call'('src_span'(240,32,240,37,9160,5),'union',[_alive2,'setExp'('rangeEnum'([_k142]))])]),'src_span'(240,18,240,20,9145,34)),'src_span_operator'('no_loc_info_available','src_span'(240,6,240,8,9134,2))),'prefix'('src_span'(241,16,241,20,9193,4),['in'(_m3),'in'(_k144)],'test','agent_call'('src_span'(241,28,241,35,9205,7),'AGREEBY',[_n137,_alive2]),'src_span'(241,25,241,27,9201,22)),'src_span_operator'('no_loc_info_available','src_span'(241,13,241,15,9190,2))),'no_loc_info_available').
57		'agent'('AGREEBY\x27\'(_alive3),'[]'('[]'('[]'('[]'('|~|'('stop'('src_span'(246,21,246,25,9330,4)),'prefix'('src_span'(246,30,246,36,9339,6),['in'(_m4),'in'(_k147)],'leader','agent_call'('src_span'(246,44,246,52,9353,8),'AGREEBY\x27\',[_alive3]),'src_span'(246,41,246,43,9349,21)),'src_span_operator'('no_loc_info_available','src_span'(246,26,246,29,9335,3))),'prefix'('src_span'(247,16,247,20,9385,4),[],'tock','agent_call'('src_span'(247,24,247,32,9393,8),'AGREEBY\x27\',[_alive3]),'src_span'(247,21,247,23,9389,23)),'src_span_operator'('no_loc_info_available','src_span'(247,13,247,15,9382,2))),'prefix'('src_span'(248,16,248,20,9424,4),['in'(_k148)],'fail','agent_call'('src_span'(248,26,248,34,9434,8),'AGREEBY\x27\',['agent_call'('src_span'(248,35,248,39,9443,4),'diff',[_alive3,'setExp'('rangeEnum'([_k148]))])]),'src_span'(248,23,248,25,9430,31)),'src_span_operator'('no_loc_info_available','src_span'(248,13,248,15,9421,2))),'prefix'('src_span'(249,16,249,22,9475,6),['in'(_k149)],'revive','agent_call'('src_span'(249,28,249,35,9487,7),'AGREEBY',['val_of'('TS','src_span'(249,36,249,38,9495,2)),'agent_call'('src_span'(249,39,249,44,9498,5),'union',[_alive3,'setExp'('rangeEnum'([_k149]))])]),'src_span'(249,25,249,27,9483,34)),'src_span_operator'('no_loc_info_available','src_span'(249,13,249,15,9472,2))),'prefix'('src_span'(250,16,250,20,9531,4),['in'(_n150),'in'(_k151)],'test','agent_call'('src_span'(250,28,250,35,9543,7),'AGREEBY',['val_of'('TS','src_span'(250,36,250,38,9551,2)),_alive3]),'src_span'(250,25,250,27,9539,23)),'src_span_operator'('no_loc_info_available','src_span'(250,13,250,15,9528,2))),'no_loc_info_available').
58		'bindval'('AlphaAgree','closure'(['tock','fail','revive','leader','test']),'src_span'(253,1,253,50,9563,49)).
59		'assertRef'('False','agent_call'('src_span'(255,8,255,15,9621,7),'AGREEBY',['int'(0),'val_of'('Proc1','src_span'(255,18,255,23,9631,5))]),'Trace','\x5c\'('val_of'('Network','src_span'(255,29,255,36,9642,7)),'agent_call'('src_span'(255,37,255,41,9650,4),'diff',['Events','val_of'('AlphaAgree','src_span'(255,49,255,59,9662,10))]),'src_span_operator'('no_loc_info_available','src_span'(255,36,255,37,9649,1))),'src_span'(255,1,255,60,9614,59)).
60		'agent'('INLEADER'('int'(0),_alive4),'[]'('[]'('[]'('[]'('&'('!='(_alive4,'setExp'('rangeEnum'([]))),'let'(['bindval'('m5','agent_call'('src_span'(265,20,265,23,9944,3),'max',[_alive4]),'src_span'(265,18,265,30,9942,12))],'[]'('prefix'('src_span'(265,38,265,48,9962,10),[],'dotTuple'(['leader','val_of'('m5','src_span'(265,45,265,46,9969,1)),'val_of'('m5','src_span'(265,47,265,48,9971,1))]),'agent_call'('src_span'(265,52,265,60,9976,8),'INLEADER',['int'(0),_alive4]),'src_span'(265,49,265,51,9972,31)),'|~|'('stop'('src_span'(266,17,266,21,10010,4)),'prefix'('src_span'(266,26,266,32,10019,6),['inGuard'(_j9,'agent_call'('src_span'(266,35,266,39,10028,4),'diff',['val_of'('Proc1','src_span'(266,40,266,45,10033,5)),'setExp'('rangeEnum'(['val_of'('m5','src_span'(266,47,266,48,10040,1))]))])),'in'(_k155)],'leader','agent_call'('src_span'(266,56,266,64,10049,8),'INLEADER',['int'(0),_alive4]),'src_span'(266,53,266,55,10045,23)),'src_span_operator'('no_loc_info_available','src_span'(266,22,266,25,10015,3))),'src_span_operator'('no_loc_info_available','src_span'(266,13,266,15,10006,2))))),'prefix'('src_span'(267,16,267,20,10084,4),[],'tock','agent_call'('src_span'(267,24,267,32,10092,8),'INLEADER',['int'(0),_alive4]),'src_span'(267,21,267,23,10088,25)),'src_span_operator'('no_loc_info_available','src_span'(267,13,267,15,10081,2))),'prefix'('src_span'(268,9,268,13,10118,4),['in'(_k156)],'fail','agent_call'('src_span'(268,19,268,28,10128,9),'INLEADER\x27\',['agent_call'('src_span'(268,29,268,33,10138,4),'diff',[_alive4,'setExp'('rangeEnum'([_k156]))])]),'src_span'(268,16,268,18,10124,32)),'src_span_operator'('no_loc_info_available','src_span'(268,6,268,8,10115,2))),'prefix'('src_span'(269,9,269,15,10163,6),['in'(_k157)],'revive','agent_call'('src_span'(269,21,269,29,10175,8),'INLEADER',['val_of'('TS','src_span'(269,30,269,32,10184,2)),'agent_call'('src_span'(269,33,269,38,10187,5),'union',[_alive4,'setExp'('rangeEnum'([_k157]))])]),'src_span'(269,18,269,20,10171,35)),'src_span_operator'('no_loc_info_available','src_span'(269,6,269,8,10160,2))),'prefix'('src_span'(270,16,270,20,10220,4),['in'(_m6),'in'(_k159)],'test','agent_call'('src_span'(270,28,270,36,10232,8),'INLEADER',['int'(0),_alive4]),'src_span'(270,25,270,27,10228,23)),'src_span_operator'('no_loc_info_available','src_span'(270,13,270,15,10217,2))),'no_loc_info_available').
61		'agent'('INLEADER'(_n160,_alive5),'[]'('[]'('[]'('[]'('|~|'('stop'('src_span'(272,22,272,26,10272,4)),'prefix'('src_span'(272,31,272,37,10281,6),['in'(_m7),'in'(_k163)],'leader','agent_call'('src_span'(272,45,272,53,10295,8),'INLEADER',[_n160,_alive5]),'src_span'(272,42,272,44,10291,23)),'src_span_operator'('no_loc_info_available','src_span'(272,27,272,30,10277,3))),'prefix'('src_span'(273,16,273,20,10329,4),[],'tock','agent_call'('src_span'(273,24,273,32,10337,8),'INLEADER',['-'(_n160,'int'(1)),_alive5]),'src_span'(273,21,273,23,10333,27)),'src_span_operator'('no_loc_info_available','src_span'(273,13,273,15,10326,2))),'prefix'('src_span'(274,9,274,13,10365,4),['in'(_k164)],'fail','agent_call'('src_span'(274,19,274,28,10375,9),'INLEADER\x27\',['agent_call'('src_span'(274,29,274,33,10385,4),'diff',[_alive5,'setExp'('rangeEnum'([_k164]))])]),'src_span'(274,16,274,18,10371,32)),'src_span_operator'('no_loc_info_available','src_span'(274,6,274,8,10362,2))),'prefix'('src_span'(275,9,275,15,10410,6),['in'(_k165)],'revive','agent_call'('src_span'(275,21,275,29,10422,8),'INLEADER',['val_of'('TS','src_span'(275,30,275,32,10431,2)),'agent_call'('src_span'(275,33,275,38,10434,5),'union',[_alive5,'setExp'('rangeEnum'([_k165]))])]),'src_span'(275,18,275,20,10418,35)),'src_span_operator'('no_loc_info_available','src_span'(275,6,275,8,10407,2))),'prefix'('src_span'(276,16,276,20,10467,4),['in'(_m8),'in'(_k167)],'test','agent_call'('src_span'(276,28,276,36,10479,8),'INLEADER',[_n160,_alive5]),'src_span'(276,25,276,27,10475,23)),'src_span_operator'('no_loc_info_available','src_span'(276,13,276,15,10464,2))),'no_loc_info_available').
62		'agent'('INLEADER\x27\'(_alive6),'[]'('[]'('[]'('[]'('|~|'('stop'('src_span'(278,21,278,25,10518,4)),'prefix'('src_span'(278,30,278,36,10527,6),['in'(_m9),'in'(_k170)],'leader','agent_call'('src_span'(278,44,278,53,10541,9),'INLEADER\x27\',[_alive6]),'src_span'(278,41,278,43,10537,22)),'src_span_operator'('no_loc_info_available','src_span'(278,26,278,29,10523,3))),'prefix'('src_span'(279,16,279,20,10574,4),[],'tock','agent_call'('src_span'(279,24,279,33,10582,9),'INLEADER\x27\',[_alive6]),'src_span'(279,21,279,23,10578,24)),'src_span_operator'('no_loc_info_available','src_span'(279,13,279,15,10571,2))),'prefix'('src_span'(280,9,280,13,10607,4),['in'(_k171)],'fail','agent_call'('src_span'(280,19,280,28,10617,9),'INLEADER\x27\',['agent_call'('src_span'(280,29,280,33,10627,4),'diff',[_alive6,'setExp'('rangeEnum'([_k171]))])]),'src_span'(280,16,280,18,10613,32)),'src_span_operator'('no_loc_info_available','src_span'(280,6,280,8,10604,2))),'prefix'('src_span'(281,9,281,15,10652,6),['in'(_k172)],'revive','agent_call'('src_span'(281,21,281,29,10664,8),'INLEADER',['val_of'('TS','src_span'(281,30,281,32,10673,2)),'agent_call'('src_span'(281,33,281,38,10676,5),'union',[_alive6,'setExp'('rangeEnum'([_k172]))])]),'src_span'(281,18,281,20,10660,35)),'src_span_operator'('no_loc_info_available','src_span'(281,6,281,8,10649,2))),'prefix'('src_span'(282,16,282,20,10709,4),['in'(_m173),'in'(_k174)],'test','agent_call'('src_span'(282,28,282,36,10721,8),'INLEADER',['val_of'('TS','src_span'(282,37,282,39,10730,2)),_alive6]),'src_span'(282,25,282,27,10717,24)),'src_span_operator'('no_loc_info_available','src_span'(282,13,282,15,10706,2))),'no_loc_info_available').
63		'assertRef'('False','agent_call'('src_span'(284,8,284,16,10748,8),'INLEADER',['int'(0),'val_of'('Proc1','src_span'(284,19,284,24,10759,5))]),'Trace','\x5c\'('val_of'('Network','src_span'(284,30,284,37,10770,7)),'agent_call'('src_span'(284,38,284,42,10778,4),'diff',['Events','val_of'('AlphaAgree','src_span'(284,50,284,60,10790,10))]),'src_span_operator'('no_loc_info_available','src_span'(284,37,284,38,10777,1))),'src_span'(284,1,284,61,10741,60)).
64		'bindval'('FailINLEADER','sharing'('closure'(['fail','revive','test']),'agent_call'('src_span'(297,16,297,24,11464,8),'INLEADER',['int'(0),'val_of'('Proc1','src_span'(297,27,297,32,11475,5))]),'agent_call'('src_span'(298,16,298,22,11525,6),'normal',['builtin_call'('CHAOS'('src_span'(298,23,298,52,11532,29),'closure'(['fail','revive','test'])))]),'src_span'(297,34,297,60,11482,26)),'src_span'(297,1,298,53,11449,113)).
65		'agent'('SOMELEADER'('int'(0),_alive7),'[]'('[]'('[]'('[]'('repChoice'(['comprehensionGenerator'(_i,_alive7)],'repInternalChoice'(['comprehensionGenerator'(_j177,'val_of'('Proc1','src_span'(307,33,307,38,11877,5)))],'prefix'('src_span'(307,41,307,51,11885,10),[],'dotTuple'(['leader',_i,_j177]),'agent_call'('src_span'(307,55,307,65,11899,10),'SOMELEADER',['int'(0),_alive7]),'src_span'(307,52,307,54,11895,33)),'src_span'(307,31,307,40,11875,9)),'src_span'(307,16,307,25,11860,9)),'prefix'('src_span'(308,16,308,20,11936,4),[],'tock','agent_call'('src_span'(308,24,308,34,11944,10),'SOMELEADER',['int'(0),_alive7]),'src_span'(308,21,308,23,11940,27)),'src_span_operator'('no_loc_info_available','src_span'(308,13,308,15,11933,2))),'prefix'('src_span'(309,9,309,13,11972,4),['in'(_k178)],'fail','agent_call'('src_span'(309,19,309,30,11982,11),'SOMELEADER\x27\',['agent_call'('src_span'(309,31,309,35,11994,4),'diff',[_alive7,'setExp'('rangeEnum'([_k178]))])]),'src_span'(309,16,309,18,11978,34)),'src_span_operator'('no_loc_info_available','src_span'(309,6,309,8,11969,2))),'prefix'('src_span'(310,9,310,15,12019,6),['in'(_k179)],'revive','agent_call'('src_span'(310,21,310,31,12031,10),'SOMELEADER',['val_of'('TS','src_span'(310,32,310,34,12042,2)),'agent_call'('src_span'(310,35,310,40,12045,5),'union',[_alive7,'setExp'('rangeEnum'([_k179]))])]),'src_span'(310,18,310,20,12027,37)),'src_span_operator'('no_loc_info_available','src_span'(310,6,310,8,12016,2))),'prefix'('src_span'(311,16,311,20,12078,4),['in'(_m180),'in'(_k181)],'test','agent_call'('src_span'(311,28,311,38,12090,10),'SOMELEADER',['int'(0),_alive7]),'src_span'(311,25,311,27,12086,25)),'src_span_operator'('no_loc_info_available','src_span'(311,13,311,15,12075,2))),'no_loc_info_available').
66		'agent'('SOMELEADER'(_n182,_alive8),'[]'('[]'('[]'('[]'('|~|'('stop'('src_span'(313,24,313,28,12134,4)),'prefix'('src_span'(313,33,313,39,12143,6),['in'(_m184),'in'(_k185)],'leader','agent_call'('src_span'(313,47,313,57,12157,10),'SOMELEADER',[_n182,_alive8]),'src_span'(313,44,313,46,12153,25)),'src_span_operator'('no_loc_info_available','src_span'(313,29,313,32,12139,3))),'prefix'('src_span'(314,16,314,20,12193,4),[],'tock','agent_call'('src_span'(314,24,314,34,12201,10),'SOMELEADER',['-'(_n182,'int'(1)),_alive8]),'src_span'(314,21,314,23,12197,29)),'src_span_operator'('no_loc_info_available','src_span'(314,13,314,15,12190,2))),'prefix'('src_span'(315,9,315,13,12231,4),['in'(_k186)],'fail','agent_call'('src_span'(315,19,315,30,12241,11),'SOMELEADER\x27\',['agent_call'('src_span'(315,31,315,35,12253,4),'diff',[_alive8,'setExp'('rangeEnum'([_k186]))])]),'src_span'(315,16,315,18,12237,34)),'src_span_operator'('no_loc_info_available','src_span'(315,6,315,8,12228,2))),'prefix'('src_span'(316,9,316,15,12278,6),['in'(_k187)],'revive','agent_call'('src_span'(316,21,316,31,12290,10),'SOMELEADER',['val_of'('TS','src_span'(316,32,316,34,12301,2)),'agent_call'('src_span'(316,35,316,40,12304,5),'union',[_alive8,'setExp'('rangeEnum'([_k187]))])]),'src_span'(316,18,316,20,12286,37)),'src_span_operator'('no_loc_info_available','src_span'(316,6,316,8,12275,2))),'prefix'('src_span'(317,16,317,20,12337,4),['in'(_m188),'in'(_k189)],'test','agent_call'('src_span'(317,28,317,38,12349,10),'SOMELEADER',[_n182,_alive8]),'src_span'(317,25,317,27,12345,25)),'src_span_operator'('no_loc_info_available','src_span'(317,13,317,15,12334,2))),'no_loc_info_available').
67		'agent'('SOMELEADER\x27\'(_alive9),'[]'('[]'('[]'('[]'('|~|'('stop'('src_span'(319,23,319,27,12392,4)),'prefix'('src_span'(319,32,319,38,12401,6),['in'(_m191),'in'(_k192)],'leader','agent_call'('src_span'(319,46,319,57,12415,11),'SOMELEADER\x27\',[_alive9]),'src_span'(319,43,319,45,12411,24)),'src_span_operator'('no_loc_info_available','src_span'(319,28,319,31,12397,3))),'prefix'('src_span'(320,16,320,20,12450,4),[],'tock','agent_call'('src_span'(320,24,320,35,12458,11),'SOMELEADER\x27\',[_alive9]),'src_span'(320,21,320,23,12454,26)),'src_span_operator'('no_loc_info_available','src_span'(320,13,320,15,12447,2))),'prefix'('src_span'(321,9,321,13,12485,4),['in'(_k193)],'fail','agent_call'('src_span'(321,19,321,30,12495,11),'SOMELEADER\x27\',['agent_call'('src_span'(321,31,321,35,12507,4),'diff',[_alive9,'setExp'('rangeEnum'([_k193]))])]),'src_span'(321,16,321,18,12491,34)),'src_span_operator'('no_loc_info_available','src_span'(321,6,321,8,12482,2))),'prefix'('src_span'(322,9,322,15,12532,6),['in'(_k194)],'revive','agent_call'('src_span'(322,21,322,31,12544,10),'SOMELEADER',['val_of'('TS','src_span'(322,32,322,34,12555,2)),'agent_call'('src_span'(322,35,322,40,12558,5),'union',[_alive9,'setExp'('rangeEnum'([_k194]))])]),'src_span'(322,18,322,20,12540,37)),'src_span_operator'('no_loc_info_available','src_span'(322,6,322,8,12529,2))),'prefix'('src_span'(323,16,323,20,12591,4),['in'(_m195),'in'(_k196)],'test','agent_call'('src_span'(323,28,323,38,12603,10),'SOMELEADER',['val_of'('TS','src_span'(323,39,323,41,12614,2)),_alive9]),'src_span'(323,25,323,27,12599,26)),'src_span_operator'('no_loc_info_available','src_span'(323,13,323,15,12588,2))),'no_loc_info_available').
68		'bindval'('FailSOMELEADER','sharing'('closure'(['fail','revive','test']),'agent_call'('src_span'(328,18,328,28,12779,10),'SOMELEADER',['int'(0),'val_of'('Proc1','src_span'(328,31,328,36,12792,5))]),'agent_call'('src_span'(329,16,329,22,12842,6),'normal',['builtin_call'('CHAOS'('src_span'(329,23,329,52,12849,29),'closure'(['fail','revive','test'])))]),'src_span'(328,38,328,64,12799,26)),'src_span'(328,1,329,53,12762,117)).
69		'comment'('lineComment'('-- The bully algorithm modelled in CSP'),'src_position'(1,2,1,38)).
70		'comment'('lineComment'('-- Bill Roscoe '),'src_position'(3,1,41,15)).
71		'comment'('lineComment'('-- See chapter 14 of Understanding Concurrent Systems for details of the'),'src_position'(5,1,58,72)).
72		'comment'('lineComment'('-- algorithm.'),'src_position'(6,1,131,13)).
73		'comment'('lineComment'('-- The number of nodes, the time-out intervals (T1 and T2) and the settle-by'),'src_position'(8,1,146,76)).
74		'comment'('lineComment'('-- parameter for the specifications'),'src_position'(9,1,223,35)).
75		'comment'('lineComment'('-- All communications in this algorithm go from high to low or low to high'),'src_position'(19,1,305,74)).
76		'comment'('lineComment'('-- so it is useful to have the following sets defined:'),'src_position'(20,1,380,54)).
77		'comment'('lineComment'('-- The alphabet as described in the assignment'),'src_position'(25,1,503,46)).
78		'comment'('lineComment'('-- Now we have a number of states a node can be in. The first is when it'),'src_position'(41,1,741,73)).
79		'comment'('lineComment'('-- is about to begin an election'),'src_position'(42,1,815,32)).
80		'comment'('lineComment'('-- which results in it sending successive election messages to the appropriate'),'src_position'(46,1,890,78)).
81		'comment'('lineComment'('-- nodes. Note how it can handle the receipt of any message it might'),'src_position'(47,1,969,69)).
82		'comment'('lineComment'('-- receive, with varying results...'),'src_position'(48,1,1039,35)).
83		'comment'('lineComment'('-- Here is is waiting for answers from its election messages, with the'),'src_position'(59,1,1567,70)).
84		'comment'('lineComment'('-- time-out making it the coordinator if it has not had one within T1.'),'src_position'(60,1,1638,70)).
85		'comment'('lineComment'('-- After it has had its answer message, it sits and waits to be sent a'),'src_position'(72,1,2201,70)).
86		'comment'('lineComment'('-- coordinator message (or any of a number of others), before starting '),'src_position'(73,1,2272,71)).
87		'comment'('lineComment'('-- another election if nothing has happened.'),'src_position'(74,1,2344,44)).
88		'comment'('lineComment'('-- This is the state it is in when it has decided, for want of life above it,'),'src_position'(88,1,2960,77)).
89		'comment'('lineComment'('-- that it is the current coordinator'),'src_position'(89,1,3038,37)).
90		'comment'('lineComment'('-- It distributes a coordinator message to all below it. Note that since it'),'src_position'(93,1,3119,76)).
91		'comment'('lineComment'('-- is the coordinator, it sends a positive response to the test message,'),'src_position'(94,1,3196,72)).
92		'comment'('lineComment'('-- unlike earlier states'),'src_position'(95,1,3269,24)).
93		'comment'('lineComment'('-- There are two running states, one as coordinator...'),'src_position'(104,1,3654,54)).
94		'comment'('lineComment'('--tock -> RunAsCoord(n)'),'src_position'(106,19,3728,23)).
95		'comment'('lineComment'('--[] '),'src_position'(107,19,3770,5)).
96		'comment'('lineComment'('--[] leader.n.n -> RunAsCoord(n)'),'src_position'(112,5,4027,32)).
97		'comment'('lineComment'('-- and one not, that thinks k is coordinator... '),'src_position'(114,1,4061,48)).
98		'comment'('lineComment'('--[] tock -> Running(n,k)'),'src_position'(117,19,4172,25)).
99		'comment'('lineComment'('--[] leader.n.k -> Running(n,k)'),'src_position'(120,5,4323,31)).
100		'comment'('lineComment'('-- thus it can test its supposed corrdinator, insitaged by the test.n.k event'),'src_position'(125,1,4530,77)).
101		'comment'('lineComment'('-- above, the test being successful if ok is received, failing by time-out'),'src_position'(126,1,4608,74)).
102		'comment'('lineComment'('-- of tock occurs first.'),'src_position'(127,1,4683,24)).
103		'comment'('lineComment'('--[] leader.n.k -> Testing(n,k)'),'src_position'(136,5,5099,31)).
104		'comment'('lineComment'('-- After performing one test successfully, it goes into the following state'),'src_position'(138,1,5132,75)).
105		'comment'('lineComment'('-- in which it has to wait a time unit before performing another one (thereby'),'src_position'(139,1,5208,77)).
106		'comment'('lineComment'('-- avoiding a potential divergence)'),'src_position'(140,1,5286,35)).
107		'comment'('lineComment'('--[] leader.n.k -> Running\x27\(n,k)'),'src_position'(147,5,5606,32)).
108		'comment'('lineComment'('-- When a process has failed...'),'src_position'(151,1,5751,31)).
109		'comment'('lineComment'('-- it can\x27\t be revived until one time unit has passed'),'src_position'(161,1,6112,53)).
110		'comment'('lineComment'('--tock -> Failed\x27\(n)'),'src_position'(163,14,6180,20)).
111		'comment'('lineComment'('-- [] '),'src_position'(164,13,6213,6)).
112		'comment'('lineComment'('-- We can put the system together (exploiting a little bit of compression'),'src_position'(175,1,6624,73)).
113		'comment'('lineComment'('-- on the individual nodes) as follows:'),'src_position'(176,1,6698,39)).
114		'comment'('lineComment'('-- The first thing to try with any timed example is a timing consistency'),'src_position'(193,1,7218,72)).
115		'comment'('lineComment'('-- check. The following events are all deemed "delayable" because we'),'src_position'(194,1,7291,69)).
116		'comment'('lineComment'('-- do not want to have to rely on them happening urgently for time to'),'src_position'(195,1,7361,69)).
117		'comment'('lineComment'('-- pass (the inclusion of test here is not essential, and might be wrong'),'src_position'(196,1,7431,72)).
118		'comment'('lineComment'('-- in other modelling approaches).'),'src_position'(197,1,7504,34)).
119		'comment'('lineComment'('-- The following give us two nearly equivalent ways of testing it, the'),'src_position'(202,1,7630,70)).
120		'comment'('lineComment'('-- second being stronger because it proves that hiding the urgent events'),'src_position'(203,1,7701,72)).
121		'comment'('lineComment'('-- can\x27\t introduce divergence, which would break various assumptions of'),'src_position'(204,1,7774,71)).
122		'comment'('lineComment'('-- the abstraction method.'),'src_position'(205,1,7846,26)).
123		'comment'('lineComment'('--assert TOCKS [F= (Network [|Delayable|] '),'src_position'(207,1,7874,42)).
124		'comment'('lineComment'('-- normal(CHAOS(Delayable)))\x5c\diff(Events,{tock})'),'src_position'(208,1,7917,65)).
125		'comment'('lineComment'('--assert TOCKS ||| CHAOS(Delayable) [FD= Network \x5c\ Urgent'),'src_position'(210,1,7984,58)).
126		'comment'('lineComment'('-- We will want normally to have our processes agree that the maximum'),'src_position'(214,1,8067,69)).
127		'comment'('lineComment'('-- live one is the leader, so the following function comes in handy:'),'src_position'(215,1,8137,68)).
128		'comment'('lineComment'('-- The following specification holds the current set of live processes'),'src_position'(220,1,8297,70)).
129		'comment'('lineComment'('-- as a parameter, and says that when appropriate things have happened since'),'src_position'(221,1,8368,76)).
130		'comment'('lineComment'('-- a node last failed or revived, anyone who expresses an opinion about'),'src_position'(222,1,8445,71)).
131		'comment'('lineComment'('-- who the leader is says the highest live one.'),'src_position'(223,1,8517,47)).
132		'comment'('lineComment'('-- Initially this condition holds, but it is disabled by a failure or'),'src_position'(225,1,8566,69)).
133		'comment'('lineComment'('-- revival.'),'src_position'(226,1,8636,11)).
134		'comment'('lineComment'('-- The following states will allow any leader events until n tocks have'),'src_position'(234,1,8906,71)).
135		'comment'('lineComment'('-- passed..'),'src_position'(235,1,8978,11)).
136		'comment'('lineComment'('-- while this one allows any until a test event has occurred followed by'),'src_position'(243,1,9223,72)).
137		'comment'('lineComment'('-- TS tocks.'),'src_position'(244,1,9296,12)).
138		'comment'('lineComment'('-- So the above trace spec (which fails) says that the network has the'),'src_position'(257,1,9675,70)).
139		'comment'('lineComment'('-- given property.'),'src_position'(258,1,9746,18)).
140		'comment'('lineComment'('-- The above having failed, we can see if the max-process always agrees'),'src_position'(260,1,9766,71)).
141		'comment'('lineComment'('-- it is the leader in the same circumstances....'),'src_position'(261,1,9838,49)).
142		'comment'('lineComment'('-- This fails as well (in turns out that making the distribution of the'),'src_position'(286,1,10803,71)).
143		'comment'('lineComment'('-- co-ordinator messages non-atomic with the possibility of a process'),'src_position'(287,1,10875,69)).
144		'comment'('lineComment'('-- failing mid-way through a distribution creates havoc with the'),'src_position'(288,1,10945,64)).
145		'comment'('lineComment'('-- algorithm: it is certainly not clear from the book that it depends on'),'src_position'(289,1,11010,72)).
146		'comment'('lineComment'('-- this atomicity). We could have strengthened this into a failures'),'src_position'(290,1,11083,68)).
147		'comment'('lineComment'('-- specification, saying that the max process can always say it is the'),'src_position'(291,1,11152,70)).
148		'comment'('lineComment'('-- leader in the given circumstances, as follows (which explains why'),'src_position'(292,1,11223,68)).
149		'comment'('lineComment'('-- all the leader events above that we do not want to insist on are'),'src_position'(293,1,11292,67)).
150		'comment'('lineComment'('-- put in |~| choice with STOP; the other events being refusable by'),'src_position'(294,1,11360,67)).
151		'comment'('lineComment'('-- the CHAOS below)'),'src_position'(295,1,11428,19)).
152		'comment'('lineComment'('--assert FailINLEADER [F= Network\x5c\diff(Events,AlphaAgree)'),'src_position'(300,1,11564,58)).
153		'comment'('lineComment'('-- On the same principle, the following specification says that'),'src_position'(302,1,11624,63)).
154		'comment'('lineComment'('-- under the same stability conditions as before, every living process'),'src_position'(303,1,11688,70)).
155		'comment'('lineComment'('-- has an option about the leader, even if not the right one!'),'src_position'(304,1,11759,61)).
156		'comment'('lineComment'('-- As a trace specification the above says nothing of any interest. The'),'src_position'(325,1,12625,72)).
157		'comment'('lineComment'('-- same device as above turns it into the right failures spec:'),'src_position'(326,1,12698,62)).
158		'comment'('lineComment'('--assert FailSOMELEADER [F= Network\x5c\diff(Events,AlphaAgree)'),'src_position'(331,1,12881,60)).
159		'comment'('lineComment'('-- As it turns out (and somewhat to my surprise, even having seen the'),'src_position'(333,1,12943,69)).
160		'comment'('lineComment'('-- problems that arise earlier on) even this specification fails.'),'src_position'(334,1,13013,65)).
161		'comment'('lineComment'('-- It would be a great achievement (I think) to spot what can go wrong'),'src_position'(335,1,13079,70)).
162		'comment'('lineComment'('-- without running the check!'),'src_position'(336,1,13150,29)).
163		'comment'('lineComment'('-- You can fix the algorithm by making nodes test their coordinator'),'src_position'(338,1,13181,67)).
164		'comment'('lineComment'('-- a small interval (one tock in our case, and in any case enough for'),'src_position'(339,1,13249,69)).
165		'comment'('lineComment'('-- the coordinator to have finished distribution) after being "bullied"'),'src_position'(340,1,13319,71)).
166		'comment'('lineComment'('-- namely told the identity of the coordinator. See bully2.csp'),'src_position'(341,1,13391,63)).
167		'comment'('lineComment'('-- MAIN = test.0.3 -> tock -> fail?x -> STOP'),'src_position'(343,1,13456,44)).
168		'comment'('lineComment'('-- MAIN = Node(1)'),'src_position'(344,1,13501,17)).
169		'symbol'('N','N','src_span'(11,1,11,2,260,1),'Ident (Groundrep.)').
170		'symbol'('T1','T1','src_span'(13,1,13,3,265,2),'Ident (Groundrep.)').
171		'symbol'('T2','T2','src_span'(14,1,14,3,272,2),'Ident (Groundrep.)').
172		'symbol'('TS','TS','src_span'(15,1,15,3,279,2),'Ident (Groundrep.)').
173		'symbol'('Proc1','Proc1','src_span'(17,1,17,6,287,5),'Ident (Groundrep.)').
174		'symbol'('above','above','src_span'(22,1,22,6,436,5),'Funktion or Process').
175		'symbol'('n','n','src_span'(22,7,22,8,442,1),'Ident (Prolog Variable)').
176		'symbol'('k','k','src_span'(22,17,22,18,452,1),'Ident (Prolog Variable)').
177		'symbol'('below','below','src_span'(23,1,23,6,469,5),'Funktion or Process').
178		'symbol'('n2','n','src_span'(23,7,23,8,475,1),'Ident (Prolog Variable)').
179		'symbol'('k2','k','src_span'(23,17,23,18,485,1),'Ident (Prolog Variable)').
180		'symbol'('election','election','src_span'(27,9,27,17,559,8),'Channel').
181		'symbol'('answer','answer','src_span'(29,9,29,15,589,6),'Channel').
182		'symbol'('coordinator','coordinator','src_span'(31,9,31,20,617,11),'Channel').
183		'symbol'('fail','fail','src_span'(33,9,33,13,650,4),'Channel').
184		'symbol'('revive','revive','src_span'(33,15,33,21,656,6),'Channel').
185		'symbol'('test','test','src_span'(35,9,35,13,678,4),'Channel').
186		'symbol'('ok','ok','src_span'(35,14,35,16,683,2),'Channel').
187		'symbol'('leader','leader','src_span'(37,9,37,15,707,6),'Channel').
188		'symbol'('tock','tock','src_span'(39,9,39,13,735,4),'Channel').
189		'symbol'('BeginElection','BeginElection','src_span'(44,1,44,14,849,13),'Funktion or Process').
190		'symbol'('n3','n','src_span'(44,15,44,16,863,1),'Ident (Prolog Variable)').
191		'symbol'('SendElections','SendElections','src_span'(50,1,50,14,1076,13),'Funktion or Process').
192		'symbol'('k3','k','src_span'(50,15,50,16,1090,1),'Ident (Prolog Variable)').
193		'symbol'('n4','n','src_span'(50,17,50,18,1092,1),'Ident (Prolog Variable)').
194		'symbol'('k\x27\','k\x27\','src_span'(52,33,52,35,1226,2),'Ident (Prolog Variable)').
195		'symbol'('k4','k','src_span'(53,31,53,32,1305,1),'Ident (Prolog Variable)').
196		'symbol'('k\x27\2','k\x27\','src_span'(54,27,54,29,1370,2),'Ident (Prolog Variable)').
197		'symbol'('k5','k','src_span'(55,36,55,37,1441,1),'Ident (Prolog Variable)').
198		'symbol'('k\x27\3','k\x27\','src_span'(57,29,57,31,1528,2),'Ident (Prolog Variable)').
199		'symbol'('AwaitAnswers','AwaitAnswers','src_span'(62,1,62,13,1710,12),'Funktion or Process').
200		'symbol'('t','t','src_span'(62,14,62,15,1723,1),'Ident (Prolog Variable)').
201		'symbol'('n5','n','src_span'(62,16,62,17,1725,1),'Ident (Prolog Variable)').
202		'symbol'('k6','k','src_span'(65,28,65,29,1872,1),'Ident (Prolog Variable)').
203		'symbol'('k7','k','src_span'(66,24,66,25,1934,1),'Ident (Prolog Variable)').
204		'symbol'('k8','k','src_span'(67,30,67,31,1997,1),'Ident (Prolog Variable)').
205		'symbol'('k9','k','src_span'(68,33,68,34,2077,1),'Ident (Prolog Variable)').
206		'symbol'('k73','k','src_span'(70,29,70,30,2164,1),'Ident (Prolog Variable)').
207		'symbol'('AwaitCoordinator','AwaitCoordinator','src_span'(77,1,77,17,2391,16),'Funktion or Process').
208		'symbol'('t2','t','src_span'(77,18,77,19,2408,1),'Ident (Prolog Variable)').
209		'symbol'('n6','n','src_span'(77,20,77,21,2410,1),'Ident (Prolog Variable)').
210		'symbol'('k76','k','src_span'(80,37,80,38,2573,1),'Ident (Prolog Variable)').
211		'symbol'('k77','k','src_span'(81,31,81,32,2633,1),'Ident (Prolog Variable)').
212		'symbol'('k78','k','src_span'(82,27,82,28,2697,1),'Ident (Prolog Variable)').
213		'symbol'('k79','k','src_span'(83,33,83,34,2767,1),'Ident (Prolog Variable)').
214		'symbol'('k80','k','src_span'(86,29,86,30,2919,1),'Ident (Prolog Variable)').
215		'symbol'('BecomeCoordinator','BecomeCoordinator','src_span'(91,1,91,18,3077,17),'Funktion or Process').
216		'symbol'('n7','n','src_span'(91,19,91,20,3095,1),'Ident (Prolog Variable)').
217		'symbol'('SendCoords','SendCoords','src_span'(97,1,97,11,3295,10),'Funktion or Process').
218		'symbol'('j','j','src_span'(97,12,97,13,3306,1),'Ident (Prolog Variable)').
219		'symbol'('n8','n','src_span'(97,14,97,15,3308,1),'Ident (Prolog Variable)').
220		'symbol'('k84','k','src_span'(99,31,99,32,3429,1),'Ident (Prolog Variable)').
221		'symbol'('k85','k','src_span'(100,34,100,35,3513,1),'Ident (Prolog Variable)').
222		'symbol'('k86','k','src_span'(102,27,102,28,3610,1),'Ident (Prolog Variable)').
223		'symbol'('RunAsCoord','RunAsCoord','src_span'(106,1,106,11,3710,10),'Funktion or Process').
224		'symbol'('n9','n','src_span'(106,12,106,13,3721,1),'Ident (Prolog Variable)').
225		'symbol'('k88','k','src_span'(108,27,108,28,3802,1),'Ident (Prolog Variable)').
226		'symbol'('k89','k','src_span'(109,34,109,35,3875,1),'Ident (Prolog Variable)').
227		'symbol'('k90','k','src_span'(110,31,110,32,3935,1),'Ident (Prolog Variable)').
228		'symbol'('Running','Running','src_span'(116,1,116,8,4111,7),'Funktion or Process').
229		'symbol'('n91','n','src_span'(116,9,116,10,4119,1),'Ident (Prolog Variable)').
230		'symbol'('k92','k','src_span'(116,11,116,12,4121,1),'Ident (Prolog Variable)').
231		'symbol'('k93','k','src_span'(118,34,118,35,4231,1),'Ident (Prolog Variable)').
232		'symbol'('j2','j','src_span'(119,29,119,30,4289,1),'Ident (Prolog Variable)').
233		'symbol'('k95','k','src_span'(121,31,121,32,4385,1),'Ident (Prolog Variable)').
234		'symbol'('j3','j','src_span'(122,27,122,28,4458,1),'Ident (Prolog Variable)').
235		'symbol'('Testing','Testing','src_span'(129,1,129,8,4709,7),'Funktion or Process').
236		'symbol'('n97','n','src_span'(129,9,129,10,4717,1),'Ident (Prolog Variable)').
237		'symbol'('k98','k','src_span'(129,11,129,12,4719,1),'Ident (Prolog Variable)').
238		'symbol'('j4','j','src_span'(131,29,131,30,4828,1),'Ident (Prolog Variable)').
239		'symbol'('k100','k','src_span'(132,34,132,35,4891,1),'Ident (Prolog Variable)').
240		'symbol'('k101','k','src_span'(133,31,133,32,4951,1),'Ident (Prolog Variable)').
241		'symbol'('j5','j','src_span'(135,27,135,28,5065,1),'Ident (Prolog Variable)').
242		'symbol'('Running\x27\','Running\x27\','src_span'(142,1,142,9,5323,8),'Funktion or Process').
243		'symbol'('n103','n','src_span'(142,10,142,11,5332,1),'Ident (Prolog Variable)').
244		'symbol'('k104','k','src_span'(142,12,142,13,5334,1),'Ident (Prolog Variable)').
245		'symbol'('k105','k','src_span'(143,34,143,35,5395,1),'Ident (Prolog Variable)').
246		'symbol'('j6','j','src_span'(144,29,144,30,5453,1),'Ident (Prolog Variable)').
247		'symbol'('k107','k','src_span'(145,31,145,32,5514,1),'Ident (Prolog Variable)').
248		'symbol'('j7','j','src_span'(148,27,148,28,5665,1),'Ident (Prolog Variable)').
249		'symbol'('j8','j','src_span'(149,25,149,26,5720,1),'Ident (Prolog Variable)').
250		'symbol'('Failed','Failed','src_span'(153,1,153,7,5801,6),'Funktion or Process').
251		'symbol'('n110','n','src_span'(153,8,153,9,5808,1),'Ident (Prolog Variable)').
252		'symbol'('k111','k','src_span'(154,28,154,29,5859,1),'Ident (Prolog Variable)').
253		'symbol'('k112','k','src_span'(155,25,155,26,5909,1),'Ident (Prolog Variable)').
254		'symbol'('k113','k','src_span'(156,21,156,22,5955,1),'Ident (Prolog Variable)').
255		'symbol'('k114','k','src_span'(157,19,157,20,6000,1),'Ident (Prolog Variable)').
256		'symbol'('k115','k','src_span'(158,23,158,24,6049,1),'Ident (Prolog Variable)').
257		'symbol'('Failed\x27\','Failed\x27\','src_span'(163,1,163,8,6167,7),'Funktion or Process').
258		'symbol'('n116','n','src_span'(163,9,163,10,6175,1),'Ident (Prolog Variable)').
259		'symbol'('k117','k','src_span'(165,28,165,29,6247,1),'Ident (Prolog Variable)').
260		'symbol'('k118','k','src_span'(166,25,166,26,6298,1),'Ident (Prolog Variable)').
261		'symbol'('k119','k','src_span'(167,21,167,22,6345,1),'Ident (Prolog Variable)').
262		'symbol'('k120','k','src_span'(168,19,168,20,6391,1),'Ident (Prolog Variable)').
263		'symbol'('k121','k','src_span'(169,23,169,24,6441,1),'Ident (Prolog Variable)').
264		'symbol'('normal','normal','src_span'(178,13,178,19,6751,6),'Transparent function').
265		'symbol'('Alpha','Alpha','src_span'(180,1,180,6,6759,5),'Funktion or Process').
266		'symbol'('n122','n','src_span'(180,7,180,8,6765,1),'Ident (Prolog Variable)').
267		'symbol'('union','union','src_span'(180,12,180,17,6770,5),'BuiltIn primitive').
268		'symbol'('k123','k','src_span'(183,35,183,36,6955,1),'Ident (Prolog Variable)').
269		'symbol'('Node','Node','src_span'(185,1,185,5,6969,4),'Funktion or Process').
270		'symbol'('n124','n','src_span'(185,6,185,7,6974,1),'Ident (Prolog Variable)').
271		'symbol'('Network','Network','src_span'(187,1,187,8,7037,7),'Ident (Groundrep.)').
272		'symbol'('n125','n','src_span'(187,14,187,15,7050,1),'Ident (Prolog Variable)').
273		'symbol'('Delayable','Delayable','src_span'(199,1,199,10,7540,9),'Ident (Groundrep.)').
274		'symbol'('Urgent','Urgent','src_span'(200,1,200,7,7583,6),'Ident (Groundrep.)').
275		'symbol'('diff','diff','src_span'(200,10,200,14,7592,4),'BuiltIn primitive').
276		'symbol'('union','union','src_span'(200,22,200,27,7604,5),'BuiltIn primitive').
277		'symbol'('TOCKS','TOCKS','src_span'(212,1,212,6,8044,5),'Ident (Groundrep.)').
278		'symbol'('max','max','src_span'(217,1,217,4,8207,3),'Funktion or Process').
279		'symbol'('S','S','src_span'(217,5,217,6,8211,1),'Ident (Prolog Variable)').
280		'symbol'('pick','pick','src_span'(217,14,217,18,8220,4),'Funktion or Process').
281		'symbol'('x','x','src_span'(217,20,217,21,8226,1),'Ident (Prolog Variable)').
282		'symbol'('x2','x','src_span'(218,20,218,21,8260,1),'Ident (Prolog Variable)').
283		'symbol'('y','y','src_span'(218,33,218,34,8273,1),'Ident (Prolog Variable)').
284		'symbol'('AGREEBY','AGREEBY','src_span'(228,1,228,8,8649,7),'Funktion or Process').
285		'symbol'('alive','alive','src_span'(228,11,228,16,8659,5),'Ident (Prolog Variable)').
286		'symbol'('m','m','src_span'(228,41,228,42,8689,1),'Ident (Prolog Variable)').
287		'symbol'('k133','k','src_span'(230,14,230,15,8781,1),'Ident (Prolog Variable)').
288		'symbol'('k134','k','src_span'(231,16,231,17,8827,1),'Ident (Prolog Variable)').
289		'symbol'('n135','n','src_span'(232,21,232,22,8881,1),'Ident (Prolog Variable)').
290		'symbol'('k136','k','src_span'(232,23,232,24,8883,1),'Ident (Prolog Variable)').
291		'symbol'('n137','n','src_span'(237,9,237,10,8999,1),'Ident (Prolog Variable)').
292		'symbol'('alive2','alive','src_span'(237,11,237,16,9001,5),'Ident (Prolog Variable)').
293		'symbol'('m2','m','src_span'(237,28,237,29,9018,1),'Ident (Prolog Variable)').
294		'symbol'('k140','k','src_span'(237,30,237,31,9020,1),'Ident (Prolog Variable)').
295		'symbol'('k141','k','src_span'(239,14,239,15,9098,1),'Ident (Prolog Variable)').
296		'symbol'('k142','k','src_span'(240,16,240,17,9144,1),'Ident (Prolog Variable)').
297		'symbol'('m3','m','src_span'(241,21,241,22,9198,1),'Ident (Prolog Variable)').
298		'symbol'('k144','k','src_span'(241,23,241,24,9200,1),'Ident (Prolog Variable)').
299		'symbol'('AGREEBY\x27\','AGREEBY\x27\','src_span'(246,1,246,9,9310,8),'Funktion or Process').
300		'symbol'('alive3','alive','src_span'(246,10,246,15,9319,5),'Ident (Prolog Variable)').
301		'symbol'('m4','m','src_span'(246,37,246,38,9346,1),'Ident (Prolog Variable)').
302		'symbol'('k147','k','src_span'(246,39,246,40,9348,1),'Ident (Prolog Variable)').
303		'symbol'('k148','k','src_span'(248,21,248,22,9429,1),'Ident (Prolog Variable)').
304		'symbol'('k149','k','src_span'(249,23,249,24,9482,1),'Ident (Prolog Variable)').
305		'symbol'('n150','n','src_span'(250,21,250,22,9536,1),'Ident (Prolog Variable)').
306		'symbol'('k151','k','src_span'(250,23,250,24,9538,1),'Ident (Prolog Variable)').
307		'symbol'('AlphaAgree','AlphaAgree','src_span'(253,1,253,11,9563,10),'Ident (Groundrep.)').
308		'symbol'('INLEADER','INLEADER','src_span'(264,1,264,9,9890,8),'Funktion or Process').
309		'symbol'('alive4','alive','src_span'(264,12,264,17,9901,5),'Ident (Prolog Variable)').
310		'symbol'('m5','m','src_span'(265,18,265,19,9942,1),'Ident (Groundrep.)').
311		'symbol'('j9','j','src_span'(266,33,266,34,10026,1),'Ident (Prolog Variable)').
312		'symbol'('k155','k','src_span'(266,51,266,52,10044,1),'Ident (Prolog Variable)').
313		'symbol'('k156','k','src_span'(268,14,268,15,10123,1),'Ident (Prolog Variable)').
314		'symbol'('k157','k','src_span'(269,16,269,17,10170,1),'Ident (Prolog Variable)').
315		'symbol'('m6','m','src_span'(270,21,270,22,10225,1),'Ident (Prolog Variable)').
316		'symbol'('k159','k','src_span'(270,23,270,24,10227,1),'Ident (Prolog Variable)').
317		'symbol'('n160','n','src_span'(272,10,272,11,10260,1),'Ident (Prolog Variable)').
318		'symbol'('alive5','alive','src_span'(272,12,272,17,10262,5),'Ident (Prolog Variable)').
319		'symbol'('m7','m','src_span'(272,38,272,39,10288,1),'Ident (Prolog Variable)').
320		'symbol'('k163','k','src_span'(272,40,272,41,10290,1),'Ident (Prolog Variable)').
321		'symbol'('k164','k','src_span'(274,14,274,15,10370,1),'Ident (Prolog Variable)').
322		'symbol'('k165','k','src_span'(275,16,275,17,10417,1),'Ident (Prolog Variable)').
323		'symbol'('m8','m','src_span'(276,21,276,22,10472,1),'Ident (Prolog Variable)').
324		'symbol'('k167','k','src_span'(276,23,276,24,10474,1),'Ident (Prolog Variable)').
325		'symbol'('INLEADER\x27\','INLEADER\x27\','src_span'(278,1,278,10,10498,9),'Funktion or Process').
326		'symbol'('alive6','alive','src_span'(278,11,278,16,10508,5),'Ident (Prolog Variable)').
327		'symbol'('m9','m','src_span'(278,37,278,38,10534,1),'Ident (Prolog Variable)').
328		'symbol'('k170','k','src_span'(278,39,278,40,10536,1),'Ident (Prolog Variable)').
329		'symbol'('k171','k','src_span'(280,14,280,15,10612,1),'Ident (Prolog Variable)').
330		'symbol'('k172','k','src_span'(281,16,281,17,10659,1),'Ident (Prolog Variable)').
331		'symbol'('m173','m','src_span'(282,21,282,22,10714,1),'Ident (Prolog Variable)').
332		'symbol'('k174','k','src_span'(282,23,282,24,10716,1),'Ident (Prolog Variable)').
333		'symbol'('FailINLEADER','FailINLEADER','src_span'(297,1,297,13,11449,12),'Ident (Groundrep.)').
334		'symbol'('SOMELEADER','SOMELEADER','src_span'(306,1,306,11,11822,10),'Funktion or Process').
335		'symbol'('alive7','alive','src_span'(306,14,306,19,11835,5),'Ident (Prolog Variable)').
336		'symbol'('i','i','src_span'(307,16,307,17,11860,1),'Ident (Prolog Variable)').
337		'symbol'('j177','j','src_span'(307,31,307,32,11875,1),'Ident (Prolog Variable)').
338		'symbol'('k178','k','src_span'(309,14,309,15,11977,1),'Ident (Prolog Variable)').
339		'symbol'('k179','k','src_span'(310,16,310,17,12026,1),'Ident (Prolog Variable)').
340		'symbol'('m180','m','src_span'(311,21,311,22,12083,1),'Ident (Prolog Variable)').
341		'symbol'('k181','k','src_span'(311,23,311,24,12085,1),'Ident (Prolog Variable)').
342		'symbol'('n182','n','src_span'(313,12,313,13,12122,1),'Ident (Prolog Variable)').
343		'symbol'('alive8','alive','src_span'(313,14,313,19,12124,5),'Ident (Prolog Variable)').
344		'symbol'('m184','m','src_span'(313,40,313,41,12150,1),'Ident (Prolog Variable)').
345		'symbol'('k185','k','src_span'(313,42,313,43,12152,1),'Ident (Prolog Variable)').
346		'symbol'('k186','k','src_span'(315,14,315,15,12236,1),'Ident (Prolog Variable)').
347		'symbol'('k187','k','src_span'(316,16,316,17,12285,1),'Ident (Prolog Variable)').
348		'symbol'('m188','m','src_span'(317,21,317,22,12342,1),'Ident (Prolog Variable)').
349		'symbol'('k189','k','src_span'(317,23,317,24,12344,1),'Ident (Prolog Variable)').
350		'symbol'('SOMELEADER\x27\','SOMELEADER\x27\','src_span'(319,1,319,12,12370,11),'Funktion or Process').
351		'symbol'('alive9','alive','src_span'(319,13,319,18,12382,5),'Ident (Prolog Variable)').
352		'symbol'('m191','m','src_span'(319,39,319,40,12408,1),'Ident (Prolog Variable)').
353		'symbol'('k192','k','src_span'(319,41,319,42,12410,1),'Ident (Prolog Variable)').
354		'symbol'('k193','k','src_span'(321,14,321,15,12490,1),'Ident (Prolog Variable)').
355		'symbol'('k194','k','src_span'(322,16,322,17,12539,1),'Ident (Prolog Variable)').
356		'symbol'('m195','m','src_span'(323,21,323,22,12596,1),'Ident (Prolog Variable)').
357		'symbol'('k196','k','src_span'(323,23,323,24,12598,1),'Ident (Prolog Variable)').
358		'symbol'('FailSOMELEADER','FailSOMELEADER','src_span'(328,1,328,15,12762,14),'Ident (Groundrep.)').