reactive-systems/bosy

BoSy is a reactive synthesis tool based on constraint-solving

bosy's Issues

Build problems

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.

Error on dependencies when trying a fresh build

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

Build Error

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)

output.txt

[OSX] Couldn't posix_spawn error 8, when --synthesize option is passed to bosy

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 ?

`false` as guarantee leads to incorrect behavior

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.

Encounters error in running the example HyperLTL spec in BoSy

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

• Build Completed!info: Linear automaton contains 4 states
  info: Hyper automaton contains 1 states
  info: build encoding for bound 1
  (set-logic UFDTLIA)
  .
  .
  .
  Foundation/Process.swift:388: Fatal error: Error Domain=NSCocoaErrorDomain Code=260 "The file doesn’t exist."
  Illegal instruction (core dumped)
  ##########

I have added complete output as attachment file

Kindly help me to fix this issue.

Broken link to Vampire dependency

The link to dependency Vampire in ./Makefile is broken: http://forsyte.at/wp-content/uploads/vampire.zip