[PATCH 00/18] Adds Formal Verification Material
Andrew.Butterfield at scss.tcd.ie
Andrew.Butterfield at scss.tcd.ie
Sat Dec 24 14:21:58 UTC 2022
Hi Joel,
Yes – apologies for not being clear abut that!
Andrew
From: Joel Sherrill <joel at rtems.org>
Reply to: "joel at rtems.org" <joel at rtems.org>
Date: Friday 23 December 2022 at 19:46
To: "Andrew.Butterfield at scss.tcd.ie" <Andrew.Butterfield at scss.tcd.ie>
Cc: "rtems-devel at rtems.org" <rtems-devel at rtems.org>
Subject: Re: [PATCH 00/18] Adds Formal Verification Material
Is this intended for the rtems-central repository?
--joel
On Thu, Dec 22, 2022 at 5:29 AM Andrew.Butterfield at scss.tcd.ie<mailto:Andrew.Butterfield at scss.tcd.ie> <Andrew.Butterfield at scss.tcd.ie<mailto: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<mailto: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<mailto: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/20221224/54d6bddd/attachment-0001.htm>
More information about the devel
mailing list