Naive approach to gilded-rose with alloy

gilded-rose.als

open util/ordering [Time]

sig Time {}

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

pred init(t: Time) {
	all i: Item {
		i.quality.t >= 0 and i.quality.t <= 20
		i.sellIn.t in 5 + 6 + 7 + 8 + 9 + 10
	}
}

pred updateQuality(t, t': Time, i: Item) {
	i in AgedBrie => {
		i.quality.t' = min[plus[i.quality.t, 1] + 20]
	}
	i in BackstagePass => {
		i.sellIn.t >= 4 => i.quality.t' = min[plus[i.quality.t, 1] + 20]
		i.sellIn.t < 4 and i.sellIn.t >= 2 => i.quality.t' = min[plus[i.quality.t, 2] + 20]
		i.sellIn.t < 2 and i.sellIn.t >= 0 => i.quality.t' = min[plus[i.quality.t, 3] + 20]
		i.sellIn.t < 0 => i.quality.t' = 0
	}
	i in Sulfuras => { i.quality.t' = i.quality.t }
	i in Common => {
		i.sellIn.t <= 0
			implies i.quality.t' = max[minus[i.quality.t, 2] + 0]
			else i.quality.t' = max[minus[i.quality.t, 1] + 0]
	}
	not (i in Sulfuras)
		implies i.sellIn.t' = minus[i.sellIn.t, 1]
		else i.sellIn.t' = i.sellIn.t

}

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

run {some AgedBrie} for 8 Int, 6 Time, 1 Item

check neverNegative {
	all t: Time | all i: Item | i.quality.t >= 0
} for 8 Int, 6 Time, 1 Item

check neverOverQuality {
	all t: Time | all i: Item | i.quality.t <= 20
} for 8 Int, 6 Time, 1 Item

check negativeSellInMeansNoQualityForBackstage {
	all t: Time | all i: BackstagePass | i.sellIn.t < 0 => i.quality.t = 0
} for 8 Int, 6 Time, 1 Item