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 | 'channel'('a','type'('dotUnitType')). | |
18 | 'channel'('b','type'('dotUnitType')). | |
19 | 'channel'('c','type'('dotUnitType')). | |
20 | 'bindval'('MAIN','[]'('prefix'('src_span'(8,8,8,9,243,1),[],'a','val_of'('MAIN','src_span'(8,13,8,17,248,4)),'src_span'(8,10,8,12,244,9)),'prefix'('src_span'(8,21,8,22,256,1),[],'b','prefix'('src_span'(8,26,8,27,261,1),[],'c','val_of'('MAIN','src_span'(8,31,8,35,266,4)),'src_span'(8,28,8,30,262,9)),'src_span'(8,23,8,25,257,14)),'src_span_operator'('no_loc_info_available','src_span'(8,18,8,20,253,2))),'src_span'(8,1,8,35,236,34)). | |
21 | 'pragma'(' ASSERT_LTL_1=="(GF e(a) => GF [a]) => F [c]" "must fail" ;\xa\ ASSERT_LTL_2=="G([b] => F(e(c)))" "must be true" ;\xa\ assert_ltl "G([a] => F(e(a)))" "optional syntax for writing ltl assertion inside of pragmas";\xa\ assert_ltl == "G([c] => F(e(a)))" "optional syntax for writing ltl assertion inside of pragmas" '). | |
22 | 'comment'('lineComment'('-- SimpleLTL'),'src_position'(1,1,0,12)). | |
23 | 'comment'('lineComment'('-- With "Start search in initialisation" check the following formula:'),'src_position'(3,1,14,69)). | |
24 | 'comment'('lineComment'('-- (GF e(a) => GF [a]) => F [c]'),'src_position'(4,1,84,31)). | |
25 | 'comment'('lineComment'('-- Initially the formula is false; after the counter example is found the same check yields formula true'),'src_position'(5,1,116,104)). | |
26 | 'comment'('pragmaComment'('{-# ASSERT_LTL_1=="(GF e(a) => GF [a]) => F [c]" "must fail" ;\xa\ ASSERT_LTL_2=="G([b] => F(e(c)))" "must be true" ;\xa\ assert_ltl "G([a] => F(e(a)))" "optional syntax for writing ltl assertion inside of pragmas";\xa\ assert_ltl == "G([c] => F(e(a)))" "optional syntax for writing ltl assertion inside of pragmas" #-}'),'src_position'(10,1,272,319)). | |
27 | 'symbol'('a','a','src_span'(7,9,7,10,230,1),'Channel'). | |
28 | 'symbol'('b','b','src_span'(7,11,7,12,232,1),'Channel'). | |
29 | 'symbol'('c','c','src_span'(7,13,7,14,234,1),'Channel'). | |
30 | 'symbol'('MAIN','MAIN','src_span'(8,1,8,5,236,4),'Ident (Groundrep.)'). |