aaltitoad ดาวน์โหลด - ดาวน์โหลดซอร์สโค้ด aaltitoad ดาวน์โหลด

aaltitoad

ซอร์สโค้ดอื่น ๆ

v1.2.0

ดาวน์โหลด

Aal Borg Ti CK ถึง CK A Utomata Vali D ator - เครื่องมือตรวจสอบและจำลองการตรวจสอบที่ขยายได้สำหรับ Tick Tock Automata

Tick Tock Automata คืออะไร?

TTA's (Tick Tock Automata) เป็นทฤษฎีที่ใช้อัตโนมัติซึ่งสามารถสร้างแบบจำลองตรรกะทางธุรกิจแบบขนานสำหรับระบบอัตโนมัติทุกประเภท TTA ประกอบด้วยชุดของสถานที่และการเปลี่ยนระหว่างพวกเขา การเปลี่ยนแปลงแต่ละครั้งสามารถได้รับการปกป้องจาก การแสดงออกของบูลีน และมีชุดของ การกำหนดตัวแปร เป็น "ผลที่ตามมา" ของ การ เปลี่ยนผ่าน

การเปรียบเทียบที่ดีสำหรับ TTA คือ statemachine ซึ่งระบบสามารถเปลี่ยนจากรัฐหนึ่งไปอีกสถานะหนึ่ง ด้านล่างเป็นตัวอย่างของ TTA อย่างง่ายที่ควบคุมแสงตามอินพุตปุ่ม

เริ่มต้นในตำแหน่งปิดมีเพียงหนึ่งขอบขาออกที่มีตัวป้องกันที่ตรวจสอบว่า btn_is_pressed เป็น จริง หรือไม่ ถ้าเป็นเช่นนั้นเราจะย้ายไปยังตำแหน่ง ON และตั้ง light ตัวแปรให้เป็น จริง ซึ่งเป็นผลมาจาก การใช้ ขอบ/การเปลี่ยนแปลง จากนั้นเมื่อปุ่มถูกปล่อยออกมาเราจะกลับไปที่ OFF Locaiton และ light ถูกตั้งค่าเป็น FALSE อีกครั้ง

สิ่งที่ทำให้ TTAs แตกต่างจากระบบการเปลี่ยนแปลงอื่น ๆ คือตัวแปร btn_is_pressed เป็นตัวแปร ภายนอก ซึ่งหมายความว่าไม่สามารถกำหนดค่าใด ๆ ได้โดยระบบการเปลี่ยนแปลงมันสามารถเปลี่ยนแปลงได้ตามอินพุตภายนอกเท่านั้น อินพุตภายนอกจะถูกอ่านเมื่อเราไม่ได้เปลี่ยนผ่าน การแยกความหมายนี้เป็นที่ที่ชื่อ Tick Tock Automata มาจาก:

Tick-Step: ประเมินยามใช้การอัปเดตเปลี่ยนตำแหน่ง
TOCK-Step: อ่านอินพุตภายนอกเขียนเอาต์พุตภายนอก

การใช้ไวยากรณ์อีกขั้นหนึ่งคุณสามารถมี TTAs เหล่านี้จำนวนมากที่ทำงานในแบบคู่ขนานแบ่งปันกลุ่มเดียวกันของตัวแปรภายในและภายนอก เครือข่ายดังกล่าวเรียกว่าเพียง n etwork ของ t ick t ock a utomata (ntta)

การอ่านเพิ่มเติม

บทความนี้อธิบายทฤษฎี Tick Tock Automata ฐาน
บทความนี้อธิบายรายละเอียดการวนซ้ำใหม่ล่าสุดของเครื่องมือ (v1.0.0+)
บทความนี้อธิบายการวนซ้ำครั้งแรกของเครื่องมือ (v0.10.x)
ลองดูที่ h-uppaal ถ้าคุณต้องการสร้าง TTAs ด้วยตัวเอง

รวบรวม (Linux)

Aaltitoad ถูกสร้างขึ้นโดยใช้ CMake คุณต้องมีคอมไพเลอร์ที่เข้ากันได้ C ++ 20, flex , bison เวอร์ชัน 3.5+ และไลบรารีเทมเพลตมาตรฐานที่ติดตั้ง การพึ่งพาอื่น ๆ ทั้งหมดได้รับการจัดการผ่านตัวจัดการแพ็คเกจ CPM ที่ยอดเยี่ยม

mkdir build && cd build
cmake -DCMAKE_BUILD_TYPE=Release ..
make

หากขั้นตอน CPM ใช้เวลานานให้ลองรันใหม่ด้วย -DCPM_SOURCE_CACHE=~/.cache/CPM

ทดสอบ

ในการเรียกใช้การทดสอบหน่วยให้รวบรวมเป้าหมาย 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

