SANY TLA+ semantic graph exploration tool fails on nested instances

[konnov]

I am trying to print the semantic graph of the following module, which captures the instantiation structure of Paxos:

------------------- MODULE P ----------------------
------------------- MODULE Vot ----------------------
------------------- MODULE Cons -------------------
VARIABLE chosen
Init == chosen = {}
Next == chosen = {2}
===================================================
chosen == {1}
C == INSTANCE Cons
===================================================
V == INSTANCE Vot
===================================================

The following call to the "TLA+ semantic graph exploration tool" results in NullPointerException (SANY honestly warned me about the NPE to be produced):

$ java -cp ~/.m2/repository/org/lamport/tla2tools/1.7.0-SNAPSHOT/tla2tools-1.7.0-SNAPSHOT.jar  tla2sany.SANY -d P.tla

****** SANY2 Version 2.1 created 24 February 2014

Parsing file /Users/igor/devl/apalache/test/tla/P.tla
Semantic processing of module P
Bug in debugging caused by inner module Vot
SANY will throw a null pointer exception.
Bug in debugging caused by inner module Vot
SANY will throw a null pointer exception.


*** TLA+ semantic graph exploration tool v 1.0 (DRJ)

>>mt

External Module Table:
| Module: *ModuleNode: P    uid: 154  kind: ModuleKind  errors: noneException in thread "main" java.lang.NullPointerException
	at tla2sany.semantic.Context.getContextEntryStringVector(Context.java:499)
	at tla2sany.semantic.ModuleNode.print(ModuleNode.java:1150)
	at tla2sany.semantic.ExternalModuleTable.printExternalModuleTable(ExternalModuleTable.java:165)
	at tla2sany.explorer.Explorer.executeCommand(Explorer.java:240)
	at tla2sany.explorer.Explorer.parseAndExecuteCommand(Explorer.java:338)
	at tla2sany.explorer.Explorer.main(Explorer.java:427)
	at tla2sany.drivers.SANY.SANYmain(SANY.java:458)
	at tla2sany.SANY.main(SANY.java:12)

[lemmy]

Probably related: #471

[konnov]

If that helps, the example works, when I extract Vot and Cons into files.

[lemmy]

FWIW, recent builds of TLC accept multiple, non-nested modules in a single .tla file:

With Root.tla being a TLA+ file, you can do:

Start of Root.tla
----- MODULE Root -----
...
A == INSTANCE A

B == INSTANCE B

====

---- MODULE A ----
...
====

---- MODULE B -----
...
====
END OF Root.tla

[konnov]

That is exactly what I tried, but the explorer fails there

[lemmy]

In that case, the bug is independent of module nesting and should also occur with three .tla files without nested modules.

[konnov]

It looks like this issue appears only when the modules are inlined in a single file