I'm learning CSP now for my research. First time doing formal work in CS. I'm having a hard time understanding the difference between choice $\square$ operator and the nondeterminism $\sqcap$ operator. Does the former perform a completely deterministic choice only based on the inputs from the environment, while the latter can make a nondeterministic choice arbitrarily?
My book says that $(a \rightarrow P) \space \square \space Stop $ is not the same thing as $(a \rightarrow P) \space \sqcap \space Stop $, because the former is the same as $P$, but I don't see how that is if $P$ cannot decide to stop based on an input.