blob: 532a8f3a863d2e9275a3a6525d654abec710eeef (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
|
; EXPECT: unsat
; COMMAND-LINE: --sygus-out=status --lang=sygus2
(set-logic BV)
;Trace length
(define-sort Stream () (_ BitVec 48))
(define-fun ZERO () Stream (_ bv0 48))
(define-fun ONE () Stream (_ bv1 48))
(define-fun S_FALSE () Stream ZERO)
(define-fun S_TRUE () Stream (bvnot S_FALSE))
; Yesterday: X << 1
(define-fun
Y ( (X Stream) ) Stream
(bvshl X ONE)
)
; Once: X|-X
(define-fun
O ( (X Stream) ) Stream
(bvor X (bvneg X))
)
; Historically: X & ~(1 + X)
(define-fun
H ( (X Stream) ) Stream
(bvand X (bvnot (bvadd ONE X)))
)
; Since: Z | (X & ~((X | Z) + Z))
(define-fun
S ( (X Stream) (Z Stream) ) Stream
(bvor Z
(bvand X
(bvnot (bvadd (bvor X Z) Z ))
)
)
)
(define-fun
bvimpl ( (X Stream) (Z Stream) ) Stream
(bvor (bvnot X) Z)
)
(synth-fun phi ((ulInformationTransfer Stream) (dlInformationTransfer Stream) (rrcConnectionReconfiguration Stream) (measurementReport Stream) (systemInformationBlockType1 Stream) (securityModeComplete Stream) (systemInformation Stream) (rrcConnectionReestablishmentReject Stream) (rrcConnectionRequest Stream) (rrcConnectionSetupComplete Stream) (rrcConnectionRelease Stream) (ueCapabilityInformation Stream) (rrcConnectionSetup Stream) (securityModeCommand Stream) (ueCapabilityEnquiry Stream) (rrcConnectionReconfigurationComplete Stream) (rrcConnectionReestablishmentRequest Stream)) Stream
((<F> Stream))
((<F> Stream (
S_TRUE
S_FALSE
( Variable Stream )
(bvnot <F>)
(bvand <F> <F>)
(bvor <F> <F>)
(bvimpl <F> <F>)
(Y <F>)
(O <F>)
(H <F>)
(S <F> <F>)
)))
)
;; Positive examples
;Positive Trace Data
(constraint
(and
(= ((_ extract 8 0) (phi #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000100000 #b000000000000000000000000000000000000000011000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000010000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000001 #b000000000000000000000000000000000000000000000100 #b000000000000000000000000000000000000000100000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000010 #b000000000000000000000000000000000000000000001000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000000)) ((_ extract 8 0) S_TRUE))
(= (phi #b000000000000000000000100000000100000000000000000 #b000000000000000000000010000000000000000000000000 #b000000101000000001010000000100000100001000100000 #b000000000100000000001000000000000010100000000000 #b000010000001000100000001000000010000000000000000 #b000000000000000000000000000000000000000000010000 #b001100000010111000000000110011000001000000000000 #b100000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000001 #b000000000000000000000000000000000000000000000100 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000100000000 #b000000000000000000000000000000000000000000000010 #b000000000000000000000000000000000000000000001000 #b000000000000000000000000000000000000000010000000 #b000001010000000010100000001000001000010001000000 #b010000000000000000000000000000000000000000000000) S_TRUE)
(= ((_ extract 15 0) (phi #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000010000010100000 #b000000000000000000000000000000000001100000000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000010000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000001 #b000000000000000000000000000000000000000000000100 #b000000000000000000000000000000001000000000000000 #b000000000000000000000000000000000000010000000000 #b000000000000000000000000000000000000000000000010 #b000000000000000000000000000000000000000000001000 #b000000000000000000000000000000000000001000000000 #b000000000000000000000000000000000100000101000000 #b000000000000000000000000000000000000000000000000)) ((_ extract 15 0) S_TRUE))
(= ((_ extract 15 0) (phi #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000010001000000 #b000000000000000000000000000000000111000000000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000100000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000001 #b000000000000000000000000000000000000000000000100 #b000000000000000000000000000000001000000000000000 #b000000000000000000000000000000000000001000000000 #b000000000000000000000000000000000000000000001010 #b000000000000000000000000000000000000000000010000 #b000000000000000000000000000000000000000100000000 #b000000000000000000000000000000000000100010000000 #b000000000000000000000000000000000000000000000000)) ((_ extract 15 0) S_TRUE))
(= ((_ extract 20 0) (phi #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000001001001010100000 #b000000000000000000000000000000000000100000000000 #b000000000000000000000000000010000100000000000000 #b000000000000000000000000000000000000000000010000 #b000000000000000000000000000001100000000000000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000001 #b000000000000000000000000000000000000000000000100 #b000000000000000000000000000100000000000000000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000010 #b000000000000000000000000000000000000000000001000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000010010010101000000 #b000000000000000000000000000000000000000000000000)) ((_ extract 20 0) S_TRUE))
)
)
;; Negative examples
;Negative Trace Data
(constraint
(and
(not (= ((_ extract 6 0) (phi #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000001000 #b000000000000000000000000000000000000000000110000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000001 #b000000000000000000000000000000000000000000000100 #b000000000000000000000000000000000000000001000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000010 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000000)) ((_ extract 6 0) S_TRUE)))
(not (= ((_ extract 45 0) (phi #b000000000000000000000001000000001000000000000000 #b000000000000000000000000100000000000000000000000 #b000000001010000000010100000001000001000010001000 #b000000000001000000000010000000000000101000000000 #b000000100000010001000000010000000100000000000000 #b000000000000000000000000000000000000000000000000 #b000011000000101110000000001100110000010000000000 #b001000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000001 #b000000000000000000000000000000000000000000000100 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000001000000 #b000000000000000000000000000000000000000000000010 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000100000 #b000000010100000000101000000010000010000100010000 #b000100000000000000000000000000000000000000000000)) ((_ extract 45 0) S_TRUE)))
(not (= ((_ extract 13 0) (phi #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000100000101000 #b000000000000000000000000000000000000011000000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000001 #b000000000000000000000000000000000000000000000100 #b000000000000000000000000000000000010000000000000 #b000000000000000000000000000000000000000100000000 #b000000000000000000000000000000000000000000000010 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000010000000 #b000000000000000000000000000000000001000001010000 #b000000000000000000000000000000000000000000000000)) ((_ extract 13 0) S_TRUE)))
(not (= ((_ extract 13 0) (phi #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000100010000 #b000000000000000000000000000000000001110000000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000001 #b000000000000000000000000000000000000000000000100 #b000000000000000000000000000000000010000000000000 #b000000000000000000000000000000000000000010000000 #b000000000000000000000000000000000000000000001010 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000001000000 #b000000000000000000000000000000000000001000100000 #b000000000000000000000000000000000000000000000000)) ((_ extract 13 0) S_TRUE)))
(not (= ((_ extract 18 0) (phi #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000010010010101000 #b000000000000000000000000000000000000001000000000 #b000000000000000000000000000000100001000000000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000011000000000000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000001 #b000000000000000000000000000000000000000000000100 #b000000000000000000000000000001000000000000000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000010 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000100100101010000 #b000000000000000000000000000000000000000000000000)) ((_ extract 18 0) S_TRUE)))
)
)
; Solution: G (p -> O f)
(check-synth)
|
