# Util/sequniv not valid Electrum

**URL:** <https://alloytools.discourse.group/t/util-sequniv-not-valid-electrum/86>\
**Category:** Alloy 6\
**Created:** [September 10, 2020, 4:17pm UTC](https://alloytools.discourse.group/t/util-sequniv-not-valid-electrum/86 "2020-09-10T16:17:04Z")\
**Posts on this page:** 1\
**Showing post:** 11

<div class="post-metadata">

**Author:** ![grayswandyr](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/grayswandyr/32/17_2.png) [@grayswandyr](https://alloytools.discourse.group/u/grayswandyr)\
**Post date:** [September 11, 2020, 9:50am UTC](https://alloytools.discourse.group/t/util-sequniv-not-valid-electrum/86/11 "2020-09-11T09:50:54Z")

</div>

IIUC, you’d like to say you have a sequence of commands to execute in order, and once a command is executed, you keep it in a list of past commands (is there a reason for this).

As it is, the model does not feature any `var` field or sig so no mutation may happen, anyway…

Also the `add` part seems bogus to me, shouldn’t it be `this.pastCommands' = (this.pastCommands).insert(0, head[this.futureCommand]))`?

Also you’re not saying that nothing happens if the list of future commands _is_ empty. So anything may happen.

But I’m not sure to see what you want to _demonstrate_? Here, the Visualizer could show commands going from one sequence to the other but is it compelling enough? I’m certainly biased but, to me, the interest of Alloy or Electrum is not to simulate the execution of sequential algorithms: encoding loops is tedious, and the fact that -in Electrum- you only have [infinite traces](https://alloytools.discourse.group/t/pluscal-in-alloy/59/15) hinders reasoning about normal or abnormal termination. If indeed you want to run sequential algorithms, I would rather use another tool…

In my opinion, Electrum really shines when your model is likely to have unexpected (to you) behaviors, and you expect the Visualizer to show them. Or when you want to check some non trivial property of a concurrent or distributed system. For plain Alloy, the same can be said when you want to assess structural designs, or check some invariants, or do some temporal reasoning that does not fit in the linear-time view enforced by Electrum.

---

_[View the full topic](https://alloytools.discourse.group/t/util-sequniv-not-valid-electrum/86)._
