Will‘s pick this week is Solving Missionaries and Cannibals Problem with Simulink Design Verifier by Mikhail.

It’s not often I see a File Exchange contribution that involves Simulink Design Verifier and even rarer that I find one with cannibals. Mikhail’s work manages to combine these ideas together into one novel demonstration.

The contribution’s description explains that the Missionaries and Cannibals problem is a classic puzzle in which you must use a boat to shuttle 3 missionaries and 3 cannibals across a river. The goal is to get everyone from one side to the other, but there are some catches. First, the boat can transport no more than 2 people and must always have 1 person on board to operate it. Second, cannibals like to eat missionaries whenever possible. But these missionaries aren’t total pushovers and are only at risk of becoming dinner when outnumbered on one of the riverbanks.

Is it possible to get everyone to the other side without a fatality? Yes, indeed. But rather than manually determining a viable sequence of boat movements, Mikhail relies on Simulink Design Verifier to uncover a solution. He achieves this by creating a model of the problem in Simulink. There are 6 inputs to the model that correspond to a command to move the 6 individuals. If the input equals 0, then that person is to stay put. If the input equals 1, then that person is to board the boat and travel to the other side of the river. There are then a series of checks that ensure that the requested move is valid:

• At least 1 but no more than 2 passengers must be on the boat.
• Passengers must be on the same river bank as the boat.
• Cannibals won’t eat any missionaries if move is taken.

If the move is valid, then the appropriate individuals have their river bank variable updated (a value of 0 corresponding to the original bank and 1 corresponding to the opposite bank).

With the model in place, Design Verifier can be used to find a solution. The image below contains the formal verification component of the model. The Logical Operator block is set to AND, meaning that its output will be true when all 6 inputs are non-zero. Because of the model’s conventions, all 6 inputs being non-zero implies that all 6 people have reached the opposite side of the river. The Logical Operator’s output signal is attached to 2 objective blocks. The “O” block is a Test Objective. Placement of the block here notifies Design Verifier that the modeler wants to find a test case where this signal is true (effectively a test case where everyone reached the other side). The “P” block is a Proof Objective. By setting the value of the block to false, the modeler is telling Design Verifier “I want you to prove that it’s impossible for all six people to reach the other side.”

Design Verifier relies on formal methods to evaluate these objectives. When the tool’s test generation task is run, it creates a test case for you that satisfies the test objective. It does this without running the model and trying a myriad of test cases; the tool can make the determination strictly based on the mathematical constructs of the model itself. Similarly, executing Design Verifier’s property proving task uncovers that the objective specified is not achievable. It creates a counterexample test case that satisfies a situation where everyone reached the other side.

The submission is accompanied by a MATLAB function that runs the test generation task and visualizes the proposed solution move-by-move. I won’t reveal the entire solution, but here are the first three steps.

• The blue line is the river.
• The magenta triangle represents the boat.
• Red squares are the cannibals.
• Green circles are the missionaries.

Comments
Let us know what you think here or leave a comment for Mikhail.