Skip to content
Run ScalaTest

Last bit to support predicates as well #2703

Sign in to view logs

Last bit to support predicates as well

Last bit to support predicates as well #2703

GitHub Actions / TestReport failed Sep 24, 2024 in 0s

1052 passed, 7 failed and 44 skipped

Tests failed
Report exceeded GitHub limit of 65535 bytes and has been trimmed

Annotations

Check failure on line 222 in test/main/vct/test/integration/helper/VeyMontSpec.scala

See this annotation in the file changed.

@github-actions github-actions / TestReport

vct.test.integration.examples.veymont.IFM2024VeyMontPermissionsSpec ► TTTlast case study (choreography verification) verifies with silicon 

Failed test found in:
  reports/ubuntu-0/TEST-vct.test.integration.examples.veymont.IFM2024VeyMontPermissionsSpec.xml
Error:
        org.scalatest.exceptions.TestFailedException: Pass did not equal Fail(List(loopUnanimityNotMaintained))
Raw output 
      org.scalatest.exceptions.TestFailedException: Pass did not equal Fail(List(loopUnanimityNotMaintained))
Expected test result: pass
Actual test result: fail with code loopUnanimityNotMaintained
      at org.scalatest.Assertions.newAssertionFailedException(Assertions.scala:472)
      at org.scalatest.Assertions.newAssertionFailedException$(Assertions.scala:471)
      at org.scalatest.Assertions$.newAssertionFailedException(Assertions.scala:1231)
      at org.scalatest.Assertions$AssertionsHelper.macroAssert(Assertions.scala:1295)
      at vct.test.integration.helper.VeyMontSpec.processResult(VeyMontSpec.scala:222)
      at vct.test.integration.helper.VeyMontSpec.$anonfun$veymontTest$4(VeyMontSpec.scala:200)
      at scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.scala:18)
      at org.scalatest.enablers.Timed$$anon$1.timeoutAfter(Timed.scala:127)
      at org.scalatest.concurrent.TimeLimits$.failAfterImpl(TimeLimits.scala:282)
      at org.scalatest.concurrent.TimeLimits.failAfter(TimeLimits.scala:231)
      at org.scalatest.concurrent.TimeLimits.failAfter$(TimeLimits.scala:230)
      at org.scalatest.concurrent.TimeLimits$.failAfter(TimeLimits.scala:274)
      at vct.test.integration.helper.VeyMontSpec.$anonfun$veymontTest$3(VeyMontSpec.scala:190)
      at vct.test.integration.helper.VeyMontSpec.$anonfun$veymontTest$3$adapted(VeyMontSpec.scala:176)
      at hre.util.FilesHelper$.withTempDir(FilesHelper.scala:11)
      at vct.test.integration.helper.VeyMontSpec.$anonfun$veymontTest$2(VeyMontSpec.scala:176)
      at scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.scala:18)
      at org.scalatest.OutcomeOf.outcomeOf(OutcomeOf.scala:85)
      at org.scalatest.OutcomeOf.outcomeOf$(OutcomeOf.scala:83)
      at org.scalatest.OutcomeOf$.outcomeOf(OutcomeOf.scala:104)
      at org.scalatest.Transformer.apply(Transformer.scala:22)
      at org.scalatest.Transformer.apply(Transformer.scala:20)
      at org.scalatest.flatspec.AnyFlatSpecLike$$anon$5.apply(AnyFlatSpecLike.scala:1684)
      at org.scalatest.TestSuite.withFixture(TestSuite.scala:196)
      at org.scalatest.TestSuite.withFixture$(TestSuite.scala:195)
      at org.scalatest.flatspec.AnyFlatSpec.withFixture(AnyFlatSpec.scala:1685)
      at org.scalatest.flatspec.AnyFlatSpecLike.invokeWithFixture$1(AnyFlatSpecLike.scala:1682)
      at org.scalatest.flatspec.AnyFlatSpecLike.$anonfun$runTest$1(AnyFlatSpecLike.scala:1694)
      at org.scalatest.SuperEngine.runTestImpl(Engine.scala:306)
      at org.scalatest.flatspec.AnyFlatSpecLike.runTest(AnyFlatSpecLike.scala:1694)
      at org.scalatest.flatspec.AnyFlatSpecLike.runTest$(AnyFlatSpecLike.scala:1676)
      at org.scalatest.flatspec.AnyFlatSpec.runTest(AnyFlatSpec.scala:1685)
      at org.scalatest.flatspec.AnyFlatSpecLike.$anonfun$runTests$1(AnyFlatSpecLike.scala:1752)
      at org.scalatest.SuperEngine.$anonfun$runTestsInBranch$1(Engine.scala:413)
      at scala.collection.immutable.List.foreach(List.scala:333)
      at org.scalatest.SuperEngine.traverseSubNodes$1(Engine.scala:401)
      at org.scalatest.SuperEngine.runTestsInBranch(Engine.scala:396)
      at org.scalatest.SuperEngine.runTestsImpl(Engine.scala:475)
      at org.scalatest.flatspec.AnyFlatSpecLike.runTests(AnyFlatSpecLike.scala:1752)
      at org.scalatest.flatspec.AnyFlatSpecLike.runTests$(AnyFlatSpecLike.scala:1751)
      at org.scalatest.flatspec.AnyFlatSpec.runTests(AnyFlatSpec.scala:1685)
      at org.scalatest.Suite.run(Suite.scala:1112)
      at org.scalatest.Suite.run$(Suite.scala:1094)
      at org.scalatest.flatspec.AnyFlatSpec.org$scalatest$flatspec$AnyFlatSpecLike$$super$run(AnyFlatSpec.scala:1685)
      at org.scalatest.flatspec.AnyFlatSpecLike.$anonfun$run$1(AnyFlatSpecLike.scala:1797)
      at org.scalatest.SuperEngine.runImpl(Engine.scala:535)
      at org.scalatest.flatspec.AnyFlatSpecLike.run(AnyFlatSpecLike.scala:1797)
      at org.scalatest.flatspec.AnyFlatSpecLike.run$(AnyFlatSpecLike.scala:1795)
      at org.scalatest.flatspec.AnyFlatSpec.run(AnyFlatSpec.scala:1685)
      at org.scalatest.Suite.callExecuteOnSuite$1(Suite.scala:1175)
      at org.scalatest.Suite.$anonfun$runNestedSuites$1(Suite.scala:1222)
      at scala.collection.ArrayOps$.foreach$extension(ArrayOps.scala:1323)
      at org.scalatest.Suite.runNestedSuites(Suite.scala:1220)
      at org.scalatest.Suite.runNestedSuites$(Suite.scala:1154)
      at org.scalatest.tools.DiscoverySuite.runNestedSuites(DiscoverySuite.scala:30)
      at org.scalatest.Suite.run(Suite.scala:1109)
      at org.scalatest.Suite.run$(Suite.scala:1094)
      at org.scalatest.tools.DiscoverySuite.run(DiscoverySuite.scala:30)
      at org.scalatest.tools.SuiteRunner.run(SuiteRunner.scala:45)
      at org.scalatest.tools.Runner$.$anonfun$doRunRunRunDaDoRunRun$13(Runner.scala:1322)
      at org.scalatest.tools.Runner$.$anonfun$doRunRunRunDaDoRunRun$13$adapted(Runner.scala:1316)
      at scala.collection.immutable.List.foreach(List.scala:333)
      at org.scalatest.tools.Runner$.doRunRunRunDaDoRunRun(Runner.scala:1316)
      at org.scalatest.tools.Runner$.$anonfun$runOptionallyWithPassFailReporter$24(Runner.scala:993)
      at org.scalatest.tools.Runner$.$anonfun$runOptionallyWithPassFailReporter$24$adapted(Runner.scala:971)
      at org.scalatest.tools.Runner$.withClassLoaderAndDispatchReporter(Runner.scala:1482)
      at org.scalatest.tools.Runner$.runOptionallyWithPassFailReporter(Runner.scala:971)
      at org.scalatest.tools.Runner$.main(Runner.scala:775)
      at org.scalatest.tools.Runner.main(Runner.scala)

