Perl 6 - the future is here, just unevenly distributed

IRC log for #divine, 2013-05-09

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

All times shown according to UTC.

Time Nick Message
06:08 xstill sakra, na většině dve je komprese záporná
06:15 spito joined #divine
06:21 xstill spito: na auře už moc neměřím
06:29 xstill mornfall: budeš mezi 9 a 10 na FI?
06:30 xstill mornfall: moc tě nezdržím
06:35 mornfall No, v devět mi jede vlak, takže až v těch deset.
08:00 spito joined #divine
08:07 spito mornfall: a přijdeš tedy do labu?
09:59 xstill mornfall: tak nic už tě tu nestíhám, začíná mi další hodina
11:28 mornfall No, nestihneš, hlavně jsem už ve dvanáct seděl ve vlaku. :-)
11:28 mornfall Spito měl větší štěstí
11:28 mornfall xstill: Tak to vyřešíme tady až budeš.
16:00 spito joined #divine
17:03 xstill mornfall: to že mi klesne kompresní poměr při LTL verifikaci asi není v pořádku, co?
17:53 xstill statistiky jsou podezřelé
17:54 xstill celá inicializace je naprosto v pořádku, pak to bouchne
17:54 xstill to znamená, že stavy v pohodě uložím a pak mi někde leaknou
18:00 spito joined #divine
18:05 xstill spito: doufám že jsi dneska pochodil lépe než já, momentálně se snažím napsat něco o model-checkingu a našel jsem leak v NTree
18:06 spito xstill: já nevim, nabastlim nějaký úvod a snad to budu mít
18:07 spito jinak mě ještě čeká vytahování jednotlivých tabulek z divajnu někam do separátna
18:08 xstill tak to už by neměl být takový problém ne?
18:09 xstill já jsem zjistil, že v LTL leaknu velkou část stavového prostoru.
18:12 xstill uvidím co na to řekne valgrind
18:15 xstill ach jo, já nedokážu popsat jak se od programu dostanu ke grafu, je něco použitelného v manuálu?
18:17 spito no, to samé mi zkritizoval mornfall
18:17 spito prý v LLVM sekci něco je
18:17 xstill ok
18:18 spito však se můžeš kouknout, co jsem měl napsáno já
18:18 spito antea: já/bc/text/bc.pdf
18:23 xstill díky
18:23 spito ale mám to špatně
18:23 spito skoro celé :D
18:23 spito tedy ten úvod
18:23 spito to je prostě peklo největš
18:23 spito í
18:29 xstill ten manuál je veselej, ale nic použitelnýho do bc, třeba tohle: "If you have ever changed a program and watched the test-case run in a loop for hundreds of iterations, wondering if the bug is really fixed, or it just stubbornly refuses to crash the program… well, DIVINE is the tool you have been waiting for."
18:33 xstill jinak je ještě veselý, že mi asi arch vypíná debug, protože se mi to stalo i na počítači doma, zcel nezávisle od noťasu
18:36 Erbureth už aby fungovalo divine verify divine, co? :)
18:40 xstill no ono by mi teď úplně stačilo kdyby valgrind nespomaloval výpočet tak 1000x
18:49 xstill mornfall: někdo rozbil timed, a dost vesele, assertí to na počkání (a to je ještě bez těch změn co jsem dělal včera, je to mainline z 4.5.)
18:50 xstill hmm na antee to neasertí
18:52 xstill že by se mi povedlo udělat vadný build na dvou strojích?
19:10 xstill tak to byl fakt vadný build, je možná na čase uvážit nějakou stabinější distribuci, to že distribuce ovlivní buildování by se fakt stávat nemělo
19:11 mornfall Jak vadný build?
19:14 xstill no ono když človÄ›k odmaže NDEBUG z nÄ›kterých  flags.make a jinde ho nechá tak to nedÄ›lá dobrotu
19:14 xstill mornfall: máš představu kde by mohlo leakovat specificky LTL?
19:17 mornfall Zajímavé.
19:17 mornfall xstill: I když pouštíš metrics třeba?
19:18 xstill zajímavý dotaz, to jsem nezkoušel, ale předpokládám že to leakovat nebude
19:18 mornfall Z hlediska stavu nejde poznat jestli tam LTL je nebo není.
19:18 xstill otestuju
19:18 mornfall Tak jestli to třeba není to že leakuje OWCTY bez ohledu na LTL.
19:18 xstill no při owcty to je ve fázi reachability
19:19 xstill mornfall: není, protože leakuje i nested-dfs
19:20 xstill nejsem si teď jistý jestli jsem testoval map
19:24 xstill mornfall: no tak metrics má vše naprosto v pořádku, 3x tolik stavů a v podstatě stejně paměti jako bez LTL
19:24 xstill podle mě je problém v dalších iteracích
19:28 xstill mornfall: ještě jsem k sobě na web nahrál novou verzi bc práce, je tam k úvodu přidáno něco víc o model checkingu, tak kdyby jsi se na to podíval...
19:31 xstill map v druhé iteraci zdá se neexplodoval
19:32 mornfall Zajímavé.
19:33 xstill už vím proč
19:33 xstill ten disown v OWCTY je Å¡patnÄ›
19:34 xstill protože do queueAny to dáváš hodnotou
19:34 xstill udělám patch
19:35 xstill to leakne celou tabulku no
19:35 mornfall :-)
19:39 xstill no on totiž jedinej validní disown je ten  v nested-dfs
19:39 xstill a teda ltlce
19:40 xstill nicméně mě aspoň může tešit že jsem to našel dřív než valgrind
19:41 mornfall :-)
19:42 mornfall Já je tam nasekal dost od boku.
19:42 xstill a víš co to ještě znamená?
19:42 mornfall A pak na to zapomněl. :-)
19:42 mornfall Co?
19:43 xstill že až dáš moje patche do mainline tak Enrico už nebude na 2. místě sám ;-)
19:44 mornfall :D
19:49 xstill jinak mě dost překvapilo, že formule co je k fisher9 platí jen u něj a ne u větších instancí
19:49 xstill což mi efektivně brání v rozumném měření LTL nad timed protože mám 1 model kde to má platnou property
19:50 xstill a teda nad llvm zase chybí property u větších modelů
19:58 xstill mornfall: ono se to nějak rozbilo, už jsem v 12 iteraci
20:00 xstill ach jo já jsem idiot
20:02 xstill já jsem viděl Vertex ale už mi nedošlo, že ten stav se tam dává jako druhý parametr, tedy node a ten disown tam být asi má
20:04 xstill mornfall: chyba je jinde
20:04 xstill mornfall: proč se při OWCTY použávají IPC frony i když je tam jen jeden thread
20:06 xstill to se pak člověk divý, když se mu nacpe všechno jako to stav do IPC fronty, žejo
20:08 xstill no jasně takže tím jsou viníci jasní, u OWCY za to může IPC fronta u NDFS stack
20:09 xstill fuj, jdu přeměřit všechno MAP-em, ještě že ho máme
20:38 mornfall No, OWCTY používá IPC fronty protože on potřebuje vyrobit transition z toho že zná "to".
20:38 mornfall Do lokální fronty to nacpat nejde, to bys do ní musel cpát následníky a ne from stavy.
20:38 mornfall A to by pak taky nešla komprimovat.
20:40 mornfall --> zzz
20:51 xstill no jo, postupně mi to nějak došlo, zatím funguje MAP dobře, ale komprese nutně potřebuje shared
20:51 xstill jdu taky spát
20:52 spito přebírám to tu
21:37 spito left #divine

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