[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

tlapm Error



Hello!

When I wanted to prove the theorem of raft, I found an TLAPM error, as follow:
-------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------
Oops, this seems to be a bug in TLAPM.
Please give feedback to developers.


 Failure("Module.Parser.parse_file")
Raised at file "pervasives.ml", line 20, characters 22-33
Called from file "m_save.ml", line 27, characters 16-20
Called from file "tlapm.ml", line 289, characters 8-112
Called from file "list.ml", line 84, characters 24-34
Called from file "tlapm.ml", line 309, characters 20-43
Called from file "tlapm.ml", line 334, characters 8-33

version == "1.4.3 (build 34695)"
built_with == "OCaml 4.01.0"
tlapm_executable == "/cygdrive/d/Java/jdk1.8.0_121/tlapm"
max_threads == 4
library_path == "/cygdrive/d/Java/lib/tlaps"
search_path == << "D:\0ICT\cygwin\usr\local\lib\tlaps\bin\"
                , "D:\0ICT\cygwin\usr\local\bin\"
                , "D:\0ICT\cygwin\usr\local\lib\tlaps\"
                , "/cygdrive/d/Java/lib/tlaps" >>
zenon == "PATH=\"${PATH}:/cygdrive/d/Java/jdk1.8.0_121:/cygdrive/d/Java/lib/tlaps/bin\"; zenon -p0 -x tla -oisar -max-time 1d \"$file\""
zenon version == "zenon version 0.7.2 [a253] 2013-03-04"
flatten_obligations == TRUE
normalize == TRUE
-------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------
And, the TLAPM console said
------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------
@!!BEGIN
@!!type:error
@!!url:http://tla.msr-inria.inria.fr/bugs
@!!msg:Oops, this seems to be a bug in TLAPM.
Please give feedback to developers.


 Failure("Module.Parser.parse_file")
Raised at file "pervasives.ml", line 20, characters 22-33
Called from file "m_save.ml", line 27, characters 16-20
Called from file "tlapm.ml", line 289, characters 8-112
Called from file "list.ml", line 84, characters 24-34
Called from file "tlapm.ml", line 309, characters 20-43
Called from file "tlapm.ml", line 334, characters 8-33

version == "1.4.3 (build 34695)"
built_with == "OCaml 4.01.0"
tlapm_executable == "/cygdrive/d/Java/jdk1.8.0_121/tlapm"
max_threads == 4
library_path == "/cygdrive/d/Java/lib/tlaps"
search_path == << "D:\0ICT\cygwin\usr\local\lib\tlaps\bin\"
                , "D:\0ICT\cygwin\usr\local\bin\"
                , "D:\0ICT\cygwin\usr\local\lib\tlaps\"
                , "/cygdrive/d/Java/lib/tlaps" >>
zenon == "PATH=\"${PATH}:/cygdrive/d/Java/jdk1.8.0_121:/cygdrive/d/Java/lib/tlaps/bin\"; zenon -p0 -x tla -oisar -max-time 1d \"$file\""
zenon version == "zenon version 0.7.2 [a253] 2013-03-04"
flatten_obligations == TRUE
normalize == TRUE
@!!END 
-------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------
I don't know how to deal with it. (/*T _ T*\)

Best regards, 
Li Xiao hui