Check failure on line 222 in test/main/vct/test/integration/helper/VeyMontSpec.scala

See this annotation in the file changed.

@github-actions github-actions / TestReport

vct.test.integration.examples.veymont.IFM2024VeyMontPermissionsSpec ► TTTmsg case study (implementation execution) verifies with silicon 

Failed test found in:
  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
Error:
        org.scalatest.exceptions.TestFailedException: Pass did not equal Error(choreography:resolutionError:endpointExprInChor,endpointExprInChor,endpointExprInChor,endpointExprInChor,endpointExprInChor,endpointExprInChor,endpointExprInChor,endpointExprInChor,endpointExprInChor)
Raw output 
      org.scalatest.exceptions.TestFailedException: Pass did not equal Error(choreography:resolutionError:endpointExprInChor,endpointExprInChor,endpointExprInChor,endpointExprInChor,endpointExprInChor,endpointExprInChor,endpointExprInChor,endpointExprInChor,endpointExprInChor)
Expected test result: pass
Actual test result: error with code choreography:resolutionError:endpointExprInChor,endpointExprInChor,endpointExprInChor,endpointExprInChor,endpointExprInChor,endpointExprInChor,endpointExprInChor,endpointExprInChor,endpointExprInChor
      at org.scalatest.Assertions.newAssertionFailedException(Assertions.scala:472)
      at org.scalatest.Assertions.newAssertionFailedException$(Assertions.scala:471)
      at org.scalatest.Assertions$.newAssertionFailedException(Assertions.scala:1231)
      at org.scalatest.Assertions$AssertionsHelper.macroAssert(Assertions.scala:1295)
      at vct.test.integration.helper.VeyMontSpec.processResult(VeyMontSpec.scala:222)
      at vct.test.integration.helper.VeyMontSpec.$anonfun$veymontTest$4(VeyMontSpec.scala:200)
      at scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.scala:18)
      at org.scalatest.enablers.Timed$$anon$1.timeoutAfter(Timed.scala:127)
      at org.scalatest.concurrent.TimeLimits$.failAfterImpl(TimeLimits.scala:282)
      at org.scalatest.concurrent.TimeLimits.failAfter(TimeLimits.scala:231)
      at org.scalatest.concurrent.TimeLimits.failAfter$(TimeLimits.scala:230)
      at org.scalatest.concurrent.TimeLimits$.failAfter(TimeLimits.scala:274)
      at vct.test.integration.helper.VeyMontSpec.$anonfun$veymontTest$3(VeyMontSpec.scala:190)
      at vct.test.integration.helper.VeyMontSpec.$anonfun$veymontTest$3$adapted(VeyMontSpec.scala:176)
      at hre.util.FilesHelper$.withTempDir(FilesHelper.scala:11)
      at vct.test.integration.helper.VeyMontSpec.$anonfun$veymontTest$2(VeyMontSpec.scala:176)
      at scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.scala:18)
      at org.scalatest.OutcomeOf.outcomeOf(OutcomeOf.scala:85)
      at org.scalatest.OutcomeOf.outcomeOf$(OutcomeOf.scala:83)
      at org.scalatest.OutcomeOf$.outcomeOf(OutcomeOf.scala:104)
      at org.scalatest.Transformer.apply(Transformer.scala:22)
      at org.scalatest.Transformer.apply(Transformer.scala:20)
      at org.scalatest.flatspec.AnyFlatSpecLike$$anon$5.apply(AnyFlatSpecLike.scala:1684)
      at org.scalatest.TestSuite.withFixture(TestSuite.scala:196)
      at org.scalatest.TestSuite.withFixture$(TestSuite.scala:195)
      at org.scalatest.flatspec.AnyFlatSpec.withFixture(AnyFlatSpec.scala:1685)
      at org.scalatest.flatspec.AnyFlatSpecLike.invokeWithFixture$1(AnyFlatSpecLike.scala:1682)
      at org.scalatest.flatspec.AnyFlatSpecLike.$anonfun$runTest$1(AnyFlatSpecLike.scala:1694)
      at org.scalatest.SuperEngine.runTestImpl(Engine.scala:306)
      at org.scalatest.flatspec.AnyFlatSpecLike.runTest(AnyFlatSpecLike.scala:1694)
      at org.scalatest.flatspec.AnyFlatSpecLike.runTest$(AnyFlatSpecLike.scala:1676)
      at org.scalatest.flatspec.AnyFlatSpec.runTest(AnyFlatSpec.scala:1685)
      at org.scalatest.flatspec.AnyFlatSpecLike.$anonfun$runTests$1(AnyFlatSpecLike.scala:1752)
      at org.scalatest.SuperEngine.$anonfun$runTestsInBranch$1(Engine.scala:413)
      at scala.collection.immutable.List.foreach(List.scala:333)
      at org.scalatest.SuperEngine.traverseSubNodes$1(Engine.scala:401)
      at org.scalatest.SuperEngine.runTestsInBranch(Engine.scala:396)
      at org.scalatest.SuperEngine.runTestsImpl(Engine.scala:475)
      at org.scalatest.flatspec.AnyFlatSpecLike.runTests(AnyFlatSpecLike.scala:1752)
      at org.scalatest.flatspec.AnyFlatSpecLike.runTests$(AnyFlatSpecLike.scala:1751)
      at org.scalatest.flatspec.AnyFlatSpec.runTests(AnyFlatSpec.scala:1685)
      at org.scalatest.Suite.run(Suite.scala:1112)
      at org.scalatest.Suite.run$(Suite.scala:1094)
      at org.scalatest.flatspec.AnyFlatSpec.org$scalatest$flatspec$AnyFlatSpecLike$$super$run(AnyFlatSpec.scala:1685)
      at org.scalatest.flatspec.AnyFlatSpecLike.$anonfun$run$1(AnyFlatSpecLike.scala:1797)
      at org.scalatest.SuperEngine.runImpl(Engine.scala:535)
      at org.scalatest.flatspec.AnyFlatSpecLike.run(AnyFlatSpecLike.scala:1797)
      at org.scalatest.flatspec.AnyFlatSpecLike.run$(AnyFlatSpecLike.scala:1795)
      at org.scalatest.flatspec.AnyFlatSpec.run(AnyFlatSpec.scala:1685)
      at org.scalatest.Suite.callExecuteOnSuite$1(Suite.scala:1175)
      at org.scalatest.Suite.$anonfun$runNestedSuites$1(Suite.scala:1222)
      at scala.collection.ArrayOps$.foreach$extension(ArrayOps.scala:1323)
      at org.scalatest.Suite.runNestedSuites(Suite.scala:1220)
      at org.scalatest.Suite.runNestedSuites$(Suite.scala:1154)
      at org.scalatest.tools.DiscoverySuite.runNestedSuites(DiscoverySuite.scala:30)
      at org.scalatest.Suite.run(Suite.scala:1109)
      at org.scalatest.Suite.run$(Suite.scala:1094)
      at org.scalatest.tools.DiscoverySuite.run(DiscoverySuite.scala:30)
      at org.scalatest.tools.SuiteRunner.run(SuiteRunner.scala:45)
      at org.scalatest.tools.Runner$.$anonfun$doRunRunRunDaDoRunRun$13(Runner.scala:1322)
      at org.scalatest.tools.Runner$.$anonfun$doRunRunRunDaDoRunRun$13$adapted(Runner.scala:1316)
      at scala.collection.immutable.List.foreach(List.scala:333)
      at org.scalatest.tools.Runner$.doRunRunRunDaDoRunRun(Runner.scala:1316)
      at org.scalatest.tools.Runner$.$anonfun$runOptionallyWithPassFailReporter$24(Runner.scala:993)
      at org.scalatest.tools.Runner$.$anonfun$runOptionallyWithPassFailReporter$24$adapted(Runner.scala:971)
      at org.scalatest.tools.Runner$.withClassLoaderAndDispatchReporter(Runner.scala:1482)
      at org.scalatest.tools.Runner$.runOptionallyWithPassFailReporter(Runner.scala:971)
      at org.scalatest.tools.Runner$.main(Runner.scala:775)
      at org.scalatest.tools.Runner.main(Runner.scala)

