pmer / tla-bin Goto Github PK

Hi,
I am trying to run the model checker from command line. It gives error on the cfg file. Can you please help with this?

Best

* Add statements after this line.
* CONSTANT definitions
CONSTANT
F <- 1
* CONSTANT definitions
CONSTANT
N <- 4
* CONSTANT definitions
CONSTANT
INPUT <- <<1,1,1,1>>
* CONSTANT definitions
CONSTANT
MAXROUND <- 10
* SPECIFICATION definition
SPECIFICATION
Spec
* INVARIANT definition
INVARIANT
Agreement
* PROPERTY definition
PROPERTY
BaitProgress
PROPERTY
MinorityReport
PROPERTY
Progress

It seems that as of December 2020 https://tla.msr-inria.inria.fr/tlatoolbox/dist/tla2tools.jar is no longer being updated. https://github.com/tlaplus/tlaplus/releases/latest/download/tla2tools.jar should work instead

Right now, the -error-codes flag will work on nightly but will induce an error on the stable release. Once v1.8 comes out, we can enable this flag unconditionally, which will be useful for CI use cases.

Related PR: tlaplus/tlaplus#483

Requested by: #9

tla.zip has already been removed in the ci builds

Hey, working on some tooling/automation for my TLA+ workflow!

Super grateful for finding this repo. You might chalk this up to my ignorance with Java but when I run the TLC binary I get this error (traceback elided):

TLC2 Version 2.13 of 18 July 2018
Exception in thread "main" java.lang.NoClassDefFoundError: javax/activation/DataSource
	at tlc2.TLC.main(TLC.java:210)
Caused by: java.lang.ClassNotFoundException: javax.activation.DataSource
	at java.base/jdk.internal.loader.BuiltinClassLoader.loadClass(BuiltinClassLoader.java:583)

java version "11.0.2" 2019-01-15 LTS
Java(TM) SE Runtime Environment 18.9 (build 11.0.2+9-LTS)
Java HotSpot(TM) 64-Bit Server VM 18.9 (build 11.0.2+9-LTS, mixed mode)

When running tlatex example.tla, got

Exception in thread "main" tla2tex.TLA2TexException: TLATeX unrecoverable error: -- Trying to run the command `latex example.tex' produced the following error
    Cannot run program "latex": error=2, No such file or directory.
	at tla2tex.Debug.ReportError(Debug.java:26)
	at tla2tex.ExecuteCommand.executeCommand(ExecuteCommand.java:34)
	at tla2tex.LaTeXOutput.RunLaTeX(LaTeXOutput.java:483)
	at tla2tex.TLA.runTranslation(TLA.java:246)
	at tla2tex.TLA.main(TLA.java:150)
` ``

Based on the "Trace Exploration through Command Line" function, adding a Trace Explorer command might be pretty handy.

Having read @will62794's tlaplus_animation repo, especially aliases.sh and get_tlatools.sh, one would add a new trace command to tla-bin/bin by:

• Copying tla-bin/bin/tlc to a tla-bin/bin/trace file;
• Changing line 9 of this trace file from ...tla2tools.jar tlc2.TLC to ...tla2tools.jar:tla2tools.jar:CommunityModules-202112291842.jar tlc2.TraceExplorer (or to wherever the latest Community Modules jar file can be downloaded from).

It would require an updated Community Modules jar file, so it'd be necessary to add that to tla-bin/download_or_update_tla.sh.

Maybe I am missing a step? Maybe trace is not necessary, given an alternative command?

Thanks

SUMMARY
tlc depends on pcal successfully running and generating the .cfg file. However, if the input file is just tla+ and does not contain the pluscal comment block, pcal fails.

EXPECTED
I'd expect pcal to succeed and generate the .cfg file even if no pluscal code is found.

REPRO

git clone https://github.com/tlaplus/Examples.git examples
cd examples/specifications/N-Queens
pcal Queens

ERROR A

ls
QueensPluscal.tla  QueensPluscal.toolbox  Queens.tla  Queens.toolbox  README  states

pcal Queens
pcal.trans Version 1.9 of 10 July 2019

Unrecoverable error:
 -- Beginning of algorithm string --algorithm not found..

This seems ok, except that I'd like to run tlc on this, too:

ERROR B

tlc Queens

TLC2 Version 2.14 of 10 July 2019 (rev: 0cae24f)
Running breadth-first search Model-Checking with fp 36 and seed 408714217296578281 with 1 worker on 8 cores with 7134MB heap and 64MB offheap memory [pid: 19015] (Linux 4.15.0-96-generic amd64, Ubuntu 11.0.6 x86_64, MSBDiskFPSet, DiskStateQueue).
Error: TLC threw an unexpected exception.
This was probably caused by an error in the spec or model.
See the User Output or TLC Console for clues to what happened.
The exception was a tlc2.tool.ConfigFileException
: TLC encountered the following error when trying to read the configuration file Queens.cfg:
File not found.
Finished in 00s at (2020-04-16 13:56:29)

I've noticed that the sany script always returns 0 error code even if there are e.g. parse errors in the input file. E.g. I would like it to return a non-zero code to use it in the test suite of a transpiler targeting TLA+ I'm working on. By the way, thank you for tla-bin!