Perl 6 - the future is here, just unevenly distributed

IRC log for #divine, 2015-04-05

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

All times shown according to UTC.

Time Nick Message
01:49 ilbot3 joined #divine
01:49 Topic for #divine is now DIVINE: A Parallel LTL Model Checker (http://divine.fi.muni.cz) | http://irclog.perlgeek.de/divine/
06:06 mornfall joined #divine
07:38 mornfall hm, zajímavý problém, tady ty C++ .bc soubory obsahujou tak 89k globálních symbolů
07:38 mornfall většinou konstanty, ale do 16 bitů se to úplně nevleze
07:38 mornfall nicméně to padající typeinfo není tím
07:39 xstill to je dost symbolů no
07:40 mornfall je k tomu přes megabajt constdata
07:40 xstill super, to je fakt všechno potřeba?
07:45 mornfall asi to chce generovat ty konstanty trochu víc inteligentně
07:47 mornfall co s tím DVE vs genexplicit?
07:52 xstill jo tohle, no ten problém je ne jen u DVE, teď to funguje tak, že pokud generátor exportuje nějaký flagy který jsou označený jako DefaultGoal, tak všechny tyhle flagy se verifikujou jako výchozí vlastnost v DESSu (safety), no ale DVE (ani ostantí mimo LLVM) teď žádný flagy neexportují, takže ve výsledném DESSu není žádnej goal. Jako co mě napadlo asi jako nejrozumnější, je přidat tam property default, která by byla výchozí ...
07:52 xstill ... (zkoušelo by se default, safety, assert v tomhle pořadí pokud nebude zadáno), takže gen-explicit -p X IN; verify --alg DESS by dávalo stejnou odpověď jako verify --alg -p X IN, což mi příjde jako docela fajn vlastnost (teď to tak funguje u LTL v podstatě, po tom včerejším patchi). Já o tom přemýšlel už když jsem ty flagy dělal, ale pak jsem došel k názoru, že je to zbytečné, ale teď už nevím proč
07:54 mornfall jo, mně přišlo jako problém to že DVE neexportuje flagy
07:56 xstill no protože já jsem o tom přemýšlel hlavně v kontextu llvm, a tam mi nedávalo až tak velký efekt exportovat sumarizovaný goal zároveň se všemi flagy, ale ty ostantí jsem nedomyslel
07:57 xstill otázka je teda spíš jestli chcem aby dess záležel na property se kterou je vygenerovanej i pokud tam není pře
07:57 xstill … přenásobení buchi
07:57 mornfall no, z tohohle pohledu by bylo lepší aby default property byla disjunkce přes flagy
07:58 xstill tj. tak jak to je, jen aby generátory museli generovat flagy?
07:58 xstill *musely
07:58 mornfall plusminus
07:59 mornfall rozhodně to dává větší smysl
08:00 xstill ok
08:01 mornfall uživatelsky, čím víc bude .dess odpovídat tomu z čeho se vygeneroval tim líp
08:05 xstill no to si právě nejsem jistej jestli tohle zajišťuje
08:06 xstill teď když uděláš gen-explicit -p mutex něco.bc a pak verify něco.bc.dess tak ti to verifikuje safety původního modelu, ne mutex
08:08 xstill proto přemýšlím jestli by neměla výchozí property nakonec reflektovat to co bylo v -p při generování
08:14 mornfall spíš bych řekl že pro gen-explicit by vůbec nemělo -p existovat
08:15 mornfall pokud existovat má tak by neměly existovat flagy
08:15 mornfall prozatím to může zůstat jako hack pro LTL
14:32 xstill hm, proč má timed error stavy ale nemá na to žádnou property
14:33 mornfall kdoví
14:53 xstill otázka je ještě co s cesmi (patch na DVE jsem poslal, teď u mě ten test prochází, ale nemám všechny generátory)
14:55 xstill ale myslím, že u cesmi se moc nemůže dělat nic jiného než vyexportovat cesmi_goal
14:55 xstill pokud vůbec
14:56 mornfall zatím asi tak, cesmi by se muselo upravit aby to dávalo větší smysl
15:28 mornfall no, dynamic_cast padá protože v těch typeinfo a vtable datech jsou cykly a nevypořádáváme se s tím úplně dobře
15:28 mornfall takže tam je na jednom místě null místo non-null
15:28 mornfall teď ještě jak to opravit aby to moc nebolelo
18:36 spito mornfall: znamená to sáhnout na libcxxabi? :D
18:49 mornfall ne
18:49 mornfall znamená to opravit divine
18:49 mornfall zatím se mi to nepovedlo
18:51 mornfall constants.cpp, storeConstant ... ono to je rekurzivní ale jak tam je cyklus tak se to někde zasekne a tam to vyrobí null
18:54 mornfall ono to je dokonce tak že tam je const expression který závisí na vlastním výsledku
18:57 spito heh? Tam ~ divine<
18:57 spito ?

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