>From 3390ccc51f46ce0a4baa60422a62530c7c3c29bd Mon Sep 17 00:00:00 2001 From: Andrew Butterfield <andrew.butterfi...@scss.tcd.ie> Date: Wed, 21 Dec 2022 18:03:47 +0000 Subject: [PATCH 00/18] Adds Formal Verification Material
This patch-set adds in the Promela/SPIN models and tools developed as part of the ESA-sponsored activity "Qualification of RTEMS Symmetric Multiprocessing (SMP)" as well as result of ongoing contributions by students at Trinity College Dublin to improve and extend them. It is a subset of the material contained at https://github.com/andrewbutterfield/RTEMS-SMP-Formal It focusses in the main on what currently produces RTEMS test code. Andrew Butterfield (18): adds in high-level directories and READMEs adds barrier manager model adds barrier manager generated material adds chains API model adds chain api generated material adds event manager model adds event manager generated material adds message manager model adds message manager generated material adds weak memory models adds in draft MrsP models for requirements and code third party code - promela parser modifies 3rd party code - promela parser third party code - comment filter modifies 3rd party code - comment filter adds test generation source code adds tests for testgen code adds automatic testgen examples formal/.gitignore | 3 + formal/README.md | 27 + formal/promela/.gitignore | 4 + formal/promela/README.md | 27 + formal/promela/models/README.md | 53 + formal/promela/models/barriers/README.md | 11 + formal/promela/models/barriers/STATUS.md | 95 + .../20221220-102256/barrier-mgr-model-0.spn | 220 +++ .../20221220-102256/barrier-mgr-model-1.spn | 216 +++ .../20221220-102256/barrier-mgr-model-10.spn | 233 +++ .../20221220-102256/barrier-mgr-model-11.spn | 229 +++ .../20221220-102256/barrier-mgr-model-12.spn | 236 +++ .../20221220-102256/barrier-mgr-model-13.spn | 232 +++ .../20221220-102256/barrier-mgr-model-14.spn | 212 +++ .../20221220-102256/barrier-mgr-model-15.spn | 208 +++ .../20221220-102256/barrier-mgr-model-16.spn | 224 +++ .../20221220-102256/barrier-mgr-model-17.spn | 220 +++ .../20221220-102256/barrier-mgr-model-18.spn | 297 +++ .../20221220-102256/barrier-mgr-model-19.spn | 293 +++ .../20221220-102256/barrier-mgr-model-2.spn | 220 +++ .../20221220-102256/barrier-mgr-model-3.spn | 216 +++ .../20221220-102256/barrier-mgr-model-4.spn | 227 +++ .../20221220-102256/barrier-mgr-model-5.spn | 223 +++ .../20221220-102256/barrier-mgr-model-6.spn | 233 +++ .../20221220-102256/barrier-mgr-model-7.spn | 229 +++ .../20221220-102256/barrier-mgr-model-8.spn | 233 +++ .../20221220-102256/barrier-mgr-model-9.spn | 229 +++ .../barrier-mgr-model.pml1.trail | 355 ++++ .../barrier-mgr-model.pml10.trail | 384 ++++ .../barrier-mgr-model.pml11.trail | 393 ++++ .../barrier-mgr-model.pml12.trail | 390 ++++ .../barrier-mgr-model.pml13.trail | 406 +++++ .../barrier-mgr-model.pml14.trail | 403 +++++ .../barrier-mgr-model.pml15.trail | 349 ++++ .../barrier-mgr-model.pml16.trail | 346 ++++ .../barrier-mgr-model.pml17.trail | 385 ++++ .../barrier-mgr-model.pml18.trail | 382 ++++ .../barrier-mgr-model.pml19.trail | 705 ++++++++ .../barrier-mgr-model.pml2.trail | 352 ++++ .../barrier-mgr-model.pml20.trail | 702 +++++++ .../barrier-mgr-model.pml3.trail | 354 ++++ .../barrier-mgr-model.pml4.trail | 351 ++++ .../barrier-mgr-model.pml5.trail | 388 ++++ .../barrier-mgr-model.pml6.trail | 385 ++++ .../barrier-mgr-model.pml7.trail | 394 ++++ .../barrier-mgr-model.pml8.trail | 391 ++++ .../barrier-mgr-model.pml9.trail | 387 ++++ .../archive/20221220-102256/model-0-test.log | 1469 +++++++++++++++ .../20221220-102256/tr-barrier-mgr-model-0.c | 399 ++++ .../20221220-102256/tr-barrier-mgr-model-1.c | 372 ++++ .../20221220-102256/tr-barrier-mgr-model-10.c | 414 +++++ .../20221220-102256/tr-barrier-mgr-model-11.c | 387 ++++ .../20221220-102256/tr-barrier-mgr-model-12.c | 419 +++++ .../20221220-102256/tr-barrier-mgr-model-13.c | 392 ++++ .../20221220-102256/tr-barrier-mgr-model-14.c | 380 ++++ .../20221220-102256/tr-barrier-mgr-model-15.c | 353 ++++ .../20221220-102256/tr-barrier-mgr-model-16.c | 395 ++++ .../20221220-102256/tr-barrier-mgr-model-17.c | 368 ++++ .../20221220-102256/tr-barrier-mgr-model-18.c | 401 ++++ .../20221220-102256/tr-barrier-mgr-model-19.c | 374 ++++ .../20221220-102256/tr-barrier-mgr-model-2.c | 399 ++++ .../20221220-102256/tr-barrier-mgr-model-3.c | 372 ++++ .../20221220-102256/tr-barrier-mgr-model-4.c | 393 ++++ .../20221220-102256/tr-barrier-mgr-model-5.c | 366 ++++ .../20221220-102256/tr-barrier-mgr-model-6.c | 414 +++++ .../20221220-102256/tr-barrier-mgr-model-7.c | 387 ++++ .../20221220-102256/tr-barrier-mgr-model-8.c | 414 +++++ .../20221220-102256/tr-barrier-mgr-model-9.c | 387 ++++ .../models/barriers/barrier-mgr-model-post.h | 44 + .../models/barriers/barrier-mgr-model-pre.h | 51 + .../models/barriers/barrier-mgr-model-rfn.yml | 169 ++ .../models/barriers/barrier-mgr-model-run.h | 91 + .../models/barriers/barrier-mgr-model.pml | 1158 ++++++++++++ .../models/barriers/tc-barrier-mgr-model.c | 180 ++ .../models/barriers/tr-barrier-mgr-model.c | 249 +++ .../models/barriers/tr-barrier-mgr-model.h | 197 ++ formal/promela/models/chains/.gitignore | 1 + formal/promela/models/chains/STATUS.md | 11 + .../20221220-101911/chains-api-model-0.spn | 79 + .../20221220-101911/chains-api-model-1.spn | 81 + .../20221220-101911/chains-api-model-10.spn | 81 + .../20221220-101911/chains-api-model-11.spn | 81 + .../20221220-101911/chains-api-model-12.spn | 83 + .../20221220-101911/chains-api-model-13.spn | 81 + .../20221220-101911/chains-api-model-14.spn | 83 + .../20221220-101911/chains-api-model-15.spn | 81 + .../20221220-101911/chains-api-model-16.spn | 81 + .../20221220-101911/chains-api-model-17.spn | 81 + .../20221220-101911/chains-api-model-18.spn | 83 + .../20221220-101911/chains-api-model-19.spn | 81 + .../20221220-101911/chains-api-model-2.spn | 79 + .../20221220-101911/chains-api-model-20.spn | 83 + .../20221220-101911/chains-api-model-3.spn | 81 + .../20221220-101911/chains-api-model-4.spn | 81 + .../20221220-101911/chains-api-model-5.spn | 83 + .../20221220-101911/chains-api-model-6.spn | 81 + .../20221220-101911/chains-api-model-7.spn | 83 + .../20221220-101911/chains-api-model-8.spn | 81 + .../20221220-101911/chains-api-model-9.spn | 79 + .../chains-api-model.pml1.trail | 77 + .../chains-api-model.pml10.trail | 77 + .../chains-api-model.pml11.trail | 80 + .../chains-api-model.pml12.trail | 80 + .../chains-api-model.pml13.trail | 83 + .../chains-api-model.pml14.trail | 80 + .../chains-api-model.pml15.trail | 83 + .../chains-api-model.pml16.trail | 80 + .../chains-api-model.pml17.trail | 80 + .../chains-api-model.pml18.trail | 80 + .../chains-api-model.pml19.trail | 83 + .../chains-api-model.pml2.trail | 80 + .../chains-api-model.pml20.trail | 80 + .../chains-api-model.pml21.trail | 83 + .../chains-api-model.pml3.trail | 77 + .../chains-api-model.pml4.trail | 80 + .../chains-api-model.pml5.trail | 80 + .../chains-api-model.pml6.trail | 83 + .../chains-api-model.pml7.trail | 80 + .../chains-api-model.pml8.trail | 83 + .../chains-api-model.pml9.trail | 80 + .../archive/20221220-101911/model-0-test.log | 900 +++++++++ .../20221220-101911/tr-chains-api-model-0.c | 170 ++ .../20221220-101911/tr-chains-api-model-1.c | 172 ++ .../20221220-101911/tr-chains-api-model-10.c | 172 ++ .../20221220-101911/tr-chains-api-model-11.c | 172 ++ .../20221220-101911/tr-chains-api-model-12.c | 174 ++ .../20221220-101911/tr-chains-api-model-13.c | 172 ++ .../20221220-101911/tr-chains-api-model-14.c | 174 ++ .../20221220-101911/tr-chains-api-model-15.c | 172 ++ .../20221220-101911/tr-chains-api-model-16.c | 172 ++ .../20221220-101911/tr-chains-api-model-17.c | 172 ++ .../20221220-101911/tr-chains-api-model-18.c | 174 ++ .../20221220-101911/tr-chains-api-model-19.c | 172 ++ .../20221220-101911/tr-chains-api-model-2.c | 170 ++ .../20221220-101911/tr-chains-api-model-20.c | 174 ++ .../20221220-101911/tr-chains-api-model-3.c | 172 ++ .../20221220-101911/tr-chains-api-model-4.c | 172 ++ .../20221220-101911/tr-chains-api-model-5.c | 174 ++ .../20221220-101911/tr-chains-api-model-6.c | 172 ++ .../20221220-101911/tr-chains-api-model-7.c | 174 ++ .../20221220-101911/tr-chains-api-model-8.c | 172 ++ .../20221220-101911/tr-chains-api-model-9.c | 170 ++ .../models/chains/chains-api-model-post.h | 3 + .../models/chains/chains-api-model-pre.h | 43 + .../models/chains/chains-api-model-rfn.yml | 64 + .../models/chains/chains-api-model-run.h | 18 + .../models/chains/chains-api-model.pml | 203 +++ .../models/chains/tr-chains-api-model.c | 70 + .../models/chains/tr-chains-api-model.h | 57 + formal/promela/models/events/.gitignore | 1 + formal/promela/models/events/STATUS.md | 21 + .../20221220-102131/event-mgr-model-0.spn | 157 ++ .../20221220-102131/event-mgr-model-1.spn | 163 ++ .../20221220-102131/event-mgr-model-10.spn | 171 ++ .../20221220-102131/event-mgr-model-2.spn | 179 ++ .../20221220-102131/event-mgr-model-3.spn | 161 ++ .../20221220-102131/event-mgr-model-4.spn | 169 ++ .../20221220-102131/event-mgr-model-5.spn | 169 ++ .../20221220-102131/event-mgr-model-6.spn | 167 ++ .../20221220-102131/event-mgr-model-7.spn | 169 ++ .../20221220-102131/event-mgr-model-8.spn | 206 +++ .../20221220-102131/event-mgr-model-9.spn | 184 ++ .../event-mgr-model.pml1.trail | 186 ++ .../event-mgr-model.pml10.trail | 244 +++ .../event-mgr-model.pml11.trail | 214 +++ .../event-mgr-model.pml2.trail | 198 ++ .../event-mgr-model.pml3.trail | 268 +++ .../event-mgr-model.pml4.trail | 192 ++ .../event-mgr-model.pml5.trail | 211 +++ .../event-mgr-model.pml6.trail | 211 +++ .../event-mgr-model.pml7.trail | 204 +++ .../event-mgr-model.pml8.trail | 213 +++ .../event-mgr-model.pml9.trail | 334 ++++ .../archive/20221220-102131/model-0-test.log | 843 +++++++++ .../20221220-102131/tr-event-mgr-model-0.c | 347 ++++ .../20221220-102131/tr-event-mgr-model-1.c | 345 ++++ .../20221220-102131/tr-event-mgr-model-10.c | 378 ++++ .../20221220-102131/tr-event-mgr-model-2.c | 358 ++++ .../20221220-102131/tr-event-mgr-model-3.c | 343 ++++ .../20221220-102131/tr-event-mgr-model-4.c | 364 ++++ .../20221220-102131/tr-event-mgr-model-5.c | 364 ++++ .../20221220-102131/tr-event-mgr-model-6.c | 364 ++++ .../20221220-102131/tr-event-mgr-model-7.c | 364 ++++ .../20221220-102131/tr-event-mgr-model-8.c | 386 ++++ .../20221220-102131/tr-event-mgr-model-9.c | 391 ++++ .../models/events/event-mgr-model-post.h | 8 + .../models/events/event-mgr-model-pre.h | 51 + .../models/events/event-mgr-model-rfn.yml | 182 ++ .../models/events/event-mgr-model-run.h | 164 ++ .../promela/models/events/event-mgr-model.pml | 848 +++++++++ .../models/events/tc-event-mgr-model.c | 358 ++++ .../models/events/tr-event-mgr-model.c | 257 +++ .../models/events/tr-event-mgr-model.h | 245 +++ formal/promela/models/messages/README.md | 10 + formal/promela/models/messages/STATUS.md | 14 + .../archive/20221220-110211/model-0-test.log | 1274 +++++++++++++ .../20221220-110211/msg-mgr-model-0.spn | 295 +++ .../20221220-110211/msg-mgr-model-1.spn | 296 +++ .../20221220-110211/msg-mgr-model-10.spn | 297 +++ .../20221220-110211/msg-mgr-model-11.spn | 297 +++ .../20221220-110211/msg-mgr-model-12.spn | 301 +++ .../20221220-110211/msg-mgr-model-13.spn | 305 ++++ .../20221220-110211/msg-mgr-model-14.spn | 309 ++++ .../20221220-110211/msg-mgr-model-15.spn | 313 ++++ .../20221220-110211/msg-mgr-model-16.spn | 317 ++++ .../20221220-110211/msg-mgr-model-17.spn | 321 ++++ .../20221220-110211/msg-mgr-model-18.spn | 325 ++++ .../20221220-110211/msg-mgr-model-19.spn | 329 ++++ .../20221220-110211/msg-mgr-model-2.spn | 295 +++ .../20221220-110211/msg-mgr-model-20.spn | 314 ++++ .../20221220-110211/msg-mgr-model-21.spn | 334 ++++ .../20221220-110211/msg-mgr-model-22.spn | 333 ++++ .../20221220-110211/msg-mgr-model-3.spn | 295 +++ .../20221220-110211/msg-mgr-model-4.spn | 307 ++++ .../20221220-110211/msg-mgr-model-5.spn | 293 +++ .../20221220-110211/msg-mgr-model-6.spn | 294 +++ .../20221220-110211/msg-mgr-model-7.spn | 314 ++++ .../20221220-110211/msg-mgr-model-8.spn | 305 ++++ .../20221220-110211/msg-mgr-model-9.spn | 303 ++++ .../20221220-110211/msg-mgr-model.pml1.trail | 482 +++++ .../20221220-110211/msg-mgr-model.pml10.trail | 507 ++++++ .../20221220-110211/msg-mgr-model.pml11.trail | 509 ++++++ .../20221220-110211/msg-mgr-model.pml12.trail | 512 ++++++ .../20221220-110211/msg-mgr-model.pml13.trail | 533 ++++++ .../20221220-110211/msg-mgr-model.pml14.trail | 554 ++++++ .../20221220-110211/msg-mgr-model.pml15.trail | 575 ++++++ .../20221220-110211/msg-mgr-model.pml16.trail | 596 ++++++ .../20221220-110211/msg-mgr-model.pml17.trail | 617 +++++++ .../20221220-110211/msg-mgr-model.pml18.trail | 638 +++++++ .../20221220-110211/msg-mgr-model.pml19.trail | 659 +++++++ .../20221220-110211/msg-mgr-model.pml2.trail | 489 +++++ .../20221220-110211/msg-mgr-model.pml20.trail | 680 +++++++ .../20221220-110211/msg-mgr-model.pml21.trail | 612 +++++++ .../20221220-110211/msg-mgr-model.pml22.trail | 702 +++++++ .../20221220-110211/msg-mgr-model.pml23.trail | 698 +++++++ .../20221220-110211/msg-mgr-model.pml3.trail | 483 +++++ .../20221220-110211/msg-mgr-model.pml4.trail | 483 +++++ .../20221220-110211/msg-mgr-model.pml5.trail | 525 ++++++ .../20221220-110211/msg-mgr-model.pml6.trail | 481 +++++ .../20221220-110211/msg-mgr-model.pml7.trail | 487 +++++ .../20221220-110211/msg-mgr-model.pml8.trail | 588 ++++++ .../20221220-110211/msg-mgr-model.pml9.trail | 520 ++++++ .../20221220-110211/tr-msg-mgr-model-0.c | 398 ++++ .../20221220-110211/tr-msg-mgr-model-1.c | 398 ++++ .../20221220-110211/tr-msg-mgr-model-10.c | 408 +++++ .../20221220-110211/tr-msg-mgr-model-11.c | 408 +++++ .../20221220-110211/tr-msg-mgr-model-12.c | 408 +++++ .../20221220-110211/tr-msg-mgr-model-13.c | 408 +++++ .../20221220-110211/tr-msg-mgr-model-14.c | 408 +++++ .../20221220-110211/tr-msg-mgr-model-15.c | 408 +++++ .../20221220-110211/tr-msg-mgr-model-16.c | 408 +++++ .../20221220-110211/tr-msg-mgr-model-17.c | 408 +++++ .../20221220-110211/tr-msg-mgr-model-18.c | 408 +++++ .../20221220-110211/tr-msg-mgr-model-19.c | 408 +++++ .../20221220-110211/tr-msg-mgr-model-2.c | 398 ++++ .../20221220-110211/tr-msg-mgr-model-20.c | 416 +++++ .../20221220-110211/tr-msg-mgr-model-21.c | 416 +++++ .../20221220-110211/tr-msg-mgr-model-22.c | 413 +++++ .../20221220-110211/tr-msg-mgr-model-3.c | 398 ++++ .../20221220-110211/tr-msg-mgr-model-4.c | 458 +++++ .../20221220-110211/tr-msg-mgr-model-5.c | 391 ++++ .../20221220-110211/tr-msg-mgr-model-6.c | 391 ++++ .../20221220-110211/tr-msg-mgr-model-7.c | 404 +++++ .../20221220-110211/tr-msg-mgr-model-8.c | 441 +++++ .../20221220-110211/tr-msg-mgr-model-9.c | 426 +++++ .../models/messages/msg-mgr-model-post.h | 8 + .../models/messages/msg-mgr-model-pre.h | 51 + .../models/messages/msg-mgr-model-rfn.yml | 202 +++ .../models/messages/msg-mgr-model-run.h | 191 ++ .../promela/models/messages/msg-mgr-model.pml | 842 +++++++++ .../models/messages/tc-msg-mgr-model.c | 211 +++ .../models/messages/tr-msg-mgr-model.c | 240 +++ .../models/messages/tr-msg-mgr-model.h | 132 ++ .../models/threadq/MrsP-Code/Chains.pml | 168 ++ .../models/threadq/MrsP-Code/Concurrency.pml | 182 ++ .../models/threadq/MrsP-Code/Heaps.pml | 103 ++ .../promela/models/threadq/MrsP-Code/Init.pml | 485 +++++ .../models/threadq/MrsP-Code/Locks.pml | 67 + .../promela/models/threadq/MrsP-Code/MAIN.pml | 74 + .../models/threadq/MrsP-Code/Priority.pml | 135 ++ .../models/threadq/MrsP-Code/RBTrees.pml | 111 ++ .../models/threadq/MrsP-Code/Scenarios.pml | 103 ++ .../models/threadq/MrsP-Code/Semaphores.pml | 360 ++++ .../models/threadq/MrsP-Code/Sizing.pml | 98 + .../models/threadq/MrsP-Code/State.pml | 137 ++ .../models/threadq/MrsP-Code/Structs.pml | 1012 +++++++++++ .../models/threadq/MrsP-Code/Values.pml | 94 + .../models/threadq/MrsP-Tests/Configure.pml | 549 ++++++ .../promela/models/threadq/MrsP-Tests/Run.pml | 440 +++++ .../models/threadq/MrsP-Tests/Sizing.pml | 161 ++ .../models/threadq/MrsP-Tests/Utilities.pml | 67 + .../MrsP-Tests/mrsp-threadq-model-post.h | 3 + .../MrsP-Tests/mrsp-threadq-model-pre.h | 43 + .../MrsP-Tests/mrsp-threadq-model-rfn.yml | 64 + .../MrsP-Tests/mrsp-threadq-model-run.h | 18 + .../threadq/MrsP-Tests/mrsp-threadq-model.pml | 79 + .../MrsP-Tests/tc-mrsp-threadq-model.c | 600 ++++++ .../MrsP-Tests/tr-mrsp-threadq-model.c | 70 + .../MrsP-Tests/tr-mrsp-threadq-model.h | 57 + .../models/threadq/Weak-Memory/RAM.pml | 48 + .../models/threadq/Weak-Memory/SPARC-TSO.pml | 198 ++ .../threadq/Weak-Memory/memory_model.pml | 60 + .../models/threadq/Weak-Memory/wmemory.pml | 74 + formal/promela/src/Makefile | 55 + formal/promela/src/README.md | 71 + formal/promela/src/examples/draft/make.sh | 77 + formal/promela/src/examples/draft/parse.pml | 129 ++ .../src/examples/model_checker/spin.pml | 8 + formal/promela/src/examples/requirements.txt | 35 + formal/promela/src/gentest.py | 46 + formal/promela/src/metrics.py | 11 + formal/promela/src/requirements.txt | 35 + formal/promela/src/spin2test.coco | 41 + formal/promela/src/src.sh | 13 + formal/promela/src/src/__init__.py | 0 formal/promela/src/src/library.coco | 94 + formal/promela/src/src/library.py | 759 ++++++++ .../src/src/modules/comment-filter/AUTHORS | 7 + .../src/src/modules/comment-filter/LICENSE | 15 + .../src/src/modules/comment-filter/README.md | 158 ++ .../comment-filter/comment_filter/__init__.py | 1 + .../comment-filter/comment_filter/language.py | 60 + .../comment-filter/comment_filter/rfc.py | 425 +++++ .../src/src/modules/comment-filter/setup.cfg | 5 + .../src/src/modules/comment-filter/setup.py | 12 + .../src/src/modules/comment-filter/tox.ini | 12 + .../src/src/modules/promela_yacc/LICENSE | 32 + .../src/src/modules/promela_yacc/README.md | 27 + .../modules/promela_yacc/promela/__init__.py | 6 + .../src/modules/promela_yacc/promela/ast.py | 1075 +++++++++++ .../src/modules/promela_yacc/promela/lex.py | 219 +++ .../src/modules/promela_yacc/promela/yacc.py | 1016 +++++++++++ .../src/src/modules/promela_yacc/setup.py | 65 + formal/promela/src/src/refine_command.coco | 487 +++++ formal/promela/src/src/refine_command.py | 1607 +++++++++++++++++ formal/promela/src/src/spin2test.coco | 104 ++ formal/promela/src/src/spin2test.py | 767 ++++++++ formal/promela/src/src/syntax_ml.coco | 211 +++ formal/promela/src/src/syntax_ml.py | 915 ++++++++++ formal/promela/src/src/syntax_pml.coco | 396 ++++ formal/promela/src/src/syntax_pml.py | 1257 +++++++++++++ formal/promela/src/src/syntax_yaml.coco | 182 ++ formal/promela/src/src/syntax_yaml.py | 940 ++++++++++ formal/promela/src/src/testgen.coco | 624 +++++++ formal/promela/src/src/testgen.py | 1368 ++++++++++++++ formal/promela/src/src/tests/__init__.py | 0 formal/promela/src/src/tests/library.coco | 154 ++ formal/promela/src/src/tests/library.py | 796 ++++++++ .../src/tests/test_coverage_spin2test.coco | 144 ++ .../src/src/tests/test_coverage_spin2test.py | 773 ++++++++ .../src/src/tests/test_coverage_testgen.coco | 394 ++++ .../src/src/tests/test_coverage_testgen.py | 958 ++++++++++ .../promela/src/src/tests/test_optional.coco | 46 + formal/promela/src/src/tests/test_optional.py | 705 ++++++++ formal/promela/src/testbuilder-template.yml | 42 + formal/promela/src/testbuilder.help | 23 + formal/promela/src/testbuilder.py | 317 ++++ formal/promela/src/testgen_ml.coco | 48 + formal/promela/src/testgen_ml.py | 707 ++++++++ formal/promela/src/testgen_ml.sh | 19 + formal/promela/src/testgen_ml_spin.sh | 19 + formal/promela/src/testgen_yaml.coco | 48 + formal/promela/src/testgen_yaml.py | 707 ++++++++ formal/promela/src/testgen_yaml.sh | 19 + formal/promela/src/testgen_yaml_spin.sh | 19 + 365 files changed, 101772 insertions(+) create mode 100644 formal/.gitignore create mode 100644 formal/README.md create mode 100644 formal/promela/.gitignore create mode 100644 formal/promela/README.md create mode 100644 formal/promela/models/README.md create mode 100644 formal/promela/models/barriers/README.md create mode 100644 formal/promela/models/barriers/STATUS.md create mode 100644 formal/promela/models/barriers/archive/20221220-102256/barrier-mgr-model-0.spn create mode 100644 formal/promela/models/barriers/archive/20221220-102256/barrier-mgr-model-1.spn create mode 100644 formal/promela/models/barriers/archive/20221220-102256/barrier-mgr-model-10.spn create mode 100644 formal/promela/models/barriers/archive/20221220-102256/barrier-mgr-model-11.spn create mode 100644 formal/promela/models/barriers/archive/20221220-102256/barrier-mgr-model-12.spn create mode 100644 formal/promela/models/barriers/archive/20221220-102256/barrier-mgr-model-13.spn create mode 100644 formal/promela/models/barriers/archive/20221220-102256/barrier-mgr-model-14.spn create mode 100644 formal/promela/models/barriers/archive/20221220-102256/barrier-mgr-model-15.spn create mode 100644 formal/promela/models/barriers/archive/20221220-102256/barrier-mgr-model-16.spn create mode 100644 formal/promela/models/barriers/archive/20221220-102256/barrier-mgr-model-17.spn create mode 100644 formal/promela/models/barriers/archive/20221220-102256/barrier-mgr-model-18.spn create mode 100644 formal/promela/models/barriers/archive/20221220-102256/barrier-mgr-model-19.spn create mode 100644 formal/promela/models/barriers/archive/20221220-102256/barrier-mgr-model-2.spn create mode 100644 formal/promela/models/barriers/archive/20221220-102256/barrier-mgr-model-3.spn create mode 100644 formal/promela/models/barriers/archive/20221220-102256/barrier-mgr-model-4.spn create mode 100644 formal/promela/models/barriers/archive/20221220-102256/barrier-mgr-model-5.spn create mode 100644 formal/promela/models/barriers/archive/20221220-102256/barrier-mgr-model-6.spn create mode 100644 formal/promela/models/barriers/archive/20221220-102256/barrier-mgr-model-7.spn create mode 100644 formal/promela/models/barriers/archive/20221220-102256/barrier-mgr-model-8.spn create mode 100644 formal/promela/models/barriers/archive/20221220-102256/barrier-mgr-model-9.spn create mode 100644 formal/promela/models/barriers/archive/20221220-102256/barrier-mgr-model.pml1.trail create mode 100644 formal/promela/models/barriers/archive/20221220-102256/barrier-mgr-model.pml10.trail create mode 100644 formal/promela/models/barriers/archive/20221220-102256/barrier-mgr-model.pml11.trail create mode 100644 formal/promela/models/barriers/archive/20221220-102256/barrier-mgr-model.pml12.trail create mode 100644 formal/promela/models/barriers/archive/20221220-102256/barrier-mgr-model.pml13.trail create mode 100644 formal/promela/models/barriers/archive/20221220-102256/barrier-mgr-model.pml14.trail create mode 100644 formal/promela/models/barriers/archive/20221220-102256/barrier-mgr-model.pml15.trail create mode 100644 formal/promela/models/barriers/archive/20221220-102256/barrier-mgr-model.pml16.trail create mode 100644 formal/promela/models/barriers/archive/20221220-102256/barrier-mgr-model.pml17.trail create mode 100644 formal/promela/models/barriers/archive/20221220-102256/barrier-mgr-model.pml18.trail create mode 100644 formal/promela/models/barriers/archive/20221220-102256/barrier-mgr-model.pml19.trail create mode 100644 formal/promela/models/barriers/archive/20221220-102256/barrier-mgr-model.pml2.trail create mode 100644 formal/promela/models/barriers/archive/20221220-102256/barrier-mgr-model.pml20.trail create mode 100644 formal/promela/models/barriers/archive/20221220-102256/barrier-mgr-model.pml3.trail create mode 100644 formal/promela/models/barriers/archive/20221220-102256/barrier-mgr-model.pml4.trail create mode 100644 formal/promela/models/barriers/archive/20221220-102256/barrier-mgr-model.pml5.trail create mode 100644 formal/promela/models/barriers/archive/20221220-102256/barrier-mgr-model.pml6.trail create mode 100644 formal/promela/models/barriers/archive/20221220-102256/barrier-mgr-model.pml7.trail create mode 100644 formal/promela/models/barriers/archive/20221220-102256/barrier-mgr-model.pml8.trail create mode 100644 formal/promela/models/barriers/archive/20221220-102256/barrier-mgr-model.pml9.trail create mode 100644 formal/promela/models/barriers/archive/20221220-102256/model-0-test.log create mode 100644 formal/promela/models/barriers/archive/20221220-102256/tr-barrier-mgr-model-0.c create mode 100644 formal/promela/models/barriers/archive/20221220-102256/tr-barrier-mgr-model-1.c create mode 100644 formal/promela/models/barriers/archive/20221220-102256/tr-barrier-mgr-model-10.c create mode 100644 formal/promela/models/barriers/archive/20221220-102256/tr-barrier-mgr-model-11.c create mode 100644 formal/promela/models/barriers/archive/20221220-102256/tr-barrier-mgr-model-12.c create mode 100644 formal/promela/models/barriers/archive/20221220-102256/tr-barrier-mgr-model-13.c create mode 100644 formal/promela/models/barriers/archive/20221220-102256/tr-barrier-mgr-model-14.c create mode 100644 formal/promela/models/barriers/archive/20221220-102256/tr-barrier-mgr-model-15.c create mode 100644 formal/promela/models/barriers/archive/20221220-102256/tr-barrier-mgr-model-16.c create mode 100644 formal/promela/models/barriers/archive/20221220-102256/tr-barrier-mgr-model-17.c create mode 100644 formal/promela/models/barriers/archive/20221220-102256/tr-barrier-mgr-model-18.c create mode 100644 formal/promela/models/barriers/archive/20221220-102256/tr-barrier-mgr-model-19.c create mode 100644 formal/promela/models/barriers/archive/20221220-102256/tr-barrier-mgr-model-2.c create mode 100644 formal/promela/models/barriers/archive/20221220-102256/tr-barrier-mgr-model-3.c create mode 100644 formal/promela/models/barriers/archive/20221220-102256/tr-barrier-mgr-model-4.c create mode 100644 formal/promela/models/barriers/archive/20221220-102256/tr-barrier-mgr-model-5.c create mode 100644 formal/promela/models/barriers/archive/20221220-102256/tr-barrier-mgr-model-6.c create mode 100644 formal/promela/models/barriers/archive/20221220-102256/tr-barrier-mgr-model-7.c create mode 100644 formal/promela/models/barriers/archive/20221220-102256/tr-barrier-mgr-model-8.c create mode 100644 formal/promela/models/barriers/archive/20221220-102256/tr-barrier-mgr-model-9.c create mode 100644 formal/promela/models/barriers/barrier-mgr-model-post.h create mode 100644 formal/promela/models/barriers/barrier-mgr-model-pre.h create mode 100644 formal/promela/models/barriers/barrier-mgr-model-rfn.yml create mode 100644 formal/promela/models/barriers/barrier-mgr-model-run.h create mode 100644 formal/promela/models/barriers/barrier-mgr-model.pml create mode 100644 formal/promela/models/barriers/tc-barrier-mgr-model.c create mode 100644 formal/promela/models/barriers/tr-barrier-mgr-model.c create mode 100644 formal/promela/models/barriers/tr-barrier-mgr-model.h create mode 100644 formal/promela/models/chains/.gitignore create mode 100644 formal/promela/models/chains/STATUS.md create mode 100644 formal/promela/models/chains/archive/20221220-101911/chains-api-model-0.spn create mode 100644 formal/promela/models/chains/archive/20221220-101911/chains-api-model-1.spn create mode 100644 formal/promela/models/chains/archive/20221220-101911/chains-api-model-10.spn create mode 100644 formal/promela/models/chains/archive/20221220-101911/chains-api-model-11.spn create mode 100644 formal/promela/models/chains/archive/20221220-101911/chains-api-model-12.spn create mode 100644 formal/promela/models/chains/archive/20221220-101911/chains-api-model-13.spn create mode 100644 formal/promela/models/chains/archive/20221220-101911/chains-api-model-14.spn create mode 100644 formal/promela/models/chains/archive/20221220-101911/chains-api-model-15.spn create mode 100644 formal/promela/models/chains/archive/20221220-101911/chains-api-model-16.spn create mode 100644 formal/promela/models/chains/archive/20221220-101911/chains-api-model-17.spn create mode 100644 formal/promela/models/chains/archive/20221220-101911/chains-api-model-18.spn create mode 100644 formal/promela/models/chains/archive/20221220-101911/chains-api-model-19.spn create mode 100644 formal/promela/models/chains/archive/20221220-101911/chains-api-model-2.spn create mode 100644 formal/promela/models/chains/archive/20221220-101911/chains-api-model-20.spn create mode 100644 formal/promela/models/chains/archive/20221220-101911/chains-api-model-3.spn create mode 100644 formal/promela/models/chains/archive/20221220-101911/chains-api-model-4.spn create mode 100644 formal/promela/models/chains/archive/20221220-101911/chains-api-model-5.spn create mode 100644 formal/promela/models/chains/archive/20221220-101911/chains-api-model-6.spn create mode 100644 formal/promela/models/chains/archive/20221220-101911/chains-api-model-7.spn create mode 100644 formal/promela/models/chains/archive/20221220-101911/chains-api-model-8.spn create mode 100644 formal/promela/models/chains/archive/20221220-101911/chains-api-model-9.spn create mode 100644 formal/promela/models/chains/archive/20221220-101911/chains-api-model.pml1.trail create mode 100644 formal/promela/models/chains/archive/20221220-101911/chains-api-model.pml10.trail create mode 100644 formal/promela/models/chains/archive/20221220-101911/chains-api-model.pml11.trail create mode 100644 formal/promela/models/chains/archive/20221220-101911/chains-api-model.pml12.trail create mode 100644 formal/promela/models/chains/archive/20221220-101911/chains-api-model.pml13.trail create mode 100644 formal/promela/models/chains/archive/20221220-101911/chains-api-model.pml14.trail create mode 100644 formal/promela/models/chains/archive/20221220-101911/chains-api-model.pml15.trail create mode 100644 formal/promela/models/chains/archive/20221220-101911/chains-api-model.pml16.trail create mode 100644 formal/promela/models/chains/archive/20221220-101911/chains-api-model.pml17.trail create mode 100644 formal/promela/models/chains/archive/20221220-101911/chains-api-model.pml18.trail create mode 100644 formal/promela/models/chains/archive/20221220-101911/chains-api-model.pml19.trail create mode 100644 formal/promela/models/chains/archive/20221220-101911/chains-api-model.pml2.trail create mode 100644 formal/promela/models/chains/archive/20221220-101911/chains-api-model.pml20.trail create mode 100644 formal/promela/models/chains/archive/20221220-101911/chains-api-model.pml21.trail create mode 100644 formal/promela/models/chains/archive/20221220-101911/chains-api-model.pml3.trail create mode 100644 formal/promela/models/chains/archive/20221220-101911/chains-api-model.pml4.trail create mode 100644 formal/promela/models/chains/archive/20221220-101911/chains-api-model.pml5.trail create mode 100644 formal/promela/models/chains/archive/20221220-101911/chains-api-model.pml6.trail create mode 100644 formal/promela/models/chains/archive/20221220-101911/chains-api-model.pml7.trail create mode 100644 formal/promela/models/chains/archive/20221220-101911/chains-api-model.pml8.trail create mode 100644 formal/promela/models/chains/archive/20221220-101911/chains-api-model.pml9.trail create mode 100644 formal/promela/models/chains/archive/20221220-101911/model-0-test.log create mode 100644 formal/promela/models/chains/archive/20221220-101911/tr-chains-api-model-0.c create mode 100644 formal/promela/models/chains/archive/20221220-101911/tr-chains-api-model-1.c create mode 100644 formal/promela/models/chains/archive/20221220-101911/tr-chains-api-model-10.c create mode 100644 formal/promela/models/chains/archive/20221220-101911/tr-chains-api-model-11.c create mode 100644 formal/promela/models/chains/archive/20221220-101911/tr-chains-api-model-12.c create mode 100644 formal/promela/models/chains/archive/20221220-101911/tr-chains-api-model-13.c create mode 100644 formal/promela/models/chains/archive/20221220-101911/tr-chains-api-model-14.c create mode 100644 formal/promela/models/chains/archive/20221220-101911/tr-chains-api-model-15.c create mode 100644 formal/promela/models/chains/archive/20221220-101911/tr-chains-api-model-16.c create mode 100644 formal/promela/models/chains/archive/20221220-101911/tr-chains-api-model-17.c create mode 100644 formal/promela/models/chains/archive/20221220-101911/tr-chains-api-model-18.c create mode 100644 formal/promela/models/chains/archive/20221220-101911/tr-chains-api-model-19.c create mode 100644 formal/promela/models/chains/archive/20221220-101911/tr-chains-api-model-2.c create mode 100644 formal/promela/models/chains/archive/20221220-101911/tr-chains-api-model-20.c create mode 100644 formal/promela/models/chains/archive/20221220-101911/tr-chains-api-model-3.c create mode 100644 formal/promela/models/chains/archive/20221220-101911/tr-chains-api-model-4.c create mode 100644 formal/promela/models/chains/archive/20221220-101911/tr-chains-api-model-5.c create mode 100644 formal/promela/models/chains/archive/20221220-101911/tr-chains-api-model-6.c create mode 100644 formal/promela/models/chains/archive/20221220-101911/tr-chains-api-model-7.c create mode 100644 formal/promela/models/chains/archive/20221220-101911/tr-chains-api-model-8.c create mode 100644 formal/promela/models/chains/archive/20221220-101911/tr-chains-api-model-9.c create mode 100644 formal/promela/models/chains/chains-api-model-post.h create mode 100644 formal/promela/models/chains/chains-api-model-pre.h create mode 100644 formal/promela/models/chains/chains-api-model-rfn.yml create mode 100644 formal/promela/models/chains/chains-api-model-run.h create mode 100644 formal/promela/models/chains/chains-api-model.pml create mode 100644 formal/promela/models/chains/tr-chains-api-model.c create mode 100644 formal/promela/models/chains/tr-chains-api-model.h create mode 100644 formal/promela/models/events/.gitignore create mode 100644 formal/promela/models/events/STATUS.md create mode 100644 formal/promela/models/events/archive/20221220-102131/event-mgr-model-0.spn create mode 100644 formal/promela/models/events/archive/20221220-102131/event-mgr-model-1.spn create mode 100644 formal/promela/models/events/archive/20221220-102131/event-mgr-model-10.spn create mode 100644 formal/promela/models/events/archive/20221220-102131/event-mgr-model-2.spn create mode 100644 formal/promela/models/events/archive/20221220-102131/event-mgr-model-3.spn create mode 100644 formal/promela/models/events/archive/20221220-102131/event-mgr-model-4.spn create mode 100644 formal/promela/models/events/archive/20221220-102131/event-mgr-model-5.spn create mode 100644 formal/promela/models/events/archive/20221220-102131/event-mgr-model-6.spn create mode 100644 formal/promela/models/events/archive/20221220-102131/event-mgr-model-7.spn create mode 100644 formal/promela/models/events/archive/20221220-102131/event-mgr-model-8.spn create mode 100644 formal/promela/models/events/archive/20221220-102131/event-mgr-model-9.spn create mode 100644 formal/promela/models/events/archive/20221220-102131/event-mgr-model.pml1.trail create mode 100644 formal/promela/models/events/archive/20221220-102131/event-mgr-model.pml10.trail create mode 100644 formal/promela/models/events/archive/20221220-102131/event-mgr-model.pml11.trail create mode 100644 formal/promela/models/events/archive/20221220-102131/event-mgr-model.pml2.trail create mode 100644 formal/promela/models/events/archive/20221220-102131/event-mgr-model.pml3.trail create mode 100644 formal/promela/models/events/archive/20221220-102131/event-mgr-model.pml4.trail create mode 100644 formal/promela/models/events/archive/20221220-102131/event-mgr-model.pml5.trail create mode 100644 formal/promela/models/events/archive/20221220-102131/event-mgr-model.pml6.trail create mode 100644 formal/promela/models/events/archive/20221220-102131/event-mgr-model.pml7.trail create mode 100644 formal/promela/models/events/archive/20221220-102131/event-mgr-model.pml8.trail create mode 100644 formal/promela/models/events/archive/20221220-102131/event-mgr-model.pml9.trail create mode 100644 formal/promela/models/events/archive/20221220-102131/model-0-test.log create mode 100644 formal/promela/models/events/archive/20221220-102131/tr-event-mgr-model-0.c create mode 100644 formal/promela/models/events/archive/20221220-102131/tr-event-mgr-model-1.c create mode 100644 formal/promela/models/events/archive/20221220-102131/tr-event-mgr-model-10.c create mode 100644 formal/promela/models/events/archive/20221220-102131/tr-event-mgr-model-2.c create mode 100644 formal/promela/models/events/archive/20221220-102131/tr-event-mgr-model-3.c create mode 100644 formal/promela/models/events/archive/20221220-102131/tr-event-mgr-model-4.c create mode 100644 formal/promela/models/events/archive/20221220-102131/tr-event-mgr-model-5.c create mode 100644 formal/promela/models/events/archive/20221220-102131/tr-event-mgr-model-6.c create mode 100644 formal/promela/models/events/archive/20221220-102131/tr-event-mgr-model-7.c create mode 100644 formal/promela/models/events/archive/20221220-102131/tr-event-mgr-model-8.c create mode 100644 formal/promela/models/events/archive/20221220-102131/tr-event-mgr-model-9.c create mode 100644 formal/promela/models/events/event-mgr-model-post.h create mode 100644 formal/promela/models/events/event-mgr-model-pre.h create mode 100644 formal/promela/models/events/event-mgr-model-rfn.yml create mode 100644 formal/promela/models/events/event-mgr-model-run.h create mode 100644 formal/promela/models/events/event-mgr-model.pml create mode 100644 formal/promela/models/events/tc-event-mgr-model.c create mode 100644 formal/promela/models/events/tr-event-mgr-model.c create mode 100644 formal/promela/models/events/tr-event-mgr-model.h create mode 100644 formal/promela/models/messages/README.md create mode 100644 formal/promela/models/messages/STATUS.md create mode 100644 formal/promela/models/messages/archive/20221220-110211/model-0-test.log create mode 100644 formal/promela/models/messages/archive/20221220-110211/msg-mgr-model-0.spn create mode 100644 formal/promela/models/messages/archive/20221220-110211/msg-mgr-model-1.spn create mode 100644 formal/promela/models/messages/archive/20221220-110211/msg-mgr-model-10.spn create mode 100644 formal/promela/models/messages/archive/20221220-110211/msg-mgr-model-11.spn create mode 100644 formal/promela/models/messages/archive/20221220-110211/msg-mgr-model-12.spn create mode 100644 formal/promela/models/messages/archive/20221220-110211/msg-mgr-model-13.spn create mode 100644 formal/promela/models/messages/archive/20221220-110211/msg-mgr-model-14.spn create mode 100644 formal/promela/models/messages/archive/20221220-110211/msg-mgr-model-15.spn create mode 100644 formal/promela/models/messages/archive/20221220-110211/msg-mgr-model-16.spn create mode 100644 formal/promela/models/messages/archive/20221220-110211/msg-mgr-model-17.spn create mode 100644 formal/promela/models/messages/archive/20221220-110211/msg-mgr-model-18.spn create mode 100644 formal/promela/models/messages/archive/20221220-110211/msg-mgr-model-19.spn create mode 100644 formal/promela/models/messages/archive/20221220-110211/msg-mgr-model-2.spn create mode 100644 formal/promela/models/messages/archive/20221220-110211/msg-mgr-model-20.spn create mode 100644 formal/promela/models/messages/archive/20221220-110211/msg-mgr-model-21.spn create mode 100644 formal/promela/models/messages/archive/20221220-110211/msg-mgr-model-22.spn create mode 100644 formal/promela/models/messages/archive/20221220-110211/msg-mgr-model-3.spn create mode 100644 formal/promela/models/messages/archive/20221220-110211/msg-mgr-model-4.spn create mode 100644 formal/promela/models/messages/archive/20221220-110211/msg-mgr-model-5.spn create mode 100644 formal/promela/models/messages/archive/20221220-110211/msg-mgr-model-6.spn create mode 100644 formal/promela/models/messages/archive/20221220-110211/msg-mgr-model-7.spn create mode 100644 formal/promela/models/messages/archive/20221220-110211/msg-mgr-model-8.spn create mode 100644 formal/promela/models/messages/archive/20221220-110211/msg-mgr-model-9.spn create mode 100644 formal/promela/models/messages/archive/20221220-110211/msg-mgr-model.pml1.trail create mode 100644 formal/promela/models/messages/archive/20221220-110211/msg-mgr-model.pml10.trail create mode 100644 formal/promela/models/messages/archive/20221220-110211/msg-mgr-model.pml11.trail create mode 100644 formal/promela/models/messages/archive/20221220-110211/msg-mgr-model.pml12.trail create mode 100644 formal/promela/models/messages/archive/20221220-110211/msg-mgr-model.pml13.trail create mode 100644 formal/promela/models/messages/archive/20221220-110211/msg-mgr-model.pml14.trail create mode 100644 formal/promela/models/messages/archive/20221220-110211/msg-mgr-model.pml15.trail create mode 100644 formal/promela/models/messages/archive/20221220-110211/msg-mgr-model.pml16.trail create mode 100644 formal/promela/models/messages/archive/20221220-110211/msg-mgr-model.pml17.trail create mode 100644 formal/promela/models/messages/archive/20221220-110211/msg-mgr-model.pml18.trail create mode 100644 formal/promela/models/messages/archive/20221220-110211/msg-mgr-model.pml19.trail create mode 100644 formal/promela/models/messages/archive/20221220-110211/msg-mgr-model.pml2.trail create mode 100644 formal/promela/models/messages/archive/20221220-110211/msg-mgr-model.pml20.trail create mode 100644 formal/promela/models/messages/archive/20221220-110211/msg-mgr-model.pml21.trail create mode 100644 formal/promela/models/messages/archive/20221220-110211/msg-mgr-model.pml22.trail create mode 100644 formal/promela/models/messages/archive/20221220-110211/msg-mgr-model.pml23.trail create mode 100644 formal/promela/models/messages/archive/20221220-110211/msg-mgr-model.pml3.trail create mode 100644 formal/promela/models/messages/archive/20221220-110211/msg-mgr-model.pml4.trail create mode 100644 formal/promela/models/messages/archive/20221220-110211/msg-mgr-model.pml5.trail create mode 100644 formal/promela/models/messages/archive/20221220-110211/msg-mgr-model.pml6.trail create mode 100644 formal/promela/models/messages/archive/20221220-110211/msg-mgr-model.pml7.trail create mode 100644 formal/promela/models/messages/archive/20221220-110211/msg-mgr-model.pml8.trail create mode 100644 formal/promela/models/messages/archive/20221220-110211/msg-mgr-model.pml9.trail create mode 100644 formal/promela/models/messages/archive/20221220-110211/tr-msg-mgr-model-0.c create mode 100644 formal/promela/models/messages/archive/20221220-110211/tr-msg-mgr-model-1.c create mode 100644 formal/promela/models/messages/archive/20221220-110211/tr-msg-mgr-model-10.c create mode 100644 formal/promela/models/messages/archive/20221220-110211/tr-msg-mgr-model-11.c create mode 100644 formal/promela/models/messages/archive/20221220-110211/tr-msg-mgr-model-12.c create mode 100644 formal/promela/models/messages/archive/20221220-110211/tr-msg-mgr-model-13.c create mode 100644 formal/promela/models/messages/archive/20221220-110211/tr-msg-mgr-model-14.c create mode 100644 formal/promela/models/messages/archive/20221220-110211/tr-msg-mgr-model-15.c create mode 100644 formal/promela/models/messages/archive/20221220-110211/tr-msg-mgr-model-16.c create mode 100644 formal/promela/models/messages/archive/20221220-110211/tr-msg-mgr-model-17.c create mode 100644 formal/promela/models/messages/archive/20221220-110211/tr-msg-mgr-model-18.c create mode 100644 formal/promela/models/messages/archive/20221220-110211/tr-msg-mgr-model-19.c create mode 100644 formal/promela/models/messages/archive/20221220-110211/tr-msg-mgr-model-2.c create mode 100644 formal/promela/models/messages/archive/20221220-110211/tr-msg-mgr-model-20.c create mode 100644 formal/promela/models/messages/archive/20221220-110211/tr-msg-mgr-model-21.c create mode 100644 formal/promela/models/messages/archive/20221220-110211/tr-msg-mgr-model-22.c create mode 100644 formal/promela/models/messages/archive/20221220-110211/tr-msg-mgr-model-3.c create mode 100644 formal/promela/models/messages/archive/20221220-110211/tr-msg-mgr-model-4.c create mode 100644 formal/promela/models/messages/archive/20221220-110211/tr-msg-mgr-model-5.c create mode 100644 formal/promela/models/messages/archive/20221220-110211/tr-msg-mgr-model-6.c create mode 100644 formal/promela/models/messages/archive/20221220-110211/tr-msg-mgr-model-7.c create mode 100644 formal/promela/models/messages/archive/20221220-110211/tr-msg-mgr-model-8.c create mode 100644 formal/promela/models/messages/archive/20221220-110211/tr-msg-mgr-model-9.c create mode 100644 formal/promela/models/messages/msg-mgr-model-post.h create mode 100644 formal/promela/models/messages/msg-mgr-model-pre.h create mode 100644 formal/promela/models/messages/msg-mgr-model-rfn.yml create mode 100644 formal/promela/models/messages/msg-mgr-model-run.h create mode 100644 formal/promela/models/messages/msg-mgr-model.pml create mode 100644 formal/promela/models/messages/tc-msg-mgr-model.c create mode 100644 formal/promela/models/messages/tr-msg-mgr-model.c create mode 100644 formal/promela/models/messages/tr-msg-mgr-model.h create mode 100644 formal/promela/models/threadq/MrsP-Code/Chains.pml create mode 100644 formal/promela/models/threadq/MrsP-Code/Concurrency.pml create mode 100644 formal/promela/models/threadq/MrsP-Code/Heaps.pml create mode 100644 formal/promela/models/threadq/MrsP-Code/Init.pml create mode 100644 formal/promela/models/threadq/MrsP-Code/Locks.pml create mode 100644 formal/promela/models/threadq/MrsP-Code/MAIN.pml create mode 100644 formal/promela/models/threadq/MrsP-Code/Priority.pml create mode 100644 formal/promela/models/threadq/MrsP-Code/RBTrees.pml create mode 100644 formal/promela/models/threadq/MrsP-Code/Scenarios.pml create mode 100644 formal/promela/models/threadq/MrsP-Code/Semaphores.pml create mode 100644 formal/promela/models/threadq/MrsP-Code/Sizing.pml create mode 100644 formal/promela/models/threadq/MrsP-Code/State.pml create mode 100644 formal/promela/models/threadq/MrsP-Code/Structs.pml create mode 100644 formal/promela/models/threadq/MrsP-Code/Values.pml create mode 100644 formal/promela/models/threadq/MrsP-Tests/Configure.pml create mode 100644 formal/promela/models/threadq/MrsP-Tests/Run.pml create mode 100644 formal/promela/models/threadq/MrsP-Tests/Sizing.pml create mode 100644 formal/promela/models/threadq/MrsP-Tests/Utilities.pml create mode 100644 formal/promela/models/threadq/MrsP-Tests/mrsp-threadq-model-post.h create mode 100644 formal/promela/models/threadq/MrsP-Tests/mrsp-threadq-model-pre.h create mode 100644 formal/promela/models/threadq/MrsP-Tests/mrsp-threadq-model-rfn.yml create mode 100644 formal/promela/models/threadq/MrsP-Tests/mrsp-threadq-model-run.h create mode 100644 formal/promela/models/threadq/MrsP-Tests/mrsp-threadq-model.pml create mode 100644 formal/promela/models/threadq/MrsP-Tests/tc-mrsp-threadq-model.c create mode 100644 formal/promela/models/threadq/MrsP-Tests/tr-mrsp-threadq-model.c create mode 100644 formal/promela/models/threadq/MrsP-Tests/tr-mrsp-threadq-model.h create mode 100644 formal/promela/models/threadq/Weak-Memory/RAM.pml create mode 100644 formal/promela/models/threadq/Weak-Memory/SPARC-TSO.pml create mode 100644 formal/promela/models/threadq/Weak-Memory/memory_model.pml create mode 100644 formal/promela/models/threadq/Weak-Memory/wmemory.pml create mode 100644 formal/promela/src/Makefile create mode 100644 formal/promela/src/README.md create mode 100644 formal/promela/src/examples/draft/make.sh create mode 100644 formal/promela/src/examples/draft/parse.pml create mode 100644 formal/promela/src/examples/model_checker/spin.pml create mode 100644 formal/promela/src/examples/requirements.txt create mode 100644 formal/promela/src/gentest.py create mode 100644 formal/promela/src/metrics.py create mode 100644 formal/promela/src/requirements.txt create mode 100644 formal/promela/src/spin2test.coco create mode 100644 formal/promela/src/src.sh create mode 100644 formal/promela/src/src/__init__.py create mode 100644 formal/promela/src/src/library.coco create mode 100644 formal/promela/src/src/library.py create mode 100644 formal/promela/src/src/modules/comment-filter/AUTHORS create mode 100644 formal/promela/src/src/modules/comment-filter/LICENSE create mode 100644 formal/promela/src/src/modules/comment-filter/README.md create mode 100644 formal/promela/src/src/modules/comment-filter/comment_filter/__init__.py create mode 100644 formal/promela/src/src/modules/comment-filter/comment_filter/language.py create mode 100644 formal/promela/src/src/modules/comment-filter/comment_filter/rfc.py create mode 100644 formal/promela/src/src/modules/comment-filter/setup.cfg create mode 100644 formal/promela/src/src/modules/comment-filter/setup.py create mode 100644 formal/promela/src/src/modules/comment-filter/tox.ini create mode 100644 formal/promela/src/src/modules/promela_yacc/LICENSE create mode 100644 formal/promela/src/src/modules/promela_yacc/README.md create mode 100644 formal/promela/src/src/modules/promela_yacc/promela/__init__.py create mode 100644 formal/promela/src/src/modules/promela_yacc/promela/ast.py create mode 100644 formal/promela/src/src/modules/promela_yacc/promela/lex.py create mode 100644 formal/promela/src/src/modules/promela_yacc/promela/yacc.py create mode 100644 formal/promela/src/src/modules/promela_yacc/setup.py create mode 100644 formal/promela/src/src/refine_command.coco create mode 100644 formal/promela/src/src/refine_command.py create mode 100644 formal/promela/src/src/spin2test.coco create mode 100644 formal/promela/src/src/spin2test.py create mode 100644 formal/promela/src/src/syntax_ml.coco create mode 100644 formal/promela/src/src/syntax_ml.py create mode 100644 formal/promela/src/src/syntax_pml.coco create mode 100644 formal/promela/src/src/syntax_pml.py create mode 100644 formal/promela/src/src/syntax_yaml.coco create mode 100644 formal/promela/src/src/syntax_yaml.py create mode 100644 formal/promela/src/src/testgen.coco create mode 100644 formal/promela/src/src/testgen.py create mode 100644 formal/promela/src/src/tests/__init__.py create mode 100644 formal/promela/src/src/tests/library.coco create mode 100644 formal/promela/src/src/tests/library.py create mode 100644 formal/promela/src/src/tests/test_coverage_spin2test.coco create mode 100644 formal/promela/src/src/tests/test_coverage_spin2test.py create mode 100644 formal/promela/src/src/tests/test_coverage_testgen.coco create mode 100644 formal/promela/src/src/tests/test_coverage_testgen.py create mode 100644 formal/promela/src/src/tests/test_optional.coco create mode 100644 formal/promela/src/src/tests/test_optional.py create mode 100644 formal/promela/src/testbuilder-template.yml create mode 100644 formal/promela/src/testbuilder.help create mode 100755 formal/promela/src/testbuilder.py create mode 100644 formal/promela/src/testgen_ml.coco create mode 100644 formal/promela/src/testgen_ml.py create mode 100755 formal/promela/src/testgen_ml.sh create mode 100755 formal/promela/src/testgen_ml_spin.sh create mode 100644 formal/promela/src/testgen_yaml.coco create mode 100644 formal/promela/src/testgen_yaml.py create mode 100755 formal/promela/src/testgen_yaml.sh create mode 100755 formal/promela/src/testgen_yaml_spin.sh -- 2.37.1 (Apple Git-137.1) _______________________________________________ devel mailing list devel@rtems.org http://lists.rtems.org/mailman/listinfo/devel