Skip to main content

Alloy

Past exams exercises

2021 06 24 WE1 Q1 (7 points) Truck Company

Consider a transportation company that is organizing a package pick-up service. The company has a certain number of trucks and drivers. All trucks have the same size. Each day, each driver drives a single truck (the same driver can drive different trucks in different days).

A pick-up request is specified by the origin and the size of the package (for simplicity, assume there are only two sizes, small and large).

A travel plan is associated with a driver and a truck in a certain day and is defined in terms of the packages that must be collected by that driver during the day, using the specified truck.

Point A (2 points)

Define suitable Alloy signatures – and any related constraints – to describe the problem above.

SOLUTION

abstract sig Size {}
one sig Small extends Size {}
one sig Large extends Size {}
sig Place {}
sig Day {}

sig Package {
  origin: Place,
  size: Size
}
sig Driver {}
sig Truck {}

sig TravelPlan {
  day: Day,
  driver: Driver,
  packages: set Package,
  truck: Truck
}

fact packageInAtMostOneTravelPlan {
  all pk: Package, tp1: TravelPlan, tp2: TravelPlan |
    (tp1 != tp2 and pk in tp1.packages) implies pk not in tp2.packages
}

Point B (2 points)

Define a signature TruckStatus that represents the snapshot of a truck, that is, the truck with its current content and current driver. Ensure that the following constraint holds: a truck never exceeds its maximum capacity, which corresponds to an amount of packages whose size is equivalent to 2 large packages. We consider that the size of one large package is equivalent to the size of 4 small packages.

SOLUTION

