لغة التحقق الرسمية من أنظمة البرمجيات

TLA ⁺ هي لغة مواصفات رسمية طورها Leslie Lamport . تُستخدم لتصميم ونمذجة وتوثيق والتحقق من البرامج، خاصة الأنظمة المتزامنة والأنظمة المُوزعة . يُعتبر TLA ⁺ شيفرة زائفة قابلة للاختبار بشكل شامل، ^[1] ويُشبه استخدامه برسم المخططات لأنظمة البرمجيات؛ ^[2] TLA هو اختصار لـ Temporal Logic of Actions .في مجال التصميم والتوثيق، تؤدي لغة TLA ⁺ نفس دور المواصفات الفنية غير الرسمية.ومع ذلك، تُكتب مواصفات TLA ⁺بلغة رسمية قائمة على المنطق والرياضيات، وتهدف دقة المواصفات المكتوبة بهذه اللغة إلى الكشف عن عيوب التصميم قبل البدء في تنفيذ النظام. ^[3]

نظرًا لأن مواصفات TLA ⁺ تُكتب بلغة رسمية، فهي قابلة للفحص باستخدام تقنيات التحقق من النماذج المنتهية. يقوم مدقق النموذج باكتشاف جميع سلوكيات النظام الممكنة حتى عدد معين من خطوات التنفيذ، ويفحصها للكشف عن أي انتهاكات لخصائص الثبات المطلوبة مثل الأمان والحيوية . تستخدم مواصفات TLA ⁺ نظرية المجموعة الأساسية لتحديد الأمان (لن تحدث أشياء سيئة) والمنطق الزمني لتحديد الحيوية (تحدث أشياء جيدة في النهاية).تُستخدم لغة TLA ⁺ أيضًا لكتابة براهين صحة يتم التحقق منها آليًا لكل من الخوارزميات والنظريات الرياضية. تُكتب هذه البراهين بأسلوب إعلاني هرمي مستقل عن أي نظام إثبات معين. يمكن كتابة البراهين الرياضية المنظمة الرسمية وغير الرسمية بلغة TLA ⁺ ؛ حيث تشبه اللغة لغة LaTeX ، وتوجد أدوات لترجمة مواصفات TLA ⁺ إلى مستندات LaTeX. ^[4]

تم تقديم لغة TLA ⁺ في عام 1999، بعد عدة عقود من البحث في طرق التحقق من صحة الأنظمة المتزامنة. ومُنذ ذلك الحين، تَم تطوير مجموعة أدوات متكاملة تشمل بيئة تطوير متكاملة IDE ومدقق النموذج الموزع.في عام 2009، تم إنشاء لغة البرمجة الشبيهة بالرمز PlusCal، وهي تنتقل إلى TLA ⁺ وهي مفيدة لتحديد الخوارزميات المتسلسلة. تم الإعلان عن TLA ⁺² في عام 2014، مما أدى إلى توسيع دعم اللغة لبناءات الإثبات. المرجع الحالي لـ TLA ⁺ هو The TLA ⁺ Hyperbook من تأليف Leslie Lamport.

تم تطوير المنطق الزمني الحديث بواسطةآرثر براير في عام 1957، وكان يُعرف آنذاك بمنطق الزمن.

وعلى الرغم من أن أمير بنويلي كان أول من درس بجدية تطبيقات المنطق الزمني في علوم الحاسوب ، فقد تكهن براير باستخدامه قبل ذلك بعقد كامل في عام 1967:

لا تعتمد فائدة الأنظمة من هذا النوع [في الوقت المنفصل] على أي افتراض ميتافيزيقي خطير مفاده أن الوقت منفصل ؛ إنها قابلة للتطبيق في مجالات الخطاب المحدودة التي نشعر بالقلق فقط بما يحدث بعد ذلك في سلسلة من الحالات المنفصلة ، على سبيل المثال في عمل جهاز كمبيوتر رقمي.

