On Mon, Jun 17, 2019 at 8:41 PM Guillermo Alberto Perez <GuillermoAlberto.Perez@uantwerpen.be> wrote:
Hello,
While running tests for SYNTCOMP 2019 we found that ltlsynt outputs an incorrect controller on one of our benchmarks:
simple_arbiter_enc_2.tlsf (available from https://bitbucket.org/swenjacobs/syntcomp/src/master/SelectedBenchmarks2018/...)
I am calling the tool with --aiger --algo=lar and using iimc as our model checker.
Hi Guillermo, Can you help me reproduce this? I'm unfamiliar with iimc and the process of checking the aiger output. So far I assume you do % IN=$(syfco simple_arbiter_enc_2.tlsf -ins) % OUT=$(syfco simple_arbiter_enc_2.tlsf -outs) % LTL=$(syfco simple_arbiter_enc_2.tlsf -f ltlxba -m fully) % ltlsynt --aiger --algo=lar --formula="$LTL" --ins="$IN" --outs="$OUT" >output.txt Then we split the REALIZABLE line from the aiger output: % head -1 output.txt REALIZABLE % sed 1d output.txt > output.aag Looking into StarExecSYNTCOMP/TLSF/synt-post-processor/process it seems the next steps are: % ./syfco --format smv simple_arbiter_enc_2.tlsf --mode fully | ./smvtoaig -L ./ltl2smv > monitor.aag % ./combine-aiger monitor.aag output.aag > combined.aag % ./iimc -t fork -t fair -t klive -t fcbmc -t join combined.aag rlim_cur: 8388608 rlim_max: 18446744073709551615 rlim_new: 33554432 0 And I understand that this last 0 is means SUCCESS, hence no issue? Also I've checked the intermediate DPA generated with --algo=lar, --algo=sd, and --algo=ds: the three are different, but they are all equivalent. They could still trigger a problem later, but as the remaining code is common to all cases, it's a bit less likely. PS: Beware the your StarExecSYNTCOMP github repository is distributing binaries without honoring the licenses of these tools. For instance IIMC's and syfco's license requires you to redistribute its LICENSE file; GPL-covered tools like ltlsynt additionally require a written offer to distribute to corresponding source, etc. -- Alexandre Duret-Lutz