[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