1load_package redlog;
2
3
4rlset(qqe,ofsf);
5
6
7{}
8
9off rlverbose;
10
11
12
13% Examples from C. Strasser's diploma thesis
14% Ch.10. Software Verifikation, p.171
15f := ex({q},((j > 5 and radd(a,q) == qepsilon) or (radd(a,q) <<>>
16qepsilon and lhead(radd(a,q)) > 23 + j)) and lhead(radd(a,q)) = x)$
17
18
19
20rlqe f;
21
22
23(a - x = 0 and a - j - 23 > 0) or j - x + 23 < 0
24
25
26f := ex({a}, ((j > 5 and radd(a,q) == qepsilon) or (radd(a,q) <<>>
27qepsilon and lhead(radd(a,q)) > 23 + j)) and lhead(radd(a,q)) = x)$
28
29
30
31rlqe f;
32
33
34(q == qepsilon and j - x + 23 < 0)
35
36 or (lhead(q) - x = 0 and q <<>> qepsilon and lhead(q) - j - 23 > 0)
37
38
39% 2-periodic queue of odd length with prefix [0,0] and postfix [1,1]:
40p2 := ex(qp,q == ladd(0,ladd(0,radd(1,radd(1,qp)))) and
41ex({x,y},x <> y and ladd(y,ladd(x,qp)) == radd(y,radd(x,qp))))$
42
43
44
45rlqe p2;
46
47
48(rtail(ltail(ltail(rtail(rtail(q))))) == qepsilon
49
50 and ltail(ltail(rtail(rtail(q)))) <<>> qepsilon and
51
52lhead(ltail(ltail(rtail(rtail(q))))) - rhead(ltail(ltail(rtail(rtail(q))))) = 0
53
54 and rhead(ltail(rtail(rtail(q)))) - 1 = 0 and rhead(rtail(rtail(q))) - 1 = 0
55
56 and lhead(rtail(q)) = 0 and lhead(q) = 0) or (
57
58ltail(ltail(ltail(ltail(rtail(rtail(q))))))
59
60 == rtail(rtail(ltail(ltail(rtail(rtail(q))))))
61
62 and rtail(ltail(ltail(rtail(rtail(q))))) <<>> qepsilon and
63
64lhead(rtail(ltail(ltail(rtail(rtail(q))))))
65
66 - rhead(ltail(ltail(ltail(rtail(rtail(q)))))) = 0 and
67
68lhead(ltail(ltail(rtail(rtail(q))))) - rhead(ltail(ltail(rtail(rtail(q))))) = 0
69
70and rhead(ltail(ltail(ltail(rtail(rtail(q))))))
71
72 - rhead(ltail(ltail(rtail(rtail(q))))) <> 0
73
74 and rhead(ltail(rtail(rtail(q)))) - 1 = 0 and rhead(rtail(rtail(q))) - 1 = 0
75
76 and lhead(rtail(q)) = 0 and lhead(q) = 0)
77
78
79end;
80
81Tested on x86_64-pc-windows CSL
82Time (counter 1): 0 ms
83
84End of Lisp run after 0.00+0.09 seconds
85real 0.25
86user 0.03
87sys 0.04
88