Error-trace shows a bag (multiset) like a sequence

[lemmy]

---- MODULE Braf ----
EXTENDS Bags, Naturals

VARIABLE x, y

Init ==
    /\ x = [ k \in {<<"a", "b">>, <<"b", "c">>} |-> 1 ]
    /\ y = 1

Next ==
    /\ UNCHANGED x
    /\ y' = y + 1

Inv ==
    y < 2

====
---- CONFIG Braf ----
INIT Init
NEXT Next
INVARIANT Inv
====

---

------ MODULE Traces -----

EXTENDS Naturals

VARIABLES x

Init ==
    x = 0

Next ==
    x' = 1

Inv ==
    x = 0

Alias ==
    [
        x |-> x
        , seq |-> <<4,5,6>>
        , seq2 |-> << <<4,5>>, <<5,6>>, <<6,7>> >>
        , s2f |-> << [ s \in {"d","c"} |-> <<s, "c">>], [ s \in {"e","f"} |-> 42] >>
        , fun |-> [ i \in 0..2 |-> i * 2 * x]
        , fn2f |-> [ i \in 0..2 |-> [ j \in 0..2 |-> j * i * 2 * x]]
        , s2n |-> [ s \in {"a","b"} |-> 42]
        , f2s |-> [ s \in {"a","b"} |-> <<s, "c">>]
        , f2f |-> [ s \in {"a","b"} |-> [ i \in {3,5,7} |-> i * 2]]
        , seq2n |-> [ k \in {<<"a", "b">>, <<"b", "c">>} |-> 23 ]
        , seq2s |-> [ k \in { {8,9}, {10,11}} |-> "ab" ]

        , seq2f |-> [ k \in { [{"a","b"} -> {TRUE}]} |-> "ab" ]
        , seq2f2 |-> [ k \in [{"a","b"} -> {TRUE, FALSE}] |-><< "ab", "de">> ]
    ]

=======
----- CONFIG Traces -----
INIT Init
NEXT Next
ALIAS Alias
INVARIANT Inv
======

Previous fix: #61

[lemmy]

I ran out of time! Any takers to update/refactor the now-removed tests in 1d9161c#diff-5ad2ff4a54440bf2b50b351c7d6092744831ab604bc4f3cbbda8757029a50b1b?

[lemmy]

The extension has only limited support for TLA+ functions, i.e., the domain (ValueKey) of its StructureValue can only be string or numeric. However, the domain may be any value in TLA+.

[lemmy]

It's impossible to see which elements have been added with bags:

@afonsonf Would it be possible to highlight the added elements of a set in addition to adding the "A" label?

[FedericoPonzi]

This seems fixed in the latest version:

Or is anything else missing?

I derived the Acceptance Criteria to be: It should be clear what item was added to the Bag.
From the screenshot above, the item has an A near it, so I think the AC checks out.

[lemmy]

Here's a screenshot of the same trace in both IDEs. If I recall correctly, Toolbox does a better job of highlighting added, removed, or modified values within deeply nested structures. However, I don't have time to reproduce that scenario right now. There may be existing Toolbox tests that cover this functionality.