# Specify a predicate being true for n steps

**URL:** <https://alloytools.discourse.group/t/specify-a-predicate-being-true-for-n-steps/388>\
**Category:** Alloy 6\
**Created:** [August 16, 2023, 6:03pm UTC](https://alloytools.discourse.group/t/specify-a-predicate-being-true-for-n-steps/388 "2023-08-16T18:03:02Z")\
**Posts on this page:** 4\
**Page:** 1

<div class="post-metadata">

**Author:** ![ale](https://avatars.discourse-cdn.com/v4/letter/a/f19dbf/32.png) [@ale](https://alloytools.discourse.group/u/ale)\
**Post date:** [August 16, 2023, 6:03pm UTC](https://alloytools.discourse.group/t/specify-a-predicate-being-true-for-n-steps/388/1 "2023-08-16T18:03:02Z")

</div>

Hi all,

I have to model something, and though I have some ideas to do it, maybe someone knows a better way to do it.

Lets say I have the predicate P and I want to specify: P is true in the following (the actual included) n (3, for instance) steps.

A straightforward way could be:  
P;P;P

The thing is I want something more general.

To generalize a little, I think something like this could be done:

> **activate a pred for 3 steps code**
>
> ```auto
> one sig STEPS_COUNTER { }
> lone sig Three_steps in STEPS_COUNTER {}
> 
> pred activate_three_steps_counter {
> COUNTER not in Three_steps;COUNTER not in Three_steps;COUNTER not in Three_steps;COUNTER in Three_steps;
> }
> 
> pred three_steps_happened {
> COUNTER in Three_steps
> }
> 
> pred P_is_true_three_steps {
> activate_three_steps_counter
> P until three_steps_happened
> }
> 
> ```

Now is ‘easy’ to specify predicate P (or any other) to be true for three steps.  
But we have 2 problems, at least:

1. we can’t specify simultaneously more than one predicate if they start at different steps and they intersect in the steps they must be activated.
2. we’re attached to 3 steps.

An idea to solve 2) is:

> **activate a pred for n steps code**
>
> ```auto
> let unchanged[r] { (r)' = (r) } 
> 
> one var sig STEPS_COUNTER {
> var actual: one Int,
> var goal: one Int,
> }
> 
> pred start_counter[set_goal: one Int] {
> let counter = STEPS_COUNTER {
> set_goal > 1
> counter.actual = 1
> counter.goal = set_goal
> unchanged[counter.goal]
> }
> }
> 
> pred steps_counter_incrementer {
> let counter = STEPS_COUNTER {
> counter.actual != counter.goal implies counter.actual' = counter.actual.plus[1]
> }
> }
> 
> fact counter_config {
> let counter = STEPS_COUNTER {
> always steps_counter_incrementer
> always (counter.actual != 1 implies unchanged[counter.goal])
> }
> }
> 
> pred step_reached {
> let counter = STEPS_COUNTER {
> counter.goal = counter.actual
> }
> }
> 
> pred activate_P_5_steps {
> start_counter[5]
> P until step_reached
> }
> 
> ```

And, lastly, to solve 1):

> **activate preds for n steps code**
>
> ```auto
> let unchanged[r] { (r)' = (r) } 
> 
> sig STEPS_COUNTER {
> var actual: one Int,
> var goal: one Int,
> }
> 
> one sig COUNTERS {
> var off: set STEPS_COUNTER,
> var on: set STEPS_COUNTER
> } {
> disj[off, on]
> off + on = STEPS_COUNTER
> }
> 
> pred start_counter[counter: STEPS_COUNTER, set_goal: one Int] {
> set_goal > 1
> counter in COUNTERS.on
> counter.actual = 1
> counter.goal = set_goal
> }
> 
> pred steps_counter_incrementer {
> all counter: COUNTERS.on {
> counter.actual != counter.goal
> implies (counter.actual' = counter.actual.plus[1] and counter in COUNTERS.on')
> else counter in COUNTERS.off'
> }
> }
> 
> fact counter_config {
> STEPS_COUNTER = COUNTERS.off
> 
> always steps_counter_incrementer
> 
> always (all counter: COUNTERS.on |
> (unchanged[counter.goal]))
> 
> }
> 
> pred step_reached[counter: STEPS_COUNTER] {
> counter.goal = counter.actual
> }
> 
> pred activate_P_5_steps {
> some counter: STEPS_COUNTER {
> before counter in COUNTERS.off
> start_counter[counter, 5]
> P until step_reached[counter]
> }
> }
> 
> pred activate_Q_6_steps {
> some counter: STEPS_COUNTER {
> before counter in COUNTERS.off
> start_counter[counter, 6]
> Q until step_reached[counter]
> }
> }
> 
> ```

For this last one the problems I see are:

1. Is not possible to start a STEPS\_COUNTER on initial step.
2. STEPS\_COUNTERs could go on without being requested, anyway it doesn’t seem a big problem. What I need is started’s STEPS\_COUNTERs behave correctly, and they should.
3. It needs at most n STEPS\_COUNTER atoms if n predicates are simultaneously requested to be activated, which would be a problem if n is high.
4. For me, the worst one: too much code.

I would be glad to hear any recommendation/improvement!

Thanks!

> **P.S.**
>
> Later of writing this I had the idea to define some field to know at which step we are (an int with 0 as initial value and increment it by 1 in each step). And activate P until the field equals the actual value + n.  
> While this seems to simplify everything a lot and require so little code I ran into two problems:
> 
> 1. Since Alloy always gives instances which are lasso traces the counter must me able to go to its initial (or some previous) state eventually.
> 2. I didn’t get how to specify at which value of the counter the pred must be released. For instance:  
> `P until step.counter = step.counter.add[5]` but that will never be true.

---

<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:** [August 17, 2023, 6:00pm UTC](https://alloytools.discourse.group/t/specify-a-predicate-being-true-for-n-steps/388/2 "2023-08-17T18:00:24Z")

</div>

Hi,

I think you can get rid of the `COUNTERS` sig by making `STEPS_COUNTER` mutable. I’m not entirely sure if what I did is correct but here is my attempt at simplifying your model (and also works for the first state).

```plaintext
let unchanged[r] { (r)' = (r) } 

var sig STEPS_COUNTER {
  var actual: one Int,
  var goal: one Int,
}

pred start_counter[counter: STEPS_COUNTER, set_goal: one Int] {
  set_goal > 1
  counter.actual' = 2
  counter.goal' = set_goal
}

pred steps_counter_incrementer {
  all counter: STEPS_COUNTER {
    counter.actual != counter.goal
      implies (counter.actual' = counter.actual.plus[1] and unchanged[counter.goal] and counter in STEPS_COUNTER')
      else (counter not in STEPS_COUNTER')
  }
}

fact counter_config {
  always steps_counter_incrementer
}

pred step_reached[counter: STEPS_COUNTER] {
  counter in STEPS_COUNTER
  counter.goal = counter.actual
}

var lone sig P {}
var lone sig Q {}

pred P { some P }
pred Q { some Q }

pred activate_P_5_steps {
  some counter: STEPS_COUNTER' - STEPS_COUNTER {
    start_counter[counter, 5]
    step_reached[counter] releases P
  }
}

pred activate_Q_6_steps {
  some counter: STEPS_COUNTER' - STEPS_COUNTER {
    start_counter[counter, 6]
    step_reached[counter] releases Q
  }
}

check {
	always (activate_P_5_steps implies (P;P;P;P;P))
	always (activate_Q_6_steps implies (Q;Q;Q;Q;Q;Q))
} for 3 but 20 steps

```

Best,  
Alcino

---

<div class="post-metadata">

**Author:** ![ale](https://avatars.discourse-cdn.com/v4/letter/a/f19dbf/32.png) [@ale](https://alloytools.discourse.group/u/ale)\
**Post date:** [August 18, 2023, 12:01pm UTC](https://alloytools.discourse.group/t/specify-a-predicate-being-true-for-n-steps/388/3 "2023-08-18T12:01:23Z")

</div>

Hi @alcino,

Thank you so much for your answer!

I like so much the improvements you did! Awesome!

One question, did you use ‘some’ for some reason in activate\_\* predicates?  
I would think of using ‘one’.

Regards,  
Ale.

---

<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:** [August 18, 2023, 2:21pm UTC](https://alloytools.discourse.group/t/specify-a-predicate-being-true-for-n-steps/388/4 "2023-08-18T14:21:10Z")

</div>

> [@ale](#):
>
> One question, did you use ‘some’ for some reason in activate\_\* predicates?  
> I would think of using ‘one’.

The semantics of the `one` quantifier is tricky - I must confess I almost never use it. In this case it is irrelevant if there is more than one counter that can do the job, so `some` is ok.