parkingsystem.als

enum ParkingCardType { VIPCard, NormalCard }

sig ParkingCard {
	type: one ParkingCardType
}

sig ManagementSystem {
	Park: set ParkingCard,
} {
	#VIPPark <= 2
	#NormalPark <= 5
}

fun VIPPark[m: ManagementSystem]: set ParkingCard { (m.Park <: type :> VIPCard) . ParkingCardType }
fun NormalPark[m: ManagementSystem]:  set ParkingCard { (m.Park <: type :> NormalCard) . ParkingCardType }

run {} for 7 Int, exactly 1 ManagementSystem, exactly 3 ParkingCard

pred enter[c: ParkingCard, s, s': ManagementSystem] {
	no s.Park & c

	s'.Park = s.Park + c
}

pred leave[c: ParkingCard, s, s': ManagementSystem] {
	one s.Park & c

	s'.Park = s.Park- c
}

run leave for 7 Int, exactly 2 ManagementSystem, exactly 3 ParkingCard