หากคุณต้องการรวมสถิติการปกคลุมด้วยรหัสให้ระบุ -DCODE_COVERAGE=ON ธง CMake

วิธีใช้

Aaltitoad จัดเตรียมเป้าหมายการรวบรวมหลักสามเป้าหมาย อินเทอร์เฟซ Commandline ทั้งหมดมีหน้าวิธีใช้ที่คุณสามารถเรียกใช้กับอาร์กิวเมนต์ --help

verifier : อินเทอร์เฟซบรรทัดคำสั่งของเอ็นจินการตรวจสอบ
- ใช้สิ่งนี้หากคุณต้องการวิเคราะห์ NTTA ของคุณ
simulator : อินเตอร์เฟสบรรทัดคำสั่งรันไทม์
- ใช้สิ่งนี้หากคุณต้องการเรียกใช้ NTTA และลิงก์ของคุณกับ tockers ที่กำหนดเองของคุณ (ดูด้านล่าง)
aaltitoad : ห้องสมุดที่มีทุกสิ่ง Aaltitoad
- ใช้สิ่งนี้เพื่อสร้างแอปพลิเคชันที่ใช้ NTTA ของคุณเองเช่นตัวตรวจสอบอื่นรันไทม์หรือแม้แต่คอมไพเลอร์

ปลั๊กอิน Tocker

Aaltitoad รองรับไลบรารี "Tocker" ของบุคคลที่สามเพื่อให้คุณสามารถฉีดการรวมที่กำหนดเองลงในรันไทม์โดยตรง ที่เก็บนี้ให้ตัวอย่าง tocker ที่เรียกว่า pipe_tocker ในไดเรกทอรี tocker_plugins เพื่อใช้เป็นตัวอย่างโครงการ "tocker" ต้องกำหนดสัญลักษณ์ต่อไปนี้:

# 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 หมายถึง C-String ที่จัดทำโดยฟังก์ชัน get_plugin_name ชื่อฟังก์ชั่นจะต้องตรงกันมิฉะนั้นปลั๊กอินจะไม่โหลด ปลั๊กอิน Tocker ต้องเชื่อมโยงกับไลบรารีที่ใช้ร่วมกัน aaltitoad และควรรวบรวมเป็นไลบรารีที่ใช้ร่วมกันเช่น:

 add_library (TOCKER_NAME_tocker SHARED *.cpp)
target_link_libraries (TOCKER_NAME_tocker aaltitoad)

เมื่อรวบรวมแล้วคุณสามารถสร้างอินสแตนซ์ tocker ได้โดยการจัดหา --tocker / -t ร่วมกับ --tocker-dir / -T ไปยังบรรทัดคำสั่ง Aaltitoad ควรให้ตัวเลือก --tocker เช่นนั้น:

--tocker-dir /path/to/tocker-plugins --tocker " TOCKER_NAME(argument string) "

"argument string" -ส่วนหนึ่งของตัวเลือกหมายถึงสตริงอาร์กิวเมนต์อินพุตที่มีให้กับฟังก์ชัน create_TOCKER_NAME ตอนนี้ tockers ของคุณควรได้รับการสร้างอินสแตนซ์และฟังก์ชั่น tock จะถูกเรียกว่าทุกครั้งที่ TTA พร้อมที่จะคำนวณค่า tocker

ประเภท tocker

มีอินเทอร์เฟซ tocker สองประเภทที่ Tocker ของบุคคลที่สามสามารถขยายได้:

การปิดกั้น tockers (ค่าเริ่มต้น tocker_t )
tockers แบบอะซิงโครนัส ( async_tocker_t )

Tocker ที่ปิดกั้นจะทำงานในเธรดเดียวและจะปิดกั้นการตรวจสอบข้อเสนอทั้งหมดจนกว่า TOCK จะเสร็จสิ้นและการรวมบุคคลที่สามควรแทนที่ฟังก์ชั่น tock เท่านั้น ในทางตรงกันข้าม tocker แบบอะซิงโครนัสจะไม่บล็อกการดำเนินการเห็บ แต่เริ่มงานแบบอะซิงโครนัสใหม่ของฟังก์ชั่น get_tock_values

เมื่อใช้ tocker ของคุณคุณควรพิจารณาว่าคุณต้องการบล็อก TTA จากการดำเนินการหรือไม่ หากคุณเลือกที่จะใช้ tocker แบบอะซิงโครนัสโปรดทราบว่าสภาพแวดล้อมการป้อนข้อมูลสามารถเปลี่ยนแปลงได้ตั้งแต่มีการออก TOCK

ปลั๊กอินตัวแยกวิเคราะห์

หากคุณไม่ต้องการใช้ตัวแยกวิเคราะห์ที่ให้มาคุณสามารถจัดหาของคุณเองได้ตลอดเวลา ตราบใดที่คุณให้สัญลักษณ์ต่อไปนี้ (จำ 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;
    }
}