Gilded rose with higher level specification

gilded-rose.als

open util/ordering [Time]

sig Time {}

abstract sig Item {
	sellIn: Int one -> Time,
	quality: Quality one -> Time
}
one sig AgedBrie extends Item {}
one sig BackstagePass extends Item {}
one sig Sulfuras extends Item {}
one sig Common extends Item {}

// quality strategies will always keep the value between 0 and 50.
// the specification of quality can be implemented separately.
abstract sig Quality {}
one sig NeverErodes extends Quality {}
one sig Expired extends Quality {}
sig IncreasesBy extends Quality { inc: Int }
sig DecreasesBy extends Quality { dec: Int }


pred init(t: Time) {
	all i: Item {
		i.sellIn.t in 5
	}
}

pred qualityStrategy(t: Time, i: Item) {
	i in AgedBrie => {
		i.quality.t.inc = 1
	}
	i in BackstagePass => {
		i.sellIn.t >= 4 => i.quality.t.inc = 1
		i.sellIn.t < 4 and i.sellIn.t >= 2 => i.quality.t.inc = 2
		i.sellIn.t < 2 and i.sellIn.t >= 0 => i.quality.t.inc = 3
		i.sellIn.t < 0 => i.quality.t = Expired
	}
	i in Sulfuras => { i.quality.t = NeverErodes }
	i in Common => {
		i.sellIn.t <= 0
			implies i.quality.t.dec = 2
			else i.quality.t.dec = 1
	}
}

pred decreaseSellIn(t, t': Time, i: Item) {
	i in Sulfuras
		implies i.sellIn.t' = i.sellIn.t
		else i.sellIn.t' = minus[i.sellIn.t, 1]
}

fact Traces {
	init [first]
	all t: Time | all i: Item | qualityStrategy [t, i]
	all t: Time - last, t': t.next | all i: Item | decreaseSellIn [t, t', i]
}

run {
	some Item
} for 8 Int, 6 Time, 7 Quality