# Learning temporal alloy - how to vary subsets correctly?

**URL:** <https://alloytools.discourse.group/t/learning-temporal-alloy-how-to-vary-subsets-correctly/293>\
**Category:** Questions\
**Created:** [October 19, 2022, 9:20pm UTC](https://alloytools.discourse.group/t/learning-temporal-alloy-how-to-vary-subsets-correctly/293 "2022-10-19T21:20:46Z")\
**Posts on this page:** 3\
**Page:** 1

<div class="post-metadata">

**Author:** ![brianhicks](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/brianhicks/32/5_2.png) [@brianhicks](https://alloytools.discourse.group/u/brianhicks)\
**Post date:** [October 19, 2022, 9:20pm UTC](https://alloytools.discourse.group/t/learning-temporal-alloy-how-to-vary-subsets-correctly/293/1 "2022-10-19T21:20:46Z")

</div>

Following [the advice in @hwayne’s Alloy documentation](https://alloy.readthedocs.io/en/latest/techniques/boolean-fields.html), I’m modeling a light turning on and off like this:

```auto
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 `sig`s 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:

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

---

<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:** [October 20, 2022, 5:58am UTC](https://alloytools.discourse.group/t/learning-temporal-alloy-how-to-vary-subsets-correctly/293/2 "2022-10-20T05:58:58Z")

</div>

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

---

<div class="post-metadata">

**Author:** ![brianhicks](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/brianhicks/32/5_2.png) [@brianhicks](https://alloytools.discourse.group/u/brianhicks)\
**Post date:** [October 20, 2022, 10:13am UTC](https://alloytools.discourse.group/t/learning-temporal-alloy-how-to-vary-subsets-correctly/293/3 "2022-10-20T10:13:40Z")

</div>

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