Re: [Spot] Bug in ltlsynt - lar algorithm

Hello, I am indeed running ltlsynt via syfco exactly as you mention. The 0 at the end of iimc's output does mean SUCCESS (1 means failure). I seem to have pointed out the wrong benchmark, sorry for that. The one for which model checking fails for me is prioritized_arbiter_enc_2.tlsf. It should be available from the same repository I linked earlier. The output I get from ltlsynt algo=lar is attached. Let me know if you need more information, Guillermo PS: Thanks a million for reminding me about the licenses! I will start uploading them ASAP. On 18/06/2019, 12:01, "Alexandre Duret-Lutz" <adl(a)lrde.epita.fr> wrote: On Mon, Jun 17, 2019 at 8:41 PM Guillermo Alberto Perez <GuillermoAlberto.Perez(a)uantwerpen.be> wrote: 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