diff --git a/.github/CODEOWNERS b/.github/CODEOWNERS index 973c9957..99af9c5d 100644 --- a/.github/CODEOWNERS +++ b/.github/CODEOWNERS @@ -3,6 +3,6 @@ # These owners will be the default owners for everything in # the repo. Unless a later match takes precedence, -# @bmw-software-engineering/maintainers will be requested for +# @bmw-software-engineering/trlc-lobster-maintainers will be requested for # review when someone opens a pull request. -* @bmw-software-engineering/maintainers +* @bmw-software-engineering/trlc-lobster-maintainers diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index d781a8da..b51cee6a 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -18,9 +18,9 @@ jobs: - uses: actions/checkout@v4 - name: Install dependencies run: | - python3 -m pip install --upgrade pip - python3 -m pip install pylint==3.2.4 pycodestyle==2.12.0 - python3 -m pip install --no-deps bmw-lobster-core bmw-lobster-tool-trlc + python3 -m pip install --upgrade pip --break-system-packages + python3 -m pip install pylint==3.2.4 pycodestyle==2.12.0 --break-system-packages + python3 -m pip install --no-deps bmw-lobster-core bmw-lobster-tool-trlc --break-system-packages - name: Executing linter run: | make lint @@ -29,46 +29,45 @@ jobs: if: success() strategy: matrix: - os: [ubuntu-latest, macos-13, macos-14] + os: [ubuntu-latest, windows-latest, macos-13, macos-14] py-version: ["3.8", "3.9", "3.10", "3.11", "3.12"] include: - os: ubuntu-latest - cvc5: "Linux" + cvc5-plat: "linux" + - os: windows-latest + cvc5-plat: "windows" - os: macos-13 brew: "/usr/local" - cvc5: "macOS" + cvc5-plat: "osx13" - os: macos-14 brew: "/opt/homebrew" - cvc5: "macOS-arm64" + cvc5-plat: "osx14" runs-on: ${{ matrix.os }} steps: - uses: actions/checkout@v4 - - name: Install cvc5 binary - uses: supplypike/setup-bin@v4 - with: - uri: 'https://github.com/cvc5/cvc5/releases/download/cvc5-1.0.8/cvc5-${{ matrix.cvc5 }}' - name: 'cvc5' - version: '1.0.8' - name: Install python version - if: matrix.os != 'macos-14' || matrix.py-version == '3.11' || matrix.py-version == '3.12' uses: actions/setup-python@v5 with: python-version: ${{ matrix.py-version }} - - name: Install python (3.8, 3.9, 3.10) on macOS-arm64 - if: matrix.os == 'macos-14' && (matrix.py-version == '3.8' || matrix.py-version == '3.9' || matrix.py-version == '3.10') + - name: Install scoop and gnu findutils on windows + if: matrix.os == 'windows-latest' run: | - brew install python@${{ matrix.py-version }} - echo "${{ matrix.brew }}/opt/python@${{ matrix.py-version }}/libexec/bin" >> $GITHUB_PATH - python${{ matrix.py-version }} -m ensurepip + Invoke-Expression (New-Object System.Net.WebClient).DownloadString('https://get.scoop.sh') + scoop install findutils + "$env:HOMEDRIVE$env:HOMEPATH\scoop\apps\findutils\current\bin" | Out-File -FilePath $env:GITHUB_PATH -Append - name: Install dependencies run: | - python -m pip install --upgrade pip - python -m pip install -r requirements_dev.txt + python3 -m pip install --upgrade pip + python3 -m pip install -r requirements_dev.txt - name: Install gnu make on macos if: startsWith(matrix.os, 'macos') run: | brew install make echo "${{ matrix.brew }}/opt/make/libexec/gnubin" >> $GITHUB_PATH + - name: Fetch CVC5 + run: | + util/fetch_cvc5.py 1.2.0 ${{ matrix.cvc5-plat }} + echo "$GITHUB_WORKSPACE" >> $GITHUB_PATH - name: Executing unit tests run: | make unit-tests diff --git a/.github/workflows/docs.yml b/.github/workflows/docs.yml index d0a4b5eb..0a73264b 100644 --- a/.github/workflows/docs.yml +++ b/.github/workflows/docs.yml @@ -32,11 +32,6 @@ jobs: uses: actions/checkout@v4 with: fetch-depth: 0 - - uses: supplypike/setup-bin@v4 - with: - uri: 'https://github.com/cvc5/cvc5/releases/download/cvc5-1.0.8/cvc5-Linux' - name: 'cvc5' - version: '1.0.8' - name: Set up Python 3.9 uses: actions/setup-python@v5 with: @@ -48,6 +43,13 @@ jobs: pip install bmw-lobster-core bmw-lobster-tool-python pip install --no-deps bmw-lobster-tool-trlc sudo apt-get install -y graphviz + - name: Fetch CVC5 + run: | + util/fetch_cvc5.py 1.2.0 linux + echo "$GITHUB_WORKSPACE" >> $GITHUB_PATH + - name: Test CVC5 + run: | + cvc5 --version - name: Generate docs run: | make docs diff --git a/.github/workflows/package.yml b/.github/workflows/package.yml index c5f5a387..6e73964c 100644 --- a/.github/workflows/package.yml +++ b/.github/workflows/package.yml @@ -15,18 +15,18 @@ jobs: steps: - uses: actions/checkout@v4 - name: Set up Python 3.9 - uses: actions/setup-python@v4 + uses: actions/setup-python@v5 with: python-version: "3.9" - name: Install dependencies run: | - python -m pip install --upgrade pip - python -m pip install --upgrade setuptools wheel requests + python3 -m pip install --upgrade pip + python3 -m pip install build - name: run: | make package - name: Archive wheel files - uses: actions/upload-artifact@v3 + uses: actions/upload-artifact@v4 with: name: wheels path: "dist/trlc-*.whl" @@ -40,7 +40,7 @@ jobs: id-token: write steps: - name: Download wheel files - uses: actions/download-artifact@v3 + uses: actions/download-artifact@v4 with: name: wheels path: dist diff --git a/.gitignore b/.gitignore index d90d539c..56e6ac6b 100644 --- a/.gitignore +++ b/.gitignore @@ -19,3 +19,7 @@ dist # Build-System ignores bazel-* + +# Special ignores for CI +cvc5 +cvc5.exe diff --git a/CHANGELOG.md b/CHANGELOG.md index 32dbb5ec..7faf77ac 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -25,7 +25,12 @@ generated in the following situations: ## Changelog -### 2.0.0-dev +### 2.0.1-dev + +* [TRLC] Fix an UnboundLocalError when missing a term + in an expression. + +### 2.0.0 This new major release includes a number of incompatible changes. These have been tagged in the changelog. @@ -52,6 +57,10 @@ changes. These have been tagged in the changelog. backwards incompatible change as it may invalidate some previously valid `.trlc` or `.rsl` files. +* [TRLC] The `--verify` command is now supported on Windows without + the use of an external `cvc5` install, now that the Python package + for CVC5 is also available on Windows. + * [TRLC, LRM] New builtin function `oneof`. This can be used to test if precisely one of a number of parameters is true. For example: diff --git a/MODULE.bazel b/MODULE.bazel index fb4a054b..30d06461 100644 --- a/MODULE.bazel +++ b/MODULE.bazel @@ -33,23 +33,23 @@ http_archive = use_repo_rule("@bazel_tools//tools/build_defs/repo:http.bzl", "ht http_archive( name = "cvc5_linux", build_file = "@trlc//:cvc5.BUILD", - sha256 = "cf291aef67da8eaa8d425a51f67f3f72f36db8b1040655dc799b64e3d69e6086", - strip_prefix = "cvc5-Linux-static", - url = "https://github.com/cvc5/cvc5/releases/download/cvc5-1.1.2/cvc5-Linux-static.zip", + sha256 = "ab9344e2dddda794669c888a3afcd99f25f2627e1d426bd7d08ecb267361b331", + strip_prefix = "cvc5-Linux-x86_64-static-gpl", + url = "https://github.com/cvc5/cvc5/releases/download/cvc5-1.2.0/cvc5-Linux-x86_64-static-gpl.zip", ) http_archive( name = "cvc5_mac", build_file = "@trlc//:cvc5.BUILD", - sha256 = "561a5ee82416441fa616c6f416ecaae2fa2dfc06dc81c2c6cc8dcfb31936e326", - strip_prefix = "cvc5-macOS-static", - url = "https://github.com/cvc5/cvc5/releases/download/cvc5-1.1.2/cvc5-macOS-static.zip", + sha256 = "2b983ca743ef1327b51408bf8ba6c08c97beaadde2c3968da701ca16bb1e3740", + strip_prefix = "cvc5-macOS-arm64-static-gpl", + url = "https://github.com/cvc5/cvc5/releases/download/cvc5-1.2.0/cvc5-macOS-arm64-static-gpl.zip", ) http_archive( name = "cvc5_windows", build_file = "@trlc//:cvc5.BUILD", - sha256 = "f06715b796020c810b2713e6df3969dae99d38c24d2a6eac225a029fc70fe1ee", - strip_prefix = "cvc5-Win64-static", - url = "https://github.com/cvc5/cvc5/releases/download/cvc5-1.1.2/cvc5-Win64-static.zip", + sha256 = "256f4af3f4181e770801df436852cb3c76c86dbf9b69a47064d7f8d5bc0ee1d2", + strip_prefix = "cvc5-Win64-x86_64-static", + url = "https://github.com/cvc5/cvc5/releases/download/cvc5-1.2.0/cvc5-Win64-x86_64-static.zip", ) diff --git a/Makefile b/Makefile index 14b752cb..062cc6e6 100644 --- a/Makefile +++ b/Makefile @@ -56,8 +56,7 @@ docs: package: @git clean -xdf - @python3 setup.py sdist bdist_wheel - @python3 setup.py bdist_wheel -p manylinux2014_x86_64 + @python3 -m build upload-main: package python3 -m twine upload --repository pypi dist/* @@ -67,7 +66,7 @@ remove-dev: github-release: git push - python3 -m util.github-release + python3 -m util.github_release bump: python3 -m util.bump_version_post_release diff --git a/documentation/LRM.md b/documentation/LRM.md index 085e8129..fec560bb 100644 --- a/documentation/LRM.md +++ b/documentation/LRM.md @@ -1,7 +1,7 @@ # TRLC LRM -* [Version 3.0](https://bmw-software-engineering.github.io/trlc/lrm.html) (Development) -* [Version 2.9](https://bmw-software-engineering.github.io/trlc/lrm-2.9.html) (Current Stable) +* [Version 3.0](https://bmw-software-engineering.github.io/trlc/lrm-3.0.html) (Current Stable) +* [Version 2.9](https://bmw-software-engineering.github.io/trlc/lrm-2.9.html) * [Version 2.8](https://bmw-software-engineering.github.io/trlc/lrm-2.8.html) * [Version 2.7](https://bmw-software-engineering.github.io/trlc/lrm-2.7.html) * [Version 2.6](https://bmw-software-engineering.github.io/trlc/lrm-2.6.html) diff --git a/documentation/TUTORIAL-INSTALL.md b/documentation/TUTORIAL-INSTALL.md index ad7c2734..2b4f5596 100644 --- a/documentation/TUTORIAL-INSTALL.md +++ b/documentation/TUTORIAL-INSTALL.md @@ -10,9 +10,9 @@ The easiest way to install the tools is through PyPI: $ pip3 install --user trlc ``` -There are currently one required dependencies (PyVCG which should be +There is currently only one required dependency (PyVCG which should be installed automatically), all you need is a moderatly recent Python -3.8 / 3.9 / 3.10 / 3.11. +3.8 / 3.9 / 3.10 / 3.11 / 3.12. Don't forget to adjust your `PATH` so that `.local/bin` (or the equivalent on Windows) is on it; so that the `trlc` executable can be diff --git a/documentation/TUTORIAL-LINT.md b/documentation/TUTORIAL-LINT.md index ed1a602e..86c55931 100644 --- a/documentation/TUTORIAL-LINT.md +++ b/documentation/TUTORIAL-LINT.md @@ -10,16 +10,14 @@ deployed and used. This is enabled by default, but you can turn these off with the `--no-lint` option. To enable more detailed checks you can also use the `--verify` -feature, but please note that this is only available on Linux, and -requires you to have installed the optional dependency -[CVC5](https://pypi.org/project/cvc5). +feature. ```bash $ trlc --verify DIRECTORIES_OR_FILES ``` -If you are on Windows or Linux, you can also download the CVC5 -executables and ask TRLC to use them directly: +If the API for CVC5 isn't avialable on your platform, then you can +also download the CVC5 executables and ask TRLC to use them directly: ```bash $ trlc --verify --use-cvc5-binary=path/to/cvc5.exe DIRECTORIES_OR_FILES diff --git a/documentation/TUTORIAL-PACKAGE.md b/documentation/TUTORIAL-PACKAGE.md index f26a971c..c01b4e60 100644 --- a/documentation/TUTORIAL-PACKAGE.md +++ b/documentation/TUTORIAL-PACKAGE.md @@ -97,7 +97,7 @@ section "Functional Requirements" { Requirement fuel { functional = true integrity = QM - description = "the car shall not use fossil fuesl" + description = "the car shall not use fossil fuels" } Requirement colour { functional = true diff --git a/language-reference-manual/lrm.trlc b/language-reference-manual/lrm.trlc index 1a74e624..3b8cb68d 100644 --- a/language-reference-manual/lrm.trlc +++ b/language-reference-manual/lrm.trlc @@ -1519,8 +1519,8 @@ section "Quantification" { Grammar Quantified_Expression { bnf = ''' quantified_expression ::= - quantifier IDENTIFIER_name 'in' IDENTIFIER_component_name '=>' - expression_PREDICATE + '(' quantifier IDENTIFIER_name 'in' IDENTIFIER_component_name '=>' + expression_PREDICATE ')' quantifier ::= 'forall' | 'exists' ''' @@ -1546,14 +1546,6 @@ section "Quantification" { quantified expression is Boolean.''' } - Dynamic_Semantics Quantification_Evaluation { - text = '''During evaluation of the quantified expression, each element - of the array is evaluated in sequence and its - value is bound to the declared name. The - predicated is then evaluated with this - binding.''' - } - Dynamic_Semantics Universal_Quantification_Semantics { text = '''For universal *(forall)* quantification the final value is true iff all predicates evaluate to @@ -1569,6 +1561,14 @@ section "Quantification" { vacuously false.)*''' } + Note Quantification_Evaluation { + text = '''During evaluation of the quantified expression, each element + of the array is evaluated in sequence and its + value is bound to the declared name. The + predicated is then evaluated with this + binding.''' + } + Recommendation Quantification_Short_Circuit_Evaluation { text = '''In general Quantification is equivalent to a chain of `and` or `or` expressions, however it is left @@ -1580,6 +1580,7 @@ section "Quantification" { '''For static analysis or linting, use non-short-circuit semantics, as using a quantifier as a complex guard is not reasonable.'''] + untraced_reason = "Non-normative text" } } @@ -1680,9 +1681,11 @@ section "Record object declarations" { | STRING | qualified_name_RECORD_OBJECT | qualified_name_ENUM_TYPE '.' IDENTIFIER_enumeration_literal - | '[' [ value { ',' value } ] ']' + | array_aggregate | tuple_aggregate + array_aggregate ::= '[' [ value { ',' value } ] ']' + tuple_aggregate ::= '(' value { ',' value } ')' | value { separator_symbol value } ''' @@ -1776,18 +1779,18 @@ section "Record object declarations" { references to R.)*''' } - Static_Semantics Tuple_Checks { + Note Tuple_Checks { text = '''The checks for a tuple aggregate are immediately evaluated after the last value is parsed.''' } - Name_Resolution Sufficiently_Distinct { + /*Name_Resolution Sufficiently_Distinct { text = '''When declaring record objects there are wider rules that indicate name clashes. Specifically a record may not be declared if its "simplified name" clashes with any other "simplified name". A "simplified name" is the name converted to - lowercase and all underscored removed.''' + lowercase and all underscores removed.''' } Note Simplified_Name_Example { @@ -1801,7 +1804,7 @@ section "Record object declarations" { Note Simplified_Name_Rationale { text = '''The purpose of this rule is to avoid requirements that have hard to distinguish names.''' - } + }*/ Recommendation Record_Object_API { text = '''When exposing record instances through the API, it is diff --git a/requirements.txt b/requirements.txt index b4b45cef..036eb7fc 100644 --- a/requirements.txt +++ b/requirements.txt @@ -1,2 +1,2 @@ -pyvcg==1.0.6 -cvc5>=1.1.1; sys.platform == "linux" or sys.platform == "darwin" +pyvcg==1.0.7 +cvc5>=1.2.0 diff --git a/requirements_dev.txt b/requirements_dev.txt index 9b2fce1c..85117e90 100644 --- a/requirements_dev.txt +++ b/requirements_dev.txt @@ -3,3 +3,4 @@ pycodestyle==2.12.0 pylint==3.2.4 coverage>=7.2 sphinx>=7.0 +build>=1.2.0 diff --git a/setup.py b/setup.py index 66f604e1..758b94d4 100644 --- a/setup.py +++ b/setup.py @@ -30,14 +30,6 @@ "Source Code" : version.CODE_URL, } -required_packages = [] -python_required = ">=3.8, <4" -if "--plat-name" in sys.argv or "-p" in sys.argv: - required_packages.append("PyVCG[api]==1.0.6") - python_required = ">=3.8, <3.12" -else: - required_packages.append("PyVCG==1.0.6") - setuptools.setup( name="trlc", version=version.TRLC_VERSION, @@ -50,8 +42,8 @@ project_urls=project_urls, license="GNU General Public License v3", packages=setuptools.find_packages(), - install_requires=required_packages, - python_requires=python_required, + install_requires="PyVCG[api]==1.0.7", + python_requires=">=3.8, <3.13", classifiers=[ "Development Status :: 5 - Production/Stable", "Environment :: Console", @@ -61,8 +53,6 @@ "Topic :: Software Development", ], entry_points={ - "console_scripts": [ - "trlc = trlc.trlc:main", - ], + "console_scripts": ["trlc = trlc.trlc:main"], }, ) diff --git a/tests-system/rbt-builtin-functions/foo.rsl b/tests-system/rbt-builtin-functions-1/foo.rsl similarity index 100% rename from tests-system/rbt-builtin-functions/foo.rsl rename to tests-system/rbt-builtin-functions-1/foo.rsl diff --git a/tests-system/rbt-builtin-functions/foo.trlc b/tests-system/rbt-builtin-functions-1/foo.trlc similarity index 100% rename from tests-system/rbt-builtin-functions/foo.trlc rename to tests-system/rbt-builtin-functions-1/foo.trlc diff --git a/tests-system/rbt-builtin-functions-1/output b/tests-system/rbt-builtin-functions-1/output new file mode 100644 index 00000000..d0a7f840 --- /dev/null +++ b/tests-system/rbt-builtin-functions-1/output @@ -0,0 +1,7 @@ +len("foo") == 3, warning "len is broken" + ^^ rbt-builtin-functions-1/foo.rsl:6: issue: expression is always true [vcg-always-true] +startswith("foo", "f"), warning "startswith is broken" +^^^^^^^^^^ rbt-builtin-functions-1/foo.rsl:7: issue: expression is always true [vcg-always-true] +endswith("foo", "o"), warning "endswith is broken" +^^^^^^^^ rbt-builtin-functions-1/foo.rsl:8: issue: expression is always true [vcg-always-true] +Processed 1 model and 1 requirement file and found 3 warnings diff --git a/tests-system/rbt-builtin-functions/output.brief b/tests-system/rbt-builtin-functions-1/output.brief similarity index 100% rename from tests-system/rbt-builtin-functions/output.brief rename to tests-system/rbt-builtin-functions-1/output.brief diff --git a/tests-system/rbt-builtin-functions/output.json b/tests-system/rbt-builtin-functions-1/output.json similarity index 100% rename from tests-system/rbt-builtin-functions/output.json rename to tests-system/rbt-builtin-functions-1/output.json diff --git a/tests-system/rbt-builtin-functions-1/output.smtlib b/tests-system/rbt-builtin-functions-1/output.smtlib new file mode 100644 index 00000000..d0a7f840 --- /dev/null +++ b/tests-system/rbt-builtin-functions-1/output.smtlib @@ -0,0 +1,7 @@ +len("foo") == 3, warning "len is broken" + ^^ rbt-builtin-functions-1/foo.rsl:6: issue: expression is always true [vcg-always-true] +startswith("foo", "f"), warning "startswith is broken" +^^^^^^^^^^ rbt-builtin-functions-1/foo.rsl:7: issue: expression is always true [vcg-always-true] +endswith("foo", "o"), warning "endswith is broken" +^^^^^^^^ rbt-builtin-functions-1/foo.rsl:8: issue: expression is always true [vcg-always-true] +Processed 1 model and 1 requirement file and found 3 warnings diff --git a/tests-system/rbt-builtin-functions-2/foo.rsl b/tests-system/rbt-builtin-functions-2/foo.rsl new file mode 100644 index 00000000..8b88f46f --- /dev/null +++ b/tests-system/rbt-builtin-functions-2/foo.rsl @@ -0,0 +1,11 @@ +package Foo + +type Requirement { + name String + description String + +} + +checks Requirement { + name != , warning "bar" +} diff --git a/tests-system/rbt-builtin-functions-2/output b/tests-system/rbt-builtin-functions-2/output new file mode 100644 index 00000000..47cd8608 --- /dev/null +++ b/tests-system/rbt-builtin-functions-2/output @@ -0,0 +1,3 @@ +name != , warning "bar" + ^ rbt-builtin-functions-2/foo.rsl:10: error: expected identifier, encountered comma ',' instead +Processed 1 model and 0 requirement files and found 1 error diff --git a/tests-system/rbt-builtin-functions-2/output.brief b/tests-system/rbt-builtin-functions-2/output.brief new file mode 100644 index 00000000..195694fe --- /dev/null +++ b/tests-system/rbt-builtin-functions-2/output.brief @@ -0,0 +1 @@ +rbt-builtin-functions-2/foo.rsl:10:13: trlc error: expected identifier, encountered comma ',' instead diff --git a/tests-system/rbt-builtin-functions-2/output.json b/tests-system/rbt-builtin-functions-2/output.json new file mode 100644 index 00000000..47cd8608 --- /dev/null +++ b/tests-system/rbt-builtin-functions-2/output.json @@ -0,0 +1,3 @@ +name != , warning "bar" + ^ rbt-builtin-functions-2/foo.rsl:10: error: expected identifier, encountered comma ',' instead +Processed 1 model and 0 requirement files and found 1 error diff --git a/tests-system/rbt-builtin-functions-2/output.smtlib b/tests-system/rbt-builtin-functions-2/output.smtlib new file mode 100644 index 00000000..47cd8608 --- /dev/null +++ b/tests-system/rbt-builtin-functions-2/output.smtlib @@ -0,0 +1,3 @@ +name != , warning "bar" + ^ rbt-builtin-functions-2/foo.rsl:10: error: expected identifier, encountered comma ',' instead +Processed 1 model and 0 requirement files and found 1 error diff --git a/tests-system/rbt-builtin-functions/output b/tests-system/rbt-builtin-functions/output deleted file mode 100644 index 9df7a0b2..00000000 --- a/tests-system/rbt-builtin-functions/output +++ /dev/null @@ -1,7 +0,0 @@ -len("foo") == 3, warning "len is broken" - ^^ rbt-builtin-functions/foo.rsl:6: issue: expression is always true [vcg-always-true] -startswith("foo", "f"), warning "startswith is broken" -^^^^^^^^^^ rbt-builtin-functions/foo.rsl:7: issue: expression is always true [vcg-always-true] -endswith("foo", "o"), warning "endswith is broken" -^^^^^^^^ rbt-builtin-functions/foo.rsl:8: issue: expression is always true [vcg-always-true] -Processed 1 model and 1 requirement file and found 3 warnings diff --git a/tests-system/rbt-builtin-functions/output.smtlib b/tests-system/rbt-builtin-functions/output.smtlib deleted file mode 100644 index 9df7a0b2..00000000 --- a/tests-system/rbt-builtin-functions/output.smtlib +++ /dev/null @@ -1,7 +0,0 @@ -len("foo") == 3, warning "len is broken" - ^^ rbt-builtin-functions/foo.rsl:6: issue: expression is always true [vcg-always-true] -startswith("foo", "f"), warning "startswith is broken" -^^^^^^^^^^ rbt-builtin-functions/foo.rsl:7: issue: expression is always true [vcg-always-true] -endswith("foo", "o"), warning "endswith is broken" -^^^^^^^^ rbt-builtin-functions/foo.rsl:8: issue: expression is always true [vcg-always-true] -Processed 1 model and 1 requirement file and found 3 warnings diff --git a/tests-system/rbt-evaluation-of-checks/foo.rsl b/tests-system/rbt-evaluation-of-checks/foo.rsl new file mode 100644 index 00000000..7d5d8019 --- /dev/null +++ b/tests-system/rbt-evaluation-of-checks/foo.rsl @@ -0,0 +1,11 @@ +package Foo + +type T { + a Integer + b Integer + freeze b = 2 +} + +checks T { + b > a, warning "a should be less than b" +} diff --git a/tests-system/rbt-evaluation-of-checks/foo.trlc b/tests-system/rbt-evaluation-of-checks/foo.trlc new file mode 100644 index 00000000..cafe35db --- /dev/null +++ b/tests-system/rbt-evaluation-of-checks/foo.trlc @@ -0,0 +1,5 @@ +package Foo + +T Bar { + a = 3 +} diff --git a/tests-system/rbt-evaluation-of-checks/output b/tests-system/rbt-evaluation-of-checks/output new file mode 100644 index 00000000..8763ecbf --- /dev/null +++ b/tests-system/rbt-evaluation-of-checks/output @@ -0,0 +1,3 @@ +T Bar { + ^^^ rbt-evaluation-of-checks/foo.trlc:3: check warning: a should be less than b +Processed 1 model and 1 requirement file and found 1 warning diff --git a/tests-system/rbt-evaluation-of-checks/output.brief b/tests-system/rbt-evaluation-of-checks/output.brief new file mode 100644 index 00000000..93e2d93c --- /dev/null +++ b/tests-system/rbt-evaluation-of-checks/output.brief @@ -0,0 +1 @@ +rbt-evaluation-of-checks/foo.trlc:3:3: trlc check warning: a should be less than b diff --git a/tests-system/rbt-evaluation-of-checks/output.json b/tests-system/rbt-evaluation-of-checks/output.json new file mode 100644 index 00000000..ea73613a --- /dev/null +++ b/tests-system/rbt-evaluation-of-checks/output.json @@ -0,0 +1,9 @@ +T Bar { + ^^^ rbt-evaluation-of-checks/foo.trlc:3: check warning: a should be less than b +{ + "Bar": { + "a": 3, + "b": 2 + } +} +Processed 1 model and 1 requirement file and found 1 warning diff --git a/tests-system/rbt-evaluation-of-checks/output.smtlib b/tests-system/rbt-evaluation-of-checks/output.smtlib new file mode 100644 index 00000000..8763ecbf --- /dev/null +++ b/tests-system/rbt-evaluation-of-checks/output.smtlib @@ -0,0 +1,3 @@ +T Bar { + ^^^ rbt-evaluation-of-checks/foo.trlc:3: check warning: a should be less than b +Processed 1 model and 1 requirement file and found 1 warning diff --git a/tests-system/rbt-existential-quantification-semantics/foo.rsl b/tests-system/rbt-existential-quantification-semantics/foo.rsl new file mode 100644 index 00000000..0a87a985 --- /dev/null +++ b/tests-system/rbt-existential-quantification-semantics/foo.rsl @@ -0,0 +1,9 @@ +package Foo + +type T { + a Integer[0..*] +} + +checks T { + (exists item in a => item == 7), warning "there is no 7 in a" +} diff --git a/tests-system/rbt-existential-quantification-semantics/foo.trlc b/tests-system/rbt-existential-quantification-semantics/foo.trlc new file mode 100644 index 00000000..982fa64f --- /dev/null +++ b/tests-system/rbt-existential-quantification-semantics/foo.trlc @@ -0,0 +1,9 @@ +package Foo + +T Bar { + a = [7] +} + +T Kitten { + a = [] +} diff --git a/tests-system/rbt-existential-quantification-semantics/output b/tests-system/rbt-existential-quantification-semantics/output new file mode 100644 index 00000000..26da7f58 --- /dev/null +++ b/tests-system/rbt-existential-quantification-semantics/output @@ -0,0 +1,3 @@ +T Kitten { + ^^^^^^ rbt-existential-quantification-semantics/foo.trlc:7: check warning: there is no 7 in a +Processed 1 model and 1 requirement file and found 1 warning diff --git a/tests-system/rbt-existential-quantification-semantics/output.brief b/tests-system/rbt-existential-quantification-semantics/output.brief new file mode 100644 index 00000000..0f28ec1b --- /dev/null +++ b/tests-system/rbt-existential-quantification-semantics/output.brief @@ -0,0 +1 @@ +rbt-existential-quantification-semantics/foo.trlc:7:3: trlc check warning: there is no 7 in a diff --git a/tests-system/rbt-existential-quantification-semantics/output.json b/tests-system/rbt-existential-quantification-semantics/output.json new file mode 100644 index 00000000..fa198fd1 --- /dev/null +++ b/tests-system/rbt-existential-quantification-semantics/output.json @@ -0,0 +1,13 @@ +T Kitten { + ^^^^^^ rbt-existential-quantification-semantics/foo.trlc:7: check warning: there is no 7 in a +{ + "Bar": { + "a": [ + 7 + ] + }, + "Kitten": { + "a": [] + } +} +Processed 1 model and 1 requirement file and found 1 warning diff --git a/tests-system/rbt-existential-quantification-semantics/output.smtlib b/tests-system/rbt-existential-quantification-semantics/output.smtlib new file mode 100644 index 00000000..26da7f58 --- /dev/null +++ b/tests-system/rbt-existential-quantification-semantics/output.smtlib @@ -0,0 +1,3 @@ +T Kitten { + ^^^^^^ rbt-existential-quantification-semantics/foo.trlc:7: check warning: there is no 7 in a +Processed 1 model and 1 requirement file and found 1 warning diff --git a/tests-system/rbt-late-reference-checking/foo.rsl b/tests-system/rbt-late-reference-checking/foo.rsl new file mode 100644 index 00000000..0ffa46c3 --- /dev/null +++ b/tests-system/rbt-late-reference-checking/foo.rsl @@ -0,0 +1,6 @@ +package Foo + +type T { + a Integer + ref T +} diff --git a/tests-system/rbt-late-reference-checking/foo.trlc b/tests-system/rbt-late-reference-checking/foo.trlc new file mode 100644 index 00000000..16ac11f7 --- /dev/null +++ b/tests-system/rbt-late-reference-checking/foo.trlc @@ -0,0 +1,11 @@ +package Foo + +T Bar { + a = 1 + ref = Kitten +} + +T Kitten { + a = 2 + ref = Potato +} diff --git a/tests-system/rbt-late-reference-checking/output b/tests-system/rbt-late-reference-checking/output new file mode 100644 index 00000000..2c556c89 --- /dev/null +++ b/tests-system/rbt-late-reference-checking/output @@ -0,0 +1,3 @@ +ref = Potato + ^^^^^^ rbt-late-reference-checking/foo.trlc:10: error: unknown symbol Potato +Processed 1 model and 1 requirement file and found 1 error diff --git a/tests-system/rbt-late-reference-checking/output.brief b/tests-system/rbt-late-reference-checking/output.brief new file mode 100644 index 00000000..4ed238c8 --- /dev/null +++ b/tests-system/rbt-late-reference-checking/output.brief @@ -0,0 +1 @@ +rbt-late-reference-checking/foo.trlc:10:11: trlc error: unknown symbol Potato diff --git a/tests-system/rbt-late-reference-checking/output.json b/tests-system/rbt-late-reference-checking/output.json new file mode 100644 index 00000000..2c556c89 --- /dev/null +++ b/tests-system/rbt-late-reference-checking/output.json @@ -0,0 +1,3 @@ +ref = Potato + ^^^^^^ rbt-late-reference-checking/foo.trlc:10: error: unknown symbol Potato +Processed 1 model and 1 requirement file and found 1 error diff --git a/tests-system/rbt-late-reference-checking/output.smtlib b/tests-system/rbt-late-reference-checking/output.smtlib new file mode 100644 index 00000000..2c556c89 --- /dev/null +++ b/tests-system/rbt-late-reference-checking/output.smtlib @@ -0,0 +1,3 @@ +ref = Potato + ^^^^^^ rbt-late-reference-checking/foo.trlc:10: error: unknown symbol Potato +Processed 1 model and 1 requirement file and found 1 error diff --git a/tests-system/rbt-mandatory-components/foo.rsl b/tests-system/rbt-mandatory-components/foo.rsl new file mode 100644 index 00000000..6e235c4c --- /dev/null +++ b/tests-system/rbt-mandatory-components/foo.rsl @@ -0,0 +1,7 @@ +package Foo + +type T { + a Integer + b Integer + c optional Integer +} diff --git a/tests-system/rbt-mandatory-components/foo.trlc b/tests-system/rbt-mandatory-components/foo.trlc new file mode 100644 index 00000000..2f19e984 --- /dev/null +++ b/tests-system/rbt-mandatory-components/foo.trlc @@ -0,0 +1,6 @@ +package Foo + +T Bar { + a = 1 + c = 3 +} diff --git a/tests-system/rbt-mandatory-components/output b/tests-system/rbt-mandatory-components/output new file mode 100644 index 00000000..b01f5903 --- /dev/null +++ b/tests-system/rbt-mandatory-components/output @@ -0,0 +1,3 @@ +T Bar { + ^^^ rbt-mandatory-components/foo.trlc:3: error: required component b (see foo.rsl:5) is not defined +Processed 1 model and 1 requirement file and found 1 error diff --git a/tests-system/rbt-mandatory-components/output.brief b/tests-system/rbt-mandatory-components/output.brief new file mode 100644 index 00000000..9b77cfc4 --- /dev/null +++ b/tests-system/rbt-mandatory-components/output.brief @@ -0,0 +1 @@ +rbt-mandatory-components/foo.trlc:3:3: trlc error: required component b (see foo.rsl:5) is not defined diff --git a/tests-system/rbt-mandatory-components/output.json b/tests-system/rbt-mandatory-components/output.json new file mode 100644 index 00000000..b01f5903 --- /dev/null +++ b/tests-system/rbt-mandatory-components/output.json @@ -0,0 +1,3 @@ +T Bar { + ^^^ rbt-mandatory-components/foo.trlc:3: error: required component b (see foo.rsl:5) is not defined +Processed 1 model and 1 requirement file and found 1 error diff --git a/tests-system/rbt-mandatory-components/output.smtlib b/tests-system/rbt-mandatory-components/output.smtlib new file mode 100644 index 00000000..b01f5903 --- /dev/null +++ b/tests-system/rbt-mandatory-components/output.smtlib @@ -0,0 +1,3 @@ +T Bar { + ^^^ rbt-mandatory-components/foo.trlc:3: error: required component b (see foo.rsl:5) is not defined +Processed 1 model and 1 requirement file and found 1 error diff --git a/tests-system/rbt-matching-value-types/foo.rsl b/tests-system/rbt-matching-value-types/foo.rsl new file mode 100644 index 00000000..9a9aea0f --- /dev/null +++ b/tests-system/rbt-matching-value-types/foo.rsl @@ -0,0 +1,6 @@ +package Foo + +type T { + a Integer + b String[1..*] +} diff --git a/tests-system/rbt-matching-value-types/foo.trlc b/tests-system/rbt-matching-value-types/foo.trlc new file mode 100644 index 00000000..f520f7f5 --- /dev/null +++ b/tests-system/rbt-matching-value-types/foo.trlc @@ -0,0 +1,11 @@ +package Foo + +T Bar { + a = 1.0 + b = ["hello", "world"] +} + +T Kitten { + a = 1 + b = [1, 2, 3] +} diff --git a/tests-system/rbt-matching-value-types/output b/tests-system/rbt-matching-value-types/output new file mode 100644 index 00000000..175910ac --- /dev/null +++ b/tests-system/rbt-matching-value-types/output @@ -0,0 +1,5 @@ +a = 1.0 + ^^^ rbt-matching-value-types/foo.trlc:4: error: expected integer literal, encountered decimal literal instead +b = [1, 2, 3] + ^ rbt-matching-value-types/foo.trlc:10: error: expected string literal, encountered integer literal instead +Processed 1 model and 1 requirement file and found 2 errors diff --git a/tests-system/rbt-matching-value-types/output.brief b/tests-system/rbt-matching-value-types/output.brief new file mode 100644 index 00000000..65629c6b --- /dev/null +++ b/tests-system/rbt-matching-value-types/output.brief @@ -0,0 +1,2 @@ +rbt-matching-value-types/foo.trlc:4:9: trlc error: expected integer literal, encountered decimal literal instead +rbt-matching-value-types/foo.trlc:10:10: trlc error: expected string literal, encountered integer literal instead diff --git a/tests-system/rbt-matching-value-types/output.json b/tests-system/rbt-matching-value-types/output.json new file mode 100644 index 00000000..175910ac --- /dev/null +++ b/tests-system/rbt-matching-value-types/output.json @@ -0,0 +1,5 @@ +a = 1.0 + ^^^ rbt-matching-value-types/foo.trlc:4: error: expected integer literal, encountered decimal literal instead +b = [1, 2, 3] + ^ rbt-matching-value-types/foo.trlc:10: error: expected string literal, encountered integer literal instead +Processed 1 model and 1 requirement file and found 2 errors diff --git a/tests-system/rbt-matching-value-types/output.smtlib b/tests-system/rbt-matching-value-types/output.smtlib new file mode 100644 index 00000000..175910ac --- /dev/null +++ b/tests-system/rbt-matching-value-types/output.smtlib @@ -0,0 +1,5 @@ +a = 1.0 + ^^^ rbt-matching-value-types/foo.trlc:4: error: expected integer literal, encountered decimal literal instead +b = [1, 2, 3] + ^ rbt-matching-value-types/foo.trlc:10: error: expected string literal, encountered integer literal instead +Processed 1 model and 1 requirement file and found 2 errors diff --git a/tests-system/rbt-quantification-naming-scope/foo.rsl b/tests-system/rbt-quantification-naming-scope/foo.rsl new file mode 100644 index 00000000..c8ba9312 --- /dev/null +++ b/tests-system/rbt-quantification-naming-scope/foo.rsl @@ -0,0 +1,11 @@ +package Foo + +type T { + a Integer[1..10] +} + +checks T { + (forall item in a => item > 0), warning "All items must be positive" + (forall item in a => item < 10), warning "All items must be less than 10" + (forall a in a => a != 7), warning "No sevens allowed" +} diff --git a/tests-system/rbt-quantification-naming-scope/output b/tests-system/rbt-quantification-naming-scope/output new file mode 100644 index 00000000..2e42ad4d --- /dev/null +++ b/tests-system/rbt-quantification-naming-scope/output @@ -0,0 +1,3 @@ +(forall a in a => a != 7), warning "No sevens allowed" + ^ rbt-quantification-naming-scope/foo.rsl:10: error: shadows Composite_Component a from foo.rsl:4 +Processed 1 model and 0 requirement files and found 1 error diff --git a/tests-system/rbt-quantification-naming-scope/output.brief b/tests-system/rbt-quantification-naming-scope/output.brief new file mode 100644 index 00000000..f3a79207 --- /dev/null +++ b/tests-system/rbt-quantification-naming-scope/output.brief @@ -0,0 +1 @@ +rbt-quantification-naming-scope/foo.rsl:10:13: trlc error: shadows Composite_Component a from foo.rsl:4 diff --git a/tests-system/rbt-quantification-naming-scope/output.json b/tests-system/rbt-quantification-naming-scope/output.json new file mode 100644 index 00000000..2e42ad4d --- /dev/null +++ b/tests-system/rbt-quantification-naming-scope/output.json @@ -0,0 +1,3 @@ +(forall a in a => a != 7), warning "No sevens allowed" + ^ rbt-quantification-naming-scope/foo.rsl:10: error: shadows Composite_Component a from foo.rsl:4 +Processed 1 model and 0 requirement files and found 1 error diff --git a/tests-system/rbt-quantification-naming-scope/output.smtlib b/tests-system/rbt-quantification-naming-scope/output.smtlib new file mode 100644 index 00000000..2e42ad4d --- /dev/null +++ b/tests-system/rbt-quantification-naming-scope/output.smtlib @@ -0,0 +1,3 @@ +(forall a in a => a != 7), warning "No sevens allowed" + ^ rbt-quantification-naming-scope/foo.rsl:10: error: shadows Composite_Component a from foo.rsl:4 +Processed 1 model and 0 requirement files and found 1 error diff --git a/tests-system/rbt-quantification-object-1/foo.rsl b/tests-system/rbt-quantification-object-1/foo.rsl new file mode 100644 index 00000000..6d5ff00d --- /dev/null +++ b/tests-system/rbt-quantification-object-1/foo.rsl @@ -0,0 +1,9 @@ +package Foo + +type Potato { + a String +} + +checks Potato { + (forall char in a => char != "a"), warning "a should not contain the letter a" +} diff --git a/tests-system/rbt-quantification-object-1/output b/tests-system/rbt-quantification-object-1/output new file mode 100644 index 00000000..f1014cb8 --- /dev/null +++ b/tests-system/rbt-quantification-object-1/output @@ -0,0 +1,3 @@ +(forall char in a => char != "a"), warning "a should not contain the letter a" + ^ rbt-quantification-object-1/foo.rsl:8: error: you can only quantify over arrays +Processed 1 model and 0 requirement files and found 1 error diff --git a/tests-system/rbt-quantification-object-1/output.brief b/tests-system/rbt-quantification-object-1/output.brief new file mode 100644 index 00000000..979f63e3 --- /dev/null +++ b/tests-system/rbt-quantification-object-1/output.brief @@ -0,0 +1 @@ +rbt-quantification-object-1/foo.rsl:8:21: trlc error: you can only quantify over arrays diff --git a/tests-system/rbt-quantification-object-1/output.json b/tests-system/rbt-quantification-object-1/output.json new file mode 100644 index 00000000..f1014cb8 --- /dev/null +++ b/tests-system/rbt-quantification-object-1/output.json @@ -0,0 +1,3 @@ +(forall char in a => char != "a"), warning "a should not contain the letter a" + ^ rbt-quantification-object-1/foo.rsl:8: error: you can only quantify over arrays +Processed 1 model and 0 requirement files and found 1 error diff --git a/tests-system/rbt-quantification-object-1/output.smtlib b/tests-system/rbt-quantification-object-1/output.smtlib new file mode 100644 index 00000000..f1014cb8 --- /dev/null +++ b/tests-system/rbt-quantification-object-1/output.smtlib @@ -0,0 +1,3 @@ +(forall char in a => char != "a"), warning "a should not contain the letter a" + ^ rbt-quantification-object-1/foo.rsl:8: error: you can only quantify over arrays +Processed 1 model and 0 requirement files and found 1 error diff --git a/tests-system/rbt-quantification-object-2/foo.rsl b/tests-system/rbt-quantification-object-2/foo.rsl new file mode 100644 index 00000000..81ab03ec --- /dev/null +++ b/tests-system/rbt-quantification-object-2/foo.rsl @@ -0,0 +1,9 @@ +package Foo + +type Potato { + a String +} + +checks Potato { + (forall char in b => char != "a"), warning "b should not contain the letter a" +} diff --git a/tests-system/rbt-quantification-object-2/output b/tests-system/rbt-quantification-object-2/output new file mode 100644 index 00000000..c9019dd7 --- /dev/null +++ b/tests-system/rbt-quantification-object-2/output @@ -0,0 +1,3 @@ +(forall char in b => char != "a"), warning "b should not contain the letter a" + ^ rbt-quantification-object-2/foo.rsl:8: error: unknown symbol b +Processed 1 model and 0 requirement files and found 1 error diff --git a/tests-system/rbt-quantification-object-2/output.brief b/tests-system/rbt-quantification-object-2/output.brief new file mode 100644 index 00000000..5688779f --- /dev/null +++ b/tests-system/rbt-quantification-object-2/output.brief @@ -0,0 +1 @@ +rbt-quantification-object-2/foo.rsl:8:21: trlc error: unknown symbol b diff --git a/tests-system/rbt-quantification-object-2/output.json b/tests-system/rbt-quantification-object-2/output.json new file mode 100644 index 00000000..c9019dd7 --- /dev/null +++ b/tests-system/rbt-quantification-object-2/output.json @@ -0,0 +1,3 @@ +(forall char in b => char != "a"), warning "b should not contain the letter a" + ^ rbt-quantification-object-2/foo.rsl:8: error: unknown symbol b +Processed 1 model and 0 requirement files and found 1 error diff --git a/tests-system/rbt-quantification-object-2/output.smtlib b/tests-system/rbt-quantification-object-2/output.smtlib new file mode 100644 index 00000000..c9019dd7 --- /dev/null +++ b/tests-system/rbt-quantification-object-2/output.smtlib @@ -0,0 +1,3 @@ +(forall char in b => char != "a"), warning "b should not contain the letter a" + ^ rbt-quantification-object-2/foo.rsl:8: error: unknown symbol b +Processed 1 model and 0 requirement files and found 1 error diff --git a/tests-system/rbt-quantified-expression/foo.rsl b/tests-system/rbt-quantified-expression/foo.rsl new file mode 100644 index 00000000..d877e168 --- /dev/null +++ b/tests-system/rbt-quantified-expression/foo.rsl @@ -0,0 +1,11 @@ +package Foo + +type T { + a Integer[1..*] +} + +checks T { + (forall item in a => item > 0), warning "All items must be positive", a + (exists item in a => item == 7), warning "7 is a lucky number", a + (forall item in a => 42), warning "All items must be positive", a +} diff --git a/tests-system/rbt-quantified-expression/foo.trlc b/tests-system/rbt-quantified-expression/foo.trlc new file mode 100644 index 00000000..3f3e23c5 --- /dev/null +++ b/tests-system/rbt-quantified-expression/foo.trlc @@ -0,0 +1,5 @@ +package Foo + +T Bar { + a = [1, 2, 3, 7] +} diff --git a/tests-system/rbt-quantified-expression/output b/tests-system/rbt-quantified-expression/output new file mode 100644 index 00000000..cd5ef1e1 --- /dev/null +++ b/tests-system/rbt-quantified-expression/output @@ -0,0 +1,3 @@ +(forall item in a => 42), warning "All items must be positive", a + ^^ rbt-quantified-expression/foo.rsl:10: error: expected expression of type Builtin_Boolean, got Builtin_Integer instead +Processed 1 model and 1 requirement file and found 1 error diff --git a/tests-system/rbt-quantified-expression/output.brief b/tests-system/rbt-quantified-expression/output.brief new file mode 100644 index 00000000..d16c8133 --- /dev/null +++ b/tests-system/rbt-quantified-expression/output.brief @@ -0,0 +1 @@ +rbt-quantified-expression/foo.rsl:10:26: trlc error: expected expression of type Builtin_Boolean, got Builtin_Integer instead diff --git a/tests-system/rbt-quantified-expression/output.json b/tests-system/rbt-quantified-expression/output.json new file mode 100644 index 00000000..cd5ef1e1 --- /dev/null +++ b/tests-system/rbt-quantified-expression/output.json @@ -0,0 +1,3 @@ +(forall item in a => 42), warning "All items must be positive", a + ^^ rbt-quantified-expression/foo.rsl:10: error: expected expression of type Builtin_Boolean, got Builtin_Integer instead +Processed 1 model and 1 requirement file and found 1 error diff --git a/tests-system/rbt-quantified-expression/output.smtlib b/tests-system/rbt-quantified-expression/output.smtlib new file mode 100644 index 00000000..cd5ef1e1 --- /dev/null +++ b/tests-system/rbt-quantified-expression/output.smtlib @@ -0,0 +1,3 @@ +(forall item in a => 42), warning "All items must be positive", a + ^^ rbt-quantified-expression/foo.rsl:10: error: expected expression of type Builtin_Boolean, got Builtin_Integer instead +Processed 1 model and 1 requirement file and found 1 error diff --git a/tests-system/rbt-quantified-expression/tracing b/tests-system/rbt-quantified-expression/tracing new file mode 100644 index 00000000..d76a7b7c --- /dev/null +++ b/tests-system/rbt-quantified-expression/tracing @@ -0,0 +1 @@ +LRM.Quantification_Type diff --git a/tests-system/rbt-record-object-declaration/foo.rsl b/tests-system/rbt-record-object-declaration/foo.rsl new file mode 100644 index 00000000..e3dfa401 --- /dev/null +++ b/tests-system/rbt-record-object-declaration/foo.rsl @@ -0,0 +1,25 @@ +package Foo + +tuple B { + a Integer + separator @ + b Integer +} + +enum E { + a + b + c +} + +type Ref {} + +type T { + tu B + array Integer[1..*] + integer Integer + decimal Decimal + string String + en E + ref Ref +} diff --git a/tests-system/rbt-record-object-declaration/foo.trlc b/tests-system/rbt-record-object-declaration/foo.trlc new file mode 100644 index 00000000..83ad5a41 --- /dev/null +++ b/tests-system/rbt-record-object-declaration/foo.trlc @@ -0,0 +1,13 @@ +package Foo + +T Potato { + tu = 1@3 + array = [1, 2, 3] + string = "hello" + integer = +1 + decimal = -1.0 + en = E.a + ref = Record +} + +Ref Record {} diff --git a/tests-system/rbt-record-object-declaration/output b/tests-system/rbt-record-object-declaration/output new file mode 100644 index 00000000..a36e3bac --- /dev/null +++ b/tests-system/rbt-record-object-declaration/output @@ -0,0 +1 @@ +Processed 1 model and 1 requirement file and found no issues diff --git a/tests-system/rbt-record-object-declaration/output.brief b/tests-system/rbt-record-object-declaration/output.brief new file mode 100644 index 00000000..e69de29b diff --git a/tests-system/rbt-record-object-declaration/output.json b/tests-system/rbt-record-object-declaration/output.json new file mode 100644 index 00000000..c168dc9d --- /dev/null +++ b/tests-system/rbt-record-object-declaration/output.json @@ -0,0 +1,20 @@ +{ + "Potato": { + "array": [ + 1, + 2, + 3 + ], + "decimal": -1.0, + "en": "a", + "integer": 1, + "ref": "Foo.Record", + "string": "hello", + "tu": { + "a": 1, + "b": 3 + } + }, + "Record": {} +} +Processed 1 model and 1 requirement file and found no issues diff --git a/tests-system/rbt-record-object-declaration/output.smtlib b/tests-system/rbt-record-object-declaration/output.smtlib new file mode 100644 index 00000000..a36e3bac --- /dev/null +++ b/tests-system/rbt-record-object-declaration/output.smtlib @@ -0,0 +1 @@ +Processed 1 model and 1 requirement file and found no issues diff --git a/tests-system/rbt-references-to-extensions/foo.rsl b/tests-system/rbt-references-to-extensions/foo.rsl new file mode 100644 index 00000000..7aad88dc --- /dev/null +++ b/tests-system/rbt-references-to-extensions/foo.rsl @@ -0,0 +1,17 @@ +package Foo + +type R { + a Integer +} + +type RE extends R { + b Integer +} + +type Potato { + ref R[1..*] +} + +type Kitten { + ref RE[1..*] +} diff --git a/tests-system/rbt-references-to-extensions/foo.trlc b/tests-system/rbt-references-to-extensions/foo.trlc new file mode 100644 index 00000000..275ded97 --- /dev/null +++ b/tests-system/rbt-references-to-extensions/foo.trlc @@ -0,0 +1,18 @@ +package Foo + +R Tiger { + a = 1 +} + +RE Lion { + a = 1 + b = 2 +} + +Potato Bar { + ref = [Tiger, Lion] +} + +Kitten Sonic { + ref = [Tiger, Lion] +} diff --git a/tests-system/rbt-references-to-extensions/output b/tests-system/rbt-references-to-extensions/output new file mode 100644 index 00000000..eec27409 --- /dev/null +++ b/tests-system/rbt-references-to-extensions/output @@ -0,0 +1,3 @@ +ref = [Tiger, Lion] + ^^^^^ rbt-references-to-extensions/foo.trlc:17: error: expected reference of type RE, but Tiger is of type R +Processed 1 model and 1 requirement file and found 1 error diff --git a/tests-system/rbt-references-to-extensions/output.brief b/tests-system/rbt-references-to-extensions/output.brief new file mode 100644 index 00000000..b11aa999 --- /dev/null +++ b/tests-system/rbt-references-to-extensions/output.brief @@ -0,0 +1 @@ +rbt-references-to-extensions/foo.trlc:17:12: trlc error: expected reference of type RE, but Tiger is of type R diff --git a/tests-system/rbt-references-to-extensions/output.json b/tests-system/rbt-references-to-extensions/output.json new file mode 100644 index 00000000..eec27409 --- /dev/null +++ b/tests-system/rbt-references-to-extensions/output.json @@ -0,0 +1,3 @@ +ref = [Tiger, Lion] + ^^^^^ rbt-references-to-extensions/foo.trlc:17: error: expected reference of type RE, but Tiger is of type R +Processed 1 model and 1 requirement file and found 1 error diff --git a/tests-system/rbt-references-to-extensions/output.smtlib b/tests-system/rbt-references-to-extensions/output.smtlib new file mode 100644 index 00000000..eec27409 --- /dev/null +++ b/tests-system/rbt-references-to-extensions/output.smtlib @@ -0,0 +1,3 @@ +ref = [Tiger, Lion] + ^^^^^ rbt-references-to-extensions/foo.trlc:17: error: expected reference of type RE, but Tiger is of type R +Processed 1 model and 1 requirement file and found 1 error diff --git a/tests-system/rbt-sufficiently-distinct-3/foo.rsl b/tests-system/rbt-sufficiently-distinct-3/foo.rsl new file mode 100644 index 00000000..cc2da462 --- /dev/null +++ b/tests-system/rbt-sufficiently-distinct-3/foo.rsl @@ -0,0 +1,9 @@ +package Foo + +type T_Bar { + a Integer +} + +type tbar { + b Integer +} diff --git a/tests-system/rbt-sufficiently-distinct-3/foo.trlc b/tests-system/rbt-sufficiently-distinct-3/foo.trlc new file mode 100644 index 00000000..efc41b46 --- /dev/null +++ b/tests-system/rbt-sufficiently-distinct-3/foo.trlc @@ -0,0 +1,17 @@ +package Foo + +T_Bar Bar_Kitten { + a = 1 +} + +T_Bar bar_kitten { + a = 2 +} + +tbar Foo_Bar { + b = 3 +} + +tbar foobar { + b = 4 +} diff --git a/tests-system/rbt-sufficiently-distinct-3/output b/tests-system/rbt-sufficiently-distinct-3/output new file mode 100644 index 00000000..d6eb6b0f --- /dev/null +++ b/tests-system/rbt-sufficiently-distinct-3/output @@ -0,0 +1,5 @@ +type tbar { + ^^^^ rbt-sufficiently-distinct-3/foo.rsl:7: error: tbar is too similar to T_Bar, declared at foo.rsl:3 +T_Bar bar_kitten { + ^^^^^^^^^^ rbt-sufficiently-distinct-3/foo.trlc:7: error: bar_kitten is too similar to Bar_Kitten, declared at foo.trlc:3 +Processed 1 model and 1 requirement file and found 2 errors diff --git a/tests-system/rbt-sufficiently-distinct-3/output.brief b/tests-system/rbt-sufficiently-distinct-3/output.brief new file mode 100644 index 00000000..d5a1248a --- /dev/null +++ b/tests-system/rbt-sufficiently-distinct-3/output.brief @@ -0,0 +1,2 @@ +rbt-sufficiently-distinct-3/foo.rsl:7:6: trlc error: tbar is too similar to T_Bar, declared at foo.rsl:3 +rbt-sufficiently-distinct-3/foo.trlc:7:7: trlc error: bar_kitten is too similar to Bar_Kitten, declared at foo.trlc:3 diff --git a/tests-system/rbt-sufficiently-distinct-3/output.json b/tests-system/rbt-sufficiently-distinct-3/output.json new file mode 100644 index 00000000..d6eb6b0f --- /dev/null +++ b/tests-system/rbt-sufficiently-distinct-3/output.json @@ -0,0 +1,5 @@ +type tbar { + ^^^^ rbt-sufficiently-distinct-3/foo.rsl:7: error: tbar is too similar to T_Bar, declared at foo.rsl:3 +T_Bar bar_kitten { + ^^^^^^^^^^ rbt-sufficiently-distinct-3/foo.trlc:7: error: bar_kitten is too similar to Bar_Kitten, declared at foo.trlc:3 +Processed 1 model and 1 requirement file and found 2 errors diff --git a/tests-system/rbt-sufficiently-distinct-3/output.smtlib b/tests-system/rbt-sufficiently-distinct-3/output.smtlib new file mode 100644 index 00000000..d6eb6b0f --- /dev/null +++ b/tests-system/rbt-sufficiently-distinct-3/output.smtlib @@ -0,0 +1,5 @@ +type tbar { + ^^^^ rbt-sufficiently-distinct-3/foo.rsl:7: error: tbar is too similar to T_Bar, declared at foo.rsl:3 +T_Bar bar_kitten { + ^^^^^^^^^^ rbt-sufficiently-distinct-3/foo.trlc:7: error: bar_kitten is too similar to Bar_Kitten, declared at foo.trlc:3 +Processed 1 model and 1 requirement file and found 2 errors diff --git a/tests-system/rbt-tuple-generic-form/foo.rsl b/tests-system/rbt-tuple-generic-form/foo.rsl new file mode 100644 index 00000000..832454cf --- /dev/null +++ b/tests-system/rbt-tuple-generic-form/foo.rsl @@ -0,0 +1,11 @@ +package Foo + +tuple Tuple { + a Integer + b String + c Integer +} + +type T { + tu Tuple +} diff --git a/tests-system/rbt-tuple-generic-form/foo.trlc b/tests-system/rbt-tuple-generic-form/foo.trlc new file mode 100644 index 00000000..ecad00c0 --- /dev/null +++ b/tests-system/rbt-tuple-generic-form/foo.trlc @@ -0,0 +1,5 @@ +package Foo + +T Bar { + tu = (1, 2.0, 3) +} diff --git a/tests-system/rbt-tuple-generic-form/output b/tests-system/rbt-tuple-generic-form/output new file mode 100644 index 00000000..b3a9f276 --- /dev/null +++ b/tests-system/rbt-tuple-generic-form/output @@ -0,0 +1,3 @@ +tu = (1, 2.0, 3) + ^^^ rbt-tuple-generic-form/foo.trlc:4: error: expected string literal, encountered decimal literal instead +Processed 1 model and 1 requirement file and found 1 error diff --git a/tests-system/rbt-tuple-generic-form/output.brief b/tests-system/rbt-tuple-generic-form/output.brief new file mode 100644 index 00000000..aaace5f4 --- /dev/null +++ b/tests-system/rbt-tuple-generic-form/output.brief @@ -0,0 +1 @@ +rbt-tuple-generic-form/foo.trlc:4:14: trlc error: expected string literal, encountered decimal literal instead diff --git a/tests-system/rbt-tuple-generic-form/output.json b/tests-system/rbt-tuple-generic-form/output.json new file mode 100644 index 00000000..b3a9f276 --- /dev/null +++ b/tests-system/rbt-tuple-generic-form/output.json @@ -0,0 +1,3 @@ +tu = (1, 2.0, 3) + ^^^ rbt-tuple-generic-form/foo.trlc:4: error: expected string literal, encountered decimal literal instead +Processed 1 model and 1 requirement file and found 1 error diff --git a/tests-system/rbt-tuple-generic-form/output.smtlib b/tests-system/rbt-tuple-generic-form/output.smtlib new file mode 100644 index 00000000..b3a9f276 --- /dev/null +++ b/tests-system/rbt-tuple-generic-form/output.smtlib @@ -0,0 +1,3 @@ +tu = (1, 2.0, 3) + ^^^ rbt-tuple-generic-form/foo.trlc:4: error: expected string literal, encountered decimal literal instead +Processed 1 model and 1 requirement file and found 1 error diff --git a/tests-system/rbt-tuple-separator-form-1/foo.rsl b/tests-system/rbt-tuple-separator-form-1/foo.rsl new file mode 100644 index 00000000..9ab8fa74 --- /dev/null +++ b/tests-system/rbt-tuple-separator-form-1/foo.rsl @@ -0,0 +1,17 @@ +package Foo + +tuple Tuple { + a Integer + separator @ + b Integer + separator : + c Integer + separator ; + d optional Integer + separator @ + e optional Integer +} + +type T { + tu Tuple +} diff --git a/tests-system/rbt-tuple-separator-form-1/foo.trlc b/tests-system/rbt-tuple-separator-form-1/foo.trlc new file mode 100644 index 00000000..d6821c8a --- /dev/null +++ b/tests-system/rbt-tuple-separator-form-1/foo.trlc @@ -0,0 +1,5 @@ +package Foo + +T Bar { + tu = 1:2@3;4 +} diff --git a/tests-system/rbt-tuple-separator-form-1/output b/tests-system/rbt-tuple-separator-form-1/output new file mode 100644 index 00000000..87fd2719 --- /dev/null +++ b/tests-system/rbt-tuple-separator-form-1/output @@ -0,0 +1,3 @@ +tu = 1:2@3;4 + ^ rbt-tuple-separator-form-1/foo.trlc:4: error: expected integer literal, encountered separator ':' instead +Processed 1 model and 1 requirement file and found 1 error diff --git a/tests-system/rbt-tuple-separator-form-1/output.brief b/tests-system/rbt-tuple-separator-form-1/output.brief new file mode 100644 index 00000000..2fad3678 --- /dev/null +++ b/tests-system/rbt-tuple-separator-form-1/output.brief @@ -0,0 +1 @@ +rbt-tuple-separator-form-1/foo.trlc:4:11: trlc error: expected integer literal, encountered separator ':' instead diff --git a/tests-system/rbt-tuple-separator-form-1/output.json b/tests-system/rbt-tuple-separator-form-1/output.json new file mode 100644 index 00000000..87fd2719 --- /dev/null +++ b/tests-system/rbt-tuple-separator-form-1/output.json @@ -0,0 +1,3 @@ +tu = 1:2@3;4 + ^ rbt-tuple-separator-form-1/foo.trlc:4: error: expected integer literal, encountered separator ':' instead +Processed 1 model and 1 requirement file and found 1 error diff --git a/tests-system/rbt-tuple-separator-form-1/output.smtlib b/tests-system/rbt-tuple-separator-form-1/output.smtlib new file mode 100644 index 00000000..87fd2719 --- /dev/null +++ b/tests-system/rbt-tuple-separator-form-1/output.smtlib @@ -0,0 +1,3 @@ +tu = 1:2@3;4 + ^ rbt-tuple-separator-form-1/foo.trlc:4: error: expected integer literal, encountered separator ':' instead +Processed 1 model and 1 requirement file and found 1 error diff --git a/tests-system/rbt-tuple-separator-form-2/foo.rsl b/tests-system/rbt-tuple-separator-form-2/foo.rsl new file mode 100644 index 00000000..9ab8fa74 --- /dev/null +++ b/tests-system/rbt-tuple-separator-form-2/foo.rsl @@ -0,0 +1,17 @@ +package Foo + +tuple Tuple { + a Integer + separator @ + b Integer + separator : + c Integer + separator ; + d optional Integer + separator @ + e optional Integer +} + +type T { + tu Tuple +} diff --git a/tests-system/rbt-tuple-separator-form-2/foo.trlc b/tests-system/rbt-tuple-separator-form-2/foo.trlc new file mode 100644 index 00000000..49b2d70a --- /dev/null +++ b/tests-system/rbt-tuple-separator-form-2/foo.trlc @@ -0,0 +1,5 @@ +package Foo + +T Bar { + tu = 1@2:3;4 +} diff --git a/tests-system/rbt-tuple-separator-form-2/output b/tests-system/rbt-tuple-separator-form-2/output new file mode 100644 index 00000000..a36e3bac --- /dev/null +++ b/tests-system/rbt-tuple-separator-form-2/output @@ -0,0 +1 @@ +Processed 1 model and 1 requirement file and found no issues diff --git a/tests-system/rbt-tuple-separator-form-2/output.brief b/tests-system/rbt-tuple-separator-form-2/output.brief new file mode 100644 index 00000000..e69de29b diff --git a/tests-system/rbt-tuple-separator-form-2/output.json b/tests-system/rbt-tuple-separator-form-2/output.json new file mode 100644 index 00000000..c9571fb4 --- /dev/null +++ b/tests-system/rbt-tuple-separator-form-2/output.json @@ -0,0 +1,12 @@ +{ + "Bar": { + "tu": { + "a": 1, + "b": 2, + "c": 3, + "d": 4, + "e": null + } + } +} +Processed 1 model and 1 requirement file and found no issues diff --git a/tests-system/rbt-tuple-separator-form-2/output.smtlib b/tests-system/rbt-tuple-separator-form-2/output.smtlib new file mode 100644 index 00000000..a36e3bac --- /dev/null +++ b/tests-system/rbt-tuple-separator-form-2/output.smtlib @@ -0,0 +1 @@ +Processed 1 model and 1 requirement file and found no issues diff --git a/tests-system/rbt-tuple-syntax-correct-form/foo.rsl b/tests-system/rbt-tuple-syntax-correct-form/foo.rsl new file mode 100644 index 00000000..af54832d --- /dev/null +++ b/tests-system/rbt-tuple-syntax-correct-form/foo.rsl @@ -0,0 +1,17 @@ +package Foo + +tuple Sep { + a Integer + separator @ + b Integer +} + +tuple NoSep { + a Integer + b Integer +} + +type T { + sep Sep + nosep NoSep +} diff --git a/tests-system/rbt-tuple-syntax-correct-form/foo.trlc b/tests-system/rbt-tuple-syntax-correct-form/foo.trlc new file mode 100644 index 00000000..d78809c3 --- /dev/null +++ b/tests-system/rbt-tuple-syntax-correct-form/foo.trlc @@ -0,0 +1,11 @@ +package Foo + +T Potato { + sep = 1@3 + nosep = 1,3 +} + +T Kitten { + sep = (1@5) + nosep = (1,3) +} diff --git a/tests-system/rbt-tuple-syntax-correct-form/output b/tests-system/rbt-tuple-syntax-correct-form/output new file mode 100644 index 00000000..a242fefc --- /dev/null +++ b/tests-system/rbt-tuple-syntax-correct-form/output @@ -0,0 +1,5 @@ +nosep = 1,3 + ^ rbt-tuple-syntax-correct-form/foo.trlc:5: error: expected opening parenthesis '(', encountered integer literal instead +sep = (1@5) + ^ rbt-tuple-syntax-correct-form/foo.trlc:9: error: expected integer literal, encountered opening parenthesis '(' instead +Processed 1 model and 1 requirement file and found 2 errors diff --git a/tests-system/rbt-tuple-syntax-correct-form/output.brief b/tests-system/rbt-tuple-syntax-correct-form/output.brief new file mode 100644 index 00000000..58da0fce --- /dev/null +++ b/tests-system/rbt-tuple-syntax-correct-form/output.brief @@ -0,0 +1,2 @@ +rbt-tuple-syntax-correct-form/foo.trlc:5:13: trlc error: expected opening parenthesis '(', encountered integer literal instead +rbt-tuple-syntax-correct-form/foo.trlc:9:11: trlc error: expected integer literal, encountered opening parenthesis '(' instead diff --git a/tests-system/rbt-tuple-syntax-correct-form/output.json b/tests-system/rbt-tuple-syntax-correct-form/output.json new file mode 100644 index 00000000..a242fefc --- /dev/null +++ b/tests-system/rbt-tuple-syntax-correct-form/output.json @@ -0,0 +1,5 @@ +nosep = 1,3 + ^ rbt-tuple-syntax-correct-form/foo.trlc:5: error: expected opening parenthesis '(', encountered integer literal instead +sep = (1@5) + ^ rbt-tuple-syntax-correct-form/foo.trlc:9: error: expected integer literal, encountered opening parenthesis '(' instead +Processed 1 model and 1 requirement file and found 2 errors diff --git a/tests-system/rbt-tuple-syntax-correct-form/output.smtlib b/tests-system/rbt-tuple-syntax-correct-form/output.smtlib new file mode 100644 index 00000000..a242fefc --- /dev/null +++ b/tests-system/rbt-tuple-syntax-correct-form/output.smtlib @@ -0,0 +1,5 @@ +nosep = 1,3 + ^ rbt-tuple-syntax-correct-form/foo.trlc:5: error: expected opening parenthesis '(', encountered integer literal instead +sep = (1@5) + ^ rbt-tuple-syntax-correct-form/foo.trlc:9: error: expected integer literal, encountered opening parenthesis '(' instead +Processed 1 model and 1 requirement file and found 2 errors diff --git a/tests-system/rbt-unique-object-names/foo.rsl b/tests-system/rbt-unique-object-names/foo.rsl new file mode 100644 index 00000000..ba7f0873 --- /dev/null +++ b/tests-system/rbt-unique-object-names/foo.rsl @@ -0,0 +1,3 @@ +package Foo + +type T {} diff --git a/tests-system/rbt-unique-object-names/foo.trlc b/tests-system/rbt-unique-object-names/foo.trlc new file mode 100644 index 00000000..7174d18c --- /dev/null +++ b/tests-system/rbt-unique-object-names/foo.trlc @@ -0,0 +1,9 @@ +package Foo + +T Foo {} + +T T {} + +T Bar {} + +T Bar {} diff --git a/tests-system/rbt-unique-object-names/output b/tests-system/rbt-unique-object-names/output new file mode 100644 index 00000000..9ff007f9 --- /dev/null +++ b/tests-system/rbt-unique-object-names/output @@ -0,0 +1,7 @@ +T Foo {} + ^^^ rbt-unique-object-names/foo.trlc:3: error: duplicate definition, previous definition at foo.rsl:1 +T T {} + ^ rbt-unique-object-names/foo.trlc:5: error: duplicate definition, previous definition at foo.rsl:3 +T Bar {} + ^^^ rbt-unique-object-names/foo.trlc:9: error: duplicate definition, previous definition at foo.trlc:7 +Processed 1 model and 1 requirement file and found 3 errors diff --git a/tests-system/rbt-unique-object-names/output.brief b/tests-system/rbt-unique-object-names/output.brief new file mode 100644 index 00000000..9af85ff5 --- /dev/null +++ b/tests-system/rbt-unique-object-names/output.brief @@ -0,0 +1,3 @@ +rbt-unique-object-names/foo.trlc:3:3: trlc error: duplicate definition, previous definition at foo.rsl:1 +rbt-unique-object-names/foo.trlc:5:3: trlc error: duplicate definition, previous definition at foo.rsl:3 +rbt-unique-object-names/foo.trlc:9:3: trlc error: duplicate definition, previous definition at foo.trlc:7 diff --git a/tests-system/rbt-unique-object-names/output.json b/tests-system/rbt-unique-object-names/output.json new file mode 100644 index 00000000..9ff007f9 --- /dev/null +++ b/tests-system/rbt-unique-object-names/output.json @@ -0,0 +1,7 @@ +T Foo {} + ^^^ rbt-unique-object-names/foo.trlc:3: error: duplicate definition, previous definition at foo.rsl:1 +T T {} + ^ rbt-unique-object-names/foo.trlc:5: error: duplicate definition, previous definition at foo.rsl:3 +T Bar {} + ^^^ rbt-unique-object-names/foo.trlc:9: error: duplicate definition, previous definition at foo.trlc:7 +Processed 1 model and 1 requirement file and found 3 errors diff --git a/tests-system/rbt-unique-object-names/output.smtlib b/tests-system/rbt-unique-object-names/output.smtlib new file mode 100644 index 00000000..9ff007f9 --- /dev/null +++ b/tests-system/rbt-unique-object-names/output.smtlib @@ -0,0 +1,7 @@ +T Foo {} + ^^^ rbt-unique-object-names/foo.trlc:3: error: duplicate definition, previous definition at foo.rsl:1 +T T {} + ^ rbt-unique-object-names/foo.trlc:5: error: duplicate definition, previous definition at foo.rsl:3 +T Bar {} + ^^^ rbt-unique-object-names/foo.trlc:9: error: duplicate definition, previous definition at foo.trlc:7 +Processed 1 model and 1 requirement file and found 3 errors diff --git a/tests-system/rbt-universal-quantification-semantics/foo.rsl b/tests-system/rbt-universal-quantification-semantics/foo.rsl new file mode 100644 index 00000000..f2f71b56 --- /dev/null +++ b/tests-system/rbt-universal-quantification-semantics/foo.rsl @@ -0,0 +1,9 @@ +package Foo + +type T { + a Integer[0..*] +} + +checks T { + (forall item in a => item > 0), warning "All items must be positive" +} diff --git a/tests-system/rbt-universal-quantification-semantics/foo.trlc b/tests-system/rbt-universal-quantification-semantics/foo.trlc new file mode 100644 index 00000000..230875da --- /dev/null +++ b/tests-system/rbt-universal-quantification-semantics/foo.trlc @@ -0,0 +1,13 @@ +package Foo + +T Bar { + a = [-1] +} + +T Kitten { + a = [] +} + +T Potato { + a = [-1, 1] +} diff --git a/tests-system/rbt-universal-quantification-semantics/output b/tests-system/rbt-universal-quantification-semantics/output new file mode 100644 index 00000000..07661ca4 --- /dev/null +++ b/tests-system/rbt-universal-quantification-semantics/output @@ -0,0 +1,5 @@ +T Bar { + ^^^ rbt-universal-quantification-semantics/foo.trlc:3: check warning: All items must be positive +T Potato { + ^^^^^^ rbt-universal-quantification-semantics/foo.trlc:11: check warning: All items must be positive +Processed 1 model and 1 requirement file and found 2 warnings diff --git a/tests-system/rbt-universal-quantification-semantics/output.brief b/tests-system/rbt-universal-quantification-semantics/output.brief new file mode 100644 index 00000000..c4f34df9 --- /dev/null +++ b/tests-system/rbt-universal-quantification-semantics/output.brief @@ -0,0 +1,2 @@ +rbt-universal-quantification-semantics/foo.trlc:3:3: trlc check warning: All items must be positive +rbt-universal-quantification-semantics/foo.trlc:11:3: trlc check warning: All items must be positive diff --git a/tests-system/rbt-universal-quantification-semantics/output.json b/tests-system/rbt-universal-quantification-semantics/output.json new file mode 100644 index 00000000..e25ab77e --- /dev/null +++ b/tests-system/rbt-universal-quantification-semantics/output.json @@ -0,0 +1,21 @@ +T Bar { + ^^^ rbt-universal-quantification-semantics/foo.trlc:3: check warning: All items must be positive +T Potato { + ^^^^^^ rbt-universal-quantification-semantics/foo.trlc:11: check warning: All items must be positive +{ + "Bar": { + "a": [ + -1 + ] + }, + "Kitten": { + "a": [] + }, + "Potato": { + "a": [ + -1, + 1 + ] + } +} +Processed 1 model and 1 requirement file and found 2 warnings diff --git a/tests-system/rbt-universal-quantification-semantics/output.smtlib b/tests-system/rbt-universal-quantification-semantics/output.smtlib new file mode 100644 index 00000000..07661ca4 --- /dev/null +++ b/tests-system/rbt-universal-quantification-semantics/output.smtlib @@ -0,0 +1,5 @@ +T Bar { + ^^^ rbt-universal-quantification-semantics/foo.trlc:3: check warning: All items must be positive +T Potato { + ^^^^^^ rbt-universal-quantification-semantics/foo.trlc:11: check warning: All items must be positive +Processed 1 model and 1 requirement file and found 2 warnings diff --git a/tests-system/rbt-valid-components/foo.rsl b/tests-system/rbt-valid-components/foo.rsl new file mode 100644 index 00000000..996bb43a --- /dev/null +++ b/tests-system/rbt-valid-components/foo.rsl @@ -0,0 +1,6 @@ +package Foo + +type T { + a Integer + freeze a = 2 +} diff --git a/tests-system/rbt-valid-components/foo.trlc b/tests-system/rbt-valid-components/foo.trlc new file mode 100644 index 00000000..ed73fe1f --- /dev/null +++ b/tests-system/rbt-valid-components/foo.trlc @@ -0,0 +1,5 @@ +package Foo + +T Bar { + a = 2 +} diff --git a/tests-system/rbt-valid-components/output b/tests-system/rbt-valid-components/output new file mode 100644 index 00000000..2dcd5cc2 --- /dev/null +++ b/tests-system/rbt-valid-components/output @@ -0,0 +1,3 @@ +a = 2 +^ rbt-valid-components/foo.trlc:4: error: cannot overwrite frozen component a +Processed 1 model and 1 requirement file and found 1 error diff --git a/tests-system/rbt-valid-components/output.brief b/tests-system/rbt-valid-components/output.brief new file mode 100644 index 00000000..2e5b0b01 --- /dev/null +++ b/tests-system/rbt-valid-components/output.brief @@ -0,0 +1 @@ +rbt-valid-components/foo.trlc:4:5: trlc error: cannot overwrite frozen component a diff --git a/tests-system/rbt-valid-components/output.json b/tests-system/rbt-valid-components/output.json new file mode 100644 index 00000000..2dcd5cc2 --- /dev/null +++ b/tests-system/rbt-valid-components/output.json @@ -0,0 +1,3 @@ +a = 2 +^ rbt-valid-components/foo.trlc:4: error: cannot overwrite frozen component a +Processed 1 model and 1 requirement file and found 1 error diff --git a/tests-system/rbt-valid-components/output.smtlib b/tests-system/rbt-valid-components/output.smtlib new file mode 100644 index 00000000..2dcd5cc2 --- /dev/null +++ b/tests-system/rbt-valid-components/output.smtlib @@ -0,0 +1,3 @@ +a = 2 +^ rbt-valid-components/foo.trlc:4: error: cannot overwrite frozen component a +Processed 1 model and 1 requirement file and found 1 error diff --git a/tests-system/rbt-valid-enumeration-literals/foo.rsl b/tests-system/rbt-valid-enumeration-literals/foo.rsl new file mode 100644 index 00000000..b8a2eb9d --- /dev/null +++ b/tests-system/rbt-valid-enumeration-literals/foo.rsl @@ -0,0 +1,11 @@ +package Foo + +enum Enum { + A + B + C +} + +type T { + en Enum +} diff --git a/tests-system/rbt-valid-enumeration-literals/foo.trlc b/tests-system/rbt-valid-enumeration-literals/foo.trlc new file mode 100644 index 00000000..4244ee6d --- /dev/null +++ b/tests-system/rbt-valid-enumeration-literals/foo.trlc @@ -0,0 +1,9 @@ +package Foo + +T Bar { + en = Enumm.A +} + +T Kitten { + en = Enum.D +} diff --git a/tests-system/rbt-valid-enumeration-literals/output b/tests-system/rbt-valid-enumeration-literals/output new file mode 100644 index 00000000..bdf33f5d --- /dev/null +++ b/tests-system/rbt-valid-enumeration-literals/output @@ -0,0 +1,5 @@ +en = Enumm.A + ^^^^^ rbt-valid-enumeration-literals/foo.trlc:4: error: unknown symbol Enumm +en = Enum.D + ^ rbt-valid-enumeration-literals/foo.trlc:8: error: unknown symbol D +Processed 1 model and 1 requirement file and found 2 errors diff --git a/tests-system/rbt-valid-enumeration-literals/output.brief b/tests-system/rbt-valid-enumeration-literals/output.brief new file mode 100644 index 00000000..b333827d --- /dev/null +++ b/tests-system/rbt-valid-enumeration-literals/output.brief @@ -0,0 +1,2 @@ +rbt-valid-enumeration-literals/foo.trlc:4:10: trlc error: unknown symbol Enumm +rbt-valid-enumeration-literals/foo.trlc:8:15: trlc error: unknown symbol D diff --git a/tests-system/rbt-valid-enumeration-literals/output.json b/tests-system/rbt-valid-enumeration-literals/output.json new file mode 100644 index 00000000..bdf33f5d --- /dev/null +++ b/tests-system/rbt-valid-enumeration-literals/output.json @@ -0,0 +1,5 @@ +en = Enumm.A + ^^^^^ rbt-valid-enumeration-literals/foo.trlc:4: error: unknown symbol Enumm +en = Enum.D + ^ rbt-valid-enumeration-literals/foo.trlc:8: error: unknown symbol D +Processed 1 model and 1 requirement file and found 2 errors diff --git a/tests-system/rbt-valid-enumeration-literals/output.smtlib b/tests-system/rbt-valid-enumeration-literals/output.smtlib new file mode 100644 index 00000000..bdf33f5d --- /dev/null +++ b/tests-system/rbt-valid-enumeration-literals/output.smtlib @@ -0,0 +1,5 @@ +en = Enumm.A + ^^^^^ rbt-valid-enumeration-literals/foo.trlc:4: error: unknown symbol Enumm +en = Enum.D + ^ rbt-valid-enumeration-literals/foo.trlc:8: error: unknown symbol D +Processed 1 model and 1 requirement file and found 2 errors diff --git a/tests-system/rbt-valid-record-types/foo.rsl b/tests-system/rbt-valid-record-types/foo.rsl new file mode 100644 index 00000000..f6203f10 --- /dev/null +++ b/tests-system/rbt-valid-record-types/foo.rsl @@ -0,0 +1,7 @@ +package Foo + +abstract type Ref {} + +type T extends Ref{ + ref Ref +} diff --git a/tests-system/rbt-valid-record-types/foo.trlc b/tests-system/rbt-valid-record-types/foo.trlc new file mode 100644 index 00000000..c3295a4b --- /dev/null +++ b/tests-system/rbt-valid-record-types/foo.trlc @@ -0,0 +1,7 @@ +package Foo + +T Potato { + ref = Kitten +} + +Ref Kitten {} diff --git a/tests-system/rbt-valid-record-types/output b/tests-system/rbt-valid-record-types/output new file mode 100644 index 00000000..09c9e6fb --- /dev/null +++ b/tests-system/rbt-valid-record-types/output @@ -0,0 +1,3 @@ +Ref Kitten {} +^^^ rbt-valid-record-types/foo.trlc:7: error: cannot declare object of abstract record type Ref +Processed 1 model and 1 requirement file and found 1 error diff --git a/tests-system/rbt-valid-record-types/output.brief b/tests-system/rbt-valid-record-types/output.brief new file mode 100644 index 00000000..f858f873 --- /dev/null +++ b/tests-system/rbt-valid-record-types/output.brief @@ -0,0 +1 @@ +rbt-valid-record-types/foo.trlc:7:1: trlc error: cannot declare object of abstract record type Ref diff --git a/tests-system/rbt-valid-record-types/output.json b/tests-system/rbt-valid-record-types/output.json new file mode 100644 index 00000000..09c9e6fb --- /dev/null +++ b/tests-system/rbt-valid-record-types/output.json @@ -0,0 +1,3 @@ +Ref Kitten {} +^^^ rbt-valid-record-types/foo.trlc:7: error: cannot declare object of abstract record type Ref +Processed 1 model and 1 requirement file and found 1 error diff --git a/tests-system/rbt-valid-record-types/output.smtlib b/tests-system/rbt-valid-record-types/output.smtlib new file mode 100644 index 00000000..09c9e6fb --- /dev/null +++ b/tests-system/rbt-valid-record-types/output.smtlib @@ -0,0 +1,3 @@ +Ref Kitten {} +^^^ rbt-valid-record-types/foo.trlc:7: error: cannot declare object of abstract record type Ref +Processed 1 model and 1 requirement file and found 1 error diff --git a/trlc/ast.py b/trlc/ast.py index 2fae7b12..5777e107 100644 --- a/trlc/ast.py +++ b/trlc/ast.py @@ -887,7 +887,8 @@ class Array_Aggregate(Expression): """ def __init__(self, location, typ): - # lobster-exclude: Constructor only declares variables + # lobster-trace: LRM.Record_Object_Declaration + super().__init__(location, typ) self.value = [] @@ -952,6 +953,8 @@ class Tuple_Aggregate(Expression): """ def __init__(self, location, typ): # lobster-trace: LRM.Unspecified_Optional_Components + # lobster-trace: LRM.Record_Object_Declaration + super().__init__(location, typ) self.value = {n_field.name : Implicit_Null(self, n_field) for n_field in self.typ.components.values()} @@ -1077,6 +1080,7 @@ def evaluate(self, mh, context): return Value(self.location, self, self.typ) def resolve_references(self, mh): + # lobster-trace: LRM.References_To_Extensions assert isinstance(mh, Message_Handler) self.target = self.package.symbols.lookup_direct( @@ -2042,6 +2046,8 @@ def __init__(self, mh, location, n_variable, n_source, n_expr): + # lobster-trace: LRM.Quantified_Expression + # lobster-trace: LRM.Quantification_Type super().__init__(location, typ) assert isinstance(typ, Builtin_Boolean) assert isinstance(universal, bool) @@ -2073,6 +2079,8 @@ def to_string(self): def evaluate(self, mh, context): # lobster-trace: LRM.Null_Is_Invalid + # lobster-trace: LRM.Universal_Quantification_Semantics + # lobster-trace: LRM.Existential_Quantification_Semantics assert isinstance(mh, Message_Handler) assert context is None or isinstance(context, dict) @@ -2933,6 +2941,8 @@ class Record_Object(Typed_Entity): def __init__(self, name, location, n_typ, section, n_package): # lobster-trace: LRM.Section_Declaration # lobster-trace: LRM.Unspecified_Optional_Components + # lobster-trace: LRM.Record_Object_Declaration + assert isinstance(n_typ, Record_Type) assert isinstance(section, list) or section is None assert isinstance(n_package, Package) @@ -2996,6 +3006,7 @@ def resolve_references(self, mh): def perform_checks(self, mh): # lobster-trace: LRM.Check_Evaluation_Order + # lobster-trace: LRM.Evaluation_Of_Checks assert isinstance(mh, Message_Handler) ok = True @@ -3140,6 +3151,8 @@ def register(self, mh, entity): # lobster-trace: LRM.Unique_Enumeration_Literals # lobster-trace: LRM.Tuple_Unique_Field_Names # lobster-trace: LRM.Sufficiently_Distinct + # lobster-trace: LRM.Unique_Object_Names + assert isinstance(mh, Message_Handler) assert isinstance(entity, Entity) diff --git a/trlc/parser.py b/trlc/parser.py index 3c759518..925100d9 100644 --- a/trlc/parser.py +++ b/trlc/parser.py @@ -166,6 +166,8 @@ def peek_kw(self, value): return self.peek("KEYWORD") and self.nt.value == value def match(self, kind): + # lobster-trace: LRM.Matching_Value_Types + assert kind in self.language_tokens, \ "%s is not a valid token" % kind if self.nt is None: @@ -1062,6 +1064,7 @@ def parse_primary(self, scope): return self.parse_name(scope) def parse_quantified_expression(self, scope): + # lobster-trace: LRM.Quantified_Expression assert isinstance(scope, ast.Scope) if self.peek_kw("forall"): @@ -1076,6 +1079,7 @@ def parse_quantified_expression(self, scope): self.match("IDENTIFIER") t_qv = self.ct if scope.contains(t_qv.value): + # lobster-trace: LRM.Quantification_Naming_Scope pdef = scope.lookup(self.mh, t_qv) self.mh.error(t_qv.location, "shadows %s %s from %s" % @@ -1090,6 +1094,7 @@ def parse_quantified_expression(self, scope): field) n_source.set_ast_link(self.ct) if not isinstance(field.n_typ, ast.Array_Type): + # lobster-trace: LRM.Quantification_Object self.mh.error(self.ct.location, "you can only quantify over arrays") n_var = ast.Quantified_Variable(t_qv.value, @@ -1305,22 +1310,21 @@ def parse_name(self, scope): # components the true grammar for function calls is always # IDENTIFIER '('; so we can slightly special case this. - if self.peek("IDENTIFIER"): - # lobster-trace: LRM.Builtin_Functions - # lobster-trace: LRM.Builtin_Type_Conversion_Functions - self.match("IDENTIFIER") - if self.peek("BRA"): - # If we follow our name with brackets - # immediately, we have a builtin function call. - n_name = self.stab.lookup(self.mh, - self.ct) - if not isinstance(n_name, (ast.Builtin_Function, - ast.Builtin_Numeric_Type)): - self.mh.error(self.ct.location, - "not a valid builtin function " - "or numeric type") - else: - n_name = self.parse_qualified_name(scope, match_ident=False) + # lobster-trace: LRM.Builtin_Functions + # lobster-trace: LRM.Builtin_Type_Conversion_Functions + self.match("IDENTIFIER") + if self.peek("BRA"): + # If we follow our name with brackets + # immediately, we have a builtin function call. + n_name = self.stab.lookup(self.mh, + self.ct) + if not isinstance(n_name, (ast.Builtin_Function, + ast.Builtin_Numeric_Type)): + self.mh.error(self.ct.location, + "not a valid builtin function " + "or numeric type") + else: + n_name = self.parse_qualified_name(scope, match_ident=False) # Enum literals are a bit different, so we deal with them # first. @@ -1559,6 +1563,7 @@ def parse_boolean(self): "expected boolean literal (true or false)") def parse_value(self, typ): + # lobster-trace: LRM.Tuple_Syntax_Correct_Form assert isinstance(typ, ast.Type) if isinstance(typ, ast.Builtin_Numeric_Type): @@ -1696,6 +1701,7 @@ def parse_value(self, typ): return rv elif isinstance(typ, ast.Tuple_Type) and typ.has_separators(): + # lobster-trace: LRM.Tuple_Separator_Form rv = ast.Tuple_Aggregate(self.nt.location, typ) next_is_optional = False @@ -1727,6 +1733,7 @@ def parse_value(self, typ): return rv elif isinstance(typ, ast.Tuple_Type) and not typ.has_separators(): + # lobster-trace: LRM.Tuple_Generic_Form self.match("BRA") rv = ast.Tuple_Aggregate(self.ct.location, typ) rv.set_ast_link(self.ct) @@ -1760,6 +1767,13 @@ def parse_markup_string(self): def parse_record_object_declaration(self): # lobster-trace: LRM.Section_Declaration + # lobster-trace: LRM.Record_Object_Declaration + # lobster-trace: LRM.Valid_Record_Types + # lobster-trace: LRM.Valid_Components + # lobster-trace: LRM.Valid_Enumeration_Literals + # lobster-trace: LRM.Mandatory_Components + # lobster-trace: LRM.Evaluation_Of_Checks + r_typ = self.parse_qualified_name(self.default_scope, ast.Record_Type) r_typ.set_ast_link(self.ct) diff --git a/trlc/trlc.py b/trlc/trlc.py index 22b0c721..6c0db925 100644 --- a/trlc/trlc.py +++ b/trlc/trlc.py @@ -18,20 +18,19 @@ # You should have received a copy of the GNU General Public License # along with TRLC. If not, see . -import re -import os -import sys -import json import argparse +import json +import os +import re import subprocess +import sys from fractions import Fraction -from trlc import ast -from trlc import lint -from trlc.errors import TRLC_Error, Location, Message_Handler, Kind -from trlc.parser import Parser +from trlc import ast, lint +from trlc.errors import Kind, Location, Message_Handler, TRLC_Error from trlc.lexer import Token_Stream -from trlc.version import TRLC_VERSION, BUGS_URL +from trlc.parser import Parser +from trlc.version import BUGS_URL, TRLC_VERSION # pylint: disable=unused-import try: @@ -457,6 +456,7 @@ def parse_trlc_files(self): return ok def resolve_record_references(self): + # lobster-trace: LRM.Late_Reference_Checking ok = True for package in self.stab.values(ast.Package): for obj in package.symbols.values(ast.Record_Object): @@ -550,7 +550,7 @@ def process(self): return self.stab -def main(): +def trlc(): ap = argparse.ArgumentParser( prog="trlc", description="TRLC %s (Python reference implementation)" % TRLC_VERSION, @@ -820,5 +820,16 @@ def get_status(parser): return 1 +def main(): + try: + return trlc() + except BrokenPipeError: + # Python flushes standard streams on exit; redirect remaining output + # to devnull to avoid another BrokenPipeError at shutdown + devnull = os.open(os.devnull, os.O_WRONLY) + os.dup2(devnull, sys.stdout.fileno()) + return 141 + + if __name__ == "__main__": sys.exit(main()) diff --git a/trlc/version.py b/trlc/version.py index f43cce4a..be077d85 100644 --- a/trlc/version.py +++ b/trlc/version.py @@ -18,7 +18,7 @@ # You should have received a copy of the GNU General Public License # along with TRLC. If not, see . -VERSION_TUPLE = (2, 0, 0) +VERSION_TUPLE = (2, 0, 1) VERSION_SUFFIX = "dev" TRLC_VERSION = ("%u.%u.%u" % VERSION_TUPLE) + \ diff --git a/util/fetch_cvc5.py b/util/fetch_cvc5.py new file mode 100755 index 00000000..1f4973e8 --- /dev/null +++ b/util/fetch_cvc5.py @@ -0,0 +1,71 @@ +#!/usr/bin/env python3 +# +# TRLC - Treat Requirements Like Code +# Copyright (C) 2024 Florian Schanda +# +# This file is part of the TRLC Python Reference Implementation. +# +# TRLC is free software: you can redistribute it and/or modify it +# under the terms of the GNU General Public License as published by +# the Free Software Foundation, either version 3 of the License, or +# (at your option) any later version. +# +# TRLC is distributed in the hope that it will be useful, but WITHOUT +# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +# or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +# License for more details. +# +# You should have received a copy of the GNU General Public License +# along with TRLC. If not, see . + +# This utility script fetches and unpacks CVC5 binaries for use in CI. + +import os +import urllib.request +import io +import zipfile +import argparse +import stat + +CVC5_RELEASES = "http://github.com/cvc5/cvc5/releases/download" +CVC5_BINARY = "cvc5" +CVC5_EXECUTABLE = True + +ap = argparse.ArgumentParser() +ap.add_argument("version") +ap.add_argument("platform") + +options = ap.parse_args() + +CVC5_VERSION = options.version + +if options.platform == "linux": + CVC5_PLATFORM = "Linux-x86_64-static" +elif options.platform == "osx13": + CVC5_PLATFORM = "macOS-x86_64-static" +elif options.platform == "osx14": + CVC5_PLATFORM = "macOS-arm64-static" +elif options.platform == "windows": + CVC5_PLATFORM = "Win64-x86_64-static" + CVC5_BINARY = "cvc5.exe" + CVC5_EXECUTABLE = False +else: + ap.error("unknown platform") + +print ("Downloading CVC5 archive (%s, %s)" % (CVC5_VERSION, CVC5_PLATFORM)) +with urllib.request.urlopen("%s/cvc5-%s/cvc5-%s.zip" % + (CVC5_RELEASES, + CVC5_VERSION, + CVC5_PLATFORM)) as fd: + content = fd.read() + +print ("Extracting %s" % CVC5_BINARY) +with zipfile.ZipFile(io.BytesIO(content)) as zf: + with zf.open("cvc5-%s/bin/%s" % (CVC5_PLATFORM, + CVC5_BINARY)) as fd: + with open(CVC5_BINARY, "wb") as fd_out: + fd_out.write(fd.read()) + +if CVC5_EXECUTABLE: + print("Setting executable bit") + os.chmod(CVC5_BINARY, stat.S_IRUSR | stat.S_IWUSR | stat.S_IXUSR) diff --git a/util/github_release.py b/util/github_release.py index 1f3cf38a..cd658d46 100644 --- a/util/github_release.py +++ b/util/github_release.py @@ -31,6 +31,7 @@ from trlc.version import TRLC_VERSION import util.changelog + def main(): username = os.environ.get("GITHUB_USERNAME", None) if username is None: @@ -59,5 +60,6 @@ def main(): r = requests.post(api_endpoint, auth=auth, data=json.dumps(data)) print(r) + if __name__ == "__main__": main()