[rtems-central commit] top-level sources
Sebastian Huber
sebh at rtems.org
Wed Jan 18 11:35:17 UTC 2023
Module: rtems-central
Branch: master
Commit: bd28429016cb5021c00e2d6481a6182df4de6b9e
Changeset: http://git.rtems.org/rtems-central/commit/?id=bd28429016cb5021c00e2d6481a6182df4de6b9e
Author: Andrew Butterfield <Andrew.Butterfield at scss.tcd.ie>
Date: Tue Jan 10 19:55:50 2023 +0000
top-level sources
---
formal/promela/src/Makefile | 55 +++++
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/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.sh | 19 ++
formal/promela/src/testgen_ml_spin.sh | 19 ++
formal/promela/src/testgen_yaml.coco | 48 +++++
formal/promela/src/testgen_yaml.sh | 19 ++
formal/promela/src/testgen_yaml_spin.sh | 19 ++
15 files changed, 755 insertions(+)
diff --git a/formal/promela/src/Makefile b/formal/promela/src/Makefile
new file mode 100644
index 00000000..ef382b5e
--- /dev/null
+++ b/formal/promela/src/Makefile
@@ -0,0 +1,55 @@
+# SPDX-License-Identifier: BSD-2-Clause
+# https://gitrepos.estec.esa.int/external/rtems-smp-qualification-qual/-/blob/ef082e24b0047790c38a9bef14414849a2ba6d5b/Makefile
+
+DIR_SRC = src
+DIR_TESTS = $(DIR_SRC)/tests
+COCO_SRC_FILES = $(wildcard *.coco $(DIR_SRC)/*.coco $(DIR_TESTS)/*.coco)
+PY_GEN_FILES = $(patsubst %.coco,%.py,$(COCO_SRC_FILES))
+
+.PHONY: all py check format analyse metric git-hash-object-calculate sha512sum-calculate check-env coverage-report env clean
+
+all: check format analyse coverage-report
+
+%.py: %.coco | check-env
+ coconut --target 3 $< $@
+
+py: $(PY_GEN_FILES) | check-env
+
+check: $(PY_GEN_FILES) | check-env
+ coverage run --branch -m pytest --capture=tee-sys -vv -s $(DIR_TESTS)/test_coverage_testgen.py $(DIR_TESTS)/test_coverage_spin2test.py
+
+format: $(PY_GEN_FILES) | check-env
+ yapf -i --parallel $^
+
+analyse: $(PY_GEN_FILES) | check-env
+ flake8 $^
+ mypy $^
+ pylint --disable=duplicate-code --disable=unspecified-encoding --disable=consider-using-dict-items --disable=use-list-literal --disable=consider-using-with $^
+
+metric: $(PY_GEN_FILES) | check-env
+ python3 metrics.py $(PY_GEN_FILES)
+
+git-hash-object-calculate:
+ git hash-object $(COCO_SRC_FILES)
+
+sha512sum-calculate:
+ sha512sum $(COCO_SRC_FILES)
+
+check-env:
+ test -n "$$VIRTUAL_ENV"
+
+EMPTY :=
+SPACE := $(EMPTY) $(EMPTY)
+COMMA := ,
+
+coverage-report: | check-env
+ coverage report -m --fail-under=100 --include=$(subst $(SPACE),$(COMMA),$(PY_GEN_FILES))
+
+# sudo apt-get install python3-venv python3-dev
+env:
+ python3 -m venv env
+ . env/bin/activate && pip install --upgrade pip && pip install -r requirements.txt
+
+clean:
+ rm -rf $(PY_GEN_FILES) .coverage .mypy_cache .pytest_cache
+ find $(DIR_SRC) -name __pycache__ -exec rm -rf '{}' +
diff --git a/formal/promela/src/gentest.py b/formal/promela/src/gentest.py
new file mode 100644
index 00000000..81cb4552
--- /dev/null
+++ b/formal/promela/src/gentest.py
@@ -0,0 +1,46 @@
+# SPDX-License-Identifier: BSD-2-Clause
+"""Converts Annotated SPIN counter-examples to program test code"""
+
+# Copyright (C) 2019-2021 Trinity College Dublin (www.tcd.ie)
+#
+# Redistribution and use in source and binary forms, with or without
+# modification, are permitted provided that the following conditions
+# are met:
+# 1. Redistributions of source code must retain the above copyright
+# notice, this list of conditions and the following disclaimer.
+# 2. Redistributions in binary form must reproduce the above copyright
+# notice, this list of conditions and the following disclaimer in the
+# documentation and/or other materials provided with the distribution.
+#
+# THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
+# AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
+# IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
+# ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
+# LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
+# CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
+# SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
+# INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
+# CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
+# ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
+# POSSIBILITY OF SUCH DAMAGE.
+
+import src.spin2test as s2t
+
+#
+
+import argparse
+import logging
+import sys
+import yaml
+
+#
+
+claparser = argparse.ArgumentParser(description="Promela to Program Test Generator")
+claparser.add_argument("root", help="Model filename root")
+claparser.add_argument("tstno", help="Model test number")
+
+cl_args = claparser.parse_args()
+fileRoot = cl_args.root
+testNumber = cl_args.tstno
+
+s2t.main(testNumber,"",fileRoot)
diff --git a/formal/promela/src/metrics.py b/formal/promela/src/metrics.py
new file mode 100644
index 00000000..a7d20a55
--- /dev/null
+++ b/formal/promela/src/metrics.py
@@ -0,0 +1,11 @@
+#
+
+# SPDX-License-Identifier: BSD-3-Clause
+# Copyright (C) 2019-2021 Trinity College Dublin (www.tcd.ie)
+
+import sys
+
+#
+
+if __name__ == '__main__':
+ print(f'{sys.argv}')
diff --git a/formal/promela/src/requirements.txt b/formal/promela/src/requirements.txt
new file mode 100644
index 00000000..f6f48fd4
--- /dev/null
+++ b/formal/promela/src/requirements.txt
@@ -0,0 +1,35 @@
+astroid==2.4.2
+attrs==20.3.0
+coconut==1.4.3
+coverage==5.3
+cPyparsing==2.4.5.0.1.1
+decorator==4.4.2
+flake8==3.8.4
+importlib-metadata==3.1.1
+iniconfig==1.1.1
+isort==5.6.4
+lazy-object-proxy==1.4.3
+mccabe==0.6.1
+mypy==0.782
+mypy-extensions==0.4.3
+networkx==2.5
+packaging==20.7
+parsec==3.5
+pluggy==0.13.1
+ply==3.10
+prompt-toolkit==3.0.8
+py==1.9.0
+pycodestyle==2.6.0
+pyflakes==2.2.0
+Pygments==2.7.2
+pylint==2.6.0
+pytest==6.1.2
+PyYAML==5.3.1
+six==1.15.0
+toml==0.10.2
+typed-ast==1.4.1
+typing-extensions==3.7.4.3
+wcwidth==0.2.5
+wrapt==1.12.1
+yapf==0.30.0
+zipp==3.4.0
diff --git a/formal/promela/src/spin2test.coco b/formal/promela/src/spin2test.coco
new file mode 100644
index 00000000..047c8114
--- /dev/null
+++ b/formal/promela/src/spin2test.coco
@@ -0,0 +1,41 @@
+# SPDX-License-Identifier: BSD-2-Clause
+"""Converts an Annotated SPIN counter-example to program test code"""
+
+# Copyright (C) 2019-2021 Trinity College Dublin (www.tcd.ie)
+#
+# Redistribution and use in source and binary forms, with or without
+# modification, are permitted provided that the following conditions
+# are met:
+# 1. Redistributions of source code must retain the above copyright
+# notice, this list of conditions and the following disclaimer.
+# 2. Redistributions in binary form must reproduce the above copyright
+# notice, this list of conditions and the following disclaimer in the
+# documentation and/or other materials provided with the distribution.
+#
+# THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
+# AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
+# IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
+# ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
+# LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
+# CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
+# SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
+# INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
+# CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
+# ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
+# POSSIBILITY OF SUCH DAMAGE.
+
+import src.spin2test
+
+#
+
+import argparse
+
+#
+
+if __name__ == '__main__':
+ claparser = argparse.ArgumentParser(description="Promela to Program Test Generator")
+ claparser.add_argument("root", help="Model filename root")
+ claparser.add_argument("tstno", help="Model test number")
+
+ cl_args = claparser.parse_args()
+ src.spin2test.main (cl_args.tstno, '', cl_args.root)
diff --git a/formal/promela/src/src.sh b/formal/promela/src/src.sh
new file mode 100644
index 00000000..9174dc60
--- /dev/null
+++ b/formal/promela/src/src.sh
@@ -0,0 +1,13 @@
+#
+
+# SPDX-License-Identifier: BSD-3-Clause
+# Copyright (C) 2019-2021 Trinity College Dublin (www.tcd.ie)
+
+if [ ! -f env/bin/activate ]
+then
+ make env
+fi
+
+source env/bin/activate
+
+make py
diff --git a/formal/promela/src/testbuilder-template.yml b/formal/promela/src/testbuilder-template.yml
new file mode 100644
index 00000000..6e7cf1d4
--- /dev/null
+++ b/formal/promela/src/testbuilder-template.yml
@@ -0,0 +1,42 @@
+# SPDX-License-Identifier: BSD-2-Clause
+# Runs SPIN to generate test code for all defined scenarios
+
+# Copyright (C) 2021 Trinity College Dublin (www.tcd.ie)
+# Robert Jennings
+# Andrew Butterfield
+#
+# Redistribution and use in source and binary forms, with or without
+# modification, are permitted provided that the following conditions
+# are met:
+# 1. Redistributions of source code must retain the above copyright
+# notice, this list of conditions and the following disclaimer.
+# 2. Redistributions in binary form must reproduce the above copyright
+# notice, this list of conditions and the following disclaimer in the
+# documentation and/or other materials provided with the distribution.
+#
+# THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
+# AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
+# IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
+# ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
+# LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
+# CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
+# SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
+# INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
+# CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
+# ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
+# POSSIBILITY OF SUCH DAMAGE.
+
+# This should be specialised for your setup, as testbuilder.yml,
+# located in the same directory as testbuilder.py
+# All pathnames should be absolute
+
+spin2test: <spin2test_directory>/spin2test.py
+rtems: <path-to-main-rtems-directory> # rtems.git, or ..../modules/rtems/
+rsb: <rsb-build_directory>/rtems/6/bin/
+simulator: <path-to>/sparc-rtems6-sis
+testyamldir: <rtems>/spec/build/testsuites/validation/ # directory containing <modelname>.yml
+testcode: <rtems>/testsuites/validation/
+testexedir: <rtems>/build/.../testsuites/validation/ # directory containing ts-<modelname>.exe
+testsuite: model-0
+simulatorargs: -leon3 -r s -m 2 # run command executes "<simulator> <simargs> <testexedir>/ts-<testsuite>.exe"
+spinallscenarios: -DTEST_GEN -run -E -c0 -e # trail generation "spin <spinallscenarios> <model>.pml"
diff --git a/formal/promela/src/testbuilder.help b/formal/promela/src/testbuilder.help
new file mode 100644
index 00000000..bd7e4e02
--- /dev/null
+++ b/formal/promela/src/testbuilder.help
@@ -0,0 +1,23 @@
+This tool can generate and remove RTEMS test files from a Promela model
+
+In order to generate test files the following input files are required:
+ `<model>.pml`
+ `<model>-rfn.yml`
+ `<model>-pre.h`
+ `<model>-post.h`
+ `<model>-run.h`
+where `<model>` is the name of the model.
+
+`all <model>` will run clean, spin, gentests, copy, compile and run
+`spin <model>` will run SPIN to find all scenarios
+`gentests <model>` will produce C tests
+`clean <model>` will remove generated files.
+`copy <model>`
+ - copies the generated C files to the relevant RTEMS test source directory
+ - updates the relevant RTEMS configuration yaml file
+`archive <model>`` will copy generated spn, trail, C, and test log files
+ to the archive sub-directory of the current model directory.
+`compile` rebuilds the RTEMS test executable
+`run` runs the tests in the SIS simulator
+`zero` removes all generated C filenames from the RTEMS configuration yaml file
+ - it does NOT remove the test sources from the RTEMS test source directory
diff --git a/formal/promela/src/testbuilder.py b/formal/promela/src/testbuilder.py
new file mode 100755
index 00000000..7eba64b8
--- /dev/null
+++ b/formal/promela/src/testbuilder.py
@@ -0,0 +1,317 @@
+#!/usr/bin/env python3
+# SPDX-License-Identifier: BSD-2-Clause
+"""Runs SPIN to generate test code for all defined scenarios"""
+
+# Copyright (C) 2021-22 Trinity College Dublin (www.tcd.ie)
+# Robert Jennings
+# Andrew Butterfield
+# James Gooding Hunt
+#
+# Redistribution and use in source and binary forms, with or without
+# modification, are permitted provided that the following conditions
+# are met:
+# 1. Redistributions of source code must retain the above copyright
+# notice, this list of conditions and the following disclaimer.
+# 2. Redistributions in binary form must reproduce the above copyright
+# notice, this list of conditions and the following disclaimer in the
+# documentation and/or other materials provided with the distribution.
+#
+# THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
+# AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
+# IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
+# ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
+# LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
+# CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
+# SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
+# INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
+# CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
+# ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
+# POSSIBILITY OF SUCH DAMAGE.
+
+import sys
+import os
+import subprocess
+import glob
+import shutil
+from functools import wraps
+import yaml
+from pathlib import Path
+from datetime import datetime
+
+
+def catch_subprocess_errors(func):
+ @wraps(func)
+ def wrapper(*args, **kwargs):
+ try:
+ result = func(*args, **kwargs)
+ except subprocess.CalledProcessError as e:
+ print(f"error executing: {e.cmd}")
+ sys.exit(1)
+ return result
+ return wrapper
+
+
+def run_all(model, config):
+ clean(model, config["testsuite"])
+ generate_spin_files(model, config["spinallscenarios"])
+ generate_test_files(model, config["spin2test"])
+ copy(sys.argv[2], config["testcode"], config["rtems"],
+ config["testyaml"], config["testsuite"])
+ compile(config["rtems"])
+ run_simulator(config["simulator"],
+ config["simulatorargs"], config["testexe"], config["testsuite"])
+
+
+def clean(model,testsuite):
+ """Cleans out generated files in current directory"""
+ print(f"Removing spin and test files for {model}")
+ files = get_generated_files(model,testsuite)
+ for file in files:
+ os.remove(file)
+
+
+def archive(model,testsuite):
+ print(f"Archiving spin and test files for {model}")
+ files = get_generated_files(model,testsuite)
+ date = datetime.now().strftime("%Y%m%d-%H%M%S")
+ archive_dir = Path(f"archive/{date}")
+ archive_dir.mkdir(parents=True, exist_ok=True)
+ for file in files:
+ shutil.copy2(file, archive_dir)
+ print(f"Files archived to {archive_dir}")
+
+
+def zero(model_file, testsuite_name):
+ """Modifies model file to refer only to the top-level testcase source"""
+ # Update {model_file}.yml
+ print(f"Zeroing {testsuite_name}.yml")
+ with open(model_file) as file:
+ model_yaml = yaml.load(file, Loader=yaml.FullLoader)
+ model_yaml['source'] = [f"testsuites/validation/ts-{testsuite_name}.c"]
+ with open(model_file, 'w') as file:
+ yaml.dump(model_yaml, file)
+
+
+def ready_to_generate(model):
+ """Checks if relevant files are in place for spin and test generation"""
+ ready = True
+ if not os.path.isfile(f"{model}.pml"):
+ print("Promela file does not exist for model")
+ ready = False
+ if not os.path.isfile(f"{model}-pre.h"):
+ print("Preconditions file does not exist for model")
+ ready = False
+ if not os.path.isfile(f"{model}-post.h"):
+ print("Postconditions file does not exist for model")
+ ready = False
+ if not os.path.isfile(f"{model}-run.h"):
+ print("Promela file does not exist for model")
+ ready = False
+ if not os.path.isfile(f"{model}-rfn.yml"):
+ print("Refinement file does not exist for model")
+ ready = False
+ return ready
+
+
+ at catch_subprocess_errors
+def generate_spin_files(model, spinallscenarios):
+ """Create spin files from model"""
+ if not ready_to_generate(model):
+ sys.exit(1)
+ print(f"Generating spin files for {model}")
+ subprocess.run(f"spin {spinallscenarios} {model}.pml",
+ check=True, shell=True)
+ no_of_trails = len(glob.glob(f"{model}*.trail"))
+ if no_of_trails == 0:
+ print("no trail files generated")
+ elif no_of_trails == 1:
+ subprocess.run(f"spin -T -t {model}.pml > {model}.spn",
+ check=True, shell=True)
+ else:
+ for i in range(no_of_trails):
+ subprocess.run(f"spin -T -t{i + 1} {model}.pml > {model}-{i}.spn",
+ check=True, shell=True)
+ os.remove('pan')
+
+ at catch_subprocess_errors
+def generate_test_files(model, testgen):
+ """Create test files from spin files"""
+ if not ready_to_generate(model):
+ sys.exit(1)
+ print(f"Generating test files for {model}")
+ no_of_trails = len(glob.glob(f"{model}*.trail"))
+ if no_of_trails == 0:
+ print("no trail files found")
+ elif no_of_trails == 1:
+ subprocess.run(f"python {testgen} {model}", check=True, shell=True)
+ else:
+ for i in range(no_of_trails):
+ subprocess.run(f"python {testgen} {model} {i}",
+ check=True, shell=True)
+
+
+def copy(model, codedir, rtems, modfile, testsuite_name):
+ """Copies C testfiles to test directory and updates the model file """
+ # Remove old test files
+ print(f"Removing old files for model {model}")
+ files = glob.glob(f"{codedir}tr-{model}*.c")
+ files += glob.glob(f"{codedir}tr-{model}*.h")
+ files += glob.glob(f"{codedir}tc-{model}*.c")
+ for file in files:
+ os.remove(file)
+
+ # Copy new test files
+ print(f"Copying new files for model {model}")
+ files = glob.glob(f"tr-{model}*.c")
+ files += glob.glob(f"tr-{model}*.h")
+ files += glob.glob(f"tc-{model}*.c")
+ for file in files:
+ shutil.copyfile(file, f"{rtems}testsuites/validation/{file}")
+
+ # Update {testsuite name}.yml
+ print(f"Updating {testsuite_name}.yml for model {model}")
+ with open(modfile) as file:
+ model_yaml = yaml.load(file, Loader=yaml.FullLoader)
+ source_list = model_yaml['source']
+ source_set = set(source_list)
+ files = glob.glob(f"tr-{model}*.c")
+ files += glob.glob(f"tc-{model}*.c")
+ for file in files:
+ source_set.add(f"testsuites/validation/{file}")
+ new_list = list(source_set)
+ model_yaml['source'] = sorted(new_list)
+ with open(modfile, 'w') as file:
+ yaml.dump(model_yaml, file)
+
+
+ at catch_subprocess_errors
+def compile(rtems_dir):
+ cwd = os.getcwd()
+ os.chdir(rtems_dir)
+ subprocess.run("./waf configure", check=True, shell=True)
+ subprocess.run("./waf", check=True, shell=True)
+ os.chdir(cwd)
+
+
+ at catch_subprocess_errors
+def run_simulator(simulator_path, simulator_args, testexe, testsuite):
+ sim_command = f"{simulator_path} {simulator_args}"
+ print(f"Doing {sim_command} {testexe}")
+ subprocess.run(f"{sim_command} {testexe} > {testsuite}-test.log",
+ check=True, shell=True)
+
+
+def get_generated_files(model,testsuite):
+ trails = glob.glob(f"{model}*.trail")
+ files = trails
+ files += glob.glob(f"{model}*.spn")
+ if len(trails) == 1:
+ files += glob.glob(f"tr-{model}-0.c")
+ else:
+ files += glob.glob(f"tr-{model}-*.c")
+ files += glob.glob(f"{testsuite}-test.log")
+ return files
+
+
+def get_config(source_dir):
+ config = dict()
+ with open(f"{source_dir}/testbuilder.yml") as file:
+ global_config = yaml.load(file, Loader=yaml.FullLoader)
+ for key, val in global_config.items():
+ config[key] = val
+ if Path("testbuilder.yml").exists():
+ with open("testbuilder.yml") as file:
+ local_config = yaml.load(file, Loader=yaml.FullLoader)
+ if local_config:
+ for key, val in local_config.items():
+ config[key] = val
+ if "testsuite" not in config.keys():
+ config["testsuite"] = "model-0"
+ missing_keys = {"spin2test", "rtems", "rsb", "simulator", "testyamldir",
+ "testcode", "testexedir", "simulatorargs",
+ "spinallscenarios"} - config.keys()
+ if missing_keys:
+ print("testbuilder.yml configuration is incomplete")
+ print("The following configuration items are missing:")
+ for key in missing_keys:
+ print(key)
+ sys.exit(1)
+ config["testyaml"] = f"{config['testyamldir']}{config['testsuite']}.yml"
+ config["testexe"] = f"{config['testexedir']}ts-{config['testsuite']}.exe"
+ return config
+
+
+def main():
+ """generates and deploys C tests from Promela models"""
+ if not (len(sys.argv) == 2 and sys.argv[1] == "help"
+ or len(sys.argv) == 3 and sys.argv[1] == "all"
+ or len(sys.argv) == 3 and sys.argv[1] == "clean"
+ or len(sys.argv) == 3 and sys.argv[1] == "archive"
+ or len(sys.argv) == 2 and sys.argv[1] == "zero"
+ or len(sys.argv) == 3 and sys.argv[1] == "spin"
+ or len(sys.argv) == 3 and sys.argv[1] == "gentests"
+ or len(sys.argv) == 3 and sys.argv[1] == "copy"
+ or len(sys.argv) == 2 and sys.argv[1] == "compile"
+ or len(sys.argv) == 2 and sys.argv[1] == "run"):
+ print("USAGE:")
+ print("help - more details about usage and commands below")
+ print("all modelname - runs clean, spin, gentests, copy, compile and "
+ "run")
+ print("clean modelname - remove spin, test files")
+ print("archive modelname - archives spin, test files")
+ print("zero - remove all tesfiles from RTEMS")
+ print("spin modelname - generate spin files")
+ print("gentests modelname - generate test files")
+ print("copy modelname - copy test files and configuration to RTEMS")
+ print("compile - compiles RTEMS tests")
+ print("run - runs RTEMS tests")
+ sys.exit(1)
+
+ source_dir = os.path.dirname(os.path.realpath(__file__))
+
+ config = get_config(source_dir)
+
+ if not Path.exists(Path(f"{source_dir}/spin2test.py")) \
+ or not Path.exists(Path(f"{source_dir}/env")):
+ print("Setup incomplete...")
+ print("Please run the following before continuing:")
+ print(f"cd {source_dir} && bash src.sh")
+ print(f". {source_dir}/env/bin/activate")
+ sys.exit(1)
+
+ if sys.argv[1] == "help":
+ with open(f"{source_dir}/testbuilder.help") as helpfile:
+ print(helpfile.read())
+
+ if sys.argv[1] == "all":
+ run_all(sys.argv[2], config)
+
+ if sys.argv[1] == "spin":
+ generate_spin_files(sys.argv[2], config["spinallscenarios"])
+
+ if sys.argv[1] == "gentests":
+ generate_test_files(sys.argv[2], config["spin2test"])
+
+ if sys.argv[1] == "clean":
+ clean(sys.argv[2], config["testsuite"])
+
+ if sys.argv[1] == "archive":
+ archive(sys.argv[2], config["testsuite"])
+
+ if sys.argv[1] == "zero":
+ zero(config["testyaml"], config["testsuite"])
+
+ if sys.argv[1] == "copy":
+ copy(sys.argv[2], config["testcode"], config["rtems"],
+ config["testyaml"], config["testsuite"])
+
+ if sys.argv[1] == "compile":
+ compile(config["rtems"])
+
+ if sys.argv[1] == "run":
+ run_simulator(config["simulator"],
+ config["simulatorargs"], config["testexe"], config["testsuite"])
+
+
+if __name__ == '__main__':
+ main()
diff --git a/formal/promela/src/testgen_ml.coco b/formal/promela/src/testgen_ml.coco
new file mode 100644
index 00000000..d4c84c68
--- /dev/null
+++ b/formal/promela/src/testgen_ml.coco
@@ -0,0 +1,48 @@
+ # SPDX-License-Identifier: BSD-2-Clause
+
+ ##############################################################################
+ # Testgen ML
+ #
+ # Copyright (C) 2019-2021 Trinity College Dublin (www.tcd.ie)
+ #
+ # All rights reserved.
+ #
+ # Redistribution and use in source and binary forms, with or without
+ # modification, are permitted provided that the following conditions are
+ # met:
+ #
+ # * Redistributions of source code must retain the above copyright
+ # notice, this list of conditions and the following disclaimer.
+ #
+ # * Redistributions in binary form must reproduce the above
+ # copyright notice, this list of conditions and the following
+ # disclaimer in the documentation and/or other materials provided
+ # with the distribution.
+ #
+ # * Neither the name of the copyright holders nor the names of its
+ # contributors may be used to endorse or promote products derived
+ # from this software without specific prior written permission.
+ #
+ # THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+ # "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+ # LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+ # A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
+ # OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
+ # SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
+ # LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
+ # DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
+ # THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+ # (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+ # OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ ##############################################################################
+
+import src.testgen
+
+#
+
+import sys
+
+#
+
+if __name__ == '__main__':
+ src.testgen.main (0, sys.argv[1:], False)
diff --git a/formal/promela/src/testgen_ml.sh b/formal/promela/src/testgen_ml.sh
new file mode 100755
index 00000000..98e57858
--- /dev/null
+++ b/formal/promela/src/testgen_ml.sh
@@ -0,0 +1,19 @@
+#!/bin/bash
+
+# SPDX-License-Identifier: BSD-3-Clause
+# Copyright (C) 2019-2021 Trinity College Dublin (www.tcd.ie)
+
+set -x
+set -e
+set -o pipefail
+
+# resolve home directory of the project
+HOME0="$(dirname "$(python3 -c "import os; print(os.path.realpath('$0'))")")"
+
+# load virtual environment
+cd "$HOME0"
+source src.sh
+cd -
+
+# exec in the virtual environment
+exec python3 "$HOME0/testgen_ml.py" "$@"
diff --git a/formal/promela/src/testgen_ml_spin.sh b/formal/promela/src/testgen_ml_spin.sh
new file mode 100755
index 00000000..80753be5
--- /dev/null
+++ b/formal/promela/src/testgen_ml_spin.sh
@@ -0,0 +1,19 @@
+#!/bin/bash
+
+# SPDX-License-Identifier: BSD-3-Clause
+# Copyright (C) 2019-2021 Trinity College Dublin (www.tcd.ie)
+
+set -x
+set -e
+set -o pipefail
+
+# resolve home directory of the project
+HOME0="$(dirname "$(python3 -c "import os; print(os.path.realpath('$0'))")")"
+
+# load virtual environment
+cd "$HOME0"
+source src.sh
+cd -
+
+# exec in the virtual environment
+exec python3 "$HOME0/testgen_ml.py" "$HOME0/../examples/model_checker/spin.pml" "$@"
diff --git a/formal/promela/src/testgen_yaml.coco b/formal/promela/src/testgen_yaml.coco
new file mode 100644
index 00000000..22c3498f
--- /dev/null
+++ b/formal/promela/src/testgen_yaml.coco
@@ -0,0 +1,48 @@
+ # SPDX-License-Identifier: BSD-2-Clause
+
+ ##############################################################################
+ # Testgen YAML
+ #
+ # Copyright (C) 2019-2021 Trinity College Dublin (www.tcd.ie)
+ #
+ # All rights reserved.
+ #
+ # Redistribution and use in source and binary forms, with or without
+ # modification, are permitted provided that the following conditions are
+ # met:
+ #
+ # * Redistributions of source code must retain the above copyright
+ # notice, this list of conditions and the following disclaimer.
+ #
+ # * Redistributions in binary form must reproduce the above
+ # copyright notice, this list of conditions and the following
+ # disclaimer in the documentation and/or other materials provided
+ # with the distribution.
+ #
+ # * Neither the name of the copyright holders nor the names of its
+ # contributors may be used to endorse or promote products derived
+ # from this software without specific prior written permission.
+ #
+ # THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+ # "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+ # LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+ # A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
+ # OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
+ # SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
+ # LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
+ # DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
+ # THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+ # (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+ # OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ ##############################################################################
+
+import src.testgen
+
+#
+
+import sys
+
+#
+
+if __name__ == '__main__':
+ src.testgen.main (0, sys.argv[1:], True)
diff --git a/formal/promela/src/testgen_yaml.sh b/formal/promela/src/testgen_yaml.sh
new file mode 100755
index 00000000..4355520a
--- /dev/null
+++ b/formal/promela/src/testgen_yaml.sh
@@ -0,0 +1,19 @@
+#!/bin/bash
+
+# SPDX-License-Identifier: BSD-3-Clause
+# Copyright (C) 2019-2021 Trinity College Dublin (www.tcd.ie)
+
+set -x
+set -e
+set -o pipefail
+
+# resolve home directory of the project
+HOME0="$(dirname "$(python3 -c "import os; print(os.path.realpath('$0'))")")"
+
+# load virtual environment
+cd "$HOME0"
+source src.sh
+cd -
+
+# exec in the virtual environment
+exec python3 "$HOME0/testgen_yaml.py" "$@"
diff --git a/formal/promela/src/testgen_yaml_spin.sh b/formal/promela/src/testgen_yaml_spin.sh
new file mode 100755
index 00000000..9f0d3dd3
--- /dev/null
+++ b/formal/promela/src/testgen_yaml_spin.sh
@@ -0,0 +1,19 @@
+#!/bin/bash
+
+# SPDX-License-Identifier: BSD-3-Clause
+# Copyright (C) 2019-2021 Trinity College Dublin (www.tcd.ie)
+
+set -x
+set -e
+set -o pipefail
+
+# resolve home directory of the project
+HOME0="$(dirname "$(python3 -c "import os; print(os.path.realpath('$0'))")")"
+
+# load virtual environment
+cd "$HOME0"
+source src.sh
+cd -
+
+# exec in the virtual environment
+exec python3 "$HOME0/testgen_yaml.py" "$HOME0/../examples/model_checker/spin.pml" "$@"
More information about the vc
mailing list