أجرى بنويلي أبحاثًا حول استخدام المنطق الزمني في توصيف البرامج الحاسوبية، وقدم المنطق الزمني الخطي في عام 1977. أصبحت LTL أداة مهمة لتحليل البرامج المتزامنة، حيث تعبر بسهولة عن خصائص مثل الاستبعاد المتبادل والتحرر من الجمود . ^[5]

بالتزامن مع عمل بنويلي على منطق الزمن الخطيLTL، كان الباحثون الأكاديميون يعملون على تعميم منطق هوار للتحقق من صحة البرامج متعددة المعالجات. وقد بدأ ليزلي لامبورت اهتمامًا بالمشكلة بعد أن اكتشفوا في مراجعة الأقران خطأً في ورقة قدمها حول الاستبعاد المتبادل.

في عام 1975،قدّم إد أشكروفت مفهوم "الثبات" في ورقته البحثية، بعنوان "إثبات العبارات حول البرامج المتوازية"، وهو المفهوم الذي استخدمه لامبورت لتعميم طريقة فلويد في ورقته البحثية عام 1977 بعنوان "إثبات صحة برامج العمليات المتعددة". قدمت ورقة لامبورت أيضًا السلامة والحيوية كتعميمات للصحة الجزئية والإنهاء على التوالي. ^[6] تم استخدام هذه الطريقة للتحقق من أول خوارزمية لجمع القمامة المتزامنة في ورقة بحثية عام 1978 مع إدجر ديكسترا . ^[7]

اطّلع لامبورت لأول مرة على منطق الزمن الخطي (LTL) الخاص بـ Pnueli أثناء ندوة في جامعة ستانفورد عام 1978 نظمتها سوزان أويكي .

وفقًا للامبورت، "كنتُ متأكدًا أن منطق الزمن مجرد هراء نظري لا يمكن أن تكون له أي تطبيقات عملية، لكنه بدا ممتعًا، فحضرتُ."

و في عام1980، نشر مقالًا بعنوان "أحيانًا يكون أحيانًا ليس أبدًا"، والذي أصبح من أكثر الأوراق البحثية استشهادًا في أدبيات المنطق الزمني. ^[8] عمل لامبورت على كتابة مواصفات المنطق الزمني أثناء عمله في معهد SRI ، لكنه وجد أن النهج غير عملي:

ومع ذلك ، شعرت بخيبة أمل من المنطق الزمني عندما رأيت كيف كان شوارتز ، ميليار سميث ، وفوجت ، يقضيون أيامًا في محاولة لتحديد بسيطة قائمة انتظار FIFO-بحجة ما إذا كانت الخصائص التي ذكروها كافية. أدركت أنه على الرغم من جاذبيتها الجمالية ، فإن كتابة مواصفات كتواصل للخصائص الزمنية لم تنجح في الممارسة العملية.

أثمر بحث لامبورت عن طريقة عملية لكتابة المواصفات عن ورقته البحثية عام 1983 بعنوان "تحديد وحدات البرمجة المتزامنة"، والتي قدّمت فكرة وصف تحولات الحالة على أنها دوال منطقية تعتمد على المتغيرات الأولية وغير الأولية. ^[9]

استمر العمل طوال ثمانينيات القرن العشرين، وبدأ لامبورت في نشر أوراقه البحثية حول المنطق الزمني للأفعال في عام 1990؛ ومع ذلك، لم يتم تقديمه رسميًا حتى نشر "المنطق الزمني للأفعال" في عام 1994. لقد مكّن TLA من استخدام الإجراءات في الصيغ الزمنية، والتي وفقًا لـ Lamport "توفر طريقة أنيقة لتنظيم وتنظيم كل الاستدلالات المستخدمة في التحقق المتزامن من النظام." ^[10]