Check failure on line 222 in test/main/vct/test/integration/helper/VeyMontSpec.scala

See this annotation in the file changed.

@github-actions github-actions / TestReport

vct.test.integration.examples.veymont.IFM2024VeyMontPermissionsSpec ► TTT case study (choreographic verification) verifies with silicon 

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:
Raw output 
      org.scalatest.exceptions.TestFailedException: Pass did not equal Crash(vct.main.modes.VeyMont$WrapSystemError: The following error occurred during choreography verification:
Internal type error: CoercionErrors must not bubble. Expression `TicTacToeAnnotations_1830103279(P1_1528702755, P2_380858853)` could not be coerced to `boolean``)
Expected test result: pass
Actual test result: crash with message:
The following error occurred during choreography verification:
Internal type error: CoercionErrors must not bubble. Expression `TicTacToeAnnotations_1830103279(P1_1528702755, P2_380858853)` could not be coerced to `boolean``
      at org.scalatest.Assertions.newAssertionFailedException(Assertions.scala:472)
      at org.scalatest.Assertions.newAssertionFailedException$(Assertions.scala:471)
      at org.scalatest.Assertions$.newAssertionFailedException(Assertions.scala:1231)
      at org.scalatest.Assertions$AssertionsHelper.macroAssert(Assertions.scala:1295)
      at vct.test.integration.helper.VeyMontSpec.processResult(VeyMontSpec.scala:222)
      at vct.test.integration.helper.VeyMontSpec.$anonfun$veymontTest$4(VeyMontSpec.scala:200)
      at scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.scala:18)
      at org.scalatest.enablers.Timed$$anon$1.timeoutAfter(Timed.scala:127)
      at org.scalatest.concurrent.TimeLimits$.failAfterImpl(TimeLimits.scala:282)
      at org.scalatest.concurrent.TimeLimits.failAfter(TimeLimits.scala:231)
      at org.scalatest.concurrent.TimeLimits.failAfter$(TimeLimits.scala:230)
      at org.scalatest.concurrent.TimeLimits$.failAfter(TimeLimits.scala:274)
      at vct.test.integration.helper.VeyMontSpec.$anonfun$veymontTest$3(VeyMontSpec.scala:190)
      at vct.test.integration.helper.VeyMontSpec.$anonfun$veymontTest$3$adapted(VeyMontSpec.scala:176)
      at hre.util.FilesHelper$.withTempDir(FilesHelper.scala:11)
      at vct.test.integration.helper.VeyMontSpec.$anonfun$veymontTest$2(VeyMontSpec.scala:176)
      at scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.scala:18)
      at org.scalatest.OutcomeOf.outcomeOf(OutcomeOf.scala:85)
      at org.scalatest.OutcomeOf.outcomeOf$(OutcomeOf.scala:83)
      at org.scalatest.OutcomeOf$.outcomeOf(OutcomeOf.scala:104)
      at org.scalatest.Transformer.apply(Transformer.scala:22)
      at org.scalatest.Transformer.apply(Transformer.scala:20)
      at org.scalatest.flatspec.AnyFlatSpecLike$$anon$5.apply(AnyFlatSpecLike.scala:1684)
      at org.scalatest.TestSuite.withFixture(TestSuite.scala:196)
      at org.scalatest.TestSuite.withFixture$(TestSuite.scala:195)
      at org.scalatest.flatspec.AnyFlatSpec.withFixture(AnyFlatSpec.scala:1685)
      at org.scalatest.flatspec.AnyFlatSpecLike.invokeWithFixture$1(AnyFlatSpecLike.scala:1682)
      at org.scalatest.flatspec.AnyFlatSpecLike.$anonfun$runTest$1(AnyFlatSpecLike.scala:1694)
      at org.scalatest.SuperEngine.runTestImpl(Engine.scala:306)
      at org.scalatest.flatspec.AnyFlatSpecLike.runTest(AnyFlatSpecLike.scala:1694)
      at org.scalatest.flatspec.AnyFlatSpecLike.runTest$(AnyFlatSpecLike.scala:1676)
      at org.scalatest.flatspec.AnyFlatSpec.runTest(AnyFlatSpec.scala:1685)
      at org.scalatest.flatspec.AnyFlatSpecLike.$anonfun$runTests$1(AnyFlatSpecLike.scala:1752)
      at org.scalatest.SuperEngine.$anonfun$runTestsInBranch$1(Engine.scala:413)
      at scala.collection.immutable.List.foreach(List.scala:333)
      at org.scalatest.SuperEngine.traverseSubNodes$1(Engine.scala:401)
      at org.scalatest.SuperEngine.runTestsInBranch(Engine.scala:396)
      at org.scalatest.SuperEngine.runTestsImpl(Engine.scala:475)
      at org.scalatest.flatspec.AnyFlatSpecLike.runTests(AnyFlatSpecLike.scala:1752)
      at org.scalatest.flatspec.AnyFlatSpecLike.runTests$(AnyFlatSpecLike.scala:1751)
      at org.scalatest.flatspec.AnyFlatSpec.runTests(AnyFlatSpec.scala:1685)
      at org.scalatest.Suite.run(Suite.scala:1112)
      at org.scalatest.Suite.run$(Suite.scala:1094)
      at org.scalatest.flatspec.AnyFlatSpec.org$scalatest$flatspec$AnyFlatSpecLike$$super$run(AnyFlatSpec.scala:1685)
      at org.scalatest.flatspec.AnyFlatSpecLike.$anonfun$run$1(AnyFlatSpecLike.scala:1797)
      at org.scalatest.SuperEngine.runImpl(Engine.scala:535)
      at org.scalatest.flatspec.AnyFlatSpecLike.run(AnyFlatSpecLike.scala:1797)
      at org.scalatest.flatspec.AnyFlatSpecLike.run$(AnyFlatSpecLike.scala:1795)
      at org.scalatest.flatspec.AnyFlatSpec.run(AnyFlatSpec.scala:1685)
      at org.scalatest.Suite.callExecuteOnSuite$1(Suite.scala:1175)
      at org.scalatest.Suite.$anonfun$runNestedSuites$1(Suite.scala:1222)
      at scala.collection.ArrayOps$.foreach$extension(ArrayOps.scala:1323)
      at org.scalatest.Suite.runNestedSuites(Suite.scala:1220)
      at org.scalatest.Suite.runNestedSuites$(Suite.scala:1154)
      at org.scalatest.tools.DiscoverySuite.runNestedSuites(DiscoverySuite.scala:30)
      at org.scalatest.Suite.run(Suite.scala:1109)
      at org.scalatest.Suite.run$(Suite.scala:1094)
      at org.scalatest.tools.DiscoverySuite.run(DiscoverySuite.scala:30)
      at org.scalatest.tools.SuiteRunner.run(SuiteRunner.scala:45)
      at org.scalatest.tools.Runner$.$anonfun$doRunRunRunDaDoRunRun$13(Runner.scala:1322)
      at org.scalatest.tools.Runner$.$anonfun$doRunRunRunDaDoRunRun$13$adapted(Runner.scala:1316)
      at scala.collection.immutable.List.foreach(List.scala:333)
      at org.scalatest.tools.Runner$.doRunRunRunDaDoRunRun(Runner.scala:1316)
      at org.scalatest.tools.Runner$.$anonfun$runOptionallyWithPassFailReporter$24(Runner.scala:993)
      at org.scalatest.tools.Runner$.$anonfun$runOptionallyWithPassFailReporter$24$adapted(Runner.scala:971)
      at org.scalatest.tools.Runner$.withClassLoaderAndDispatchReporter(Runner.scala:1482)
      at org.scalatest.tools.Runner$.runOptionallyWithPassFailReporter(Runner.scala:971)
      at org.scalatest.tools.Runner$.main(Runner.scala:775)
      at org.scalatest.tools.Runner.main(Runner.scala)

