|  | 
| 1 | 1 | (new-declaration (spec X Y) (:= X Y)) | 
| 2 |  | -(spec u4 [(-b _ 1 _) (-b _ 2 _) (-b _ 3 _) (-b _ 4 _) ok]) | 
| 3 |  | - | 
| 4 | 2 | (new-declaration (:: Tested Test) | 
| 5 |  | -  (== @(exec (process #Test #Tested)) ok)) | 
|  | 3 | +  (== @(interact (process #Test #Tested)) ok)) | 
|  | 4 | + | 
|  | 5 | +(spec u4 [(-b _ 1 _) (-b _ 2 _) (-b _ 3 _) (-b _ 4 _) ok]) | 
| 6 | 6 | 
 | 
| 7 | 7 | (:= (make_bin Name X1 X2 X3 X4) | 
| 8 | 8 |   { [(+b Name 1 X1)] [(+b Name 2 X2)] [(+b Name 3 X3)] [(+b Name 4 X4)] }) | 
|  | 
| 18 | 18 | 
 | 
| 19 | 19 | (:= (if A = X and B = Y then R = Z) [(-b A I X) (-b B I Y) (+b R I Z)]) | 
| 20 | 20 | 
 | 
| 21 |  | -''' | 
| 22 |  | -'FIXME | 
| 23 |  | - | 
| 24 |  | -(:= (and AA BB RR) { | 
| 25 |  | -  #(if AA = 0 and BB = XX then RR = 0) | 
| 26 |  | -  #(if AA = 1 and BB = XX then RR = XX) }) | 
| 27 |  | -(show #(and b1 b2 r1)) | 
| 28 |  | -(show (process #b1 #(and b1 b2 r1) #b2)) | 
|  | 21 | +(:= (and A B R) { | 
|  | 22 | +  #(if A = 0 and B = _ then R = 0) | 
|  | 23 | +  #(if A = 1 and B = X then R = X) }) | 
|  | 24 | +(show (process #b1 #(and b1 b2 r) #b2)) | 
| 29 | 25 | 
 | 
| 30 | 26 | (:= (or A B R) { | 
| 31 |  | -  [(-b A I 0) (-b B I X) (+b R I X)] | 
| 32 |  | -  [(-b A I 1) (-b B I X) (+b R I 1)]}) | 
|  | 27 | +  #(if A = 0 and B = X then R = X) | 
|  | 28 | +  #(if A = 1 and B = Y then R = 1) }) | 
|  | 29 | +(show (process #b1 #(or b1 b2 r) #b2)) | 
| 33 | 30 | 
 | 
|  | 31 | +''' | 
| 34 | 32 | (:= (xor A B R) { | 
| 35 |  | -  [(-b A I 1) (-b B I 0) (+b R I 1)] | 
| 36 |  | -  [(-b A I 0) (-b B I 1) (+b R I 1)] | 
| 37 |  | -  [(-b A I 0) (-b B I 0) (+b R I 0)] | 
| 38 |  | -  [(-b A I 1) (-b B I 1) (+b R I 0)]}) | 
|  | 33 | +  #(if A = X and B = X then R = 0) }) | 
|  | 34 | +(show (process #b1 #(xor b1 b2 r) #b2)) | 
| 39 | 35 | ''' | 
0 commit comments