Initial Setup in Windows OS

[Paulovss85]

Hello. Regarding Initial Setup

Assuming the ESBMC.exe path is C:\user\ESBMC\ESBMC-Windows\bin

The files config.json and .env should in which folder( directory)?
The path above should be added in config.json

Could share the folder structure to merge esbmc-ai to esbmc?

[Yiannis128]

Hi, the files config.json and .env should be in the directory where ESBMC-AI is in. So let's say you have ESBMC-AI in a directory: C:\user\esbmc-ai, then the file path for both config.json and .env should be:

• C:\user\esbmc-ai\config.json
• C:\user\esbmc-ai\.env

I'm working towards making this program available in PyPi, so you will be able to install it through Pip, but for now, if you require anymore help, please let me know :)

[Yiannis128]

I've enabled discussions, please ask me any questions you have still there :)

[Paulovss85]

First of all, thanks for your time.

OK, i using ESBMC to make the model checking normally.
The image below is my esbmc-ai folder look like. Is this correct? I mean, the files.

Which files should be in the esbmc-ai folder in order to run?

[Yiannis128]

Without knowing what's in each file, it seems the contents are correct. Make sure the .env file contains your API keys for the LLMs that you want to use. So if you're using OpenAI models, make sure to include the OpenAI API keys.

In the config.json file, make sure to replace the contents of esbmc_path path from the default to the location of your ESBMC executable, so in your case: C:\user\ESBMC\ESBMC-Windows\bin\ESBMC.exe assuming that ESBMC.exe is the name of the executable.

Make sure to also install all the prerequisites detailed in requirements.txt or the Pipfile.

If you have anymore issues, please let me know :)

[Yiannis128]

I would like to add that I haven't tested if this is necessary, so I would appreciate it if you let me know: The file paths in the config are using the Linux path separators, do any problems present in Windows for using the Linux path separators?

Example from .env: ESBMC_AI_CFG_PATH=./config.json

If that's a problem, it may need to be changed to ESBMC_AI_CFG_PATH=.\config.json for Windows. If it's possible please let me know if that's the case 😀

[Paulovss85]

hello.

I will try to use de WSL to check it. Maybe what you saying make sense bc all path uses Linux separators.

Once again, thanks for you support

[Paulovss85]

Hello, now i having the error below:

[Yiannis128]

Hi, did you make sure to install the dependencies? You should run pip install -r requirements.txt

[Paulovss85]

After some research in web, i found a solution to the previous issue. It seems that dependencies now working fine

Now, I'm having issue below:

My currents directories are:

To esbmc.exe ->/mnt/c/esbmc/ESBMC-7.2.0-Linux/bin
To .evn and config.jason -> /mnt/c/esbmc/esbmc-ai

my config.json content

It seems that have any permission problem right now

[Yiannis128]

There are two issues:

• Your esbmc_path in config.json needs to point to the executable, not the folder it is located in. So it should be something like: /mnt/c/esbmc/ESBMC-7.2.0-Linux/bin/esbmc assuming that that's the name of the executable (you should verify on your machine).
• The second issue I've found is that you should rename ESBMC_CFG_PATH to ESBMC_AI_CFG_PATH in your .env file.

Also, you should remove your OpenAI API key from being visible on GitHub as I think people can steal it :)

[Paulovss85]

When i use sudo, its returned error below:
The modules not found

[Yiannis128]

That's because when using sudo, it uses the root user, which doesn't have the Pip packages installed, as you've probably installed them local to your user.

There is no need to use sudo. The problem must be in the config you are using, we will figure it out...

[Yiannis128]

Hi, have you managed to get ESBMC-AI to work?

[Paulovss85]

Hello Yiannis. Not yet. Im having issues in the WLS. The dependecias seems be installed, but not reconized when i try run the verification. But i will try do more verification this week. Thanks for your help Em dom., 23 de jul. de 2023 às 19:47, Yiannis Charalambous < ***@***.***> escreveu:

…

Hi, have you managed to get ESBMC-AI to work? — Reply to this email directly, view it on GitHub <#76 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AWSN2SZSTD3NFGJ6773PPMDXRWZZNANCNFSM6AAAAAA2DEOKSA> . You are receiving this because you authored the thread.Message ID: ***@***.***>

[Yiannis128]

I see. If there's anything else I can assist with, please let me know. I will close this discussion for now. Feel free to start a new one.

[Yiannis128]

Closing discussion as no update in months.