tlapm Error

[lixh...@gmail.com]

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

[Stephan Merz]

It looks like one of those cases where the PM parser does not agree with SANY. The most likely culprit is a construct involving tuple binding, but there are a few other cases. These problems are expected to disappear with the next major release of TLAPS.

I asked the sender of the message to provide me the offending source module(s) off-list and will summarize the findings when I hear back.

Stephan

--
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...@googlegroups.com.
To post to this group, send email to tla...@googlegroups.com.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.