Perl 6 - the future is here, just unevenly distributed

IRC log for #divine, 2013-12-14

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

All times shown according to UTC.

Time Nick Message
00:14 mornfall (8/18) BitTuple: ./tmp/rpmout/BUILD/divine-3.0.91+pre4614/divine/toolkit/bittuple.test.h: 34: assertion `a == b' failed; got [42] != [11] instead
00:15 mornfall něco v tom bittuple není dobře...
02:47 _ilbot joined #divine
02:47 Topic for #divine is now DIVINE: A Parallel LTL Model Checker (http://divine.fi.muni.cz) | http://irclog.perlgeek.de/divine/
04:14 xstill joined #divine
08:26 xstill super, jo a to gcc 4.8.2 kompilovalo libdivine skoro 6 hodin
08:29 xstill ubuntu 13.4 padá protože nemá CMD_LLVMGOLD
08:30 xstill hm, a minimálně na windows se nám nějak dostalo -fno-exceptions do wibble
08:32 xstill aha, jo problém je že jsi vypnul exception handling v execution a ono includuje wibble/string.h kterej někde používá výjimky
08:33 xstill proč vlastně builduješ execution bez výjimek?
09:24 mornfall přišlo mi zbytečný generovat 2MB unwind tabulek (hlavně to je extra symbol pro každou vygenerovanou fci)
09:26 mornfall to je zase nějaká divnost
09:26 mornfall xstill: jo, ten throw je jen v #ifdef _WIN32 kolem toho to_string :\
09:27 xstill jo no
09:30 mornfall ale tak to nijak nehoří
09:44 mornfall LLVMgold.so to nenajde protože hledá ve /var/empty :-P
09:44 mornfall sed -e 's^/usr\([ /]\|$\)^/var/empty\1^g' -e 's^/opt\([ /]\|$\)^/var/empty\1^g' < "$fn" >            "$fn.tmp"
09:46 mornfall takže zbývá exceptions.sh na 32b, bug v ConcurrentHashSet... a ten mutex v draw bych mohl opravit :)
10:38 xstill proč se hledal v /var/empty?
10:39 mornfall protože ten sed
10:40 xstill a ten byl kde?
10:40 xstill taková zákeřná věc
10:40 mornfall to dělá nixpkgs v cmake hooku
10:41 mornfall ono to existuje protože nixpkgs běhá aj na ne-nixosu
10:41 xstill jo aby se tam nenahledaly věci mimo nix
11:12 xstill mornfall: hele spin je v nixpkgs, až uděláme release měli bysme tam protlačit divine :-D
11:12 mornfall to je asi nejmenší problém
11:17 mornfall blížíme se ke kulatému 5000. patchi...
11:19 xstill kde to vidís?
11:19 mornfall timeline v tracu
11:19 mornfall 4616
11:19 xstill v status jsou nějaká cisla kolem 4600
11:20 xstill ale jo tak blízíme se
11:20 xstill (proc mi nefungují písmena s hácky?)
11:20 mornfall máš to rozbitý, počítám :D
11:21 xstill jo no
11:43 xstill jakej formát automatu produkuje LTL2BA v DIVINE?
11:44 mornfall to externí? asi dve
11:45 xstill a jak to funguje když verifikuješ třeba LLVM s LTL?
11:45 xstill to se ta LTL přeloží na DVE a nad tím se udělá product?
11:45 mornfall ne, tam je nějaký API
11:46 mornfall žádnej fromát se negeneruje
11:46 mornfall (když chceš llvm+ltl teda)
11:46 xstill takže to generuje nějaký interní struktury který divine pozná
11:46 xstill ?
11:47 mornfall jo, on to někdo zabalil, viz divine/utility/buchi.*
11:48 xstill já že jsem se koukal na ten SPOT
11:49 xstill nezdá se, že by úplně měli knihovnu
11:49 mornfall mně to taky dost přišlo že nemaj
11:49 xstill navíc je to teda GPL takže to asi není moc ideální k přidání k divine
11:49 Erbureth ltl2ba generuje BA struktury
12:01 mornfall je to kříž, no
12:04 mornfall xstill: povedlo se ti to přeložit?
12:05 mornfall jako public headerů to má dost
12:07 mornfall a maj nějaký SPOT_API #define kterým značí třídy
12:09 mornfall ale hlavně teda nepoužívaj klasický buchi automaty ale TGBA
12:10 mornfall (umí teda aj BA, ale zdá se že TGBA je pro LTL lepší formalismus...)
12:22 xstill no přeložit se mi to povedlo
12:23 xstill dokonce mám i expression
12:23 xstill a zkoušel jsem tu utilitu
12:23 xstill ale do zdrojáků jsem se ještě nekoukal
12:23 xstill ale s tím TBGA zase neumíme pracovat, ne?
12:23 mornfall neumíme
12:24 mornfall nemáme na to algoritmy
12:24 mornfall :-)
12:29 xstill potom je otázka jak moc dobrej maj degeneralizátor
12:32 xstill přes vánoce se na to musím pořádně podívat
13:12 mornfall btw. shodou okolností spot a ltl3ba pro těch pár formulí co jsem zkusil generujou docela stejný automaty
13:13 mornfall http://spot.lip6.fr/ltl2tgba.html
13:34 xstill zajímavé
14:08 mornfall jaký máte program na úterý a na středu?
14:08 mornfall (a kde je spito furt? :)
18:08 _ilbot joined #divine
18:08 Topic for #divine is now DIVINE: A Parallel LTL Model Checker (http://divine.fi.muni.cz) | http://irclog.perlgeek.de/divine/
18:36 xstill mornfall: na úterý písemka z automatů 9 - 11:30 nebo tak něco
18:37 xstill a ve středu sítě 14-16
18:37 xstill + oba dny učím jako obvykle od 16
18:37 mornfall na ty sítě se chceš aj učit? (jak tě znám tak asi jo.... :P)
18:39 xstill už jsem se na ně učil až moc mi příjde
18:39 xstill a ještě jsem si to ani nepřečetl celý
18:39 xstill spíš bych se měl učit automaty
18:40 xstill u těch sítí mě asi známka zas tak neštve
18:41 xstill hm, možná jsem se nejdřív měl podívat na muny a pak se teprve (ne)jít učit
18:42 mornfall možná bychom mohli dát sraz na středu, dořešit co je potřeba a možná nějak nahodit tu iSCSI věc
18:42 xstill "Ako je digitalizovaný zvukový záznam? Uveďte tri formáty zvukového záznamu." wtf tohle dělá v sítích
18:43 mornfall asi nemyslí PCM a PDM ... :-)
18:43 xstill jo středa by asi byla lepší
18:43 mornfall a DM by mohlo být třetí
19:48 spito joined #divine
19:51 spito mornfall: tak už jsem tu
19:51 mornfall :-)
19:51 spito a překvapivě se učím
19:52 spito měl bych otázku (nekamenovat prosím)
19:53 spito LTL formule: a R (b R c)
19:54 spito když si z toho vyrobím BA, tak nějak stále nechápu přechod z iniciálního stavu pod (c && a) do stavu 1
19:54 spito http://www.lsv.ens-cachan.fr/~gastin/ltl2ba/index.php
20:00 xstill hm, typoval bych že ltl2ba nebude ten standartní algoritmus z přednášky, bude tam magie navíc
20:00 xstill vzhledem k tomu, že ltl2ba se reáně používá
20:01 xstill ale teda to c && a asi smysl dává
20:01 xstill protože release (x R y) znamená: Buď platí teď x i y, nebo platí y až do té doby než platí x && y (doufám)
20:01 mornfall typoval, to ses naučil v Haskellu? :)
20:02 xstill (já se pravopis nikdy neučil)
20:03 xstill spíš by mě ale zajímalo, proč je ta smyčka pod c nad init
20:05 mornfall a R b ... a "is released" by b, tzn. a musí platit než přijde b a osvobodí ho
20:05 spito mornfall: jo, to jsem pochopil
20:05 mornfall (obráceně)
20:05 mornfall a releases b ;-)
20:05 mornfall se to čte
20:05 spito jojo
20:06 xstill jo no, taky mám pocit, že release je lehce divnej
20:06 mornfall lepší než until :P
20:06 spito ten mi přijde jednodušší
20:06 mornfall nevim
20:07 mornfall ono asi samo o sobÄ› to je jedno
20:07 mornfall a jak se to začne vnořovat tak je to všechno stejně zlý
20:08 mornfall radši bych psal (omega)regexy teda :-)
20:08 xstill není ta formule docela zvrhlá?
20:09 xstill může být třeba tohle platný běh: c, c, c && a, c, c, c && b?
20:10 xstill release je weak, nebo ne?
20:10 mornfall na to aby a mohlo osvobodit b musí ho potkat :-)
20:11 mornfall aha, to je to druhý
20:11 mornfall ano, může to platit donekonečna
20:11 mornfall (tzn. a nemusí nikdy nastat)
20:11 xstill no ale a neosvobozuje b ale b R c
20:12 xstill pak už ten automat začínám chápat
20:12 mornfall no myslel jsem v a R b
20:12 mornfall máme zmatek ve formulích
20:12 spito mornfall: jestli to tedy chápu dobře, tak - vesele si jedu céčka a přechodem a&&c osvobodím b R c, ale ta samotná se musí případně umět osvobodit
20:14 xstill (já bych řekl, že jo)
20:16 mornfall no, (b R c) musí aspoň jednou platit, takže bez bčka neutečeš
20:16 spito ujištění: genBA umí všechny omega reg jazyky a je pro všechny deterministický, BA umí být determ. jen pro star-free, pro zbytek je nedeterm.?
20:18 xstill ani genBA neumí být deterministický vždy, ne?
20:19 * mornfall neví... na úplnÄ› deterministický asi potÅ™ebujeÅ¡ reject stavy
20:19 mornfall resp. množiny
20:19 xstill nebo umíš konečně mnoho a na genBA deterministicky?
20:20 xstill hm, nezachovává degeneralizace determinismus?
20:22 xstill podle mÄ› jo
21:48 xstill spito: budeš se učit převod MSO <-> automat?
21:49 xstill mně to příjde jako moc velkej opruz
21:57 spito xstill: na automaty?
21:57 spito no, já nevim
21:57 spito mám šanci na lepší známku jak E, tak asi jo
21:57 spito tedy v mém případě učit se <=> podívat se na to a mít iluzi toho, že jsem to pochopil
22:11 xstill jo na automaty. Mně to příjde dost dlouhý, potřeboval bych vědět jestli to Křetínskej fakt chce. Ale tak asi se na to podívám.
22:12 xstill protože totiž pokud tam bude příklad na převod a nebude podmínka, že to musí být ten alg. tak se to dá udělat "od oka"
22:36 zbeasnyy joined #divine

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