Created page with "This puzzle is [https://bgr.com/2015/11/20/apple-interview-questions/ apparently an Interview question at Apple]. Quoting from [https://bgr.com/2015/11/20/apple-interview-ques..." |
No edit summary |
||
| Line 6: | Line 6: | ||
* (4) By looking at the fruit, how can you immediately label all of the boxes correctly? | * (4) By looking at the fruit, how can you immediately label all of the boxes correctly? | ||
Here is one encoding of this puzzle in B | Here is one encoding of this puzzle in B: | ||
<pre> | <pre> | ||
MACHINE ApplesOranges | MACHINE ApplesOranges | ||
| Line 32: | Line 33: | ||
END | END | ||
</pre> | </pre> | ||
We have abstracted the box of apples <tt>a</tt> by the set containing <tt>apple</tt>. Ditto for <tt>o</tt> and <tt>b</tt>, which are abstracted by <tt>{orange}</tt} and <tt>{apple,orange}</tt> respectively. | |||
Note: you need a recent version of ProB 1.5.1-beta3 or newer to load the above model with its one-line comments. If you have an older version of ProB, simply use the normal comments <tt>/* ... */</tt>. | Note: you need a recent version of ProB 1.5.1-beta3 or newer to load the above model with its one-line comments. If you have an older version of ProB, simply use the normal comments <tt>/* ... */</tt>. | ||
This puzzle is apparently an Interview question at Apple. Quoting from [1] we have the following information:
Here is one encoding of this puzzle in B:
MACHINE ApplesOranges
SETS
Fruit={apple,orange}; // possible content for the boxes
Label={A,O,Both} // labels for the boxes
CONSTANTS a,o,b, // a,o,b are the three boxes
Take, // which box should we open (the label of that box)
DecisionFunction // given the fruit we pick from Take: what are the contents of the boxes labeled A,O,Both
PROPERTIES
a = {apple} & o={orange} & b={apple,orange} // (1)
&
Take : Label //3
&
DecisionFunction : Fruit --> (Label >->> {a,o,b}) & //4
!label. ( // the decision function has to work for all allowed labelings
( label : {a,o,b} >->> Label &
label(a) /= A & label(o) /= O & label(b) /= Both // (2)
)
=>
!f.(f: label~(Take)
=> DecisionFunction(f)=label~ // the function should tell us what is behind label A,O,Both
)
)
END
We have abstracted the box of apples a by the set containing apple. Ditto for o and b, which are abstracted by {orange}</tt} and {apple,orange} respectively.
Note: you need a recent version of ProB 1.5.1-beta3 or newer to load the above model with its one-line comments. If you have an older version of ProB, simply use the normal comments /* ... */.
Loading this model with ProB gives you just one solution (after less than 10 ms):

As we can see, the only solution is to open the box labelled with "Both". We can inspect the decision function by using the B REPL (e.g., double click on the State Properties pane to open it):
>>>> DecisionFunction(apple)
{(A|->{orange}),(O|->{apple,orange}),(Both|->{apple})}
>>>> DecisionFunction(orange)
{(A|->{apple,orange}),(O|->{apple}),(Both|->{orange})}