| 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'('BSet',['constructor'('phils')]). | |
| 18 | 'dataTypeDef'('BPhils',['constructor'('p1'),'constructor'('p2'),'constructor'('p3')]). | |
| 19 | 'agent'('B'('phils'),'BPhils','src_span'(4,12,4,18,65,6)). | |
| 20 | 'channel'('think','type'('dotTupleType'(['agent_call'('src_span'(7,61,7,62,134,1),'B',['phils'])]))). | |
| 21 | 'channel'('eat','type'('dotTupleType'(['agent_call'('src_span'(7,61,7,62,134,1),'B',['phils'])]))). | |
| 22 | 'channel'('TakeLeftFork','type'('dotTupleType'(['agent_call'('src_span'(7,61,7,62,134,1),'B',['phils'])]))). | |
| 23 | 'channel'('TakeRightFork','type'('dotTupleType'(['agent_call'('src_span'(7,61,7,62,134,1),'B',['phils'])]))). | |
| 24 | 'channel'('DropFork','type'('dotTupleType'(['agent_call'('src_span'(7,61,7,62,134,1),'B',['phils'])]))). | |
| 25 | 'bindval'('MAIN','repInterleave'(['comprehensionGenerator'(_p,'agent_call'('src_span'(10,14,10,15,158,1),'B',['phils']))],'agent_call'('src_span'(10,25,10,29,169,4),'PHIL',[_p]),'src_span'(10,12,10,24,156,12)),'src_span'(10,1,10,32,145,31)). | |
| 26 | 'agent'('PHIL'(_P),'prefix'('src_span'(12,11,12,16,188,5),['out'(_P)],'think','prefix'('src_span'(12,22,12,34,199,12),['out'(_P)],'TakeLeftFork','prefix'('src_span'(12,40,12,53,217,13),['out'(_P)],'TakeRightFork','prefix'('src_span'(13,11,13,14,246,3),['out'(_P)],'eat','prefix'('src_span'(13,20,13,28,255,8),['out'(_P)],'DropFork','prefix'('src_span'(13,34,13,42,269,8),['out'(_P)],'DropFork','agent_call'('src_span'(13,48,13,52,283,4),'PHIL',[_P]),'src_span'(13,45,13,47,279,13)),'src_span'(13,31,13,33,265,27)),'src_span'(13,17,13,19,251,41)),'src_span'(12,56,13,10,232,60)),'src_span'(12,37,12,39,213,79)),'src_span'(12,19,12,21,195,97)),'src_span'(12,11,13,55,188,102)). | |
| 27 | 'bindval'('Test2','prefix'('src_span'(16,11,16,16,325,5),['in'(_x)],'think','prefix'('src_span'(16,22,16,25,336,3),['in'(_x2)],'eat','stop'('src_span'(16,31,16,35,345,4)),'src_span'(16,28,16,30,341,10)),'src_span'(16,19,16,21,332,19)),'src_span'(16,2,16,35,316,33)). | |
| 28 | 'bindval'('Phil1','agent_call'('src_span'(17,9,17,13,358,4),'PHIL',['p1']),'src_span'(17,1,17,17,350,16)). | |
| 29 | 'bindval'('TESTC','repChoice'(['comprehensionGenerator'(_p4,'agent_call'('src_span'(19,14,19,15,381,1),'B',['phils']))],'agent_call'('src_span'(19,25,19,29,392,4),'PHIL',[_p4]),'src_span'(19,12,19,24,379,12)),'src_span'(19,1,19,32,368,31)). | |
| 30 | 'bindval'('TESTC2','repInternalChoice'(['comprehensionGenerator'(_p5,'agent_call'('src_span'(20,16,20,17,415,1),'B',['phils']))],'agent_call'('src_span'(20,27,20,31,426,4),'PHIL',[_p5]),'src_span'(20,14,20,26,413,12)),'src_span'(20,1,20,34,400,33)). | |
| 31 | 'channel'('c','type'('dotTupleType'(['setExp'('rangeClosed'('int'(1),'int'(9)))]))). | |
| 32 | 'channel'('d','type'('dotTupleType'(['setExp'('rangeClosed'('int'(1),'int'(9)))]))). | |
| 33 | 'bindval'('TestNeil','prefix'('src_span'(25,12,25,13,468,1),['in'(_x3)],'c','prefix'('src_span'(25,19,25,20,475,1),['out'('+'(_x3,'int'(1)))],'d','stop'('src_span'(25,30,25,34,486,4)),'src_span'(25,27,25,29,482,14)),'src_span'(25,16,25,18,471,21)),'src_span'(25,1,25,34,457,33)). | |
| 34 | 'assertModelCheckExt'('False','val_of'('TESTC','src_span'(31,8,31,13,595,5)),'DeadlockFree','F'). | |
| 35 | 'assertModelCheckExt'('False','val_of'('TESTC2','src_span'(32,8,32,14,631,6)),'DeadlockFree','F'). | |
| 36 | 'assertModelCheckExt'('False','val_of'('MAIN','src_span'(34,8,34,12,669,4)),'DeadlockFree','F'). | |
| 37 | 'assertModelCheck'('False','val_of'('MAIN','src_span'(35,8,35,12,704,4)),'LivelockFree'). | |
| 38 | 'assertRef'('True','val_of'('MAIN','src_span'(36,12,36,16,739,4)),'Trace','val_of'('Test2','src_span'(36,21,36,26,748,5)),'src_span'(36,1,36,26,728,25)). | |
| 39 | 'assertRef'('False','val_of'('MAIN','src_span'(37,8,37,12,761,4)),'Trace','val_of'('Phil1','src_span'(37,17,37,22,770,5)),'src_span'(37,1,37,22,754,21)). | |
| 40 | 'assertRef'('True','val_of'('MAIN','src_span'(38,12,38,16,787,4)),'Failure','val_of'('Phil1','src_span'(38,21,38,26,796,5)),'src_span'(38,1,38,26,776,25)). | |
| 41 | 'pragma'(' ASSERT_LTL_1=="Fe(think.p1)" ;\xa\ ASSERT_LTL_2=="Fe(think.p2)";\xa\ ASSERT_LTL_3=="Fe(think.p3)";\xa\ ASSERT_LTL == "G(e(DropFork.p1) => Y O [TakeLeftFork.p1])" ;\xa\ ASSERT_LTL == "G(e(DropFork.p2) => Y O [TakeLeftFork.p2])" ;\xa\ ASSERT_LTL == "G(e(DropFork.p3) => Y O [TakeLeftFork.p3])" '). | |
| 42 | 'comment'('lineComment'('--x = think!p1 -> STOP'),'src_position'(15,1,292,22)). | |
| 43 | 'comment'('lineComment'('-- HIDE_CSPB = {| eat |}'),'src_position'(27,1,492,24)). | |
| 44 | 'comment'('lineComment'('--These assertions have been added automatically by the ProB tool.--'),'src_position'(29,1,518,68)). | |
| 45 | 'comment'('lineComment'('--End of the automatically added assertions.--'),'src_position'(41,1,804,46)). | |
| 46 | 'comment'('pragmaComment'('{-# ASSERT_LTL_1=="Fe(think.p1)" ;\xa\ ASSERT_LTL_2=="Fe(think.p2)";\xa\ ASSERT_LTL_3=="Fe(think.p3)";\xa\ ASSERT_LTL == "G(e(DropFork.p1) => Y O [TakeLeftFork.p1])" ;\xa\ ASSERT_LTL == "G(e(DropFork.p2) => Y O [TakeLeftFork.p2])" ;\xa\ ASSERT_LTL == "G(e(DropFork.p3) => Y O [TakeLeftFork.p3])" #-}'),'src_position'(44,1,853,299)). | |
| 47 | 'symbol'('BSet','BSet','src_span'(2,10,2,14,10,4),'Datatype'). | |
| 48 | 'symbol'('phils','phils','src_span'(2,17,2,22,17,5),'Constructor of Datatype'). | |
| 49 | 'symbol'('BPhils','BPhils','src_span'(3,10,3,16,32,6),'Datatype'). | |
| 50 | 'symbol'('p1','p1','src_span'(3,19,3,21,41,2),'Constructor of Datatype'). | |
| 51 | 'symbol'('p2','p2','src_span'(3,24,3,26,46,2),'Constructor of Datatype'). | |
| 52 | 'symbol'('p3','p3','src_span'(3,29,3,31,51,2),'Constructor of Datatype'). | |
| 53 | 'symbol'('B','B','src_span'(4,1,4,2,54,1),'Funktion or Process'). | |
| 54 | 'symbol'('phils','phils','src_span'(2,17,2,22,17,5),'Constructor of Datatype'). | |
| 55 | 'symbol'('think','think','src_span'(7,9,7,14,82,5),'Channel'). | |
| 56 | 'symbol'('eat','eat','src_span'(7,16,7,19,89,3),'Channel'). | |
| 57 | 'symbol'('TakeLeftFork','TakeLeftFork','src_span'(7,21,7,33,94,12),'Channel'). | |
| 58 | 'symbol'('TakeRightFork','TakeRightFork','src_span'(7,35,7,48,108,13),'Channel'). | |
| 59 | 'symbol'('DropFork','DropFork','src_span'(7,50,7,58,123,8),'Channel'). | |
| 60 | 'symbol'('MAIN','MAIN','src_span'(10,1,10,5,145,4),'Ident (Groundrep.)'). | |
| 61 | 'symbol'('p','p','src_span'(10,12,10,13,156,1),'Ident (Prolog Variable)'). | |
| 62 | 'symbol'('PHIL','PHIL','src_span'(12,1,12,5,178,4),'Funktion or Process'). | |
| 63 | 'symbol'('P','P','src_span'(12,6,12,7,183,1),'Ident (Prolog Variable)'). | |
| 64 | 'symbol'('Test2','Test2','src_span'(16,2,16,7,316,5),'Ident (Groundrep.)'). | |
| 65 | 'symbol'('x','x','src_span'(16,17,16,18,331,1),'Ident (Prolog Variable)'). | |
| 66 | 'symbol'('x2','x','src_span'(16,26,16,27,340,1),'Ident (Prolog Variable)'). | |
| 67 | 'symbol'('Phil1','Phil1','src_span'(17,1,17,6,350,5),'Ident (Groundrep.)'). | |
| 68 | 'symbol'('TESTC','TESTC','src_span'(19,1,19,6,368,5),'Ident (Groundrep.)'). | |
| 69 | 'symbol'('p4','p','src_span'(19,12,19,13,379,1),'Ident (Prolog Variable)'). | |
| 70 | 'symbol'('TESTC2','TESTC2','src_span'(20,1,20,7,400,6),'Ident (Groundrep.)'). | |
| 71 | 'symbol'('p5','p','src_span'(20,14,20,15,413,1),'Ident (Prolog Variable)'). | |
| 72 | 'symbol'('c','c','src_span'(23,9,23,10,444,1),'Channel'). | |
| 73 | 'symbol'('d','d','src_span'(23,11,23,12,446,1),'Channel'). | |
| 74 | 'symbol'('TestNeil','TestNeil','src_span'(25,1,25,9,457,8),'Ident (Groundrep.)'). | |
| 75 | 'symbol'('x3','x','src_span'(25,14,25,15,470,1),'Ident (Prolog Variable)'). |