تتكوَّن مواصفات TLA في الغالب من رياضيات غير زمنية، وهو ما وجده لامبورت أقل تعقيدًا من المواصفات الزمنية البحتة. وقد وفَّر TLA أساسًا رياضيًا للغة المواصفات TLA ⁺ ، التي قُدِمت في الورقة البحثية "تحديد الأنظمة المتزامنة باستخدام TLA ⁺ " في عام 1999. وفي نفس العام، كتب يوان يو أداة التحقق النموذجي TLC الخاصة بمواصفات TLA ⁺ ؛ وقد استُخدامت TLC لاكتشاف أخطاء في بروتوكول تماسك ذاكرة المخبئية في معالج متعدد الأنوية تابع لشركة من Compaq . ^[11]

نشر لامبورت كتابًا دراسيًا شاملًا حول TLA ⁺ في عام 2002، بعنوان "تحديد الأنظمة: لغة وأدوات TLA ⁺ لمهندسي البرمجيات". ^[12]في عام 2009، قدّم لغة PlusCal ^[13] وتليها أداة إثبات المعروفة باسم TLA ⁺ proof (TLAPS) في عام 2012. ^[14] تم الإعلان عن TLA ⁺² في عام 2014، حيث أضاف بعض التراكيب اللغوية الإضافية بالإضافة إلى زيادة الدعم داخل اللغة لنظام الإثبات بشكل كبير.

لامبورت يعمل حاليًا على إعداد مرجع محدّث للغة تحت عنوان TLA ⁺ "The TLA ⁺ Hyperbook". وهو عمل غير مكتمل متاح على موقعه الرسمي. كما يقوم Lamport أيضًا بإنشاء دورة فيديو TLA ⁺ ، والتي تم وصفها فيها بأنها "عمل قيد التقدم يتكون من بداية سلسلة من محاضرات الفيديو لتعليم المبرمجين ومهندسي البرمجيات كيفية كتابة مواصفات TLA ⁺ بأنفسهم".

تُنظَّم مُواصفات TLA ⁺ فِي وحدات. حيث يمكن لكل وحدة النمطية أن تمتد أو تستورد وحدات أخرى لاستخدام وظائفها. على الرغم من أن معيار TLA ⁺ محدد في رموز رياضية منسقة، فإن أدوات TLA ⁺ الحالية تستخدم تعريفات رموز شبيهة بـ LaTeX في ASCII . يستخدم TLA ⁺ العديد من المصطلحات التي تتطلب التعريف:

• الحالة - تعيين القيم للمتغيرات
• السلوك – سلسلة من الحالات
• الخطوة - زوج من الحالات المتتالية في السلوك
• خطوة التأتأة - وهي خطوة لا تتغير فيها المتغيرات
• علاقة الحالة التالية - علاقة تصف كيف يمكن للمتغيرات أن تتغير في أي خطوة
• دالة الحالة - تعبير يحتوي على متغيرات وثوابت ليست علاقة حالة تالية
• مسند الحالة – دالة حالة ذات قيمة منطقية
• ثابت - مسند حالة صحيح في جميع الحالات التي يمكن الوصول إليها
• الصيغة الزمنية - عبارة تحتوي على عبارات في المنطق الزمني

تهتم TLA ⁺ بتعريف مجموعة جميع السلوكيات الصحيحة للنظام. على سبيل المثال، يمكن تحديد ساعة ذات بت واحد تدق بلا نهاية بين 0 و1 على النحو التالي:

الساعة المتغيرة 

Init == clock \in {0, 1}

Tick == IF clock = 0 THEN clock' = 1 ELSE clock' = 0

Spec == Init /\ [][Tick]_<<clock>>

علاقة الحالة التالية Tick تحدد قيمة clock ′ (قيمة clock في الحالة التالية) إلى 1 إذا كانت clock تساوي 0، و0 إذا كانت clock تساوي 1.

المتغير الشرطي Init يكون صحيحًا إذا كانت قيمة clock إما 0 أو 1.

