# 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:** 19\
**Page:** 1

<div class="post-metadata">

**Author:** ![keithb\_b](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/keithb_b/32/7_2.png) [@keithb\_b](https://alloytools.discourse.group/u/keithb_b)\
**Post date:** [September 10, 2020, 4:17pm UTC](https://alloytools.discourse.group/t/util-sequniv-not-valid-electrum/86/1 "2020-09-10T16:17:04Z")

</div>

So, I tried to use `seq` in an Electrum model and it fails to parse because `module util/sequniv` uses primed names. Will this be fixed? What’s the currently recommended work-around?

---

<div class="post-metadata">

**Author:** ![peter.kriens](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/peter.kriens/32/3_2.png) [@peter.kriens](https://alloytools.discourse.group/u/peter.kriens)\
**Post date:** [September 10, 2020, 4:42pm UTC](https://alloytools.discourse.group/t/util-sequniv-not-valid-electrum/86/2 "2020-09-10T16:42:36Z")

</div>

I’ve flagged it as a bug. When Electrum is moved to the Alloy 6 code base it is hopefully fixed. Which I hope will happen soon.

I do not know a workaround at the moment ☹

---

<div class="post-metadata">

**Author:** ![keithb\_b](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/keithb_b/32/7_2.png) [@keithb\_b](https://alloytools.discourse.group/u/keithb_b)\
**Post date:** [September 10, 2020, 4:46pm UTC](https://alloytools.discourse.group/t/util-sequniv-not-valid-electrum/86/3 "2020-09-10T16:46:17Z")

</div>

OK. I’ll live without `seq` for now.

---

<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 10, 2020, 7:24pm UTC](https://alloytools.discourse.group/t/util-sequniv-not-valid-electrum/86/4 "2020-09-10T19:24:33Z")

</div>

It’s fixed in the forthcoming release candidate. We’ll soon make an announcement.

My favorite workaround is to avoid using sequences as much as I can 🙂

If you really need them _now_, you may use the `util/sequence` module I think.

---

<div class="post-metadata">

**Author:** ![peter.kriens](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/peter.kriens/32/3_2.png) [@peter.kriens](https://alloytools.discourse.group/u/peter.kriens)\
**Post date:** [September 11, 2020, 6:59am UTC](https://alloytools.discourse.group/t/util-sequniv-not-valid-electrum/86/5 "2020-09-11T06:59:27Z")

</div>

> [@grayswandyr](#):
>
> My favorite workaround is to avoid using sequences as much as I can 🙂

I also avoid them but that is mostly because they awkward to use. In many of my problems ordering is very important. So how do you solve these type of problems?

---

<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, 8:03am UTC](https://alloytools.discourse.group/t/util-sequniv-not-valid-electrum/86/6 "2020-09-11T08:03:07Z")

</div>

Well there’s no magical wand that would work for all such situations.

As you say, sequences (in the `seq` sense) feel a bit awkward (to me at least) and may be costly in terms of size of the state space.

Therefore I try to put as few constraints as possible on the data that must be ordered. For instance by just declaring the piece of data as a plain field, constrained by a fact that doesn’t impose as much as totally ordered sequences of things. Or by “concretizing” the sequence as two or three fields, which may be deemed enough (depending on the problem at hand) to evaluate whether there are problems in your model (= an abstraction of a problem at hand).

---

<div class="post-metadata">

**Author:** ![keithb\_b](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/keithb_b/32/7_2.png) [@keithb\_b](https://alloytools.discourse.group/u/keithb_b)\
**Post date:** [September 11, 2020, 8:50am UTC](https://alloytools.discourse.group/t/util-sequniv-not-valid-electrum/86/8 "2020-09-11T08:50:13Z")

</div>

No, module `util/sequence[elem]` also uses primed names.

---

<div class="post-metadata">

**Author:** ![keithb\_b](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/keithb_b/32/7_2.png) [@keithb\_b](https://alloytools.discourse.group/u/keithb_b)\
**Post date:** [September 11, 2020, 8:55am UTC](https://alloytools.discourse.group/t/util-sequniv-not-valid-electrum/86/9 "2020-09-11T08:55:32Z")

</div>

So, I’m not using `seq` in a constraint in my model. What I want to do is have the trace of my model be shown in the visualiser. I’d like to do this as a hook for getting the testers at work interested. My first thought was to do something like this:

```
abstract sig Command {
    ,vehicle: one Vehicle
    ,zone: Zone}
sig UnlockCommanded extends Command{
}{
    vehicle.unlockAZone[zone]
}  

sig Script{
    ,futureCommands: seq Command
    ,pastCommands: seq Command
}

pred Script::step{
    !isEmpty[this.futureCommands] =>
            this.futureCommands' = rest[this.futureCommands]
        and add[this.pastCommands, head[this.futureCommands, this.pastCommands']]     
}

```

If there’s another way to make it so that my testers can see what Electrum thinks the trace looks like all at once the I’d love to learn it.

---

<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:13am UTC](https://alloytools.discourse.group/t/util-sequniv-not-valid-electrum/86/10 "2020-09-11T09:13:43Z")

</div>

Yes but, if you really need it, as a workaround, you may copy-paste `sequence` in a new file and replace all primes by `"` (which is an accepted symbol in Alloy). Then you just open the new file. You can’t do this with `seq` as it’s wired in the tool.

---

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

---

<div class="post-metadata">

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

</div>

OK, so I did that, and then

```
sig Script{
    ,futureCommands: Seq
    ,pastCommands: Seq
}

pred Script::step{
    !isEmpty[this.futureCommands] =>
            rest[this.futureCommands, this.futureCommands'] //rest is a pred
        and add[this.pastCommands, first[this.futureCommands], this.pastCommands'] // add is a pred, first is a fun   
}

```

which produces this error

```
Name cannot be resolved; possible incorrect
function/predicate call; perhaps you used ( ) when you
should have used []

This cannot be a correct call to pred sequence/add.
The parameters are
s: {sequence/Seq}
e: {this/Command}
added: {sequence/Seq}
so the arguments cannot be
sequence/inds[s] (type = {sequence/SeqIdx})
Int[1] (type = {Int})

This cannot be a correct call to fun integer/add.
The parameters are
n1: {Int}
n2: {Int}
so the arguments cannot be
sequence/inds[s] (type = {sequence/SeqIdx})
Int[1] (type = {Int})

```

where `sequence\add` is

```
pred add [s: Seq, e: elem, added: Seq] {
  added.startsWith[s]
  added.seqElems[s.afterLastIdx] = e
  #added.inds = #s.inds.add[1]
}

```

I find this deeply perplexing.

---

<div class="post-metadata">

**Author:** ![steve.freeman](https://avatars.discourse-cdn.com/v4/letter/s/2acd7d/32.png) [@steve.freeman](https://alloytools.discourse.group/u/steve.freeman)\
**Post date:** [September 11, 2020, 10:13am UTC](https://alloytools.discourse.group/t/util-sequniv-not-valid-electrum/86/13 "2020-09-11T10:13:35Z")

</div>

This is an interesting discussion. One of the difficulties for outsiders is to understand the appropriateness of each tool.

In this case, is there a way to export the various stages that we can see in the visualiser, rather than trying to record them in the actual model?

---

<div class="post-metadata">

**Author:** ![keithb\_b](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/keithb_b/32/7_2.png) [@keithb\_b](https://alloytools.discourse.group/u/keithb_b)\
**Post date:** [September 11, 2020, 10:13am UTC](https://alloytools.discourse.group/t/util-sequniv-not-valid-electrum/86/14 "2020-09-11T10:13:39Z")

</div>

Ok, so, the problem I think Alloy/Electrum might be able to help me with is some folks at work who struggle to reconstruct their understanding of some tricky real-world behaviour every time they have to do something new with it. They in particular struggle to extend their testing to cover new behaviour. The system in question is the remote-control “zonal locking” on light commercial vehicles.

I am not trying to find defects in the real world system, it is what it is. That said, if we _did_ find something surprising it might lead to a recall on a vehicle manufacturer’s most profitable product, so that would be fun. It _is_ a distributed system, but I’m not looking for tricksy computer science properties of it. Again there might be some surprises hidden away and that would be interesting, but it’s not my near-term goal. And I wouldn’t be able to discuss any such in public anyway.

My near term goal is to record the essential complexity of the real world system in a way that can be demonstrated to be correct and that can aid practitioners in their day-to-day work. And one of the biggest difficulties I see is with testing. So, my thought is to model the behaviour of the remote and the vehicle as described in the vehicle users’ manual (and eventually some other channels that will interact with the vehicle security system, but that are proprietary). And I’d like to be able to show testers how that model can generate test cases for them. There’s no “sequential algorithm”, there’s “sequences of things that a user might try to do”, and I’d like the Visualiser to make visible _those sequences_ as well as allowing someone, for example a tester, to step through the effect on the model.

The sequence of commands that I’d like to be able to see would turn into a test script: user commands this, vehicle _in fact_ does that.

---

<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, 11:51am UTC](https://alloytools.discourse.group/t/util-sequniv-not-valid-electrum/86/15 "2020-09-11T11:51:02Z")

</div>

As a matter of fact, yes (well almost)!

In the new Electrum Visualizer, once you’re satisfied with a trace, you may export it as Electrum code! Go to `File->Export->LTL` and copy the code. Paste it in a fresh run command and you’re done. A caveat: there’s an issue with lines in the export that feature `Int/...`, just delete them and it should be ok.

---

<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, 11:55am UTC](https://alloytools.discourse.group/t/util-sequniv-not-valid-electrum/86/16 "2020-09-11T11:55:27Z")

</div>

Apparently, you have at least a namespace issue: `add` is also defined in module `integer` (which may be opened implicitly… I’m not sure about that). Try using namespace disambiguation by writing `sequence/add` (if your module is called `sequence`).

---

<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, 12:10pm UTC](https://alloytools.discourse.group/t/util-sequniv-not-valid-electrum/86/17 "2020-09-11T12:10:12Z")

</div>

OK. I’m not fully sure to grasp everything but this may be useful: perhaps you don’t need `Script`, `futureCommands` and `pastCommands` at all. IIUC, at every instant, a command is “executed” or execution is over. So if you have a way to know which command is executed at each step, then a trace will necessarily contain, in particular, the list of commands. Would it be enough? If that is so, I can demonstrate our favorite way to do this in a later post.

---

<div class="post-metadata">

**Author:** ![keithb\_b](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/keithb_b/32/7_2.png) [@keithb\_b](https://alloytools.discourse.group/u/keithb_b)\
**Post date:** [September 11, 2020, 12:12pm UTC](https://alloytools.discourse.group/t/util-sequniv-not-valid-electrum/86/18 "2020-09-11T12:12:03Z")

</div>

Ok, this yak will remain unshaven. Thanks.

---

<div class="post-metadata">

**Author:** ![keithb\_b](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/keithb_b/32/7_2.png) [@keithb\_b](https://alloytools.discourse.group/u/keithb_b)\
**Post date:** [September 11, 2020, 12:13pm UTC](https://alloytools.discourse.group/t/util-sequniv-not-valid-electrum/86/19 "2020-09-11T12:13:02Z")

</div>

Yes, that would be enough. A explanation of how to do that would be most welcome.

---

<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 12, 2020, 1:18pm UTC](https://alloytools.discourse.group/t/util-sequniv-not-valid-electrum/86/20 "2020-09-12T13:18:34Z")

</div>

Sorry for the delay.  
So, with what I know, I would represent commands as events. Events are represented as _predicates_. Then, using the [“reified event” idiom](https://alloytools.discourse.group/t/modelling-a-state-machine-in-electrum-towards-alloy-6/88), _occurring events_ will be present in every trace you’ll get. As a matter of fact, they will be the commands you were trying to memorize in the `Script` sig. You may export the trace to retrieve them in a shape amenable to further processing in the context of testing.  
Hope this helps.