This module specifies a system that models the one described in the missionaries and cannibals problem. On 20 December 2018, Wikipedia contained the following description of this problem.
[T]hree missionaries and three cannibals must cross a river using a boat which can carry at most two people, under the constraint that, for both banks, if there are missionaries present on the bank, they cannot be outnumbered by cannibals (if they were, the cannibals would eat the missionaries). The boat cannot cross the river by itself with no people on board.
As explained below, we can use the specification and the TLC model checker to find a solution to the problem.
The following EXTENDS statement imports definitions of the ordinary arithmetic operations on integers and the definition of the Cardinality operator, where Cardinality(S) is the number of elements in S if S is a finite set.