Perl 6 - the future is here, just unevenly distributed

IRC log for #divine, 2015-12-22

| Channels | #divine index | Today | | Search | Google Search | Plain-Text | summary

All times shown according to UTC.

Time Nick Message
22:48 xtomast1 joined #divine
23:19 xtomast1 ahoj, narazil jsem na problem pri vytvareni dalsich LTL prikladu, a jsem bohuzel tak v koncich, ze me nenapada nic lepsiho, nez se o nej podelit
23:20 xtomast1 jsem si vedom, ze nacasovani je to extremne spatne, takze si urcite nenechte zkazit svatky ci podobne a treba se na to podivejte, az/jestli budete mit nekdy cas
23:20 xtomast1 problem jsem zredukoval na velmi minimalisticky priklad: program http://pastebin.com/nChNSeJ2, prikaz divine verify sanity_ltl.bc --no-shared --fair -w 8 -d -p finished_ok, vysledek: vlastnost neplati a cyklus v protiprikladu je 4x ten uplne stejny stav, jen s jinym fairness id (diffoval jsem je), pricemz thread 0 je v busy loopu v entry.cpp, ale thread 1 je podle toho vypisu ve switch/case v mainu, dokonce primo na tom radku kde by se mela napln
23:20 xtomast1 it ta atomicka propozice, ktera je potreba, aby byla splnena verifikovana formule (uryvek: http://pastebin.com/Qm167fUk, je to bohuzel humus pres ty datatypy a spol. (ony to nejsou doopravdy konstanty, takze s nimi asi nic neudelam))
23:20 xtomast1 takze ten protipriklad dost nechapu, neprijde mi moc fer -- jak to, ze se thread 1 nepohne?
23:26 mornfall hm, chtělo by to entry.cpp
23:27 mornfall (ale podle čísel řádků to vypadá jako že v thread 0 už main spíš skončil)
23:29 mornfall dokonce bych řekl že ten protipříklad vypadá jako že je na F(a && Fb) nikoliv (Fa) && (Fb)
23:31 mornfall no nebo není...
23:31 mornfall ten thread 0 dělá nějaký haluze a bez entry.cpp asi nepoznáme jaký

| Channels | #divine index | Today | | Search | Google Search | Plain-Text | summary