👨🏾‍💼 🙀 🧔🏾 Cara Menangkap Kucing dengan TLA + 🌬️ 👲🏾 🧑🏿‍🤝‍🧑🏿

Banyak programmer yang berjuang ketika menggunakan metode formal untuk menyelesaikan masalah dalam program mereka, karena metode tersebut, walaupun efektif, bisa sangat kompleks. Untuk memahami mengapa ini terjadi, mari kita gunakan metode pengecekan model untuk memecahkan teka-teki yang relatif mudah:

Ketentuan

Anda berada di lorong dengan tujuh pintu di satu sisi mengarah ke tujuh kamar. Seekor kucing bersembunyi di salah satu kamar ini. Tugas Anda adalah menangkap kucing. Membuka pintu membutuhkan satu langkah. Jika Anda menebak pintu yang benar, Anda menangkap kucing itu. Jika Anda tidak menebak pintu yang benar, kucing berlari ke kamar sebelah.

TLA + dan logika temporal

Beberapa alat dapat memecahkan masalah seperti ini. Sebagai contoh, pemecah SMT , yang sering digunakan dalam kasus-kasus ini, menggunakan logika predikat untuk menyelesaikan masalah, tetapi itu membutuhkan penggunaan array, yang merepotkan bagi programmer dan seringkali menghasilkan urutan tindakan kompleks yang tidak perlu. TLA + , di sisi lain, menggunakan logika temporal, yang memungkinkan program untuk menggunakan keadaan sistem baik pada langkah saat ini dan selanjutnya dalam satu pernyataan.

CatDistr' = CatDistr \ {n}

Kondisi ini menyatakan bahwa setelah memeriksa di belakang pintu N, jumlah pintu tempat kucing dapat ditemukan, bertepatan dengan seperangkat kamar tempat N diambil. (Jika kucing itu di belakang pintu N, tentu saja, dia tertangkap.)

Dalam bahasa pemrograman imperatif, ini menciptakan variabel baru yang dihitung dari yang lama.

Tentang set

Posisi kucing ditentukan oleh variabel dalam himpunan semua kamar yang mungkin, bukan ruang tertentu seperti dalam sistem pemodelan simulasi. Metode formal pemrograman mempertimbangkan pluralitas dari nilai yang mungkin, bukan nilai saat ini. Ini seringkali terlalu rumit untuk pengembang pemula, jadi menyederhanakan sistem ini akan membantu pengembang tersebut bekerja lebih cepat.

Struktur program dalam TLA +

Program ini terdiri dari deklarasi dan pernyataan (prediktor), yang menggambarkan:

Keadaan awal
Tautan antara kondisi aktual
Keadaan selanjutnya
Invarian yang beroperasi di semua negara bagian yang tersedia.

Mungkin ada juga predikat tambahan (misalnya parameter) yang terlibat.

 ---- 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 /= {} =============================================================================

Dalam contoh itu:

Baris pertama dan terakhir menyatakan bahwa ini adalah modul sumber.
== berarti 'sama dengan definisi'.
= berarti nilai ekspresi yang dihitung sama
Pintu adalah set konstan dalam file konfigurasi.
CatDistr menentukan ruangan tempat kucing itu berada.
Variabel LastDoor , yang mewakili ruang terakhir diperiksa, mudah membaca output dari program. Untuk model besar, variabel tersebut dapat memperlambat alur kerja program dan meningkatkan jumlah status yang perlu dianalisis. Namun dalam model ini, negara bagian sekarang memuat sejarah pintu mana yang dibuka. Dengan demikian, keadaan yang sama dibuat dengan cara yang berbeda sekarang berbeda.
Prediktor Init menggambarkan kondisi awal program - dalam hal ini, belum ada pintu yang dibuka.
OpenDoor (n) menjelaskan apa yang terjadi ketika pintu n dibuka - apakah Anda menangkap kucing, atau tidak.
Prediktor berikutnya ada karena TLA + tidak tahu di ruang mana kita mungkin masuk berikutnya, sehingga akan memeriksa untuk melihat apakah invarian benar dalam setiap kasus.

Berikut ini varian yang lebih jelas:
```
 Next == OpenDoor(0) \/ OpenDoor(1) \/ ... \/ OpenDoor(Doors) 
```
Dalam hal ini, kode berfungsi dengan jumlah kamar tetap, membuat kode parameter.
Akhirnya, invarian CatWalk menentukan di mana kucing bersembunyi. Pelanggaran invarian berarti kucing itu ditangkap di mana pun ia bersembunyi. Saat memverifikasi spesifikasi, pelanggaran invarian adalah kesalahan, tetapi karena kami tidak menggunakan alat untuk tujuan yang dimaksud, mendapatkan kesalahan dalam hal ini berarti menyelesaikan masalah.

Konfigurasi model

 CONSTANTS Doors = 6 INIT Init NEXT Next INVARIANT CatWalk

Konfigurasi ini mencakup kondisi awal, jumlah kamar, kondisi untuk perubahan keadaan, dan pengujian yang dapat diverifikasi.

Anda dapat menjalankan model ini dari baris perintah menggunakan perintah ini:
tlc2 -config cat.cfg cat.tla .

TLA + memiliki GUI canggih dan diluncurkan oleh perintah tla-toolbox . Sayangnya, ia tidak mengerti file .cfg , sehingga parameter model harus dikonfigurasi melalui menu.

Kesimpulan

Membuat program khusus ini cukup sederhana, tetapi dalam banyak kasus, menerapkan metode formal akan membutuhkan model yang jauh lebih besar dan penggunaan berbagai konstruksi bahasa. Kami berharap memecahkan teka-teki sederhana seperti ini akan memberikan cara yang mudah dan menarik untuk menerapkan metode formal proyek kerja.

Program sederhana untuk verifikasi solusi interaktif dapat ditemukan di sini .
Pelajari lebih lanjut tentang TLA + di sini .