Hi y’all, I’m pretty new to Alloy 6 and also formal modeling in general. I’m working on a very simple model, basically a linear function that every time step progresses along a slope (simplified in this model) towards a max point. It starts a certain point on the line (position), then takes a step forward each time step until it reaches a the end the (width).
After a bit of toil, I was able to get a basic version of the model working, but it never progresses more than 3 steps, ending up forever looping back to the stutter state.
Here’s the model inline:
abstract sig Bool {}
one sig True, False extends Bool {}
pred isTrue[b: Bool] { b in True }
pred isFalse[b: Bool] { b in False }
// LinearFeeFunction is the abstract model of our fee function. We use lone here
// to indicate that only one of them exists in our model. Our model will use
// time to drive this single instance.
one sig LinearFeeFunction {
// startFeeRate is the starting fee rate of our model.
var startingFeeRate: Int,
// endingFeeRate is the max fee rate we'll be ending out once the deadline
// has been reached.
var endingFeeRate: Int,
// currentFeeRate is the current fee rate we're using to bump the
// transaction.
var currentFeeRate: Int,
// width is the number of blocks between the starting block height and the
// deadline height.
var width: Int,
// position is the number of between the current height and the starting
// height. This is our progress as time passes, we'll increment by a single
// block.
var position: Int,
// deltaFeeRate is the fee rate time step in msat/kw that we'll take each
// time we update our progress (scaled by position). In this simplified model, this will always be 1.
var deltaFeeRate: Int,
var started: Bool,
} {
position >= 0
position <= width
isFalse[started] => position = 0
startingFeeRate > 0
currentFeeRate > 0
endingFeeRate > 0
width > 4
// We'll simplify our model by ensuring that the fee delta is just always one. Alloy doesn't do well with
// arithmetic, so we'll just always step forward by one.
deltaFeeRate = 1
endingFeeRate >= startingFeeRate
startingFeeRate <= currentFeeRate
}
// init is a predicate to initialize the params of the fee function.
pred init[f: LinearFeeFunction, maxFeeRate, startFeeRate: Int, confTarget: Int] {
// We only want to initiate once, so we'll have a guard that only proceeds
// if the values are not set.
isFalse[f.started]
// The starting rate and the ending rate shouldn't be equal to each other.
maxFeeRate != startFeeRate
maxFeeRate > startFeeRate
startFeeRate < 3
// If the conf target is zero, then we'll just jump straight to max params.
confTarget = 0 implies {
f.startingFeeRate' = maxFeeRate
f.endingFeeRate' = maxFeeRate
f.currentFeeRate' = maxFeeRate
f.position' = 0
f.width' = confTarget
f.deltaFeeRate' = 1
f.started' = True
} else {
// Otherwise, we'll be starting from a position that we can use to drive
// forward the system.
confTarget != 0
f.startingFeeRate' = startFeeRate
f.currentFeeRate' = startFeeRate
f.endingFeeRate' = maxFeeRate
f.width' = confTarget
f.position' = 0
// Our delta fee rate is just always 1, we'll take a single step towards the final solution at a time.
f.deltaFeeRate' = 1
f.started' = True
}
}
// increment is a predicate that implements our fee bumping routine.
pred increment[f: LinearFeeFunction] {
// Update our fee rate to take into account our new position. Increase our
// position by one, as a single block has past.
increaseFeeRate[f, f.position.add[1]]
}
// increaseFeeRate takes a new position, and our fee function, then updates
// based on this relationship:
// feeRate = startingFeeRate + position * delta.
// - width: deadlineBlockHeight - startingBlockHeight
// - delta: (endingFeeRate - startingFeeRate) / width
// - position: currentBlockHeight - startingBlockHeight
pred increaseFeeRate[f : LinearFeeFunction, newPosition: Int] {
// Update the position of the model in the next timestep.
f.position' = newPosition
// Ensure that our position hasn't passed our width yet. This is an error
// scenario in the original Go code.
f.position' <= f.width
// Our new position is the distance between the
f.currentFeeRate' = feeRateAtPosition[f, newPosition]
f.startingFeeRate' = f.startingFeeRate
f.endingFeeRate' = f.endingFeeRate
f.started' = f.started
f.width' = f.width
f.deltaFeeRate' = f.deltaFeeRate
}
// feeRateAtPosition computes the new fee rate based on an updated position.
fun feeRateAtPosition[f: LinearFeeFunction, p: Int]: Int {
// If the position is equal to the width, then we'll go straight to the max
// fee rate.
p >= f.width implies f.endingFeeRate
else
// Otherwise, we'll do the fee rate bump.
let deltaRate = f.deltaFeeRate,
newFeeRate = f.currentFeeRate.add[deltaRate] |
// If the new fee rate would exceed the ending rate, then we clamp it
// to our max fee rate. Otherwise we return our normal fee rate.
newFeeRate > f.endingFeeRate => f.endingFeeRate else newFeeRate
}
pred stutter[f: LinearFeeFunction] {
// No change in any of our variables.
f.startingFeeRate' = f.startingFeeRate
f.endingFeeRate' = f.endingFeeRate
f.currentFeeRate' = f.currentFeeRate
f.position' = f.position
f.width' = f.width
f.deltaFeeRate' = f.deltaFeeRate
f.started' = f.started
}
pred max_fee_rate_before_deadline[f: LinearFeeFunction] {
f.position = f.width.sub[1] => f.currentFeeRate = f.endingFeeRate
}
pred fee_bump_step[f: LinearFeeFunction] {
isTrue[f.started]
increment[f]
}
enum Event { Stutter, Init, FeeBump }
fun stutter : set Event -> LinearFeeFunction {
{ e: Stutter, f: LinearFeeFunction | stutter[f] }
}
fun init : Event -> LinearFeeFunction -> Int -> Int -> Int {
{ e: Init, f: LinearFeeFunction, m: Int, s: Int, c: Int | init[f, m, s, c] }
}
fun fee_bump : Event -> LinearFeeFunction {
{ e: FeeBump, f: LinearFeeFunction | fee_bump_step[f] }
}
fun events : set Event {
stutter.LinearFeeFunction + init.Int.Int.Int.LinearFeeFunction + fee_bump.LinearFeeFunction
}
fact traces {
always some events
}
run {
all f: LinearFeeFunction | f.started = False
eventually (some init and after some fee_bump and after some fee_bump)
}
Here’s a sample run in the analyzer. I’m able to get the initial init event off, it does the fee_bump event, but then just continues to loop back to the stutter step.
So my question is: with the simplified model where currentFeeRate only increments by one each time, and there are no further guards for the init event, why does it loop back to the stutter event each time?
