# Simple Linear Function Model - not progressing with time

**URL:** <https://alloytools.discourse.group/t/simple-linear-function-model-not-progressing-with-time/467>\
**Category:** Questions\
**Created:** [May 14, 2024, 6:25pm UTC](https://alloytools.discourse.group/t/simple-linear-function-model-not-progressing-with-time/467 "2024-05-14T18:25:34Z")\
**Posts on this page:** 6\
**Page:** 1

<div class="post-metadata">

**Author:** ![roasbeef](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/roasbeef/32/233_2.png) [@roasbeef](https://alloytools.discourse.group/u/roasbeef)\
**Post date:** [May 14, 2024, 6:25pm UTC](https://alloytools.discourse.group/t/simple-linear-function-model-not-progressing-with-time/467/1 "2024-05-14T18:25:34Z")

</div>

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:

```auto
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.

 ![Screenshot 2024-05-14 at 11.26.11 AM](https://global.discourse-cdn.com/free1/uploads/alloytools/original/1X/a65e2a491928bfe5fb40feabdbc1af447e54b43f.png)

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?

---

<div class="post-metadata">

**Author:** ![peter.kriens](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/peter.kriens/32/3_2.png) [@peter.kriens](https://alloytools.discourse.group/u/peter.kriens)\
**Post date:** [May 15, 2024, 8:48am UTC](https://alloytools.discourse.group/t/simple-linear-function-model-not-progressing-with-time/467/2 "2024-05-15T08:48:45Z")

</div>

There are only 16 integers by default, -8…+7.

To increase the number of integers (and the time to find a solution of your model), you can extend the `run` scope.

```auto
run {
   all f: LinearFeeFunction | f.started = False
   eventually (some init and after some fee_bump and after some fee_bump)
} for 6 but 8 int

```

8 is the bitwidth used for integers, `8 int` gives 2^8=256 integers, from -128…127. The model is encoded in a boolean expression for a SAT solvers. This requires all integers to be encoded as boolean expressions, greatly increasing the complexity of finding the solution.

---

<div class="post-metadata">

**Author:** ![roasbeef](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/roasbeef/32/233_2.png) [@roasbeef](https://alloytools.discourse.group/u/roasbeef)\
**Post date:** [May 16, 2024, 10:56pm UTC](https://alloytools.discourse.group/t/simple-linear-function-model-not-progressing-with-time/467/3 "2024-05-16T22:56:44Z")

</div>

Hi @peter.kriens, thanks for replying!

My initial model had a bit more arithmetic, but eventually I found the documentation pertaining to constraints of integer size. After I internalized this, I simplified the model to just increment by one each time. Based on my current understanding, I don’t think the current model is limited by integer bitwidth.

Here’s a simple model that still captures the essence of what I’m trying to model. We have a simple counter with a starting value of zero. Each time step we can increment the counter by one until it equals four.

```auto
abstract sig Bool {}

one sig True, False extends Bool {}

pred isTrue[b: Bool] { b in True }

pred isFalse[b: Bool] { b in False }

one sig Counter {
   var count: Int,

   var started: Bool,
}

pred init[c: Counter] {
  isFalse[c.started]
  
  c.count' = 0
  c.started' = True
}

pred increment[c: Counter] {
  isTrue[c.started]
  c.count < 5
 
  c.count' = c.count.add[1]

  c.started' = c.started
}

pred stutter[c: Counter] {
   c.count' = c.count
   c.started' = c.started
}

enum Event { Stutter, Init, Increment }

fun stutter : set Event -> Counter {
  { e: Stutter, c: Counter | stutter[c] }
}

fun init : Event -> Counter {
  { e: Init, c: Counter | init[c] }
}

fun increment : Event -> Counter {
  { e: Increment, c: Counter | increment[c] }
}

fun events : set Event {
  stutter.Counter + init.Counter + increment.Counter
}

fact traces {
  always some events
}

run {
   all c: Counter | c.started = False
   eventually (some init and after some increment and after some increment)
} for 6 but 8 int

```

Similar to my original model, a solution is never found that involved more than one increment step (the counter never exceeds zero):

 ![Screenshot 2024-05-16 at 3.54.41 PM](https://global.discourse-cdn.com/free1/uploads/alloytools/original/1X/477b1a23a202980e6a4a7bbdd4f9ea28ba30fe1a.png)

What I don’t understand is what prevents the model from advancing in the state space, beyond a single `increment` event. The analyzer never finds an instance with more than 3 steps (init, increment, stutter).

---

<div class="post-metadata">

**Author:** ![roasbeef](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/roasbeef/32/233_2.png) [@roasbeef](https://alloytools.discourse.group/u/roasbeef)\
**Post date:** [May 16, 2024, 11:40pm UTC](https://alloytools.discourse.group/t/simple-linear-function-model-not-progressing-with-time/467/4 "2024-05-16T23:40:27Z")

</div>

Hehe, I may have just answered my own question!

With the simplified model, I can for the state space to advance further by clicking “new fork” in the analyzer. After advancing a few times, I arrive at my desired state of the max counter value (4):

 ![Screenshot 2024-05-16 at 4.40.18 PM](https://global.discourse-cdn.com/free1/uploads/alloytools/original/1X/2603db0ba315043aac1073aae5bae71f704f8d97.png)

However this doesn’t work with the original `LinearFeeFunction` model for some reason. I get that there are no more satisfying instances.

---

<div class="post-metadata">

**Author:** ![alcino](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/alcino/32/25_2.png) [@alcino](https://alloytools.discourse.group/u/alcino)\
**Post date:** [May 17, 2024, 6:59am UTC](https://alloytools.discourse.group/t/simple-linear-function-model-not-progressing-with-time/467/5 "2024-05-17T06:59:03Z")

</div>

Hi,

Btw, this formula is not constraining the trace to have two increment steps because `after` has higher priority than `and`.

> [@roasbeef](#):
>
> `eventually (some init and after some increment and after some increment)`

Either you add some parenthesis

```alloy
eventually (some init and after (some increment and after some increment))

```

or use the semi-colon operator that is is equivalent to `and after` but is right associative.

```alloy
eventually (some init; some increment; some increment)

```

Best,  
Alcino

---

<div class="post-metadata">

**Author:** ![alcino](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/alcino/32/25_2.png) [@alcino](https://alloytools.discourse.group/u/alcino)\
**Post date:** [May 17, 2024, 7:02am UTC](https://alloytools.discourse.group/t/simple-linear-function-model-not-progressing-with-time/467/6 "2024-05-17T07:02:22Z")

</div>

Hi again,

> [@roasbeef](#):
>
> However this doesn’t work with the original `LinearFeeFunction` model for some reason. I get that there are no more satisfying instances.

I tried your original model and it works for me - I can fork in the last transition and get another `fee_bump` instead of `stutter`.

Alcino