reactive-systems / bosy Goto Github PK
View Code? Open in Web Editor NEWBoSy is a reactive synthesis tool based on constraint-solving
Home Page: https://www.react.uni-saarland.de/tools/bosy/
License: GNU Affero General Public License v3.0
BoSy is a reactive synthesis tool based on constraint-solving
Home Page: https://www.react.uni-saarland.de/tools/bosy/
License: GNU Affero General Public License v3.0
The link to dependency Vampire in ./Makefile is broken: http://forsyte.at/wp-content/uploads/vampire.zip
As title, when I tried to use the --synthesize option on OSX, an error is reported.
And I think the issue is related to the use of some linux-64 bit binaries
For example, in Solver.swift line 528
it tries to launch a binary under Tools/quabscm, which turns out to be a 64bit ELF executable
When I checked the make file, it is downloaded from a dropbox link, with only the linux binary in it.
Under the folder Tools, there are actually 4 binaries that are ELF executable instead of Mac-O executable:
caqem, hqs-linux, quabscm,vampire, that can likely cause the same problem.
So I'm just wandering if you would kindly provide the Mac-Version binary as well ?
Just having a single guarantee false
causes both players to be winning.
The probable cause is the construction of the CoBüchiautomaton.
This is a corner case that may not be handled correctly while looking for rejecting sinks.
When building BoSy the cadet tool dependency causes an error due to an implicit function declaration.
Please find the compiler output attached.
Environment:
macOS 10.15.6
Apple clang version 12.0.0 (clang-1200.0.32.2)
Environment : Ubuntu 20.04
I have installed the swift
Done BoSy make
Installed other packages mentioned in the git page for Ubuntu 20.04
When I try to run : swift run -c release BoSyHyper Samples/HyperLTL/SecretDecision.bosy
I got the below error
##########
[1/1] Planning build
I have added complete output as attachment file
Kindly help me to fix this issue.
When trying to build, seems that there's an issue in Swift dependency graph file (I'm not sure of this, never used Swift before, I'm not sure how it handles dependencies).
cp Tools/spot-2.5/bin/ltl2tgba Tools/
swift build --configuration release -Xcc -O3 -Xcc -DNDEBUG -Xswiftc -Ounchecked
Updating https://github.com/ltentrup/CAiger.git
Updating https://github.com/ltentrup/SafetySynth.git
Updating https://github.com/apple/swift-package-manager.git
Updating https://github.com/ltentrup/CUDD.git
error: dependency graph is unresolvable; found these conflicting requirements:
Dependencies:
https://github.com/ltentrup/CAiger.git @ 0.1.0..<1.0.0
https://github.com/ltentrup/CUDD.git @ 0.2.0..<1.0.0
make: *** [Makefile:11: release] Error 1
Environment:
OS: macOS 10.13.3 Beta
swiftc version: 4.0.3
I got a few errors while trying to build bosy:
While building ltl3ba
:
cd Tools ; curl -OL https://sourceforge.net/projects/ltl3ba/files/ltl3ba/1.1/ltl3ba-1.1.3.tar.gz
% Total % Received % Xferd Average Speed Time Time Time Current
Dload Upload Total Spent Left Speed
0 0 0 0 0 0 0 0 --:--:-- --:--:-- --:--:-- 0
100 746 100 746 0 0 1286 0 --:--:-- --:--:-- --:--:-- 1286
cd Tools ; tar xzf ltl3ba-1.1.3.tar.gz
tar: Unrecognized archive format
tar: Error exit delayed from previous errors.
make: *** [Tools/ltl3ba-1.1.3] Error 1
rm Tools/ltl3ba-1.1.3.tar.gz
I downloaded the tarball manually from Sourceforge and edited out that part of the Makefile. Then:
cd Tools ; make -C ltl3ba-1.1.3
g++ -O3 -DNXT -I/usr/local/include/ -c -o parse.o parse.c
clang: warning: treating 'c' input as 'c++' when in C++ mode, this behavior is deprecated [-Wdeprecated]
In file included from parse.c:36:
./ltl3ba.h:40:10: fatal error: 'bdd.h' file not found
#include <bdd.h>
^~~~~~~
1 error generated.
make[1]: *** [parse.o] Error 1
make: *** [Tools/ltl3ba-1.1.3/ltl3ba] Error 2
I determined this is because ltl3ba requires BuDDy (according to that project's readme). So, I downloaded v 2.4 from Sourceforge, then:
tar xzf buddy-2.4.tar.gz
cd buddy-2.4
./configure && make
make install
I didn't mind installing these to my system, but ideally if this were a part of building these directories would be installed more locally.
After that things seem to go OK, although I got this warning on each file:
cd Tools ; make -C ltl3ba-1.1.3
g++ -O3 -DNXT -I/usr/local/include/ -c -o parse.o parse.c
clang: warning: treating 'c' input as 'c++' when in C++ mode, this behavior is deprecated [-Wdeprecated]
In file included from parse.c:36:
./ltl3ba.h:241:15: warning: 'print_set_out' has C-linkage specified, but returns user-defined type 'std::ostream &' (aka 'basic_ostream<char> &') which is incompatible with C [-Wreturn-type-c-linkage]
std::ostream& print_set_out(std::ostream &, int *, int);
^
1 warning generated.
After that, I ran the simple_arbiter sample and it seemed to work OK.
A declarative, efficient, and flexible JavaScript library for building user interfaces.
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
The Web framework for perfectionists with deadlines.
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
We are working to build community through open source technology. NB: members must have two-factor auth.
Open source projects and samples from Microsoft.
Google ❤️ Open Source for everyone.
Alibaba Open Source for everyone
Data-Driven Documents codes.
China tencent open source team.