Perl 6 - the future is here, just unevenly distributed

IRC log for #divine, 2017-01-05

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

All times shown according to UTC.

Time Nick Message
07:05 yaqwsx joined #divine
07:53 mornfall u assume se počítá že vytváří novou abstraktní hodnotu, takže omezení tohoto typu by neměl být problém tvořit jako nový uzly
08:17 xstill jako, že operace by vytvářeli nody toho grafu operací (který by byl poskládaný z weak pointerů počítám) a abstraktní pointry jsou něco co nejde dereferencovat, nebo to ani nemá přiřazenou paměť? a verzování nepotřebuješ protože když v cyklu narazíš na a = a + 1 tak to přeložíš jako new_node_a = (old_node_a + 1). Assume by ale neměl vytvářet abstraktní hodnotu, ne? Musí
08:18 xstill být v nějakém vztahu k té původní, to mi zatím není moc jasný jak v tomhle systému reprezentovat
08:19 xstill druhá věc je, že paměť tímto způsobem bude asi docela drahá, obvzlášť pokud budu načítat po jinak velkých kusech než jsem tam zapsal. Zatímco pokud by na identifikaci sym hodnoty v paměti stačil ukazatel, tak jde v podstatě všechny hodnoty reprezentovat jako spojení 8bit hodnot
08:20 mornfall však jo, uzel by vypadal jako assume <hodnota> <výraz>
08:20 xstill je teda fajn, že to řeší živost samo
08:21 xstill aha, to by vlastně šlo
08:21 mornfall assume musí hodnotu vytvořit protože u jiných abstrakcí by to jinak nemohlo ani fungovat
08:22 mornfall o cenu bych se teď úplně nebál, když teď člověk vytvoří pole symbolických bajtů má úplně jiný starosti
08:28 xstill a abstraktní pointry teda mají fungovat jak?
08:29 mornfall jo to nejsou abstraktní pointry, jen mají flag aby je šlo poznat
08:29 mornfall ukazujou na výraz kterej je reprezentovaný jako normální objekt na haldě
08:30 xstill jo, nemyslel jsem abstraktní ve smyslu symbolické. Šlo mi o to jestli to má nějakou specielní funkcionalitu
08:30 mornfall (uzel)
08:30 mornfall nemělo by být potřeba, jen sym algoritmus je musí umět poznat
09:16 xstill_ jo a jako abstrak jsou označené jen ty první pointry (co teď vedou jen z registrů), ty vnitřní už ne?
09:34 mornfall ano
09:48 xstill_ hm, ten assume by mohl být jen assume <výraz> ne, stejně v tom může být víc hodnot než jedna
09:48 xstill_ a vytvoří to nějaký assume registr
09:49 mornfall nemůže, protože když si vezmeš třeba is-not-0 abstrakci, tak assume == 0 na ? je 0 a musí se to projevit v dalším běhu
09:49 mornfall (a assume == 0 na not-0 je kontradikce)
09:50 mornfall aby teda mělo smysl tam nějakej assume vůbec dávat
09:50 mornfall a zase u symbolické hodnoty se může stát assume a < b
09:51 xstill_ tj. ty bys chtěl, aby se pak ten assume používal místo té původní hodnoty?
09:51 mornfall jo
09:51 mornfall dokonce si myslim, že to xheno tak implementoval
09:52 xstill_ no ale pro to a < b pak rozbiješ že ten vztah je nějakým způsobem symetrický, protože jednu z těch proměnných budeš muset určit jako tu hodnotu pro assume
09:53 mornfall nebudeš, protože dostaneš %a1 = assume a, a < b, %a2 = assume b, a < b
09:53 xstill_ to zas máš zbytečné uzly
09:54 mornfall které?
09:54 xstill_ teda pro sym. no máš to tam dvakrát ten assume. Pro sym by stačil jednou
09:54 mornfall stačil, ale ten výraz se může klidně sdílet, takže to zas takový problém není
09:55 xstill_ jo, to by musela zajistit transformace, že se bude sdílet
09:55 xstill_ nebo myslíš sdílet na úrovni uložení haldy?
09:56 mornfall to je nejmíň
09:56 mornfall ne, ve smyslu %c = constraint a < b, %a1 = assume a %c
09:57 mornfall stejně do toho assume nejspíš nepůjde narvat ten výraz jinak než že se vytvoří
09:57 mornfall nejdřív
09:57 xstill_ to je vlastně pravda
09:59 mornfall zacyklil se mi cmake
09:59 mornfall teda ninja vs cmake
09:59 xstill_ super…
09:59 mornfall [0/1] Re-running CMake...
10:00 mornfall už asi po pátý
10:00 mornfall nojo, na arke je plný /
10:00 xstill_ cože?
10:01 mornfall /dev/sdb2        450G  448G   87M 100% /
10:01 xstill_ nojo vidím no
10:01 xstill_ radost
10:01 xstill_ moc buildů
10:01 xstill_ dám /var/obj na samostatnou partiton
10:01 xstill_ teda asi moc buildů nevím co by to mohlo být jinak
10:01 xstill_ zjistí
10:01 mornfall já nějaký smažu... je tam další disk?
10:02 xstill_ určitě
10:03 xstill_ buď tam můžu vrazit 400 G sda, nebo jsou ta ještě 2x3TB
10:04 xstill_ disků je až dost koukám
10:04 xstill_ jo /var/obj/ má 325 GB
10:05 mornfall no už mi funguje make tak aspoň něco... asi by bylo dobrý tam dát terabajtovou partici (klidně raid0 když na to přijde)
10:06 mornfall pokud ty disky teda fungujou
10:06 xstill_ to by šlo, udělám TB LVM raid0
10:08 xstill_ rsyncnu tam ty buldy a pak to vyměním asi
10:09 mornfall ok, pak řekni než budeš dělat druhej rsync abych do toho zrovna nezapisoval
10:10 xstill_ taky by nebylo marný arke updatovat a restartovat
10:11 xstill_ hm, asi to budu muset nejdřív restartovat, protože LVM se se mnou nechce moc bavit
10:11 xstill_ device-mapper: reload ioctl on (254:2) failed: Invalid argument
10:11 xstill_ Failed to activate new LV.
10:12 mornfall Jan 05 11:07:22 arke kernel: ata3.00: failed command: FLUSH CACHE EXT
10:12 mornfall to by mohlo být tímhle
10:13 mornfall Jan 05 11:07:23 arke kernel: ata3.00: both IDENTIFYs aborted, assuming NODEV
10:13 mornfall takže ten disk už asi neexistuje
10:14 xstill_ hm
10:22 xstill_ to ten disk umřel ze samého nicnedělání?
10:22 xstill_ systém ho ale pořád vidí, nebo ho má v nějaké cache možná
10:23 xstill_ jo ale podle smartu je tam spousta chyb
10:23 xstill_ tak to nebude raid no
10:24 xstill_ doufám, že ten druhej hned nezdechne
10:24 xstill_ protože je stejnej asi
10:29 xstill_ "mount: unknown filesystem type 'ext4'" … ok
10:31 mornfall no proč ne
10:32 mornfall ale to btrfs na / se skoro plný chová fakt bizarně
10:47 mornfall hm, furt to dělá úplný haluze
11:30 xstill_ hm, jo, to bude totiž asi tím, že mám nový e2fsprogs ale "starý" kernel
11:30 xstill_ asi bych to rebootnul
11:31 xstill_ mornfall: můžu, nebo máš něco rozdělaného teď?
11:34 xstill_ jsem někde zahlíd, že v nových e2fsprogs něco zapnuly, tak by to mohlo možná být tím, i když je to skoro divný, když jedu na LTS kernelu, že by se měnilo co to umí v ext4
11:36 xstill_ co to dělá?
11:39 xstill_ je to nějaký jetý no
11:54 xstill_ už to snad bude OK
12:10 mornfall muzes
12:22 xstill_ hm, rebootnuté to je, jen teda ipmi na arke se se mnou moc nebaví, ani lokálně
12:36 xstill_ aha, tak remote se to se mnou baví, jen divně
12:36 xstill_ lokálně ale ne
12:36 xstill_ to je asi jedno
12:37 xstill_ (sol payload enable nefunguje ale sol activate funguje, a lanpus nefunguje pro jistotu vůbec)
13:07 xstill_ mornfall: když ty tam taky máš minimálně 4x nějaký hrozný 9-12 GB tar
13:10 mornfall kde?
13:10 xstill_ ls -lh /var/obj/xrockai-divine-dist/debug/_CPack_Packages/Linux-Source/TBZ2/divine-3.90.2+2016.12.21/divine-3.90.2+2016.12.21.tar.Z
13:11 xstill_ je tam toho ještě víc, teď se kopírují nějaké v TGZ (místo TBZ2) o něco menší ale přes 2 GB
13:23 mornfall ha, 37G
13:23 mornfall co ta věc dělá
13:28 mornfall já totiž celej ten cpack nesmysl vyhodil, ale tahle změna zdá se nepřežila úmrtí /home
13:30 xstill_ zkus se mrknout na anně do toho /mnt/home-copy
13:30 xstill_ jestli je to něco netriviálního
13:31 mornfall ls: cannot access '/mnt/home-copy/xrockai/src/divine/dist/Makefile': Structure needs cleaning
13:32 xstill_ aha :-/
13:33 xstill_ fsck jsem udělal na té první kopii home a to to nejspíš zničilo úplně, takže víc se s tím asi dělat nedá
13:33 mornfall asi ne no... a ty tary jsou zjevně rekurzivní
13:34 xstill_ super…
13:34 mornfall zajímavý je, že verze v /srv/www/divine/... vypadá OK
13:34 xstill_ tam je kopie?
13:35 mornfall těch tarů
13:35 xstill_ aha
13:35 mornfall to se celý nějak úplně rozpadlo
13:40 mornfall navíc mi na arke přestal fungovat shell (wtf)
13:41 xstill_ jakože máš bash? nebo jinak?
13:41 mornfall tys udělal upgrade?
13:41 mornfall ne, fish
13:41 mornfall ale nefunguje
13:41 xstill_ jo dělal
13:41 mornfall tak to bude asi tím
13:41 xstill_ (jsem psal, že to potřebuju restartovat aby naběhl novej kernel)
13:42 mornfall jo no, nová verze tam je
13:42 xstill_ to je divný, fish je v balíku, to by nemusel být rozbitej
13:42 xstill_ první rsync hotov, můžu to syncout znovu a vyměnit?
13:42 mornfall jo
13:43 xstill_ done
13:43 xstill_ ještě smazat ten starý obsah
13:45 mornfall dobrý, fish už jsem opravil, nekompatibilní změna
13:46 xstill_ ok, teď je všude stejná verze, takže by ti to mělo fungovat všude
14:13 mornfall nj, navíc teda nightly buildy nefungují protože nightly repo je zaprasený po restoru a current je tím pádem někdy z 13.12.
14:17 mornfall a tar-y vznikly tak, že z arke zmizelo /srv/www, takže mv těch tarů neprocházel a cpack je tam začal přibalovat a furt dokola
14:18 xstill_ aha, teď už tam zase je
14:20 mornfall a tím že je to všechno rozbitý jsem si ani nevšim že včera jsem způsobil že neprochází jedinej test
14:21 xstill_ hm jo a na anně je vypnutej cron, takže buildbot taky nebuildí DIVINE
14:23 xstill_ jo navíc /srv/builds chybí v fstab
14:24 mornfall asi se blíží divine week
14:24 mornfall čekám že v neděli exploduje serverovna nebo tak něco
14:25 xstill_ to doufám, že ne, stačí co se dělo před vánoci
14:29 xstill_ aha navíc se aktualizoval postgres a zjevně si teď neporadí s vlastní databází, super…
14:31 mornfall to není tak úplně chyba postgresu, to že upgrade RDBMS znamená dump/reload je dost dobře zavedený
14:31 mornfall debian to třeba zvládá zorganizovat sám, když mu to nezakážeš
14:31 mornfall nainstalovat původní verzi, dump, re-upgrade, load, jinak to asi nepůjde
14:32 xstill_ ještě že náhodou mám dump z 29. 12.
14:32 xstill_ takže stačí asi jen load
14:32 mornfall no, nebo
14:33 xstill_ i když, nejdřív se podívám kdy buildbot poslal tu tunu spamu, protože jestli je ten dump starší tak se pak pošle znovu…
14:35 xstill_ jo, dump je starý, to mám z toho, že nedávám pozor co updatuju
14:38 mornfall xstill_: koukám že tys taky rozbil spoustu testů a nevšim si toho :p
14:38 xstill_ co? kde?
14:38 mornfall 'no errors found' ... to se grepuje v testech :-)
14:39 xstill_ aha, sakra
14:40 mornfall ... tímhle tempem ta 4.0 nebude ani dneska
14:54 divine-buildbot joined #divine
14:54 xstill_ \o/
14:54 xstill_ mornfall: ty testy opravíš, nebo to mám opravit?
14:55 mornfall jo už se to dostalo docela daleko
14:55 mornfall tak třeba už to bylo všechno
16:01 mornfall ještě jedna úvaha k symu... řekněme, že nedeterministické hodnoty vznikají z nějakého streamu, takže mají unikátní identifikátory
16:02 mornfall program je na dané cestě deterministický, takže všechny hodnoty jsou plně determinované hodnotama takto vzniklých 'vstupních' hodnot
16:02 mornfall (a popsané jako symbolický výraz s nějakýma omezeníma)
16:03 mornfall pro jednoduchost řekněme, že x je jediný vstup
16:05 mornfall forall x. path₁(x) <=> path₂(x) ∧ ⋀{ l₁(x) = l₂(x) | l ∈ live set }
16:05 mornfall tohle by mohlo docela dobře popisovat že dva stavy jsou identický, ne?
16:06 mornfall x (a spol) jsou jediné volné proměnné, takže by to mělo jít napsat jako quantifier-free tautology problém
16:08 mornfall (kde path je konjunkce přes výrazy ve všech assume uzlech)
16:09 mornfall s,volné,výrokové,
16:20 yaqwsx joined #divine
16:20 mornfall plusminus path₁ → ⋀
16:20 mornfall yaqwsx: jdeš vhod ;-)
16:49 yaqwsx Poslouchám.
16:49 mornfall yaqwsx: ideálně viz log
16:50 mornfall za dnešek
16:50 xstill_ mornfall: path je co? path condition?
16:50 xstill_ yaqwsx: od 17:00
16:50 mornfall xstill_: „path je konjunkce přes výrazy ve všech assume uzlech“ ... takže jo
16:50 xstill_ nebo od včerejšího večera, podle toho jak chceš podrobně
16:51 xstill_ l je co?
16:51 xstill_ jo vidím
16:52 xstill_ ten popis dat
16:53 xstill_ teoreticky můžou nastat i případy, kdy l1(x) = l2(y) tj. pro různé vstupy dostateš stejný sym stav, otázka je jestli to je k něčemu nutné mít, asi ne
16:53 mornfall že se rovnají ve smyslu celé té velké konjunkce jo?
16:54 xstill_ jo, že by se všechny živé věci rovnaly přesto, že se vstupy nerovnají
16:54 xstill_ ale myslím, že to není nutné mít ani k terminaci ani ke korenktnosti
16:54 xstill_ (korektnosti LTL)
16:55 xstill_ protože tam tě to stejně zajímá jestli existuje cyklus nějakou fixní vstupní hodnotu
16:55 xstill_ otázka je jestli to fakt popisuje rovnost, zatím nevidím proč by ne
16:56 xstill_ no podle mě jo
16:56 xstill_ otázka je proč by na něco takového Vilík nepřišel
16:56 yaqwsx mornfall: Co když budu mít ale dva stavy, které ve své historii mají různé vstupy, ale vedou na stejné ohodnocení programových proměnných?
16:57 mornfall yaqwsx: co znamená různé vstupy v tomto případě
16:58 xstill_ yaqwsx: to je to nad čím jsem se zamýšlel taky
16:58 xstill_ příjde mi, že to nevadí je rozpojit
16:58 xstill_ (jen to může udělat víc stavů)
16:58 yaqwsx while( nondet() ) x = nondet()
16:58 yaqwsx Pokud je to path preserving (což teď skutečně nevím), tak pak to nemá problém s korektností LTL
16:59 xstill_ tohle by se rozbalilo podle mornfalla pokud to dobře chápu
17:00 mornfall já přemýšlím spíš jestli je vůbec korektní sloučit různý vstupy
17:01 xstill_ ty je neslučuješ, jen se ptáš, jestli v živých proměnných můžou být stejný hodnoty i přes to, že vstupy jsou různý
17:01 mornfall xstill_: no právě 'můžou' není korektní, si myslim... 'musí', budiž
17:01 xstill_ yaqwsx: ten cyklus se v symdivine nerozbalí, jo?
17:02 yaqwsx xstill_: V tomto případě ne.
17:02 yaqwsx Protože výsledné stavy po opuštění/před vstupem do další iterace sloučíš.
17:03 mornfall ale to jen proto žes ten nondet okamžitě zapomněl
17:03 mornfall (z předchozí iterace)
17:03 xstill_ no to jo, on žije jen chvíli, jenže ty bys ho měl v té path
17:04 xstill_ jinak to l neovlivňuje
17:04 mornfall neměl, protože je nedosažitelnej
17:04 mornfall (z live setu)
17:04 xstill_ path je ovlivněná tím, co je dosažitelné?
17:04 yaqwsx mornfall: Dá se to tak říci, ale je to proto, že nerozeznám od sebe stavy po n a m iteracích.
17:05 mornfall yaqwsx: zrovna tenhleten příklad je dost akademický, protože čtení odkudkoliv má většinou vedlejší efekty, takže to sloučit nejde
17:05 xstill_ mornfall: no reálně se ptáš na musí no, protože se ptáš jestli pro všechny vstupy x1 existuje vstup y1, takový že  se to liší
17:07 yaqwsx mornfall: Souhlasím, ale co příklad sekvenční kompozice n pure procedur?
17:07 mornfall yaqwsx: pure procedura nemá kde vzít nedeterminizmus
17:08 yaqwsx mornfall: Beru zpět, tam se to vyřeší eliminací mrtvých proměnných.
17:08 yaqwsx mornfall: Špatný termín - izolovaných - taková, která sama pracuje se vstupem, ale nemá efekt na následujícící procedury.
17:09 mornfall yaqwsx: to by muselo znamenat že čte odjinud než ostatní procedury
17:09 mornfall (víceméně že nedělá vůbec nic :-
17:09 mornfall )
17:09 yaqwsx mornfall: ?
17:09 xstill_ proč by nemohla číst odjinut?
17:10 xstill_ připojíš 3 kvantové generátory náhodných čísel ja jedeš
17:10 mornfall no, když něco přečte a nijak to neovlivní stav, tak ta procedura nedělá nic ne?
17:10 xstill_ tak tenhle cyklus taky nic nedělá
17:10 mornfall no to byla taky moje námitka vůči němu :)
17:11 mornfall rádoby čte stejnej bajt z neměnného souboru
17:12 yaqwsx Mám proceduru, která něco dělá, ale nic nevrací. Abych ověřil safety/LTL musím zkontrolovat její stavový prostor. A původní myšlenka byla, že by se mi při sekvenční kompozici takových procedur vždy roz-n-til stavový prostor a kontroloval bych tu poslední proceduru exponenciálněkrát. Ale pak jsem si uvědomil, že se to dít nebude, jelikož proměnné, na kterých to závislo už dávno budou mrtvé
17:12 xstill_ ale co když máš něco jako return nondet() + nondet();? musel by tam ještě být nějakej if teda aby to nebylo *
17:14 xstill_ specielní případ tvýho tvrzení je vlstně, že pokud má program jiný počet vstupů tak nemůže být ve stejném stavu, že?
17:15 mornfall vstupů který jsou odkazovaný živýma proměnnýma
17:16 xstill_ no ne, podle mě v path můžeš mít jakýkoli vstupy, ne?
17:16 mornfall proč?
17:16 xstill_ if ( x < nondet() ) return foo(); else return bar(); kde x je sym
17:17 xstill_ to ti vytvoří constraint na x, ne?
17:17 mornfall to nemá žádnou path condition
17:17 xstill_ proč?
17:18 mornfall protože jakmile se vyhodnotí ten if tak je jeho výsledek mrtvej
17:19 xstill_ hm, ty chceš zapomínat fragmenty path condition vykonaných bloků? protože ty honoty už nebudou živý?
17:19 xstill_ to teď nevím jestli můžeš
17:19 xstill_ ale i kdyby, tak ti to pořád ovlivňuje to a, ne?
17:19 mornfall žádná živá proměnná na to omezení neodkazuje, tak nemůže mít vliv na to co bude ten program dělat
17:20 mornfall ktterý a?
17:20 mornfall který*
17:20 xstill_ x
17:20 mornfall jak?
17:20 mornfall constraint na x že x < nondet můžeš asi rovnou zahodit
17:21 mornfall nebo ho přepsat na x != INT_MAX
17:21 xstill_ no to nemusíš staticky poznat, že to je *
17:21 xstill_ foo() { y = nondet(); if ( x < y ) { return foo(); } else { return bar(); }
17:22 mornfall x, y jsou globální?
17:22 xstill_ y je lokální
17:22 xstill_ x je z vnějšího scope
17:22 mornfall pak to u x přežije (v tom původním jsem bral že x je lokální, pak je totiž taky mrtvý)
17:24 mornfall každopádně se to celý točí kolem sémantiky nondet()
17:25 mornfall proto jsem na začátku řekl, uvažujme že nedeterministické hodnoty vznikají ze streamu
17:27 mornfall to modeluje třeba socket, nebo stdin...
17:27 mornfall nejsem přesvědčený, že můžeš říct, že nezáleží na tom, jestli je v proměnný uložený desátý nebo dvacátý bajt vstupu
17:32 xstill_ asi to už dneska nedávám rozkódovat
17:32 xstill_ minimálně ne teď
17:48 yaqwsx joined #divine
18:16 yaqwsx mornfall: Přemýšlel jsem nad tím a zatím jsem nenašel důvod, proč by to nefungovalo.
18:17 mornfall fajn... on by neměl být velkej problém tvořit formule v jednom nebo v druhém tvaru, když na to přijde, a klidně to pak třeba srovnat (pokud teda ten tvar co jsem včera večer popisoval skutečně funguje)
18:19 mornfall ono to jistým způsobem štimuje v tom, že kvantifikátory (zhruba) odpovídají permutacím pořadí vstupu...
18:20 mornfall osobně bych ale tipnul, že za ně zaplatíš mnohem víc než vyhraješ slučováním stavů
18:22 mornfall představuju si, že typický (zvládnutelný) verifikační problém má fixní počet nondet vstupů
18:23 mornfall (zvládnutelný a zároveň aspoň trochu smysluplný)
19:32 xstill mornfall: pokud budeš vstupu brát jako jeden stream (tj. reálně ty stavy zipuješ nejen podle živých hodnot ale i podle vstupů), tak se ti nebudou sbíhat diamondy myslím. Vezmi dvě vlákna, která každé čte jednu rouru, roury jsou simulované nondet vstupem. Řekněme, že každé vlákno přečte 4 čísla a ty vrátí přes sdílenou paměť do mainu a kontroluje jestli jsou v nějakém
19:32 xstill rozsahu (každé v jiném). Pak ti prokládání udělá větvení, které nespojíš.
19:39 xstill taky si nejsem jistý, že můžeš zapomínat fragmenty path condition které vznikly z vstupů na které už se nic neodkazuje. Verzmi třeba toto: main() { int x = input(), z; { int y = input(); if ( y > 0 ) { z = doSomething( x ) } else { z = 42; } }; assert( x != 42 ); řekněme, že první větví nemůžeš dostat z = 42. Pokud máš protipříklad, tak v jeho path condition už podle toho jak jsem
19:39 xstill tě pochopil nemá být informace o y, to ale znamená, že z toho nezrekonstruuješ přímo vstupy pro protipříklad. Akorát tady by to asi ještě šlo pustit podle choice, takže by se to z toho vymlátit dalo, přemýšlím, jestli to dokážu rozbít úplně…
19:40 xstill hm, control flow je asi jasně určený sledem choice
19:42 mornfall xstill: nesloučí, ale pokud to budou dvě roury tak není problém aby měla každá svůj stream
19:43 mornfall intuitivně mi právě přijde dost divoký aby se to při prokládání slučovalo jakože jsou ty proložení ekvivalentní i když to bralo data ze společného vstupu (v jiným pořadí)
19:43 xstill ještě jsem přemýšlel nad LTL, lehkou modifikací toho Honzova příkladu (opět předpokládám, že soubory jsou simulovány nedeterminismem), něco jako: ifstream f(…); while ( f.good() ) { int x; f >> x; if ( x < 0 ) break; } AP( fin );. Verifikuješ AF( fin )
19:44 xstill mornfall: to ale znamená dost komplikovaný modelování vstupů pokud je chceš rozdělovat
19:44 mornfall xstill: ale taky jediný smysluplný, nebo možná nevidim co má znamenat vstup
19:45 xstill hm, ještě mi řekni co si myslíš o tom cyklu
19:45 xstill tam je jeden stream a řekl bych že je tam problém
19:46 xstill řekněme, že je to něco co monitoruje výstup nějaký abstrahovaný komponenty
19:46 mornfall no AF( fin ) by mělo být false pokud je f stream (a ne soubor)
19:46 mornfall a true pokud je to soubor
19:46 xstill jo, ono to je false, jen je to nekonečně stavový najednou
19:47 xstill (pro stream)
19:47 xstill v symdivine by to nemuselo být nekonečně stavový
19:48 mornfall jestli to bude konečně nebo nekonečně stavový záleží od toho jak budeš ty vstupy číslovat
19:49 mornfall pokud bys chtěl sémantiku kde přečtený a zapomenutý data nedělaj rozdíl, mělo by stačit recyklovat číslování toho streamu
19:51 mornfall navíc teda relaxovat podmínku na pořadí vstupů by taky neměl být problém, stačí je 'nějak' (smysluplně, aby se nerozpojovalo zbytečně moc) zazipovat
19:51 xstill hm
19:51 mornfall (to odpovídá té představě, že kvantifikátory kódujou permutace vstupu)
20:14 xstill ok, minimálně pro safety nevidím jak by to mohlo schovat bug. Asi mi dává největší smysl vyzkoušet obojí, jen to teda znamená zamyslet se nad tím na co se má vlastně symbolický DIVINE používat a podle toho sehnat benchmarky
20:23 mornfall no, pro LTL to taky snad nemůže schovat bug (jinak než že divine neskončí)
20:23 mornfall mohlo by to nekódovat rovnost

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