Bizitasun propietate

Konkurrentzian, bizitasun propietateak adierazten du zerbait ona noizbait gertatuko dela. Hau da, jarritako helburua lehenago edo beranduago lortuko dugula. Bizitasun propietateak aurrerapen bat behar du.

Aurrerapen propietate batek adierazten du beti emango dela kasua non ekintza noibait izango den egikaritua. Aurrerapenaren aurkakoa: gosez hil, ekintza inoiz egikaritzen ez den egoera.

Sistema batek bizitasun propietateak betetzen dituen galdetzea ez da oso esanguratsua. Nahikoa da infinitu kasutan sistema behatzea, eta sistema errealak ez egikaritzea inoiz. Bizitasuna garrantzitsuena den propietatearen hurbilketa da.

Adibidea

Bide bakarreko zubiaren problema

Ibai bateko zubi bat oso estua da, eta soilik kotxe bat konkurrenteki mugi daiteke, soilik norabide berean mugitzen badira. Segurtasun botxaketa bat gertatuko da aldi berean bi kotxe zubian sartzen badira norabide ezberdinean. Ezkerretik eskubira kotxe urdinak eta eskubitik ezkerrera kotxe gorriak.

Kolore bakoitzeko kotxe bat baino gehiago daudenean, posible da lehenengoz kotxe gorri bat zubian sartzea, eta ondoren kotxe gorriak sartzen jarraitzea, urdinei inoiz pasatzen ez utziz(edo alderantziz).

Bizitasun propietatea betetzeko, kasu honetan lehenago edo beranduago kotxe urdinak zubia zeharkatu beharko luke(edo beste kasuan gorria). Hau egiteko nahikoa da semaforo bat ezartzea eta horrela gorriak eta urdinak zeharkatuko dute zubia.

Kanpo estekak

• (Ingelesez) Liveness properties. Joost-Pieter Katoen

• Datuak: Q12255316