Comments (11)
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.
Related Issues (7)
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.
from bosy.