Check failure on line 192 in test/main/vct/test/integration/examples/veymont/IFM2024VeyMontPermissionsSpec.scala

See this annotation in the file changed.

@github-actions github-actions / TestReport

vct.test.integration.examples.veymont.IFM2024VeyMontPermissionsSpec ► TTTlast case study (implementation execution) verifies with silicon 

Failed test found in:
  reports/ubuntu-6/TEST-vct.test.integration.examples.veymont.IFM2024VeyMontPermissionsSpec.xml
Error:
        java.lang.ClassNotFoundException: MyScriptContainer
Raw output 
      java.lang.ClassNotFoundException: MyScriptContainer
      at java.base/java.net.URLClassLoader.findClass(URLClassLoader.java:445)
      at java.base/java.lang.ClassLoader.loadClass(ClassLoader.java:592)
      at java.base/java.net.FactoryURLClassLoader.loadClass(URLClassLoader.java:872)
      at java.base/java.lang.ClassLoader.loadClass(ClassLoader.java:525)
      at java.base/java.lang.Class.forName0(Native Method)
      at java.base/java.lang.Class.forName(Class.java:467)
      at vct.test.integration.examples.veymont.IFM2024VeyMontPermissionsSpec.runJava(IFM2024VeyMontPermissionsSpec.scala:192)
      at vct.test.integration.examples.veymont.IFM2024VeyMontPermissionsSpec.runTttImplementation(IFM2024VeyMontPermissionsSpec.scala:146)
      at vct.test.integration.examples.veymont.IFM2024VeyMontPermissionsSpec.$anonfun$new$2(IFM2024VeyMontPermissionsSpec.scala:126)
      at vct.test.integration.examples.veymont.IFM2024VeyMontPermissionsSpec.$anonfun$new$2$adapted(IFM2024VeyMontPermissionsSpec.scala:126)
      at vct.test.integration.helper.VeyMontSpec.$anonfun$veymontTest$5(VeyMontSpec.scala:202)
      at vct.test.integration.helper.VeyMontSpec.$anonfun$veymontTest$5$adapted(VeyMontSpec.scala:202)
      at scala.Option.foreach(Option.scala:437)
      at vct.test.integration.helper.VeyMontSpec.$anonfun$veymontTest$4(VeyMontSpec.scala:202)
      at scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.scala:18)
      at org.scalatest.enablers.Timed$$anon$1.timeoutAfter(Timed.scala:127)
      at org.scalatest.concurrent.TimeLimits$.failAfterImpl(TimeLimits.scala:282)
      at org.scalatest.concurrent.TimeLimits.failAfter(TimeLimits.scala:231)
      at org.scalatest.concurrent.TimeLimits.failAfter$(TimeLimits.scala:230)
      at org.scalatest.concurrent.TimeLimits$.failAfter(TimeLimits.scala:274)
      at vct.test.integration.helper.VeyMontSpec.$anonfun$veymontTest$3(VeyMontSpec.scala:190)
      at vct.test.integration.helper.VeyMontSpec.$anonfun$veymontTest$3$adapted(VeyMontSpec.scala:176)
      at hre.util.FilesHelper$.withTempDir(FilesHelper.scala:11)
      at vct.test.integration.helper.VeyMontSpec.$anonfun$veymontTest$2(VeyMontSpec.scala:176)
      at scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.scala:18)
      at org.scalatest.OutcomeOf.outcomeOf(OutcomeOf.scala:85)
      at org.scalatest.OutcomeOf.outcomeOf$(OutcomeOf.scala:83)
      at org.scalatest.OutcomeOf$.outcomeOf(OutcomeOf.scala:104)
      at org.scalatest.Transformer.apply(Transformer.scala:22)
      at org.scalatest.Transformer.apply(Transformer.scala:20)
      at org.scalatest.flatspec.AnyFlatSpecLike$$anon$5.apply(AnyFlatSpecLike.scala:1684)
      at org.scalatest.TestSuite.withFixture(TestSuite.scala:196)
      at org.scalatest.TestSuite.withFixture$(TestSuite.scala:195)
      at org.scalatest.flatspec.AnyFlatSpec.withFixture(AnyFlatSpec.scala:1685)
      at org.scalatest.flatspec.AnyFlatSpecLike.invokeWithFixture$1(AnyFlatSpecLike.scala:1682)
      at org.scalatest.flatspec.AnyFlatSpecLike.$anonfun$runTest$1(AnyFlatSpecLike.scala:1694)
      at org.scalatest.SuperEngine.runTestImpl(Engine.scala:306)
      at org.scalatest.flatspec.AnyFlatSpecLike.runTest(AnyFlatSpecLike.scala:1694)
      at org.scalatest.flatspec.AnyFlatSpecLike.runTest$(AnyFlatSpecLike.scala:1676)
      at org.scalatest.flatspec.AnyFlatSpec.runTest(AnyFlatSpec.scala:1685)
      at org.scalatest.flatspec.AnyFlatSpecLike.$anonfun$runTests$1(AnyFlatSpecLike.scala:1752)
      at org.scalatest.SuperEngine.$anonfun$runTestsInBranch$1(Engine.scala:413)
      at scala.collection.immutable.List.foreach(List.scala:333)
      at org.scalatest.SuperEngine.traverseSubNodes$1(Engine.scala:401)
      at org.scalatest.SuperEngine.runTestsInBranch(Engine.scala:396)
      at org.scalatest.SuperEngine.runTestsImpl(Engine.scala:475)
      at org.scalatest.flatspec.AnyFlatSpecLike.runTests(AnyFlatSpecLike.scala:1752)
      at org.scalatest.flatspec.AnyFlatSpecLike.runTests$(AnyFlatSpecLike.scala:1751)
      at org.scalatest.flatspec.AnyFlatSpec.runTests(AnyFlatSpec.scala:1685)
      at org.scalatest.Suite.run(Suite.scala:1112)
      at org.scalatest.Suite.run$(Suite.scala:1094)
      at org.scalatest.flatspec.AnyFlatSpec.org$scalatest$flatspec$AnyFlatSpecLike$$super$run(AnyFlatSpec.scala:1685)
      at org.scalatest.flatspec.AnyFlatSpecLike.$anonfun$run$1(AnyFlatSpecLike.scala:1797)
      at org.scalatest.SuperEngine.runImpl(Engine.scala:535)
      at org.scalatest.flatspec.AnyFlatSpecLike.run(AnyFlatSpecLike.scala:1797)
      at org.scalatest.flatspec.AnyFlatSpecLike.run$(AnyFlatSpecLike.scala:1795)
      at org.scalatest.flatspec.AnyFlatSpec.run(AnyFlatSpec.scala:1685)
      at org.scalatest.Suite.callExecuteOnSuite$1(Suite.scala:1175)
      at org.scalatest.Suite.$anonfun$runNestedSuites$1(Suite.scala:1222)
      at scala.collection.ArrayOps$.foreach$extension(ArrayOps.scala:1323)
      at org.scalatest.Suite.runNestedSuites(Suite.scala:1220)
      at org.scalatest.Suite.runNestedSuites$(Suite.scala:1154)
      at org.scalatest.tools.DiscoverySuite.runNestedSuites(DiscoverySuite.scala:30)
      at org.scalatest.Suite.run(Suite.scala:1109)
      at org.scalatest.Suite.run$(Suite.scala:1094)
      at org.scalatest.tools.DiscoverySuite.run(DiscoverySuite.scala:30)
      at org.scalatest.tools.SuiteRunner.run(SuiteRunner.scala:45)
      at org.scalatest.tools.Runner$.$anonfun$doRunRunRunDaDoRunRun$13(Runner.scala:1322)
      at org.scalatest.tools.Runner$.$anonfun$doRunRunRunDaDoRunRun$13$adapted(Runner.scala:1316)
      at scala.collection.immutable.List.foreach(List.scala:333)
      at org.scalatest.tools.Runner$.doRunRunRunDaDoRunRun(Runner.scala:1316)
      at org.scalatest.tools.Runner$.$anonfun$runOptionallyWithPassFailReporter$24(Runner.scala:993)
      at org.scalatest.tools.Runner$.$anonfun$runOptionallyWithPassFailReporter$24$adapted(Runner.scala:971)
      at org.scalatest.tools.Runner$.withClassLoaderAndDispatchReporter(Runner.scala:1482)
      at org.scalatest.tools.Runner$.runOptionallyWithPassFailReporter(Runner.scala:971)
      at org.scalatest.tools.Runner$.main(Runner.scala:775)
      at org.scalatest.tools.Runner.main(Runner.scala)

