Encounters error in running the example HyperLTL spec in BoSy about bosy HOT 11 CLOSED

Hey
I could not reproduce the Error on my VM form just the command you used.
I could not find the file you attached, could you please upload it again? Without it we're not really able to help you with your issue

Thanks

from bosy.

sorry, here is the file
BoSy_err.txt

Also where can I find the explanation for the spec of given samples in BoSy, such as (arbiter & load balancer)

from bosy.

I want the SMV output from this offline tool, what is the command to generate the same ?

Can I run HyperLTL in online interface ? If so what's the format?

from bosy.

Hi,
can you compare the binaries in Tools/ with the list in the makefile? Looks like some external call was impossible.

The online interface does not support HyperLTL currently.

from bosy.

Thanks @nimetz for your response

I tried installing swift & bosy in other Ubuntu system and tried the same hyperLTL example, I faced the same issue.

I have attached the logs of make file and hyperLTL output, for more information kindly do check and help me to resolve this issue
hyperLTL_output.txt
make_all_output.txt
make_all_output_2.txt

In my work I wanna make use of the SMV output of HyperLTL from this tool, therefore kindly confirm whether the SMV will be generated for HyperLTL or not?

from bosy.

From skimming over your build logs it seems that a download location for a tool is no longer available or I messed up the link wenn fixing the Makefile. I will check that once I am in front of my machine again. Maybe that produces your error

from bosy.

The output of BoSyHyper is in .dot and .aag format, but you can easily add the line print((solution as! SmvRepresentable).smv) to file /Sources/BoSyHyper/main.swift in line 118, and it will print also the .smv representable of the solution to stdout.

To have a quick fix for the curl error of idq before we fix it, please comment out line 55 in the makefile and try compiling again (If necessary, repeat that for every curl that didn't work). You can add the binary of idq later on, but BoSyHyper does not use it.

from bosy.

The output of BoSyHyper is in .dot and .aag format, but you can easily add the line print((solution as! SmvRepresentable).smv) to file /Sources/BoSyHyper/main.swift in line 118, and it will print also the .smv representable of the solution to stdout.

To have a quick fix for the curl error of idq before we fix it, please comment out line 55 in the makefile and try compiling again (If necessary, repeat that for every curl that didn't work). You can add the binary of idq later on, but BoSyHyper does not use it.

Thank you @nimetz
I have made the changes as you said, check new log files below
make_log.txt
hyperLTL_output_log.txt

suggest me further changes to fix the issue.

from bosy.

Seems fine, to execute synthesis you need to add the --synthesize flag to the call, otherwise only realizability is checked:
swift run -c release BoSyHyper --synthesize Samples/HyperLTL/SecretDecision.bosy

The unsupported logic error is an error from z3, based on your make output I would assume the correct z3 version is installed. You should validate that the z3 --version is 4.8.7.

from bosy.

Seems fine, to execute synthesis you need to add the --synthesize flag to the call, otherwise only realizability is checked:
swift run -c release BoSyHyper --synthesize Samples/HyperLTL/SecretDecision.bosy

The unsupported logic error is an error from z3, based on your make output I would assume the correct z3 version is installed. You should validate that the z3 --version is 4.8.7.

I have the latest version of z3 which is 4.8.10, So i need to downgrade to use this tool?
I think the tool is working fine now, kindly confirm, check below file
hyperLTL_output_log.txt

from bosy.

yes, looks fine!

from bosy.