Skip to content

Disallow nesting endpointExpr and chor #2692

Disallow nesting endpointExpr and chor

Disallow nesting endpointExpr and chor #2692

Triggered via push September 19, 2024 14:21
Status Failure
Total duration 23m 33s
Artifacts 13

scalatest.yml

on: push
Matrix: ScalaTest
ScalaTestWindowsBasic
7m 3s
ScalaTestWindowsBasic
ScalaTestMacOsBasic
7m 29s
ScalaTestMacOsBasic
GenerateTestReport
22s
GenerateTestReport
Fit to window
Zoom out
Zoom in

Annotations

20 errors and 28 warnings
ScalaTest (-n MATRIX[2])
Process completed with exit code 1.
ScalaTest (-n MATRIX[4])
Process completed with exit code 1.
ScalaTest (-n MATRIX[0])
Process completed with exit code 1.
ScalaTest (-n MATRIX[7])
Process completed with exit code 1.
ScalaTest (-n MATRIX[6])
Process completed with exit code 1.
ScalaTest (-n MATRIX[1])
Process completed with exit code 1.
ScalaTest (-n MATRIX[3])
Process completed with exit code 1.
ScalaTest (-n MATRIX[5])
Process completed with exit code 1.
vct.test.integration.examples.veymont.IFM2024VeyMontPermissionsSpec ► TTTlast case study (choreography verification) verifies with silicon: test/main/vct/test/integration/helper/VeyMontSpec.scala#L222
Failed test found in: reports/ubuntu-0/TEST-vct.test.integration.examples.veymont.IFM2024VeyMontPermissionsSpec.xml reports/ubuntu-1/TEST-vct.test.integration.examples.veymont.IFM2024VeyMontPermissionsSpec.xml reports/ubuntu-2/TEST-vct.test.integration.examples.veymont.IFM2024VeyMontPermissionsSpec.xml reports/ubuntu-5/TEST-vct.test.integration.examples.veymont.IFM2024VeyMontPermissionsSpec.xml reports/ubuntu-5/TEST-vct.test.integration.examples.veymont.IFM2024VeyMontPermissionsSpec.xml reports/ubuntu-6/TEST-vct.test.integration.examples.veymont.IFM2024VeyMontPermissionsSpec.xml Error: org.scalatest.exceptions.TestFailedException: Pass did not equal Error(choreography:resolutionError:endpointExprInChor,endpointExprInChor,endpointExprInChor,endpointExprInChor,endpointExprInChor,endpointExprInChor,endpointExprInChor,endpointExprInChor,endpointExprInChor)
vct.test.integration.examples.veymont.VeyMontExamplesSpec ► Tic-Tac-Toe (generated permissions) verifies with silicon: test/main/vct/test/integration/helper/VeyMontSpec.scala#L222
Failed test found in: reports/ubuntu-0/TEST-vct.test.integration.examples.veymont.VeyMontExamplesSpec.xml Error: org.scalatest.exceptions.TestFailedException: Pass did not equal Crash(vct.main.modes.VeyMont$WrapSystemError: The following error occurred during choreography verification:
vct.test.integration.examples.veymont.FM2023VeyMontSpec ► Files examples/publications/2023/FM2023VeyMont/applicability/2pc-5.pvl verifies with silicon: test/main/vct/test/integration/helper/VeyMontSpec.scala#L222
Failed test found in: reports/ubuntu-1/TEST-vct.test.integration.examples.veymont.FM2023VeyMontSpec.xml Error: org.scalatest.exceptions.TestFailedException: Pass did not equal Crash(vct.main.modes.VeyMont$WrapSystemError: The following error occurred during choreography verification:
vct.test.integration.examples.veymont.FM2023VeyMontSpec ► Files examples/publications/2023/FM2023VeyMont/applicability/consensus-3.pvl verifies with silicon: test/main/vct/test/integration/helper/VeyMontSpec.scala#L222
Failed test found in: reports/ubuntu-1/TEST-vct.test.integration.examples.veymont.FM2023VeyMontSpec.xml Error: org.scalatest.exceptions.TestFailedException: Pass did not equal Crash(vct.main.modes.VeyMont$WrapSystemError: The following error occurred during choreography verification:
vct.test.integration.examples.veymont.FM2023VeyMontSpec ► Files examples/publications/2023/FM2023VeyMont/applicability/election-5.pvl verifies with silicon: test/main/vct/test/integration/helper/VeyMontSpec.scala#L222
Failed test found in: reports/ubuntu-1/TEST-vct.test.integration.examples.veymont.FM2023VeyMontSpec.xml Error: org.scalatest.exceptions.TestFailedException: Pass did not equal Crash(vct.main.modes.VeyMont$WrapSystemError: The following error occurred during choreography verification:
vct.test.integration.examples.veymont.FM2023VeyMontSpec ► Files examples/publications/2023/FM2023VeyMont/applicability/consensus-5.pvl verifies with silicon: test/main/vct/test/integration/helper/VeyMontSpec.scala#L222
Failed test found in: reports/ubuntu-3/TEST-vct.test.integration.examples.veymont.FM2023VeyMontSpec.xml Error: org.scalatest.exceptions.TestFailedException: Pass did not equal Crash(vct.main.modes.VeyMont$WrapSystemError: The following error occurred during choreography verification:
vct.test.integration.examples.veymont.TechnicalVeyMontSpec ► Files examples/technical/veymont/checkLTS/ltstest.pvl verifies with silicon: test/main/vct/test/integration/helper/VeyMontSpec.scala#L222
Failed test found in: reports/ubuntu-3/TEST-vct.test.integration.examples.veymont.TechnicalVeyMontSpec.xml Error: org.scalatest.exceptions.TestFailedException: Pass did not equal Crash(vct.main.modes.VeyMont$WrapSystemError: The following error occurred during choreography verification:
vct.test.integration.examples.veymont.VeyMontExamplesSpec ► Leader elect ring (generated permissions) verifies with silicon: test/main/vct/test/integration/helper/VeyMontSpec.scala#L222
Failed test found in: reports/ubuntu-4/TEST-vct.test.integration.examples.veymont.VeyMontExamplesSpec.xml Error: org.scalatest.exceptions.TestFailedException: Pass did not equal Crash(vct.main.modes.VeyMont$WrapSystemError: The following error occurred during choreography verification:
vct.test.integration.examples.veymont.VeyMontExamplesSpec ► Parallel while (generated permissions) verifies with silicon: test/main/vct/test/integration/helper/VeyMontSpec.scala#L222
Failed test found in: reports/ubuntu-4/TEST-vct.test.integration.examples.veymont.VeyMontExamplesSpec.xml Error: org.scalatest.exceptions.TestFailedException: Pass did not equal Crash(vct.main.modes.VeyMont$WrapSystemError: The following error occurred during choreography verification:
vct.test.integration.examples.veymont.IFM2024VeyMontPermissionsSpec ► TTT case study (choreographic verification) verifies with silicon: test/main/vct/test/integration/helper/VeyMontSpec.scala#L222
Failed test found in: reports/ubuntu-5/TEST-vct.test.integration.examples.veymont.IFM2024VeyMontPermissionsSpec.xml Error: org.scalatest.exceptions.TestFailedException: Pass did not equal Crash(vct.main.modes.VeyMont$WrapSystemError: The following error occurred during choreography verification:
vct.test.integration.examples.veymont.TechnicalVeyMontSpec ► Files examples/technical/veymont/checkLTS/simpleifelse.pvl verifies with silicon: test/main/vct/test/integration/helper/VeyMontSpec.scala#L222
Failed test found in: reports/ubuntu-6/TEST-vct.test.integration.examples.veymont.TechnicalVeyMontSpec.xml Error: org.scalatest.exceptions.TestFailedException: Pass did not equal Crash(vct.main.modes.VeyMont$WrapSystemError: The following error occurred during choreography verification:
GenerateTestReport
Failed test were found and 'fail-on-error' option is set to true
Compile
The following actions uses node12 which is deprecated and will be forced to run on node16: actions/checkout@v2, actions/setup-java@v1. For more info: https://github.blog/changelog/2023-06-13-github-actions-all-actions-will-run-on-node16-instead-of-node12-by-default/
Compile
The following actions use a deprecated Node.js version and will be forced to run on node20: actions/checkout@v2, actions/setup-java@v1, actions/cache@v3, actions/upload-artifact@v3. For more info: https://github.blog/changelog/2024-03-07-github-actions-all-actions-will-run-on-node20-instead-of-node16-by-default/
ScalaTest (-l MATRIX)
The following actions uses node12 which is deprecated and will be forced to run on node16: actions/checkout@v2, actions/setup-java@v1. For more info: https://github.blog/changelog/2023-06-13-github-actions-all-actions-will-run-on-node16-instead-of-node12-by-default/
ScalaTest (-l MATRIX)
The following actions use a deprecated Node.js version and will be forced to run on node20: actions/checkout@v2, actions/setup-java@v1, actions/download-artifact@v3, actions/upload-artifact@v3. For more info: https://github.blog/changelog/2024-03-07-github-actions-all-actions-will-run-on-node20-instead-of-node16-by-default/
ScalaTest (-n MATRIX[2])
The following actions uses node12 which is deprecated and will be forced to run on node16: actions/checkout@v2, actions/setup-java@v1. For more info: https://github.blog/changelog/2023-06-13-github-actions-all-actions-will-run-on-node16-instead-of-node12-by-default/
ScalaTest (-n MATRIX[2])
The following actions use a deprecated Node.js version and will be forced to run on node20: actions/checkout@v2, actions/setup-java@v1, actions/download-artifact@v3, actions/upload-artifact@v3. For more info: https://github.blog/changelog/2024-03-07-github-actions-all-actions-will-run-on-node20-instead-of-node16-by-default/
ScalaTest (-n MATRIX[4])
The following actions uses node12 which is deprecated and will be forced to run on node16: actions/checkout@v2, actions/setup-java@v1. For more info: https://github.blog/changelog/2023-06-13-github-actions-all-actions-will-run-on-node16-instead-of-node12-by-default/
ScalaTest (-n MATRIX[4])
The following actions use a deprecated Node.js version and will be forced to run on node20: actions/checkout@v2, actions/setup-java@v1, actions/download-artifact@v3, actions/upload-artifact@v3. For more info: https://github.blog/changelog/2024-03-07-github-actions-all-actions-will-run-on-node20-instead-of-node16-by-default/
ScalaTest (-n MATRIX[0])
The following actions uses node12 which is deprecated and will be forced to run on node16: actions/checkout@v2, actions/setup-java@v1. For more info: https://github.blog/changelog/2023-06-13-github-actions-all-actions-will-run-on-node16-instead-of-node12-by-default/
ScalaTest (-n MATRIX[0])
The following actions use a deprecated Node.js version and will be forced to run on node20: actions/checkout@v2, actions/setup-java@v1, actions/download-artifact@v3, actions/upload-artifact@v3. For more info: https://github.blog/changelog/2024-03-07-github-actions-all-actions-will-run-on-node20-instead-of-node16-by-default/
ScalaTest (-n MATRIX[7])
The following actions uses node12 which is deprecated and will be forced to run on node16: actions/checkout@v2, actions/setup-java@v1. For more info: https://github.blog/changelog/2023-06-13-github-actions-all-actions-will-run-on-node16-instead-of-node12-by-default/
ScalaTest (-n MATRIX[7])
The following actions use a deprecated Node.js version and will be forced to run on node20: actions/checkout@v2, actions/setup-java@v1, actions/download-artifact@v3, actions/upload-artifact@v3. For more info: https://github.blog/changelog/2024-03-07-github-actions-all-actions-will-run-on-node20-instead-of-node16-by-default/
ScalaTest (-n MATRIX[6])
The following actions uses node12 which is deprecated and will be forced to run on node16: actions/checkout@v2, actions/setup-java@v1. For more info: https://github.blog/changelog/2023-06-13-github-actions-all-actions-will-run-on-node16-instead-of-node12-by-default/
ScalaTest (-n MATRIX[6])
The following actions use a deprecated Node.js version and will be forced to run on node20: actions/checkout@v2, actions/setup-java@v1, actions/download-artifact@v3, actions/upload-artifact@v3. For more info: https://github.blog/changelog/2024-03-07-github-actions-all-actions-will-run-on-node20-instead-of-node16-by-default/
ScalaTestWindowsBasic
The following actions uses node12 which is deprecated and will be forced to run on node16: actions/checkout@v2, actions/setup-java@v1, actions/cache@v2. For more info: https://github.blog/changelog/2023-06-13-github-actions-all-actions-will-run-on-node16-instead-of-node12-by-default/
ScalaTestWindowsBasic
The following actions use a deprecated Node.js version and will be forced to run on node20: actions/checkout@v2, actions/setup-java@v1, actions/cache@v2, actions/download-artifact@v3, actions/upload-artifact@v3. For more info: https://github.blog/changelog/2024-03-07-github-actions-all-actions-will-run-on-node20-instead-of-node16-by-default/
ScalaTestMacOsBasic
The following actions uses node12 which is deprecated and will be forced to run on node16: actions/checkout@v2, actions/setup-java@v1. For more info: https://github.blog/changelog/2023-06-13-github-actions-all-actions-will-run-on-node16-instead-of-node12-by-default/
ScalaTestMacOsBasic
The following actions use a deprecated Node.js version and will be forced to run on node20: actions/checkout@v2, actions/setup-java@v1, actions/download-artifact@v3, actions/upload-artifact@v3. For more info: https://github.blog/changelog/2024-03-07-github-actions-all-actions-will-run-on-node20-instead-of-node16-by-default/
ScalaTest (-n MATRIX[1])
The following actions uses node12 which is deprecated and will be forced to run on node16: actions/checkout@v2, actions/setup-java@v1. For more info: https://github.blog/changelog/2023-06-13-github-actions-all-actions-will-run-on-node16-instead-of-node12-by-default/
ScalaTest (-n MATRIX[1])
The following actions use a deprecated Node.js version and will be forced to run on node20: actions/checkout@v2, actions/setup-java@v1, actions/download-artifact@v3, actions/upload-artifact@v3. For more info: https://github.blog/changelog/2024-03-07-github-actions-all-actions-will-run-on-node20-instead-of-node16-by-default/
ScalaTest (-n MATRIX[3])
The following actions uses node12 which is deprecated and will be forced to run on node16: actions/checkout@v2, actions/setup-java@v1. For more info: https://github.blog/changelog/2023-06-13-github-actions-all-actions-will-run-on-node16-instead-of-node12-by-default/
ScalaTest (-n MATRIX[3])
The following actions use a deprecated Node.js version and will be forced to run on node20: actions/checkout@v2, actions/setup-java@v1, actions/download-artifact@v3, actions/upload-artifact@v3. For more info: https://github.blog/changelog/2024-03-07-github-actions-all-actions-will-run-on-node20-instead-of-node16-by-default/
ScalaTest (-n MATRIX[5])
The following actions uses node12 which is deprecated and will be forced to run on node16: actions/checkout@v2, actions/setup-java@v1. For more info: https://github.blog/changelog/2023-06-13-github-actions-all-actions-will-run-on-node16-instead-of-node12-by-default/
ScalaTest (-n MATRIX[5])
The following actions use a deprecated Node.js version and will be forced to run on node20: actions/checkout@v2, actions/setup-java@v1, actions/download-artifact@v3, actions/upload-artifact@v3. For more info: https://github.blog/changelog/2024-03-07-github-actions-all-actions-will-run-on-node20-instead-of-node16-by-default/
GenerateTestReport
The following actions uses node12 which is deprecated and will be forced to run on node16: actions/checkout@v2. For more info: https://github.blog/changelog/2023-06-13-github-actions-all-actions-will-run-on-node16-instead-of-node12-by-default/
GenerateTestReport
The following actions use a deprecated Node.js version and will be forced to run on node20: actions/checkout@v2, actions/download-artifact@v3. For more info: https://github.blog/changelog/2024-03-07-github-actions-all-actions-will-run-on-node20-instead-of-node16-by-default/
GenerateTestReport
Test report summary exceeded limit of 65535 bytes and will be trimmed
Deprecation notice: v1, v2, and v3 of the artifact actions
The following artifacts were uploaded using a version of actions/upload-artifact that is scheduled for deprecation: "allTests", "test-report-macos-latest", "test-report-ubuntu-latest--l MATRIX", "test-report-ubuntu-latest--n MATRIX[0]", "test-report-ubuntu-latest--n MATRIX[1]", "test-report-ubuntu-latest--n MATRIX[2]", "test-report-ubuntu-latest--n MATRIX[3]", "test-report-ubuntu-latest--n MATRIX[4]", "test-report-ubuntu-latest--n MATRIX[5]", "test-report-ubuntu-latest--n MATRIX[6]", "test-report-ubuntu-latest--n MATRIX[7]", "test-report-windows-latest", "vcllvm". Please update your workflow to use v4 of the artifact actions. Learn more: https://github.blog/changelog/2024-04-16-deprecation-notice-v3-of-the-artifact-actions/

Artifacts

Produced during runtime
Name Size
allTests
129 MB
test-report-macos-latest
22.3 KB
test-report-ubuntu-latest--l MATRIX
299 KB
test-report-ubuntu-latest--n MATRIX[0]
1.19 MB
test-report-ubuntu-latest--n MATRIX[1]
1.52 MB
test-report-ubuntu-latest--n MATRIX[2]
323 KB
test-report-ubuntu-latest--n MATRIX[3]
1.75 MB
test-report-ubuntu-latest--n MATRIX[4]
1.83 MB
test-report-ubuntu-latest--n MATRIX[5]
1.17 MB
test-report-ubuntu-latest--n MATRIX[6]
2.07 MB
test-report-ubuntu-latest--n MATRIX[7]
692 KB
test-report-windows-latest
24.7 KB
vcllvm
27.4 MB