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

```
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:

- 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.
- we’re attached to 3 steps.

An idea to solve 2) is:

## activate a pred for n steps code

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

```
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:

- Is not possible to start a STEPS_COUNTER on initial step.
- 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.
- 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.
- 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:

- Since Alloy always gives instances which are lasso traces the counter must me able to go to its initial (or some previous) state eventually.
- 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.