aaltitoad
v1.2.0
Aal borg ti ck ke ck a utomata vali d ator - mesin verifikasi dan simulator yang dapat diperpanjang untuk centang tock automata.
TTA (Tick Tock Automata) adalah teori berbasis automata yang dapat memodelkan logika bisnis paralel untuk semua jenis sistem otomatisasi. TTA terdiri dari satu set lokasi dan transisi di antara mereka. Setiap transisi dapat dijaga oleh ekspresi boolean dan memiliki serangkaian penugasan variabel sebagai "konsekuensi" untuk mengambil transisi.
Analogi yang baik dengan TTA adalah statemachine , di mana suatu sistem dapat beralih dari satu negara ke negara lain. Di bawah ini adalah contoh TTA sederhana yang mengontrol lampu berdasarkan input tombol.
Mulai di lokasi off, hanya ada satu tepi keluar dengan penjaga yang memeriksa apakah btn_is_pressed benar . Jika ya, kami pindah ke lokasi di dan mengatur light variabel ke true sebagai konsekuensi dari mengambil tepi/transisi. Kemudian, ketika tombol dilepaskan, kami kembali ke Off Locaiton dan light diatur ke False lagi.
Apa yang membuat TTA berbeda dari sistem transisi lainnya adalah bahwa variabel btn_is_pressed adalah variabel eksternal , yang berarti bahwa ia tidak dapat ditetapkan untuk nilai apa pun oleh sistem transisi, ia hanya dapat berubah berdasarkan input eksternal. Input eksternal dibaca ketika kita tidak mengambil transisi. Perpecahan semantik ini adalah tempat nama Tock Automata berasal:
Mengambil sintaks satu langkah lebih jauh, Anda dapat memiliki banyak TTA ini berjalan secara paralel, berbagi kumpulan variabel internal dan eksternal yang sama. Jaringan semacam itu disebut hanya merupakan pekerjaan dari utomata (NTTA).
Aaltitoad dibangun menggunakan cmake. Anda harus memiliki kompiler C ++ 20 yang kompatibel, flex , versi bison 3.5+ dan pustaka template standar yang diinstal. Semua dependensi lain ditangani melalui manajer paket CPM yang luar biasa.
mkdir build && cd build
cmake -DCMAKE_BUILD_TYPE=Release ..
make Jika langkah CPM memakan waktu lama, coba rerunning dengan -DCPM_SOURCE_CACHE=~/.cache/CPM
Untuk menjalankan tes unit, kompilasi target aaltitoad_tests
mkdir build-test && cd build-test
cmake -DCMAKE_BUILD_TYPE=Debug ..
make aaltitoad_tests
# run the tests
./aaltitoad_test -r xml -d yes --order lex Jika Anda ingin menyertakan statistik kode -cakupan, berikan -DCODE_COVERAGE=ON bendera cmake.
Aaltitoad menyediakan tiga target kompilasi utama. Semua antarmuka Commandline memiliki halaman bantuan yang dapat Anda panggil dengan argumen --help .
verifier : Antarmuka Baris Perintah Mesin Verifikasisimulator : Antarmuka baris perintah runtimeaaltitoad : Perpustakaan dengan semua hal aaltitoad AALTITOAD mendukung perpustakaan "Toker" pihak ketiga, sehingga Anda dapat menyuntikkan integrasi khusus langsung ke runtime. Repositori ini memberikan contoh Toker yang disebut pipe_tocker di direktori tocker_plugins untuk berfungsi sebagai contoh proyek. "Toker" harus menentukan simbol -simbol berikut:
# include < plugin_system.h > // aaltitoad::* typedefs
extern " C " {
const char * get_plugin_name (); // Return value of this func dictates the name the next two funcs
aaltitoad:: tocker_t * create_TOCKER_NAME ( const std::string& argument, const aaltitoad:: ntta_t & ntta);
void destroy_TOCKER_NAME ( tocker_t * tocker);
plugin_type get_plugin_type () {
return plugin_type::tocker;
}
} TOCKER_NAME mengacu pada c-string yang disediakan oleh fungsi get_plugin_name . Nama fungsi harus cocok, jika tidak plugin tidak akan dimuat. Plugin Toker harus menautkan dengan pustaka bersama aaltitoad , dan harus dikompilasi sebagai perpustakaan bersama, seperti itu:
add_library (TOCKER_NAME_tocker SHARED *.cpp)
target_link_libraries (TOCKER_NAME_tocker aaltitoad) Setelah dikompilasi, Anda dapat membuat instantiasi Toker dengan menyediakan --tocker / -t bersama -sama dengan --tocker-dir / -T ke baris perintah Aaltitoad. Opsi --tocker harus disediakan seperti itu:
--tocker-dir /path/to/tocker-plugins --tocker " TOCKER_NAME(argument string) " "argument string" -Part dari opsi mengacu pada string argumen input yang disediakan untuk fungsi create_TOCKER_NAME . Sekarang Toker Anda seharusnya dipakai, dan fungsi tock akan dipanggil setiap kali TTA siap menghitung nilai Toker.
Ada dua jenis antarmuka Toker yang dapat diperluas oleh Toker pihak ketiga:
tocker_t )async_tocker_t ) Toker pemblokiran akan berjalan dalam satu utas dan akan memblokir semua eksekusi kutu sampai Tock telah selesai, dan integrasi pihak ketiga hanya boleh mengesampingkan fungsi tock . Sebaliknya, tokok asinkron tidak akan memblokir eksekusi kutu, tetapi memulai tugas asinkron baru dari fungsi get_tock_values .
Saat menerapkan Toker Anda, Anda harus mempertimbangkan jika Anda ingin memblokir TTA dari mengeksekusi atau tidak. Jika Anda memilih untuk mengimplementasikan Toker Asynchronous, ketahuilah bahwa lingkungan input dapat berubah sejak Tock dikeluarkan.
Jika Anda tidak ingin menggunakan parser yang disertakan, Anda selalu dapat menyediakan sendiri. Selama Anda memberikan simbol -simbol berikut (ingat extern "C" ):
# include < plugin_system.h > // aaltitoad::* typedefs
extern " C " {
const char * get_plugin_name ();
const char * get_plugin_version ();
aaltitoad:: ntta_t * load ( const std::vector<std::string>& folders, const std::vector<std::string>& ignore_list);
plugin_type get_plugin_type () {
return plugin_type::parser;
}
} Untuk membuatnya sedikit lebih mudah membangun objek aaltitoad::ntta_t , kami menyediakan beberapa kelas pembangun: aaltitoad::tta_builder dan aaltitoad::ntta_builder
