Failed to check realizability

[lht011129]

I have downloaded jkind.jar, jkind, jrealizability and jlustre2kind from the the latest release and changed permissions for the downloaded files to be executable, as figure1 showed. I have added the directory to PATH environment variable. But when I want to check realizability in FRET, I met the issue showed in figure2.

[andreaskatis]

Hi @lht011129,

Jkind (or Kind 2) is one of two required dependencies for realizability checking. The other one is Z3, which also needs to be added to PATH. Do you have Z3 installed?

Best Regards,

Andreas

[lht011129]

Hi Andreas, Thanks for your suggestion, I have resolved this issue by installing Z3. Best Regards, Lin

…

------------------ 原始邮件 ------------------ 发件人: "NASA-SW-VnV/fret" ***@***.***>; 发送时间: 2024年5月15日(星期三) 晚上7:55 ***@***.***>; ***@***.******@***.***>; 主题: Re: [NASA-SW-VnV/fret] Failed to check realizability (Discussion #81) Hi @lht011129, Jkind (or Kind 2) is one of two required dependencies for realizability checking. The other one is Z3, which also needs to be added to PATH. Do you have Z3 installed? Best Regards, Andreas — Reply to this email directly, view it on GitHub, or unsubscribe. You are receiving this because you were mentioned.Message ID: ***@***.***>

[andreaskatis]

Thank you for letting us know!