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