CSC2021 Software Engineering Coursework February 2017 Modelling Exercise: The Farmer and the River Crossing Issued: 21 Feb 2017 Due: 16:00, Fri 17th March 2017 Submission: via Ness This coursework provides practice with a variety of modelling techniques in VDM-SL. The coursework is marked out of 16: it is worth 16% of the module mark for CSC2021. The remaining 4% of the assessment comes from completing the Overture tutorials. Answers will be assessed and given a mark up to the maximum mark shown for each question. Marks will be given for technical correctness and clarity of explanations. 1 Tasks Download the project Crossing.zip from Blackboard and import it into Overture in the usual way. Consult Tutorial 1 if you need a reminder for this step. Answer the following questions by making modifications to the specification file. Annotate your specification by adding comments to explain your answer: comments are signified with -- two dashes for a single line comment, or /* a multiline comment is indicated between begin-end markers as shown here */ Please submit through Ness your annotated crossing.vdmsl file, containing your completed specification, and output crossing-run.txt file (produced in Question 3). 1Scenario: The Farmer and the River Crossing This coursework is based on an old puzzle involving a farmer, a wolf, a goat, a cabbage, a river and a boat. The farmer is travelling with three valuable items: a cabbage, a goat, and a wolf. While the farmer is with these items, they are safe - but if wolf and goat are left alone, the wolf will eat the goat; and if the goat and the cabbage are left alone, the goat will eat the cabbage. The wolf is a strict carnivore and will not eat the cabbage. This unusual party comes to a river which must be crossed (from left bank to right bank), and the only way to do this is using a small boat conveniently found on the left bank of the river. The boat can take no more than 2 items - and since the farmer must row the boat, this means that the farmer can take only one item at a time in the boat across the river. So, the puzzle is to get the farmer and all 3 items across the river in one piece: • To begin with, the farmer, the boat and all the items are on the left side of the river. • At the end, the farmer, boat and all items are on the right side of the river. • The boat can fit a maximum of 2 items, one of whom must be the farmer. • The wolf can never be left alone with the goat. • The goat can never be left alone with the cabbage. This is a classic puzzle with well-documented solutions: a standard one can be found at https://illuminations.nctm.org/BrainTeasers.aspx?id=4992. The aim of this coursework is not to find the solution: instead it is to model the problem. In the next section an initial version of the model is presented. 2 The Basic Model The following types have been identified: ✞ types Passenger = |||; Bank = |; Place = set of Passenger; ✡ ✝ ✆ The Passenger enumerated type represents the different items that can be transported. The Bank enumerated type will tell us which side the boat is currently on, and a Place represents the places that Passengers may be gathered. 2The crossing itself is represented as the persistent state of the model: ✞ state Crossing of leftBank : Place rightBank : Place boatPos : Bank inv cr == true -- invariant to be added here: replace true with your invariant init cr == cr = mk_Crossing({,,,},{},) end ✡ ✝ ✆ The init clause gives the initial state for the model by giving the values of the leftBank, rightBank and boatPos variables. Initially leftBank is a set of all the Passengers, rightBank is the empty set, and boatPos is the left bank. The following will be required in order to complete the model: 1. A state invariant to ensure that wolf and goat, and goat and cabbage, are never left alone on the left or right banks 2. Operations to modify the state, by moving a set of Passengers (including the Farmer) from left bank to right bank or from right bank to left bank, without breaking the state invariant. 3. A Run() operation to simulate the execution of the model and output the change in state after each move 3 Questions Answer the following questions in your specification file, adding any necessary explanatory text as comments. Question 1: State invariant The state invariant must ensure that at all times: • Neither the left bank nor the right bank has a dangerous pairing of passengers, as specified above • Passengers are on either the left bank or the right bank, but not both. Add an invariant to the state to represent this constraint, by replacing ”true” in the state invariant with your invariant. You may find it helpful to write one or more boolean auxiliary functions to break down the invariant (see the Traffic Light Kernel case study in the lecture notes). [6] 3Question 2: Crossing the River Model the moving of passengers from one side of the river to the other, by writing two operations: ✞ operations CrossRight: set of Passenger ==> () CrossRight(passengers) == is not yet specified; CrossLeft: set of Passenger ==> () CrossLeft(passengers) == is not yet specified; ✡ ✝ ✆ Complete the operation definition by replacing ”is not yet specified” with a sequence of statements modifying the state variables leftBank,rightBank and boatPos. Ensure that you have taken account of the need to maintain the state invariant by adding preconditions to the operations. Remember also that a maximum of 2 passengers can cross, and one of the passengers must be the farmer. [6] Question 3: Run operation Add a Run() operation to the model: ✞ Run: () ==> () Run() == ( fopen(); -- open output file, overwriting current contents -- complete this operation by adding a sequence of steps to solve the puzzle -- solution can be found at -- https://illuminations.nctm.org/BrainTeasers.aspx?id=4992 ); ✡ ✝ ✆ The Run() operation will take the model from its initial state to the final (solution) state by a series of calls to the CrossRight and CrossLeft operations. After each operation call, use the provided fprint and toString operations to output the state to an output file (in the same way as in the tutorials). You can also use the operation fprintState() to print the current Crossing state. For example, the Run() operation could begin: ✞ Run: () ==> () Run() == ( fopen(); fprintln("Start of run"); fprintState(); CrossRight({,}); 4fprintln("Farmer crosses right with goat"); fprintState(); CrossLeft({}); fprintln("Farmer returns alone"); fprintState(); -- etc ✡ ✝ ✆ [4] Submission. Submit your updated crossing.vdmsl file and crossing-run.txt output file to Ness by the deadline. 5