Bakery-Boulangerie specs don't satisfy `DeadlockFree` or `StarvationFree` liveness properties
Nessuno ha ancora preso questa issue.
Valutazione
- Difficoltà
- 5/5
- Tempo stimato
- Più di una settimana
- Idoneità per principianti
- 25/100
- Tipo di issue
- Bug
- Chiarezza
- Da chiarire
- Stato di attività
- Ferma
- Ambito
- tooling
Direzione di ricerca
Esamina le specifiche di Bakery-Boulangerie e le assunzioni di equità in Spec, che l'issue identifica come insufficienti. Determina le assunzioni necessarie per DeadlockFree e StarvationFree; il lavoro è completato quando entrambe le proprietà di vivacità sono soddisfatte dalle specifiche.
Scritto dal modello di indicizzazione a partire dal testo della issue.
Descrizione
I've been defining models as part of work on #107. Currently these properties fail so these specs can only be subject to safety checking. Some fairness assumptions are required for the properties to be satisfied. @muenchnerkindl any idea what those fairness assumptions would be? The one in Spec is insufficient.
- Lingua principale
- TLA
- Stelle
- 1.6k
- Fork
- 225
- Metriche di merge delle PR
- Nessuna PR unita negli ultimi 30g
Preparare l'ambiente
Avvia il container di sviluppo del progetto nel browser, con il tuo account GitHub.
- Nessun Dockerfile né file Docker Compose
- Nessun modello di pull request
- Leggi la guida per i contributori
Come iniziare
- Leggi tutta la issue e poi la guida ai contributi del progetto.
- Commenta sulla issue per dire che te ne occupi tu — evita che due persone facciano lo stesso lavoro.
- Fai un fork del repository e lavora su un branch.
- Apri una pull request che faccia riferimento al numero della issue.
Altre issue di tlaplus/Examples
-
question
Difficoltà 3/5 1-2 giorni Idoneità per principianti 48/100
-
Difficoltà 2/5 1-3 ore Idoneità per principianti 35/100
-
Difficoltà 5/5 Più di una settimana Idoneità per principianti 25/100
-
help wanted
Difficoltà 3/5 1-2 giorni Idoneità per principianti 35/100
Tutte le issue di tlaplus/Examples
Issue simili
-
Difficoltà 2/5 1-3 ore Idoneità per principianti 70/100
nolabs-ai/nono-packs#44 ·
I maintainer di solito rispondono entro 1 giorno
-
namespace operations
Difficoltà 2/5 1-3 ore Idoneità per principianti 64/100
EclipseFdn/open-vsx.org#13665 ·
I maintainer di solito rispondono entro 1 giorno
-
Difficoltà 2/5 1-3 ore Idoneità per principianti 78/100
need4deed-org/sdk#267 ·
I maintainer di solito rispondono entro 1 giorno
-
Difficoltà 2/5 1-3 ore Idoneità per principianti 88/100
I maintainer di solito rispondono entro 1 giorno
-
Make LICENSE a regular fileApertaeasy low
Difficoltà 2/5 1-3 ore Idoneità per principianti 84/100
open-nudge/opentemplate#184 ·
I maintainer di solito rispondono entro 1 giorno