كيفية التقاط القط مع TLA +

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

الشروط

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

TLA + والمنطق الزمني

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

CatDistr' = CatDistr \ {n} 

تنص هذه الحالة على أنه بعد التحقق من وراء الباب N ، يتطابق عدد الأبواب التي يمكن تحديد موقع القط فيها مع مجموعة الغرف التي تم أخذ N منها. (إذا كانت القطة وراء الباب N ، بالطبع ، فقد تم القبض عليه.)

في لغة البرمجة الحتمية ، يؤدي هذا إلى إنشاء متغير جديد محسوب من المتغير القديم.

حول مجموعات

يتم تحديد موضع القط بواسطة متغير داخل مجموعة جميع الغرف الممكنة ، بدلاً من غرفة محددة كما في نظام نمذجة المحاكاة. تأخذ الطرق الرسمية للبرمجة في الاعتبار تعدد القيم الممكنة ، بدلاً من القيمة الحالية. غالبًا ما يكون هذا الأمر معقدًا للغاية بالنسبة للمطورين الأساسيين ، لذا فإن تبسيط هذا النظام سيساعد هؤلاء المطورين على العمل بسرعة أكبر.

هيكل البرنامج في TLA +

يتكون البرنامج من الإعلانات والبيانات (المتنبئين) ، والتي تصف:

• الحالة الأولية
• الصلة بين الحالات الفعلية
• الدولة القادمة
• ثابت يعمل في جميع الحالات المتاحة.

قد يكون هناك أيضا مسندات مساعدة (مثل المعلمات) المعنية.

 ---- MODULE cat ------------------------------------------------------------- EXTENDS Integers CONSTANTS Doors VARIABLES CatDistr, LastDoor Init == /\ CatDistr = 0..Doors /\ LastDoor = -1 OpenDoor(n) == /\ CatDistr' = 0..Doors \intersect UNION { {x-1, x+1} : x \in CatDistr \ {n} } /\ LastDoor' = n Next == \E door \in 0..Doors : OpenDoor(door) CatWalk == CatDistr /= {} ============================================================================= 

في هذا المثال:

• يعلن السطران الأول والأخير أن هذه وحدة نمطية للمصدر.
• == يعني "بالتساوي بحكم التعريف".
• = يعني أن قيم التعبير المحسوبة متساوية
• الأبواب هي مجموعة ثابتة في ملف التكوين.
• يحدد CatDistr الغرفة التي يقع فيها القط.
• المتغير LastDoor ، الذي يمثل الغرفة المحددة الأخيرة ، يقرأ بسهولة إخراج البرنامج. بالنسبة للنماذج الكبيرة ، قد تؤدي هذه المتغيرات إلى إبطاء سير عمل البرنامج وزيادة عدد الحالات التي تحتاج إلى تحليل. ومع ذلك ، في هذا النموذج ، تحتوي الدولة الآن على تاريخ فتح الأبواب. وهكذا ، أصبحت الحالات المتساوية التي تم إنشاؤها بطرق مختلفة مختلفة الآن.
• يصف متنبئ التهيئة الحالة الأولية للبرنامج - في هذه الحالة ، لم يتم فتح أي أبواب بعد.
• يصف OpenDoor (n) ما يحدث عندما يتم فتح الباب n - إما أنك اشتعلت القطة ، أو لم تفعل ذلك.
• يوجد التوقع التالي لأن TLA + لا يعرف في أي غرفة قد ندخل بعد ذلك ، لذلك سوف يتحقق لمعرفة ما إذا كان المتغيرون صحيحين في كل حالة.
  
  إليك متغير أكثر وضوحًا:
  
  

   Next == OpenDoor(0) \/ OpenDoor(1) \/ ... \/ OpenDoor(Doors) 

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

التكوين النموذجي

 CONSTANTS Doors = 6 INIT Init NEXT Next INVARIANT CatWalk 

يتضمن هذا التكوين الشرط الأولي وعدد الغرف وشروط تغيير الحالة واختبار يمكن التحقق منه.

يمكنك تشغيل هذا النموذج من سطر الأوامر باستخدام هذا الأمر:
tlc2 -config cat.cfg cat.tla .

يحتوي TLA + على واجهة المستخدم الرسومية المتقدمة ويتم تشغيله بواسطة الأمر tla -toolbox . لسوء الحظ ، لا يفهم ملفات .cfg ، لذلك يجب تكوين معلمات النموذج من خلال القائمة.

استنتاج

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

• يمكن العثور هنا على برنامج بسيط للتحقق من الحلول التفاعلية.
• تعرف على المزيد حول TLA + هنا .