[PATCH 00/18] Adds Formal Verification Material
Joel Sherrill
joel at rtems.org
Fri Dec 23 19:44:46 UTC 2022
Is this intended for the rtems-central repository?
--joel
On Thu, Dec 22, 2022 at 5:29 AM Andrew.Butterfield at scss.tcd.ie <
Andrew.Butterfield at scss.tcd.ie> wrote:
> From 3390ccc51f46ce0a4baa60422a62530c7c3c29bd Mon Sep 17 00:00:00 2001
> From: Andrew Butterfield <Andrew.Butterfield at 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 at rtems.org
> http://lists.rtems.org/mailman/listinfo/devel
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.rtems.org/pipermail/devel/attachments/20221223/91e3792e/attachment-0001.htm>
More information about the devel
mailing list