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?