[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
theorems from instantiated modules in `tlapm` version 2
I encountered the following behavior with v2-tlapm @ fd345f78c7e356b53c67e24f17e99df449d7b3a3 [1].
It may be internally unsupported syntax, but the old `tlapm == 1.4.3 (build 34695)` is happy with the modules involved,
and `tla2sany` too, so it seems worth reporting.
Issue 1:
The statement [2]:
```
try
Ok (Sany.import_xml channel)
with
| e ->
Error e
```
appears to be catching errors that do not originate from `sany.jar`.
(I am not familiar with OCaml, but see issue 2 below.)
Those are later reported as "TLA to XML conversion error... java return code is 0".
This behavior initially suggested that something is wrong with the syntax,
but running `sany.jar` directly showed no errors (as suggested by the return code).
Changing the invocation from within OCaml to dump the XML to
a file showed the same result (no errors from `sany.jar`).
Issue 2:
Removing the `try` statement to obtain:
```
Ok (Sany.import_xml channel)
```
produces the message:
```
Exception: (Failure
"We expected exactly one matching child in <AssumeProveNode> but got 0")
Backtrace: Raised at file "format.ml", line 185, characters 41-52
Called from file "format.ml", line 412, characters 8-33
Called from file "format.ml", line 427, characters 6-24
```
However, the module that causes this is `B` from below.
(Module `A` is in the include paths, and is seen by `sany.jar`.)
The issue seems to relate to instantiation of module `A`,
because if I change the statements to either
`Inst == INSTANCE Nat` and `Inst!Nat`
or remove the `BY` statement, then the error disappears.
------------------------------- MODULE B ---------------------------------------
Inst == INSTANCE A
THEOREM
ASSUME TRUE
PROVE TRUE
BY Inst!SomeTheorem
================================================================================
----------------------------- MODULE A -----------------------------------------
THEOREM SomeTheorem ==
ASSUME TRUE
PROVE TRUE
================================================================================
Please let me know in case I should open an issue at [1] for this or similar issues in the future.
[1] https://github.com/tlaplus/v2-tlapm
[2] https://github.com/tlaplus/v2-tlapm/blob/fd345f78c7e356b53c67e24f17e99df449d7b3a3/src/tlapm.ml#L59
Best regards,
ioannis