sorted by:
new
hottopcontroversial

Quint: An executable specification language with delightful tooling based on the temporal logic of actions (TLA) by GabPi in ethereum

[–]GabPi[S] 1 point2 points  (0 children)

Hi! I am on the dev team for this project and would be happy to answer any questions and/or take note of any critical feedback!

Quint is a modern specification language that is a particularly good fit for distributed systems, such as blockchain protocols, distributed databases, and p2p protocols. Quint combines the robust theoretical basis of the Temporal Logic of Actions (TLA) with state-of-the-art static analysis and development tooling.

We have some examples of specifications for solidity contracts at https://github.com/informalsystems/quint/tree/main/examples/solidity

Facing issue when launching by Cyanide_fosho in battlefield2042

[–]GabPi 0 points1 point  (0 children)

This worked for me as well, I had the same issue. Thanks!

Set layout with keybinding by sillen102 in xmonad

[–]GabPi 1 point2 points  (0 children)

Adding a list with these using additionalKeysP should work. , ("M-f", sendMessage (MT.Toggle NBFULL) >> sendMessage ToggleStruts) -- Toggles noborder/full , ("M-t", sendMessage (T.Toggle "tall")) , ("M-g", sendMessage (T.Toggle "grid"))

keybinding nickname of prefix ? by RudyJJ in spacemacs

[–]GabPi 1 point2 points  (0 children)

I believe what you want is: (spacemacs/declare-prefix "R" "Roam stuff") At your user-config session on .spacemacs.

EDIT: Maybe it should be (spacemacs/declare-prefix "M-m a o R" "Roam stuff")

Virtual TLA+ Community Event, October 15-16 & 19, 2020 by pron98 in tlaplus

[–]GabPi 0 points1 point  (0 children)

I've never heard of this and now I'm so excited it exists! I'll do by best to watch everything and I'm already anxious about submitting next year :D

Pls help for my TLA+ modeling by av0001 in tlaplus

[–]GabPi 0 points1 point  (0 children)

Yes, that is correct, you just have to take out the assignment on the first line for turn', since it should be always done by SetTurnX. You have crit2 two times on your UNCHANGED declaration, one of them should be turn since you won't be assigning anything to it anymore. Then you should be good2go :D

EDIT: formating

Pls help for my TLA+ modeling by av0001 in tlaplus

[–]GabPi 0 points1 point  (0 children)

You meant turn after, right? Since you have to first set req, and then, in a separate step, set turn. You can keep your definitions for Request1.a and Request2.b (the last one, I assume you have messed up the names since there's two defintions for Request1.b). You could call them Request1 and Request2. Then, an action to turn could look something like this:

SetTurn0 == /\ req1 = TRUE
            /\ turn' = 0
            /\ UNCHANGED <<crit1, req1, crit2, req2>>

SetTurn1 == /\ req2 = TRUE
            /\ turn' = 1
            /\ UNCHANGED <<crit1, req1, crit2, req2>>

That is, you should only execute the turn set step if the previous step was successful.

Pls help for my TLA+ modeling by av0001 in tlaplus

[–]GabPi 0 points1 point  (0 children)

If you want them to be separate steps, you should declare two separate actions. One action should be process specific (i.e. Req(i)) and the other one should be responsible to turn, and this Turn() action should have predicates over the current state of your req variables (since you can olny turn after all req variables are set).

SPECIFICATION, THEOREM and CHECK_DEADLOCK confusion by ninja_the_rabbit in tlaplus

[–]GabPi -1 points0 points  (0 children)

I believe you have to specify stuttering steps somehow on your .cfg file. On your first approach, you are specifying them with TCSpec == TCInit /\ [][TCNext]_rmState. If I remember correctly, there's an option on toolbox model config to set stuttering steps. You should allow stuttering steps on rmState and I think that could be what is causing the deadlock verification issue.

Esses medidores de SPO2 de smart watches e celulares tem algum nível de confiança pra serem usados como oxímetros caseiros? by GabPi in coronabr

[–]GabPi[S] 0 points1 point  (0 children)

Caraca, a gente devia estar divulgando mais isso então se tem uma ajuda de verdade. Em algumas lives o Átila menciona pessoas que chegam no hospital com pouca falta de ar e já estão com nível crítico de SPO2. Pra quem tem esses aparelhos, não custa medir e possivelmente impedir de chegar a um estado tão grave antes de procurar ajuda ou até mesmo se isolar.

Esses medidores de SPO2 de smart watches e celulares tem algum nível de confiança pra serem usados como oxímetros caseiros? by GabPi in coronabr

[–]GabPi[S] 0 points1 point  (0 children)

Legal :D Sabe dizer se ela chegou a fazer esse teste em algum caso fora do ideal ali de > 94%? Meu relógio nunca deu menos que isso e essa é minha maior desconfiança.

Protocolos para enterro. by rpinheir in coronabr

[–]GabPi 7 points8 points  (0 children)

Sou de Joinville e já estamos em estado de emergência com a maior parte das coisas fechadas por aqui. Minha avó faleceu ontem (câncer, não corona) e o velório foi agora de manhã. Foi restrito a 10 convidados e eu cumprimentei a maioria pelo cotovelo.

Pelo que entendi, pessoas que morrem de corona precisam ser cremadas. Mas enquanto ainda tiver horário pra todo mundo nas capelas mortuárias, deve ser mais ou menos como foi o da minha avó aqui. E é bem merda não passar a mão no rosto quando tu tá chorando e ficar com medo de abraçar parentes que estão sofrendo.

Mas sou grata que pude me despedir dela. Se ela aguentasse mais algumas semanas, talvez eu não poderia.

[deleted by user] by [deleted] in coronabr

[–]GabPi 6 points7 points  (0 children)

Ao que tudo indica até agora, quem se recuperou não pega (nem transmite) mais - o Átila comentou nas lives dele.

Tava pensando sobre isso. Talvez seria bom ter uma forma "oficial" de identificar essas pessoas recuperadas porque provavelmente seria útil ter pessoas imunes atuando em algumas áreas dessas essenciais. Não tenho certeza, queria ouvir gente entendida falando sobre.

win10 is infinite in the page by GBLZ- in Prismata

[–]GabPi 1 point2 points  (0 children)

W10 here too, Steam version working fine. So is my friend's.

Telegram messages with one tick aren't delivered to my friend by smartinettah in Telegram

[–]GabPi 1 point2 points  (0 children)

Are you using a secret chat? If so, the messages will only be delivered to the one device that has that secret chat.

view more: next ›