Is this intended for the rtems-central repository? --joel
On Thu, Dec 22, 2022 at 5:29 AM andrew.butterfi...@scss.tcd.ie < andrew.butterfi...@scss.tcd.ie> wrote: > 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 >
_______________________________________________ devel mailing list devel@rtems.org http://lists.rtems.org/mailman/listinfo/devel