vscode-tlaplus
vscode-tlaplus copied to clipboard
Error-trace shows a bag (multiset) like a sequence
---- 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: https://github.com/tlaplus/vscode-tlaplus/issues/61