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'('DATA','setExp'('rangeEnum'(['int'(0),'int'(1)])),'src_span'(29,1,29,13,1229,12)).
18		'bindval'('TAG','setExp'('rangeEnum'(['int'(0),'int'(1)])),'src_span'(32,1,32,12,1404,11)).
19		'channel'('left','type'('dotTupleType'(['val_of'('DATA','src_span'(34,20,34,24,1463,4))]))).
20		'channel'('right','type'('dotTupleType'(['val_of'('DATA','src_span'(34,20,34,24,1463,4))]))).
21		'channel'('a','type'('dotTupleType'(['val_of'('TAG','src_span'(35,13,35,16,1480,3)),'val_of'('DATA','src_span'(35,17,35,21,1484,4))]))).
22		'channel'('b','type'('dotTupleType'(['val_of'('TAG','src_span'(35,13,35,16,1480,3)),'val_of'('DATA','src_span'(35,17,35,21,1484,4))]))).
23		'channel'('c','type'('dotTupleType'(['val_of'('TAG','src_span'(36,13,36,16,1501,3))]))).
24		'channel'('d','type'('dotTupleType'(['val_of'('TAG','src_span'(36,13,36,16,1501,3))]))).
25		'agent'('BUFF'(_s),'ifte'('agent_call'('src_span'(42,15,42,19,1694,4),'null',[_s]),'prefix'('src_span'(42,30,42,34,1709,4),['in'(_x)],'left','agent_call'('src_span'(42,40,42,44,1719,4),'BUFF',['listExp'('rangeEnum'([_x]))]),'src_span'(42,37,42,39,1715,15)),'[]'('prefix'('src_span'(43,19,43,24,1748,5),['out'('agent_call'('src_span'(43,26,43,30,1755,4),'head',[_s]))],'right','agent_call'('src_span'(43,38,43,42,1767,4),'BUFF',['agent_call'('src_span'(43,43,43,47,1772,4),'tail',[_s])]),'src_span'(43,35,43,37,1763,27)),'|~|'('stop'('src_span'(44,21,44,25,1802,4)),'ifte'('=='('#'(_s),'val_of'('N','src_span'(44,41,44,42,1822,1))),'stop'('src_span'(44,49,44,53,1830,4)),'prefix'('src_span'(45,37,45,41,1871,4),['in'(_x2)],'left','agent_call'('src_span'(45,47,45,51,1881,4),'BUFF',['^'(_s,'listExp'('rangeEnum'([_x2])))]),'src_span'(45,44,45,46,1877,17)),'src_span'(44,31,44,43,1812,12),'src_span'(44,44,44,48,1824,19),'src_span'(44,54,45,35,1834,63)),'src_span_operator'('no_loc_info_available','src_span'(44,26,44,29,1807,3))),'src_span_operator'('no_loc_info_available','src_span'(44,18,44,20,1799,2))),'src_span'(42,11,42,23,1690,12),'src_span'(42,24,42,28,1702,36),'src_span'(42,51,43,16,1729,188)),'src_span'(42,11,45,62,1690,206)).
26		'bindval'('N','int'(3),'src_span'(49,1,49,6,1931,5)).
27		'bindval'('SPEC','agent_call'('src_span'(51,8,51,12,2013,4),'BUFF',['listExp'('rangeEnum'([]))]),'src_span'(51,1,51,16,2006,15)).
28		'bindval'('L','int'(3),'src_span'(59,1,59,6,2363,5)).
29		'agent'('E'(_n),'prefix'('src_span'(61,8,61,9,2377,1),['in'(_tag),'in'(_data)],'a','ifte'('=='(_n,'int'(0)),'prefix'('src_span'(61,39,61,40,2408,1),['out'(_tag),'out'(_data)],'b','agent_call'('src_span'(61,53,61,54,2422,1),'E',['-'('val_of'('L','src_span'(61,55,61,56,2424,1)),'int'(1))]),'src_span'(61,50,61,52,2418,15)),'|~|'('prefix'('src_span'(62,32,62,33,2461,1),['out'(_tag),'out'(_data)],'b','agent_call'('src_span'(62,46,62,47,2475,1),'E',['-'('val_of'('L','src_span'(62,48,62,49,2477,1)),'int'(1))]),'src_span'(62,43,62,45,2471,15)),'agent_call'('src_span'(62,59,62,60,2488,1),'E',['-'(_n,'int'(1))]),'src_span_operator'('no_loc_info_available','src_span'(62,54,62,57,2483,3))),'src_span'(61,23,61,32,2392,9),'src_span'(61,33,61,37,2401,34),'src_span'(61,61,62,29,2429,88)),'src_span'(61,19,61,21,2387,114)),'src_span'(61,8,62,67,2377,119)).
30		'agent'('F'(_n2),'prefix'('src_span'(64,8,64,9,2505,1),['in'(_tag2)],'c','ifte'('=='(_n2,'int'(0)),'prefix'('src_span'(64,34,64,35,2531,1),['out'(_tag2)],'d','agent_call'('src_span'(64,43,64,44,2540,1),'F',['-'('val_of'('L','src_span'(64,45,64,46,2542,1)),'int'(1))]),'src_span'(64,40,64,42,2536,14)),'|~|'('prefix'('src_span'(65,32,65,33,2579,1),['out'(_tag2)],'d','agent_call'('src_span'(65,41,65,42,2588,1),'F',['-'('val_of'('L','src_span'(65,43,65,44,2590,1)),'int'(1))]),'src_span'(65,38,65,40,2584,14)),'agent_call'('src_span'(65,54,65,55,2601,1),'F',['-'(_n2,'int'(1))]),'src_span_operator'('no_loc_info_available','src_span'(65,49,65,52,2596,3))),'src_span'(64,18,64,27,2515,9),'src_span'(64,28,64,32,2524,29),'src_span'(64,51,65,29,2547,78)),'src_span'(64,14,64,16,2510,103)),'src_span'(64,8,65,62,2505,104)).
31		'bindval'('Null','int'(99),'src_span'(79,1,79,8,3182,7)).
32		'agent'('SEND'(_v,_bit),'[]'('ifte'('=='(_v,'val_of'('Null','src_span'(81,25,81,29,3241,4))),'prefix'('src_span'(82,18,82,22,3270,4),['in'(_x3)],'left','agent_call'('src_span'(82,28,82,32,3280,4),'SEND',[_x3,'-'('int'(1),_bit)]),'src_span'(82,25,82,27,3276,21)),'prefix'('src_span'(83,18,83,19,3320,1),['out'(_bit),'out'(_v)],'a','agent_call'('src_span'(83,29,83,33,3331,4),'SEND',[_v,_bit]),'src_span'(83,26,83,28,3327,17)),'src_span'(81,16,81,30,3232,14),'src_span'(81,31,82,16,3246,61),'src_span'(82,45,83,16,3296,74)),'prefix'('src_span'(84,18,84,19,3362,1),['in'(_ack)],'d','ifte'('=='(_ack,_bit),'agent_call'('src_span'(84,46,84,50,3390,4),'SEND',['val_of'('Null','src_span'(84,51,84,55,3395,4)),_bit]),'agent_call'('src_span'(85,30,85,34,3435,4),'SEND',[_v,_bit]),'src_span'(84,27,84,40,3371,13),'src_span'(84,41,84,45,3384,30),'src_span'(84,61,85,29,3404,56)),'src_span'(84,24,84,25,3367,84)),'src_span_operator'('no_loc_info_available','src_span'(84,15,84,17,3359,2))),'no_loc_info_available').
33		'bindval'('SND','agent_call'('src_span'(89,7,89,11,3538,4),'SEND',['val_of'('Null','src_span'(89,12,89,16,3543,4)),'int'(1)]),'src_span'(89,1,89,19,3532,18)).
34		'agent'('REC'(_bit2),'[]'('prefix'('src_span'(97,12,97,13,3871,1),['in'(_tag3),'in'(_data2)],'b','ifte'('=='(_tag3,_bit2),'prefix'('src_span'(97,46,97,51,3905,5),['out'(_data2)],'right','agent_call'('src_span'(97,60,97,63,3919,3),'REC',['-'('int'(1),_bit2)]),'src_span'(97,57,97,59,3915,19)),'agent_call'('src_span'(98,44,98,47,3973,3),'REC',[_bit2]),'src_span'(97,27,97,40,3886,13),'src_span'(97,41,97,45,3899,40),'src_span'(97,71,98,43,3929,76)),'src_span'(97,23,97,25,3881,106)),'prefix'('src_span'(99,16,99,17,3998,1),['out'('-'('int'(1),_bit2))],'c','agent_call'('src_span'(99,29,99,32,4011,3),'REC',[_bit2]),'src_span'(99,26,99,28,4007,20)),'src_span_operator'('no_loc_info_available','src_span'(99,12,99,14,3994,2))),'no_loc_info_available').
35		'bindval'('DRCV','agent_call'('src_span'(104,8,104,11,4126,3),'REC',['int'(0)]),'src_span'(104,1,104,14,4119,13)).
36		'bindval'('DIVSYSTEM','\x5c\'('sharing'('closure'(['a','d']),'val_of'('SND','src_span'(114,13,114,16,4573,3)),'sharing'('closure'(['b','c']),'|||'('agent_call'('src_span'(114,31,114,32,4591,1),'E',['-'('val_of'('L','src_span'(114,33,114,34,4593,1)),'int'(1))]),'agent_call'('src_span'(114,40,114,41,4600,1),'F',['-'('val_of'('L','src_span'(114,42,114,43,4602,1)),'int'(1))]),'src_span_operator'('no_loc_info_available','src_span'(114,37,114,40,4597,3))),'val_of'('DRCV','src_span'(114,60,114,64,4620,4)),'src_span'(114,47,114,60,4607,13)),'src_span'(114,16,114,29,4576,13)),'closure'(['a','b','c','d']),'src_span_operator'('no_loc_info_available','src_span'(114,65,114,66,4625,1))),'src_span'(114,1,114,77,4561,76)).
37		'assertRef'('False','val_of'('SPEC','src_span'(116,8,116,12,4646,4)),'Trace','val_of'('DIVSYSTEM','src_span'(116,17,116,26,4655,9)),'src_span'(116,1,116,26,4639,25)).
38		'assertRef'('True','val_of'('SPEC','src_span'(117,12,117,16,4677,4)),'FailureDivergence','val_of'('DIVSYSTEM','src_span'(117,22,117,31,4687,9)),'src_span'(117,1,117,31,4666,30)).
39		'bindval'('ALT','prefix'('src_span'(126,7,126,8,5109,1),['in'(_bit3),'in'(_data3)],'b','prefix'('src_span'(126,21,126,22,5123,1),['in'(_bit4)],'c','val_of'('ALT','src_span'(126,30,126,33,5132,3)),'src_span'(126,27,126,29,5128,11)),'src_span'(126,18,126,20,5119,21)),'src_span'(126,1,126,33,5103,32)).
40		'agent'('LIMITc'(_M,_n3),'[]'('prefix'('src_span'(130,15,130,16,5174,1),['in'(_bit5),'in'(_data4)],'b','agent_call'('src_span'(130,29,130,35,5188,6),'LIMITb',[_M,'int'(1)]),'src_span'(130,26,130,28,5184,20)),'ifte'('=='(_n3,_M),'stop'('src_span'(131,32,131,36,5231,4)),'prefix'('src_span'(131,43,131,44,5242,1),['in'(_bit6)],'c','agent_call'('src_span'(131,52,131,58,5251,6),'LIMITc',[_M,'+'(_n3,'int'(1))]),'src_span'(131,49,131,51,5247,23)),'src_span'(131,17,131,26,5216,9),'src_span'(131,27,131,31,5225,16),'src_span'(131,37,131,41,5235,36)),'src_span_operator'('no_loc_info_available','src_span'(131,14,131,16,5213,2))),'no_loc_info_available').
41		'agent'('LIMITb'(_M2,_n4),'[]'('prefix'('src_span'(133,15,133,16,5284,1),['in'(_bit7)],'c','agent_call'('src_span'(133,24,133,30,5293,6),'LIMITc',[_M2,'int'(1)]),'src_span'(133,21,133,23,5289,19)),'ifte'('=='(_n4,_M2),'stop'('src_span'(134,32,134,36,5336,4)),'prefix'('src_span'(134,43,134,44,5347,1),['in'(_bit8),'in'(_data5)],'b','agent_call'('src_span'(134,57,134,63,5361,6),'LIMITb',[_M2,'+'(_n4,'int'(1))]),'src_span'(134,54,134,56,5357,24)),'src_span'(134,17,134,26,5321,9),'src_span'(134,27,134,31,5330,16),'src_span'(134,37,134,41,5340,41)),'src_span_operator'('no_loc_info_available','src_span'(134,14,134,16,5318,2))),'no_loc_info_available').
42		'agent'('LIMIT'(_M3),'[]'('prefix'('src_span'(136,13,136,14,5392,1),['in'(_bit9)],'c','agent_call'('src_span'(136,22,136,28,5401,6),'LIMITc',[_M3,'int'(1)]),'src_span'(136,19,136,21,5397,19)),'prefix'('src_span'(136,37,136,38,5416,1),['in'(_bit75),'in'(_data6)],'b','agent_call'('src_span'(136,51,136,57,5430,6),'LIMITb',[_M3,'int'(1)]),'src_span'(136,48,136,50,5426,20)),'src_span_operator'('no_loc_info_available','src_span'(136,34,136,36,5413,2))),'no_loc_info_available').
43		'agent'('NDC'(_M4,_n5),'ifte'('=='(_n5,'int'(0)),'prefix'('src_span'(141,29,141,30,5564,1),['in'(_bit79)],'c','agent_call'('src_span'(141,38,141,41,5573,3),'NDC',[_M4,'int'(1)]),'src_span'(141,35,141,37,5569,16)),'ifte'('=='(_n5,_M4),'prefix'('src_span'(142,34,142,35,5616,1),['in'(_bit80),'in'(_data7)],'b','agent_call'('src_span'(142,48,142,51,5630,3),'NDC',[_M4,'-'(_M4,'int'(1))]),'src_span'(142,45,142,47,5626,21)),'|~|'('prefix'('src_span'(143,20,143,21,5663,1),['in'(_bit82)],'c','agent_call'('src_span'(143,29,143,32,5672,3),'NDC',[_M4,'+'(_n5,'int'(1))]),'src_span'(143,26,143,28,5668,20)),'prefix'('src_span'(143,48,143,49,5691,1),['in'(_bit83),'in'(_data8)],'b','agent_call'('src_span'(143,62,143,65,5705,3),'NDC',[_M4,'-'(_n5,'int'(1))]),'src_span'(143,59,143,61,5701,21)),'src_span_operator'('no_loc_info_available','src_span'(143,43,143,46,5686,3))),'src_span'(142,18,142,27,5600,9),'src_span'(142,28,142,32,5609,40),'src_span'(142,62,143,17,5643,104)),'src_span'(141,13,141,22,5548,9),'src_span'(141,23,141,27,5557,31),'src_span'(141,48,142,17,5582,156)),'src_span'(141,12,143,77,5547,173)).
44		'bindval'('RCVA','sharing'('closure'(['b','c']),'val_of'('DRCV','src_span'(150,8,150,12,5921,4)),'val_of'('ALT','src_span'(150,23,150,26,5936,3)),'src_span'(150,12,150,23,5925,11)),'src_span'(150,1,150,26,5914,25)).
45		'bindval'('RCVL','sharing'('closure'(['b','c']),'val_of'('DRCV','src_span'(151,8,151,12,5947,4)),'agent_call'('src_span'(151,23,151,28,5962,5),'LIMIT',['int'(3)]),'src_span'(151,12,151,23,5951,11)),'src_span'(151,1,151,31,5940,30)).
46		'bindval'('RCVN','sharing'('closure'(['b','c']),'val_of'('DRCV','src_span'(152,8,152,12,5978,4)),'agent_call'('src_span'(152,23,152,26,5993,3),'NDC',['int'(4),'int'(2)]),'src_span'(152,12,152,23,5982,11)),'src_span'(152,1,152,31,5971,30)).
47		'bindval'('ASYSTEM','\x5c\'('sharing'('closure'(['a','d']),'val_of'('SND','src_span'(156,11,156,14,6068,3)),'sharing'('closure'(['b','c']),'|||'('agent_call'('src_span'(156,27,156,28,6084,1),'E',['-'('val_of'('L','src_span'(156,29,156,30,6086,1)),'int'(1))]),'agent_call'('src_span'(156,36,156,37,6093,1),'F',['-'('val_of'('L','src_span'(156,38,156,39,6095,1)),'int'(1))]),'src_span_operator'('no_loc_info_available','src_span'(156,33,156,36,6090,3))),'val_of'('RCVA','src_span'(156,54,156,58,6111,4)),'src_span'(156,43,156,54,6100,11)),'src_span'(156,14,156,25,6071,11)),'closure'(['a','b','c','d']),'src_span_operator'('no_loc_info_available','src_span'(156,59,156,60,6116,1))),'src_span'(156,1,156,71,6058,70)).
48		'bindval'('LSYSTEM','\x5c\'('sharing'('closure'(['a','d']),'val_of'('SND','src_span'(158,11,158,14,6140,3)),'sharing'('closure'(['b','c']),'|||'('agent_call'('src_span'(158,27,158,28,6156,1),'E',['-'('val_of'('L','src_span'(158,29,158,30,6158,1)),'int'(1))]),'agent_call'('src_span'(158,36,158,37,6165,1),'F',['-'('val_of'('L','src_span'(158,38,158,39,6167,1)),'int'(1))]),'src_span_operator'('no_loc_info_available','src_span'(158,33,158,36,6162,3))),'val_of'('RCVL','src_span'(158,54,158,58,6183,4)),'src_span'(158,43,158,54,6172,11)),'src_span'(158,14,158,25,6143,11)),'closure'(['a','b','c','d']),'src_span_operator'('no_loc_info_available','src_span'(158,59,158,60,6188,1))),'src_span'(158,1,158,71,6130,70)).
49		'bindval'('NSYSTEM','\x5c\'('sharing'('closure'(['a','d']),'val_of'('SND','src_span'(160,11,160,14,6212,3)),'sharing'('closure'(['b','c']),'|||'('agent_call'('src_span'(160,27,160,28,6228,1),'E',['-'('val_of'('L','src_span'(160,29,160,30,6230,1)),'int'(1))]),'agent_call'('src_span'(160,36,160,37,6237,1),'F',['-'('val_of'('L','src_span'(160,38,160,39,6239,1)),'int'(1))]),'src_span_operator'('no_loc_info_available','src_span'(160,33,160,36,6234,3))),'val_of'('RCVN','src_span'(160,54,160,58,6255,4)),'src_span'(160,43,160,54,6244,11)),'src_span'(160,14,160,25,6215,11)),'closure'(['a','b','c','d']),'src_span_operator'('no_loc_info_available','src_span'(160,59,160,60,6260,1))),'src_span'(160,1,160,71,6202,70)).
50		'assertRef'('False','val_of'('SPEC','src_span'(164,8,164,12,6319,4)),'FailureDivergence','val_of'('ASYSTEM','src_span'(164,18,164,25,6329,7)),'src_span'(164,1,164,25,6312,24)).
51		'assertRef'('False','val_of'('SPEC','src_span'(165,8,165,12,6344,4)),'FailureDivergence','val_of'('LSYSTEM','src_span'(165,18,165,25,6354,7)),'src_span'(165,1,165,25,6337,24)).
52		'assertRef'('False','val_of'('SPEC','src_span'(166,8,166,12,6369,4)),'FailureDivergence','val_of'('NSYSTEM','src_span'(166,18,166,25,6379,7)),'src_span'(166,1,166,25,6362,24)).
53		'agent'('RECimp'(_bit85),'prefix'('src_span'(173,15,173,16,6625,1),['in'(_tag4),'in'(_data9)],'b','ifte'('=='(_tag4,_bit85),'prefix'('src_span'(174,43,174,48,6702,5),['out'(_data9)],'right','prefix'('src_span'(174,57,174,58,6716,1),['out'(_tag4)],'c','agent_call'('src_span'(174,66,174,72,6725,6),'RECimp',['-'('int'(1),_bit85)]),'src_span'(174,63,174,65,6721,21)),'src_span'(174,54,174,56,6712,31)),'prefix'('src_span'(175,46,175,47,6785,1),['out'(_tag4)],'c','agent_call'('src_span'(175,55,175,61,6794,6),'RECimp',[_bit85]),'src_span'(175,52,175,54,6790,19)),'src_span'(173,30,173,43,6640,13),'src_span'(173,44,174,41,6653,96),'src_span'(174,81,175,44,6739,105)),'src_span'(173,26,173,28,6635,177)),'src_span'(173,15,175,68,6625,182)).
54		'bindval'('RCVimp','agent_call'('src_span'(177,8,177,14,6816,6),'RECimp',['int'(0)]),'src_span'(177,1,177,17,6809,16)).
55		'bindval'('SYSTEMimp','\x5c\'('sharing'('closure'(['a','d']),'val_of'('SND','src_span'(182,13,182,16,6990,3)),'sharing'('closure'(['b','c']),'|||'('agent_call'('src_span'(182,29,182,30,7006,1),'E',['-'('val_of'('L','src_span'(182,31,182,32,7008,1)),'int'(1))]),'agent_call'('src_span'(182,38,182,39,7015,1),'F',['-'('val_of'('L','src_span'(182,40,182,41,7017,1)),'int'(1))]),'src_span_operator'('no_loc_info_available','src_span'(182,35,182,38,7012,3))),'val_of'('RCVimp','src_span'(182,56,182,62,7033,6)),'src_span'(182,45,182,56,7022,11)),'src_span'(182,16,182,27,6993,11)),'closure'(['a','b','c','d']),'src_span_operator'('no_loc_info_available','src_span'(182,63,182,64,7040,1))),'src_span'(182,1,182,75,6978,74)).
56		'assertRef'('False','val_of'('SPEC','src_span'(184,8,184,12,7061,4)),'FailureDivergence','val_of'('SYSTEMimp','src_span'(184,18,184,27,7071,9)),'src_span'(184,1,184,27,7054,26)).
57		'bindval'('MAIN','val_of'('SYSTEMimp','src_span'(222,8,222,17,8423,9)),'src_span'(222,1,222,17,8416,16)).
58		'comment'('lineComment'('-- abp.csp'),'src_position'(1,1,0,10)).
59		'comment'('lineComment'('-- Alternating bit protocol.'),'src_position'(3,1,12,28)).
60		'comment'('lineComment'('-- Bill Roscoe, August 1992'),'src_position'(5,1,42,27)).
61		'comment'('lineComment'('-- FDR2 version, June 1996'),'src_position'(6,1,70,26)).
62		'comment'('lineComment'('-- This is the simplest of a number of our examples'),'src_position'(8,1,98,51)).
63		'comment'('lineComment'('-- which make use of a pair of media'),'src_position'(9,1,150,36)).
64		'comment'('lineComment'('-- which are permitted to lose data, and provided no infinite sequence is lost'),'src_position'(10,1,187,78)).
65		'comment'('lineComment'('-- will work independently of how lossy the channels are (unlike the file'),'src_position'(11,1,266,73)).
66		'comment'('lineComment'('-- prots.csp where the protocols were designed to cope with specific badnesses).-- They work by transmitting messages one way and acknowledgements the other.'),'src_position'(12,1,340,157)).
67		'comment'('lineComment'('-- The alternating bit protocol provides the most standard of all protocol'),'src_position'(14,1,499,74)).
68		'comment'('lineComment'('-- examples, and is while it is too simple for practical purposes, its'),'src_position'(15,1,574,70)).
69		'comment'('lineComment'('-- analysis contains much that remains relevant in realistic examples.'),'src_position'(16,1,645,70)).
70		'comment'('lineComment'('-- You will find a number of other versions of this protocol in this'),'src_position'(18,1,717,68)).
71		'comment'('lineComment'('-- collection of example files: at least in chapter8, chapter12 and'),'src_position'(19,1,786,67)).
72		'comment'('lineComment'('-- chapter14. There are also other communication protocol files in'),'src_position'(20,1,854,67)).
73		'comment'('lineComment'('-- chapter12 (where the most satisfactory model of fault tolerance is'),'src_position'(21,1,922,69)).
74		'comment'('lineComment'('-- developed).'),'src_position'(22,1,992,14)).
75		'comment'('lineComment'('-- CHANNELS and DATA TYPES'),'src_position'(24,1,1008,26)).
76		'comment'('lineComment'('-- left and right are the external input and output, which we set to'),'src_position'(25,1,1035,68)).
77		'comment'('lineComment'('-- one-bit. a and b carry a tag and a data value.'),'src_position'(26,1,1104,50)).
78		'comment'('lineComment'('-- c and d carry an acknowledgement tag. In this protocol tags are bits'),'src_position'(27,1,1155,72)).
79		'comment'('lineComment'('-- in a data-independent program, where nothing is done to'),'src_position'(29,15,1243,58)).
80		'comment'('lineComment'('-- or conditional on data, this is sufficient to establish'),'src_position'(30,15,1316,58)).
81		'comment'('lineComment'('-- correctness'),'src_position'(31,15,1389,14)).
82		'comment'('lineComment'('-- the alternating bits.'),'src_position'(32,15,1418,24)).
83		'comment'('lineComment'('-- The overall specification we want to meet is that of a buffer. The'),'src_position'(38,1,1506,70)).
84		'comment'('lineComment'('-- most nondeterministic (left-to-right) buffer with size bounded by N is'),'src_position'(39,1,1577,73)).
85		'comment'('lineComment'('-- given by BUFF(<>), where'),'src_position'(40,1,1651,27)).
86		'comment'('lineComment'('-- For our purposes we will set'),'src_position'(47,1,1898,31)).
87		'comment'('lineComment'('-- since this example does not introduce more buffering than this.'),'src_position'(49,8,1938,66)).
88		'comment'('lineComment'('-- The protocol is designed to work in the presence of lossy channels.'),'src_position'(53,1,2023,70)).
89		'comment'('lineComment'('-- We specify here channels which must transmit one out of any L=3 values, but '),'src_position'(54,1,2094,79)).
90		'comment'('lineComment'('-- any definition would work provided it maintains order and does not lose'),'src_position'(55,1,2174,74)).
91		'comment'('lineComment'('-- an infinite sequence of values. The only difference would evidence itself'),'src_position'(56,1,2249,77)).
92		'comment'('lineComment'('-- in the size of the state-space!'),'src_position'(57,1,2327,34)).
93		'comment'('lineComment'('-- Increasing L makes this definition less deterministic. '),'src_position'(67,1,2611,59)).
94		'comment'('lineComment'('-- The implementation of the protocol consists of a sender process and'),'src_position'(69,1,2672,70)).
95		'comment'('lineComment'('-- receiver process, linked by E and F above. '),'src_position'(70,1,2743,47)).
96		'comment'('lineComment'('-- In the text, the medium processes considered have the additional'),'src_position'(71,1,2791,67)).
97		'comment'('lineComment'('-- ability to duplicate messages boundedly. It easy to extend this'),'src_position'(72,1,2859,67)).
98		'comment'('lineComment'('-- file to that case, and this is left as an exercise.'),'src_position'(73,1,2927,54)).
99		'comment'('lineComment'('-- The sender process is parameterised by the current value it tries to send'),'src_position'(75,1,2983,76)).
100		'comment'('lineComment'('-- out, which may be null in which case it does not try to send it, but'),'src_position'(76,1,3060,72)).
101		'comment'('lineComment'('-- instead accepts a new one from channel left.'),'src_position'(77,1,3133,47)).
102		'comment'('lineComment'('-- any value not in DATA'),'src_position'(79,10,3191,24)).
103		'comment'('lineComment'('-- Initially the data value is Null & bit=1 so the first value input gets bit=0.'),'src_position'(87,1,3450,80)).
104		'comment'('lineComment'('-- The basic part of the receiver takes in messages, sends acknowledgements,'),'src_position'(91,1,3552,76)).
105		'comment'('lineComment'('-- and transmits messages to the environment. REC(b) is a process that'),'src_position'(92,1,3629,71)).
106		'comment'('lineComment'('-- will always accept a message or send an acknowledgement, save that it'),'src_position'(93,1,3701,72)).
107		'comment'('lineComment'('-- will not do so when it has a pending message to transmit to'),'src_position'(94,1,3774,62)).
108		'comment'('lineComment'('-- the environment. '),'src_position'(95,1,3837,21)).
109		'comment'('lineComment'('-- The first message to be output has tag 0, and there is no pending'),'src_position'(101,1,4037,68)).
110		'comment'('lineComment'('-- message.'),'src_position'(102,1,4106,11)).
111		'comment'('lineComment'('-- If this receiver is placed in the system, there is the danger of'),'src_position'(106,1,4134,67)).
112		'comment'('lineComment'('-- livelock, or divergence, if an infinite sequence of acknowledgements is'),'src_position'(107,1,4202,74)).
113		'comment'('lineComment'('-- transmitted by REC and received by SEND without the next message being'),'src_position'(108,1,4277,73)).
114		'comment'('lineComment'('-- transmitted, as is possible. Alternatively, a message can be transmitted'),'src_position'(109,1,4351,76)).
115		'comment'('lineComment'('-- and received infinitely without being acknowledged.'),'src_position'(110,1,4428,54)).
116		'comment'('lineComment'('-- Thus, while the following system is'),'src_position'(111,1,4483,38)).
117		'comment'('lineComment'('-- partially correct, it can diverge:'),'src_position'(112,1,4522,37)).
118		'comment'('lineComment'('-- We can avoid divergence by preventing the receiver acknowledging or'),'src_position'(119,1,4698,70)).
119		'comment'('lineComment'('-- receiving infinitely without doing the other. This can be done by'),'src_position'(120,1,4769,69)).
120		'comment'('lineComment'('-- putting it in parallel with any process which allows these actions'),'src_position'(121,1,4839,69)).
121		'comment'('lineComment'('-- in such a way as to avoid these infinitely unfair sequences. In fact,'),'src_position'(122,1,4909,73)).
122		'comment'('lineComment'('-- the receiver may choose one of the two to do rather than give the'),'src_position'(123,1,4983,68)).
123		'comment'('lineComment'('-- choice as above. Examples that will work are:'),'src_position'(124,1,5052,49)).
124		'comment'('lineComment'('-- simple alternation'),'src_position'(128,1,5137,21)).
125		'comment'('lineComment'('-- gives the environment the choice, provided there is no run of more'),'src_position'(138,1,5444,69)).
126		'comment'('lineComment'('-- than M of either.'),'src_position'(139,1,5514,20)).
127		'comment'('lineComment'('-- chooses nondeterministically which to allow, within provided the totals'),'src_position'(145,1,5722,74)).
128		'comment'('lineComment'('-- of b\x27\s and c\x27\s do not differ too much.'),'src_position'(146,1,5797,41)).
129		'comment'('lineComment'('-- Modified receiver processes, with small values for the constants, are'),'src_position'(148,1,5840,72)).
130		'comment'('lineComment'('-- and the respective systems to check against SPEC:'),'src_position'(154,1,6004,52)).
131		'comment'('lineComment'('-- We can now prove full refinement '),'src_position'(162,1,6274,36)).
132		'comment'('lineComment'('--un'),'src_position'(166,26,6387,4)).
133		'comment'('lineComment'('-- of course, one would not normally construct one\x27\s receiver as a composition'),'src_position'(169,1,6394,78)).
134		'comment'('lineComment'('-- of an algorithmic process and constraint in this way, but we now know that'),'src_position'(170,1,6473,77)).
135		'comment'('lineComment'('-- any receiver which refines RCVN (for example) will work'),'src_position'(171,1,6551,58)).
136		'comment'('lineComment'('-- You can check that RCVimp refines RCVN, which proves that the revised'),'src_position'(179,1,6827,72)).
137		'comment'('lineComment'('-- system below is correct. This can, in this instance, be proved directly!'),'src_position'(180,1,6900,76)).
138		'comment'('lineComment'('-- un'),'src_position'(184,28,7081,5)).
139		'comment'('lineComment'('-- Indeed, RCVimp actually equals (semantically) RCVA, and you can check'),'src_position'(186,1,7088,72)).
140		'comment'('lineComment'('-- that refinement either way.'),'src_position'(187,1,7161,30)).
141		'comment'('lineComment'('-- If you want to develop this example much further, perhaps by inserting'),'src_position'(189,1,7193,73)).
142		'comment'('lineComment'('-- a more interesting process in one or both channels, the state-space may'),'src_position'(190,1,7267,74)).
143		'comment'('lineComment'('-- grow uncomfortably large for a Full check (including absence of divergence).'),'src_position'(191,1,7342,79)).
144		'comment'('lineComment'('-- Any different channel definitions which satisfy'),'src_position'(193,1,7423,50)).
145		'comment'('lineComment'('-- outputs(tr) subseq of inputs(tr) in the obvious sense;'),'src_position'(195,1,7475,60)).
146		'comment'('lineComment'('-- will not do an infinite sequence of inputs without an output;'),'src_position'(197,1,7537,64)).
147		'comment'('lineComment'('-- and refines '),'src_position'(199,1,7603,15)).
148		'comment'('lineComment'('-- We cannot parse this: because events is not defined'),'src_position'(201,1,7620,54)).
149		'comment'('lineComment'('-- IorO(inp, outp) = inp?x -> IorO(inp,outp) |~| '),'src_position'(202,1,7675,49)).
150		'comment'('lineComment'('-- (|~| x:events(outp) @ x -> IorO(inp,outp))'),'src_position'(203,1,7725,63)).
151		'comment'('lineComment'('-- (i.e., can always either input any value, or make an output).'),'src_position'(205,1,7790,64)).
152		'comment'('lineComment'('-- is substitutable for E and/or F.'),'src_position'(207,1,7856,35)).
153		'comment'('lineComment'('-- Note the relationship of the above statement to what is said'),'src_position'(209,1,7893,63)).
154		'comment'('lineComment'('-- in the text about the buffer tolerance of ABP. It should be easy'),'src_position'(210,1,7957,68)).
155		'comment'('lineComment'('-- for you to try out the buffer tolerance claims by modifying the'),'src_position'(211,1,8026,66)).
156		'comment'('lineComment'('-- examples in this file.'),'src_position'(212,1,8093,25)).
157		'comment'('lineComment'('-- In fact, as observed in the text, all our divergence-free versions'),'src_position'(215,1,8121,69)).
158		'comment'('lineComment'('-- of the ABP are actually equivalent to COPY. Therefore, like the'),'src_position'(216,1,8191,67)).
159		'comment'('lineComment'('-- MajSys example in chapter5-1.csp, we have an example of a process'),'src_position'(217,1,8259,68)).
160		'comment'('lineComment'('-- with much internal nondeterminism displaying a deterministic face to'),'src_position'(218,1,8328,71)).
161		'comment'('lineComment'('-- the world.'),'src_position'(219,1,8400,13)).
162		'symbol'('DATA','DATA','src_span'(29,1,29,5,1229,4),'Ident (Groundrep.)').
163		'symbol'('TAG','TAG','src_span'(32,1,32,4,1404,3),'Ident (Groundrep.)').
164		'symbol'('left','left','src_span'(34,9,34,13,1452,4),'Channel').
165		'symbol'('right','right','src_span'(34,14,34,19,1457,5),'Channel').
166		'symbol'('a','a','src_span'(35,9,35,10,1476,1),'Channel').
167		'symbol'('b','b','src_span'(35,11,35,12,1478,1),'Channel').
168		'symbol'('c','c','src_span'(36,9,36,10,1497,1),'Channel').
169		'symbol'('d','d','src_span'(36,11,36,12,1499,1),'Channel').
170		'symbol'('BUFF','BUFF','src_span'(42,1,42,5,1680,4),'Funktion or Process').
171		'symbol'('s','s','src_span'(42,6,42,7,1685,1),'Ident (Prolog Variable)').
172		'symbol'('null','null','src_span'(42,15,42,19,1694,4),'BuiltIn primitive').
173		'symbol'('x','x','src_span'(42,35,42,36,1714,1),'Ident (Prolog Variable)').
174		'symbol'('head','head','src_span'(43,26,43,30,1755,4),'BuiltIn primitive').
175		'symbol'('tail','tail','src_span'(43,43,43,47,1772,4),'BuiltIn primitive').
176		'symbol'('x2','x','src_span'(45,42,45,43,1876,1),'Ident (Prolog Variable)').
177		'symbol'('N','N','src_span'(49,1,49,2,1931,1),'Ident (Groundrep.)').
178		'symbol'('SPEC','SPEC','src_span'(51,1,51,5,2006,4),'Ident (Groundrep.)').
179		'symbol'('L','L','src_span'(59,1,59,2,2363,1),'Ident (Groundrep.)').
180		'symbol'('E','E','src_span'(61,1,61,2,2370,1),'Funktion or Process').
181		'symbol'('n','n','src_span'(61,3,61,4,2372,1),'Ident (Prolog Variable)').
182		'symbol'('tag','tag','src_span'(61,10,61,13,2379,3),'Ident (Prolog Variable)').
183		'symbol'('data','data','src_span'(61,14,61,18,2383,4),'Ident (Prolog Variable)').
184		'symbol'('F','F','src_span'(64,1,64,2,2498,1),'Funktion or Process').
185		'symbol'('n2','n','src_span'(64,3,64,4,2500,1),'Ident (Prolog Variable)').
186		'symbol'('tag2','tag','src_span'(64,10,64,13,2507,3),'Ident (Prolog Variable)').
187		'symbol'('Null','Null','src_span'(79,1,79,5,3182,4),'Ident (Groundrep.)').
188		'symbol'('SEND','SEND','src_span'(81,1,81,5,3217,4),'Funktion or Process').
189		'symbol'('v','v','src_span'(81,6,81,7,3222,1),'Ident (Prolog Variable)').
190		'symbol'('bit','bit','src_span'(81,8,81,11,3224,3),'Ident (Prolog Variable)').
191		'symbol'('x3','x','src_span'(82,23,82,24,3275,1),'Ident (Prolog Variable)').
192		'symbol'('ack','ack','src_span'(84,20,84,23,3364,3),'Ident (Prolog Variable)').
193		'symbol'('SND','SND','src_span'(89,1,89,4,3532,3),'Ident (Groundrep.)').
194		'symbol'('REC','REC','src_span'(97,1,97,4,3860,3),'Funktion or Process').
195		'symbol'('bit2','bit','src_span'(97,5,97,8,3864,3),'Ident (Prolog Variable)').
196		'symbol'('tag3','tag','src_span'(97,14,97,17,3873,3),'Ident (Prolog Variable)').
197		'symbol'('data2','data','src_span'(97,18,97,22,3877,4),'Ident (Prolog Variable)').
198		'symbol'('DRCV','DRCV','src_span'(104,1,104,5,4119,4),'Ident (Groundrep.)').
199		'symbol'('DIVSYSTEM','DIVSYSTEM','src_span'(114,1,114,10,4561,9),'Ident (Groundrep.)').
200		'symbol'('ALT','ALT','src_span'(126,1,126,4,5103,3),'Ident (Groundrep.)').
201		'symbol'('bit3','bit','src_span'(126,9,126,12,5111,3),'Ident (Prolog Variable)').
202		'symbol'('data3','data','src_span'(126,13,126,17,5115,4),'Ident (Prolog Variable)').
203		'symbol'('bit4','bit','src_span'(126,23,126,26,5125,3),'Ident (Prolog Variable)').
204		'symbol'('LIMITc','LIMITc','src_span'(130,1,130,7,5160,6),'Funktion or Process').
205		'symbol'('M','M','src_span'(130,8,130,9,5167,1),'Ident (Prolog Variable)').
206		'symbol'('n3','n','src_span'(130,10,130,11,5169,1),'Ident (Prolog Variable)').
207		'symbol'('bit5','bit','src_span'(130,17,130,20,5176,3),'Ident (Prolog Variable)').
208		'symbol'('data4','data','src_span'(130,21,130,25,5180,4),'Ident (Prolog Variable)').
209		'symbol'('bit6','bit','src_span'(131,45,131,48,5244,3),'Ident (Prolog Variable)').
210		'symbol'('LIMITb','LIMITb','src_span'(133,1,133,7,5270,6),'Funktion or Process').
211		'symbol'('M2','M','src_span'(133,8,133,9,5277,1),'Ident (Prolog Variable)').
212		'symbol'('n4','n','src_span'(133,10,133,11,5279,1),'Ident (Prolog Variable)').
213		'symbol'('bit7','bit','src_span'(133,17,133,20,5286,3),'Ident (Prolog Variable)').
214		'symbol'('bit8','bit','src_span'(134,45,134,48,5349,3),'Ident (Prolog Variable)').
215		'symbol'('data5','data','src_span'(134,49,134,53,5353,4),'Ident (Prolog Variable)').
216		'symbol'('LIMIT','LIMIT','src_span'(136,1,136,6,5380,5),'Funktion or Process').
217		'symbol'('M3','M','src_span'(136,7,136,8,5386,1),'Ident (Prolog Variable)').
218		'symbol'('bit9','bit','src_span'(136,15,136,18,5394,3),'Ident (Prolog Variable)').
219		'symbol'('bit75','bit','src_span'(136,39,136,42,5418,3),'Ident (Prolog Variable)').
220		'symbol'('data6','data','src_span'(136,43,136,47,5422,4),'Ident (Prolog Variable)').
221		'symbol'('NDC','NDC','src_span'(141,1,141,4,5536,3),'Funktion or Process').
222		'symbol'('M4','M','src_span'(141,5,141,6,5540,1),'Ident (Prolog Variable)').
223		'symbol'('n5','n','src_span'(141,7,141,8,5542,1),'Ident (Prolog Variable)').
224		'symbol'('bit79','bit','src_span'(141,31,141,34,5566,3),'Ident (Prolog Variable)').
225		'symbol'('bit80','bit','src_span'(142,36,142,39,5618,3),'Ident (Prolog Variable)').
226		'symbol'('data7','data','src_span'(142,40,142,44,5622,4),'Ident (Prolog Variable)').
227		'symbol'('bit82','bit','src_span'(143,22,143,25,5665,3),'Ident (Prolog Variable)').
228		'symbol'('bit83','bit','src_span'(143,50,143,53,5693,3),'Ident (Prolog Variable)').
229		'symbol'('data8','data','src_span'(143,54,143,58,5697,4),'Ident (Prolog Variable)').
230		'symbol'('RCVA','RCVA','src_span'(150,1,150,5,5914,4),'Ident (Groundrep.)').
231		'symbol'('RCVL','RCVL','src_span'(151,1,151,5,5940,4),'Ident (Groundrep.)').
232		'symbol'('RCVN','RCVN','src_span'(152,1,152,5,5971,4),'Ident (Groundrep.)').
233		'symbol'('ASYSTEM','ASYSTEM','src_span'(156,1,156,8,6058,7),'Ident (Groundrep.)').
234		'symbol'('LSYSTEM','LSYSTEM','src_span'(158,1,158,8,6130,7),'Ident (Groundrep.)').
235		'symbol'('NSYSTEM','NSYSTEM','src_span'(160,1,160,8,6202,7),'Ident (Groundrep.)').
236		'symbol'('RECimp','RECimp','src_span'(173,1,173,7,6611,6),'Funktion or Process').
237		'symbol'('bit85','bit','src_span'(173,8,173,11,6618,3),'Ident (Prolog Variable)').
238		'symbol'('tag4','tag','src_span'(173,17,173,20,6627,3),'Ident (Prolog Variable)').
239		'symbol'('data9','data','src_span'(173,21,173,25,6631,4),'Ident (Prolog Variable)').
240		'symbol'('RCVimp','RCVimp','src_span'(177,1,177,7,6809,6),'Ident (Groundrep.)').
241		'symbol'('SYSTEMimp','SYSTEMimp','src_span'(182,1,182,10,6978,9),'Ident (Groundrep.)').
242		'symbol'('MAIN','MAIN','src_span'(222,1,222,5,8416,4),'Ident (Groundrep.)').