| 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'('AIRPORT',['constructor'('LGW'),'constructor'('SOU'),'constructor'('AMS')]). | |
| 18 | 'bindval'('airportpairs','setExp'('rangeEnum'(['tupleExp'([_i,_j])]),['comprehensionGenerator'(_i,'AIRPORT'),'comprehensionGenerator'(_j,'AIRPORT')]),'src_span'(38,1,38,45,1601,44)). | |
| 19 | 'channel'('link','type'('dotTupleType'(['AIRPORT','AIRPORT']))). | |
| 20 | 'channel'('break','type'('dotTupleType'(['AIRPORT','AIRPORT']))). | |
| 21 | 'bindval'('Sigma','closure'(['link','break']),'src_span'(41,1,41,23,1682,22)). | |
| 22 | 'agent'('LNK'(_i2,_j2),'[]'('prefix'('src_span'(43,12,43,20,1717,8),[],'dotTuple'(['link',_i2,_j2]),'prefix'('src_span'(43,24,43,32,1729,8),[],'dotTuple'(['link',_j2,_i2]),'agent_call'('src_span'(43,36,43,39,1741,3),'BRK',[_i2,_j2]),'src_span'(43,33,43,35,1737,20)),'src_span'(43,21,43,23,1725,32)),'prefix'('src_span'(43,48,43,56,1753,8),[],'dotTuple'(['link',_j2,_i2]),'prefix'('src_span'(43,60,43,68,1765,8),[],'dotTuple'(['link',_i2,_j2]),'agent_call'('src_span'(43,72,43,75,1777,3),'BRK',[_i2,_j2]),'src_span'(43,69,43,71,1773,20)),'src_span'(43,57,43,59,1761,32)),'src_span_operator'('no_loc_info_available','src_span'(43,45,43,47,1750,2))),'no_loc_info_available'). | |
| 23 | 'agent'('BRK'(_i3,_j3),'[]'('prefix'('src_span'(44,12,44,21,1797,9),[],'dotTuple'(['break',_i3,_j3]),'prefix'('src_span'(44,25,44,34,1810,9),[],'dotTuple'(['break',_j3,_i3]),'agent_call'('src_span'(44,38,44,41,1823,3),'LNK',[_i3,_j3]),'src_span'(44,35,44,37,1819,21)),'src_span'(44,22,44,24,1806,34)),'prefix'('src_span'(44,50,44,59,1835,9),[],'dotTuple'(['break',_j3,_i3]),'prefix'('src_span'(44,63,44,72,1848,9),[],'dotTuple'(['break',_i3,_j3]),'agent_call'('src_span'(44,76,44,79,1861,3),'LNK',[_i3,_j3]),'src_span'(44,73,44,75,1857,21)),'src_span'(44,60,44,62,1844,34)),'src_span_operator'('no_loc_info_available','src_span'(44,47,44,49,1832,2))),'no_loc_info_available'). | |
| 24 | 'agent'('alpha'(_i4,_j4),'setExp'('rangeEnum'(['dotTuple'(['link',_i4,_j4]),'dotTuple'(['link',_j4,_i4]),'dotTuple'(['break',_i4,_j4]),'dotTuple'(['break',_j4,_i4])])),'src_span'(46,14,46,56,1884,42)). | |
| 25 | 'bindval'('MAIN','procRepAParallel'(['comprehensionGenerator'('tuplePat'([_i5,_j5]),'val_of'('airportpairs','src_span'(48,17,48,29,1944,12)))],'pair'('agent_call'('src_span'(48,33,48,38,1960,5),'alpha',[_i5,_j5]),'agent_call'('src_span'(48,45,48,48,1972,3),'LNK',[_i5,_j5])),'src_span'(48,11,48,31,1938,20)),'src_span'(48,1,48,53,1928,52)). | |
| 26 | 'bindval'('SPEC','|~|'('stop'('src_span'(50,8,50,12,1990,4)),'repInternalChoice'(['comprehensionGenerator'(_x,'agent_call'('src_span'(50,24,50,28,2006,4),'diff',['val_of'('Sigma','src_span'(50,29,50,34,2011,5)),'setExp'('rangeEnum'(['dotTuple'(['link',_i6,_i6]),'dotTuple'(['break',_i6,_i6])]),['comprehensionGenerator'(_i6,'AIRPORT')])]))],'prefix'('src_span'(50,68,50,69,2050,1),[],_x,'val_of'('SPEC','src_span'(50,71,50,75,2053,4)),'src_span'(50,70,50,70,2051,7)),'src_span'(50,22,50,68,2004,46)),'src_span_operator'('no_loc_info_available','src_span'(50,13,50,16,1995,3))),'src_span'(50,1,50,76,1983,75)). | |
| 27 | 'assertRef'('False','val_of'('SPEC','src_span'(52,8,52,12,2067,4)),'Failure','val_of'('MAIN','src_span'(52,17,52,21,2076,4)),'src_span'(52,1,52,21,2060,20)). | |
| 28 | 'assertRef'('True','val_of'('MAIN','src_span'(53,12,53,16,2092,4)),'Trace','val_of'('SPEC','src_span'(53,21,53,25,2101,4)),'src_span'(53,1,53,25,2081,24)). | |
| 29 | 'comment'('lineComment'('-- AiportCtrl'),'src_position'(1,1,0,13)). | |
| 30 | 'comment'('lineComment'('--SPEC allows all behaviour apart from aiports'),'src_position'(3,1,15,46)). | |
| 31 | 'comment'('lineComment'('--linking or breaking with themselves'),'src_position'(4,1,62,37)). | |
| 32 | 'comment'('lineComment'('--the CSPm process MAIN does not refine the SPEC'),'src_position'(6,1,101,48)). | |
| 33 | 'comment'('lineComment'('--as aiports can be link or break with themselves'),'src_position'(7,1,150,49)). | |
| 34 | 'comment'('lineComment'('--the guards in the B component of the CSP||B combination block such behaviour '),'src_position'(9,1,201,79)). | |
| 35 | 'comment'('lineComment'('--and so it should satisfy the assertion'),'src_position'(10,1,281,40)). | |
| 36 | 'comment'('lineComment'('--However, when combining the CSP||M model all CSP events e are renamed to CSP:e '),'src_position'(12,1,323,81)). | |
| 37 | 'comment'('lineComment'('--hence a spurious counterexample is returned'),'src_position'(13,1,405,45)). | |
| 38 | 'comment'('lineComment'('--as the alphabet of the CSP process SPEC '),'src_position'(14,1,451,42)). | |
| 39 | 'comment'('lineComment'('--and the CSP||M combination MAIN do not match'),'src_position'(15,1,494,46)). | |
| 40 | 'comment'('lineComment'('--We request that each event in the alphabet of each CSP process '),'src_position'(17,1,542,65)). | |
| 41 | 'comment'('lineComment'('--used within assertion specified in the CSP file are prepended with \x27\CSP:\x27\ '),'src_position'(18,1,608,76)). | |
| 42 | 'comment'('lineComment'('--when CSP is being used to drive a B machine'),'src_position'(19,1,685,45)). | |
| 43 | 'comment'('lineComment'('--Alternatively, like MAIN, SPEC could be a special process name'),'src_position'(21,1,732,64)). | |
| 44 | 'comment'('lineComment'('--for a process that should have all events in its alphabet'),'src_position'(22,1,797,59)). | |
| 45 | 'comment'('lineComment'('--prepended with \x27\CSP:\x27\ for this purpose, if this aids implementation.'),'src_position'(23,1,857,70)). | |
| 46 | 'comment'('lineComment'('--This would allow only one assertion for each file, but others could'),'src_position'(24,1,928,69)). | |
| 47 | 'comment'('lineComment'('--be commented out when checking alternative assertions.'),'src_position'(25,1,998,56)). | |
| 48 | 'comment'('lineComment'('--In the meantime we are able to output the entire statespace of the CSP||B'),'src_position'(27,1,1056,75)). | |
| 49 | 'comment'('lineComment'('--combination to an FDR file to perform such checks, but on larger models'),'src_position'(28,1,1132,73)). | |
| 50 | 'comment'('lineComment'('--losing on the fly model checking becomes problematic'),'src_position'(29,1,1206,54)). | |
| 51 | 'comment'('lineComment'('--Note, we realise that the same property could be checked by hiding break.i.j '),'src_position'(31,1,1262,79)). | |
| 52 | 'comment'('lineComment'('--and link.i.j events where i!=j and then checking whether this modified'),'src_position'(32,1,1342,72)). | |
| 53 | 'comment'('lineComment'('--MAIN process refines STOP.'),'src_position'(33,1,1415,28)). | |
| 54 | 'comment'('lineComment'('--However, in general we wish to express any arbitrary SPEC that may'),'src_position'(34,1,1444,68)). | |
| 55 | 'comment'('lineComment'('--not be possible to checked with a similar trick.'),'src_position'(35,1,1513,50)). | |
| 56 | 'symbol'('AIRPORT','AIRPORT','src_span'(37,10,37,17,1574,7),'Datatype'). | |
| 57 | 'symbol'('LGW','LGW','src_span'(37,20,37,23,1584,3),'Constructor of Datatype'). | |
| 58 | 'symbol'('SOU','SOU','src_span'(37,26,37,29,1590,3),'Constructor of Datatype'). | |
| 59 | 'symbol'('AMS','AMS','src_span'(37,32,37,35,1596,3),'Constructor of Datatype'). | |
| 60 | 'symbol'('airportpairs','airportpairs','src_span'(38,1,38,13,1601,12),'Ident (Groundrep.)'). | |
| 61 | 'symbol'('i','i','src_span'(38,23,38,24,1623,1),'Ident (Prolog Variable)'). | |
| 62 | 'symbol'('j','j','src_span'(38,34,38,35,1634,1),'Ident (Prolog Variable)'). | |
| 63 | 'symbol'('link','link','src_span'(40,9,40,13,1655,4),'Channel'). | |
| 64 | 'symbol'('break','break','src_span'(40,14,40,19,1660,5),'Channel'). | |
| 65 | 'symbol'('Sigma','Sigma','src_span'(41,1,41,6,1682,5),'Ident (Groundrep.)'). | |
| 66 | 'symbol'('LNK','LNK','src_span'(43,1,43,4,1706,3),'Funktion or Process'). | |
| 67 | 'symbol'('i2','i','src_span'(43,5,43,6,1710,1),'Ident (Prolog Variable)'). | |
| 68 | 'symbol'('j2','j','src_span'(43,7,43,8,1712,1),'Ident (Prolog Variable)'). | |
| 69 | 'symbol'('BRK','BRK','src_span'(44,1,44,4,1786,3),'Funktion or Process'). | |
| 70 | 'symbol'('i3','i','src_span'(44,5,44,6,1790,1),'Ident (Prolog Variable)'). | |
| 71 | 'symbol'('j3','j','src_span'(44,7,44,8,1792,1),'Ident (Prolog Variable)'). | |
| 72 | 'symbol'('alpha','alpha','src_span'(46,1,46,6,1871,5),'Funktion or Process'). | |
| 73 | 'symbol'('i4','i','src_span'(46,7,46,8,1877,1),'Ident (Prolog Variable)'). | |
| 74 | 'symbol'('j4','j','src_span'(46,9,46,10,1879,1),'Ident (Prolog Variable)'). | |
| 75 | 'symbol'('MAIN','MAIN','src_span'(48,1,48,5,1928,4),'Ident (Groundrep.)'). | |
| 76 | 'symbol'('i5','i','src_span'(48,12,48,13,1939,1),'Ident (Prolog Variable)'). | |
| 77 | 'symbol'('j5','j','src_span'(48,14,48,15,1941,1),'Ident (Prolog Variable)'). | |
| 78 | 'symbol'('SPEC','SPEC','src_span'(50,1,50,5,1983,4),'Ident (Groundrep.)'). | |
| 79 | 'symbol'('x','x','src_span'(50,22,50,23,2004,1),'Ident (Prolog Variable)'). | |
| 80 | 'symbol'('diff','diff','src_span'(50,24,50,28,2006,4),'BuiltIn primitive'). | |
| 81 | 'symbol'('i6','i','src_span'(50,55,50,56,2037,1),'Ident (Prolog Variable)'). |