| Dear Ioannis,
thanks for reporting this, and if you encounter such behavior, please do open an issue on GitHub so that we can keep track easily.
The code that you are experimenting with is in internal development, not even an alpha release yet, and the TLA to XML converter still has a number of issues that we are hunting down (be they bugs or misunderstandings on our side).
Regards, Stephan
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
--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@xxxxxxxxxxxxxxxx.
To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.
|