المواصفة Spec هي صيغة زمنية تنص على أن جميع سلوكيات ساعة البت الواحد يجب أن تحقق بداية شرط Init وأن كل خطوة إما متطابقة مع Tick أو خطوات متقطعة. ومن بين هذه السلوكيات:

0 -> 1 -> 0 -> 1 -> 0 -> ...

1 -> 0 -> 1 -> 0 -> 1 -> ...

خصائص السلامة لساعة البت الواحد - أي مجموعة الحالات النظامية الممكن الوصول إليها - يتم وصفها بشكل مناسب بالمواصفات.

المواصفة السابقة تمنع الحالات الغريبة للساعة ذات البت الواحد، ولكنها لا تقول إن الساعة سوف تدق على الإطلاق. على سبيل المثال، يتم قبول السلوكيات التالية التي تؤدي إلى التأتأة بشكل دائم:

وهما: 
 0 -> 0 -> 0 -> 0 -> 0 -> ... 

1 -> 1 -> 1 -> 1 -> 1 -> ...

الساعة التي لا تدقّ ليست مفيدة، لذا يجب استبعاد هذه السلوكيات. إحدى الحلول هي تعطيل التوقف، لكن TLA ⁺ يشترط أن يكون التوقف ممكنًا دائمًا؛ تمثل خطوة التلعثم تغييرًا في جزء من النظام غير الموصوف في المواصفات، وهي مفيدة للتحسين . ولضمان أن عقارب الساعة يجب أن تدق في النهاية، يتم التأكيد على ضعف العدالة فيما يتعلق بـ Tick :

Spec == Init /\ [][Tick]_<<clock>> /\ WF_<<clock>>(Tick)

العدالة الضعيفة بالنسبة لفعل معين تعني أنه إذا كان هذا الفعل ممكنًا بشكل مستمر، فلا بد أن يتم تنفيذه في نهاية المطاف. في حالة الإنصاف الضعيف في علامة التجزئة، يُسمح فقط بعدد محدود من خطوات التلعثم بين العلامات. يُطلق على هذه العبارة المنطقية الزمنية حول تيك اسم تأكيد الحيوية. بشكل عام، يجب أن يكون تأكيد الحيوية مغلقًا آليًا : لا ينبغي أن يقيد مجموعة الحالات التي يمكن الوصول إليها، بل مجموعة السلوكيات الممكنة فقط. ^[15]

معظم المواصفات لا تتطلب إثبات خصائص الحيوية. إذ تكفي خصائص السلامة لكل من التحقق من النموذج التوجيه في تنفيذ النظام. ^[16]

تعتمد لغة TLA ⁺ على نظام زيرميلو-فرانكل ZF ، لذا تتضمن العمليات على المتغيرات التعامل مع المجموعات. تشمل اللغة مجموعة العضوية ، والاتحاد ، والتقاطع ، والفرق ، ومجموعة القوى ، ومشغلات المجموعة الفرعية . كما تتضمن اللغة أيضًا مشغلات المنطق من الدرجة الأولى مثل ∨ و ∧ و ¬ و ⇒ و ↔ و ≡ ، بالإضافة إلى الكميات العالمية والوجودية ∀ و ∃ . كما تتوفر أداة هيلبرت كعامل CHOOSE، الذي يختار عنصرًا فريدًا وعشوائيًا من مجموعة معينة. وتحتوي العمليات الحسابية على الأعداد الحقيقية ، والأعداد الصحيحة ، والأعداد الطبيعية من الوحدات النمطية القياسية.

تحتوي لغة TLA ⁺ على مُشغلات زمنية مدمجة. تستخدم الصيغ الزمنية الرموز التالية: ${\displaystyle \Box P}$ تعني أن العبارة P صحيحة دائمًا، و ${\displaystyle \Diamond P}$ تعني أن P صحيح في النهاية. ويمكن دمج هذه المُشغّلات مثل:

${\displaystyle \Box \Diamond P}$ تعني أن العبارة P صحيحة بشكل متكرر إلى ما لا نهاية، أو ${\displaystyle \Diamond \Box P}$ أن يعني في النهاية أن P سوف يكون صحيحًا دائمًا.