pred sizePackagesCoherent[ps: set Package] {
  // 0 Large
  (#ps <= 8 and no p: Package | p in ps and p.size = Large) or
  // 1 large
  (#ps <= 5 and one p: Package | p in ps and p.size = Large) or
  // 2 Large
  (#ps <= 2)
}

sig TruckStatus {
  truck: one Truck,
  currentDriver: lone Driver,
  currentContent: set Package
}{sizePackagesCoherent[currentContent]}

Point C (1.5 points)

Formalize the following constraint: a travel plan should never exceed the truck capacity.

SOLUTION

fact noTravelPlanExceedsCapacity {
  all tp: TravelPlan | sizePackagesCoherent[tp.packages]
}

Point D (1.5 points)

Formalize the following constraint: drivers and trucks cannot be assigned to multiple travel plans in the same day.

SOLUTION

fact AtMostOneTralvelPlanPerDayAndDriver {
  all disj tp1, tp2: TravelPlan | (tp1.driver = tp2.driver) => tp1.day != tp2.day
}

fact AtMostOneTralvelPlanPerDayAndTruck {
  all disj tp1, tp2: TravelPlan | (tp1.truck = tp2.truck) => tp1.day != tp2.day
}

2021 02 05 WE1 Q1 (7 points) DBMS

Consider the following figure that describes the status of a replicated and partitioned database management system (DBMS). The figure shows that database tables are deployed on three “nodes”. More specifically, in the example, tables A, B, and C are partitioned and each partition is deployed on a different node (for instance, the whole table A is composed of A’, A’’ and A’’’, where A’, A’’ and A’’’ are sets of disjoint tuples belonging to table A). Table D, instead, is replicated on all subsystems, which means that all its tuples occur in all nodes.

Point A (4 points)

Define in Alloy the signatures to represent the concepts of node, tuple, replicated tables, and partitioned tables, together with any other concept you may need.

SOLUTION

sig Node {}
sig Tuple {}

sig abstract Table {
	tuples : set Tuple
}

sig Partition extends Table 
	node: Node
}
sig PartitionedTable extends Table {
	partitions: some Partition
}

sig Replication extends Table {
	node: Node
}
sig ReplicatedTable extends Table {
	replications: some Replication
}

fact partitionedTableHasAllTuples {
	all pt: PartitionedTable, p: Partition, t: Tuple |
		(p in pt.partitions and t in p.tuples) implies (t in pt.tuples)
	all pt: PartitionedTable, t: Tuple |
		(t in pt.tuples) implies (one p: Partition | p in pt.partitions and t in p.tuples)
}

fact replicationsSameTuples {
	all rt: ReplicatedTable, disj r1, r2: Replication |
    	(r1 in rt.replications and r2 in rt.replications) => (all t: Tuple | (t in r1.tuples <=> t in r2.tuples)
}

Point B (1.5 points)

Define a fact to ensure that each replicated table is deployed on at least two nodes.

SOLUTION

fact replicatedInAtLeatTwoNodes {
	all rt: ReplicatedTable | #rt.replications > 1
	all rt: ReplicatedTable, disj r1, re: Replication |
		(r1 in rt.replications and r2 in rt.replications) implies r1.node != r2.node
}

Point C (1.5 points)

Define a fact to ensure that each partitioned table does not contain tuples that are replicated on multiple nodes.

SOLUTION

fact noDuplicateTuplesInNodes {
	all pt: PartitionedTable, disj p1, p2: Partition |
		p1 in pt.partitions and p2 in pt.partitions and p1.node & p2.node = none
		implies
		p1.tuples & p2.tuples = none
}

2020 06 17 Q1 (7 points) Online exams

We want to develop an integrated system that supports the execution of online exams. Each online exam is handled by one or more instructors, it can be taken by some students, it is associated with a virtual room and with the exam text, plus the answers by the students. The following rules hold:

  1. Only students who registered for the exam can enter the virtual room.
  2. While the exam is running, students in the room must have their camera, mic and screen sharing on, otherwise the system assumes they have exited the room.
  3. If the exam is running or it has ended, students that result to have exited the room cannot enter again

Consider the following Alloy signatures that provide a partial model for the problem at hand:

sig Person {}
sig Instructor extends Person {}
sig Exam {
	instructors: some Instructor,
	students: set Student,
	vr: VirtualRoom,
	test: ExamTest,
	examStatus: EStatus
}
sig Description {}
sig ExamTest {
	description: Description,
	answers: set Student
}
sig EStatus {}
one sig Planned extends EStatus{}
one sig Running extends EStatus{}
one sig Ended extends EStatus{}

Point A (2 points)

Define the concept of Student, who must own some devices (camera, mic and screen sharing). Add all signatures/constraints/facts needed to make the Student concept self-contained and coherent with the description above.

SOLUTION

sig Student extends Person {
	camera: Camera,
    mic: Mic,
    screen: Screen
}
sig abstract DeviceStatus {}
one sig On extends DeviceStatus {}
one sig Off extends DeviceStatus {}
sig abstract Device {
	status: DeviceStatus
}
sig Camera extends Device {}
sig Mic extends Device {}
sig Screen extends Device {}

Point B (1 point)

Define the concept of VirtualRoom that separately captures the students who entered the room at some point, those that are currently in the room, and those that exited the room, in addition to the instructors supervising the room. Add all signatures/constraints/facts you need.

SOLUTION

sig VirtualRomm {
	entered: set Student,
    inside: set Student,
    exited set Student,
    instructors: some Instructor
}{
	inside + exited = entered
    inside & exited = none
}

Point C (1 point)

Define a fact modelling constraint 1) “Only students who registered for the exam can enter the virtual room”.

SOLUTION

fact onlyRegisteredInRoom {
	all e: Exam, vr: VirtualRoom, s: Student |
    	(vr in e.vr and s not in e.students) => (s not in vr.entered)
}

Point D (1 point)

Define a fact modelling constraint 2) “While the exam is running, students in the room must have their camera, mic and screen sharing on, otherwise the system assumes they have exited the room”.

SOLUTION

fact devicesOnInRunningExam {
	all e: Exam, vr: VirtualRoom, s: Student |
    	(e.examStatus=Running and vr=e.vr and s in vr.inside) => (s.mic.status = On and s.camera.status = On and s.screen.status = On)
}

Point E (2 point)

Define a predicate modelling operation letIn that is invoked to let students into the room, and which enforces constraint 3) “If the exam is running or it has ended, students that result to have exited the room cannot enter again. If the exam is planned, they can get in even if they have been out”.

SOLUTION

pred letIn[e, e':  Exam, s: Student] {
	s in e.students
	(e.status = Planned) or (s not in e.vr.entered)
    
    e'.vr.entered = e.vr.entered + s
    e'.vr.inside = e.vr.inside + s
    e'.vr.exited = e.vr.exited - s
    
    e'.instructors = e.instructors
	e'.students = e.students
    e'.test = e.test
	e'.examStatus = e.examStatus
}
Back to top