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