تشمل المشغلات الزمنية الأخرى العدل الضعيف والعادل القوي. إن العدالة الضعيفة WF _e ( A ) تعني أنه إذا تم تمكين الإجراء A بشكل مستمر (أي بدون انقطاعات)، فيجب اتخاذه في النهاية. العدالة القوية SF _e ( A ) تعني أنه إذا تم تمكين الإجراء A بشكل مستمر (بشكل متكرر، مع أو بدون انقطاعات)، فيجب اتخاذه في النهاية.

تتضمن لغة TLA ⁺ ، على الرغم من عدم وجود دعم من الأدوات.

المعاملات المعرفة من قبل المستخدم تشبه الماكرو . وتختلف المعاملات عن الوظائف في أن مجالها لا يشترط أن يكون مجموعة: فعلى سبيل المثال، معامل عضوية المجموعة لديه فئة المجموعات كمجال له، وهي ليست مجموعة صالحة في ZFC (نظرًا لأن وجودها يؤدي إلى مفارقة راسل ). تمت إضافة مشغلات محددة من قبل المستخدم متكررة ومجهولة في TLA ⁺² .

البنية الأساسية للبيانات في TLA ⁺ هي المجموعة. تُنشأ المجموعات إما بالتعداد الصريح لعناصرها، أو من مجموعات أخرى باستخدام معاملات، أو بصيغة {x \in S : p} حيث p هو شرط على x ، أو بصيغة {e : x \in S} حيث e دالة على x . المجموعة الفارغة الفريدة تُمثَّل بـ {} .

الوظائف في TLA ⁺ تُسنِد قيمة لكل عنصر في مجالها، والذي يكون مجموعة. التعبير [S -> T]يمثل مجموعة جميع الدوال التي يكون فيها f[ x ] منتمية إلى T ، لكل x في مجموعة المجال S.

على سبيل المثال، الدالة في TLA ⁺ Double[x \in Nat] == x*2 هي عنصر من المجموعة [Nat -> Nat] وبالتالي فإن العبارة Double \in [Nat -> Nat] هي عبارة صحيحة في TLA ⁺ . كما يمكن تعريف الوظائف باستخدام الصيغة [x \in S |-> e] لبعض التعبيرات e ، أو عن طريق تعديل وظيفة موجودة [f EXCEPT ![v 1 ] = v 2 ] .

السجلات هِي نَوُع من الوظائف في TLA ⁺ . السجل [name |-> "John", age |-> 35] هو سجل يحتوي على الحقول name وage، ويمكن الوصول إليه باستخدام r.name و r.age .

هذا السجل ينتمي إلى مجموعة السجلات المعرفة بالشكل [name : String, age : Nat] .

تتضمّن العناصر في TLA ⁺ . يتم تعريفها صراحةً هذه باستخدام الصيغة <<e 1 ,e 2 ,e 3 >> أو يمكن إنشاؤها باستخدام المعاملات الموجودة في التسلسلات القياسية. يتم تعريف مجموعات الكائنات المرتبة من خلال حاصل الضرب الديكارتي ؛ على سبيل المثال، تُعرَّف مجموعة جميع أزواج الأعداد الطبيعية بـ Nat \X Nat .

تمتلك TLA ⁺ مجموعة من الوحدات القياسية التي تحتوي على المعاملات الشائعة. يتم توزيع هذه الوحدات من محلل الصياغة. ويستخدم مدقق النماذج TLC نسخًا مُنفذة بلغة Java لتحسين الأداء.

