|  | 
| 1 |  | -''' | 
| 2 |  | -(spec u4 [(-b 1 _) (-b 2 _) (-b 3 _) (-b 4 _) ok]) | 
|  | 1 | +(spec u4 [(-b _ 1 _) (-b _ 2 _) (-b _ 3 _) (-b _ 4 _) ok]) | 
| 3 | 2 | 
 | 
| 4 |  | -(new-declaration (:: tested test) | 
| 5 |  | -  (:= test @(exec (process #test #test{b=>+b}))) | 
| 6 |  | -  (== test ok)) | 
|  | 3 | +(new-declaration (:: Tested Test) | 
|  | 4 | +  (== @(exec (process #Test #Tested)) ok)) | 
| 7 | 5 | 
 | 
| 8 |  | -(:= b1 [ [(b 1 1)] [(b 2 0)] [(b 3 0)] [(b 4 1)]]) | 
| 9 |  | -(:: b1 u4) | 
|  | 6 | +(:= (make_bin Name X1 X2 X3 X4) | 
|  | 7 | +  { [(+b Name 1 X1)] [(+b Name 2 X2)] [(+b Name 3 X3)] [(+b Name 4 X4)] }) | 
| 10 | 8 | 
 | 
| 11 |  | -(:= b2 [ [(b 1 0)] [(b 2 0)] [(b 3 1)] [(b 4 1)]]) | 
|  | 9 | +(:= b1 #(make_bin b1 0 0 0 1)) | 
| 12 | 10 | (:: b1 u4) | 
| 13 | 11 | 
 | 
| 14 |  | -(:= and [ | 
| 15 |  | -  [(-b1 arg 0) (-b2 arg X) (b arg 0)] | 
| 16 |  | -  [(-b1 arg 1) (-b2 arg X) (b arg X)]]) | 
| 17 |  | - | 
| 18 |  | -(:= or [ | 
| 19 |  | -  [(-b1 arg 0) (-b2 arg X) (b arg X)] | 
| 20 |  | -  [(-b1 arg 1) (-b2 arg X) (b arg 1)]]) | 
| 21 |  | - | 
| 22 |  | -(:= xor [ | 
| 23 |  | -  [(-b1 arg 1) (-b2 arg 0) (b arg 1)] | 
| 24 |  | -  [(-b1 arg 0) (-b2 arg 1) (b arg 1)] | 
| 25 |  | -  [(-b1 arg 0) (-b2 arg 0) (b arg 0)] | 
| 26 |  | -  [(-b1 arg 1) (-b2 arg 1) (b arg 0)]]) | 
| 27 |  | - | 
| 28 |  | -'logical AND | 
| 29 |  | -<show exec (process | 
| 30 |  | -  #b1{b=>+b1} | 
| 31 |  | -  #and{arg=>1} #and{arg=>2} #and{arg=>3} #and{arg=>4} | 
| 32 |  | -  #b2{b=>+b2} | 
| 33 |  | -  kill)> | 
| 34 |  | - | 
| 35 |  | -'logical OR | 
| 36 |  | -<show exec (process | 
| 37 |  | -  #b1{b=>+b1} | 
| 38 |  | -  #or{arg=>1} #or{arg=>2} #or{arg=>3} #or{arg=>4} | 
| 39 |  | -  #b2{b=>+b2} | 
| 40 |  | -  kill)> | 
| 41 |  | - | 
| 42 |  | -'logical XOR | 
| 43 |  | -<show exec (process | 
| 44 |  | -  #b1{b=>+b1} | 
| 45 |  | -  #xor{arg=>1} #xor{arg=>2} #xor{arg=>3} #xor{arg=>4} | 
| 46 |  | -  #b2{b=>+b2} | 
| 47 |  | -  kill)> | 
| 48 |  | -  ''' | 
|  | 12 | +(:= b2 #(make_bin b2 0 0 1 1)) | 
|  | 13 | +(:: b2 u4) | 
|  | 14 | + | 
|  | 15 | +(show #b1) | 
|  | 16 | +(show #b2) | 
|  | 17 | + | 
|  | 18 | +(:= (if A = X and B = Y then R = Z) [(-b A I X) (-b B I Y) (+b R I Z)]) | 
|  | 19 | + | 
|  | 20 | +''' | 
|  | 21 | +'FIXME | 
|  | 22 | + | 
|  | 23 | +(:= (and AA BB RR) { | 
|  | 24 | +  #(if AA = 0 and BB = XX then RR = 0) | 
|  | 25 | +  #(if AA = 1 and BB = XX then RR = XX) }) | 
|  | 26 | +(show #(and b1 b2 r1)) | 
|  | 27 | +(show (process #b1 #(and b1 b2 r1) #b2)) | 
|  | 28 | + | 
|  | 29 | +(:= (or A B R) { | 
|  | 30 | +  [(-b A I 0) (-b B I X) (+b R I X)] | 
|  | 31 | +  [(-b A I 1) (-b B I X) (+b R I 1)]}) | 
|  | 32 | + | 
|  | 33 | +(:= (xor A B R) { | 
|  | 34 | +  [(-b A I 1) (-b B I 0) (+b R I 1)] | 
|  | 35 | +  [(-b A I 0) (-b B I 1) (+b R I 1)] | 
|  | 36 | +  [(-b A I 0) (-b B I 0) (+b R I 0)] | 
|  | 37 | +  [(-b A I 1) (-b B I 1) (+b R I 0)]}) | 
|  | 38 | +''' | 
0 commit comments