Vlny provádění se počítají z grafu a úkoly v jedné vlně, které sahají na stejné cesty, se hlásí jako serializované

deklarovaný stav○deklarovaný stav: zaručeno Deklarováno jako deterministické a blokující, implementováno a s uvedeným behaviorálním testem, který to má dokázat. Zda to zaznamenaný běh podporuje, říká verdikt důkazů zobrazený vedle.

zaznamenané důkazy○zaznamenané důkazy: nespuštěno Deklarováno jako zaručené, ale nepodložené zaznamenaným během: test je pojmenován, ale žádný úspěšný běh nad současnými vstupy zaznamenán není. jak se zaznamenávají důkazy

Sdílení vlny je pro souběžnost nutné, ale nestačí. Překrývající se deklarovaný rozsah se serializuje konzervativně, protože falešná serializace stojí čas a falešná paralelnost stojí konflikt.

majordomus plan waves
# Wave 1
#   I0002   READY     …
#   I0003   READY     …
#
# serialised by scope overlap:
#   I0002 shares lib/project.awk with I0003; they may not run concurrently

Detail vykreslený z docs/claims/execution-waves.md.

Od tvrzení k důkazu

1. 1 · veřejné tvrzení

   Vlny provádění se počítají z grafu a úkoly v jedné vlně, které sahají na stejné cesty, se hlásí jako serializované

   Učiněno na Planning, Plan.

2. 2 · kanonické tvrzení

   execution-waves○deklarovaný stav: zaručeno v docs/CLAIMS.yaml

   Definováno v přečtěte si to na tomto webu · docs/PLANNING.md

3. 3 · implementace

   lib/project.awk

4. 4 · test a scénáře

   Test: test/cases/42_dag_waves.sh

   Provedeno v Dodávejte úkoly ve vlnách, které graf spočítá, a vezměte další, Veďte plán jako milníky a úkoly, které nástroj umí validovat.

5. 5 · zaznamenané běhy

   ○zaznamenané důkazy: nespuštěno jak se zaznamenávají důkazy

Ověřte si to sami

Test běží v jednorázovém dočasném repozitáři a ověřuje chování, ne řetězec ve zdrojovém kódu.

bash test/run.sh 42_dag_waves

Kde se toto tvrzení používá

Související tvrzení stejná implementace

• ○deklarovaný stav: záruka Stav úkolů a milníků se odvozuje ze zaznamenaných faktů a nikde se neukládá
• ○deklarovaný stav: zaručeno Cyklus, závislost na sobě samém a závislost na neexistujícím úkolu se odmítnou každé zvlášť jménem

Okamžiky, na které to odpovídá

• → přečetl tři plány rozvoje jednoho projektu a nevěřil žádnému Plán vedený v próze je snímek a každá jeho kopie se rozchází svým tempem; uložený stav je tvrzení, které platí i poté, co se svět pohnul.
• → se zeptal, kam milník dospěl, a musel se jít ptát čtyř lidí Pokrok je agregát, který existuje jen v lidech, protože části, které agreguje, se nikdy nezaznamenaly ve tvaru, který by šel sečíst.