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
}
Back to top