| 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'(8,1,8,6,170,5)). | |
| 18 | 'bindval'('x','int'(2),'src_span'(9,1,9,6,176,5)). | |
| 19 | 'bindval'('PHILNAMES','setExp'('rangeClosed'('int'(0),'-'('val_of'('N','src_span'(10,16,10,17,197,1)),'int'(1)))),'src_span'(10,1,10,20,182,19)). | |
| 20 | 'bindval'('FORKNAMES','setExp'('rangeClosed'('int'(0),'-'('val_of'('N','src_span'(11,17,11,18,218,1)),'int'(1)))),'src_span'(11,1,11,21,202,20)). | |
| 21 | 'channel'('sits','type'('dotTupleType'(['val_of'('PHILNAMES','src_span'(13,28,13,37,251,9))]))). | |
| 22 | 'channel'('eats','type'('dotTupleType'(['val_of'('PHILNAMES','src_span'(13,28,13,37,251,9))]))). | |
| 23 | 'channel'('getsup','type'('dotTupleType'(['val_of'('PHILNAMES','src_span'(13,28,13,37,251,9))]))). | |
| 24 | 'channel'('picks','type'('dotTupleType'(['val_of'('PHILNAMES','src_span'(14,25,14,34,285,9)),'val_of'('FORKNAMES','src_span'(14,35,14,44,295,9))]))). | |
| 25 | 'channel'('putsdown','type'('dotTupleType'(['val_of'('PHILNAMES','src_span'(14,25,14,34,285,9)),'val_of'('FORKNAMES','src_span'(14,35,14,44,295,9))]))). | |
| 26 | 'agent'('PHIL'(_i),'prefix'('src_span'(19,11,19,15,434,4),['out'(_i)],'sits','prefix'('src_span'(19,21,19,26,444,5),['out'(_i),'out'(_i)],'picks','prefix'('src_span'(19,34,19,39,457,5),['out'(_i),'out'('%'('+'(_i,'int'(1)),'val_of'('N','src_span'(19,49,19,50,472,1))))],'picks','prefix'('src_span'(20,11,20,15,488,4),['out'(_i)],'eats','prefix'('src_span'(20,21,20,29,498,8),['out'(_i),'out'('%'('+'(_i,'int'(1)),'val_of'('N','src_span'(20,39,20,40,516,1))))],'putsdown','prefix'('src_span'(20,45,20,53,522,8),['out'(_i),'out'(_i)],'putsdown','prefix'('src_span'(20,61,20,67,538,6),['out'(_i)],'getsup','agent_call'('src_span'(20,73,20,77,550,4),'PHIL',[_i]),'src_span'(20,70,20,72,546,13)),'src_span'(20,58,20,60,534,25)),'src_span'(20,42,20,44,518,49)),'src_span'(20,18,20,20,494,65)),'src_span'(19,52,20,10,474,93)),'src_span'(19,31,19,33,453,106)),'src_span'(19,18,19,20,440,119)),'src_span'(19,11,20,80,434,123)). | |
| 27 | 'agent'('PHIL1'(_i2),'agent_call'('src_span'(22,12,22,16,570,4),'PHIL',[_i2]),'src_span'(22,12,22,19,570,7)). | |
| 28 | 'agent'('PHILs'(_i3),'prefix'('src_span'(27,13,27,18,726,5),['out'(_i3),'out'(_i3)],'picks','prefix'('src_span'(27,26,27,31,739,5),['out'(_i3),'out'('%'('+'(_i3,'int'(1)),'val_of'('N','src_span'(27,41,27,42,754,1))))],'picks','prefix'('src_span'(28,12,28,20,771,8),['out'(_i3),'out'('%'('+'(_i3,'int'(1)),'val_of'('N','src_span'(28,30,28,31,789,1))))],'putsdown','prefix'('src_span'(28,36,28,44,795,8),['out'(_i3),'out'(_i3)],'putsdown','agent_call'('src_span'(28,52,28,57,811,5),'PHILs',[_i3]),'src_span'(28,49,28,51,807,14)),'src_span'(28,33,28,35,791,38)),'src_span'(27,44,28,11,756,73)),'src_span'(27,23,27,25,735,86)),'src_span'(27,13,28,60,726,93)). | |
| 29 | 'agent'('AlphaP'(_i4),'setExp'('rangeEnum'(['dotTuple'(['sits',_i4]),'dotTuple'(['picks',_i4,_i4]),'dotTuple'(['picks',_i4,'%'('+'(_i4,'int'(1)),'val_of'('N','src_span'(34,45,34,46,887,1)))]),'dotTuple'(['eats',_i4]),'dotTuple'(['putsdown',_i4,_i4]),'dotTuple'(['putsdown',_i4,'%'('+'(_i4,'int'(1)),'val_of'('N','src_span'(35,31,35,32,940,1)))]),'dotTuple'(['getsup',_i4])])),'src_span'(34,13,35,42,855,96)). | |
| 30 | 'agent'('FORK'(_i5),'[]'('prefix'('src_span'(39,11,39,16,1022,5),['out'(_i5),'out'(_i5)],'picks','prefix'('src_span'(39,24,39,32,1035,8),['out'(_i5),'out'(_i5)],'putsdown','agent_call'('src_span'(39,40,39,44,1051,4),'FORK',[_i5]),'src_span'(39,37,39,39,1047,13)),'src_span'(39,21,39,23,1031,29)),'prefix'('src_span'(40,14,40,19,1072,5),['out'('%'('-'(_i5,'int'(1)),'val_of'('N','src_span'(40,27,40,28,1085,1)))),'out'(_i5)],'picks','prefix'('src_span'(40,35,40,43,1093,8),['out'('%'('-'(_i5,'int'(1)),'val_of'('N','src_span'(40,51,40,52,1109,1)))),'out'(_i5)],'putsdown','agent_call'('src_span'(40,59,40,63,1117,4),'FORK',[_i5]),'src_span'(40,56,40,58,1113,13)),'src_span'(40,32,40,34,1089,37)),'src_span_operator'('no_loc_info_available','src_span'(40,10,40,12,1068,2))),'no_loc_info_available'). | |
| 31 | 'agent'('AlphaF'(_i6),'setExp'('rangeEnum'(['dotTuple'(['picks',_i6,_i6]),'dotTuple'(['picks','%'('-'(_i6,'int'(1)),'val_of'('N','src_span'(42,37,42,38,1162,1))),_i6]),'dotTuple'(['putsdown',_i6,_i6]),'dotTuple'(['putsdown','%'('-'(_i6,'int'(1)),'val_of'('N','src_span'(42,71,42,72,1196,1))),_i6])])),'src_span'(42,13,42,75,1138,62)). | |
| 32 | 'bindval'('SYSTEM','procRepAParallel'(['comprehensionGenerator'(_i7,'val_of'('PHILNAMES','src_span'(50,15,50,24,1483,9)))],'pair'('agent_call'('src_span'(50,26,50,31,1494,5),'union',['agent_call'('src_span'(50,32,50,38,1500,6),'AlphaP',[_i7]),'agent_call'('src_span'(50,42,50,48,1510,6),'AlphaF',[_i7])]),'aParallel'('agent_call'('src_span'(51,34,51,40,1556,6),'AlphaP',[_i7]),'agent_call'('src_span'(51,25,51,30,1547,5),'PHIL1',[_i7]),'agent_call'('src_span'(51,46,51,52,1568,6),'AlphaF',[_i7]),'agent_call'('src_span'(51,57,51,61,1579,4),'FORK',[_i7]),'src_span'(51,33,51,56,1555,23))),'src_span'(50,13,50,25,1481,12)),'src_span'(50,1,51,65,1469,118)). | |
| 33 | 'bindval'('SYSTEMs','procRepAParallel'(['comprehensionGenerator'(_i8,'val_of'('PHILNAMES','src_span'(55,16,55,25,1625,9)))],'pair'('agent_call'('src_span'(55,27,55,32,1636,5),'union',['agent_call'('src_span'(55,33,55,39,1642,6),'AlphaP',[_i8]),'agent_call'('src_span'(55,43,55,49,1652,6),'AlphaF',[_i8])]),'aParallel'('agent_call'('src_span'(56,34,56,40,1698,6),'AlphaP',[_i8]),'agent_call'('src_span'(56,25,56,30,1689,5),'PHILs',[_i8]),'agent_call'('src_span'(56,46,56,52,1710,6),'AlphaF',[_i8]),'agent_call'('src_span'(56,57,56,61,1721,4),'FORK',[_i8]),'src_span'(56,33,56,56,1697,23))),'src_span'(55,14,55,26,1623,12)),'src_span'(55,1,56,65,1610,119)). | |
| 34 | 'bindval'('PHILS','repInterleave'(['comprehensionGenerator'(_i9,'val_of'('PHILNAMES','src_span'(64,15,64,24,1951,9)))],'agent_call'('src_span'(64,26,64,30,1962,4),'PHIL',[_i9]),'src_span'(64,13,64,25,1949,12)),'src_span'(64,1,64,33,1937,32)). | |
| 35 | 'bindval'('FORKS','repInterleave'(['comprehensionGenerator'(_i48,'val_of'('FORKNAMES','src_span'(65,15,65,24,1984,9)))],'agent_call'('src_span'(65,26,65,30,1995,4),'FORK',[_i48]),'src_span'(65,13,65,25,1982,12)),'src_span'(65,1,65,33,1970,32)). | |
| 36 | 'bindval'('SYSTEM\x27\','sharing'('closure'(['picks','putsdown']),'val_of'('PHILS','src_span'(67,11,67,16,2014,5)),'val_of'('FORKS','src_span'(67,39,67,44,2042,5)),'src_span'(67,16,67,39,2019,23)),'src_span'(67,1,67,44,2004,43)). | |
| 37 | 'assertModelCheckExt'('False','val_of'('SYSTEM','src_span'(71,8,71,14,2106,6)),'DeadlockFree','F'). | |
| 38 | 'assertModelCheckExt'('False','val_of'('SYSTEMs','src_span'(74,8,74,15,2182,7)),'DeadlockFree','F'). | |
| 39 | 'agent'('BUTLER'(_j),'[]'('&'('>'(_j,'int'(0)),'prefix'('src_span'(83,19,83,25,2515,6),['in'(_i50)],'getsup','agent_call'('src_span'(83,31,83,37,2527,6),'BUTLER',['-'(_j,'int'(1))]),'src_span'(83,28,83,30,2523,17))),'&'('<'(_j,'-'('val_of'('N','src_span'(84,17,84,18,2555,1)),'int'(1))),'prefix'('src_span'(84,23,84,27,2561,4),['in'(_i51)],'sits','agent_call'('src_span'(84,33,84,39,2571,6),'BUTLER',['+'(_j,'int'(1))]),'src_span'(84,30,84,32,2567,17))),'src_span_operator'('no_loc_info_available','src_span'(84,13,84,15,2551,2))),'no_loc_info_available'). | |
| 40 | 'bindval'('BSYSTEM','sharing'('closure'(['sits','getsup']),'val_of'('SYSTEM','src_span'(86,11,86,17,2594,6)),'agent_call'('src_span'(86,39,86,45,2622,6),'BUTLER',['int'(0)]),'src_span'(86,18,86,38,2601,20)),'src_span'(86,1,86,48,2584,47)). | |
| 41 | 'bindval'('MAIN','val_of'('BSYSTEM','src_span'(88,8,88,15,2640,7)),'src_span'(88,1,88,15,2633,14)). | |
| 42 | 'assertModelCheckExt'('False','val_of'('BSYSTEM','src_span'(90,8,90,15,2656,7)),'DeadlockFree','F'). | |
| 43 | 'agent'('LPHIL'(_i52),'prefix'('src_span'(98,11,98,17,2942,6),[],'dotTuple'(['sits',_i52]),'prefix'('src_span'(98,21,98,38,2952,17),[],'dotTuple'(['picks',_i52,'%'('+'(_i52,'int'(1)),'val_of'('N','src_span'(98,36,98,37,2967,1)))]),'prefix'('src_span'(98,42,98,51,2973,9),[],'dotTuple'(['picks',_i52,_i52]),'prefix'('src_span'(99,11,99,17,2997,6),[],'dotTuple'(['eats',_i52]),'prefix'('src_span'(99,21,99,41,3007,20),[],'dotTuple'(['putsdown',_i52,'%'('+'(_i52,'int'(1)),'val_of'('N','src_span'(99,39,99,40,3025,1)))]),'prefix'('src_span'(99,45,99,57,3031,12),[],'dotTuple'(['putsdown',_i52,_i52]),'prefix'('src_span'(99,61,99,69,3047,8),[],'dotTuple'(['getsup',_i52]),'agent_call'('src_span'(99,73,99,78,3059,5),'LPHIL',[_i52]),'src_span'(99,70,99,72,3055,20)),'src_span'(99,58,99,60,3043,36)),'src_span'(99,42,99,44,3027,60)),'src_span'(99,18,99,20,3003,70)),'src_span'(98,52,99,10,2982,94)),'src_span'(98,39,98,41,2969,115)),'src_span'(98,18,98,20,2948,125)),'src_span'(98,11,99,81,2942,125)). | |
| 44 | 'bindval'('ASPHILS','repInterleave'(['comprehensionGenerator'(_i53,'val_of'('PHILNAMES','src_span'(101,17,101,26,3085,9)))],'ifte'('=='(_i53,'int'(0)),'agent_call'('src_span'(101,42,101,47,3110,5),'LPHIL',[_i53]),'agent_call'('src_span'(101,56,101,60,3124,4),'PHIL',[_i53]),'no_loc_info_available','no_loc_info_available','src_span'(101,51,101,55,3118,21)),'src_span'(101,15,101,28,3083,13)),'src_span'(101,1,101,63,3069,62)). | |
| 45 | 'bindval'('ASSYSTEM','sharing'('closure'(['picks','putsdown']),'val_of'('ASPHILS','src_span'(103,12,103,19,3144,7)),'val_of'('FORKS','src_span'(103,42,103,47,3174,5)),'src_span'(103,19,103,42,3151,23)),'src_span'(103,1,103,47,3133,46)). | |
| 46 | 'assertModelCheckExt'('False','val_of'('ASSYSTEM','src_span'(107,8,107,16,3265,8)),'DeadlockFree','F'). | |
| 47 | 'agent'('LPHILs'(_i54),'prefix'('src_span'(112,13,112,30,3493,17),[],'dotTuple'(['picks',_i54,'%'('+'(_i54,'int'(1)),'val_of'('N','src_span'(112,28,112,29,3508,1)))]),'prefix'('src_span'(112,34,112,43,3514,9),[],'dotTuple'(['picks',_i54,_i54]),'prefix'('src_span'(113,12,113,32,3539,20),[],'dotTuple'(['putsdown',_i54,'%'('+'(_i54,'int'(1)),'val_of'('N','src_span'(113,30,113,31,3557,1)))]),'prefix'('src_span'(113,36,113,48,3563,12),[],'dotTuple'(['putsdown',_i54,_i54]),'agent_call'('src_span'(113,52,113,58,3579,6),'LPHILs',[_i54]),'src_span'(113,49,113,51,3575,25)),'src_span'(113,33,113,35,3559,49)),'src_span'(112,44,113,11,3523,74)),'src_span'(112,31,112,33,3510,95)),'src_span'(112,13,113,61,3493,95)). | |
| 48 | 'bindval'('ASPHILSs','repInterleave'(['comprehensionGenerator'(_i55,'val_of'('PHILNAMES','src_span'(115,18,115,27,3607,9)))],'ifte'('=='(_i55,'int'(0)),'agent_call'('src_span'(115,43,115,49,3632,6),'LPHILs',[_i55]),'agent_call'('src_span'(115,58,115,63,3647,5),'PHILs',[_i55]),'no_loc_info_available','no_loc_info_available','src_span'(115,53,115,57,3641,23)),'src_span'(115,16,115,29,3605,13)),'src_span'(115,1,115,66,3590,65)). | |
| 49 | 'bindval'('ASSYSTEMs','sharing'('closure'(['picks','putsdown']),'val_of'('ASPHILSs','src_span'(117,13,117,21,3669,8)),'val_of'('FORKS','src_span'(117,44,117,49,3700,5)),'src_span'(117,21,117,44,3677,23)),'src_span'(117,1,117,49,3657,48)). | |
| 50 | 'assertModelCheckExt'('False','val_of'('ASSYSTEMs','src_span'(119,8,119,17,3714,9)),'DeadlockFree','F'). | |
| 51 | 'pragma'(' assert_ltl "SF(picks.0.1) => G ([picks.0.0] => F [eats.0])" "No starvation for philosopher 0" '). | |
| 52 | 'pragma'(' assert_ltl "SF(sits.0) => G ([picks.1.1] => F [eats.1])" '). | |
| 53 | 'pragma'(' assert_ltl "SF(sits.0) => G ([picks.1.0] => F [eats.1])" '). | |
| 54 | 'pragma'(' assert_ltl "SF(sits.1) => G ([picks.0.1] => F [eats.0])" '). | |
| 55 | 'pragma'(' assert_ltl "(GF e(sits.0) => GF [sits.0]) => G ([picks.1.1] => F [eats.1])" '). | |
| 56 | 'pragma'(' assert_ltl "(GF e(sits.0) => GF [sits.0]) => G ([picks.1.0] => F [eats.1])" '). | |
| 57 | 'pragma'(' assert_ltl "SF(picks.0.1) & SF(picks.0.0) => G ([sits.0] => F [eats.0])" '). | |
| 58 | 'pragma'(' assert_ltl "SF(picks.0._) => G ([sits.0] => F [eats.0])" '). | |
| 59 | 'comment'('lineComment'('-- The five dining philosophers for FDR'),'src_position'(1,1,0,39)). | |
| 60 | 'comment'('lineComment'('-- Bill Roscoe'),'src_position'(3,1,41,14)). | |
| 61 | 'comment'('lineComment'('-- The most standard example of them all. We can determine how many'),'src_position'(5,1,57,68)). | |
| 62 | 'comment'('lineComment'('-- (with the conventional number being 5):'),'src_position'(6,1,126,42)). | |
| 63 | 'comment'('lineComment'('-- A philosopher thinks, sits down, picks up two forks, eats, puts down forks'),'src_position'(16,1,306,77)). | |
| 64 | 'comment'('lineComment'('-- and gets up, in an unending cycle.\x9\'),'src_position'(17,1,384,38)). | |
| 65 | 'comment'('lineComment'('-- Of course the only events relevant to deadlock are the picks and putsdown'),'src_position'(24,1,579,76)). | |
| 66 | 'comment'('lineComment'('-- ones. Try the alternative "stripped down" definition'),'src_position'(25,1,656,56)). | |
| 67 | 'comment'('lineComment'('-- Its alphabet is'),'src_position'(32,1,823,18)). | |
| 68 | 'comment'('lineComment'('-- A fork can only be picked up by one neighbour at once!'),'src_position'(37,1,953,57)). | |
| 69 | 'comment'('lineComment'('-- We can build the system up in several ways, but certainly'),'src_position'(44,1,1202,60)). | |
| 70 | 'comment'('lineComment'('-- have to use some form of parallel that allows us to'),'src_position'(45,1,1263,54)). | |
| 71 | 'comment'('lineComment'('-- build a network parameterized by N. The following uses'),'src_position'(46,1,1318,58)). | |
| 72 | 'comment'('lineComment'('-- a composition of N philosopher/fork pairs, each individually'),'src_position'(47,1,1377,63)). | |
| 73 | 'comment'('lineComment'('-- a parallel composition.'),'src_position'(48,1,1441,26)). | |
| 74 | 'comment'('lineComment'('-- or stripped down'),'src_position'(53,1,1589,19)). | |
| 75 | 'comment'('lineComment'('-- As an alternative (see Section 2.3) we can create separate'),'src_position'(59,1,1732,61)). | |
| 76 | 'comment'('lineComment'('-- collections of the philosophers and forks, each composed'),'src_position'(60,1,1794,59)). | |
| 77 | 'comment'('lineComment'('-- using interleaving ||| since there is no communication inside'),'src_position'(61,1,1854,64)). | |
| 78 | 'comment'('lineComment'('-- these groups.'),'src_position'(62,1,1919,16)). | |
| 79 | 'comment'('lineComment'('-- The potential for deadlock is illustrated by '),'src_position'(69,1,2049,48)). | |
| 80 | 'comment'('lineComment'('-- or equivalently in the stripped down'),'src_position'(73,1,2135,39)). | |
| 81 | 'comment'('lineComment'('-- which will find the same deadlock a lot faster.'),'src_position'(76,1,2212,50)). | |
| 82 | 'comment'('lineComment'('-- There are several well-known solutions to the problem. One involves a'),'src_position'(78,1,2264,73)). | |
| 83 | 'comment'('lineComment'('-- butler who must co-operate on the sitting down and getting up events,'),'src_position'(79,1,2338,72)). | |
| 84 | 'comment'('lineComment'('-- and always ensures that no more than four of the five'),'src_position'(80,1,2411,56)). | |
| 85 | 'comment'('lineComment'('-- philosophers are seated.'),'src_position'(81,1,2468,27)). | |
| 86 | 'comment'('lineComment'('-- We would have to reduce the amount of stripping down for this,'),'src_position'(92,1,2686,65)). | |
| 87 | 'comment'('lineComment'('-- since it makes the sits and getsup events useful...try this.'),'src_position'(93,1,2752,63)). | |
| 88 | 'comment'('lineComment'('-- A second solution involves replacing one of the above right-handed (say)'),'src_position'(95,1,2817,75)). | |
| 89 | 'comment'('lineComment'('-- philosophers by a left-handed one:'),'src_position'(96,1,2893,37)). | |
| 90 | 'comment'('lineComment'('-- This asymmetric system is deadlock free, as can be proved using Check. '),'src_position'(105,1,3181,75)). | |
| 91 | 'comment'('lineComment'('-- If you want to run a lot of dining philosophers, the best results will'),'src_position'(109,1,3296,73)). | |
| 92 | 'comment'('lineComment'('-- probably be obtained by removing the events irrelevant to ASSYSTEM'),'src_position'(110,1,3370,69)). | |
| 93 | 'comment'('lineComment'('-- (leaving only picks and putsdown) in:'),'src_position'(111,1,3440,40)). | |
| 94 | 'comment'('lineComment'('-- Setting N=10 will show the spectacular difference in running the'),'src_position'(121,1,3746,67)). | |
| 95 | 'comment'('lineComment'('-- stripped down version. Try to undertand why there is such an'),'src_position'(122,1,3814,64)). | |
| 96 | 'comment'('lineComment'('-- enormous difference.'),'src_position'(123,1,3879,23)). | |
| 97 | 'comment'('lineComment'('-- Compare the stripped down versions with the idea of "Leaf Compression"'),'src_position'(125,1,3904,73)). | |
| 98 | 'comment'('lineComment'('-- discussed in Chapter 8.'),'src_position'(126,1,3978,26)). | |
| 99 | 'comment'('pragmaComment'('{-# assert_ltl "SF(picks.0.1) => G ([picks.0.0] => F [eats.0])" "No starvation for philosopher 0" #-}'),'src_position'(128,1,4006,101)). | |
| 100 | 'comment'('pragmaComment'('{-# assert_ltl "SF(sits.0) => G ([picks.1.1] => F [eats.1])" #-}'),'src_position'(129,1,4108,64)). | |
| 101 | 'comment'('pragmaComment'('{-# assert_ltl "SF(sits.0) => G ([picks.1.0] => F [eats.1])" #-}'),'src_position'(130,1,4173,64)). | |
| 102 | 'comment'('pragmaComment'('{-# assert_ltl "SF(sits.1) => G ([picks.0.1] => F [eats.0])" #-}'),'src_position'(131,1,4238,64)). | |
| 103 | 'comment'('pragmaComment'('{-# assert_ltl "(GF e(sits.0) => GF [sits.0]) => G ([picks.1.1] => F [eats.1])" #-}'),'src_position'(132,1,4303,83)). | |
| 104 | 'comment'('pragmaComment'('{-# assert_ltl "(GF e(sits.0) => GF [sits.0]) => G ([picks.1.0] => F [eats.1])" #-}'),'src_position'(133,1,4387,83)). | |
| 105 | 'comment'('pragmaComment'('{-# assert_ltl "SF(picks.0.1) & SF(picks.0.0) => G ([sits.0] => F [eats.0])" #-}'),'src_position'(134,1,4471,80)). | |
| 106 | 'comment'('pragmaComment'('{-# assert_ltl "SF(picks.0._) => G ([sits.0] => F [eats.0])" #-}'),'src_position'(135,1,4552,64)). | |
| 107 | 'symbol'('N','N','src_span'(8,1,8,2,170,1),'Ident (Groundrep.)'). | |
| 108 | 'symbol'('x','x','src_span'(9,1,9,2,176,1),'Ident (Groundrep.)'). | |
| 109 | 'symbol'('PHILNAMES','PHILNAMES','src_span'(10,1,10,10,182,9),'Ident (Groundrep.)'). | |
| 110 | 'symbol'('FORKNAMES','FORKNAMES','src_span'(11,1,11,10,202,9),'Ident (Groundrep.)'). | |
| 111 | 'symbol'('sits','sits','src_span'(13,9,13,13,232,4),'Channel'). | |
| 112 | 'symbol'('eats','eats','src_span'(13,15,13,19,238,4),'Channel'). | |
| 113 | 'symbol'('getsup','getsup','src_span'(13,21,13,27,244,6),'Channel'). | |
| 114 | 'symbol'('picks','picks','src_span'(14,9,14,14,269,5),'Channel'). | |
| 115 | 'symbol'('putsdown','putsdown','src_span'(14,16,14,24,276,8),'Channel'). | |
| 116 | 'symbol'('PHIL','PHIL','src_span'(19,1,19,5,424,4),'Funktion or Process'). | |
| 117 | 'symbol'('i','i','src_span'(19,6,19,7,429,1),'Ident (Prolog Variable)'). | |
| 118 | 'symbol'('PHIL1','PHIL1','src_span'(22,1,22,6,559,5),'Funktion or Process'). | |
| 119 | 'symbol'('i2','i','src_span'(22,7,22,8,565,1),'Ident (Prolog Variable)'). | |
| 120 | 'symbol'('PHILs','PHILs','src_span'(27,1,27,6,714,5),'Funktion or Process'). | |
| 121 | 'symbol'('i3','i','src_span'(27,7,27,8,720,1),'Ident (Prolog Variable)'). | |
| 122 | 'symbol'('AlphaP','AlphaP','src_span'(34,1,34,7,843,6),'Funktion or Process'). | |
| 123 | 'symbol'('i4','i','src_span'(34,8,34,9,850,1),'Ident (Prolog Variable)'). | |
| 124 | 'symbol'('FORK','FORK','src_span'(39,1,39,5,1012,4),'Funktion or Process'). | |
| 125 | 'symbol'('i5','i','src_span'(39,6,39,7,1017,1),'Ident (Prolog Variable)'). | |
| 126 | 'symbol'('AlphaF','AlphaF','src_span'(42,1,42,7,1126,6),'Funktion or Process'). | |
| 127 | 'symbol'('i6','i','src_span'(42,8,42,9,1133,1),'Ident (Prolog Variable)'). | |
| 128 | 'symbol'('SYSTEM','SYSTEM','src_span'(50,1,50,7,1469,6),'Ident (Groundrep.)'). | |
| 129 | 'symbol'('i7','i','src_span'(50,13,50,14,1481,1),'Ident (Prolog Variable)'). | |
| 130 | 'symbol'('union','union','src_span'(50,26,50,31,1494,5),'BuiltIn primitive'). | |
| 131 | 'symbol'('SYSTEMs','SYSTEMs','src_span'(55,1,55,8,1610,7),'Ident (Groundrep.)'). | |
| 132 | 'symbol'('i8','i','src_span'(55,14,55,15,1623,1),'Ident (Prolog Variable)'). | |
| 133 | 'symbol'('union','union','src_span'(55,27,55,32,1636,5),'BuiltIn primitive'). | |
| 134 | 'symbol'('PHILS','PHILS','src_span'(64,1,64,6,1937,5),'Ident (Groundrep.)'). | |
| 135 | 'symbol'('i9','i','src_span'(64,13,64,14,1949,1),'Ident (Prolog Variable)'). | |
| 136 | 'symbol'('FORKS','FORKS','src_span'(65,1,65,6,1970,5),'Ident (Groundrep.)'). | |
| 137 | 'symbol'('i48','i','src_span'(65,13,65,14,1982,1),'Ident (Prolog Variable)'). | |
| 138 | 'symbol'('SYSTEM\x27\','SYSTEM\x27\','src_span'(67,1,67,8,2004,7),'Ident (Groundrep.)'). | |
| 139 | 'symbol'('BUTLER','BUTLER','src_span'(83,1,83,7,2497,6),'Funktion or Process'). | |
| 140 | 'symbol'('j','j','src_span'(83,8,83,9,2504,1),'Ident (Prolog Variable)'). | |
| 141 | 'symbol'('i50','i','src_span'(83,26,83,27,2522,1),'Ident (Prolog Variable)'). | |
| 142 | 'symbol'('i51','i','src_span'(84,28,84,29,2566,1),'Ident (Prolog Variable)'). | |
| 143 | 'symbol'('BSYSTEM','BSYSTEM','src_span'(86,1,86,8,2584,7),'Ident (Groundrep.)'). | |
| 144 | 'symbol'('MAIN','MAIN','src_span'(88,1,88,5,2633,4),'Ident (Groundrep.)'). | |
| 145 | 'symbol'('LPHIL','LPHIL','src_span'(98,1,98,6,2932,5),'Funktion or Process'). | |
| 146 | 'symbol'('i52','i','src_span'(98,7,98,8,2938,1),'Ident (Prolog Variable)'). | |
| 147 | 'symbol'('ASPHILS','ASPHILS','src_span'(101,1,101,8,3069,7),'Ident (Groundrep.)'). | |
| 148 | 'symbol'('i53','i','src_span'(101,15,101,16,3083,1),'Ident (Prolog Variable)'). | |
| 149 | 'symbol'('ASSYSTEM','ASSYSTEM','src_span'(103,1,103,9,3133,8),'Ident (Groundrep.)'). | |
| 150 | 'symbol'('LPHILs','LPHILs','src_span'(112,1,112,7,3481,6),'Funktion or Process'). | |
| 151 | 'symbol'('i54','i','src_span'(112,8,112,9,3488,1),'Ident (Prolog Variable)'). | |
| 152 | 'symbol'('ASPHILSs','ASPHILSs','src_span'(115,1,115,9,3590,8),'Ident (Groundrep.)'). | |
| 153 | 'symbol'('i55','i','src_span'(115,16,115,17,3605,1),'Ident (Prolog Variable)'). | |
| 154 | 'symbol'('ASSYSTEMs','ASSYSTEMs','src_span'(117,1,117,10,3657,9),'Ident (Groundrep.)'). |