[PATCH 00/18] Adds Formal Verification Material

Andrew.Butterfield at scss.tcd.ie Andrew.Butterfield at scss.tcd.ie
Thu Dec 22 11:29:07 UTC 2022


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)
 



More information about the devel mailing list