| 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'('books',['constructor'('b1'),'constructor'('b2')]). | |
| 18 | 'dataTypeDef'('members',['constructor'('m1')]). | |
| 19 | 'channel'('lend','type'('dotTupleType'(['books','members']))). | |
| 20 | 'channel'('renew','type'('dotTupleType'(['books']))). | |
| 21 | 'channel'('return','type'('dotTupleType'(['books']))). | |
| 22 | 'channel'('acquire','type'('dotTupleType'(['books']))). | |
| 23 | 'channel'('discard','type'('dotTupleType'(['books']))). | |
| 24 | 'channel'('register','type'('dotTupleType'(['members']))). | |
| 25 | 'channel'('unregister','type'('dotTupleType'(['members']))). | |
| 26 | 'agent'('loans'(_bld,_mld),'[]'('prefix'('src_span'(18,19,18,31,491,12),[],'dotTuple'(['lend',_bld,_mld]),'agent_call'('src_span'(18,35,18,41,507,6),'loans2',[_bld,_mld]),'src_span'(18,32,18,34,503,31)),'skip'('src_span'(18,54,18,58,526,4)),'src_span_operator'('no_loc_info_available','src_span'(18,51,18,53,523,2))),'no_loc_info_available'). | |
| 27 | 'agent'('loans2'(_bld2,_mld2),'[]'('prefix'('src_span'(19,19,19,28,549,9),[],'dotTuple'(['renew',_bld2]),'agent_call'('src_span'(19,32,19,38,562,6),'loans2',[_bld2,_mld2]),'src_span'(19,29,19,31,558,28)),'prefix'('src_span'(20,19,20,29,599,10),[],'dotTuple'(['return',_bld2]),'agent_call'('src_span'(20,33,20,38,613,5),'loans',[_bld2,_mld2]),'src_span'(20,30,20,32,609,28)),'src_span_operator'('no_loc_info_available','src_span'(19,48,19,50,578,2))),'no_loc_info_available'). | |
| 28 | 'agent'('loan'(_bld3,_mld3),'prefix'('src_span'(23,18,23,30,678,12),[],'dotTuple'(['lend',_bld3,_mld3]),'agent_call'('src_span'(23,34,23,39,694,5),'loan2',[_bld3,_mld3]),'src_span'(23,31,23,33,690,30)),'src_span'(23,18,23,48,678,30)). | |
| 29 | 'agent'('loan2'(_bld4,_mld4),'[]'('prefix'('src_span'(24,18,24,27,726,9),[],'dotTuple'(['renew',_bld4]),'agent_call'('src_span'(24,31,24,37,739,6),'loans2',[_bld4,_mld4]),'src_span'(24,28,24,30,735,28)),'prefix'('src_span'(25,19,25,29,776,10),[],'dotTuple'(['return',_bld4]),'skip'('src_span'(25,33,25,37,790,4)),'src_span'(25,30,25,32,786,18)),'src_span_operator'('no_loc_info_available','src_span'(24,47,24,49,755,2))),'no_loc_info_available'). | |
| 30 | 'agent'('book'(_bld5),'prefix'('src_span'(27,13,27,24,808,11),[],'dotTuple'(['acquire',_bld5]),'agent_call'('src_span'(27,28,27,33,823,5),'book2',[_bld5]),'src_span'(27,25,27,27,819,25)),'src_span'(27,13,27,38,808,25)). | |
| 31 | 'agent'('book2'(_bld6),'[]'('prefix'('src_span'(28,14,28,25,847,11),[],'dotTuple'(['discard',_bld6]),'agent_call'('src_span'(28,29,28,33,862,4),'book',[_bld6]),'src_span'(28,26,28,28,858,24)),';'('repChoice'(['comprehensionGenerator'(_mld5,'members')],'agent_call'('src_span'(29,30,29,34,904,4),'loan',[_bld6,_mld5]),'src_span'(29,18,29,30,892,12)),'agent_call'('src_span'(29,47,29,52,921,5),'book2',[_bld6]),'src_span_operator'('no_loc_info_available','src_span'(29,45,29,46,919,1))),'src_span_operator'('no_loc_info_available','src_span'(28,39,28,41,872,2))),'no_loc_info_available'). | |
| 32 | 'agent'('mem'(_mld6),'prefix'('src_span'(32,12,32,24,946,12),[],'dotTuple'(['register',_mld6]),'agent_call'('src_span'(32,28,32,32,962,4),'mem2',[_mld6]),'src_span'(32,25,32,27,958,25)),'src_span'(32,12,32,37,946,25)). | |
| 33 | 'agent'('mem2'(_mld7),'[]'('prefix'('src_span'(33,13,33,27,984,14),[],'dotTuple'(['unregister',_mld7]),'agent_call'('src_span'(33,31,33,34,1002,3),'mem',[_mld7]),'src_span'(33,28,33,30,998,26)),';'('repInterleave'(['comprehensionGenerator'(_bld7,'books')],'agent_call'('src_span'(34,28,34,33,1041,5),'loans',[_bld7,_mld7]),'src_span'(34,18,34,28,1031,10)),'agent_call'('src_span'(34,46,34,50,1059,4),'mem2',[_mld7]),'src_span_operator'('no_loc_info_available','src_span'(34,44,34,45,1057,1))),'src_span_operator'('no_loc_info_available','src_span'(33,40,33,42,1011,2))),'no_loc_info_available'). | |
| 34 | 'bindval'('mems','repInterleave'(['comprehensionGenerator'(_mld8,'members')],'agent_call'('src_span'(36,23,36,26,1093,3),'mem',[_mld8]),'src_span'(36,11,36,23,1081,12)),'src_span'(36,1,36,31,1071,30)). | |
| 35 | 'bindval'('bks','repInterleave'(['comprehensionGenerator'(_bld8,'books')],'agent_call'('src_span'(37,21,37,25,1122,4),'book',[_bld8]),'src_span'(37,11,37,21,1112,10)),'src_span'(37,1,37,30,1102,29)). | |
| 36 | 'bindval'('MAIN','sharing'('closure'(['lend','return','renew']),'val_of'('mems','src_span'(39,8,39,12,1140,4)),'val_of'('bks','src_span'(39,45,39,48,1177,3)),'src_span'(39,13,39,44,1145,31)),'src_span'(39,1,39,48,1133,47)). | |
| 37 | 'bindval'('PROB_TEST_TRACE','prefix'('src_span'(41,19,41,30,1200,11),[],'dotTuple'(['register','m1']),'prefix'('src_span'(41,34,41,44,1215,10),[],'dotTuple'(['acquire','b2']),'prefix'('src_span'(41,48,41,58,1229,10),[],'dotTuple'(['lend','b2','m1']),'prefix'('src_span'(41,62,41,70,1243,8),[],'dotTuple'(['renew','b2']),'prefix'('src_span'(41,74,41,83,1255,9),[],'dotTuple'(['return','b2']),'prefix'('src_span'(41,87,41,100,1268,13),[],'dotTuple'(['unregister','m1']),'prefix'('src_span'(41,104,41,114,1285,10),[],'dotTuple'(['discard','b2']),'stop'('src_span'(41,118,41,122,1299,4)),'src_span'(41,115,41,117,1295,18)),'src_span'(41,101,41,103,1281,35)),'src_span'(41,84,41,86,1264,48)),'src_span'(41,71,41,73,1251,60)),'src_span'(41,59,41,61,1239,74)),'src_span'(41,45,41,47,1225,88)),'src_span'(41,31,41,33,1211,103)),'src_span'(41,1,41,122,1182,121)). | |
| 38 | 'assertRef'('False','val_of'('MAIN','src_span'(42,8,42,12,1311,4)),'Trace','val_of'('PROB_TEST_TRACE','src_span'(42,17,42,32,1320,15)),'src_span'(42,1,42,32,1304,31)). | |
| 39 | 'assertModelCheckExt'('False','val_of'('MAIN','src_span'(43,8,43,12,1343,4)),'DeadlockFree','F'). | |
| 40 | 'comment'('lineComment'('-- Library'),'src_position'(1,1,0,10)). | |
| 41 | 'comment'('lineComment'('-- hand translated from ASTD by Michael Leuschel, 11th April 2018'),'src_position'(2,1,11,65)). | |
| 42 | 'comment'('lineComment'('-- some optimisations done by hand; e.g., hand translation of loan *'),'src_position'(3,1,77,68)). | |
| 43 | 'comment'('lineComment'('-- has an infinite state space for FDR (version 2 at least)'),'src_position'(4,1,146,59)). | |
| 44 | 'comment'('lineComment'('-- | b3'),'src_position'(6,26,232,7)). | |
| 45 | 'comment'('lineComment'('-- | m2 | m3'),'src_position'(7,23,262,12)). | |
| 46 | 'comment'('lineComment'('-- a translation of loan *'),'src_position'(17,1,446,26)). | |
| 47 | 'comment'('lineComment'('-- a translation of single loan'),'src_position'(22,1,629,31)). | |
| 48 | 'comment'('lineComment'('-- assert MAIN |= LTL: "G not(e(unregister.m1))"'),'src_position'(44,1,1370,48)). | |
| 49 | 'comment'('lineComment'('-- for 3 books, 3 members: 5969 states, 38671 transitions, 45 seconds'),'src_position'(46,1,1420,69)). | |
| 50 | 'symbol'('books','books','src_span'(6,10,6,15,216,5),'Datatype'). | |
| 51 | 'symbol'('b1','b1','src_span'(6,18,6,20,224,2),'Constructor of Datatype'). | |
| 52 | 'symbol'('b2','b2','src_span'(6,23,6,25,229,2),'Constructor of Datatype'). | |
| 53 | 'symbol'('members','members','src_span'(7,10,7,17,249,7),'Datatype'). | |
| 54 | 'symbol'('m1','m1','src_span'(7,20,7,22,259,2),'Constructor of Datatype'). | |
| 55 | 'symbol'('lend','lend','src_span'(9,9,9,13,284,4),'Channel'). | |
| 56 | 'symbol'('renew','renew','src_span'(10,9,10,14,311,5),'Channel'). | |
| 57 | 'symbol'('return','return','src_span'(11,9,11,15,331,6),'Channel'). | |
| 58 | 'symbol'('acquire','acquire','src_span'(12,9,12,16,353,7),'Channel'). | |
| 59 | 'symbol'('discard','discard','src_span'(13,9,13,16,376,7),'Channel'). | |
| 60 | 'symbol'('register','register','src_span'(14,9,14,17,399,8),'Channel'). | |
| 61 | 'symbol'('unregister','unregister','src_span'(15,9,15,19,425,10),'Channel'). | |
| 62 | 'symbol'('loans','loans','src_span'(18,1,18,6,473,5),'Funktion or Process'). | |
| 63 | 'symbol'('bld','bld','src_span'(18,7,18,10,479,3),'Ident (Prolog Variable)'). | |
| 64 | 'symbol'('mld','mld','src_span'(18,11,18,14,483,3),'Ident (Prolog Variable)'). | |
| 65 | 'symbol'('loans2','loans2','src_span'(19,1,19,7,531,6),'Funktion or Process'). | |
| 66 | 'symbol'('bld2','bld','src_span'(19,8,19,11,538,3),'Ident (Prolog Variable)'). | |
| 67 | 'symbol'('mld2','mld','src_span'(19,12,19,15,542,3),'Ident (Prolog Variable)'). | |
| 68 | 'symbol'('loan','loan','src_span'(23,1,23,5,661,4),'Funktion or Process'). | |
| 69 | 'symbol'('bld3','bld','src_span'(23,6,23,9,666,3),'Ident (Prolog Variable)'). | |
| 70 | 'symbol'('mld3','mld','src_span'(23,10,23,13,670,3),'Ident (Prolog Variable)'). | |
| 71 | 'symbol'('loan2','loan2','src_span'(24,1,24,6,709,5),'Funktion or Process'). | |
| 72 | 'symbol'('bld4','bld','src_span'(24,7,24,10,715,3),'Ident (Prolog Variable)'). | |
| 73 | 'symbol'('mld4','mld','src_span'(24,11,24,14,719,3),'Ident (Prolog Variable)'). | |
| 74 | 'symbol'('book','book','src_span'(27,1,27,5,796,4),'Funktion or Process'). | |
| 75 | 'symbol'('bld5','bld','src_span'(27,6,27,9,801,3),'Ident (Prolog Variable)'). | |
| 76 | 'symbol'('book2','book2','src_span'(28,1,28,6,834,5),'Funktion or Process'). | |
| 77 | 'symbol'('bld6','bld','src_span'(28,7,28,10,840,3),'Ident (Prolog Variable)'). | |
| 78 | 'symbol'('mld5','mld','src_span'(29,18,29,21,892,3),'Ident (Prolog Variable)'). | |
| 79 | 'symbol'('mem','mem','src_span'(32,1,32,4,935,3),'Funktion or Process'). | |
| 80 | 'symbol'('mld6','mld','src_span'(32,5,32,8,939,3),'Ident (Prolog Variable)'). | |
| 81 | 'symbol'('mem2','mem2','src_span'(33,1,33,5,972,4),'Funktion or Process'). | |
| 82 | 'symbol'('mld7','mld','src_span'(33,6,33,9,977,3),'Ident (Prolog Variable)'). | |
| 83 | 'symbol'('bld7','bld','src_span'(34,18,34,21,1031,3),'Ident (Prolog Variable)'). | |
| 84 | 'symbol'('mems','mems','src_span'(36,1,36,5,1071,4),'Ident (Groundrep.)'). | |
| 85 | 'symbol'('mld8','mld','src_span'(36,11,36,14,1081,3),'Ident (Prolog Variable)'). | |
| 86 | 'symbol'('bks','bks','src_span'(37,1,37,4,1102,3),'Ident (Groundrep.)'). | |
| 87 | 'symbol'('bld8','bld','src_span'(37,11,37,14,1112,3),'Ident (Prolog Variable)'). | |
| 88 | 'symbol'('MAIN','MAIN','src_span'(39,1,39,5,1133,4),'Ident (Groundrep.)'). | |
| 89 | 'symbol'('PROB_TEST_TRACE','PROB_TEST_TRACE','src_span'(41,1,41,16,1182,15),'Ident (Groundrep.)'). |