• FiniteSets : وحدة للعمل مع المجموعات المحدودة . يوفر مشغلي IsFiniteSet(S) و Cardinality(S) .
• التسلسلات : تحدد المشغلات على الثنائيات مثل Len(S) ، و Head(S) ، و Tail(S) ، و Append(S, E) ، و concatenation ، و filter .
• الحقائب : وحدة للعمل مع مجموعات متعددة . يوفر نظائر تشغيل المجموعة البدائية والعد المكرر.
• الأعداد الطبيعية : تحدد الأعداد الطبيعية إلى جانب المتباينات والعمليات الحسابية.
• الأعداد الصحيحة : تُعرَّف الأعداد الصحيحة .
• الأعداد الحقيقية : تحدد الأعداد الحقيقية إلى جانب القسمة واللانهاية .
• الوقت الحقيقي : يوفر تعريفات مفيدة في مواصفات النظام في الوقت الحقيقي .
• TLC : توفر وظائف مفيدة للمواصفات التي تم فحصها بواسطة النموذج، مثل التسجيل والتأكيدات.

يتم استيراد الوحدات القياسية في TLA+ باستخدام عبارتي EXTENDS أو INSTANCE .

في شركة Microsoft ، تَمَ اكتشاف خطأ حرج في وحدة ذاكرة Xbox 360 أثناء عملية كتابة المواصفات باستخدام TLA ⁺ . ^[22] استُخدام TLA ⁺ أيضًا لكتابة براهين رسمية لصحة Byzantine Paxos ومكونات جدول التجزئة الموزع Pastry . ^[19]

تستخدم Amazon Web Services تقنية TLA ⁺ منذ عام 2011. كشف التحقق من النماذج باستخدام TLA ⁺ عن أخطاء في DynamoDB و S3 و EBS ومدير القفل الموزع الداخلي؛ بعض هذه الأخطاء تطلّب تتبع حالة يتضمن 35 خطوة. كما استُخدم التحقق من النماذج للتحقق من صحة تحسينات متقدمة. بالإضافة إلى ذلك، وُجد أن مواصفات TLA ⁺ تحمل قيمة كبيرة كوثائق ومساعدات في التصميم. ^{[23] [24]}

استخدمت Microsoft Azure تقنية TLA ⁺ لتصميم Cosmos DB ، وهي قاعدة بيانات موزعة عالميًا تدعم خمسة نماذج مختلفة للاتساق. ^{[25] [26]}

استخدمت شركة Altreonic NV أداة TLA+ للتحقق من نموذج OpenComRTOS .

متجر القيمة الرئيسية مع عزل اللقطة :

--------------------------- MODULE KeyValueStore ---------------------------
CONSTANTS  Key,      \* The set of all keys.
      Val,      \* The set of all values.
      TxId      \* The set of all transaction IDs.
VARIABLES  store,     \* A data store mapping keys to values.
      tx,       \* The set of open snapshot transactions.
      snapshotStore, \* Snapshots of the store for each transaction.
      written,    \* A log of writes performed within each transaction.
      missed     \* The set of writes invisible to each transaction.
----------------------------------------------------------------------------
NoVal ==  \* Choose something to represent the absence of a value.
  CHOOSE v : v \notin Val

Store ==  \* The set of all key-value stores.
  [Key -> Val \cup {NoVal}]

Init == \* The initial predicate.
  /\ store = [k \in Key |-> NoVal]    \* All store values are initially NoVal.
  /\ tx = {}               \* The set of open transactions is initially empty.
  /\ snapshotStore =           \* All snapshotStore values are initially NoVal.
    [t \in TxId |-> [k \in Key |-> NoVal]]
  /\ written = [t \in TxId |-> {}]    \* All write logs are initially empty.
  /\ missed = [t \in TxId |-> {}]     \* All missed writes are initially empty.
  
TypeInvariant ==  \* The type invariant.
  /\ store \in Store
  /\ tx \subseteq TxId
  /\ snapshotStore \in [TxId -> Store]
  /\ written \in [TxId -> SUBSET Key]
  /\ missed \in [TxId -> SUBSET Key]
  
