14 02 12

Page 1

Dipartimento di Elettronica e Informazione Politecnico di Milano prof. Elisabetta Di Nitto and Raffaela Mirandola 20133 Milano (Italia) Piazza Leonardo da Vinci, 32 Tel. (39) 02-­2399.3400 Fax (39) 02-­2399.3411 Software Engineering II 14 February 2012 Last Name First Name Id number (Matricola) Note 1. The exam is not valid if you don’t fill in the above data. 2. Write your answers on these pages. Extra sheets will be ignored. You may use a pencil. 3. The use of any electronic apparatus (computer, cell phone, camera, etc.) is strictly forbidden. 4. You cannot keep a copy of the exam w hen you leave the room . 2 Question 1 Alloy (7 points) A company operates a system for sharing electric vehicles. The vehicles can be cars, scooters and electric bicycles. The company provides its users with the charging stations for vehicles, and with a number of vehicles. Each user can either rent a vehicle (only one at a time), or use the charging stations provided by the company to recharge his vehicle. The company handles bookings for both vehicles and charging stations. Define an Alloy model for the above domain. Specifically, define the facts modeling the following constraints: • A vehicle cannot be used by multiple users simultaneously. • A charging station has a finite capacity (defined by the number of electrical outlets available). The number of vehicles using the station cannot exceed this capacity. • A user with a disability cannot use scooters or bicycles. • A vehicle in charge cannot be (at the same time) used by a user. Define the predicate acquireVehicle that, given a vehicle, models its acquisition by a user. Solution one sig Company { stations: set ChargingStation, vehicles: set Vehicle } sig User { ownedVehicles: set Vehicle, usedVehicle: lone Vehicle, disability:…