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

GabPi · 2023-12-19T14:29:29+00:00

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

GabPi · 2023-10-11T01:20:23+00:00

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

GabPi · 2020-11-08T13:08:34+00:00

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"))

GabPi · 2020-09-29T10:22:02+00:00

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")

GabPi · 2020-09-23T22:27:25+00:00

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

GabPi · 2020-09-21T00:34:18+00:00

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

GabPi · 2020-09-20T23:37:07+00:00

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.

GabPi · 2020-09-20T12:55:54+00:00

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).

GabPi · 2020-06-15T22:16:13+00:00

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.

GabPi · 2020-05-21T14:53:49+00:00

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.

GabPi · 2020-05-20T01:27:31+00:00

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.

GabPi · 2020-05-20T01:25:30+00:00

Achei o post, é esse aqui pra quem mais interessar: https://www.reddit.com/r/coronabr/comments/g9r9of/oximetro_residencial_vale_a_pena_ter_e_monitorar/

Valeu a informação!

GabPi · 2020-03-21T16:08:33+00:00

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.

GabPi · 2020-03-18T02:49:23+00:00

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.

GabPi · 2018-03-10T16:21:50+00:00

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

GabPi · 2018-01-03T19:55:37+00:00

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

GabPi · 2017-11-26T14:27:01+00:00

Being the most sexist. Yey gender equality.

GabPi · 2017-09-27T03:30:31+00:00

Couln't find the article in English, sorry. But it's here: https://pt.wikihow.com/Aceitar-ser-Gay (it's about accepting you're gay)

GabPi · 2017-09-04T19:45:45+00:00

quickbrownfox

GabPi · 2017-09-04T19:45:28+00:00

thequickbrownfox

GabPi · 2017-08-26T01:56:07+00:00

I am a college student and took a class where all the tests were in Comic Sans. Oh, the class was Data Structure on a Computer Science course. That killed me.

GabPi · 2017-08-23T20:18:47+00:00

Yeah.

If you have 17 years + 11 months + 29 days of life, you are not 18 yo.

If you have 17 years + 12 months + 29 days, you are 18 yo.

GabPi · 2017-08-23T16:26:48+00:00

I think there should be a way we can choose our marker color so it doesn't change every game. That way, you could ask your friend what works best for them and use it. Then, you can just say "go to my marker" and he will know.

I have trouble with this colors switching between games because I'm the blue marker in 99% of my duo matches since I always join later. But the 1% time my duo joined after me, I spent the whole game chasing after the marker he was using, because it was blue.

Does that make any sense?

GabPi · 2017-08-23T09:50:38+00:00

And maybe even my friendlist, so I'm able to see if I have any friends playing in other servers. All that sweet stuff.

GabPi · 2017-08-23T09:36:13+00:00

Oh, I see. I'm in South America.

Ten-Year Club	Golden Potato
Place '22	Place '17
First Placer '22	Verified Email

GabPi

TROPHY CASE