vscode-tlaplus icon indicating copy to clipboard operation
vscode-tlaplus copied to clipboard

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

Open lemmy opened this issue 3 years ago • 5 comments

---- 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
====
Screen Shot 2022-03-14 at 10 07 36 PM Screen Shot 2022-03-14 at 10 11 19 PM
------ 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: https://github.com/tlaplus/vscode-tlaplus/issues/61

lemmy avatar Mar 15 '22 05:03 lemmy