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		'dataTypeDef'('names',['constructor'('lois'),'constructor'('leah'),'constructor'('hugh'),'constructor'('henry')]).
18		'dataTypeDef'('data',['constructor'('Zero'),'constructor'('One')]).
19		'channel'('send','type'('dotTupleType'(['names','data']))).
20		'channel'('rec','type'('dotTupleType'(['names','data']))).
21		'channel'('in','type'('dotTupleType'(['names','names','data']))).
22		'channel'('out','type'('dotTupleType'(['names','data']))).
23		'bindval'('H','closureComp'(['comprehensionGenerator'(_n,'setExp'('rangeEnum'(['hugh','henry'])))],['dotTuple'(['send',_n]),'dotTuple'(['rec',_n])]),'src_span'(35,1,35,43,1004,42)).
24		'bindval'('L','closureComp'(['comprehensionGenerator'(_n2,'setExp'('rangeEnum'(['lois','leah'])))],['dotTuple'(['send',_n2]),'dotTuple'(['rec',_n2])]),'src_span'(37,1,37,41,1048,40)).
25		'bindval'('SendL','prefix'('src_span'(45,9,45,18,1260,9),['in'(_x)],'dotTuple'(['send','lois']),'prefix'('src_span'(45,24,45,36,1275,12),['out'(_x)],'dotTuple'(['in','lois','leah']),'val_of'('SendL','src_span'(45,42,45,47,1293,5)),'src_span'(45,39,45,41,1289,11)),'src_span'(45,21,45,23,1271,29)),'src_span'(45,1,45,47,1252,46)).
26		'bindval'('SendH','prefix'('src_span'(47,9,47,18,1308,9),['in'(_x2)],'dotTuple'(['send','hugh']),'prefix'('src_span'(47,24,47,37,1323,13),['out'(_x2)],'dotTuple'(['in','hugh','henry']),'val_of'('SendH','src_span'(47,43,47,48,1342,5)),'src_span'(47,40,47,42,1338,11)),'src_span'(47,21,47,23,1319,30)),'src_span'(47,1,47,48,1300,47)).
27		'bindval'('RecL','prefix'('src_span'(49,8,49,16,1356,8),['in'(_x3)],'dotTuple'(['out','leah']),'prefix'('src_span'(49,22,49,30,1370,8),['out'(_x3)],'dotTuple'(['rec','leah']),'val_of'('RecL','src_span'(49,36,49,40,1384,4)),'src_span'(49,33,49,35,1380,10)),'src_span'(49,19,49,21,1366,24)),'src_span'(49,1,49,40,1349,39)).
28		'bindval'('RecH','prefix'('src_span'(51,8,51,17,1397,9),['in'(_x4)],'dotTuple'(['out','henry']),'prefix'('src_span'(51,23,51,32,1412,9),['out'(_x4)],'dotTuple'(['rec','henry']),'val_of'('RecH','src_span'(51,38,51,42,1427,4)),'src_span'(51,35,51,37,1423,10)),'src_span'(51,20,51,22,1408,25)),'src_span'(51,1,51,42,1390,41)).
29		'bindval'('Medium','prefix'('src_span'(53,10,53,12,1442,2),['in'(_s),'in'(_t),'in'(_x5)],'in','prefix'('src_span'(53,22,53,25,1454,3),['out'(_t),'out'(_x5)],'out','val_of'('Medium','src_span'(53,33,53,39,1465,6)),'src_span'(53,30,53,32,1461,12)),'src_span'(53,19,53,21,1450,23)),'src_span'(53,1,53,39,1433,38)).
30		'bindval'('System1','\x5c\'('sharing'('closure'(['out']),'sharing'('closure'(['in']),'|||'('val_of'('SendL','src_span'(55,14,55,19,1486,5)),'val_of'('SendH','src_span'(55,24,55,29,1496,5)),'src_span_operator'('no_loc_info_available','src_span'(55,20,55,23,1492,3))),'val_of'('Medium','src_span'(55,42,55,48,1514,6)),'src_span'(55,31,55,41,1503,10)),'|||'('val_of'('RecL','src_span'(56,25,56,29,1546,4)),'val_of'('RecH','src_span'(56,34,56,38,1555,4)),'src_span_operator'('no_loc_info_available','src_span'(56,30,56,33,1551,3))),'src_span'(56,13,56,24,1534,11)),'closure'(['in','out']),'src_span_operator'('no_loc_info_available','src_span'(56,40,56,41,1561,1))),'src_span'(55,1,56,51,1473,99)).
31		'agent_curry'('LAbs'([_h],[_P]),'\x5c\'('sharing'(_h,_P,'builtin_call'('CHAOS'('src_span'(60,21,60,29,1656,8),_h)),'src_span'(60,16,60,21,1651,5)),_h,'src_span_operator'('no_loc_info_available','src_span'(60,30,60,31,1665,1))),'no_loc_info_available').
32		'assertModelCheckExt'('True','agent_call_curry'('LAbs',[['val_of'('H','src_span'(64,17,64,18,1749,1))],['val_of'('System1','src_span'(64,20,64,27,1752,7))]]),'Deterministic','F').
33		'bindval'('Medium2','[]'('prefix'('src_span'(73,11,73,18,1995,7),['in'(_t2),'in'(_x6)],'dotTuple'(['in','lois']),'prefix'('src_span'(73,26,73,29,2010,3),['out'(_t2),'out'(_x6)],'out','val_of'('Medium2','src_span'(73,37,73,44,2021,7)),'src_span'(73,34,73,36,2017,13)),'src_span'(73,23,73,25,2006,24)),'prefix'('src_span'(74,13,74,20,2041,7),['in'(_t3),'in'(_x7)],'dotTuple'(['in','hugh']),'agent_call'('src_span'(74,28,74,36,2056,8),'Medium2\x27\',[_t3,_x7]),'src_span'(74,25,74,27,2052,19)),'src_span_operator'('no_loc_info_available','src_span'(74,10,74,12,2038,2))),'src_span'(73,1,74,41,1985,84)).
34		'agent'('Medium2\x27\'(_t4,_x8),'[]'('prefix'('src_span'(76,17,76,24,2087,7),['in'(_t_quote),'in'(_x_quote)],'dotTuple'(['in','lois']),'prefix'('src_span'(76,34,76,37,2104,3),['out'(_t_quote),'out'(_x_quote)],'out','val_of'('Medium2','src_span'(76,47,76,54,2117,7)),'src_span'(76,44,76,46,2113,14)),'src_span'(76,31,76,33,2100,27)),'prefix'('src_span'(77,19,77,24,2143,5),['out'(_x8)],'dotTuple'(['out',_t4]),'val_of'('Medium2','src_span'(77,30,77,37,2154,7)),'src_span'(77,27,77,29,2150,13)),'src_span_operator'('no_loc_info_available','src_span'(77,16,77,18,2140,2))),'no_loc_info_available').
35		'bindval'('System2','\x5c\'('sharing'('closure'(['out']),'sharing'('closure'(['in']),'|||'('val_of'('SendL','src_span'(79,14,79,19,2176,5)),'val_of'('SendH','src_span'(79,24,79,29,2186,5)),'src_span_operator'('no_loc_info_available','src_span'(79,20,79,23,2182,3))),'val_of'('Medium2','src_span'(79,42,79,49,2204,7)),'src_span'(79,31,79,41,2193,10)),'|||'('val_of'('RecL','src_span'(80,25,80,29,2237,4)),'val_of'('RecH','src_span'(80,34,80,38,2246,4)),'src_span_operator'('no_loc_info_available','src_span'(80,30,80,33,2242,3))),'src_span'(80,13,80,24,2225,11)),'closure'(['in','out']),'src_span_operator'('no_loc_info_available','src_span'(80,40,80,41,2252,1))),'src_span'(79,1,80,51,2163,100)).
36		'assertModelCheckExt'('False','agent_call_curry'('LAbs',[['val_of'('H','src_span'(84,13,84,14,2319,1))],['val_of'('System2','src_span'(84,16,84,23,2322,7))]]),'Deterministic','F').
37		'agent'('BN'(_N,_s2,_left,_right),'[]'('&'('<'('#'(_s2),_N),'prefix'('src_span'(89,29,89,33,2479,4),['in'(_x9)],_left,'agent_call'('src_span'(89,39,89,41,2489,2),'BN',[_N,'^'(_s2,'listExp'('rangeEnum'([_x9]))),_left,_right]),'src_span'(89,36,89,38,2485,28))),'&'('>'('#'(_s2),'int'(0)),'prefix'('src_span'(90,29,90,34,2540,5),['out'('agent_call'('src_span'(90,35,90,39,2546,4),'head',[_s2]))],_right,'agent_call'('src_span'(90,46,90,48,2557,2),'BN',[_N,'agent_call'('src_span'(90,51,90,55,2562,4),'tail',[_s2]),_left,_right]),'src_span'(90,43,90,45,2553,36))),'src_span_operator'('no_loc_info_available','src_span'(90,19,90,21,2530,2))),'no_loc_info_available').
38		'assertRef'('True','agent_call'('src_span'(92,12,92,14,2594,2),'BN',['int'(3),'listExp'('rangeEnum'([])),'dotTuple'(['send','hugh']),'dotTuple'(['rec','henry'])]),'Trace','agent_call_curry'('LAbs',[['val_of'('L','src_span'(92,50,92,51,2632,1))],['val_of'('System2','src_span'(92,53,92,60,2635,7))]]),'src_span'(92,1,92,61,2583,60)).
39		'assertRef'('False','agent_call'('src_span'(97,8,97,10,2786,2),'BN',['int'(3),'listExp'('rangeEnum'([])),'dotTuple'(['send','lois']),'dotTuple'(['rec','leah'])]),'Failure','agent_call_curry'('LAbs',[['val_of'('H','src_span'(97,45,97,46,2823,1))],['val_of'('System2','src_span'(97,48,97,55,2826,7))]]),'src_span'(97,1,97,56,2779,55)).
40		'channel'('ok','type'('dotUnitType')).
41		'channel'('ref','type'('dotUnitType')).
42		'bindval'('SendH3','prefix'('src_span'(107,10,107,19,3020,9),['in'(_x71)],'dotTuple'(['send','hugh']),'prefix'('src_span'(107,25,107,38,3035,13),['out'(_x71)],'dotTuple'(['in','hugh','henry']),'agent_call'('src_span'(107,44,107,51,3054,7),'SendH3\x27\',[_x71]),'src_span'(107,41,107,43,3050,16)),'src_span'(107,22,107,24,3031,35)),'src_span'(107,1,107,54,3011,53)).
43		'agent'('SendH3\x27\'(_x72),'[]'('prefix'('src_span'(109,14,109,16,3079,2),[],'ok','val_of'('SendH3','src_span'(109,20,109,26,3085,6)),'src_span'(109,17,109,19,3081,12)),'prefix'('src_span'(110,16,110,19,3107,3),[],'ref','prefix'('src_span'(110,23,110,36,3114,13),['out'(_x72)],'dotTuple'(['in','hugh','henry']),'agent_call'('src_span'(110,42,110,49,3133,7),'SendH3\x27\',[_x72]),'src_span'(110,39,110,41,3129,16)),'src_span'(110,20,110,22,3110,36)),'src_span_operator'('no_loc_info_available','src_span'(110,13,110,15,3104,2))),'no_loc_info_available').
44		'bindval'('Medium3','[]'('prefix'('src_span'(112,11,112,18,3156,7),['in'(_t5),'in'(_x74)],'dotTuple'(['in','lois']),'prefix'('src_span'(112,26,112,29,3171,3),['out'(_t5),'out'(_x74)],'out','val_of'('Medium3','src_span'(112,37,112,44,3182,7)),'src_span'(112,34,112,36,3178,13)),'src_span'(112,23,112,25,3167,24)),'prefix'('src_span'(113,13,113,20,3202,7),['in'(_t6),'in'(_x76)],'dotTuple'(['in','hugh']),'agent_call'('src_span'(113,28,113,36,3217,8),'Medium3\x27\',[_t6,_x76]),'src_span'(113,25,113,27,3213,19)),'src_span_operator'('no_loc_info_available','src_span'(113,10,113,12,3199,2))),'src_span'(112,1,113,41,3146,84)).
45		'agent'('Medium3\x27\'(_t7,_x78),'[]'('prefix'('src_span'(115,17,115,24,3248,7),['in'(_t_quote2),'in'(_x_quote2)],'dotTuple'(['in','lois']),'prefix'('src_span'(115,34,115,37,3265,3),[],'ref','prefix'('src_span'(115,41,115,44,3272,3),['out'(_t_quote2),'out'(_x_quote2)],'out','val_of'('Medium3','src_span'(115,54,115,61,3285,7)),'src_span'(115,51,115,53,3281,14)),'src_span'(115,38,115,40,3268,27)),'src_span'(115,31,115,33,3261,34)),'prefix'('src_span'(116,19,116,24,3311,5),['out'(_x78)],'dotTuple'(['out',_t7]),'prefix'('src_span'(116,30,116,32,3322,2),[],'ok','val_of'('Medium3','src_span'(116,37,116,44,3329,7)),'src_span'(116,33,116,36,3324,14)),'src_span'(116,27,116,29,3318,20)),'src_span_operator'('no_loc_info_available','src_span'(116,16,116,18,3308,2))),'no_loc_info_available').
46		'bindval'('System3','\x5c\'('sharing'('closure'(['out']),'sharing'('closure'(['in','ok','ref']),'|||'('val_of'('SendL','src_span'(118,14,118,19,3351,5)),'val_of'('SendH3','src_span'(118,24,118,30,3361,6)),'src_span_operator'('no_loc_info_available','src_span'(118,20,118,23,3357,3))),'val_of'('Medium3','src_span'(118,50,118,57,3387,7)),'src_span'(118,32,118,49,3369,17)),'|||'('val_of'('RecL','src_span'(119,25,119,29,3420,4)),'val_of'('RecH','src_span'(119,34,119,38,3429,4)),'src_span_operator'('no_loc_info_available','src_span'(119,30,119,33,3425,3))),'src_span'(119,13,119,24,3408,11)),'closure'(['in','out','ok','ref']),'src_span_operator'('no_loc_info_available','src_span'(119,40,119,41,3435,1))),'src_span'(118,1,119,58,3338,115)).
47		'assertModelCheckExt'('False','agent_call_curry'('LAbs',[['val_of'('H','src_span'(123,14,123,15,3495,1))],['val_of'('System3','src_span'(123,17,123,24,3498,7))]]),'Deterministic','F').
48		'assertRef'('False','agent_call'('src_span'(127,8,127,10,3580,2),'BN',['int'(3),'listExp'('rangeEnum'([])),'dotTuple'(['send','hugh']),'dotTuple'(['rec','henry'])]),'Trace','agent_call_curry'('LAbs',[['val_of'('L','src_span'(127,46,127,47,3618,1))],['val_of'('System3','src_span'(127,49,127,56,3621,7))]]),'src_span'(127,1,127,57,3573,56)).
49		'assertRef'('False','agent_call'('src_span'(131,8,131,10,3673,2),'BN',['int'(3),'listExp'('rangeEnum'([])),'dotTuple'(['send','lois']),'dotTuple'(['rec','leah'])]),'Failure','agent_call_curry'('LAbs',[['val_of'('H','src_span'(131,45,131,46,3710,1))],['val_of'('System3','src_span'(131,48,131,55,3713,7))]]),'src_span'(131,1,131,56,3666,55)).
50		'bindval'('SendL4','prefix'('src_span'(143,10,143,19,4178,9),['in'(_x81)],'dotTuple'(['send','lois']),'prefix'('src_span'(143,25,143,37,4193,12),['out'(_x81)],'dotTuple'(['in','lois','leah']),'prefix'('src_span'(143,43,143,51,4211,8),['in'(_x82)],'dotTuple'(['out','lois']),'val_of'('SendL4','src_span'(143,57,143,63,4225,6)),'src_span'(143,54,143,56,4221,12)),'src_span'(143,40,143,42,4207,26)),'src_span'(143,22,143,24,4189,44)),'src_span'(143,1,143,63,4169,62)).
51		'bindval'('SendH4','prefix'('src_span'(145,10,145,19,4242,9),['in'(_x83)],'dotTuple'(['send','hugh']),'prefix'('src_span'(145,25,145,38,4257,13),['out'(_x83)],'dotTuple'(['in','hugh','henry']),'prefix'('src_span'(145,44,145,52,4276,8),['in'(_x84)],'dotTuple'(['out','hugh']),'val_of'('SendH4','src_span'(145,58,145,64,4290,6)),'src_span'(145,55,145,57,4286,12)),'src_span'(145,41,145,43,4272,26)),'src_span'(145,22,145,24,4253,45)),'src_span'(145,1,145,64,4233,63)).
52		'bindval'('RecL4','prefix'('src_span'(147,9,147,17,4306,8),['in'(_x85)],'dotTuple'(['out','leah']),'prefix'('src_span'(147,23,147,31,4320,8),['out'(_x85)],'dotTuple'(['rec','leah']),'prefix'('src_span'(147,37,147,54,4334,17),[],'dotTuple'(['in','leah','lois','Zero']),'val_of'('RecL4','src_span'(147,58,147,63,4355,5)),'src_span'(147,55,147,57,4351,26)),'src_span'(147,34,147,36,4330,32)),'src_span'(147,20,147,22,4316,46)),'src_span'(147,1,147,63,4298,62)).
53		'bindval'('RecH4','prefix'('src_span'(149,9,149,18,4370,9),['in'(_x86)],'dotTuple'(['out','henry']),'prefix'('src_span'(149,24,149,33,4385,9),['out'(_x86)],'dotTuple'(['rec','henry']),'prefix'('src_span'(149,39,149,57,4400,18),[],'dotTuple'(['in','henry','hugh','Zero']),'val_of'('RecH4','src_span'(149,61,149,66,4422,5)),'src_span'(149,58,149,60,4418,27)),'src_span'(149,36,149,38,4396,33)),'src_span'(149,21,149,23,4381,48)),'src_span'(149,1,149,66,4362,65)).
54		'bindval'('System4','\x5c\'('sharing'('closure'(['in','out']),'|||'('|||'('|||'('val_of'('SendL4','src_span'(152,13,152,19,4442,6)),'val_of'('SendH4','src_span'(152,24,152,30,4453,6)),'src_span_operator'('no_loc_info_available','src_span'(152,20,152,23,4449,3))),'val_of'('RecL4','src_span'(152,35,152,40,4464,5)),'src_span_operator'('no_loc_info_available','src_span'(152,31,152,34,4460,3))),'val_of'('RecH4','src_span'(152,45,152,50,4474,5)),'src_span_operator'('no_loc_info_available','src_span'(152,41,152,44,4470,3))),'val_of'('Medium','src_span'(153,29,153,35,4510,6)),'src_span'(153,14,153,28,4495,14)),'closure'(['in','out']),'src_span_operator'('no_loc_info_available','src_span'(153,36,153,37,4517,1))),'src_span'(152,1,153,47,4430,98)).
55		'assertModelCheckExt'('False','agent_call_curry'('LAbs',[['val_of'('H','src_span'(158,13,158,14,4571,1))],['val_of'('System4','src_span'(158,16,158,23,4574,7))]]),'Deterministic','F').
56		'assertRef'('False','agent_call'('src_span'(162,8,162,10,4654,2),'BN',['int'(1),'listExp'('rangeEnum'([])),'dotTuple'(['send','hugh']),'dotTuple'(['rec','henry'])]),'Failure','agent_call_curry'('LAbs',[['val_of'('L','src_span'(162,46,162,47,4692,1))],['val_of'('System4','src_span'(162,49,162,56,4695,7))]]),'src_span'(162,1,162,57,4647,56)).
57		'assertRef'('False','agent_call'('src_span'(163,8,163,10,4711,2),'BN',['int'(1),'listExp'('rangeEnum'([])),'dotTuple'(['send','lois']),'dotTuple'(['rec','leah'])]),'Failure','agent_call_curry'('LAbs',[['val_of'('H','src_span'(163,45,163,46,4748,1))],['val_of'('System4','src_span'(163,48,163,55,4751,7))]]),'src_span'(163,1,163,56,4704,55)).
58		'assertModelCheckExt'('False','sharing'('val_of'('H','src_span'(181,17,181,18,5360,1)),'val_of'('System4','src_span'(181,8,181,15,5351,7)),'stop'('src_span'(181,20,181,24,5363,4)),'src_span'(181,15,181,20,5358,5)),'Deterministic','FD').
59		'assertRef'('False','sharing'('val_of'('H','src_span'(182,17,182,18,5406,1)),'val_of'('System4','src_span'(182,8,182,15,5397,7)),'stop'('src_span'(182,20,182,24,5409,4)),'src_span'(182,15,182,20,5404,5)),'Failure','agent_call_curry'('LAbs',[['val_of'('H','src_span'(182,34,182,35,5423,1))],['val_of'('System4','src_span'(182,37,182,44,5426,7))]]),'src_span'(182,1,182,45,5390,44)).
60		'comment'('lineComment'('-- commsec.csp'),'src_position'(1,1,0,14)).
61		'comment'('lineComment'('-- illustrating the use of abstraction and determinism for checking'),'src_position'(3,1,16,67)).
62		'comment'('lineComment'('-- information-flow security properties'),'src_position'(4,1,84,39)).
63		'comment'('lineComment'('-- This file is only slightly adapted from the TCS version, so in particular'),'src_position'(6,1,125,76)).
64		'comment'('lineComment'('-- goes more deeply into this example than Section 6.5 of UCS.'),'src_position'(7,1,202,62)).
65		'comment'('lineComment'('-- See Example 12.4.1 in TCS'),'src_position'(8,1,265,28)).
66		'comment'('lineComment'('-- Bill Roscoe'),'src_position'(10,1,295,14)).
67		'comment'('lineComment'('-- We have two low-clearance, and two high-clearance, users'),'src_position'(12,1,311,59)).
68		'comment'('lineComment'('-- who send each other messages (a data type of size 2 being enough'),'src_position'(16,1,417,67)).
69		'comment'('lineComment'('-- by the arguments in chapter 17 on data independence)'),'src_position'(17,1,485,55)).
70		'comment'('lineComment'('-- In this example Hugh always sends messages to Henry, and Lois to Leah,'),'src_position'(21,1,570,73)).
71		'comment'('lineComment'('-- so we only need one name field on the messages transacted with the users'),'src_position'(22,1,644,75)).
72		'comment'('lineComment'('-- (the name identifies who is communicating, the other party being implicit)'),'src_position'(23,1,720,77)).
73		'comment'('lineComment'('-- The input to the communication medium carries sender and address fields'),'src_position'(27,1,830,74)).
74		'comment'('lineComment'('-- The sets of high and low level actions'),'src_position'(33,1,961,41)).
75		'comment'('lineComment'('---*--*--*--*--*--*--*--*--*--*--*--*--*--*--*--*--*--*--*--*--*--*--*--*--*-'),'src_position'(39,1,1090,77)).
76		'comment'('lineComment'('-- Version 1'),'src_position'(41,1,1169,12)).
77		'comment'('lineComment'('-- A naive version in which the two channels share a common medium:'),'src_position'(43,1,1183,67)).
78		'comment'('lineComment'('-- Lazy abstraction (defined over the stable failures model)'),'src_position'(58,1,1574,60)).
79		'comment'('lineComment'('-- The insecurity of this version is demonstrated by the check'),'src_position'(62,1,1669,62)).
80		'comment'('lineComment'('--=#==#==#==#==#==#==#==#==#==#==#==#==#==#==#==#==#==#==#==#==#==#==#==#==#='),'src_position'(66,1,1783,77)).
81		'comment'('lineComment'('-- Version 2'),'src_position'(68,1,1862,12)).
82		'comment'('lineComment'('-- Security is attained in this version at the expense of throwing away'),'src_position'(70,1,1876,71)).
83		'comment'('lineComment'('-- messages between Hugh and Henry:'),'src_position'(71,1,1948,35)).
84		'comment'('lineComment'('-- security is demonstrated by the check'),'src_position'(82,1,2265,40)).
85		'comment'('lineComment'('-- but the inadequacy of this implementation to high-level users is'),'src_position'(86,1,2353,67)).
86		'comment'('lineComment'('-- demonstrated by the check'),'src_position'(87,1,2421,28)).
87		'comment'('lineComment'('-- showing that the high view loses messages (note this is only a trace'),'src_position'(94,1,2646,71)).
88		'comment'('lineComment'('-- check) even though the low-level view is highly reliable'),'src_position'(95,1,2718,59)).
89		'comment'('lineComment'('--/%//%//%//%//%//%//%//%//%//%//%//%//%//%//%//%//%//%//%//%//%//%//%//%//%/'),'src_position'(99,1,2837,77)).
90		'comment'('lineComment'('-- Version 3:'),'src_position'(101,1,2916,13)).
91		'comment'('lineComment'('-- This version makes the process SendH re-send lost messages:'),'src_position'(103,1,2931,62)).
92		'comment'('lineComment'('-- This retains security:'),'src_position'(121,1,3455,25)).
93		'comment'('lineComment'('-- while improving the high-level utility:'),'src_position'(125,1,3529,42)).
94		'comment'('lineComment'('-- without changing the low view'),'src_position'(129,1,3632,32)).
95		'comment'('lineComment'('--/^\x5c\/^\x5c\/^\x5c\/^\x5c\/^\x5c\/^\x5c\/^\x5c\/^\x5c\/^\x5c\/^\x5c\/^\x5c\/^\x5c\/^\x5c\/^\x5c\/^\x5c\/^\x5c\/^\x5c\/^\x5c\/^\x5c\/^\x5c\/^\x5c\/^\x5c\/^\x5c\/^\x5c\/^\x5c\'),'src_position'(133,1,3724,77)).
96		'comment'('lineComment'('-- Even in version 3 the high users can be blocked by the low ones:'),'src_position'(135,1,3803,67)).
97		'comment'('lineComment'('-- the process LAbs(L)(System3) is nondeterministic'),'src_position'(136,1,3871,51)).
98		'comment'('lineComment'('-- This can be avoided by using more flow control, implemented here as'),'src_position'(138,1,3924,70)).
99		'comment'('lineComment'('-- back-messages from Henry\x27\s process to Hugh\x27\s, and from Leah\x27\s to'),'src_position'(139,1,3995,67)).
100		'comment'('lineComment'('-- Lois\x27\s. The content of these back messages are irrelevant; they are'),'src_position'(140,1,4063,71)).
101		'comment'('lineComment'('-- just acknowledgement packets.'),'src_position'(141,1,4135,32)).
102		'comment'('lineComment'('-- Not only is this secure'),'src_position'(156,1,4531,26)).
103		'comment'('lineComment'('-- But both views are now deterministic:'),'src_position'(160,1,4605,40)).
104		'comment'('lineComment'('--!*!!*!!*!!*!!*!!*!!*!!*!!*!!*!!*!!*!!*!!*!!*!!*!!*!!*!!*!!*!!*!!*!!*!!*!!*!'),'src_position'(165,1,4761,77)).
105		'comment'('lineComment'('-- PLEASE NOTE'),'src_position'(167,1,4840,14)).
106		'comment'('lineComment'('-- Many of the above checks are based (for reasons discussed in the'),'src_position'(169,1,4856,67)).
107		'comment'('lineComment'('-- text) on failures determinism checking of processes which can actually'),'src_position'(170,1,4924,73)).
108		'comment'('lineComment'('-- diverge in the representations given in this file. With such checks,'),'src_position'(171,1,4998,72)).
109		'comment'('lineComment'('-- at the time of writing, it is possible that no answer will be found by FDR.'),'src_position'(172,1,5071,78)).
110		'comment'('lineComment'('-- See Section 8.7 for a discussion of this. One way around this is to'),'src_position'(173,1,5150,71)).
111		'comment'('lineComment'('-- perform the pair of checks:'),'src_position'(174,1,5222,30)).
112		'comment'('lineComment'('-- assert P[|H|]STOP :[deterministic [FD]]'),'src_position'(176,1,5254,42)).
113		'comment'('lineComment'('-- assert P[|H|]STOP [F= LAbs(H)(P)'),'src_position'(177,1,5297,35)).
114		'comment'('lineComment'('-- as in'),'src_position'(179,1,5334,8)).
115		'symbol'('names','names','src_span'(14,10,14,15,381,5),'Datatype').
116		'symbol'('lois','lois','src_span'(14,18,14,22,389,4),'Constructor of Datatype').
117		'symbol'('leah','leah','src_span'(14,25,14,29,396,4),'Constructor of Datatype').
118		'symbol'('hugh','hugh','src_span'(14,32,14,36,403,4),'Constructor of Datatype').
119		'symbol'('henry','henry','src_span'(14,39,14,44,410,5),'Constructor of Datatype').
120		'symbol'('data','data','src_span'(19,10,19,14,551,4),'Datatype').
121		'symbol'('Zero','Zero','src_span'(19,17,19,21,558,4),'Constructor of Datatype').
122		'symbol'('One','One','src_span'(19,24,19,27,565,3),'Constructor of Datatype').
123		'symbol'('send','send','src_span'(25,9,25,13,807,4),'Channel').
124		'symbol'('rec','rec','src_span'(25,15,25,18,813,3),'Channel').
125		'symbol'('in','in','src_span'(29,9,29,11,914,2),'Channel').
126		'symbol'('out','out','src_span'(31,9,31,12,944,3),'Channel').
127		'symbol'('H','H','src_span'(35,1,35,2,1004,1),'Ident (Groundrep.)').
128		'symbol'('n','n','src_span'(35,23,35,24,1026,1),'Ident (Prolog Variable)').
129		'symbol'('L','L','src_span'(37,1,37,2,1048,1),'Ident (Groundrep.)').
130		'symbol'('n2','n','src_span'(37,22,37,23,1069,1),'Ident (Prolog Variable)').
131		'symbol'('SendL','SendL','src_span'(45,1,45,6,1252,5),'Ident (Groundrep.)').
132		'symbol'('x','x','src_span'(45,19,45,20,1270,1),'Ident (Prolog Variable)').
133		'symbol'('SendH','SendH','src_span'(47,1,47,6,1300,5),'Ident (Groundrep.)').
134		'symbol'('x2','x','src_span'(47,19,47,20,1318,1),'Ident (Prolog Variable)').
135		'symbol'('RecL','RecL','src_span'(49,1,49,5,1349,4),'Ident (Groundrep.)').
136		'symbol'('x3','x','src_span'(49,17,49,18,1365,1),'Ident (Prolog Variable)').
137		'symbol'('RecH','RecH','src_span'(51,1,51,5,1390,4),'Ident (Groundrep.)').
138		'symbol'('x4','x','src_span'(51,18,51,19,1407,1),'Ident (Prolog Variable)').
139		'symbol'('Medium','Medium','src_span'(53,1,53,7,1433,6),'Ident (Groundrep.)').
140		'symbol'('s','s','src_span'(53,13,53,14,1445,1),'Ident (Prolog Variable)').
141		'symbol'('t','t','src_span'(53,15,53,16,1447,1),'Ident (Prolog Variable)').
142		'symbol'('x5','x','src_span'(53,17,53,18,1449,1),'Ident (Prolog Variable)').
143		'symbol'('System1','System1','src_span'(55,1,55,8,1473,7),'Ident (Groundrep.)').
144		'symbol'('LAbs','LAbs','src_span'(60,1,60,5,1636,4),'Funktion or Process').
145		'symbol'('h','h','src_span'(60,6,60,7,1641,1),'Ident (Prolog Variable)').
146		'symbol'('P','P','src_span'(60,9,60,10,1644,1),'Ident (Prolog Variable)').
147		'symbol'('Medium2','Medium2','src_span'(73,1,73,8,1985,7),'Ident (Groundrep.)').
148		'symbol'('t2','t','src_span'(73,19,73,20,2003,1),'Ident (Prolog Variable)').
149		'symbol'('x6','x','src_span'(73,21,73,22,2005,1),'Ident (Prolog Variable)').
150		'symbol'('t3','t','src_span'(74,21,74,22,2049,1),'Ident (Prolog Variable)').
151		'symbol'('x7','x','src_span'(74,23,74,24,2051,1),'Ident (Prolog Variable)').
152		'symbol'('Medium2\x27\','Medium2\x27\','src_span'(76,1,76,9,2071,8),'Funktion or Process').
153		'symbol'('t4','t','src_span'(76,10,76,11,2080,1),'Ident (Prolog Variable)').
154		'symbol'('x8','x','src_span'(76,12,76,13,2082,1),'Ident (Prolog Variable)').
155		'symbol'('t\x27\','t\x27\','src_span'(76,25,76,27,2095,2),'Ident (Prolog Variable)').
156		'symbol'('x\x27\','x\x27\','src_span'(76,28,76,30,2098,2),'Ident (Prolog Variable)').
157		'symbol'('System2','System2','src_span'(79,1,79,8,2163,7),'Ident (Groundrep.)').
158		'symbol'('BN','BN','src_span'(89,1,89,3,2451,2),'Funktion or Process').
159		'symbol'('N','N','src_span'(89,4,89,5,2454,1),'Ident (Prolog Variable)').
160		'symbol'('s2','s','src_span'(89,6,89,7,2456,1),'Ident (Prolog Variable)').
161		'symbol'('left','left','src_span'(89,8,89,12,2458,4),'Ident (Prolog Variable)').
162		'symbol'('right','right','src_span'(89,13,89,18,2463,5),'Ident (Prolog Variable)').
163		'symbol'('x9','x','src_span'(89,34,89,35,2484,1),'Ident (Prolog Variable)').
164		'symbol'('head','head','src_span'(90,35,90,39,2546,4),'BuiltIn primitive').
165		'symbol'('tail','tail','src_span'(90,51,90,55,2562,4),'BuiltIn primitive').
166		'symbol'('ok','ok','src_span'(105,9,105,11,3003,2),'Channel').
167		'symbol'('ref','ref','src_span'(105,12,105,15,3006,3),'Channel').
168		'symbol'('SendH3','SendH3','src_span'(107,1,107,7,3011,6),'Ident (Groundrep.)').
169		'symbol'('x71','x','src_span'(107,20,107,21,3030,1),'Ident (Prolog Variable)').
170		'symbol'('SendH3\x27\','SendH3\x27\','src_span'(109,1,109,8,3066,7),'Funktion or Process').
171		'symbol'('x72','x','src_span'(109,9,109,10,3074,1),'Ident (Prolog Variable)').
172		'symbol'('Medium3','Medium3','src_span'(112,1,112,8,3146,7),'Ident (Groundrep.)').
173		'symbol'('t5','t','src_span'(112,19,112,20,3164,1),'Ident (Prolog Variable)').
174		'symbol'('x74','x','src_span'(112,21,112,22,3166,1),'Ident (Prolog Variable)').
175		'symbol'('t6','t','src_span'(113,21,113,22,3210,1),'Ident (Prolog Variable)').
176		'symbol'('x76','x','src_span'(113,23,113,24,3212,1),'Ident (Prolog Variable)').
177		'symbol'('Medium3\x27\','Medium3\x27\','src_span'(115,1,115,9,3232,8),'Funktion or Process').
178		'symbol'('t7','t','src_span'(115,10,115,11,3241,1),'Ident (Prolog Variable)').
179		'symbol'('x78','x','src_span'(115,12,115,13,3243,1),'Ident (Prolog Variable)').
180		'symbol'('t\x27\2','t\x27\','src_span'(115,25,115,27,3256,2),'Ident (Prolog Variable)').
181		'symbol'('x\x27\2','x\x27\','src_span'(115,28,115,30,3259,2),'Ident (Prolog Variable)').
182		'symbol'('System3','System3','src_span'(118,1,118,8,3338,7),'Ident (Groundrep.)').
183		'symbol'('SendL4','SendL4','src_span'(143,1,143,7,4169,6),'Ident (Groundrep.)').
184		'symbol'('x81','x','src_span'(143,20,143,21,4188,1),'Ident (Prolog Variable)').
185		'symbol'('x82','x','src_span'(143,52,143,53,4220,1),'Ident (Prolog Variable)').
186		'symbol'('SendH4','SendH4','src_span'(145,1,145,7,4233,6),'Ident (Groundrep.)').
187		'symbol'('x83','x','src_span'(145,20,145,21,4252,1),'Ident (Prolog Variable)').
188		'symbol'('x84','x','src_span'(145,53,145,54,4285,1),'Ident (Prolog Variable)').
189		'symbol'('RecL4','RecL4','src_span'(147,1,147,6,4298,5),'Ident (Groundrep.)').
190		'symbol'('x85','x','src_span'(147,18,147,19,4315,1),'Ident (Prolog Variable)').
191		'symbol'('RecH4','RecH4','src_span'(149,1,149,6,4362,5),'Ident (Groundrep.)').
192		'symbol'('x86','x','src_span'(149,19,149,20,4380,1),'Ident (Prolog Variable)').
193		'symbol'('System4','System4','src_span'(152,1,152,8,4430,7),'Ident (Groundrep.)').