Perl 6 - the future is here, just unevenly distributed

IRC log for #divine, 2014-09-21

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

All times shown according to UTC.

Time Nick Message
01:48 ilbot3 joined #divine
01:48 Topic for #divine is now DIVINE: A Parallel LTL Model Checker (http://divine.fi.muni.cz) | http://irclog.perlgeek.de/divine/
12:27 spito joined #divine
15:44 xstill mornfall: můžeš se mi mrknout na https://paradise.fi.muni.cz/~xstill/memics.pdf, jestli to alespoň trochu odpovídá?
15:45 xstill než mi to zítra zkritizují všichni ostatní…
15:46 mornfall assition (slajd 2)
15:47 mornfall člen v „gives counterexample“
15:47 mornfall asi bych psal spíš techniques for mitigating state-space explosion
15:49 mornfall kolik je na to času?
15:49 xstill ok, dík opraveno
15:49 xstill nevím
15:49 xstill musím se podívat
15:50 xstill to sem si asi mohl zjistit hned na začátku…
15:50 mornfall 2012 byl jeden slot 20 minut
15:51 xstill teď to nemůžu najít, ale 20 minut je dost podle mě
15:52 mornfall slajd 7 -- píšeš number of different countexamples ale to v tý tabulce nevidim?
15:52 xstill hm zato jsem našel že místnosti v hotelu je třeba rezervovat do konce měsíce
15:53 xstill aha, já blbec to odstranil ze slidu a v popisku nechal
15:53 xstill (se to tam nevešlo a není to až tak zajímavý)
15:54 mornfall slajd 3 -- asi bych řekl we primarily target (a bez here na konci), without negatively affecting verification of bug-free programs
15:54 mornfall jo a context switches bez spojovníku
15:54 mornfall (spojovník jen když to je celý jedno přídavný jméno)
15:55 mornfall to stejný model checking o slajd dál
15:57 mornfall a taky by asi bylo zajímavý udělat příklad kde bude mít něco indegree víc než 1
15:57 mornfall (a ideálně pod různým počtem CS)
15:57 xstill ten spojovník u model checking jsi myslel symbolic model checking na slidu 4?
15:58 mornfall jo, taky pak context-switches slajd 4 bod 2 a model checking slajd 12 předposlední bod
15:58 xstill a co explicit state model checking na slidu 2? ten taky?
15:59 mornfall jo, explicit-state model checking
15:59 mornfall hm, a v podnadpisu na slajdu 2 taky
15:59 mornfall a 4
15:59 mornfall ty podnadpisy jsou docela nenápadný
16:00 mornfall boldface text uvnitř slajdu by určitě upoutal víc
16:01 xstill takže state-space explosion se spojovníkem protože je to přídavné jméno?
16:01 mornfall jo, snad :)
16:01 xstill ok, začínám to snad chápat
16:02 mornfall stejně jako LLVM-translated nebo BFS-based
16:02 xstill ty podnadpisi nevím no, zkusím to boldem
16:06 xstill fuj zase; no nevím jestli to zase nepůsobí moc výrazně
16:06 xstill (aktualizováno)
16:06 xstill hm, složitější případ bych mohl zkusit vymyslet
16:07 xstill myslíš, že obsahově by to šlo (hlavně ten úvod jsem nevěděl moc co)
16:07 xstill ?
16:08 mornfall asi jo... možná budeš muset něco přidat ještě
16:08 mornfall jaj, Univerzity si oprav
16:09 xstill s tam má být?
16:09 mornfall jj
16:10 mornfall jo, taky by bylo dobrý zvýraznit šipky který dělaj CS
16:10 mornfall v příkladu
16:10 xstill no, zkoušel jsem na ně dát dvojšipku a to podle mě vypadalo divně, podívám se co tikz umí
16:11 mornfall můžeš je obarvit
16:11 mornfall nebo ostatní udělat přerušovaný
16:11 xstill hm, mohl bych je udělat červený asi
16:11 mornfall (nebo jenom použít tlustší čáru)
16:19 xstill jo to by šlo
19:43 xstill achjo, symdivine nejde zkompilovat a nix za to nemůže
19:47 xstill přitom poctivě zkopírovali wrappery na llvm hlavičky
20:10 xstill ok, tak za to nemůžou, to jen nemůžu kompilovat gcc protil llvmSelf

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