Learning temporal alloy - how to vary subsets correctly?

Questions
1

Following the advice in @hwayne’s Alloy documentation, I’m modeling a light turning on and off like this:

sig Circuit {}
sig ClosedCircuit extends Circuit {}

pred turnOn[c: Circuit] {
  c in ClosedCircuit
}

Now I want to see that happening over time, so I’m making both sigs varying, like this, and throwing in some initialization and frame conditions. Just to see the system work, I want to say “eventually it should be possible for these all to be on at once.”

I’m modeling that like this:

var sig Circuit {}
var sig ClosedCircuit extends Circuit {}

pred init {
  some Circuit
  no ClosedCircuit
}

pred stutter {
  Circuit' = Circuit
  ClosedCircuit' = ClosedCircuit
}

pred turnOn[c: Circuit] {
  c not in ClosedCircuit
  ClosedCircuit' = ClosedCircuit + c

  // frame
  Circuit' = Circuit
}

fact traces {
  init
  always {
    stutter
    or (one c: Circuit | turnOn[c])
  }
}

run traces {
  eventually Circuit = ClosedCircuit
}

But when I ask for that to be evaluated, I get an inconsistent predicate. Plus, MiniSat says that basically everything in here conflicts. I don’t understand how!

What I think I’m asking it:

  • init: give me a world where there exist some non-closed circuits
  • stutter: nothing about the world changes
  • turnOn: given a circuit that’s off, turn it on

What am I missing, here?

2

Hi,

You should use a variable subset signature instead of a variable extension. If you replace extends by in it should work. Also, since Circuit never changes you don’t need to declare it as variable (nor the respective frame conditions).

The variable extension signature does not work because atoms cannot change their type. With extends the atoms in ClosedCircuit can vary, but they cannot become part of Circuit-ClosedCircuit, nor the atoms in Circuit-ClosedCircuit can become part of Circuit. With subset signatures, since they are not types, we don’t have this restriction.

Best,
Alcino

3

Excellent. Thank you so much! I guess I’m gonna have to go review the difference here to understand it well, but that solved my problem. :+1: