Merge branch 'main' into iteration-api-by-section

.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

.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

.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

.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

.gitignore

@@ -19,3 +19,7 @@ dist
 
 # Build-System ignores
 bazel-*
+
+# Special ignores for CI
+cvc5
+cvc5.exe

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:
 

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",
 )

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

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)

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

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

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

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

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

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