Perl 6 - the future is here, just unevenly distributed

IRC log for #divine, 2014-06-11

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

All times shown according to UTC.

Time Nick Message
07:46 xbarnat joined #divine
07:46 xbarnat Hola. Vite nekdo jak se ma divine k modelum, ktere maji vicero inicialnich stavu?
07:47 xbarnat Je to uplna blbost a nemelo by se to povolovat, ze? :-)
07:49 xbarnat Zase ale nadruhou stranu v dokumentaci (konkretne v sekci CESMI) je to povoleno ...
07:49 xbarnat No ale pak treba counterexample trace 0,0,0 je nejasny, protoze chybi informace ze ktereho inicialniho stavu se ten trace ma delat ...
07:50 xbarnat minimalne tedy report potrebuje info o CE-init-state
08:28 xbarnat a co je to safety u CESMI ?
08:30 xbarnat aha to je nereachabilita goal-state ...
09:29 mornfall xbarnat: informace nechybí, první číslo je číslo iniciálního stavu
10:14 xbarnat aha
10:15 xbarnat no ale nasel jsem bug, pro dosazitelnost goal state se v CESMI negeneruje dobre protipriklad
10:17 mornfall ukaž
10:20 xbarnat poslal jsem patch na divine@fi.muni.cz
10:20 mornfall třeba jednou dorazí
10:21 xbarnat uz
10:21 xbarnat (poslal jsem ho darcs send) a to nedorazil, tak jsem ho preposlal rucne (darcs send -o ...)
10:25 mornfall chvíli to potrvá, musim přeložit divine s cesmi
10:35 mornfall searching... 1 states, 0 edges, GOAL
10:35 mornfall to je zajímavej protipříklad
10:36 mornfall hm, tos mohl rovnou říct že to nefunguje když je iniciální stav goal
10:38 xbarnat no me to napise zejo otazniky ...
10:38 mornfall divine draw --label :)
10:38 mornfall --labels
10:38 xbarnat a co jako draw funguje no
10:40 mornfall no že tam je jasně vidět co je problém
10:40 xbarnat j tak ...
10:40 mornfall s více iniciálníma stavama to každopádně nesouvisí
10:40 xbarnat no na tom prikladu, co posilal tom kratochvila je ten otaznikovej protipriklad delsi ...
10:40 mornfall když vyrobim model s jedním stavem kterej je zároveň goal tak se to rozsype
10:40 xbarnat aha ok
10:41 xbarnat nj, ale u toho tomova prikladu nelze spolehat na to, ze se nekde neco neprepisuje ...
10:58 mornfall no, naopak, lze se spoléhat že přepisuje
10:59 mornfall když to přeložim s -O2 dostanu výrazně jinej stavovej prostor než s -O0
11:00 mornfall ten model je blbě, ostatně jako všechny co jsem od něj kdy viděl
11:06 xbarnat nj, co nadelame ... otazka je, jak mu pomoct, ze ...
11:08 xbarnat ostatne stoji to na nsimulinku, co implementoval Nikola ...
11:08 mornfall říkal jsem si že ten kód nevypadá jako Tom...
11:10 xstill joined #divine
11:14 xHire joined #divine
11:17 xbarnat nj, kdyz se to prelozi jako -DSTANDALONE a pusti s valgrindem, tak to pise nejake chyby
11:18 xHire joined #divine
11:39 xbarnat tak potvrzeno, neinicializovana promena v nsimulink.h ...  Takze jedine co zbyva je odstranit tu chybu s protiprikladem, kdyz goal state je rovnou ten inicialni stav.
12:08 mornfall no, tak jsem si tu proměnnou nezávisle našel taky...
12:08 mornfall radost
12:24 mornfall ale ta odpověď, to je za všechny drobný
12:29 xHire joined #divine
12:43 xHire joined #divine
17:37 xstill ta protipříkladová chyba je cesmi specific, nebo je to obecně nějaká blbost v ltlce?
17:38 mornfall myslim že to s cesmi nic nemá, ale ještě jsem to nezkusil :)
17:39 xstill ono to by dávalo smysl, jen teda mě nenapadá, co by se tam mohlo podělat
17:39 xstill je to teda iniciální = goal?
17:39 mornfall jo
17:41 xstill aha, no podle mě totiž ve skutečnosti trace nezačíná iniciálním stavem, ale jeho prvním následníkem (typuju)
17:41 xstill empty.dve má deadlock na iniciální, nezobrazí nic v ce-init
17:42 mornfall to je ta chyba, jo :)
17:43 xstill to je ale divný, protože kdyby to fakt začínalo od následníka initu, tak simulate-counterexample (a pravděpodobně ani draw trace) nebude fungovat
17:43 mornfall přesně tak :)
17:43 mornfall zkus si udělat jednokrokovej protipříklad
17:44 xstill momentálně bych potřeboval vůbec v testech najít dve model co má deadlock :-D
17:44 mornfall CE-Init: 1,2
17:46 xstill to bude nějakej debilní bug, protože přesně ten jednokrokovej protipříklad padal když jsem to předělával, takže jsem ho "opravil"
17:46 mornfall :-)))
17:47 mornfall dokonce správně dostanu aj CE-Init: 2,2
17:48 mornfall (protipříklad z druhýho iniciálního stavu)
17:48 xstill do dokáže jen cesmi, že?
17:48 mornfall nevim
17:48 mornfall asi :)
17:48 mornfall chtěl jsem říct murphi, ale ten se stejně překládá na cesmi
17:49 xstill to jsem nikdy ani neviděl
17:49 mornfall tak, to je taková Jiříkovina ;-)) asi jako probabilistic llvm :)
17:53 xstill hm, to je super, gdb mi sežralo 4GB paměti snažíc se natáhnout symboly z debug divine
17:54 xstill potřebuju menší build aby se dal debugovat…
17:55 xstill škoda že 16GB paměti pořád stojí docela dost
17:55 xstill na to jak často by to člověk reálně využil
17:57 mornfall hlavně když máš 2 4GiB moduly
17:57 mornfall (jako třeba já)
17:57 mornfall ale budu mít mSATA SSD :-) už zítra
17:57 mornfall půl terabajtu v laptopu, solid state, win :)
17:58 xstill :-)
17:58 xstill no právě, taky mám 2 4GB moduly
18:00 mornfall tak, pokud zůstanu u RH, tak někdy na vánoce 2015 budu updatovat HW, prozatím bude muset 8G stačit
18:00 xstill jo, chybu jsem identifikoval, udělám a pošlu patch
18:00 xstill jako že budeš mít novej laptop?
18:00 mornfall (trapný teda je, že to co mám je poslední model s mSATA slotem)
18:00 mornfall jo
18:00 xstill to je trapný ovšem
18:01 xstill a vůbec x240 se mi nelíbila
18:01 xstill měli zůstat u konzervativního vzhledu
18:01 mornfall :) mně aj docela jo, ale neměl jsem to v ruce
18:01 mornfall tak, já mam chiclet klávesnici už teď :-)
18:01 xstill to nevadí, ale x240 jí má menší myslím a větší touchpad
18:01 xstill a divný panty
18:02 mornfall hmm, ale upgrade disku v NASu vyjde na víc než to SSD
18:02 mornfall to není dobrý
18:02 xstill to kupuješ 4TB?
18:02 mornfall no, je tam 1T, takže míň než 3T upgrade nemá úplně smysl
18:02 mornfall 3T vyjde na 3.2kKč
18:03 mornfall 240G SSD jsem koupil za ~2.9
18:03 xstill aha, a co máš za SSD?
18:03 mornfall crucial m500
18:04 mornfall ten mSATA tady je 3Gb, a žádný další mSATA už nebude, takže nic lepšího nemá smysl
18:05 xstill hm, je to ale divný
18:05 mornfall co?
18:05 xstill ten ltlce
18:07 xstill ono to asi souvisí s tím, že shared().ce.initial není vůbec initial, ale naopak goal asi
18:08 mornfall ono se to nejmenuje is_ce_initial náhodou :-)
18:08 mornfall jo, shared().ce.initial je iniciální stav toho trace-u
18:09 mornfall možná bychom to mohli nazvat origin
18:13 mornfall no, 406 je chyba
18:13 xstill aha, začínám to chápat
18:13 mornfall succTrace přidává ID iniciálního stavu -- ale ne když je ten protipříklad jinak prázdnej
18:13 xstill no to vím, jen mi šlo o to jak se tam vůbec dostanu tak daleko
18:13 xstill už to vidím
18:16 xstill a typuju, že zjistíme, že test na empty.dve je blbě
18:17 mornfall tak, tam se testuje jen že tam ten deadlock je, jinak nic
18:17 mornfall celkově na protipříklady moc v testech nekoukáme
18:17 xstill aha, to by se zrovna v tomhle případě testovat mohl i protipříklad
18:21 xstill doprčic, já nemůžu jen tak zavolat whichInitial z succTrace
18:33 xstill jo ta chyba je sice na tom řádku ale opravit se musí úplně jidne
18:48 xstill hm tak teď by tu byl fix s jedním malým goto, zbývá to polidštit…
18:49 xstill (asi podruhé v životě jsem do vážně zamýšleného kódu napsal goto)
18:49 xstill (ale v tom minulém i zůstalo)
18:49 mornfall :-)
18:52 mornfall skoro bych řek, že chyba je že tam je successor_id 0
18:52 xstill no to je :-)
18:54 xstill a je to tím, že ten cyklus na 352 je napsaný "obráceně", prvně má být to testování na initial a pak teprve ten krok
18:54 xstill teda snad
18:54 mornfall žejo :-)
18:56 xstill to jsou ty chyby co se strašně blbě hledaj, protože se objeví v jednom specielním případě
18:56 xstill mám pocit, že tahle je (snad už jen byla) v divine dost častá
19:04 xstill patch poslán
19:06 mornfall :-)
19:11 mornfall yup, zdá se že to funguje
19:11 mornfall řekl bych že to že se to často vyskytuje je problém hlavně nedostatečných testů :)
19:11 xstill to už ti to došlo? Mě totiž ne
19:12 mornfall no, něco mi došlo :-)
19:12 xstill jo mě už taky
19:14 xstill ještě ti pošlu patch na to, že jsem před rokem pořádně nevěděl jak fungují šablony :-D
19:15 mornfall :D
19:16 xstill máš to tam
19:17 xstill (konečně zase jednou patch který ubírá kód)
19:19 mornfall :-)
19:19 mornfall pouštím na to nějaký testy, pak to pushnu
19:20 xstill jo, dve testy prošli, ostatní jsem nezkoušel
19:21 xstill *prošly
19:22 mornfall no, já chci asi hlavně vidět MPI a COMPRESSION
19:22 xstill hm, to je fakt
19:44 mornfall otázka je co s těma testama
19:46 mornfall chtělo by to nějaký jednoduchý asserty do simulate
19:46 mornfall "jsem v goal stavu", "zapamatuj si stav a", "jsem v a" :)
19:47 mornfall evaluace LTL na běhu by byla boží ;-)
19:50 mornfall (ne že bych tušil jak rozumně evaluovat atomický propozice...)
19:57 xstill asi tě  nechápu co cheš v tom simulate
20:05 mornfall no, napsat něco jako --trace=1,2,1,isgoal :-)
20:06 mornfall resp. --trace=1,2,3,save,2,1,check
20:07 mornfall tzn. šlo by jednoduše kontrolovat jestli ten protipříklad dává aspoň nějaký smysl
20:13 xstill no pokud chceš aby Marek časem dělal ten debugger, tak mu zadej na prázdniny toto ať se ttrochu sžije s divine jako takovým
20:13 mornfall :-)
20:14 xstill podle mě to totiž bude jednoduchý (celkem) ale dělat bych to nechtěl
20:14 xstill a simulate není tak strašnej kód aby se toho musal leknout
20:15 xstill pokud bude brát zbytek jako blackbox pro začátek
20:15 xstill to by moh i celý pochopit jak to simulate funguje relativně rychle
20:23 mornfall no uvidíme

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