22c:181 Formal Methods in Software Engineering Fall 2013 Mini Project 1 Due: Tuesday, October 15, by 7pm This mini-project can be done in teams of up to 2 people. Each student is responsible for contacting other students and form a team. Individual submissions are accepted but not encouraged. In particular, no reduction of work will be granted to them. The grade for the assignment will be given on an individual basis. For team submissions, both students must also submit an evaluation (on a form provided by the instructor) of how well they and their teammate performed as team members. Each evaluation is condential and will be incorporated in the calculation of the grade. The Setting You are going to develop an Alloy model for a classic planning domain in Articial Intelligence: the Blocks World. Everything you need to know about this domain to complete this project is provided below. In this project, the only predened Alloy module you can use is the util/ordering module. The Blocks World We have a number of children’s blocks of various colors on a table. The blocks have the same size and can be stacked on top of each other. Each of them has one of the following colors: blue, green, red, yellow and white. We have a one-armed robot that is able to pick a block from one location and move to another location. The only possible locations are the table or the top of another block. The purpose of the robot is to arrange the blocks in some goal conguration (e.g., all stacked in a single stack; stacked together by color; in a specic stack with a red block on top of a green one on top of a blue one; and so on.) The following physical constraints limit what the robot can do. The robot can pick and hold only one block at a time. It is not possible to place more than one block directly on another. Every block is on something, the table or another block. 1
Part A: Static Modeling Write a static Alloy model for this world that models the Blocks world described above but without the…