TxLifecycle ==
  /\ \A t \in tx :  \* If store != snapshot & we haven't written it, we must have missed a write.
    \A k \in Key : (store[k] /= snapshotStore[t][k] /\ k \notin written[t]) => k \in missed[t]
  /\ \A t \in TxId \ tx : \* Checks transactions are cleaned up after disposal.
    /\ \A k \in Key : snapshotStore[t][k] = NoVal
    /\ written[t] = {}
    /\ missed[t] = {}

OpenTx(t) ==  \* Open a new transaction.
  /\ t \notin tx
  /\ tx' = tx \cup {t}
  /\ snapshotStore' = [snapshotStore EXCEPT ![t] = store]
  /\ UNCHANGED <<written, missed, store>>

Add(t, k, v) == \* Using transaction t, add value v to the store under key k.
  /\ t \in tx
  /\ snapshotStore[t][k] = NoVal
  /\ snapshotStore' = [snapshotStore EXCEPT ![t][k] = v]
  /\ written' = [written EXCEPT ![t] = @ \cup {k}]
  /\ UNCHANGED <<tx, missed, store>>
  
Update(t, k, v) == \* Using transaction t, update the value associated with key k to v.
  /\ t \in tx
  /\ snapshotStore[t][k] \notin {NoVal, v}
  /\ snapshotStore' = [snapshotStore EXCEPT ![t][k] = v]
  /\ written' = [written EXCEPT ![t] = @ \cup {k}]
  /\ UNCHANGED <<tx, missed, store>>
  
Remove(t, k) == \* Using transaction t, remove key k from the store.
  /\ t \in tx
  /\ snapshotStore[t][k] /= NoVal
  /\ snapshotStore' = [snapshotStore EXCEPT ![t][k] = NoVal]
  /\ written' = [written EXCEPT ![t] = @ \cup {k}]
  /\ UNCHANGED <<tx, missed, store>>
  
RollbackTx(t) ==  \* Close the transaction without merging writes into store.
  /\ t \in tx
  /\ tx' = tx \ {t}
  /\ snapshotStore' = [snapshotStore EXCEPT ![t] = [k \in Key |-> NoVal]]
  /\ written' = [written EXCEPT ![t] = {}]
  /\ missed' = [missed EXCEPT ![t] = {}]
  /\ UNCHANGED store

CloseTx(t) ==  \* Close transaction t, merging writes into store.
  /\ t \in tx
  /\ missed[t] \cap written[t] = {}  \* Detection of write-write conflicts.
  /\ store' =             \* Merge snapshotStore writes into store.
    [k \in Key |-> IF k \in written[t] THEN snapshotStore[t][k] ELSE store[k]]
  /\ tx' = tx \ {t}
  /\ missed' =  \* Update the missed writes for other open transactions.
    [otherTx \in TxId |-> IF otherTx \in tx' THEN missed[otherTx] \cup written[t] ELSE {}]
  /\ snapshotStore' = [snapshotStore EXCEPT ![t] = [k \in Key |-> NoVal]]
  /\ written' = [written EXCEPT ![t] = {}]

Next == \* The next-state relation.
  \/ \E t \in TxId : OpenTx(t)
  \/ \E t \in tx : \E k \in Key : \E v \in Val : Add(t, k, v)
  \/ \E t \in tx : \E k \in Key : \E v \in Val : Update(t, k, v)
  \/ \E t \in tx : \E k \in Key : Remove(t, k)
  \/ \E t \in tx : RollbackTx(t)
  \/ \E t \in tx : CloseTx(t)
    
Spec == \* Initialize state with Init and transition with Next.
  Init /\ [][Next]_<<store, tx, snapshotStore, written, missed>>
----------------------------------------------------------------------------
THEOREM Spec => [](TypeInvariant /\ TxLifecycle)
=============================================================================

• التواصل بشأن العمليات المتسلسلة
• سبيكة (لغة المواصفات)
• الطريقة ب
• منطق شجرة الحساب
• بلس كال
• المنطق الزمني
• المنطق الزمني للأفعال
• تدوين Z