Check failure on line 222 in test/main/vct/test/integration/helper/VeyMontSpec.scala

See this annotation in the file changed.

@github-actions github-actions / TestReport

vct.test.integration.examples.veymont.VeyMontExamplesSpec ► Leader elect star (generated permissions) verifies with silicon 

Failed test found in:
  reports/ubuntu-6/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:
Raw output 
      org.scalatest.exceptions.TestFailedException: Pass did not equal Crash(vct.main.modes.VeyMont$WrapSystemError: The following error occurred during choreography verification:
Internal type error: CoercionErrors must not bubble. Expression `(C_1333186355.N_489475072 == 0 ==>
    A_1872749322.MaxVal_1588928862 == A_1872749322.Rank_507697652 &&
        B_2084584028.MaxVal_1588928862 == B_2084584028.Rank_507697652 &&
        C_1333186355.MaxVal_1566112771 == C_1333186355.Rank_620259180 &&
        D_809897193.MaxVal_1588928862 == D_809897193.Rank_507697652) **
    (C_1333186355.N_489475072 == 1 ==>
        (C_1333186355.Rank_620259180 > A_1872749322.Rank_507697652
            ? A_1872749322.MaxVal_1588928862 == C_1333186355.Rank_620259180
            : A_1872749322.MaxVal_1588928862 == A_1872749322.Rank_507697652)) **
    (C_1333186355.N_489475072 == 1 ==>
        (C_1333186355.Rank_620259180 > B_2084584028.Rank_507697652
            ? B_2084584028.MaxVal_1588928862 == C_1333186355.Rank_620259180
            : B_2084584028.MaxVal_1588928862 == B_2084584028.Rank_507697652)) **
    (C_1333186355.N_489475072 == 1 ==>
        (C_1333186355.Rank_620259180 > D_809897193.Rank_507697652
            ? D_809897193.MaxVal_1588928862 == C_1333186355.Rank_620259180
            : D_809897193.MaxVal_1588928862 == D_809897193.Rank_507697652)) **
    (C_1333186355.N_489475072 >= 1 ==>
        C_1333186355.MaxVal_1566112771 ==
            C_1333186355.MaxVal_116384706(
                A_1872749322.Rank_507697652,
                B_2084584028.Rank_507697652,
                D_809897193.Rank_507697652,
                C_1333186355.Rank_620259180
            )) **
    (C_1333186355.N_489475072 == 2 ==>
        A_1872749322.MaxVal_1588928862 ==
            C_1333186355.MaxVal_116384706(
                A_1872749322.Rank_507697652,
                B_2084584028.Rank_507697652,
                D_809897193.Rank_507697652,
                C_1333186355.Rank_620259180
            )) **
    (C_1333186355.N_489475072 == 2 ==>
        B_2084584028.MaxVal_1588928862 ==
            C_1333186355.MaxVal_116384706(
                A_1872749322.Rank_507697652,
                B_2084584028.Rank_507697652,
                D_809897193.Rank_507697652,
                C_1333186355.Rank_620259180
            )) **
    (C_1333186355.N_489475072 == 2 ==>
        D_809897193.MaxVal_1588928862 ==
            C_1333186355.MaxVal_116384706(
                A_1872749322.Rank_507697652,
                B_2084584028.Rank_507697652,
                D_809897193.Rank_507697652,
                C_1333186355.Rank_620259180
            )) **
    A_1872749322.N_2047741270 < 2 == B_2084584028.N_2047741270 < 2 **
    B_2084584028.N_2047741270 < 2 == D_809897193.N_2047741270 < 2 **
    D_809897193.N_2047741270 < 2 == C_1333186355.N_489475072 < 2` could not be coerced to `boolean``)
Expected test result: pass
Actual test result: crash with message:
The following error occurred during choreography verification:
Internal type error: CoercionErrors must not bubble. Expression `(C_1333186355.N_489475072 == 0 ==>
    A_1872749322.MaxVal_1588928862 == A_1872749322.Rank_507697652 &&
        B_2084584028.MaxVal_1588928862 == B_2084584028.Rank_507697652 &&
        C_1333186355.MaxVal_1566112771 == C_1333186355.Rank_620259180 &&
        D_809897193.MaxVal_1588928862 == D_809897193.Rank_507697652) **
    (C_1333186355.N_489475072 == 1 ==>
        (C_1333186355.Rank_620259180 > A_1872749322.Rank_507697652
            ? A_1872749322.MaxVal_1588928862 == C_1333186355.Rank_620259180
            : A_1872749322.MaxVal_1588928862 == A_1872749322.Rank_507697652)) **
    (C_1333186355.N_489475072 == 1 ==>
        (C_1333186355.Rank_620259180 > B_2084584028.Rank_507697652
            ? B_2084584028.MaxVal_1588928862 == C_1333186355.Rank_620259180
            : B_2084584028.MaxVal_1588928862 == B_2084584028.Rank_507697652)) **
    (C_1333186355.N_489475072 == 1 ==>
        (C_1333186355.Rank_620259180 > D_809897193.Rank_507697652
            ? D_809897193.MaxVal_1588928862 == C_1333186355.Rank_620259180
            : D_809897193.MaxVal_1588928862 == D_809897193.Rank_507697652)) **
    (C_1333186355.N_489475072 >= 1 ==>
        C_1333186355.MaxVal_1566112771 ==
            C_1333186355.MaxVal_116384706(
                A_1872749322.Rank_507697652,
                B_2084584028.Rank_507697652,
                D_809897193.Rank_507697652,
                C_1333186355.Rank_620259180
            )) **
    (C_1333186355.N_489475072 == 2 ==>
        A_1872749322.MaxVal_1588928862 ==
            C_1333186355.MaxVal_116384706(
                A_1872749322.Rank_507697652,
                B_2084584028.Rank_507697652,
                D_809897193.Rank_507697652,
                C_1333186355.Rank_620259180
            )) **
    (C_1333186355.N_489475072 == 2 ==>
        B_2084584028.MaxVal_1588928862 ==
            C_1333186355.MaxVal_116384706(
                A_1872749322.Rank_507697652,
                B_2084584028.Rank_507697652,
                D_809897193.Rank_507697652,
                C_1333186355.Rank_620259180
            )) **
    (C_1333186355.N_489475072 == 2 ==>
        D_809897193.MaxVal_1588928862 ==
            C_1333186355.MaxVal_116384706(
                A_1872749322.Rank_507697652,
                B_2084584028.Rank_507697652,
                D_809897193.Rank_507697652,
                C_1333186355.Rank_620259180
            )) **
    A_1872749322.N_2047741270 < 2 == B_2084584028.N_2047741270 < 2 **
    B_2084584028.N_2047741270 < 2 == D_809897193.N_2047741270 < 2 **
    D_809897193.N_2047741270 < 2 == C_1333186355.N_489475072 < 2` could not be coerced to `boolean``
      at org.scalatest.Assertions.newAssertionFailedException(Assertions.scala:472)
      at org.scalatest.Assertions.newAssertionFailedException$(Assertions.scala:471)
      at org.scalatest.Assertions$.newAssertionFailedException(Assertions.scala:1231)
      at org.scalatest.Assertions$AssertionsHelper.macroAssert(Assertions.scala:1295)
      at vct.test.integration.helper.VeyMontSpec.processResult(VeyMontSpec.scala:222)
      at vct.test.integration.helper.VeyMontSpec.$anonfun$veymontTest$4(VeyMontSpec.scala:200)
      at scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.scala:18)
      at org.scalatest.enablers.Timed$$anon$1.timeoutAfter(Timed.scala:127)
      at org.scalatest.concurrent.TimeLimits$.failAfterImpl(TimeLimits.scala:282)
      at org.scalatest.concurrent.TimeLimits.failAfter(TimeLimits.scala:231)
      at org.scalatest.concurrent.TimeLimits.failAfter$(TimeLimits.scala:230)
      at org.scalatest.concurrent.TimeLimits$.failAfter(TimeLimits.scala:274)
      at vct.test.integration.helper.VeyMontSpec.$anonfun$veymontTest$3(VeyMontSpec.scala:190)
      at vct.test.integration.helper.VeyMontSpec.$anonfun$veymontTest$3$adapted(VeyMontSpec.scala:176)
      at hre.util.FilesHelper$.withTempDir(FilesHelper.scala:11)
      at vct.test.integration.helper.VeyMontSpec.$anonfun$veymontTest$2(VeyMontSpec.scala:176)
      at scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.scala:18)
      at org.scalatest.OutcomeOf.outcomeOf(OutcomeOf.scala:85)
      at org.scalatest.OutcomeOf.outcomeOf$(OutcomeOf.scala:83)
      at org.scalatest.OutcomeOf$.outcomeOf(OutcomeOf.scala:104)
      at org.scalatest.Transformer.apply(Transformer.scala:22)
      at org.scalatest.Transformer.apply(Transformer.scala:20)
      at org.scalatest.flatspec.AnyFlatSpecLike$$anon$5.apply(AnyFlatSpecLike.scala:1684)
      at org.scalatest.TestSuite.withFixture(TestSuite.scala:196)
      at org.scalatest.TestSuite.withFixture$(TestSuite.scala:195)
      at org.scalatest.flatspec.AnyFlatSpec.withFixture(AnyFlatSpec.scala:1685)
      at org.scalatest.flatspec.AnyFlatSpecLike.invokeWithFixture$1(AnyFlatSpecLike.scala:1682)
      at org.scalatest.flatspec.AnyFlatSpecLike.$anonfun$runTest$1(AnyFlatSpecLike.scala:1694)
      at org.scalatest.SuperEngine.runTestImpl(Engine.scala:306)
      at org.scalatest.flatspec.AnyFlatSpecLike.runTest(AnyFlatSpecLike.scala:1694)
      at org.scalatest.flatspec.AnyFlatSpecLike.runTest$(AnyFlatSpecLike.scala:1676)
      at org.scalatest.flatspec.AnyFlatSpec.runTest(AnyFlatSpec.scala:1685)
      at org.scalatest.flatspec.AnyFlatSpecLike.$anonfun$runTests$1(AnyFlatSpecLike.scala:1752)
      at org.scalatest.SuperEngine.$anonfun$runTestsInBranch$1(Engine.scala:413)
      at scala.collection.immutable.List.foreach(List.scala:333)
      at org.scalatest.SuperEngine.traverseSubNodes$1(Engine.scala:401)
      at org.scalatest.SuperEngine.runTestsInBranch(Engine.scala:396)
      at org.scalatest.SuperEngine.runTestsImpl(Engine.scala:475)
      at org.scalatest.flatspec.AnyFlatSpecLike.runTests(AnyFlatSpecLike.scala:1752)
      at org.scalatest.flatspec.AnyFlatSpecLike.runTests$(AnyFlatSpecLike.scala:1751)
      at org.scalatest.flatspec.AnyFlatSpec.runTests(AnyFlatSpec.scala:1685)
      at org.scalatest.Suite.run(Suite.scala:1112)
      at org.scalatest.Suite.run$(Suite.scala:1094)
      at org.scalatest.flatspec.AnyFlatSpec.org$scalatest$flatspec$AnyFlatSpecLike$$super$run(AnyFlatSpec.scala:1685)
      at org.scalatest.flatspec.AnyFlatSpecLike.$anonfun$run$1(AnyFlatSpecLike.scala:1797)
      at org.scalatest.SuperEngine.runImpl(Engine.scala:535)
      at org.scalatest.flatspec.AnyFlatSpecLike.run(AnyFlatSpecLike.scala:1797)
      at org.scalatest.flatspec.AnyFlatSpecLike.run$(AnyFlatSpecLike.scala:1795)
      at org.scalatest.flatspec.AnyFlatSpec.run(AnyFlatSpec.scala:1685)
      at org.scalatest.Suite.callExecuteOnSuite$1(Suite.scala:1175)
      at org.scalatest.Suite.$anonfun$runNestedSuites$1(Suite.scala:1222)
      at scala.collection.ArrayOps$.foreach$extension(ArrayOps.scala:1323)
      at org.scalatest.Suite.runNestedSuites(Suite.scala:1220)
      at org.scalatest.Suite.runNestedSuites$(Suite.scala:1154)
      at org.scalatest.tools.DiscoverySuite.runNestedSuites(DiscoverySuite.scala:30)
      at org.scalatest.Suite.run(Suite.scala:1109)
      at org.scalatest.Suite.run$(Suite.scala:1094)
      at org.scalatest.tools.DiscoverySuite.run(DiscoverySuite.scala:30)
      at org.scalatest.tools.SuiteRunner.run(SuiteRunner.scala:45)
      at org.scalatest.tools.Runner$.$anonfun$doRunRunRunDaDoRunRun$13(Runner.scala:1322)
      at org.scalatest.tools.Runner$.$anonfun$doRunRunRunDaDoRunRun$13$adapted(Runner.scala:1316)
      at scala.collection.immutable.List.foreach(List.scala:333)
      at org.scalatest.tools.Runner$.doRunRunRunDaDoRunRun(Runner.scala:1316)
      at org.scalatest.tools.Runner$.$anonfun$runOptionallyWithPassFailReporter$24(Runner.scala:993)
      at org.scalatest.tools.Runner$.$anonfun$runOptionallyWithPassFailReporter$24$adapted(Runner.scala:971)
      at org.scalatest.tools.Runner$.withClassLoaderAndDispatchReporter(Runner.scala:1482)
      at org.scalatest.tools.Runner$.runOptionallyWithPassFailReporter(Runner.scala:971)
      at org.scalatest.tools.Runner$.main(Runner.scala:775)
      at org.scalatest.tools.Runner.main(Runner.scala)
View more details on GitHub Actions