1.1 Pár szó az útmutatóról // Tanuljuk meg a TLA+-t

Ez az útmutató a szükséges legkevesebbre fókuszál annak érdekében, hogy a lehető leggyorsabban nyújtson használható ismeretet a témáról, illetve ezen túlmenően néhány haladó technikával is megismertet a modellek finomítása érdekében. Ez a megközelítés figyelmen kívül hagyja vagy átszalad a TLA+ legnagyobb része felett, annak érdekében, hogy a fókuszban álló kis részt viszont egyszerűen tanulhatóvá tegye. Ez távolról sem jelenti azt, hogy a kihagyott részek unalmasak, bonyolultak vagy haszontalanok lennének. Egyszerűen csak kívül esnek jelen útmutató hatókörén.

Az útmutató írása során feltételezem, hogy az alábbi, szükséges háttérrel rendelkezel:

  • Tapasztalt programozó vagy: ez az útmutató nem egy programozás alapjaiba bevezető írás, és a TLA+ nem egy felhasználóbarát eszköz.
  • Jártas vagy a tesztelésben: ha nem használtál korábban egységteszteket (unit teszteket), akkor annak megtanulása sokkal hasznosabb lenne a számodra első közelítésben.
  • Van némi matematikai ismereted: a TLA+ erősen kölcsönöz a matematikai szerkezetekből és szintakszisból. Ha hallottál a De Morgan azonosságokról, tudod hogy mi az a halmaz, és érted hogy a (P => Q) => (~P => ~Q) mit jelent, akkor minden oké. Ellenkező esetben is használható az útmutató, de sok helyen jóval kevésbé lesz intuitív.

Szükséged lesz a TLA+ eszköztárra. Szintén szükséged lehet az alábbi anyagokra:

  • A PlusCal kézikönyv: a PlusCal az algoritmikus interfész a TLA+-hoz. Mindent, ami szükséges, azt lefedi jelen útmutató, de hasznos lehet a teljes referencia is. Mi a kézikönyv p-verzióját használjuk.
  • A TLA+ puska: pontosan az, aminek hangzik. Jelen útmutató hatáskörén kívül eső dolgok szintakszisát is tartalmazza.
  • Specifying Systems: ezt a könyvet Leslie Lamport, a TLA+ kitalálója írta, és azóta is a legátfogóbb könyv a témában. Sokkal haladóbb, mint jelen útmutató, de nem árt, ha tudsz a létezéséről.

1. Bevezetés // Tanuljuk meg a TLA+-t

Mi a TLA+?

A TLA+ egy formális specifikációs nyelv. Egy eszköz, amelyet rendszerek és algoritmusok tervezésére találtak ki, majd annak program általi verifikálására, hogy ezek a rendszerek nem tartalmaznak kritikus hibákat. Tulajdonképpen a tervrajz szoftveres megfelelője.

Miért kellene használni?

Itt látható egy egyszerű TLA+ specifikáció. A specifikáció kereskedőket reprezentál, akik egyedi tételekkel kereskednek. Megtalálod a hibát?

People == {"alice", "bob"}
Items == {"ore", "sheep", "brick"}
(* --algorithm trade
variable owner_of \in [Items -> People]

process giveitem \in 1..3 \* up to three possible trades made
variables item \in Items, 
          owner = owner_of[item], 
          to \in People,
          origin_of_trade \in People
begin Give:
    if origin_of_trade = owner then 
        owner_of[item] := to;
    end if;
end process;
end algorithm; *)

Ha ellenőrizzük, hogy valóban a tétel tulajdonosa az, aki eladja, akkor bizonyosan védve vagyunk a csalásoktól, nem igaz? Ha lefuttatjuk a modellellenőrzőt, akkor megláthatjuk, hogy nem igaz: Alice eladhatja a tételt saját magának, és mielőtt ez a folyamat befejeződne, ezzel párhuzamosan eladhatja Bobnak is. Aztán az első adásvétel végbemegy, és Alice visszakapja az eladott tételt. Az algoritmusunk versenyhelyzet miatt hibásan működik, és ezt azért tudjuk, mert a TLA+ felderített minden lehetséges állapotot és időbeli lefolyást.

Van persze néhány lehetséges mód ezt a hibás működést kijavítani. De a javításunk vajon működik kettőnél több ember esetében is? A TLA+-ban ennek ellenőrzése ennyire egyszerű: People == {"alice", "bob", "eve"}. Működik abban az esetben is, ha többféle tételt adhatunk el egyszerre? variable item \in SUBSET Items. Mi a helyzet akkor, ha több birka, érc, tégla van? amount_owned = [People \X Items -> 0..5]. Mi a helyzet akkor, ha mindhárom kereskedő egy ércet és egy birkát ad el minden többi kereskedőnek, míg Eve nulla téglát az el Alicenek? Ha ez a lehetséges állapottérben van, akkor a TLA+ ellenőrizni fogja.

Nehéz használni?

A formális metódusoknak van egy olyan megítélése, miszerint annyira nehéz őket használni, hogy az csak kritikus rendszerekben éri meg. Ez azzal is jár, hogy minden útmutató azzal a feltételezéssel íródik, hogy az olvasója kritikus rendszereken dolgozik, és kívül-belül ismernie kell a teljes TLA+-t, hogy teljesen biztos lehessen abban, a rendszere nem fog véletlenül megölni valakit.

Ha a veszélyes bug azt jelenti, hogy “valaki meghal”, akkor igen, a formális módszerek bonyolultak. Ha a veszélyes bug azt jelenti, hogy “senki nem hal meg, de az ügyfeleink nagyon dühösek lesznek, és két hetet azzal kell töltenünk, hogy megtaláljuk és kijavítsuk a hibát”, akkor a TLA+ egy kis részhalmazának ismerete elegendő, amely valójában nagyon egyszerűen megtanulható. Csak egy olyan útmutatót kell találni, amely a kezdők számára is barátságos.

Hol található egy ilyen, kezdők számára barátságos útmutató?

Helló! Ez az útmutató lefedi a TLA+ alapjait egy egyszerű, kézenfekvő módon. Egyébként: üdvözöllek a TLA+ világában!