1
Vote

Problem occurred

description

When I used TLAPS to prove some algorithms, I met a problem. I don't know how to deal with it. Here is the "TLAPM error"

Oops, this seems to be a bug in TLAPM.
Please give feedback to developers.


Failure("Executable \"zenon\" not found in this PATH:\n/cygdrive/d/Java/jdk1.8.0_121/bin/server:/cygdrive/d/Java/jdk1.8.0_121/bin:/cygdrive/d/Java/jdk1.8.0_121/lib/amd64:/cygdrive/d/0ICT/tlaps-1.4.3/OCaml/bin:/cygdrive/c/ProgramData/Oracle/Java/javapath:/cygdrive/c/Program Files/PTC/MKSTOO~1/bin64:/cygdrive/c/Program Files/PTC/MKSTOO~1/bin:/cygdrive/c/Program Files/PTC/MKSTOO~1/bin/X11:/cygdrive/c/Program Files/PTC/MKSTOO~1/mksnt:/cygdrive/c/Windows/system32:/cygdrive/c/Windows:/cygdrive/c/Windows/System32/Wbem:/cygdrive/c/Windows/System32/WindowsPowerShell/v1.0:/cygdrive/d/Java/jdk1.8.0_121:/cygdrive/d/Java/JAVA/bin:/cygdrive/d/Rational/common:/cygdrive/c/Program Files/Common Files/Autodesk Shared:/cygdrive/c/Windows/system32/config/systemprofile/.dnx/bin:/cygdrive/c/Program Files/Microsoft DNX/Dnvm:/cygdrive/c/Program Files/Microsoft SQL Server/130/Tools/Binn:/cygdrive/d/MATLAB/MATLAB Production Server/R2015a/runtime/win64:/cygdrive/d/MATLAB/MATLAB Production Server/R2015a/bin:/cygdrive/d/MATLAB/MATLAB Production Server/R2015a/polyspace/bin:/cygdrive/d/Python27:/cygdrive/d/Python27/Scripts:/cygdrive/c/Windows/System32:/cygdrive/d/Java/jdk1.8.0_121/bin:/cygdrive/d/Java/jdk1.8.0_121/jre/bin:/cygdrive/c/Windows/system32:/cygdrive/c/Windows:/:/usr/bin:/usr/local/bin:/cygdrive/e/toolbox:/:/lib/tlaps/bin\n")
Raised at file "pervasives.ml", line 20, characters 22-33
Called from file "params.ml", line 399, characters 12-26
Called from file "tlapm_args.ml", line 229, characters 2-20
Called from file "tlapm.ml", line 334, characters 13-33

version == "1.4.3 (build 34695)"
built_with == "OCaml 4.01.0"
tlapm_executable == "//tlapm"
max_threads == 4
library_path == "/lib/tlaps"
search_path == << "E:\Cygwin\usr\local\lib\tlaps\"
            , "/lib/tlaps" >>
Executable "zenon" not found in this PATH:
/cygdrive/d/Java/jdk1.8.0_121/bin/server:/cygdrive/d/Java/jdk1.8.0_121/bin:/cygdrive/d/Java/jdk1.8.0_121/lib/amd64:/cygdrive/d/0ICT/tlaps-1.4.3/OCaml/bin:/cygdrive/c/ProgramData/Oracle/Java/javapath:/cygdrive/c/Program Files/PTC/MKSTOO~1/bin64:/cygdrive/c/Program Files/PTC/MKSTOO~1/bin:/cygdrive/c/Program Files/PTC/MKSTOO~1/bin/X11:/cygdrive/c/Program Files/PTC/MKSTOO~1/mksnt:/cygdrive/c/Windows/system32:/cygdrive/c/Windows:/cygdrive/c/Windows/System32/Wbem:/cygdrive/c/Windows/System32/WindowsPowerShell/v1.0:/cygdrive/d/Java/jdk1.8.0_121:/cygdrive/d/Java/JAVA/bin:/cygdrive/d/Rational/common:/cygdrive/c/Program Files/Common Files/Autodesk Shared:/cygdrive/c/Windows/system32/config/systemprofile/.dnx/bin:/cygdrive/c/Program Files/Microsoft DNX/Dnvm:/cygdrive/c/Program Files/Microsoft SQL Server/130/Tools/Binn:/cygdrive/d/MATLAB/MATLAB Production Server/R2015a/runtime/win64:/cygdrive/d/MATLAB/MATLAB Production Server/R2015a/bin:/cygdrive/d/MATLAB/MATLAB Production Server/R2015a/polyspace/bin:/cygdrive/d/Python27:/cygdrive/d/Python27/Scripts:/cygdrive/c/Windows/System32:/cygdrive/d/Java/jdk1.8.0_121/bin:/cygdrive/d/Java/jdk1.8.0_121/jre/bin:/cygdrive/c/Windows/system32:/cygdrive/c/Windows:/:/usr/bin:/usr/local/bin:/cygdrive/e/toolbox:/:/lib/tlaps/bin

flatten_obligations == TRUE

normalize == TRUE

comments