Specify a predicate being true for n steps

Alloy 6
1

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:

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

  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.
2

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).

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

3

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.

4

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.