----- MODULE Foo -----
EXTENDS Naturals
CONSTANT C
VARIABLE v
vars == v
Init == v = 0
Next == v' \in C
Spec == Init /\ [][Next]_v
=====
We may check that module Bar refines Foo with:
----- MODULE Bar ------
EXTENDS Naturals
VARIABLE v
S == {0, 42}
Spec == v = 0 /\ [][v' \in S]_v
F1 == INSTANCE Foo WITH C <- S
THEOREM A == Spec => F1!Spec
THEOREM B == Spec => F1!Init /\ [][F1!Next]_F1!vars
F2(c) == INSTANCE Foo WITH C <- c
THEOREM C == Spec => F2(S)!Spec
THEOREM D == Spec => F2(S)!Init /\ [][F2(S)!Next]_F2(S)!vars \* TLAPS doesn't like F2(S)!vars
=====
SANY accept A, B, C, and D just fine, but TLAPS' parser reports a syntax error for D:
-> % ~/.opam/5.1.0/bin/tlapm --version
6acb3cb
-> % ~/.opam/5.1.0/bin/tlapm Bar.tla
File "./Bar.tla", line 16, character 53
Unexpected (
File "<unknown>":
Error: Could not parse "./Bar.tla" successfully.
tlapm ending abnormally with Failure("Module.Parser.parse_file")
Raised at Stdlib.failwith in file "stdlib.ml", line 29, characters 17-33
Called from Tlapm_lib__M_save.clocking in file "src/module/m_save.ml", line 24, characters 18-22
Called from Tlapm_lib.read_new_modules.(fun) in file "src/tlapm_lib.ml", line 503, characters 8-57
Called from Stdlib__List.fold_left in file "list.ml", line 123, characters 24-34
Called from Tlapm_lib.main in file "src/tlapm_lib.ml", line 561, characters 20-43
Called from Tlapm_lib.init in file "src/tlapm_lib.ml", line 589, characters 8-33
-> % tlapm --version
1.5.0
-> % tlapm Bar.tla
File "./Bar.tla", line 16, character 53
Unexpected (
File "<unknown>":
Error: Could not parse "./Bar.tla" successfully.
tlapm ending abnormally with Failure("Module.Parser.parse_file")
Raised at Stdlib.failwith in file "stdlib.ml", line 29, characters 17-33
Called from M_save.clocking in file "m_save.ml", line 25, characters 16-20
Called from Tlapm.read_new_modules.(fun) in file "tlapm.ml", line 455, characters 8-112
Called from Stdlib__list.fold_left in file "list.ml", line 121, characters 24-34
Called from Tlapm.main in file "tlapm.ml", line 490, characters 20-43
Called from Tlapm.init in file "tlapm.ml", line 518, characters 8-33
(We recently added better support for parameterized refinement in TLC: https://github.com/tlaplus/tlaplus/issues/687)
We may check that module
Bar
refinesFoo
with:SANY accept
A
,B
,C
, andD
just fine, but TLAPS' parser reports a syntax error forD
: