Does CoCoSim support Matlab 2020B

[aogrcs]

Does CoCoSim support Matlab 2020B

[andreaskatis]

Hello,

2020b definitely works, as it is the one that I am personally using at the moment. Please make sure that:

1. Your installation completed without errors
2. When in MATLAB, use the file explorer window to navigate to the home directory of the CoCoSim repo, then run start_cocosim from the MATLAB terminal
3. Open up a project (any one from the provide examples can also work). Then in the "Tools" menu (top left for me) you should be able to see the options regarding CoCoSim

[aogrcs]

Hi, there is my error logs:
[2021-07-27 22:54:48] [progress] Checking required dependencies
[2021-07-27 22:54:48] [debug] Found cc at /usr/bin/cc
[2021-07-27 22:54:48] [debug] Found c++ at /usr/bin/c++
[2021-07-27 22:54:48] [debug] Found cat at /bin/cat
[2021-07-27 22:54:48] [debug] Found rm at /bin/rm
[2021-07-27 22:54:48] [debug] Found mv at /bin/mv
[2021-07-27 22:54:48] [debug] Found cp at /bin/cp
[2021-07-27 22:54:48] [debug] Found ln at /bin/ln
[2021-07-27 22:54:48] [debug] Found find at /usr/bin/find
[2021-07-27 22:54:48] [debug] Found tee at /usr/bin/tee
[2021-07-27 22:54:48] [debug] Found patch at /usr/bin/patch
[2021-07-27 22:54:48] [debug] Found tar at /usr/bin/tar
[2021-07-27 22:54:48] [debug] Found gzip at /usr/bin/gzip
[2021-07-27 22:54:48] [debug] Found gunzip at /usr/bin/gunzip
[2021-07-27 22:54:48] [debug] Found xz at /usr/local/bin/xz
[2021-07-27 22:54:48] [debug] Found make at /usr/bin/make
[2021-07-27 22:54:48] [debug] Found install at /usr/bin/install
[2021-07-27 22:54:48] [debug] Found git at /usr/bin/git
[2021-07-27 22:54:48] [debug] Found opam at /usr/local/bin/opam
[2021-07-27 22:54:48] [debug] Found autoconf at /usr/local/bin/autoconf
[2021-07-27 22:54:48] [debug] Found automake at /usr/local/bin/automake
[2021-07-27 22:54:48] [debug] Found aclocal at /usr/local/bin/aclocal
[2021-07-27 22:54:48] [debug] Found pkg-config at /usr/local/bin/pkg-config
[2021-07-27 22:54:48] [debug] Found curl at /usr/bin/curl
[2021-07-27 22:54:48] [success] Found all required utilities
[2021-07-27 22:54:48] [progress] Checking for Python
[2021-07-27 22:54:48] [debug] 'python --version':
Python 2.7.16
[2021-07-27 22:54:48] [success] Found Python 2.7.16
[2021-07-27 22:54:48] [debug] 'python --version':
Python 2.7.16
[2021-07-27 22:54:48] [progress] Installing OCaml 4.07.0, ocamlfind, ocamlbuild, cmdliner and ocamlgraph
[2021-07-27 22:54:48] [progress] opam init -y --comp=4.07.0

<><> Required setup - please read <><><><><><><><><><><><><><><><><><><><><> 🐫

In normal operation, opam only alters files within ~/.opam.

However, to best integrate with your system, some environment variables
should be set. If you allow it to, this initialisation step will update
your bash configuration by adding the following line to ~/.bash_profile:

test -r /Users/wenlongxie/.opam/opam-init/init.sh && . /Users/wenlongxie/.opam/opam-init/init.sh > /dev/null 2> /dev/null || true

Otherwise, every time you want to access your opam installation, you will
need to run:

eval $(opam env)

You can always re-run this setup with 'opam init' later.

[WARNING] Shell not updated in non-interactive mode: use --shell-setup
A hook can be added to opam's init scripts to ensure that the shell remains in sync with the opam environment when they are loaded. Set that up? [y/N] y
[2021-07-27 22:54:48] [progress] opam switch -y 4.07.0
[2021-07-27 22:54:48] [progress] eval OPAM_SWITCH_PREFIX='/Users/wenlongxie/.opam/4.07.0'; export OPAM_SWITCH_PREFIX; CAML_LD_LIBRARY_PATH='/Users/wenlongxie/.opam/4.07.0/lib/stublibs:/Users/wenlongxie/.opam/4.07.0/lib/ocaml/stublibs:/Users/wenlongxie/.opam/4.07.0/lib/ocaml'; export CAML_LD_LIBRARY_PATH; OCAML_TOPLEVEL_PATH='/Users/wenlongxie/.opam/4.07.0/lib/toplevel'; export OCAML_TOPLEVEL_PATH; PATH='/Users/wenlongxie/.opam/4.07.0/bin:/Users/wenlongxie/Downloads/OPEN-SOURCE/clawcircus/bin:/Users/wenlongxie/Downloads/formal_methods_tools/crux-llvm-0.4-macOS-x86_64/bin:/Users/wenlongxie/Downloads/formal_methods_tools/clang+llvm-9.0.0-x86_64-darwin-apple/lib/clang/7.0.7/include:/Users/wenlongxie/Downloads/formal_methods_tools/clang+llvm-9.0.0-x86_64-darwin-apple/include/c++/v1:/Users/wenlongxie/Downloads/formal_methods_tools/clang+llvm-9.0.0-x86_64-darwin-apple/bin:/Users/wenlongxie/Downloads/formal_methods_tools/z3-4.8.10-x64-osx-10.15.7/bin:/Users/wenlongxie/Downloads/formal_methods_tools/saw-0.7-macOS-x86_64/bin:/Users/wenlongxie/Downloads/drake/bin:/Users/wenlongxie/Downloads/formal_methods_tools/cryptol-2.9.0-macOS-x86_64/bin:/Users/wenlongxie/Downloads/formal_methods_tools/gcc-arm-none-eabi-8-2019-q3-update/bin:/Users/wenlongxie/Downloads/formal_methods_tools/SeaHorn-0.1.0-rc3-Darwin-x86_64/bin:/Users/wenlongxie/Downloads/formal_methods_tools/infer-osx-v0.15.0/bin:/usr/local/Cellar/make/4.2.1_1/bin:/usr/local/bin:/usr/bin:/bin:/usr/sbin:/sbin:/Applications/VMware Fusion.app/Contents/Public:/opt/X11/bin:/Library/Apple/usr/bin'; export PATH;
[2021-07-27 22:54:48] [progress] opam update

<><> Updating package repositories ><><><><><><><><><><><><><><><><><><><><> 🐫
[default] no changes from https://opam.ocaml.org

<><> Synchronising development packages <><><><><><><><><><><><><><><><><><> 🐫
[kind2.1.4.0] synchronised (no changes)
[2021-07-27 22:59:13] [progress] opam install -y depext ocamlfind ocamlbuild ocamlgraph fmt logs topkg cmdliner num yojson zarith
[WARNING] Opam packages conf-gmp.3 and conf-python-2-7.1.1 depend on the following system packages that are no longer installed: gmp python
[NOTE] Package num is already installed (current version is 1.4).
[NOTE] Package ocamlfind is already installed (current version is 1.8.1).
[ERROR] depext unmet availability conditions, e.g. 'opam-version >= "2.0.0~beta5" & opam-version < "2.1"'
[2021-07-27 22:59:16] [error] Error while installing ocaml. see /Users/wenlongxie/Downloads/CoCoSim_v1.2/tools/build/bootstrap.log for more details.
[2021-07-27 22:59:16] [progress] opam pin add -y z3 4.8.1
[NOTE] Pinning unchanged
z3 is now pinned to version 4.8.1

[WARNING] Opam packages conf-gmp.3 and conf-python-2-7.1.1 depend on the following system packages that are no longer installed: gmp python
The following actions will be performed:
↻ recompile conf-gmp 3 [upstream or system changes]
↻ recompile conf-python-2-7 1.1 [upstream or system changes]
↻ recompile z3 4.8.1*
===== ↻ 3 =====

The following system packages will first need to be installed:
gmp python

<><> Handling external dependencies <><><><><><><><><><><><><><><><><><><><> 🐫
Let opam run your package manager to install the required system packages? [Y/n] y

• /usr/local/bin/brew "install" "gmp" "python"

• Warning: gmp 6.2.1 is already installed and up-to-date
• To reinstall 6.2.1, run brew reinstall gmp
• Warning: [email protected] 3.9.0_4 is already installed, it's just not linked
• You can use brew link [email protected] to link this version.

<><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><> 🐫
⬇ retrieved z3.4.8.1 (cached)
⊘ removed z3.4.8.1
⊘ removed conf-gmp.3
⊘ removed conf-python-2-7.1.1
∗ installed conf-gmp.3
∗ installed conf-python-2-7.1.1
∗ installed z3.4.8.1
Done.
[2021-07-27 23:05:10] [progress] opam install -y z3
[WARNING] Opam packages conf-gmp.3 and conf-python-2-7.1.1 depend on the following system packages that are no longer installed: gmp python
[NOTE] Package z3 is already installed (current version is 4.8.1).
[2021-07-27 23:05:12] [progress] opam install -y menhir
[WARNING] Opam packages conf-gmp.3 and conf-python-2-7.1.1 depend on the following system packages that are no longer installed: gmp python
[NOTE] Package menhir is already installed (current version is 20210419).
[2021-07-27 23:05:14] [progress] Using already built z3
[2021-07-27 23:05:28] [debug] '/Users/wenlongxie/Downloads/CoCoSim_v1.2/tools/verifiers/osx/z3/bin/z3 --version':
[2021-07-27 23:05:28] [error] Unable to detect the version of 'z3'
[2021-07-27 23:05:28] [progress] Using already built lustrec
[2021-07-27 23:05:28] [success] lustrec successfully installed
[2021-07-27 23:05:30] [progress] opam pin add -y -n kind2 https://github.com/kind2-mc/kind2.git#develop
[NOTE] Package kind2 is already pinned to git+https://github.com/kind2-mc/kind2.git#develop (version 1.4.0).
[kind2.1.4.0] synchronised (no changes)
kind2 is now pinned to git+https://github.com/kind2-mc/kind2.git#develop (version 1.4.0)
[2021-07-27 23:05:32] [progress] opam depext -y kind2
Opam plugin "depext" is not installed. Install it on the current switch? [Y/n] y

Do I use the error version opam? my version is 2.1.0~beta2!
Thanks

[andreaskatis]

Hi,

Thank you for providing the logs. This does seem like an issue with your version of opam. Did you have that installed yourself, before trying to install CoCoSim? In my current installation, I'm using opam v2.0.5. Perhaps you can try that in the meantime, and install again?

Finally, could you also provide a copy of the contents under /Users/wenlongxie/Downloads/CoCoSim_v1.2/tools/build/bootstrap.log ?

I will try to install CoCoSim on a fresh image later today and see if I can replicate this on my end as well.

[aogrcs]

Hi, this is the log, but it could not install kind2, it stoped at "opam depext -y kind2"
bootstrap.log

[andreaskatis]

Hello,

Thank you very much for the logs! It appears that you are trying to install CoCoSim from source. Installing from source, as per the INSTALL.md instructions, is not the recommended way, at the moment.

Anyway, from the kind of errors that you were getting related to kind2, it appears that there may be a network issue on your side when trying to access the Kind 2 repository: https://github.com/kind2-mc/kind2 . Can you check whether you can download Kind 2 using this command:

wget https://github.com/kind2-mc/kind2/releases/download/v1.2.0/kind2-v1.2.0-macosx.tar.gz -O - | tar -xz
It should normally download a binary called "kind2-v1.2.0-macosx" (You can safely delete the download right after). If it doesn't you may need to provide the binary to your machine in a different way. I can then help you figure out how to use it with CoCoSim.

Please be aware that when installing from source, an additional step is required i.e., installing external libraries using install_cocosim_lib from the MATLAB terminal.

In any case, as I mentioned above, installing from sources is not currently recommended. If your original intention was to just try CoCoSim, installing it from release should be significantly easier. You can do so by downloading the latest stable release. The rest of this process should be simple:

1. You extract the .zip file and run the install_cocosim script.
2. When (1) is completed, you have to open up MATLAB and navigate using MATLAB's explorer window to the home directory of the downloaded CoCoSim release. Then, start CoCoSim from the MATLAB terminal by running start_cocosim
3. As soon as (2) is completed (you should be able to see an option to boot up a verification example, you are good to go!

Please let me know if you are okay with closing this issue, as it has diverted a bit from the original question. For further assistance with installing and using CoCoSim please do not hesitate to reach out to me at [email protected] .

[aogrcs]

Hi
I find that Z3 version in the stable version of CoCoSim is 4.8.10, but I do not find this version in the opam web, here is the error during install:

I can start CoCoSim using start_cocosim, but I do not find the tools, here is:

thanks!
Sincerely

[aogrcs]

Hi, I also download kind2 using your commands!

[andreaskatis]

Hi,

The stable version of CoCoSim comes pre-packed with Z3 4.8.8. The error "unable to detect the version of 'z3'" does not affect the installation of CoCoSim.

In your second screenshot, there is a "Tools" option at the top left, right above the project navigation arrows. You should be able to see it as an option there.

With that being said, I am closing this thread, as it has diverted a lot from the issue's subject. If you need further help with the installation or usage of CoCoSim, please make sure to read the manual, watch the tool videos, and most importantly send me an e-mail at [email protected]

Thank you,

Andreas