Perl 6 - the future is here, just unevenly distributed

IRC log for #divine, 2014-08-01

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

All times shown according to UTC.

Time Nick Message
00:06 mornfall also, http://arxiv.org/pdf/1303.5956 :-)
03:25 mornfall http://videos.rennes.inria.fr/GIPSy/Moshe-Vardi/gipsy11.pdf (formátování děsivý, ale obsah zajímavej)
03:52 ilbot3 joined #divine
03:52 Topic for #divine is now DIVINE: A Parallel LTL Model Checker (http://divine.fi.muni.cz) | http://irclog.perlgeek.de/divine/
07:36 xstill co je TLA?
08:52 xstill no ale jak tak koukám na wikipedii tak mi příjde, že TLA popisuje konečné běhy, takže to není úplně náhrada za LTL
08:59 xstill aha tak jsem konečně snad našel něco kde to vysvětlují
09:08 mornfall WP je k ničemu
09:08 mornfall http://research.microsoft.com/pubs/64074/lamport-actions.pdf
09:09 xstill ha, jsem čekal že když jsi psal v 5 tak se probudíš až odpoledne :-)
09:10 mornfall má to dva mínusy, jednak se zdá že ta stuttering-invariance není tak růžová jak Lamport tvrdí...
09:10 mornfall a druhak by to znamenalo rozšířit buchi automaty
09:16 mornfall (teda, on sice všude píše že TLA formule jsou stutter-invariant, ale nedokážu to z tý definice vyčíst nikde... řekl bych že to platí jen když pro ∀podformuli G[A]_f platí že f ⊆ var(A) ...
09:16 mornfall )
09:17 mornfall (G ≡ box)
09:17 mornfall eh, a myslel jsem var(A) ⊆ f samo sebou...
09:40 mornfall aha! já su totiž tak trochu idiot
09:40 mornfall ta stuttering invariance funguje, jen bych se musel zamyslet
09:40 mornfall oooh, shiny
10:14 xstill jo, budeš psát ten závěr, nebo mám zkusit něco vyplodit a jen to zkontroluješ?
10:31 mornfall kruci :-) nějak jsem se zabral do dizertačky
10:31 mornfall jo kouknu se na to
10:44 xstill dík
11:05 mornfall no, svn up... horší je že jsem zase propálil page limit o 3/4 stránky
11:06 mornfall něco půjde zachránit redistribucí grafů na [t] místo [p]
11:07 xstill zkusím si s tím pohrát
11:08 mornfall (topfraction nepomáhá, bude se to muset v textu posunout)
11:09 mornfall dal bych to ještě teda přečíst Jiříkovi, třeba něco poškrtá
11:10 mornfall taky jde pokrátit reference (třeba smazáním plných názvů konferencí se ušetří několik řádek, nejspíš)
11:11 xstill taky jde
11:19 mornfall trochu jsem to pokrátil ten bib
11:20 mornfall jdu od toho, dělej co umíš :D
11:30 xstill no my máme spoustu volnýho místa kolem figur, to musí jít nějak přeuspořádat
12:12 mornfall řekl bych, že divine na hashtabulce se šťastně zacyklil
12:13 xstill super
12:14 xstill a zacyklil se v tabulce v modelu, nebo v tabulce ve visitoru :-D?
12:15 mornfall :-))) to zjistím až dostanu na auru použitelný gdb... snad
12:15 mornfall i když se bojim že až uvidí 60 vláken v kombinaci s divineovýma symbolama, tak z toho hodí core ;P
12:16 xstill :-D
12:16 mornfall 50360912 stavů to zatím vygenerovalo
12:16 xstill jo už potřebujeme ušetřit jen 9 řádků
12:17 xstill to je dost
12:17 mornfall za starých dobrých časů by tam Jiřík nacpal a bylo by :P
12:17 mornfall nacpal pslatex*
12:17 xstill to je co?
12:17 mornfall (tzn. times new roman jako body font)
12:18 mornfall ve frontě je 2424642 stavů... to taky není zrovna málo
12:18 xstill jako pořát máme dost místa okolo floatů, ale texu se moc nechce pod dva floaty ještě vrazit půl odstavce
12:18 mornfall no, tam už možná \renewcommand{\topfraction}{.80} pomůže
12:19 xstill to je co?
12:19 mornfall povolí 80% stránky zabrat top floatama
12:19 xstill :-)
12:19 mornfall pagelimit je věčný nepřítel :-)
12:20 mornfall \raggedbottom \sloppy taky třeba :-)
12:25 xstill sláva
12:27 mornfall kulový se zacyklilo, rehashuje jak o život na jednom vlákně a zbylých 59 busy-cyklí na spinlocku
12:27 xstill tak už jsme na 12 stránkách
12:27 xstill :-(
12:27 xstill ten bug by to chtělo opravit
12:27 mornfall tak, v brick-hashset je opravenej, otázka jestli radši portovat fix nebo divine :-)
12:28 mornfall ale začíná to být dost akutní teda
12:28 mornfall a mám interního oponenta... docent Kopeček
12:28 xstill no já bych byl pro portovat divine na bricks
12:28 mornfall já taky, to je taky ten důvod proč to ještě není :D
12:28 xstill akorát teda tam zůstanou i věci co budo ve wibble asi :-(
12:29 mornfall to jde dělat po kouskách, jak s tím commandline
12:29 xstill jo
12:30 mornfall zkusim to nějak dneska umlátit čepicí, aspoň ten hashset
12:30 mornfall jinak to nebude zverifikovaný ani do vánoc
12:30 xstill jo počkej pošlu ti patche jak jsem čistil include
12:33 xstill jo Kopečka jsem jednou viděl, na informatickém semináři
12:33 mornfall on to má na starosti co pamatuju
12:41 xstill teda na to aby člověk zkompiloval celej divine by to chtělo alespoň 4 jádra 16GB paměti
12:42 xstill jenže to bych asi musel mít větší počítač
12:44 xstill jo zětšil jsem ten font u grafů, je zhruba tak velkej jako ty popisky, tak je to snad ok
12:47 mornfall pod tabulky by se snesl negativní vspace, kdyby někdo potřeboval něco připsat ještě
12:48 mornfall jinak super
12:48 mornfall Jiřík a poslat :-)
12:48 mornfall (i když asi bychom si to měli přečíst ještě všichni, odshora dolů...)
12:50 xstill jo
12:53 xstill Jiříkovi asi napíšu mail, protže on tady dneska není
12:54 xstill a aby toho nebylo málo tak já tady možná nebudu v pondělí
12:56 xstill hm, "This work has been partially supported by ..." byla něčím nebo to mám smazat?
13:30 xstill hm, máme context-switch-directed search, context-switch directed search a i context switch directed reachability, co je správně?
13:44 xstill totéž u thread-id, i když tady bych řekl, že by to mělo být bez pomlčky
14:29 xstill tak jo, ještě jsem si to přečetl a opravil pár drobností. ty pomlčky jsem ale nechal na tebe protože nevím co je správně
15:15 mornfall podstatný jména bez pomlček, přídavný s pomlčkama
15:15 mornfall a navíc jsou to spojovníky :D
17:09 xstill hele divine dokáže vstřebat 16MB .bc soubor :-)
19:22 xstill hm, to že divine inicializuje fifo matrix i v shared je poněkud zbytečné
19:23 xstill ale hlavně to teda brání tomu aby se dal z algoritmu udělat model
19:26 xstill jo a ten padding ve fifo je podle mě úplně blbě
19:47 xstill asi budu muset přes víkend portovat divine na brick asserty a vůbec co půjde
20:03 xstill hm, ty patche co jsem ti poslal nejsou kompletní
20:06 xstill (posílám znova)
21:01 xstill mornfall: kde jsi vzal to fungující gdb na auře?
21:06 xstill hm, asi to chce llvm splitter pro ntree

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