Disallow nesting endpointExpr and chor #2692
GitHub Actions / TestReport
failed
Sep 19, 2024 in 1s
1038 passed, 21 failed and 44 skipped
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
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
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)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
github-actions / TestReport
vct.test.integration.examples.veymont.VeyMontExamplesSpec ► Tic-Tac-Toe (generated permissions) verifies with silicon
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:Raw output
org.scalatest.exceptions.TestFailedException: Pass did not equal Crash(vct.main.modes.VeyMont$WrapSystemError: The following error occurred during choreography verification:
The encodePermissionStratification rewrite caused the AST to no longer typecheck:
======================================
1399 Perm(p2.turn, write) ** Perm(epOwnerTurn(p2, p2), write) **
1400 true **
[------------------
1401 (unfolding epOwnerC00(p1, p1) in
------------------]
1402 unfolding epOwnerC01(p1, p1) in
1403 unfolding epOwnerC02(p1, p1) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1400 true **
1401 (unfolding epOwnerC00(p1, p1) in
[------------------
1402 unfolding epOwnerC01(p1, p1) in
------------------]
1403 unfolding epOwnerC02(p1, p1) in
1404 unfolding epOwnerC10(p1, p1) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1401 (unfolding epOwnerC00(p1, p1) in
1402 unfolding epOwnerC01(p1, p1) in
[------------------
1403 unfolding epOwnerC02(p1, p1) in
------------------]
1404 unfolding epOwnerC10(p1, p1) in
1405 unfolding epOwnerC11(p1, p1) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1402 unfolding epOwnerC01(p1, p1) in
1403 unfolding epOwnerC02(p1, p1) in
[------------------
1404 unfolding epOwnerC10(p1, p1) in
------------------]
1405 unfolding epOwnerC11(p1, p1) in
1406 unfolding epOwnerC12(p1, p1) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1403 unfolding epOwnerC02(p1, p1) in
1404 unfolding epOwnerC10(p1, p1) in
[------------------
1405 unfolding epOwnerC11(p1, p1) in
------------------]
1406 unfolding epOwnerC12(p1, p1) in
1407 unfolding epOwnerC20(p1, p1) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1404 unfolding epOwnerC10(p1, p1) in
1405 unfolding epOwnerC11(p1, p1) in
[------------------
1406 unfolding epOwnerC12(p1, p1) in
------------------]
1407 unfolding epOwnerC20(p1, p1) in
1408 unfolding epOwnerC21(p1, p1) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1405 unfolding epOwnerC11(p1, p1) in
1406 unfolding epOwnerC12(p1, p1) in
[------------------
1407 unfolding epOwnerC20(p1, p1) in
------------------]
1408 unfolding epOwnerC21(p1, p1) in
1409 unfolding epOwnerC22(p1, p1) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1406 unfolding epOwnerC12(p1, p1) in
1407 unfolding epOwnerC20(p1, p1) in
[------------------
1408 unfolding epOwnerC21(p1, p1) in
------------------]
1409 unfolding epOwnerC22(p1, p1) in
1410 unfolding epOwnerMyToken(p1, p1) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1407 unfolding epOwnerC20(p1, p1) in
1408 unfolding epOwnerC21(p1, p1) in
[------------------
1409 unfolding epOwnerC22(p1, p1) in
------------------]
1410 unfolding epOwnerMyToken(p1, p1) in
1411 unfolding epOwnerMove(p1, p1) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1408 unfolding epOwnerC21(p1, p1) in
1409 unfolding epOwnerC22(p1, p1) in
[----------------------
1410 unfolding epOwnerMyToken(p1, p1) in
----------------------]
1411 unfolding epOwnerMove(p1, p1) in
1412 unfolding epOwnerTurn(p1, p1) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1409 unfolding epOwnerC22(p1, p1) in
1410 unfolding epOwnerMyToken(p1, p1) in
[-------------------
1411 unfolding epOwnerMove(p1, p1) in
-------------------]
1412 unfolding epOwnerTurn(p1, p1) in
1413 unfolding epOwnerI(p1, p1.move) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1410 unfolding epOwnerMyToken(p1, p1) in
1411 unfolding epOwnerMove(p1, p1) in
[-------------------
1412 unfolding epOwnerTurn(p1, p1) in
-------------------]
1413 unfolding epOwnerI(p1, p1.move) in
1414 unfolding epOwnerJ(p1, p1.move) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1411 unfolding epOwnerMove(p1, p1) in
1412 unfolding epOwnerTurn(p1, p1) in
[---------------------
1413 unfolding epOwnerI(p1, p1.move) in
---------------------]
1414 unfolding epOwnerJ(p1, p1.move) in
1415 unfolding epOwnerToken(p1, p1.move) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1412 unfolding epOwnerTurn(p1, p1) in
1413 unfolding epOwnerI(p1, p1.move) in
[---------------------
1414 unfolding epOwnerJ(p1, p1.move) in
---------------------]
1415 unfolding epOwnerToken(p1, p1.move) in
1416 unfolding epOwnerC00(p2, p2) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1413 unfolding epOwnerI(p1, p1.move) in
1414 unfolding epOwnerJ(p1, p1.move) in
[-------------------------
1415 unfolding epOwnerToken(p1, p1.move) in
-------------------------]
1416 unfolding epOwnerC00(p2, p2) in
1417 unfolding epOwnerC01(p2, p2) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1414 unfolding epOwnerJ(p1, p1.move) in
1415 unfolding epOwnerToken(p1, p1.move) in
[------------------
1416 unfolding epOwnerC00(p2, p2) in
------------------]
1417 unfolding epOwnerC01(p2, p2) in
1418 unfolding epOwnerC02(p2, p2) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1415 unfolding epOwnerToken(p1, p1.move) in
1416 unfolding epOwnerC00(p2, p2) in
[------------------
1417 unfolding epOwnerC01(p2, p2) in
------------------]
1418 unfolding epOwnerC02(p2, p2) in
1419 unfolding epOwnerC10(p2, p2) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1416 unfolding epOwnerC00(p2, p2) in
1417 unfolding epOwnerC01(p2, p2) in
[------------------
1418 unfolding epOwnerC02(p2, p2) in
------------------]
1419 unfolding epOwnerC10(p2, p2) in
1420 unfolding epOwnerC11(p2, p2) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1417 unfolding epOwnerC01(p2, p2) in
1418 unfolding epOwnerC02(p2, p2) in
[------------------
1419 unfolding epOwnerC10(p2, p2) in
------------------]
1420 unfolding epOwnerC11(p2, p2) in
1421 unfolding epOwnerC12(
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1418 unfolding epOwnerC02(p2, p2) in
1419 unfolding epOwnerC10(p2, p2) in
[------------------
1420 unfolding epOwnerC11(p2, p2) in
------------------]
1421 unfolding epOwnerC12(
1422 p2,
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1419 unfolding epOwnerC10(p2, p2) in
1420 unfolding epOwnerC11(p2, p2) in
[-----------
1421 unfolding epOwnerC12(
1422 p2,
1423 p2
1424 ) in
---------------------------------------------------------------------------------------------]
1425 unfolding epOwnerC20(
1426 p2,
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1423 p2
1424 ) in
[-----------
1425 unfolding epOwnerC20(
1426 p2,
1427 p2
1428 ) in
-------------------------------------------------------------------------------------------------]
1429 unfolding epOwnerC21(
1430 p2,
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1427 p2
1428 ) in
[-----------
1429 unfolding epOwnerC21(
1430 p2,
1431 p2
1432 ) in
-----------------------------------------------------------------------------------------------------]
1433 unfolding epOwnerC22(
1434 p2,
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1431 p2
1432 ) in
[-----------
1433 unfolding epOwnerC22(
1434 p2,
1435 p2
1436 ) in
---------------------------------------------------------------------------------------------------------]
1437 unfolding epOwnerMyToken(
1438 p2,
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1435 p2
1436 ) in
[---------------
1437 unfolding epOwnerMyToken(
1438 p2,
1439 p2
1440 ) in
-------------------------------------------------------------------------------------------------------------]
1441 unfolding epOwnerMove(
1442 p2,
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1439 p2
1440 ) in
[------------
1441 unfolding epOwnerMove(
1442 p2,
1443 p2
1444 ) in
-----------------------------------------------------------------------------------------------------------------]
1445 unfolding epOwnerTurn(
1446 p2,
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1443 p2
1444 ) in
[------------
1445 unfolding epOwnerTurn(
1446 p2,
1447 p2
1448 ) in
---------------------------------------------------------------------------------------------------------------------]
1449 unfolding epOwnerI(
1450 p2,
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1447 p2
1448 ) in
[---------
1449 unfolding epOwnerI(
1450 p2,
1451 p2.move
1452 ) in
-------------------------------------------------------------------------------------------------------------------------]
1453 unfolding epOwnerJ(
1454 p2,
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1451 p2.move
1452 ) in
[---------
1453 unfolding epOwnerJ(
1454 p2,
1455 p2.move
1456 ) in
-----------------------------------------------------------------------------------------------------------------------------]
1457 unfolding epOwnerToken(
1458 p2,
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1455 p2.move
1456 ) in
[-------------
1457 unfolding epOwnerToken(
1458 p2,
1459 p2.move
1460 ) in
---------------------------------------------------------------------------------------------------------------------------------]
1461 [write](p1.myToken ==
1462 0 **
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1800 loop_invariant Perm(p2.turn, write);
1801 loop_invariant Perm(epOwnerTurn(p2, p2), write);
[------------------
1802 loop_invariant unfolding epOwnerC00(p1, p1) in
------------------]
1803 unfolding epOwnerC01(p1, p1) in
1804 unfolding epOwnerC02(p1, p1) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1801 loop_invariant Perm(epOwnerTurn(p2, p2), write);
1802 loop_invariant unfolding epOwnerC00(p1, p1) in
[------------------
1803 unfolding epOwnerC01(p1, p1) in
------------------]
1804 unfolding epOwnerC02(p1, p1) in
1805 unfolding epOwnerC10(p1, p1) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1802 loop_invariant unfolding epOwnerC00(p1, p1) in
1803 unfolding epOwnerC01(p1, p1) in
[------------------
1804 unfolding epOwnerC02(p1, p1) in
------------------]
1805 unfolding epOwnerC10(p1, p1) in
1806 unfolding epOwnerC11(p1, p1) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1803 unfolding epOwnerC01(p1, p1) in
1804 unfolding epOwnerC02(p1, p1) in
[------------------
1805 unfolding epOwnerC10(p1, p1) in
------------------]
1806 unfolding epOwnerC11(p1, p1) in
1807 unfolding epOwnerC12(p1, p1) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1804 unfolding epOwnerC02(p1, p1) in
1805 unfolding epOwnerC10(p1, p1) in
[------------------
1806 unfolding epOwnerC11(p1, p1) in
------------------]
1807 unfolding epOwnerC12(p1, p1) in
1808 unfolding epOwnerC20(p1, p1) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1805 unfolding epOwnerC10(p1, p1) in
1806 unfolding epOwnerC11(p1, p1) in
[------------------
1807 unfolding epOwnerC12(p1, p1) in
------------------]
1808 unfolding epOwnerC20(p1, p1) in
1809 unfolding epOwnerC21(p1, p1) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1806 unfolding epOwnerC11(p1, p1) in
1807 unfolding epOwnerC12(p1, p1) in
[------------------
1808 unfolding epOwnerC20(p1, p1) in
------------------]
1809 unfolding epOwnerC21(p1, p1) in
1810 unfolding epOwnerC22(p1, p1) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1807 unfolding epOwnerC12(p1, p1) in
1808 unfolding epOwnerC20(p1, p1) in
[------------------
1809 unfolding epOwnerC21(p1, p1) in
------------------]
1810 unfolding epOwnerC22(p1, p1) in
1811 unfolding epOwnerMyToken(p1, p1) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1808 unfolding epOwnerC20(p1, p1) in
1809 unfolding epOwnerC21(p1, p1) in
[------------------
1810 unfolding epOwnerC22(p1, p1) in
------------------]
1811 unfolding epOwnerMyToken(p1, p1) in
1812 unfolding epOwnerMove(p1, p1) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1809 unfolding epOwnerC21(p1, p1) in
1810 unfolding epOwnerC22(p1, p1) in
[----------------------
1811 unfolding epOwnerMyToken(p1, p1) in
----------------------]
1812 unfolding epOwnerMove(p1, p1) in
1813 unfolding epOwnerTurn(p1, p1) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1810 unfolding epOwnerC22(p1, p1) in
1811 unfolding epOwnerMyToken(p1, p1) in
[-------------------
1812 unfolding epOwnerMove(p1, p1) in
-------------------]
1813 unfolding epOwnerTurn(p1, p1) in
1814 unfolding epOwnerI(p1, p1.move) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1811 unfolding epOwnerMyToken(p1, p1) in
1812 unfolding epOwnerMove(p1, p1) in
[-------------------
1813 unfolding epOwnerTurn(p1, p1) in
-------------------]
1814 unfolding epOwnerI(p1, p1.move) in
1815 unfolding epOwnerJ(p1, p1.move) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1812 unfolding epOwnerMove(p1, p1) in
1813 unfolding epOwnerTurn(p1, p1) in
[---------------------
1814 unfolding epOwnerI(p1, p1.move) in
---------------------]
1815 unfolding epOwnerJ(p1, p1.move) in
1816 unfolding epOwnerToken(p1, p1.move) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1813 unfolding epOwnerTurn(p1, p1) in
1814 unfolding epOwnerI(p1, p1.move) in
[---------------------
1815 unfolding epOwnerJ(p1, p1.move) in
---------------------]
1816 unfolding epOwnerToken(p1, p1.move) in
1817 unfolding epOwnerC00(p2, p2) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1814 unfolding epOwnerI(p1, p1.move) in
1815 unfolding epOwnerJ(p1, p1.move) in
[-------------------------
1816 unfolding epOwnerToken(p1, p1.move) in
-------------------------]
1817 unfolding epOwnerC00(p2, p2) in
1818 unfolding epOwnerC01(p2, p2) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1815 unfolding epOwnerJ(p1, p1.move) in
1816 unfolding epOwnerToken(p1, p1.move) in
[------------------
1817 unfolding epOwnerC00(p2, p2) in
------------------]
1818 unfolding epOwnerC01(p2, p2) in
1819 unfolding epOwnerC02(p2, p2) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1816 unfolding epOwnerToken(p1, p1.move) in
1817 unfolding epOwnerC00(p2, p2) in
[------------------
1818 unfolding epOwnerC01(p2, p2) in
------------------]
1819 unfolding epOwnerC02(p2, p2) in
1820 unfolding epOwnerC10(p2, p2) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1817 unfolding epOwnerC00(p2, p2) in
1818 unfolding epOwnerC01(p2, p2) in
[------------------
1819 unfolding epOwnerC02(p2, p2) in
------------------]
1820 unfolding epOwnerC10(p2, p2) in
1821 unfolding epOwnerC11(p2, p2) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1818 unfolding epOwnerC01(p2, p2) in
1819 unfolding epOwnerC02(p2, p2) in
[------------------
1820 unfolding epOwnerC10(p2, p2) in
------------------]
1821 unfolding epOwnerC11(p2, p2) in
1822 unfolding epOwnerC12(p2, p2) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1819 unfolding epOwnerC02(p2, p2) in
1820 unfolding epOwnerC10(p2, p2) in
[------------------
1821 unfolding epOwnerC11(p2, p2) in
------------------]
1822 unfolding epOwnerC12(p2, p2) in
1823 unfolding epOwnerC20(
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1820 unfolding epOwnerC10(p2, p2) in
1821 unfolding epOwnerC11(p2, p2) in
[------------------
1822 unfolding epOwnerC12(p2, p2) in
------------------]
1823 unfolding epOwnerC20(
1824 p2,
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1821 unfolding epOwnerC11(p2, p2) in
1822 unfolding epOwnerC12(p2, p2) in
[-----------
1823 unfolding epOwnerC20(
1824 p2,
1825 p2
1826 ) in
---------------------------------------------------------------------------------------------]
1827 unfolding epOwnerC21(
1828 p2,
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1825 p2
1826 ) in
[-----------
1827 unfolding epOwnerC21(
1828 p2,
1829 p2
1830 ) in
-------------------------------------------------------------------------------------------------]
1831 unfolding epOwnerC22(
1832 p2,
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1829 p2
1830 ) in
[-----------
1831 unfolding epOwnerC22(
1832 p2,
1833 p2
1834 ) in
-----------------------------------------------------------------------------------------------------]
1835 unfolding epOwnerMyToken(
1836 p2,
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1833 p2
1834 ) in
[---------------
1835 unfolding epOwnerMyToken(
1836 p2,
1837 p2
1838 ) in
---------------------------------------------------------------------------------------------------------]
1839 unfolding epOwnerMove(
1840 p2,
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1837 p2
1838 ) in
[------------
1839 unfolding epOwnerMove(
1840 p2,
1841 p2
1842 ) in
-------------------------------------------------------------------------------------------------------------]
1843 unfolding epOwnerTurn(
1844 p2,
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1841 p2
1842 ) in
[------------
1843 unfolding epOwnerTurn(
1844 p2,
1845 p2
1846 ) in
-----------------------------------------------------------------------------------------------------------------]
1847 unfolding epOwnerI(
1848 p2,
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1845 p2
1846 ) in
[---------
1847 unfolding epOwnerI(
1848 p2,
1849 p2.move
1850 ) in
---------------------------------------------------------------------------------------------------------------------]
1851 unfolding epOwnerJ(
1852 p2,
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1849 p2.move
1850 ) in
[---------
1851 unfolding epOwnerJ(
1852 p2,
1853 p2.move
1854 ) in
-------------------------------------------------------------------------------------------------------------------------]
1855 unfolding epOwnerToken(
1856 p2,
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1853 p2.move
1854 ) in
[-------------
1855 unfolding epOwnerToken(
1856 p2,
1857 p2.move
1858 ) in
-----------------------------------------------------------------------------------------------------------------------------]
1859 [write](p1.myToken ==
1860 0 **
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1870 p2.move !=
1871 null);
[------------------
1872 loop_invariant unfolding epOwnerC00(p1, p1) in
------------------]
1873 unfolding epOwnerC01(p1, p1) in
1874 unfolding epOwnerC02(p1, p1) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1871 null);
1872 loop_invariant unfolding epOwnerC00(p1, p1) in
[------------------
1873 unfolding epOwnerC01(p1, p1) in
------------------]
1874 unfolding epOwnerC02(p1, p1) in
1875 unfolding epOwnerC10(p1, p1) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1872 loop_invariant unfolding epOwnerC00(p1, p1) in
1873 unfolding epOwnerC01(p1, p1) in
[------------------
1874 unfolding epOwnerC02(p1, p1) in
------------------]
1875 unfolding epOwnerC10(p1, p1) in
1876 unfolding epOwnerC11(p1, p1) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1873 unfolding epOwnerC01(p1, p1) in
1874 unfolding epOwnerC02(p1, p1) in
[------------------
1875 unfolding epOwnerC10(p1, p1) in
------------------]
1876 unfolding epOwnerC11(p1, p1) in
1877 unfolding epOwnerC12(p1, p1) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1874 unfolding epOwnerC02(p1, p1) in
1875 unfolding epOwnerC10(p1, p1) in
[------------------
1876 unfolding epOwnerC11(p1, p1) in
------------------]
1877 unfolding epOwnerC12(p1, p1) in
1878 unfolding epOwnerC20(p1, p1) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1875 unfolding epOwnerC10(p1, p1) in
1876 unfolding epOwnerC11(p1, p1) in
[------------------
1877 unfolding epOwnerC12(p1, p1) in
------------------]
1878 unfolding epOwnerC20(p1, p1) in
1879 unfolding epOwnerC21(p1, p1) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
================...
Check failure on line 222 in test/main/vct/test/integration/helper/VeyMontSpec.scala
github-actions / TestReport
vct.test.integration.examples.veymont.FM2023VeyMontSpec ► Files examples/publications/2023/FM2023VeyMont/applicability/2pc-5.pvl verifies with silicon
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:Raw output
org.scalatest.exceptions.TestFailedException: Pass did not equal Crash(vct.main.modes.VeyMont$WrapSystemError: The following error occurred during choreography verification:
The encodePermissionStratification rewrite caused the AST to no longer typecheck:
======================================
838 readStatus(s3, s3) == s3.initialS3(s3) **
839 readStatus(s4, s4) == s4.initialS4(s4) **
[------------------
840 (unfolding epOwnerQuery(c, c) in
------------------]
841 unfolding epOwnerTemp(c, c) in
842 unfolding epOwnerFlag(c, c) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
839 readStatus(s4, s4) == s4.initialS4(s4) **
840 (unfolding epOwnerQuery(c, c) in
[-----------------
841 unfolding epOwnerTemp(c, c) in
-----------------]
842 unfolding epOwnerFlag(c, c) in
843 unfolding epOwnerFlag1(c, c) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
840 (unfolding epOwnerQuery(c, c) in
841 unfolding epOwnerTemp(c, c) in
[-----------------
842 unfolding epOwnerFlag(c, c) in
-----------------]
843 unfolding epOwnerFlag1(c, c) in
844 unfolding epOwnerFlag2(c, c) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
841 unfolding epOwnerTemp(c, c) in
842 unfolding epOwnerFlag(c, c) in
[------------------
843 unfolding epOwnerFlag1(c, c) in
------------------]
844 unfolding epOwnerFlag2(c, c) in
845 unfolding epOwnerFlag3(c, c) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
842 unfolding epOwnerFlag(c, c) in
843 unfolding epOwnerFlag1(c, c) in
[------------------
844 unfolding epOwnerFlag2(c, c) in
------------------]
845 unfolding epOwnerFlag3(c, c) in
846 unfolding epOwnerFlag4(c, c) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
843 unfolding epOwnerFlag1(c, c) in
844 unfolding epOwnerFlag2(c, c) in
[------------------
845 unfolding epOwnerFlag3(c, c) in
------------------]
846 unfolding epOwnerFlag4(c, c) in
847 unfolding epOwnerSerialNumber(c, c.query) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
844 unfolding epOwnerFlag2(c, c) in
845 unfolding epOwnerFlag3(c, c) in
[------------------
846 unfolding epOwnerFlag4(c, c) in
------------------]
847 unfolding epOwnerSerialNumber(c, c.query) in
848 unfolding epOwnerSerialNumber(c, c.temp) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
845 unfolding epOwnerFlag3(c, c) in
846 unfolding epOwnerFlag4(c, c) in
[-------------------------------
847 unfolding epOwnerSerialNumber(c, c.query) in
-------------------------------]
848 unfolding epOwnerSerialNumber(c, c.temp) in
849 unfolding epOwnerStatus(s1, s1) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
846 unfolding epOwnerFlag4(c, c) in
847 unfolding epOwnerSerialNumber(c, c.query) in
[------------------------------
848 unfolding epOwnerSerialNumber(c, c.temp) in
------------------------------]
849 unfolding epOwnerStatus(s1, s1) in
850 unfolding epOwnerFlag5(s1, s1) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
847 unfolding epOwnerSerialNumber(c, c.query) in
848 unfolding epOwnerSerialNumber(c, c.temp) in
[---------------------
849 unfolding epOwnerStatus(s1, s1) in
---------------------]
850 unfolding epOwnerFlag5(s1, s1) in
851 unfolding epOwnerQuery1(s1, s1) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
848 unfolding epOwnerSerialNumber(c, c.temp) in
849 unfolding epOwnerStatus(s1, s1) in
[--------------------
850 unfolding epOwnerFlag5(s1, s1) in
--------------------]
851 unfolding epOwnerQuery1(s1, s1) in
852 unfolding epOwnerSerialNumber(s1, s1.query) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
849 unfolding epOwnerStatus(s1, s1) in
850 unfolding epOwnerFlag5(s1, s1) in
[---------------------
851 unfolding epOwnerQuery1(s1, s1) in
---------------------]
852 unfolding epOwnerSerialNumber(s1, s1.query) in
853 unfolding epOwnerStatus(s2, s2) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
850 unfolding epOwnerFlag5(s1, s1) in
851 unfolding epOwnerQuery1(s1, s1) in
[---------------------------------
852 unfolding epOwnerSerialNumber(s1, s1.query) in
---------------------------------]
853 unfolding epOwnerStatus(s2, s2) in
854 unfolding epOwnerFlag5(s2, s2) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
851 unfolding epOwnerQuery1(s1, s1) in
852 unfolding epOwnerSerialNumber(s1, s1.query) in
[---------------------
853 unfolding epOwnerStatus(s2, s2) in
---------------------]
854 unfolding epOwnerFlag5(s2, s2) in
855 unfolding epOwnerQuery1(s2, s2) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
852 unfolding epOwnerSerialNumber(s1, s1.query) in
853 unfolding epOwnerStatus(s2, s2) in
[--------------------
854 unfolding epOwnerFlag5(s2, s2) in
--------------------]
855 unfolding epOwnerQuery1(s2, s2) in
856 unfolding epOwnerSerialNumber(
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
853 unfolding epOwnerStatus(s2, s2) in
854 unfolding epOwnerFlag5(s2, s2) in
[---------------------
855 unfolding epOwnerQuery1(s2, s2) in
---------------------]
856 unfolding epOwnerSerialNumber(
857 s2,
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
854 unfolding epOwnerFlag5(s2, s2) in
855 unfolding epOwnerQuery1(s2, s2) in
[--------------------
856 unfolding epOwnerSerialNumber(
857 s2,
858 s2.query
859 ) in
-----------------------------------------------------------------------------]
860 unfolding epOwnerStatus(s3, s3) in
861 unfolding epOwnerFlag5(s3, s3) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
858 s2.query
859 ) in
[---------------------
860 unfolding epOwnerStatus(s3, s3) in
---------------------]
861 unfolding epOwnerFlag5(s3, s3) in
862 unfolding epOwnerQuery1(
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
859 ) in
860 unfolding epOwnerStatus(s3, s3) in
[--------------------
861 unfolding epOwnerFlag5(s3, s3) in
--------------------]
862 unfolding epOwnerQuery1(
863 s3,
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
860 unfolding epOwnerStatus(s3, s3) in
861 unfolding epOwnerFlag5(s3, s3) in
[--------------
862 unfolding epOwnerQuery1(
863 s3,
864 s3
865 ) in
-----------------------------------------------------------------------------------------]
866 unfolding epOwnerSerialNumber(
867 s3,
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
864 s3
865 ) in
[--------------------
866 unfolding epOwnerSerialNumber(
867 s3,
868 s3.query
869 ) in
---------------------------------------------------------------------------------------------]
870 unfolding epOwnerStatus(
871 s4,
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
868 s3.query
869 ) in
[--------------
870 unfolding epOwnerStatus(
871 s4,
872 s4
873 ) in
-------------------------------------------------------------------------------------------------]
874 unfolding epOwnerFlag5(
875 s4,
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
872 s4
873 ) in
[-------------
874 unfolding epOwnerFlag5(
875 s4,
876 s4
877 ) in
-----------------------------------------------------------------------------------------------------]
878 unfolding epOwnerQuery1(
879 s4,
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
876 s4
877 ) in
[--------------
878 unfolding epOwnerQuery1(
879 s4,
880 s4
881 ) in
---------------------------------------------------------------------------------------------------------]
882 unfolding epOwnerSerialNumber(
883 s4,
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
880 s4
881 ) in
[--------------------
882 unfolding epOwnerSerialNumber(
883 s4,
884 s4.query
885 ) in
-------------------------------------------------------------------------------------------------------------]
886 [write]((!c.flag ==>
887 s1.isUncommitted()) &&
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1157 loop_invariant readStatus(s4, s4) == s4.initialS4(s4) || readStatus(s4, s4) == s4.committedS4(s4) ||
1158 readStatus(s4, s4) == s4.abortedS4(s4);
[------------------
1159 loop_invariant unfolding epOwnerQuery(c, c) in
------------------]
1160 unfolding epOwnerTemp(c, c) in
1161 unfolding epOwnerFlag(c, c) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1158 readStatus(s4, s4) == s4.abortedS4(s4);
1159 loop_invariant unfolding epOwnerQuery(c, c) in
[-----------------
1160 unfolding epOwnerTemp(c, c) in
-----------------]
1161 unfolding epOwnerFlag(c, c) in
1162 unfolding epOwnerFlag1(c, c) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1159 loop_invariant unfolding epOwnerQuery(c, c) in
1160 unfolding epOwnerTemp(c, c) in
[-----------------
1161 unfolding epOwnerFlag(c, c) in
-----------------]
1162 unfolding epOwnerFlag1(c, c) in
1163 unfolding epOwnerFlag2(c, c) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1160 unfolding epOwnerTemp(c, c) in
1161 unfolding epOwnerFlag(c, c) in
[------------------
1162 unfolding epOwnerFlag1(c, c) in
------------------]
1163 unfolding epOwnerFlag2(c, c) in
1164 unfolding epOwnerFlag3(c, c) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1161 unfolding epOwnerFlag(c, c) in
1162 unfolding epOwnerFlag1(c, c) in
[------------------
1163 unfolding epOwnerFlag2(c, c) in
------------------]
1164 unfolding epOwnerFlag3(c, c) in
1165 unfolding epOwnerFlag4(c, c) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1162 unfolding epOwnerFlag1(c, c) in
1163 unfolding epOwnerFlag2(c, c) in
[------------------
1164 unfolding epOwnerFlag3(c, c) in
------------------]
1165 unfolding epOwnerFlag4(c, c) in
1166 unfolding epOwnerSerialNumber(c, c.query) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1163 unfolding epOwnerFlag2(c, c) in
1164 unfolding epOwnerFlag3(c, c) in
[------------------
1165 unfolding epOwnerFlag4(c, c) in
------------------]
1166 unfolding epOwnerSerialNumber(c, c.query) in
1167 unfolding epOwnerSerialNumber(c, c.temp) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1164 unfolding epOwnerFlag3(c, c) in
1165 unfolding epOwnerFlag4(c, c) in
[-------------------------------
1166 unfolding epOwnerSerialNumber(c, c.query) in
-------------------------------]
1167 unfolding epOwnerSerialNumber(c, c.temp) in
1168 unfolding epOwnerStatus(s1, s1) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1165 unfolding epOwnerFlag4(c, c) in
1166 unfolding epOwnerSerialNumber(c, c.query) in
[------------------------------
1167 unfolding epOwnerSerialNumber(c, c.temp) in
------------------------------]
1168 unfolding epOwnerStatus(s1, s1) in
1169 unfolding epOwnerFlag5(s1, s1) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1166 unfolding epOwnerSerialNumber(c, c.query) in
1167 unfolding epOwnerSerialNumber(c, c.temp) in
[---------------------
1168 unfolding epOwnerStatus(s1, s1) in
---------------------]
1169 unfolding epOwnerFlag5(s1, s1) in
1170 unfolding epOwnerQuery1(s1, s1) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1167 unfolding epOwnerSerialNumber(c, c.temp) in
1168 unfolding epOwnerStatus(s1, s1) in
[--------------------
1169 unfolding epOwnerFlag5(s1, s1) in
--------------------]
1170 unfolding epOwnerQuery1(s1, s1) in
1171 unfolding epOwnerSerialNumber(s1, s1.query) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1168 unfolding epOwnerStatus(s1, s1) in
1169 unfolding epOwnerFlag5(s1, s1) in
[---------------------
1170 unfolding epOwnerQuery1(s1, s1) in
---------------------]
1171 unfolding epOwnerSerialNumber(s1, s1.query) in
1172 unfolding epOwnerStatus(s2, s2) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1169 unfolding epOwnerFlag5(s1, s1) in
1170 unfolding epOwnerQuery1(s1, s1) in
[---------------------------------
1171 unfolding epOwnerSerialNumber(s1, s1.query) in
---------------------------------]
1172 unfolding epOwnerStatus(s2, s2) in
1173 unfolding epOwnerFlag5(s2, s2) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1170 unfolding epOwnerQuery1(s1, s1) in
1171 unfolding epOwnerSerialNumber(s1, s1.query) in
[---------------------
1172 unfolding epOwnerStatus(s2, s2) in
---------------------]
1173 unfolding epOwnerFlag5(s2, s2) in
1174 unfolding epOwnerQuery1(s2, s2) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1171 unfolding epOwnerSerialNumber(s1, s1.query) in
1172 unfolding epOwnerStatus(s2, s2) in
[--------------------
1173 unfolding epOwnerFlag5(s2, s2) in
--------------------]
1174 unfolding epOwnerQuery1(s2, s2) in
1175 unfolding epOwnerSerialNumber(s2, s2.query) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1172 unfolding epOwnerStatus(s2, s2) in
1173 unfolding epOwnerFlag5(s2, s2) in
[---------------------
1174 unfolding epOwnerQuery1(s2, s2) in
---------------------]
1175 unfolding epOwnerSerialNumber(s2, s2.query) in
1176 unfolding epOwnerStatus(s3, s3) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1173 unfolding epOwnerFlag5(s2, s2) in
1174 unfolding epOwnerQuery1(s2, s2) in
[---------------------------------
1175 unfolding epOwnerSerialNumber(s2, s2.query) in
---------------------------------]
1176 unfolding epOwnerStatus(s3, s3) in
1177 unfolding epOwnerFlag5(s3, s3) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1174 unfolding epOwnerQuery1(s2, s2) in
1175 unfolding epOwnerSerialNumber(s2, s2.query) in
[---------------------
1176 unfolding epOwnerStatus(s3, s3) in
---------------------]
1177 unfolding epOwnerFlag5(s3, s3) in
1178 unfolding epOwnerQuery1(s3, s3) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1175 unfolding epOwnerSerialNumber(s2, s2.query) in
1176 unfolding epOwnerStatus(s3, s3) in
[--------------------
1177 unfolding epOwnerFlag5(s3, s3) in
--------------------]
1178 unfolding epOwnerQuery1(s3, s3) in
1179 unfolding epOwnerSerialNumber(
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1176 unfolding epOwnerStatus(s3, s3) in
1177 unfolding epOwnerFlag5(s3, s3) in
[---------------------
1178 unfolding epOwnerQuery1(s3, s3) in
---------------------]
1179 unfolding epOwnerSerialNumber(
1180 s3,
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1177 unfolding epOwnerFlag5(s3, s3) in
1178 unfolding epOwnerQuery1(s3, s3) in
[--------------------
1179 unfolding epOwnerSerialNumber(
1180 s3,
1181 s3.query
1182 ) in
-----------------------------------------------------------------------------------------]
1183 unfolding epOwnerStatus(
1184 s4,
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1181 s3.query
1182 ) in
[--------------
1183 unfolding epOwnerStatus(
1184 s4,
1185 s4
1186 ) in
---------------------------------------------------------------------------------------------]
1187 unfolding epOwnerFlag5(
1188 s4,
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1185 s4
1186 ) in
[-------------
1187 unfolding epOwnerFlag5(
1188 s4,
1189 s4
1190 ) in
-------------------------------------------------------------------------------------------------]
1191 unfolding epOwnerQuery1(
1192 s4,
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1189 s4
1190 ) in
[--------------
1191 unfolding epOwnerQuery1(
1192 s4,
1193 s4
1194 ) in
-----------------------------------------------------------------------------------------------------]
1195 unfolding epOwnerSerialNumber(
1196 s4,
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1193 s4
1194 ) in
[--------------------
1195 unfolding epOwnerSerialNumber(
1196 s4,
1197 s4.query
1198 ) in
---------------------------------------------------------------------------------------------------------]
1199 [write]((!c.flag ==>
1200 s1.isUncommitted()) &&
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
965 requires readStatus(s3, s3) == s3.initialS3(s3);
966 requires readStatus(s4, s4) == s4.initialS4(s4);
[------------------
967 requires unfolding epOwnerQuery(c, c) in
------------------]
968 unfolding epOwnerTemp(c, c) in
969 unfolding epOwnerFlag(c, c) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
966 requires readStatus(s4, s4) == s4.initialS4(s4);
967 requires unfolding epOwnerQuery(c, c) in
[-----------------
968 unfolding epOwnerTemp(c, c) in
-----------------]
969 unfolding epOwnerFlag(c, c) in
970 unfolding epOwnerFlag1(c, c) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
967 requires unfolding epOwnerQuery(c, c) in
968 unfolding epOwnerTemp(c, c) in
[-----------------
969 unfolding epOwnerFlag(c, c) in
-----------------]
970 unfolding epOwnerFlag1(c, c) in
971 unfolding epOwnerFlag2(c, c) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
968 unfolding epOwnerTemp(c, c) in
969 unfolding epOwnerFlag(c, c) in
[------------------
970 unfolding epOwnerFlag1(c, c) in
------------------]
971 unfolding epOwnerFlag2(c, c) in
972 unfolding epOwnerFlag3(c, c) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
969 unfolding epOwnerFlag(c, c) in
970 unfolding epOwnerFlag1(c, c) in
[------------------
971 unfolding epOwnerFlag2(c, c) in
------------------]
972 unfolding epOwnerFlag3(c, c) in
973 unfolding epOwnerFlag4(c, c) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
970 unfolding epOwnerFlag1(c, c) in
971 unfolding epOwnerFlag2(c, c) in
[------------------
972 unfolding epOwnerFlag3(c, c) in
------------------]
973 unfolding epOwnerFlag4(c, c) in
974 unfolding epOwnerSerialNumber(c, c.query) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
971 unfolding epOwnerFlag2(c, c) in
972 unfolding epOwnerFlag3(c, c) in
[------------------
973 unfolding epOwnerFlag4(c, c) in
------------------]
974 unfolding epOwnerSerialNumber(c, c.query) in
975 unfolding epOwnerSerialNumber(c, c.temp) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
972 unfolding epOwnerFlag3(c, c) in
973 unfolding epOwnerFlag4(c, c) in
[-------------------------------
974 unfolding epOwnerSerialNumber(c, c.query) in
-------------------------------]
975 unfolding epOwnerSerialNumber(c, c.temp) in
976 unfolding epOwnerStatus(s1, s1) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
973 unfolding epOwnerFlag4(c, c) in
974 unfolding epOwnerSerialNumber(c, c.query) in
[------------------------------
975 unfolding epOwnerSerialNumber(c, c.temp) in
------------------------------]
976 unfolding epOwnerStatus(s1, s1) in
977 unfolding epOwnerFlag5(s1, s1) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
974 unfolding epOwnerSerialNumber(c, c.query) in
975 unfolding epOwnerSerialNumber(c, c.temp) in
[---------------------
976 unfolding epOwnerStatus(s1, s1) in
---------------------]
977 unfolding epOwnerFlag5(s1, s1) in
978 unfolding epOwnerQuery1(s1, s1) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
975 unfolding epOwnerSerialNumber(c, c.temp) in
976 unfolding epOwnerStatus(s1, s1) in
[--------------------
977 unfolding epOwnerFlag5(s1, s1) in
--------------------]
978 unfolding epOwnerQuery1(s1, s1) in
979 unfolding epOwnerSerialNumber(s1, s1.query) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
976 unfolding epOwnerStatus(s1, s1) in
977 unfolding epOwnerFlag5(s1, s1) in
[---------------------
978 unfolding epOwnerQuery1(s1, s1) in
---------------------]
979 unfolding epOwnerSerialNumber(s1, s1.query) in
980 unfolding epOwnerStatus(s2, s2) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
977 unfolding epOwnerFlag5(s1, s1) in
978 unfolding epOwnerQuery1(s1, s1) in
[---------------------------------
979 unfolding epOwnerSerialNumber(s1, s1.query) in
---------------------------------]
980 unfolding epOwnerStatus(s2, s2) in
981 unfolding epOwnerFlag5(s2, s2) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
978 unfolding epOwnerQuery1(s1, s1) in
979 unfolding epOwnerSerialNumber(s1, s1.query) in
[---------------------
980 unfolding epOwnerStatus(s2, s2) in
---------------------]
981 unfolding epOwnerFlag5(s2, s2) in
982 unfolding epOwnerQuery1(s2, s2) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
979 unfolding epOwnerSerialNumber(s1, s1.query) in
980 unfolding epOwnerStatus(s2, s2) in
[--------------------
981 unfolding epOwnerFlag5(s2, s2) in
--------------------]
982 unfolding epOwnerQuery1(s2, s2) in
983 unfolding epOwnerSerialNumber(s2, s2.query) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
980 unfolding epOwnerStatus(s2, s2) in
981 unfolding epOwnerFlag5(s2, s2) in
[---------------------
982 unfolding epOwnerQuery1(s2, s2) in
---------------------]
983 unfolding epOwnerSerialNumber(s2, s2.query) in
984 unfolding epOwnerStatus(s3, s3) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
981 unfolding epOwnerFlag5(s2, s2) in
982 unfolding epOwnerQuery1(s2, s2) in
[---------------------------------
983 unfolding epOwnerSerialNumber(s2, s2.query) in
---------------------------------]
984 unfolding epOwnerStatus(s3, s3) in
985 unfolding epOwnerFlag5(s3, s3) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
982 unfolding epOwnerQuery1(s2, s2) in
983 unfolding epOwnerSerialNumber(s2, s2.query) in
[---------------------
984 unfolding epOwnerStatus(s3, s3) in
---------------------]
985 unfolding epOwnerFlag5(s3, s3) in
986 unfolding epOwnerQuery1(s3, s3) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
983 unfolding epOwnerSerialNumber(s2, s2.query) in
984 unfolding epOwnerStatus(s3, s3) in
[--------------------
985 unfolding epOwnerFlag5(s3, s3) in
--------------------]
986 unfolding epOwnerQuery1(s3, s3) in
987 unfolding epOwnerSerialNumber(
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
984 unfolding epOwnerStatus(s3, s3) in
985 unfolding epOwnerFlag5(s3, s3) in
[---------------------
986 unfolding epOwnerQuery1(s3, s3) in
---------------------]
987 unfolding epOwnerSerialNumber(
988 s3,
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
985 unfolding epOwnerFlag5(s3, s3) in
986 unfolding epOwnerQuery1(s3, s3) in
[--------------------
987 unfolding epOwnerSerialNumber(
988 s3,
989 s3.query
990 ) in
-------------------------------------------------------------------------------------]
991 unfolding epOwnerStatus(
992 s4,
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
989 s3.query
990 ) in
[--------------
991 unfolding epOwnerStatus(
992 s4,
993 s4
994 ) in
-----------------------------------------------------------------------------------------]
995 unfolding epOwnerFlag5(
996...
Check failure on line 222 in test/main/vct/test/integration/helper/VeyMontSpec.scala
github-actions / TestReport
vct.test.integration.examples.veymont.FM2023VeyMontSpec ► Files examples/publications/2023/FM2023VeyMont/applicability/consensus-3.pvl verifies with silicon
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:Raw output
org.scalatest.exceptions.TestFailedException: Pass did not equal Crash(vct.main.modes.VeyMont$WrapSystemError: The following error occurred during choreography verification:
The encodePermissionStratification rewrite caused the AST to no longer typecheck:
======================================
1209 (readV3(p3, p3) == 0 || readV3(p3, p3) == 1) &&
1210 (readTiebreaker(p3, p3) == 0 || readTiebreaker(p3, p3) == 1)) **
[----------------
1211 (unfolding epOwnerN(p1, p1) in
----------------]
1212 unfolding epOwnerF(p1, p1) in
1213 unfolding epOwnerFault(p1, p1) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1210 (readTiebreaker(p3, p3) == 0 || readTiebreaker(p3, p3) == 1)) **
1211 (unfolding epOwnerN(p1, p1) in
[----------------
1212 unfolding epOwnerF(p1, p1) in
----------------]
1213 unfolding epOwnerFault(p1, p1) in
1214 unfolding epOwnerV(p1, p1) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1211 (unfolding epOwnerN(p1, p1) in
1212 unfolding epOwnerF(p1, p1) in
[--------------------
1213 unfolding epOwnerFault(p1, p1) in
--------------------]
1214 unfolding epOwnerV(p1, p1) in
1215 unfolding epOwnerV1(p1, p1) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1212 unfolding epOwnerF(p1, p1) in
1213 unfolding epOwnerFault(p1, p1) in
[----------------
1214 unfolding epOwnerV(p1, p1) in
----------------]
1215 unfolding epOwnerV1(p1, p1) in
1216 unfolding epOwnerV2(p1, p1) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1213 unfolding epOwnerFault(p1, p1) in
1214 unfolding epOwnerV(p1, p1) in
[-----------------
1215 unfolding epOwnerV1(p1, p1) in
-----------------]
1216 unfolding epOwnerV2(p1, p1) in
1217 unfolding epOwnerV3(p1, p1) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1214 unfolding epOwnerV(p1, p1) in
1215 unfolding epOwnerV1(p1, p1) in
[-----------------
1216 unfolding epOwnerV2(p1, p1) in
-----------------]
1217 unfolding epOwnerV3(p1, p1) in
1218 unfolding epOwnerTiebreaker(p1, p1) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1215 unfolding epOwnerV1(p1, p1) in
1216 unfolding epOwnerV2(p1, p1) in
[-----------------
1217 unfolding epOwnerV3(p1, p1) in
-----------------]
1218 unfolding epOwnerTiebreaker(p1, p1) in
1219 unfolding epOwnerN(p2, p2) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1216 unfolding epOwnerV2(p1, p1) in
1217 unfolding epOwnerV3(p1, p1) in
[-------------------------
1218 unfolding epOwnerTiebreaker(p1, p1) in
-------------------------]
1219 unfolding epOwnerN(p2, p2) in
1220 unfolding epOwnerF(p2, p2) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1217 unfolding epOwnerV3(p1, p1) in
1218 unfolding epOwnerTiebreaker(p1, p1) in
[----------------
1219 unfolding epOwnerN(p2, p2) in
----------------]
1220 unfolding epOwnerF(p2, p2) in
1221 unfolding epOwnerFault(p2, p2) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1218 unfolding epOwnerTiebreaker(p1, p1) in
1219 unfolding epOwnerN(p2, p2) in
[----------------
1220 unfolding epOwnerF(p2, p2) in
----------------]
1221 unfolding epOwnerFault(p2, p2) in
1222 unfolding epOwnerV(p2, p2) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1219 unfolding epOwnerN(p2, p2) in
1220 unfolding epOwnerF(p2, p2) in
[--------------------
1221 unfolding epOwnerFault(p2, p2) in
--------------------]
1222 unfolding epOwnerV(p2, p2) in
1223 unfolding epOwnerV1(p2, p2) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1220 unfolding epOwnerF(p2, p2) in
1221 unfolding epOwnerFault(p2, p2) in
[----------------
1222 unfolding epOwnerV(p2, p2) in
----------------]
1223 unfolding epOwnerV1(p2, p2) in
1224 unfolding epOwnerV2(p2, p2) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1221 unfolding epOwnerFault(p2, p2) in
1222 unfolding epOwnerV(p2, p2) in
[-----------------
1223 unfolding epOwnerV1(p2, p2) in
-----------------]
1224 unfolding epOwnerV2(p2, p2) in
1225 unfolding epOwnerV3(p2, p2) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1222 unfolding epOwnerV(p2, p2) in
1223 unfolding epOwnerV1(p2, p2) in
[-----------------
1224 unfolding epOwnerV2(p2, p2) in
-----------------]
1225 unfolding epOwnerV3(p2, p2) in
1226 unfolding epOwnerTiebreaker(p2, p2) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1223 unfolding epOwnerV1(p2, p2) in
1224 unfolding epOwnerV2(p2, p2) in
[-----------------
1225 unfolding epOwnerV3(p2, p2) in
-----------------]
1226 unfolding epOwnerTiebreaker(p2, p2) in
1227 unfolding epOwnerN(p3, p3) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1224 unfolding epOwnerV2(p2, p2) in
1225 unfolding epOwnerV3(p2, p2) in
[-------------------------
1226 unfolding epOwnerTiebreaker(p2, p2) in
-------------------------]
1227 unfolding epOwnerN(p3, p3) in
1228 unfolding epOwnerF(p3, p3) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1225 unfolding epOwnerV3(p2, p2) in
1226 unfolding epOwnerTiebreaker(p2, p2) in
[----------------
1227 unfolding epOwnerN(p3, p3) in
----------------]
1228 unfolding epOwnerF(p3, p3) in
1229 unfolding epOwnerFault(p3, p3) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1226 unfolding epOwnerTiebreaker(p2, p2) in
1227 unfolding epOwnerN(p3, p3) in
[----------------
1228 unfolding epOwnerF(p3, p3) in
----------------]
1229 unfolding epOwnerFault(p3, p3) in
1230 unfolding epOwnerV(p3, p3) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1227 unfolding epOwnerN(p3, p3) in
1228 unfolding epOwnerF(p3, p3) in
[--------------------
1229 unfolding epOwnerFault(p3, p3) in
--------------------]
1230 unfolding epOwnerV(p3, p3) in
1231 unfolding epOwnerV1(
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1228 unfolding epOwnerF(p3, p3) in
1229 unfolding epOwnerFault(p3, p3) in
[----------------
1230 unfolding epOwnerV(p3, p3) in
----------------]
1231 unfolding epOwnerV1(
1232 p3,
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1229 unfolding epOwnerFault(p3, p3) in
1230 unfolding epOwnerV(p3, p3) in
[----------
1231 unfolding epOwnerV1(
1232 p3,
1233 p3
1234 ) in
---------------------------------------------------------------------------------------------]
1235 unfolding epOwnerV2(
1236 p3,
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1233 p3
1234 ) in
[----------
1235 unfolding epOwnerV2(
1236 p3,
1237 p3
1238 ) in
-------------------------------------------------------------------------------------------------]
1239 unfolding epOwnerV3(
1240 p3,
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1237 p3
1238 ) in
[----------
1239 unfolding epOwnerV3(
1240 p3,
1241 p3
1242 ) in
-----------------------------------------------------------------------------------------------------]
1243 unfolding epOwnerTiebreaker(
1244 p3,
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1241 p3
1242 ) in
[------------------
1243 unfolding epOwnerTiebreaker(
1244 p3,
1245 p3
1246 ) in
---------------------------------------------------------------------------------------------------------]
1247 [write](p1.n ==
1248 p2.n &&
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1257 p3.f ==
1258 p1.f)) **
[----------------
1259 (unfolding epOwnerN(p1, p1) in
----------------]
1260 unfolding epOwnerF(p1, p1) in
1261 unfolding epOwnerFault(p1, p1) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1258 p1.f)) **
1259 (unfolding epOwnerN(p1, p1) in
[----------------
1260 unfolding epOwnerF(p1, p1) in
----------------]
1261 unfolding epOwnerFault(p1, p1) in
1262 unfolding epOwnerV(p1, p1) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1259 (unfolding epOwnerN(p1, p1) in
1260 unfolding epOwnerF(p1, p1) in
[--------------------
1261 unfolding epOwnerFault(p1, p1) in
--------------------]
1262 unfolding epOwnerV(p1, p1) in
1263 unfolding epOwnerV1(p1, p1) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1260 unfolding epOwnerF(p1, p1) in
1261 unfolding epOwnerFault(p1, p1) in
[----------------
1262 unfolding epOwnerV(p1, p1) in
----------------]
1263 unfolding epOwnerV1(p1, p1) in
1264 unfolding epOwnerV2(p1, p1) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1261 unfolding epOwnerFault(p1, p1) in
1262 unfolding epOwnerV(p1, p1) in
[-----------------
1263 unfolding epOwnerV1(p1, p1) in
-----------------]
1264 unfolding epOwnerV2(p1, p1) in
1265 unfolding epOwnerV3(p1, p1) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1262 unfolding epOwnerV(p1, p1) in
1263 unfolding epOwnerV1(p1, p1) in
[-----------------
1264 unfolding epOwnerV2(p1, p1) in
-----------------]
1265 unfolding epOwnerV3(p1, p1) in
1266 unfolding epOwnerTiebreaker(p1, p1) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1263 unfolding epOwnerV1(p1, p1) in
1264 unfolding epOwnerV2(p1, p1) in
[-----------------
1265 unfolding epOwnerV3(p1, p1) in
-----------------]
1266 unfolding epOwnerTiebreaker(p1, p1) in
1267 unfolding epOwnerN(p2, p2) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1264 unfolding epOwnerV2(p1, p1) in
1265 unfolding epOwnerV3(p1, p1) in
[-------------------------
1266 unfolding epOwnerTiebreaker(p1, p1) in
-------------------------]
1267 unfolding epOwnerN(p2, p2) in
1268 unfolding epOwnerF(p2, p2) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1265 unfolding epOwnerV3(p1, p1) in
1266 unfolding epOwnerTiebreaker(p1, p1) in
[----------------
1267 unfolding epOwnerN(p2, p2) in
----------------]
1268 unfolding epOwnerF(p2, p2) in
1269 unfolding epOwnerFault(p2, p2) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1266 unfolding epOwnerTiebreaker(p1, p1) in
1267 unfolding epOwnerN(p2, p2) in
[----------------
1268 unfolding epOwnerF(p2, p2) in
----------------]
1269 unfolding epOwnerFault(p2, p2) in
1270 unfolding epOwnerV(p2, p2) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1267 unfolding epOwnerN(p2, p2) in
1268 unfolding epOwnerF(p2, p2) in
[--------------------
1269 unfolding epOwnerFault(p2, p2) in
--------------------]
1270 unfolding epOwnerV(p2, p2) in
1271 unfolding epOwnerV1(p2, p2) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1268 unfolding epOwnerF(p2, p2) in
1269 unfolding epOwnerFault(p2, p2) in
[----------------
1270 unfolding epOwnerV(p2, p2) in
----------------]
1271 unfolding epOwnerV1(p2, p2) in
1272 unfolding epOwnerV2(p2, p2) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1269 unfolding epOwnerFault(p2, p2) in
1270 unfolding epOwnerV(p2, p2) in
[-----------------
1271 unfolding epOwnerV1(p2, p2) in
-----------------]
1272 unfolding epOwnerV2(p2, p2) in
1273 unfolding epOwnerV3(p2, p2) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1270 unfolding epOwnerV(p2, p2) in
1271 unfolding epOwnerV1(p2, p2) in
[-----------------
1272 unfolding epOwnerV2(p2, p2) in
-----------------]
1273 unfolding epOwnerV3(p2, p2) in
1274 unfolding epOwnerTiebreaker(p2, p2) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1271 unfolding epOwnerV1(p2, p2) in
1272 unfolding epOwnerV2(p2, p2) in
[-----------------
1273 unfolding epOwnerV3(p2, p2) in
-----------------]
1274 unfolding epOwnerTiebreaker(p2, p2) in
1275 unfolding epOwnerN(p3, p3) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1272 unfolding epOwnerV2(p2, p2) in
1273 unfolding epOwnerV3(p2, p2) in
[-------------------------
1274 unfolding epOwnerTiebreaker(p2, p2) in
-------------------------]
1275 unfolding epOwnerN(p3, p3) in
1276 unfolding epOwnerF(p3, p3) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1273 unfolding epOwnerV3(p2, p2) in
1274 unfolding epOwnerTiebreaker(p2, p2) in
[----------------
1275 unfolding epOwnerN(p3, p3) in
----------------]
1276 unfolding epOwnerF(p3, p3) in
1277 unfolding epOwnerFault(p3, p3) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1274 unfolding epOwnerTiebreaker(p2, p2) in
1275 unfolding epOwnerN(p3, p3) in
[----------------
1276 unfolding epOwnerF(p3, p3) in
----------------]
1277 unfolding epOwnerFault(p3, p3) in
1278 unfolding epOwnerV(p3, p3) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1275 unfolding epOwnerN(p3, p3) in
1276 unfolding epOwnerF(p3, p3) in
[--------------------
1277 unfolding epOwnerFault(p3, p3) in
--------------------]
1278 unfolding epOwnerV(p3, p3) in
1279 unfolding epOwnerV1(
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1276 unfolding epOwnerF(p3, p3) in
1277 unfolding epOwnerFault(p3, p3) in
[----------------
1278 unfolding epOwnerV(p3, p3) in
----------------]
1279 unfolding epOwnerV1(
1280 p3,
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1277 unfolding epOwnerFault(p3, p3) in
1278 unfolding epOwnerV(p3, p3) in
[----------
1279 unfolding epOwnerV1(
1280 p3,
1281 p3
1282 ) in
---------------------------------------------------------------------------------------------]
1283 unfolding epOwnerV2(
1284 p3,
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1281 p3
1282 ) in
[----------
1283 unfolding epOwnerV2(
1284 p3,
1285 p3
1286 ) in
-------------------------------------------------------------------------------------------------]
1287 unfolding epOwnerV3(
1288 p3,
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1285 p3
1286 ) in
[----------
1287 unfolding epOwnerV3(
1288 p3,
1289 p3
1290 ) in
-----------------------------------------------------------------------------------------------------]
1291 unfolding epOwnerTiebreaker(
1292 p3,
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1289 p3
1290 ) in
[------------------
1291 unfolding epOwnerTiebreaker(
1292 p3,
1293 p3
1294 ) in
---------------------------------------------------------------------------------------------------------]
1295 p1.fault +
1296 p2.fault +
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1370 (readV3(p3, p3) == 0 || readV3(p3, p3) == 1) &&
1371 (readTiebreaker(p3, p3) == 0 || readTiebreaker(p3, p3) == 1));
[----------------
1372 requires unfolding epOwnerN(p1, p1) in
----------------]
1373 unfolding epOwnerF(p1, p1) in
1374 unfolding epOwnerFault(p1, p1) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1371 (readTiebreaker(p3, p3) == 0 || readTiebreaker(p3, p3) == 1));
1372 requires unfolding epOwnerN(p1, p1) in
[----------------
1373 unfolding epOwnerF(p1, p1) in
----------------]
1374 unfolding epOwnerFault(p1, p1) in
1375 unfolding epOwnerV(p1, p1) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1372 requires unfolding epOwnerN(p1, p1) in
1373 unfolding epOwnerF(p1, p1) in
[--------------------
1374 unfolding epOwnerFault(p1, p1) in
--------------------]
1375 unfolding epOwnerV(p1, p1) in
1376 unfolding epOwnerV1(p1, p1) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1373 unfolding epOwnerF(p1, p1) in
1374 unfolding epOwnerFault(p1, p1) in
[----------------
1375 unfolding epOwnerV(p1, p1) in
----------------]
1376 unfolding epOwnerV1(p1, p1) in
1377 unfolding epOwnerV2(p1, p1) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1374 unfolding epOwnerFault(p1, p1) in
1375 unfolding epOwnerV(p1, p1) in
[-----------------
1376 unfolding epOwnerV1(p1, p1) in
-----------------]
1377 unfolding epOwnerV2(p1, p1) in
1378 unfolding epOwnerV3(p1, p1) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1375 unfolding epOwnerV(p1, p1) in
1376 unfolding epOwnerV1(p1, p1) in
[-----------------
1377 unfolding epOwnerV2(p1, p1) in
-----------------]
1378 unfolding epOwnerV3(p1, p1) in
1379 unfolding epOwnerTiebreaker(p1, p1) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1376 unfolding epOwnerV1(p1, p1) in
1377 unfolding epOwnerV2(p1, p1) in
[-----------------
1378 unfolding epOwnerV3(p1, p1) in
-----------------]
1379 unfolding epOwnerTiebreaker(p1, p1) in
1380 unfolding epOwnerN(p2, p2) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1377 unfolding epOwnerV2(p1, p1) in
1378 unfolding epOwnerV3(p1, p1) in
[-------------------------
1379 unfolding epOwnerTiebreaker(p1, p1) in
-------------------------]
1380 unfolding epOwnerN(p2, p2) in
1381 unfolding epOwnerF(p2, p2) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1378 unfolding epOwnerV3(p1, p1) in
1379 unfolding epOwnerTiebreaker(p1, p1) in
[----------------
1380 unfolding epOwnerN(p2, p2) in
----------------]
1381 unfolding epOwnerF(p2, p2) in
1382 unfolding epOwnerFault(p2, p2) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1379 unfolding epOwnerTiebreaker(p1, p1) in
1380 unfolding epOwnerN(p2, p2) in
[----------------
1381 unfolding epOwnerF(p2, p2) in
----------------]
1382 unfolding epOwnerFault(p2, p2) in
1383 unfolding epOwnerV(p2, p2) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1380 unfolding epOwnerN(p2, p2) in
1381 unfolding epOwnerF(p2, p2) in
[--------------------
1382 unfolding epOwnerFault(p2, p2) in
--------------------]
1383 unfolding epOwnerV(p2, p2) in
1384 unfolding epOwnerV1(p2, p2) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1381 unfolding epOwnerF(p2, p2) in
1382 unfolding epOwnerFault(p2, p2) in
[----------------
1383 unfolding epOwnerV(p2, p2) in
----------------]
1384 unfolding epOwnerV1(p2, p2) in
1385 unfolding epOwnerV2(p2, p2) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1382 unfolding epOwnerFault(p2, p2) in
1383 unfolding epOwnerV(p2, p2) in
[-----------------
1384 unfolding epOwnerV1(p2, p2) in
-----------------]
1385 unfolding epOwnerV2(p2, p2) in
1386 unfolding epOwnerV3(p2, p2) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1383 unfolding epOwnerV(p2, p2) in
1384 unfolding epOwnerV1(p2, p2) in
[-----------------
1385 unfolding epOwnerV2(p2, p2) in
-----------------]
1386 unfolding epOwnerV3(p2, p2) in
1387 unfolding epOwnerTiebreaker(p2, p2) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1384 unfolding epOwnerV1(p2, p2) in
1385 unfolding epOwnerV2(p2, p2) in
[-----------------
1386 unfolding epOwnerV3(p2, p2) in
-----------------]
1387 unfolding epOwnerTiebreaker(p2, p2) in
1388 unfolding epOwnerN(p3, p3) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1385 unfolding epOwnerV2(p2, p2) in
1386 unfolding epOwnerV3(p2, p2) in
[-------------------------
1387 unfolding epOwnerTiebreaker(p2, p2) in
-------------------------]
1388 unfolding epOwnerN(p3, p3) in
1389 unfolding epOwnerF(p3, p3) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1386 unfolding epOwnerV3(p2, p2) in
1387 unfolding epOwnerTiebreaker(p2, p2) in
[----------------
1388 unfolding epOwnerN(p3, p3) in
----------------]
1389 unfolding epOwnerF(p3, p3) in
1390 unfolding epOwnerFault(p3, p3) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1387 unfolding epOwnerTiebreaker(p2, p2) in
1388 unfolding epOwnerN(p3, p3) in
[----------------
1389 unfolding epOwnerF(p3, p3) in
----------------]
1390 unfolding epOwnerFault(p3, p3) in
1391 unfolding epOwnerV(p3, p3) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1388 unfolding epOwnerN(p3, p3) in
1389 unfolding epOwnerF(p3, p3) in
[--------------------
1390 unfolding epOwnerFault(p3, p3) in
--------------------]
1391 unfolding epOwnerV(p3, p3) in
1392 unfolding epOwnerV1(p3, p3) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1389 unfolding epOwnerF(p3, p3) in
1390 unfolding epOwnerFault(p3, p3) in
[----------------
1391 unfolding epOwnerV(p3, p3) in
----------------]
1392 unfolding epOwnerV1(p3, p3) in
1393 unfolding epOwnerV2(p3, p3) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1390 unfolding epOwnerFault(p3, p3) in
1391 unfolding epOwnerV(p3, p3) in
[-----------------
1392 unfolding epOwnerV1(p3, p3) in
-----------------]
1393 unfolding epOwnerV2(p3, p3) in
1394 unfolding epOwnerV3(
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1391 unfolding epOwnerV(p3, p3) in
1392 unfolding epOwnerV1(p3, p3) in
[-----------------
1393 unfolding epOwnerV2(p3, p3) in
-----------------]
1394 unfolding epOwnerV3(
1395 p3,
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1392 unfolding epOwnerV1(p3, p3) in
1393 unfolding epOwnerV2(p3, p3) in
[----------
1394 unfolding epOwnerV3(
1395 p3,
1396 p3
1397 ) in
---------------------------------------------------------------------------------------------]
1398 unfolding epOwnerTiebreaker(
1399 p3,
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1396 p3
1397 ) in
[------------------
1398 unfolding epOwnerTiebreaker(
1399 p3,
1400 p3
1401 ) in
-------------------------------------------------------------------------------------------------]
1402 [write](p1.n ==
1403 p2.n &&
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1407 p2.f == p3.f &&
1408 p3.f == p1.f);
[----------------
1409 requires unfolding epOwnerN(p1, p1) in
----------------]
1410 unfolding epOwnerF(p1, p1) in
1411 unfolding epOwnerFault(p1, p1) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1408 p3.f == p1.f);
1409 requires unfolding epOwnerN(p1, p1) in
[----------------
1410 unfolding epOwnerF(p1, p1) in
----------------]
1411 unfolding epOwnerFault(p1, p1) in
1412 unfolding epOwnerV(p1, p1) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1409 requires unfolding epOwnerN(p1, p1) in
1410 unfolding epOwnerF(p1, p1) in
[--------------------
1411 unfolding epOwnerFault(p1, p1) in
--...
Check failure on line 222 in test/main/vct/test/integration/helper/VeyMontSpec.scala
github-actions / TestReport
vct.test.integration.examples.veymont.FM2023VeyMontSpec ► Files examples/publications/2023/FM2023VeyMont/applicability/election-5.pvl verifies with silicon
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:Raw output
org.scalatest.exceptions.TestFailedException: Pass did not equal Crash(vct.main.modes.VeyMont$WrapSystemError: The following error occurred during choreography verification:
The encodePermissionStratification rewrite caused the AST to no longer typecheck:
======================================
1079 !p4.hasMaxIdP4(p4) **
1080 !p5.hasMaxIdP5(p5) **
[---------------------
1081 (unfolding epOwnerLeader(p1, p1) in
---------------------]
1082 unfolding epOwnerId1(p1, p1) in
1083 unfolding epOwnerId2(p1, p1) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1080 !p5.hasMaxIdP5(p5) **
1081 (unfolding epOwnerLeader(p1, p1) in
[------------------
1082 unfolding epOwnerId1(p1, p1) in
------------------]
1083 unfolding epOwnerId2(p1, p1) in
1084 unfolding epOwnerId3(p1, p1) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1081 (unfolding epOwnerLeader(p1, p1) in
1082 unfolding epOwnerId1(p1, p1) in
[------------------
1083 unfolding epOwnerId2(p1, p1) in
------------------]
1084 unfolding epOwnerId3(p1, p1) in
1085 unfolding epOwnerId4(p1, p1) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1082 unfolding epOwnerId1(p1, p1) in
1083 unfolding epOwnerId2(p1, p1) in
[------------------
1084 unfolding epOwnerId3(p1, p1) in
------------------]
1085 unfolding epOwnerId4(p1, p1) in
1086 unfolding epOwnerId5(p1, p1) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1083 unfolding epOwnerId2(p1, p1) in
1084 unfolding epOwnerId3(p1, p1) in
[------------------
1085 unfolding epOwnerId4(p1, p1) in
------------------]
1086 unfolding epOwnerId5(p1, p1) in
1087 unfolding epOwnerLeader(p2, p2) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1084 unfolding epOwnerId3(p1, p1) in
1085 unfolding epOwnerId4(p1, p1) in
[------------------
1086 unfolding epOwnerId5(p1, p1) in
------------------]
1087 unfolding epOwnerLeader(p2, p2) in
1088 unfolding epOwnerId1(p2, p2) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1085 unfolding epOwnerId4(p1, p1) in
1086 unfolding epOwnerId5(p1, p1) in
[---------------------
1087 unfolding epOwnerLeader(p2, p2) in
---------------------]
1088 unfolding epOwnerId1(p2, p2) in
1089 unfolding epOwnerId2(p2, p2) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1086 unfolding epOwnerId5(p1, p1) in
1087 unfolding epOwnerLeader(p2, p2) in
[------------------
1088 unfolding epOwnerId1(p2, p2) in
------------------]
1089 unfolding epOwnerId2(p2, p2) in
1090 unfolding epOwnerId3(p2, p2) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1087 unfolding epOwnerLeader(p2, p2) in
1088 unfolding epOwnerId1(p2, p2) in
[------------------
1089 unfolding epOwnerId2(p2, p2) in
------------------]
1090 unfolding epOwnerId3(p2, p2) in
1091 unfolding epOwnerId4(p2, p2) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1088 unfolding epOwnerId1(p2, p2) in
1089 unfolding epOwnerId2(p2, p2) in
[------------------
1090 unfolding epOwnerId3(p2, p2) in
------------------]
1091 unfolding epOwnerId4(p2, p2) in
1092 unfolding epOwnerId5(p2, p2) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1089 unfolding epOwnerId2(p2, p2) in
1090 unfolding epOwnerId3(p2, p2) in
[------------------
1091 unfolding epOwnerId4(p2, p2) in
------------------]
1092 unfolding epOwnerId5(p2, p2) in
1093 unfolding epOwnerLeader(p3, p3) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1090 unfolding epOwnerId3(p2, p2) in
1091 unfolding epOwnerId4(p2, p2) in
[------------------
1092 unfolding epOwnerId5(p2, p2) in
------------------]
1093 unfolding epOwnerLeader(p3, p3) in
1094 unfolding epOwnerId1(p3, p3) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1091 unfolding epOwnerId4(p2, p2) in
1092 unfolding epOwnerId5(p2, p2) in
[---------------------
1093 unfolding epOwnerLeader(p3, p3) in
---------------------]
1094 unfolding epOwnerId1(p3, p3) in
1095 unfolding epOwnerId2(p3, p3) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1092 unfolding epOwnerId5(p2, p2) in
1093 unfolding epOwnerLeader(p3, p3) in
[------------------
1094 unfolding epOwnerId1(p3, p3) in
------------------]
1095 unfolding epOwnerId2(p3, p3) in
1096 unfolding epOwnerId3(p3, p3) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1093 unfolding epOwnerLeader(p3, p3) in
1094 unfolding epOwnerId1(p3, p3) in
[------------------
1095 unfolding epOwnerId2(p3, p3) in
------------------]
1096 unfolding epOwnerId3(p3, p3) in
1097 unfolding epOwnerId4(p3, p3) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1094 unfolding epOwnerId1(p3, p3) in
1095 unfolding epOwnerId2(p3, p3) in
[------------------
1096 unfolding epOwnerId3(p3, p3) in
------------------]
1097 unfolding epOwnerId4(p3, p3) in
1098 unfolding epOwnerId5(p3, p3) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1095 unfolding epOwnerId2(p3, p3) in
1096 unfolding epOwnerId3(p3, p3) in
[------------------
1097 unfolding epOwnerId4(p3, p3) in
------------------]
1098 unfolding epOwnerId5(p3, p3) in
1099 unfolding epOwnerLeader(p4, p4) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1096 unfolding epOwnerId3(p3, p3) in
1097 unfolding epOwnerId4(p3, p3) in
[------------------
1098 unfolding epOwnerId5(p3, p3) in
------------------]
1099 unfolding epOwnerLeader(p4, p4) in
1100 unfolding epOwnerId1(p4, p4) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1097 unfolding epOwnerId4(p3, p3) in
1098 unfolding epOwnerId5(p3, p3) in
[---------------------
1099 unfolding epOwnerLeader(p4, p4) in
---------------------]
1100 unfolding epOwnerId1(p4, p4) in
1101 unfolding epOwnerId2(
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1098 unfolding epOwnerId5(p3, p3) in
1099 unfolding epOwnerLeader(p4, p4) in
[------------------
1100 unfolding epOwnerId1(p4, p4) in
------------------]
1101 unfolding epOwnerId2(
1102 p4,
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1099 unfolding epOwnerLeader(p4, p4) in
1100 unfolding epOwnerId1(p4, p4) in
[-----------
1101 unfolding epOwnerId2(
1102 p4,
1103 p4
1104 ) in
---------------------------------------------------------------------------------------------]
1105 unfolding epOwnerId3(
1106 p4,
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1103 p4
1104 ) in
[-----------
1105 unfolding epOwnerId3(
1106 p4,
1107 p4
1108 ) in
-------------------------------------------------------------------------------------------------]
1109 unfolding epOwnerId4(
1110 p4,
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1107 p4
1108 ) in
[-----------
1109 unfolding epOwnerId4(
1110 p4,
1111 p4
1112 ) in
-----------------------------------------------------------------------------------------------------]
1113 unfolding epOwnerId5(
1114 p4,
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1111 p4
1112 ) in
[-----------
1113 unfolding epOwnerId5(
1114 p4,
1115 p4
1116 ) in
---------------------------------------------------------------------------------------------------------]
1117 unfolding epOwnerLeader(
1118 p5,
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1115 p4
1116 ) in
[--------------
1117 unfolding epOwnerLeader(
1118 p5,
1119 p5
1120 ) in
-------------------------------------------------------------------------------------------------------------]
1121 unfolding epOwnerId1(
1122 p5,
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1119 p5
1120 ) in
[-----------
1121 unfolding epOwnerId1(
1122 p5,
1123 p5
1124 ) in
-----------------------------------------------------------------------------------------------------------------]
1125 unfolding epOwnerId2(
1126 p5,
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1123 p5
1124 ) in
[-----------
1125 unfolding epOwnerId2(
1126 p5,
1127 p5
1128 ) in
---------------------------------------------------------------------------------------------------------------------]
1129 unfolding epOwnerId3(
1130 p5,
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1127 p5
1128 ) in
[-----------
1129 unfolding epOwnerId3(
1130 p5,
1131 p5
1132 ) in
-------------------------------------------------------------------------------------------------------------------------]
1133 unfolding epOwnerId4(
1134 p5,
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1131 p5
1132 ) in
[-----------
1133 unfolding epOwnerId4(
1134 p5,
1135 p5
1136 ) in
-----------------------------------------------------------------------------------------------------------------------------]
1137 unfolding epOwnerId5(
1138 p5,
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1135 p5
1136 ) in
[-----------
1137 unfolding epOwnerId5(
1138 p5,
1139 p5
1140 ) in
---------------------------------------------------------------------------------------------------------------------------------]
1141 [write](p1.id1 ==
1142 p2.id1 &&
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1597 loop_invariant !readLeader(p4, p4);
1598 loop_invariant !readLeader(p5, p5);
[---------------------
1599 loop_invariant unfolding epOwnerLeader(p1, p1) in
---------------------]
1600 unfolding epOwnerId1(p1, p1) in
1601 unfolding epOwnerId2(p1, p1) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1598 loop_invariant !readLeader(p5, p5);
1599 loop_invariant unfolding epOwnerLeader(p1, p1) in
[------------------
1600 unfolding epOwnerId1(p1, p1) in
------------------]
1601 unfolding epOwnerId2(p1, p1) in
1602 unfolding epOwnerId3(p1, p1) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1599 loop_invariant unfolding epOwnerLeader(p1, p1) in
1600 unfolding epOwnerId1(p1, p1) in
[------------------
1601 unfolding epOwnerId2(p1, p1) in
------------------]
1602 unfolding epOwnerId3(p1, p1) in
1603 unfolding epOwnerId4(p1, p1) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1600 unfolding epOwnerId1(p1, p1) in
1601 unfolding epOwnerId2(p1, p1) in
[------------------
1602 unfolding epOwnerId3(p1, p1) in
------------------]
1603 unfolding epOwnerId4(p1, p1) in
1604 unfolding epOwnerId5(p1, p1) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1601 unfolding epOwnerId2(p1, p1) in
1602 unfolding epOwnerId3(p1, p1) in
[------------------
1603 unfolding epOwnerId4(p1, p1) in
------------------]
1604 unfolding epOwnerId5(p1, p1) in
1605 unfolding epOwnerLeader(p2, p2) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1602 unfolding epOwnerId3(p1, p1) in
1603 unfolding epOwnerId4(p1, p1) in
[------------------
1604 unfolding epOwnerId5(p1, p1) in
------------------]
1605 unfolding epOwnerLeader(p2, p2) in
1606 unfolding epOwnerId1(p2, p2) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1603 unfolding epOwnerId4(p1, p1) in
1604 unfolding epOwnerId5(p1, p1) in
[---------------------
1605 unfolding epOwnerLeader(p2, p2) in
---------------------]
1606 unfolding epOwnerId1(p2, p2) in
1607 unfolding epOwnerId2(p2, p2) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1604 unfolding epOwnerId5(p1, p1) in
1605 unfolding epOwnerLeader(p2, p2) in
[------------------
1606 unfolding epOwnerId1(p2, p2) in
------------------]
1607 unfolding epOwnerId2(p2, p2) in
1608 unfolding epOwnerId3(p2, p2) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1605 unfolding epOwnerLeader(p2, p2) in
1606 unfolding epOwnerId1(p2, p2) in
[------------------
1607 unfolding epOwnerId2(p2, p2) in
------------------]
1608 unfolding epOwnerId3(p2, p2) in
1609 unfolding epOwnerId4(p2, p2) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1606 unfolding epOwnerId1(p2, p2) in
1607 unfolding epOwnerId2(p2, p2) in
[------------------
1608 unfolding epOwnerId3(p2, p2) in
------------------]
1609 unfolding epOwnerId4(p2, p2) in
1610 unfolding epOwnerId5(p2, p2) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1607 unfolding epOwnerId2(p2, p2) in
1608 unfolding epOwnerId3(p2, p2) in
[------------------
1609 unfolding epOwnerId4(p2, p2) in
------------------]
1610 unfolding epOwnerId5(p2, p2) in
1611 unfolding epOwnerLeader(p3, p3) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1608 unfolding epOwnerId3(p2, p2) in
1609 unfolding epOwnerId4(p2, p2) in
[------------------
1610 unfolding epOwnerId5(p2, p2) in
------------------]
1611 unfolding epOwnerLeader(p3, p3) in
1612 unfolding epOwnerId1(p3, p3) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1609 unfolding epOwnerId4(p2, p2) in
1610 unfolding epOwnerId5(p2, p2) in
[---------------------
1611 unfolding epOwnerLeader(p3, p3) in
---------------------]
1612 unfolding epOwnerId1(p3, p3) in
1613 unfolding epOwnerId2(p3, p3) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1610 unfolding epOwnerId5(p2, p2) in
1611 unfolding epOwnerLeader(p3, p3) in
[------------------
1612 unfolding epOwnerId1(p3, p3) in
------------------]
1613 unfolding epOwnerId2(p3, p3) in
1614 unfolding epOwnerId3(p3, p3) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1611 unfolding epOwnerLeader(p3, p3) in
1612 unfolding epOwnerId1(p3, p3) in
[------------------
1613 unfolding epOwnerId2(p3, p3) in
------------------]
1614 unfolding epOwnerId3(p3, p3) in
1615 unfolding epOwnerId4(p3, p3) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1612 unfolding epOwnerId1(p3, p3) in
1613 unfolding epOwnerId2(p3, p3) in
[------------------
1614 unfolding epOwnerId3(p3, p3) in
------------------]
1615 unfolding epOwnerId4(p3, p3) in
1616 unfolding epOwnerId5(p3, p3) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1613 unfolding epOwnerId2(p3, p3) in
1614 unfolding epOwnerId3(p3, p3) in
[------------------
1615 unfolding epOwnerId4(p3, p3) in
------------------]
1616 unfolding epOwnerId5(p3, p3) in
1617 unfolding epOwnerLeader(p4, p4) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1614 unfolding epOwnerId3(p3, p3) in
1615 unfolding epOwnerId4(p3, p3) in
[------------------
1616 unfolding epOwnerId5(p3, p3) in
------------------]
1617 unfolding epOwnerLeader(p4, p4) in
1618 unfolding epOwnerId1(p4, p4) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1615 unfolding epOwnerId4(p3, p3) in
1616 unfolding epOwnerId5(p3, p3) in
[---------------------
1617 unfolding epOwnerLeader(p4, p4) in
---------------------]
1618 unfolding epOwnerId1(p4, p4) in
1619 unfolding epOwnerId2(p4, p4) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1616 unfolding epOwnerId5(p3, p3) in
1617 unfolding epOwnerLeader(p4, p4) in
[------------------
1618 unfolding epOwnerId1(p4, p4) in
------------------]
1619 unfolding epOwnerId2(p4, p4) in
1620 unfolding epOwnerId3(
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1617 unfolding epOwnerLeader(p4, p4) in
1618 unfolding epOwnerId1(p4, p4) in
[------------------
1619 unfolding epOwnerId2(p4, p4) in
------------------]
1620 unfolding epOwnerId3(
1621 p4,
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1618 unfolding epOwnerId1(p4, p4) in
1619 unfolding epOwnerId2(p4, p4) in
[-----------
1620 unfolding epOwnerId3(
1621 p4,
1622 p4
1623 ) in
---------------------------------------------------------------------------------------------]
1624 unfolding epOwnerId4(
1625 p4,
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1622 p4
1623 ) in
[-----------
1624 unfolding epOwnerId4(
1625 p4,
1626 p4
1627 ) in
-------------------------------------------------------------------------------------------------]
1628 unfolding epOwnerId5(
1629 p4,
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1626 p4
1627 ) in
[-----------
1628 unfolding epOwnerId5(
1629 p4,
1630 p4
1631 ) in
-----------------------------------------------------------------------------------------------------]
1632 unfolding epOwnerLeader(
1633 p5,
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1630 p4
1631 ) in
[--------------
1632 unfolding epOwnerLeader(
1633 p5,
1634 p5
1635 ) in
---------------------------------------------------------------------------------------------------------]
1636 unfolding epOwnerId1(
1637 p5,
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1634 p5
1635 ) in
[-----------
1636 unfolding epOwnerId1(
1637 p5,
1638 p5
1639 ) in
-------------------------------------------------------------------------------------------------------------]
1640 unfolding epOwnerId2(
1641 p5,
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1638 p5
1639 ) in
[-----------
1640 unfolding epOwnerId2(
1641 p5,
1642 p5
1643 ) in
-----------------------------------------------------------------------------------------------------------------]
1644 unfolding epOwnerId3(
1645 p5,
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1642 p5
1643 ) in
[-----------
1644 unfolding epOwnerId3(
1645 p5,
1646 p5
1647 ) in
---------------------------------------------------------------------------------------------------------------------]
1648 unfolding epOwnerId4(
1649 p5,
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1646 p5
1647 ) in
[-----------
1648 unfolding epOwnerId4(
1649 p5,
1650 p5
1651 ) in
-------------------------------------------------------------------------------------------------------------------------]
1652 unfolding epOwnerId5(
1653 p5,
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1650 p5
1651 ) in
[-----------
1652 unfolding epOwnerId5(
1653 p5,
1654 p5
1655 ) in
-----------------------------------------------------------------------------------------------------------------------------]
1656 [write](p1.id1 ==
1657 p2.id1 &&
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1276 requires !p4.hasMaxIdP4(p4);
1277 requires !p5.hasMaxIdP5(p5);
[---------------------
1278 requires unfolding epOwnerLeader(p1, p1) in
---------------------]
1279 unfolding epOwnerId1(p1, p1) in
1280 unfolding epOwnerId2(p1, p1) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1277 requires !p5.hasMaxIdP5(p5);
1278 requires unfolding epOwnerLeader(p1, p1) in
[------------------
1279 unfolding epOwnerId1(p1, p1) in
------------------]
1280 unfolding epOwnerId2(p1, p1) in
1281 unfolding epOwnerId3(p1, p1) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1278 requires unfolding epOwnerLeader(p1, p1) in
1279 unfolding epOwnerId1(p1, p1) in
[------------------
1280 unfolding epOwnerId2(p1, p1) in
------------------]
1281 unfolding epOwnerId3(p1, p1) in
1282 unfolding epOwnerId4(p1, p1) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1279 unfolding epOwnerId1(p1, p1) in
1280 unfolding epOwnerId2(p1, p1) in
[------------------
1281 unfolding epOwnerId3(p1, p1) in
------------------]
1282 unfolding epOwnerId4(p1, p1) in
1283 unfolding epOwnerId5(p1, p1) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1280 unfolding epOwnerId2(p1, p1) in
1281 unfolding epOwnerId3(p1, p1) in
[------------------
1282 unfolding epOwnerId4(p1, p1) in
------------------]
1283 unfolding epOwnerId5(p1, p1) in
1284 unfolding epOwnerLeader(p2, p2) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1281 unfolding epOwnerId3(p1, p1) in
1282 unfolding epOwnerId4(p1, p1) in
[------------------
1283 unfolding epOwnerId5(p1, p1) in
------------------]
1284 unfolding epOwnerLeader(p2, p2) in
1285 unfolding epOwnerId1(p2, p2) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1282 unfolding epOwnerId4(p1, p1) in
1283 unfolding epOwnerId5(p1, p1) in
[---------------------
1284 unfolding epOwnerLeader(p2, p2) in
---------------------]
1285 unfolding epOwnerId1(p2, p2) in
1286 unfolding epOwnerId2(p2, p2) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
=======================...
Check failure on line 222 in test/main/vct/test/integration/helper/VeyMontSpec.scala
github-actions / TestReport
vct.test.integration.examples.veymont.FM2023VeyMontSpec ► Files examples/publications/2023/FM2023VeyMont/applicability/consensus-5.pvl verifies with silicon
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:Raw output
org.scalatest.exceptions.TestFailedException: Pass did not equal Crash(vct.main.modes.VeyMont$WrapSystemError: The following error occurred during choreography verification:
The encodePermissionStratification rewrite caused the AST to no longer typecheck:
======================================
2287 (readV5(p5, p5) == 0 || readV5(p5, p5) == 1) &&
2288 (readTiebreaker(p5, p5) == 0 || readTiebreaker(p5, p5) == 1)) **
[----------------
2289 (unfolding epOwnerN(p1, p1) in
----------------]
2290 unfolding epOwnerF(p1, p1) in
2291 unfolding epOwnerFault(p1, p1) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
2288 (readTiebreaker(p5, p5) == 0 || readTiebreaker(p5, p5) == 1)) **
2289 (unfolding epOwnerN(p1, p1) in
[----------------
2290 unfolding epOwnerF(p1, p1) in
----------------]
2291 unfolding epOwnerFault(p1, p1) in
2292 unfolding epOwnerV(p1, p1) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
2289 (unfolding epOwnerN(p1, p1) in
2290 unfolding epOwnerF(p1, p1) in
[--------------------
2291 unfolding epOwnerFault(p1, p1) in
--------------------]
2292 unfolding epOwnerV(p1, p1) in
2293 unfolding epOwnerV1(p1, p1) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
2290 unfolding epOwnerF(p1, p1) in
2291 unfolding epOwnerFault(p1, p1) in
[----------------
2292 unfolding epOwnerV(p1, p1) in
----------------]
2293 unfolding epOwnerV1(p1, p1) in
2294 unfolding epOwnerV2(p1, p1) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
2291 unfolding epOwnerFault(p1, p1) in
2292 unfolding epOwnerV(p1, p1) in
[-----------------
2293 unfolding epOwnerV1(p1, p1) in
-----------------]
2294 unfolding epOwnerV2(p1, p1) in
2295 unfolding epOwnerV3(p1, p1) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
2292 unfolding epOwnerV(p1, p1) in
2293 unfolding epOwnerV1(p1, p1) in
[-----------------
2294 unfolding epOwnerV2(p1, p1) in
-----------------]
2295 unfolding epOwnerV3(p1, p1) in
2296 unfolding epOwnerV4(p1, p1) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
2293 unfolding epOwnerV1(p1, p1) in
2294 unfolding epOwnerV2(p1, p1) in
[-----------------
2295 unfolding epOwnerV3(p1, p1) in
-----------------]
2296 unfolding epOwnerV4(p1, p1) in
2297 unfolding epOwnerV5(p1, p1) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
2294 unfolding epOwnerV2(p1, p1) in
2295 unfolding epOwnerV3(p1, p1) in
[-----------------
2296 unfolding epOwnerV4(p1, p1) in
-----------------]
2297 unfolding epOwnerV5(p1, p1) in
2298 unfolding epOwnerTiebreaker(p1, p1) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
2295 unfolding epOwnerV3(p1, p1) in
2296 unfolding epOwnerV4(p1, p1) in
[-----------------
2297 unfolding epOwnerV5(p1, p1) in
-----------------]
2298 unfolding epOwnerTiebreaker(p1, p1) in
2299 unfolding epOwnerN(p2, p2) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
2296 unfolding epOwnerV4(p1, p1) in
2297 unfolding epOwnerV5(p1, p1) in
[-------------------------
2298 unfolding epOwnerTiebreaker(p1, p1) in
-------------------------]
2299 unfolding epOwnerN(p2, p2) in
2300 unfolding epOwnerF(p2, p2) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
2297 unfolding epOwnerV5(p1, p1) in
2298 unfolding epOwnerTiebreaker(p1, p1) in
[----------------
2299 unfolding epOwnerN(p2, p2) in
----------------]
2300 unfolding epOwnerF(p2, p2) in
2301 unfolding epOwnerFault(p2, p2) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
2298 unfolding epOwnerTiebreaker(p1, p1) in
2299 unfolding epOwnerN(p2, p2) in
[----------------
2300 unfolding epOwnerF(p2, p2) in
----------------]
2301 unfolding epOwnerFault(p2, p2) in
2302 unfolding epOwnerV(p2, p2) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
2299 unfolding epOwnerN(p2, p2) in
2300 unfolding epOwnerF(p2, p2) in
[--------------------
2301 unfolding epOwnerFault(p2, p2) in
--------------------]
2302 unfolding epOwnerV(p2, p2) in
2303 unfolding epOwnerV1(p2, p2) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
2300 unfolding epOwnerF(p2, p2) in
2301 unfolding epOwnerFault(p2, p2) in
[----------------
2302 unfolding epOwnerV(p2, p2) in
----------------]
2303 unfolding epOwnerV1(p2, p2) in
2304 unfolding epOwnerV2(p2, p2) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
2301 unfolding epOwnerFault(p2, p2) in
2302 unfolding epOwnerV(p2, p2) in
[-----------------
2303 unfolding epOwnerV1(p2, p2) in
-----------------]
2304 unfolding epOwnerV2(p2, p2) in
2305 unfolding epOwnerV3(p2, p2) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
2302 unfolding epOwnerV(p2, p2) in
2303 unfolding epOwnerV1(p2, p2) in
[-----------------
2304 unfolding epOwnerV2(p2, p2) in
-----------------]
2305 unfolding epOwnerV3(p2, p2) in
2306 unfolding epOwnerV4(p2, p2) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
2303 unfolding epOwnerV1(p2, p2) in
2304 unfolding epOwnerV2(p2, p2) in
[-----------------
2305 unfolding epOwnerV3(p2, p2) in
-----------------]
2306 unfolding epOwnerV4(p2, p2) in
2307 unfolding epOwnerV5(p2, p2) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
2304 unfolding epOwnerV2(p2, p2) in
2305 unfolding epOwnerV3(p2, p2) in
[-----------------
2306 unfolding epOwnerV4(p2, p2) in
-----------------]
2307 unfolding epOwnerV5(p2, p2) in
2308 unfolding epOwnerTiebreaker(
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
2305 unfolding epOwnerV3(p2, p2) in
2306 unfolding epOwnerV4(p2, p2) in
[-----------------
2307 unfolding epOwnerV5(p2, p2) in
-----------------]
2308 unfolding epOwnerTiebreaker(
2309 p2,
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
2306 unfolding epOwnerV4(p2, p2) in
2307 unfolding epOwnerV5(p2, p2) in
[------------------
2308 unfolding epOwnerTiebreaker(
2309 p2,
2310 p2
2311 ) in
-----------------------------------------------------------------------------------------]
2312 unfolding epOwnerN(
2313 p3,
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
2310 p2
2311 ) in
[---------
2312 unfolding epOwnerN(
2313 p3,
2314 p3
2315 ) in
---------------------------------------------------------------------------------------------]
2316 unfolding epOwnerF(
2317 p3,
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
2314 p3
2315 ) in
[---------
2316 unfolding epOwnerF(
2317 p3,
2318 p3
2319 ) in
-------------------------------------------------------------------------------------------------]
2320 unfolding epOwnerFault(
2321 p3,
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
2318 p3
2319 ) in
[-------------
2320 unfolding epOwnerFault(
2321 p3,
2322 p3
2323 ) in
-----------------------------------------------------------------------------------------------------]
2324 unfolding epOwnerV(
2325 p3,
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
2322 p3
2323 ) in
[---------
2324 unfolding epOwnerV(
2325 p3,
2326 p3
2327 ) in
---------------------------------------------------------------------------------------------------------]
2328 unfolding epOwnerV1(
2329 p3,
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
2326 p3
2327 ) in
[----------
2328 unfolding epOwnerV1(
2329 p3,
2330 p3
2331 ) in
-------------------------------------------------------------------------------------------------------------]
2332 unfolding epOwnerV2(
2333 p3,
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
2330 p3
2331 ) in
[----------
2332 unfolding epOwnerV2(
2333 p3,
2334 p3
2335 ) in
-----------------------------------------------------------------------------------------------------------------]
2336 unfolding epOwnerV3(
2337 p3,
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
2334 p3
2335 ) in
[----------
2336 unfolding epOwnerV3(
2337 p3,
2338 p3
2339 ) in
---------------------------------------------------------------------------------------------------------------------]
2340 unfolding epOwnerV4(
2341 p3,
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
2338 p3
2339 ) in
[----------
2340 unfolding epOwnerV4(
2341 p3,
2342 p3
2343 ) in
-------------------------------------------------------------------------------------------------------------------------]
2344 unfolding epOwnerV5(
2345 p3,
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
2342 p3
2343 ) in
[----------
2344 unfolding epOwnerV5(
2345 p3,
2346 p3
2347 ) in
-----------------------------------------------------------------------------------------------------------------------------]
2348 unfolding epOwnerTiebreaker(
2349 p3,
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
2346 p3
2347 ) in
[------------------
2348 unfolding epOwnerTiebreaker(
2349 p3,
2350 p3
2351 ) in
---------------------------------------------------------------------------------------------------------------------------------]
2352 unfolding epOwnerN(
2353 p4,
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
2350 p3
2351 ) in
[---------
2352 unfolding epOwnerN(
2353 p4,
2354 p4
2355 ) in
-------------------------------------------------------------------------------------------------------------------------------------]
2356 unfolding epOwnerF(
2357 p4,
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
2354 p4
2355 ) in
[---------
2356 unfolding epOwnerF(
2357 p4,
2358 p4
2359 ) in
-----------------------------------------------------------------------------------------------------------------------------------------]
2360 unfolding epOwnerFault(
2361 p4,
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
2358 p4
2359 ) in
[-------------
2360 unfolding epOwnerFault(
2361 p4,
2362 p4
2363 ) in
---------------------------------------------------------------------------------------------------------------------------------------------]
2364 unfolding epOwnerV(
2365 p4,
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
2362 p4
2363 ) in
[---------
2364 unfolding epOwnerV(
2365 p4,
2366 p4
2367 ) in
-------------------------------------------------------------------------------------------------------------------------------------------------]
2368 unfolding epOwnerV1(
2369 p4,
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
2366 p4
2367 ) in
[----------
2368 unfolding epOwnerV1(
2369 p4,
2370 p4
2371 ) in
-----------------------------------------------------------------------------------------------------------------------------------------------------]
2372 unfolding epOwnerV2(
2373 p4,
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
2370 p4
2371 ) in
[----------
2372 unfolding epOwnerV2(
2373 p4,
2374 p4
2375 ) in
---------------------------------------------------------------------------------------------------------------------------------------------------------]
2376 unfolding epOwnerV3(
2377 p4,
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
2374 p4
2375 ) in
[----------
2376 unfolding epOwnerV3(
2377 p4,
2378 p4
2379 ) in
-------------------------------------------------------------------------------------------------------------------------------------------------------------]
2380 unfolding epOwnerV4(
2381 p4,
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
2378 p4
2379 ) in
[----------
2380 unfolding epOwnerV4(
2381 p4,
2382 p4
2383 ) in
-----------------------------------------------------------------------------------------------------------------------------------------------------------------]
2384 unfolding epOwnerV5(
2385 p4,
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
2382 p4
2383 ) in
[----------
2384 unfolding epOwnerV5(
2385 p4,
2386 p4
2387 ) in
---------------------------------------------------------------------------------------------------------------------------------------------------------------------]
2388 unfolding epOwnerTiebreaker(
2389 p4,
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
2386 p4
2387 ) in
[------------------
2388 unfolding epOwnerTiebreaker(
2389 p4,
2390 p4
2391 ) in
-------------------------------------------------------------------------------------------------------------------------------------------------------------------------]
2392 unfolding epOwnerN(
2393 p5,
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
2390 p4
2391 ) in
[---------
2392 unfolding epOwnerN(
2393 p5,
2394 p5
2395 ) in
-----------------------------------------------------------------------------------------------------------------------------------------------------------------------------]
2396 unfolding epOwnerF(
2397 p5,
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
2394 p5
2395 ) in
[---------
2396 unfolding epOwnerF(
2397 p5,
2398 p5
2399 ) in
---------------------------------------------------------------------------------------------------------------------------------------------------------------------------------]
2400 unfolding epOwnerFault(
2401 p5,
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
2398 p5
2399 ) in
[-------------
2400 unfolding epOwnerFault(
2401 p5,
2402 p5
2403 ) in
-------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------]
2404 unfolding epOwnerV(
2405 p5,
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
2402 p5
2403 ) in
[---------
2404 unfolding epOwnerV(
2405 p5,
2406 p5
2407 ) in
-----------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------]
2408 unfolding epOwnerV1(
2409 p5,
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
2406 p5
2407 ) in
[----------
2408 unfolding epOwnerV1(
2409 p5,
2410 p5
2411 ) in
---------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------]
2412 unfolding epOwnerV2(
2413 p5,
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
2410 p5
2411 ) in
[----------
2412 unfolding epOwnerV2(
2413 p5,
2414 p5
2415 ) in
-------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------]
2416 unfolding epOwnerV3(
2417 p5,
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
2414 p5
2415 ) in
[----------
2416 unfolding epOwnerV3(
2417 p5,
2418 p5
2419 ) in
-----------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------]
2420 unfolding epOwnerV4(
2421 p5,
-------------------------------...
Check failure on line 222 in test/main/vct/test/integration/helper/VeyMontSpec.scala
github-actions / TestReport
vct.test.integration.examples.veymont.TechnicalVeyMontSpec ► Files examples/technical/veymont/checkLTS/ltstest.pvl verifies with silicon
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:Raw output
org.scalatest.exceptions.TestFailedException: Pass did not equal Crash(vct.main.modes.VeyMont$WrapSystemError: The following error occurred during choreography verification:
The encodePermissionStratification rewrite caused the AST to no longer typecheck:
======================================
103 ensures Perm(c.left, write);
104 ensures Perm(epOwnerLeft(c, c), write);
[--------------
105 ensures unfolding epOwnerX(a, a) in
--------------]
106 unfolding epOwnerLeft(a, a) in unfolding epOwnerX(b, b) in unfolding epOwnerLeft(b, b) in a.x == b.x;
107 ensures unfolding epOwnerX(b, b) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
104 ensures Perm(epOwnerLeft(c, c), write);
105 ensures unfolding epOwnerX(a, a) in
[-----------------
106 unfolding epOwnerLeft(a, a) in unfolding epOwnerX(b, b) in unfolding epOwnerLeft(b, b) in a.x == b.x;
-----------------]
107 ensures unfolding epOwnerX(b, b) in
108 unfolding epOwnerLeft(b, b) in unfolding epOwnerX(c, c) in unfolding epOwnerLeft(c, c) in b.x == c.x;
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
104 ensures Perm(epOwnerLeft(c, c), write);
105 ensures unfolding epOwnerX(a, a) in
[--------------
106 unfolding epOwnerLeft(a, a) in unfolding epOwnerX(b, b) in unfolding epOwnerLeft(b, b) in a.x == b.x;
--------------]
107 ensures unfolding epOwnerX(b, b) in
108 unfolding epOwnerLeft(b, b) in unfolding epOwnerX(c, c) in unfolding epOwnerLeft(c, c) in b.x == c.x;
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
104 ensures Perm(epOwnerLeft(c, c), write);
105 ensures unfolding epOwnerX(a, a) in
[-----------------
106 unfolding epOwnerLeft(a, a) in unfolding epOwnerX(b, b) in unfolding epOwnerLeft(b, b) in a.x == b.x;
-----------------]
107 ensures unfolding epOwnerX(b, b) in
108 unfolding epOwnerLeft(b, b) in unfolding epOwnerX(c, c) in unfolding epOwnerLeft(c, c) in b.x == c.x;
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
105 ensures unfolding epOwnerX(a, a) in
106 unfolding epOwnerLeft(a, a) in unfolding epOwnerX(b, b) in unfolding epOwnerLeft(b, b) in a.x == b.x;
[--------------
107 ensures unfolding epOwnerX(b, b) in
--------------]
108 unfolding epOwnerLeft(b, b) in unfolding epOwnerX(c, c) in unfolding epOwnerLeft(c, c) in b.x == c.x;
109 run {
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
106 unfolding epOwnerLeft(a, a) in unfolding epOwnerX(b, b) in unfolding epOwnerLeft(b, b) in a.x == b.x;
107 ensures unfolding epOwnerX(b, b) in
[-----------------
108 unfolding epOwnerLeft(b, b) in unfolding epOwnerX(c, c) in unfolding epOwnerLeft(c, c) in b.x == c.x;
-----------------]
109 run {
110 int intermediate;
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
106 unfolding epOwnerLeft(a, a) in unfolding epOwnerX(b, b) in unfolding epOwnerLeft(b, b) in a.x == b.x;
107 ensures unfolding epOwnerX(b, b) in
[--------------
108 unfolding epOwnerLeft(b, b) in unfolding epOwnerX(c, c) in unfolding epOwnerLeft(c, c) in b.x == c.x;
--------------]
109 run {
110 int intermediate;
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
106 unfolding epOwnerLeft(a, a) in unfolding epOwnerX(b, b) in unfolding epOwnerLeft(b, b) in a.x == b.x;
107 ensures unfolding epOwnerX(b, b) in
[-----------------
108 unfolding epOwnerLeft(b, b) in unfolding epOwnerX(c, c) in unfolding epOwnerLeft(c, c) in b.x == c.x;
-----------------]
109 run {
110 int intermediate;
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
)
Expected test result: pass
Actual test result: crash with message:
The following error occurred during choreography verification:
The encodePermissionStratification rewrite caused the AST to no longer typecheck:
======================================
103 ensures Perm(c.left, write);
104 ensures Perm(epOwnerLeft(c, c), write);
[--------------
105 ensures unfolding epOwnerX(a, a) in
--------------]
106 unfolding epOwnerLeft(a, a) in unfolding epOwnerX(b, b) in unfolding epOwnerLeft(b, b) in a.x == b.x;
107 ensures unfolding epOwnerX(b, b) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
104 ensures Perm(epOwnerLeft(c, c), write);
105 ensures unfolding epOwnerX(a, a) in
[-----------------
106 unfolding epOwnerLeft(a, a) in unfolding epOwnerX(b, b) in unfolding epOwnerLeft(b, b) in a.x == b.x;
-----------------]
107 ensures unfolding epOwnerX(b, b) in
108 unfolding epOwnerLeft(b, b) in unfolding epOwnerX(c, c) in unfolding epOwnerLeft(c, c) in b.x == c.x;
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
104 ensures Perm(epOwnerLeft(c, c), write);
105 ensures unfolding epOwnerX(a, a) in
[--------------
106 unfolding epOwnerLeft(a, a) in unfolding epOwnerX(b, b) in unfolding epOwnerLeft(b, b) in a.x == b.x;
--------------]
107 ensures unfolding epOwnerX(b, b) in
108 unfolding epOwnerLeft(b, b) in unfolding epOwnerX(c, c) in unfolding epOwnerLeft(c, c) in b.x == c.x;
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
104 ensures Perm(epOwnerLeft(c, c), write);
105 ensures unfolding epOwnerX(a, a) in
[-----------------
106 unfolding epOwnerLeft(a, a) in unfolding epOwnerX(b, b) in unfolding epOwnerLeft(b, b) in a.x == b.x;
-----------------]
107 ensures unfolding epOwnerX(b, b) in
108 unfolding epOwnerLeft(b, b) in unfolding epOwnerX(c, c) in unfolding epOwnerLeft(c, c) in b.x == c.x;
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
105 ensures unfolding epOwnerX(a, a) in
106 unfolding epOwnerLeft(a, a) in unfolding epOwnerX(b, b) in unfolding epOwnerLeft(b, b) in a.x == b.x;
[--------------
107 ensures unfolding epOwnerX(b, b) in
--------------]
108 unfolding epOwnerLeft(b, b) in unfolding epOwnerX(c, c) in unfolding epOwnerLeft(c, c) in b.x == c.x;
109 run {
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
106 unfolding epOwnerLeft(a, a) in unfolding epOwnerX(b, b) in unfolding epOwnerLeft(b, b) in a.x == b.x;
107 ensures unfolding epOwnerX(b, b) in
[-----------------
108 unfolding epOwnerLeft(b, b) in unfolding epOwnerX(c, c) in unfolding epOwnerLeft(c, c) in b.x == c.x;
-----------------]
109 run {
110 int intermediate;
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
106 unfolding epOwnerLeft(a, a) in unfolding epOwnerX(b, b) in unfolding epOwnerLeft(b, b) in a.x == b.x;
107 ensures unfolding epOwnerX(b, b) in
[--------------
108 unfolding epOwnerLeft(b, b) in unfolding epOwnerX(c, c) in unfolding epOwnerLeft(c, c) in b.x == c.x;
--------------]
109 run {
110 int intermediate;
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
106 unfolding epOwnerLeft(a, a) in unfolding epOwnerX(b, b) in unfolding epOwnerLeft(b, b) in a.x == b.x;
107 ensures unfolding epOwnerX(b, b) in
[-----------------
108 unfolding epOwnerLeft(b, b) in unfolding epOwnerX(c, c) in unfolding epOwnerLeft(c, c) in b.x == c.x;
-----------------]
109 run {
110 int intermediate;
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
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
github-actions / TestReport
vct.test.integration.examples.veymont.VeyMontExamplesSpec ► Leader elect ring (generated permissions) verifies with silicon
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:Raw output
org.scalatest.exceptions.TestFailedException: Pass did not equal Crash(vct.main.modes.VeyMont$WrapSystemError: The following error occurred during choreography verification:
The encodePermissionStratification rewrite caused the AST to no longer typecheck:
======================================
237 Perm(d.n, write) ** Perm(epOwnerN(d, d), write) **
238 true **
[-----------------
239 (unfolding epOwnerRank(a, a) in
-----------------]
240 unfolding epOwnerMaxVal(a, a) in
241 unfolding epOwnerLeft(a, a) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
238 true **
239 (unfolding epOwnerRank(a, a) in
[-------------------
240 unfolding epOwnerMaxVal(a, a) in
-------------------]
241 unfolding epOwnerLeft(a, a) in
242 unfolding epOwnerN(a, a) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
239 (unfolding epOwnerRank(a, a) in
240 unfolding epOwnerMaxVal(a, a) in
[-----------------
241 unfolding epOwnerLeft(a, a) in
-----------------]
242 unfolding epOwnerN(a, a) in
243 unfolding epOwnerRank(b, b) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
240 unfolding epOwnerMaxVal(a, a) in
241 unfolding epOwnerLeft(a, a) in
[--------------
242 unfolding epOwnerN(a, a) in
--------------]
243 unfolding epOwnerRank(b, b) in
244 unfolding epOwnerMaxVal(b, b) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
241 unfolding epOwnerLeft(a, a) in
242 unfolding epOwnerN(a, a) in
[-----------------
243 unfolding epOwnerRank(b, b) in
-----------------]
244 unfolding epOwnerMaxVal(b, b) in
245 unfolding epOwnerLeft(b, b) in unfolding epOwnerN(b, b) in a.rank != b.rank) **
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
242 unfolding epOwnerN(a, a) in
243 unfolding epOwnerRank(b, b) in
[-------------------
244 unfolding epOwnerMaxVal(b, b) in
-------------------]
245 unfolding epOwnerLeft(b, b) in unfolding epOwnerN(b, b) in a.rank != b.rank) **
246 (unfolding epOwnerRank(a, a) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
243 unfolding epOwnerRank(b, b) in
244 unfolding epOwnerMaxVal(b, b) in
[-----------------
245 unfolding epOwnerLeft(b, b) in unfolding epOwnerN(b, b) in a.rank != b.rank) **
-----------------]
246 (unfolding epOwnerRank(a, a) in
247 unfolding epOwnerMaxVal(a, a) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
243 unfolding epOwnerRank(b, b) in
244 unfolding epOwnerMaxVal(b, b) in
[--------------
245 unfolding epOwnerLeft(b, b) in unfolding epOwnerN(b, b) in a.rank != b.rank) **
--------------]
246 (unfolding epOwnerRank(a, a) in
247 unfolding epOwnerMaxVal(a, a) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
244 unfolding epOwnerMaxVal(b, b) in
245 unfolding epOwnerLeft(b, b) in unfolding epOwnerN(b, b) in a.rank != b.rank) **
[-----------------
246 (unfolding epOwnerRank(a, a) in
-----------------]
247 unfolding epOwnerMaxVal(a, a) in
248 unfolding epOwnerLeft(a, a) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
245 unfolding epOwnerLeft(b, b) in unfolding epOwnerN(b, b) in a.rank != b.rank) **
246 (unfolding epOwnerRank(a, a) in
[-------------------
247 unfolding epOwnerMaxVal(a, a) in
-------------------]
248 unfolding epOwnerLeft(a, a) in
249 unfolding epOwnerN(a, a) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
246 (unfolding epOwnerRank(a, a) in
247 unfolding epOwnerMaxVal(a, a) in
[-----------------
248 unfolding epOwnerLeft(a, a) in
-----------------]
249 unfolding epOwnerN(a, a) in
250 unfolding epOwnerRank(c, c) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
247 unfolding epOwnerMaxVal(a, a) in
248 unfolding epOwnerLeft(a, a) in
[--------------
249 unfolding epOwnerN(a, a) in
--------------]
250 unfolding epOwnerRank(c, c) in
251 unfolding epOwnerMaxVal(c, c) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
248 unfolding epOwnerLeft(a, a) in
249 unfolding epOwnerN(a, a) in
[-----------------
250 unfolding epOwnerRank(c, c) in
-----------------]
251 unfolding epOwnerMaxVal(c, c) in
252 unfolding epOwnerLeft(c, c) in unfolding epOwnerN(c, c) in a.rank != c.rank) **
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
249 unfolding epOwnerN(a, a) in
250 unfolding epOwnerRank(c, c) in
[-------------------
251 unfolding epOwnerMaxVal(c, c) in
-------------------]
252 unfolding epOwnerLeft(c, c) in unfolding epOwnerN(c, c) in a.rank != c.rank) **
253 (unfolding epOwnerRank(a, a) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
250 unfolding epOwnerRank(c, c) in
251 unfolding epOwnerMaxVal(c, c) in
[-----------------
252 unfolding epOwnerLeft(c, c) in unfolding epOwnerN(c, c) in a.rank != c.rank) **
-----------------]
253 (unfolding epOwnerRank(a, a) in
254 unfolding epOwnerMaxVal(a, a) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
250 unfolding epOwnerRank(c, c) in
251 unfolding epOwnerMaxVal(c, c) in
[--------------
252 unfolding epOwnerLeft(c, c) in unfolding epOwnerN(c, c) in a.rank != c.rank) **
--------------]
253 (unfolding epOwnerRank(a, a) in
254 unfolding epOwnerMaxVal(a, a) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
251 unfolding epOwnerMaxVal(c, c) in
252 unfolding epOwnerLeft(c, c) in unfolding epOwnerN(c, c) in a.rank != c.rank) **
[-----------------
253 (unfolding epOwnerRank(a, a) in
-----------------]
254 unfolding epOwnerMaxVal(a, a) in
255 unfolding epOwnerLeft(a, a) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
252 unfolding epOwnerLeft(c, c) in unfolding epOwnerN(c, c) in a.rank != c.rank) **
253 (unfolding epOwnerRank(a, a) in
[-------------------
254 unfolding epOwnerMaxVal(a, a) in
-------------------]
255 unfolding epOwnerLeft(a, a) in
256 unfolding epOwnerN(a, a) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
253 (unfolding epOwnerRank(a, a) in
254 unfolding epOwnerMaxVal(a, a) in
[-----------------
255 unfolding epOwnerLeft(a, a) in
-----------------]
256 unfolding epOwnerN(a, a) in
257 unfolding epOwnerRank(d, d) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
254 unfolding epOwnerMaxVal(a, a) in
255 unfolding epOwnerLeft(a, a) in
[--------------
256 unfolding epOwnerN(a, a) in
--------------]
257 unfolding epOwnerRank(d, d) in
258 unfolding epOwnerMaxVal(d, d) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
255 unfolding epOwnerLeft(a, a) in
256 unfolding epOwnerN(a, a) in
[-----------------
257 unfolding epOwnerRank(d, d) in
-----------------]
258 unfolding epOwnerMaxVal(d, d) in
259 unfolding epOwnerLeft(d, d) in unfolding epOwnerN(d, d) in a.rank != d.rank) **
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
256 unfolding epOwnerN(a, a) in
257 unfolding epOwnerRank(d, d) in
[-------------------
258 unfolding epOwnerMaxVal(d, d) in
-------------------]
259 unfolding epOwnerLeft(d, d) in unfolding epOwnerN(d, d) in a.rank != d.rank) **
260 (unfolding epOwnerRank(b, b) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
257 unfolding epOwnerRank(d, d) in
258 unfolding epOwnerMaxVal(d, d) in
[-----------------
259 unfolding epOwnerLeft(d, d) in unfolding epOwnerN(d, d) in a.rank != d.rank) **
-----------------]
260 (unfolding epOwnerRank(b, b) in
261 unfolding epOwnerMaxVal(b, b) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
257 unfolding epOwnerRank(d, d) in
258 unfolding epOwnerMaxVal(d, d) in
[--------------
259 unfolding epOwnerLeft(d, d) in unfolding epOwnerN(d, d) in a.rank != d.rank) **
--------------]
260 (unfolding epOwnerRank(b, b) in
261 unfolding epOwnerMaxVal(b, b) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
258 unfolding epOwnerMaxVal(d, d) in
259 unfolding epOwnerLeft(d, d) in unfolding epOwnerN(d, d) in a.rank != d.rank) **
[-----------------
260 (unfolding epOwnerRank(b, b) in
-----------------]
261 unfolding epOwnerMaxVal(b, b) in
262 unfolding epOwnerLeft(b, b) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
259 unfolding epOwnerLeft(d, d) in unfolding epOwnerN(d, d) in a.rank != d.rank) **
260 (unfolding epOwnerRank(b, b) in
[-------------------
261 unfolding epOwnerMaxVal(b, b) in
-------------------]
262 unfolding epOwnerLeft(b, b) in
263 unfolding epOwnerN(b, b) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
260 (unfolding epOwnerRank(b, b) in
261 unfolding epOwnerMaxVal(b, b) in
[-----------------
262 unfolding epOwnerLeft(b, b) in
-----------------]
263 unfolding epOwnerN(b, b) in
264 unfolding epOwnerRank(c, c) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
261 unfolding epOwnerMaxVal(b, b) in
262 unfolding epOwnerLeft(b, b) in
[--------------
263 unfolding epOwnerN(b, b) in
--------------]
264 unfolding epOwnerRank(c, c) in
265 unfolding epOwnerMaxVal(c, c) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
262 unfolding epOwnerLeft(b, b) in
263 unfolding epOwnerN(b, b) in
[-----------------
264 unfolding epOwnerRank(c, c) in
-----------------]
265 unfolding epOwnerMaxVal(c, c) in
266 unfolding epOwnerLeft(c, c) in unfolding epOwnerN(c, c) in b.rank != c.rank) **
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
263 unfolding epOwnerN(b, b) in
264 unfolding epOwnerRank(c, c) in
[-------------------
265 unfolding epOwnerMaxVal(c, c) in
-------------------]
266 unfolding epOwnerLeft(c, c) in unfolding epOwnerN(c, c) in b.rank != c.rank) **
267 (unfolding epOwnerRank(b, b) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
264 unfolding epOwnerRank(c, c) in
265 unfolding epOwnerMaxVal(c, c) in
[-----------------
266 unfolding epOwnerLeft(c, c) in unfolding epOwnerN(c, c) in b.rank != c.rank) **
-----------------]
267 (unfolding epOwnerRank(b, b) in
268 unfolding epOwnerMaxVal(b, b) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
264 unfolding epOwnerRank(c, c) in
265 unfolding epOwnerMaxVal(c, c) in
[--------------
266 unfolding epOwnerLeft(c, c) in unfolding epOwnerN(c, c) in b.rank != c.rank) **
--------------]
267 (unfolding epOwnerRank(b, b) in
268 unfolding epOwnerMaxVal(b, b) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
265 unfolding epOwnerMaxVal(c, c) in
266 unfolding epOwnerLeft(c, c) in unfolding epOwnerN(c, c) in b.rank != c.rank) **
[-----------------
267 (unfolding epOwnerRank(b, b) in
-----------------]
268 unfolding epOwnerMaxVal(b, b) in
269 unfolding epOwnerLeft(b, b) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
266 unfolding epOwnerLeft(c, c) in unfolding epOwnerN(c, c) in b.rank != c.rank) **
267 (unfolding epOwnerRank(b, b) in
[-------------------
268 unfolding epOwnerMaxVal(b, b) in
-------------------]
269 unfolding epOwnerLeft(b, b) in
270 unfolding epOwnerN(b, b) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
267 (unfolding epOwnerRank(b, b) in
268 unfolding epOwnerMaxVal(b, b) in
[-----------------
269 unfolding epOwnerLeft(b, b) in
-----------------]
270 unfolding epOwnerN(b, b) in
271 unfolding epOwnerRank(d, d) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
268 unfolding epOwnerMaxVal(b, b) in
269 unfolding epOwnerLeft(b, b) in
[--------------
270 unfolding epOwnerN(b, b) in
--------------]
271 unfolding epOwnerRank(d, d) in
272 unfolding epOwnerMaxVal(d, d) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
269 unfolding epOwnerLeft(b, b) in
270 unfolding epOwnerN(b, b) in
[-----------------
271 unfolding epOwnerRank(d, d) in
-----------------]
272 unfolding epOwnerMaxVal(d, d) in
273 unfolding epOwnerLeft(d, d) in unfolding epOwnerN(d, d) in b.rank != d.rank) **
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
270 unfolding epOwnerN(b, b) in
271 unfolding epOwnerRank(d, d) in
[-------------------
272 unfolding epOwnerMaxVal(d, d) in
-------------------]
273 unfolding epOwnerLeft(d, d) in unfolding epOwnerN(d, d) in b.rank != d.rank) **
274 (unfolding epOwnerRank(c, c) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
271 unfolding epOwnerRank(d, d) in
272 unfolding epOwnerMaxVal(d, d) in
[-----------------
273 unfolding epOwnerLeft(d, d) in unfolding epOwnerN(d, d) in b.rank != d.rank) **
-----------------]
274 (unfolding epOwnerRank(c, c) in
275 unfolding epOwnerMaxVal(c, c) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
271 unfolding epOwnerRank(d, d) in
272 unfolding epOwnerMaxVal(d, d) in
[--------------
273 unfolding epOwnerLeft(d, d) in unfolding epOwnerN(d, d) in b.rank != d.rank) **
--------------]
274 (unfolding epOwnerRank(c, c) in
275 unfolding epOwnerMaxVal(c, c) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
272 unfolding epOwnerMaxVal(d, d) in
273 unfolding epOwnerLeft(d, d) in unfolding epOwnerN(d, d) in b.rank != d.rank) **
[-----------------
274 (unfolding epOwnerRank(c, c) in
-----------------]
275 unfolding epOwnerMaxVal(c, c) in
276 unfolding epOwnerLeft(c, c) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
273 unfolding epOwnerLeft(d, d) in unfolding epOwnerN(d, d) in b.rank != d.rank) **
274 (unfolding epOwnerRank(c, c) in
[-------------------
275 unfolding epOwnerMaxVal(c, c) in
-------------------]
276 unfolding epOwnerLeft(c, c) in
277 unfolding epOwnerN(c, c) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
274 (unfolding epOwnerRank(c, c) in
275 unfolding epOwnerMaxVal(c, c) in
[-----------------
276 unfolding epOwnerLeft(c, c) in
-----------------]
277 unfolding epOwnerN(c, c) in
278 unfolding epOwnerRank(d, d) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
275 unfolding epOwnerMaxVal(c, c) in
276 unfolding epOwnerLeft(c, c) in
[--------------
277 unfolding epOwnerN(c, c) in
--------------]
278 unfolding epOwnerRank(d, d) in
279 unfolding epOwnerMaxVal(d, d) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
276 unfolding epOwnerLeft(c, c) in
277 unfolding epOwnerN(c, c) in
[-----------------
278 unfolding epOwnerRank(d, d) in
-----------------]
279 unfolding epOwnerMaxVal(d, d) in
280 unfolding epOwnerLeft(d, d) in unfolding epOwnerN(d, d) in c.rank != d.rank) **
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
277 unfolding epOwnerN(c, c) in
278 unfolding epOwnerRank(d, d) in
[-------------------
279 unfolding epOwnerMaxVal(d, d) in
-------------------]
280 unfolding epOwnerLeft(d, d) in unfolding epOwnerN(d, d) in c.rank != d.rank) **
281 readN(c, c) == 0 **
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
278 unfolding epOwnerRank(d, d) in
279 unfolding epOwnerMaxVal(d, d) in
[-----------------
280 unfolding epOwnerLeft(d, d) in unfolding epOwnerN(d, d) in c.rank != d.rank) **
-----------------]
281 readN(c, c) == 0 **
282 (unfolding epOwnerRank(a, a) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
278 unfolding epOwnerRank(d, d) in
279 unfolding epOwnerMaxVal(d, d) in
[--------------
280 unfolding epOwnerLeft(d, d) in unfolding epOwnerN(d, d) in c.rank != d.rank) **
--------------]
281 readN(c, c) == 0 **
282 (unfolding epOwnerRank(a, a) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
280 unfolding epOwnerLeft(d, d) in unfolding epOwnerN(d, d) in c.rank != d.rank) **
281 readN(c, c) == 0 **
[-----------------
282 (unfolding epOwnerRank(a, a) in
-----------------]
283 unfolding epOwnerMaxVal(a, a) in
284 unfolding epOwnerLeft(a, a) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
281 readN(c, c) == 0 **
282 (unfolding epOwnerRank(a, a) in
[-------------------
283 unfolding epOwnerMaxVal(a, a) in
-------------------]
284 unfolding epOwnerLeft(a, a) in
285 unfolding epOwnerN(a, a) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
282 (unfolding epOwnerRank(a, a) in
283 unfolding epOwnerMaxVal(a, a) in
[-----------------
284 unfolding epOwnerLeft(a, a) in
-----------------]
285 unfolding epOwnerN(a, a) in
286 unfolding epOwnerRank(c, c) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
283 unfolding epOwnerMaxVal(a, a) in
284 unfolding epOwnerLeft(a, a) in
[--------------
285 unfolding epOwnerN(a, a) in
--------------]
286 unfolding epOwnerRank(c, c) in
287 unfolding epOwnerMaxVal(c, c) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
284 unfolding epOwnerLeft(a, a) in
285 unfolding epOwnerN(a, a) in
[-----------------
286 unfolding epOwnerRank(c, c) in
-----------------]
287 unfolding epOwnerMaxVal(c, c) in
288 unfolding epOwnerLeft(c, c) in unfolding epOwnerN(c, c) in a.n == c.n) **
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
285 unfolding epOwnerN(a, a) in
286 unfolding epOwnerRank(c, c) in
[-------------------
287 unfolding epOwnerMaxVal(c, c) in
-------------------]
288 unfolding epOwnerLeft(c, c) in unfolding epOwnerN(c, c) in a.n == c.n) **
289 (unfolding epOwnerRank(b, b) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
286 unfolding epOwnerRank(c, c) in
287 unfolding epOwnerMaxVal(c, c) in
[-----------------
288 unfolding epOwnerLeft(c, c) in unfolding epOwnerN(c, c) in a.n == c.n) **
-----------------]
289 (unfolding epOwnerRank(b, b) in
290 unfolding epOwnerMaxVal(b, b) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
286 unfolding epOwnerRank(c, c) in
287 unfolding epOwnerMaxVal(c, c) in
[--------------
288 unfolding epOwnerLeft(c, c) in unfolding epOwnerN(c, c) in a.n == c.n) **
--------------]
289 (unfolding epOwnerRank(b, b) in
290 unfolding epOwnerMaxVal(b, b) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
287 unfolding epOwnerMaxVal(c, c) in
288 unfolding epOwnerLeft(c, c) in unfolding epOwnerN(c, c) in a.n == c.n) **
[-----------------
289 (unfolding epOwnerRank(b, b) in
-----------------]
290 unfolding epOwnerMaxVal(b, b) in
291 unfolding epOwnerLeft(b, b) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
288 unfolding epOwnerLeft(c, c) in unfolding epOwnerN(c, c) in a.n == c.n) **
289 (unfolding epOwnerRank(b, b) in
[-------------------
290 unfolding epOwnerMaxVal(b, b) in
-------------------]
291 unfolding epOwnerLeft(b, b) in
292 unfolding epOwnerN(b, b) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
289 (unfolding epOwnerRank(b, b) in
290 unfolding epOwnerMaxVal(b, b) in
[-----------------
291 unfolding epOwnerLeft(b, b) in
-----------------]
292 unfolding epOwnerN(b, b) in
293 unfolding epOwnerRank(c, c) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
290 unfolding epOwnerMaxVal(b, b) in
291 unfolding epOwnerLeft(b, b) in
[--------------
292 unfolding epOwnerN(b, b) in
--------------]
293 unfolding epOwnerRank(c, c) in
294 unfolding epOwnerMaxVal(c, c) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
291 unfolding epOwnerLeft(b, b) in
292 unfolding epOwnerN(b, b) in
[-----------------
293 unfolding epOwnerRank(c, c) in
-----------------]
294 unfolding epOwnerMaxVal(c, c) in
295 unfolding epOwnerLeft(c, c) in unfolding epOwnerN(c, c) in b.n == c.n) **
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
292 unfolding epOwnerN(b, b) in
293 unfolding epOwnerRank(c, c) in
[-------------------
294 unfolding epOwnerMaxVal(c, c) in
-------------------]
295 unfolding epOwnerLeft(c, c) in unfolding epOwnerN(c, c) in b.n == c.n) **
296 (unfolding epOwnerRank(d, d) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
293 unfolding epOwnerRank(c, c) in
294 unfolding epOwnerMaxVal(c, c) in
[-----------------
295 unfolding epOwnerLeft(c, c) in unfolding epOwnerN(c, c) in b.n == c.n) **
-----------------]
296 (unfolding epOwnerRank(d, d) in
297 unfolding epOwnerMaxVal(d, d) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
293 unfolding epOwnerRank(c, c) in
294 unfolding epOwnerMaxVal(c, c) in
[--------------
295 unfolding epOwnerLeft(c, c) in unfolding epOwnerN(c, c) in b.n == c.n) **
--------------]
296 (unfolding epOwnerRank(d, d) in
297 unfolding epOwnerMaxVal(d, d) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
294 unfolding epOwnerMaxVal(c, c) in
295 unfolding epOwnerLeft(c, c) in unfolding epOwnerN(c, c) in b.n == c.n) **
[-----------------
296 (unfolding epOwnerRank(d, d) in
-----------------]
297 unfolding epOwnerMaxVal(d, d) in
298 unfolding epOwnerLeft(d, d) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
295 unfolding epOwnerLeft(c, c) in unfolding epOwnerN(c, c) in b.n == c.n) **
296 (unfolding epOwnerRank(d, d) in
[-------------------
297 unfolding epOwnerMaxVal(d, d) in
-------------------]
298 unfolding epOwnerLeft(d, d) in
299 unfolding epOwnerN(d, d) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
296 (unfolding epOwnerRank(d, d) in
297 unfolding epOwnerMaxVal(d, d) in
[-----------------
298 unfolding epOwnerLeft(d, d) in
-----------------]
299 unfolding epOwnerN(d, d) in
300 unfolding epOwnerRank(c, c) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
297 unfolding epOwnerMaxVal(d, d) in
298 unfolding epOwnerLeft(d, d) in
[--------------
299 unfolding epOwnerN(d, d) in
--------------]
300 unfolding epOwnerRank(c, c) in
301 unfolding epOwnerMaxVal(c, c) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
298 unfolding epOwnerLeft(d, d) in
299 unfolding epOwnerN(d, d) in
[-----------------
300 unfolding epOwnerRank(c, c) in
-----------------]
301 unfolding epOwnerMaxVal(c, c) in
302 unfolding epOwnerLeft(c, c) in unfolding epOwnerN(c, c) in d.n == c.n) **
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
299 unfolding epOwnerN(d, d) in
300 unfolding epOwnerRank(c, c) in
[-------------------
301 unfolding epOwnerMaxVal(c, c) in
-------------------]
302 unfolding epOwnerLeft(c, c) in unfolding epOwnerN(c, c) in d.n == c.n) **
303 readMaxVal(a, a) == readRank(a, a) **
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
300 unfolding epOwnerRank(c, c) in
301 unfolding epOwnerMaxVal(c, c) in
[-----------------
302 unfolding epOwnerLeft(c, c) in unfolding epOwnerN(c, c) in d.n == c.n) **
-----------------]
303 readMaxVal(a, a) == readRank(a, a) **
304 readMaxVal(b, b) == readRank(b, b) **
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
300 unfolding epOwnerRank(c, c) in
301 unfolding epOwnerMaxVal(c, c) in
[--------------
302 unfolding epOwnerLeft(c, c) in unfolding epOwnerN(c, c) in d.n == c.n) **
--------------]
303 readMaxVal(a, a) == readRank(a, a) **
304 readMaxVal(b, b) == readRank(b, b) **
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
606 loop_invariant readRank(c, c) == \old(readRank(c, c));
607 loop_invariant readRank(d, d) == \old(readRank(d, d));
[-----------------
608 loop_invariant unfolding epOwnerRank(a, a) in
-----------------]
609 unfolding epOwnerMaxVal(a, a) in
610 unfolding epOwnerLeft(a, a) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
607 loop_invariant readRank(d, d) == \old(readRank(d, d));
608 loop_invariant unfolding epOwnerRank(a, a) in
[-------------------
609 unfolding epOwnerMaxVal(a, a) in
-------------------]
610 unfolding epOwnerLeft(a, a) in
611 unfolding epOwnerN(a, a) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
608 loop_invariant unfolding epOwnerRank(a, a) in
609 unfolding epOwnerMaxVal(a, a) in
[-----------------
610 unfolding epOwnerLeft(a, a) in
-----------------]
611 unfolding epOwnerN(a, a) in
612 unfolding epOwnerRank(b, b) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
609 unfolding epOwnerMaxVal(a, a) in
610 unfolding epOwnerLeft(a, a) in
[--------------
611 unfolding epOwnerN(a, a) in
--------------]
612 unfolding epOwnerRank(b, b) in
613 unfolding epOwnerMaxVal(b, b) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
610 unfolding epOwnerLeft(a, a) in
611 unfolding epOwnerN(a, a) in
[-----------------
612 unfolding epOwnerRank(b, b) in
-----------------]
613 unfolding epOwnerMaxVal(b, b) in
614 unfolding epOwnerLeft(b, b) in unfolding epOwnerN(b, b) in a.rank != b.rank;
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
611 unfolding epOwnerN(a, a) in
612 unfolding epOwnerRank(b, b) in
[-------------------
613 unfolding epOwnerMaxVal(b, b) in
-------------------]
614 unfolding epOwnerLeft(b, b) in unfolding epOwnerN(b, b) in a.rank != b.rank;
615 loop_invariant unfolding epOwnerRank(a, a) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
612 unfolding epOwnerRank(b, b) in
613 unfolding epOwnerMaxVal(b, b) in
[-----------------
614 unfolding epOwnerLeft(b, b) in unfolding epOwnerN(b, b) in a.rank != b.rank;
-----------------]
615 loop_invariant unfolding epOwnerRank(a, a) in
616 unfolding epOwnerMaxVal(a, a) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
612 unfolding epOwnerRank(b, b) in
613 unfolding epOwnerMaxVal(b, b) in
[--------------
614 unfolding epOwnerLeft(b, b) in unfolding epOwnerN(b, b) in a.rank != b.rank;
--------------]
615 loop_invariant unfolding epOwnerRank(a, a) in
616 unfolding epOwnerMaxVal(a, a) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
613 unfolding epOwnerMaxVal(b, b) in
614 unfolding epOwnerLeft(b, b) in unfolding epOwnerN(b, b) in a.rank != b.rank;
[-----------------
615 loop_invariant unfolding epOwnerRank(a, a) in
-----------------]
616 unfolding epOwnerMaxVal(a, a) in
617 unfolding epOwnerLeft(a, a) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
614 unfolding epOwnerLeft(b, b) in unfolding epOwnerN(b, b) in a.rank != b.rank;
615 loop_invariant unfolding epOwnerRank(a, a) in
[-------------------
616 unfolding epOwnerMaxVal(a, a) in
-------------------]
617 unfolding epOwnerLeft(a, a) in
618 unfolding epOwnerN(a, a) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
615 loop_invariant unfolding epOwnerRank(a, a) in
616 unfolding epOwnerMaxVal(a, a) in
[-----------------
617 unfolding epOwnerLeft(a, a) in
-----------------]
618 unfolding epOwnerN(a, a) in
619 unfolding epOwnerRank(c, c) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
616 unfolding epOwnerMaxVal(a, a) in
617 unfolding epOwnerLeft(a, a) in
[--------------
618 unfolding epOwnerN(a, a) in
--------------]
619 unfolding epOwnerRank(c, c) in
620 unfolding epOwnerMaxVal(c, c) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
617 unfolding epOwnerLeft(a, a) in
618 unfolding epOwnerN(a, a) in
[-----------------
619 unfolding epOwnerRank(c, c) in
-----------------]
620 unfolding epOwnerMaxVal(c, c) in
621 unfolding epOwnerLeft(c, c) in unfolding epOwnerN(c, c) in a.rank != c.rank;
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
618 unfolding epOwnerN(a, a) in
619 unfolding epOwnerRank(c, c) in
[-------------------
620 unfolding epOwnerMaxVal(c, c) in
-------------------]
621 unfolding epOwnerLeft(c, c) in unfolding epOwnerN(c, c) in a.rank != c.rank;
622 loop_invariant unfolding epOwnerRank(a, a) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
619 unfolding epOwnerRank(c, c) in
620 unfolding epOwnerMaxVal(c, c) in
[-----------------
621 unfolding epOwnerLeft(c, c) in unfolding epOwnerN(c, c) in a.rank != c.rank;
-----------------]
622 loop_invariant unfolding epOwnerRank(a, a) in
623 unfolding epOwnerMaxVal(a, a) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
619 unfolding epOwnerRank(c, c) in
620 unfolding epOwnerMaxVal(c, c) in
[--------------
621 unfolding epOwnerLeft(c, c) in unfolding epOwnerN(c, c) in a.rank != c.rank;
--------------]
622 loop_invariant unfolding epOwnerRank(a, a) in
623 unfolding epOwnerMaxVal(a, a) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
620 unfolding epOwnerMaxVal(c, c) in
621 unfolding epOwnerLeft(c, c) in unfolding epOwnerN(c, c) in a.rank != c.rank;
[-----------------
622 loop_invariant unfolding epOwnerRank(a, a) in
-----------------]
623 unfolding epOwnerMaxVal(a, a) in
624 unfolding epOwnerLeft(a, a) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
621 unfolding epOwnerLeft(c, c) in unfolding epOwnerN(c, c) in a.rank != c.rank;
622 loop_invariant unfolding epOwnerRank(a, a) in
[-------------------
623 unfolding epOwnerMaxVal(a, a) in
-------------------]
624 unfolding epOwnerLeft(a, a) in
625 unfolding epOwnerN(a, a) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
622 loop_invariant unfolding epOwnerRank(a, a) in
623 unfolding epOwnerMaxVal(a, a) in
[-----------------
624 unfolding epOwnerLeft(a, a) in
-----------------]
625 unfolding epOwnerN(a, a) in
626 unfolding epOwnerRank(d, d) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
623 unfolding epOwnerMaxVal(a, a) in
624 unfolding epOwnerLeft(a, a) in
[--------------
625 unfolding epOwnerN(a, a) in
--------------]
626 unfolding epOwnerRank(d, d) in
627 unfolding epOwnerMaxVal(d, d) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
624 unfolding epOwnerLeft(a, a) in
625 unfolding epOwnerN(a, a) in
[-----------------
626 unfolding epOwnerRank(d, d) in
-----------------]
627 unfolding epOwnerMaxVal(d, d) in
628 unfolding epOwnerLeft(d, d) in unfolding epOwnerN(d, d) in a.rank != d.rank;
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
625 unfolding epOwnerN(a, a) in
626 unfolding epOwnerRank(d, d) in
[-------------------
627 unfolding epOwnerMaxVal(d, d) in
-------------------]
628 unfolding epOwnerLeft(d, d) in unfolding epOwnerN(d, d) in a.rank != d.rank;
629 loop_invariant unfolding epOwnerRank(b, b) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
626 unfolding epOwnerRank(d, d) in
627 unfolding epOwnerMaxVal(d, d) in
[-----------------
628 unfolding epOwnerLeft(d, d) in unfolding epOwnerN(d, d) in a.rank != d.rank;
-----------------]
629 loop_invariant unfolding epOwnerRank(b, b) in
630 unfolding epOwnerMaxVal(b, b) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
626 unfolding epOwnerRank(d, d) in
627 unfolding epOwnerMaxVal(d, d) in
[--------------
628 unfolding epOwnerLeft(d, d) in unfolding epOwnerN(d, d) in a.rank != d.rank;
--------------]
629 loop_invariant unfolding epOwnerRank(b, b) in
630 unfolding epOwnerMaxVal(b, b) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
627 unfolding epOwnerMaxVal(d, d) in
628 unfolding epOwnerLeft(d, d) in unfolding epOwnerN(d, d) in a.rank != d.rank;
[-----------------
629 loop_invariant unfolding epOwnerRank(b, b) in
-----------------]
630 unfolding epOwnerMaxVal(b, b) in
631 unfolding epOwnerLeft(b, b) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
628 unfolding epOwnerLeft(d, d) in unfolding epOwnerN(d, d) in a.rank != d.rank;
629 loop_invariant unfolding epOwnerRank(b, b) in
[-------------------
630 unfolding epOwnerMaxVal(b, b) in
-------------------]
631 unfolding epOwnerLeft(b, b) in
632 unfolding epOwnerN(b, b) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
629 loop_invariant unfolding epOwnerRank(b, b) in
630 unfolding epOwnerMaxVal(b, b) in
[-----------------
631 ...
Check failure on line 222 in test/main/vct/test/integration/helper/VeyMontSpec.scala
github-actions / TestReport
vct.test.integration.examples.veymont.VeyMontExamplesSpec ► Parallel while (generated permissions) verifies with silicon
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:Raw output
org.scalatest.exceptions.TestFailedException: Pass did not equal Crash(vct.main.modes.VeyMont$WrapSystemError: The following error occurred during choreography verification:
The encodePermissionStratification rewrite caused the AST to no longer typecheck:
======================================
49 Perm(c.left, write) ** Perm(epOwnerLeft(c, c), write) **
50 true **
[--------------
51 (unfolding epOwnerX(b, b) in
--------------]
52 unfolding epOwnerLeft(b, b) in
53 unfolding epOwnerX(c, c) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
50 true **
51 (unfolding epOwnerX(b, b) in
[-----------------
52 unfolding epOwnerLeft(b, b) in
-----------------]
53 unfolding epOwnerX(c, c) in
54 unfolding epOwnerLeft(c, c) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
51 (unfolding epOwnerX(b, b) in
52 unfolding epOwnerLeft(b, b) in
[--------------
53 unfolding epOwnerX(c, c) in
--------------]
54 unfolding epOwnerLeft(c, c) in
55 unfolding epOwnerX(a, a) in unfolding epOwnerLeft(a, a) in b.x - c.x == c.x - a.x);
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
52 unfolding epOwnerLeft(b, b) in
53 unfolding epOwnerX(c, c) in
[-----------------
54 unfolding epOwnerLeft(c, c) in
-----------------]
55 unfolding epOwnerX(a, a) in unfolding epOwnerLeft(a, a) in b.x - c.x == c.x - a.x);
56 }
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
53 unfolding epOwnerX(c, c) in
54 unfolding epOwnerLeft(c, c) in
[--------------
55 unfolding epOwnerX(a, a) in unfolding epOwnerLeft(a, a) in b.x - c.x == c.x - a.x);
--------------]
56 }
57
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
53 unfolding epOwnerX(c, c) in
54 unfolding epOwnerLeft(c, c) in
[-----------------
55 unfolding epOwnerX(a, a) in unfolding epOwnerLeft(a, a) in b.x - c.x == c.x - a.x);
-----------------]
56 }
57
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
150 loop_invariant Perm(c.left, write);
151 loop_invariant Perm(epOwnerLeft(c, c), write);
[--------------
152 loop_invariant unfolding epOwnerX(b, b) in
--------------]
153 unfolding epOwnerLeft(b, b) in
154 unfolding epOwnerX(c, c) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
151 loop_invariant Perm(epOwnerLeft(c, c), write);
152 loop_invariant unfolding epOwnerX(b, b) in
[-----------------
153 unfolding epOwnerLeft(b, b) in
-----------------]
154 unfolding epOwnerX(c, c) in
155 unfolding epOwnerLeft(c, c) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
152 loop_invariant unfolding epOwnerX(b, b) in
153 unfolding epOwnerLeft(b, b) in
[--------------
154 unfolding epOwnerX(c, c) in
--------------]
155 unfolding epOwnerLeft(c, c) in
156 unfolding epOwnerX(a, a) in unfolding epOwnerLeft(a, a) in b.x - c.x == c.x - a.x;
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
153 unfolding epOwnerLeft(b, b) in
154 unfolding epOwnerX(c, c) in
[-----------------
155 unfolding epOwnerLeft(c, c) in
-----------------]
156 unfolding epOwnerX(a, a) in unfolding epOwnerLeft(a, a) in b.x - c.x == c.x - a.x;
157 loop_invariant unfolding epOwnerX(b, b) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
154 unfolding epOwnerX(c, c) in
155 unfolding epOwnerLeft(c, c) in
[--------------
156 unfolding epOwnerX(a, a) in unfolding epOwnerLeft(a, a) in b.x - c.x == c.x - a.x;
--------------]
157 loop_invariant unfolding epOwnerX(b, b) in
158 unfolding epOwnerLeft(b, b) in unfolding epOwnerX(a, a) in unfolding epOwnerLeft(a, a) in b.left == a.x;
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
154 unfolding epOwnerX(c, c) in
155 unfolding epOwnerLeft(c, c) in
[-----------------
156 unfolding epOwnerX(a, a) in unfolding epOwnerLeft(a, a) in b.x - c.x == c.x - a.x;
-----------------]
157 loop_invariant unfolding epOwnerX(b, b) in
158 unfolding epOwnerLeft(b, b) in unfolding epOwnerX(a, a) in unfolding epOwnerLeft(a, a) in b.left == a.x;
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
155 unfolding epOwnerLeft(c, c) in
156 unfolding epOwnerX(a, a) in unfolding epOwnerLeft(a, a) in b.x - c.x == c.x - a.x;
[--------------
157 loop_invariant unfolding epOwnerX(b, b) in
--------------]
158 unfolding epOwnerLeft(b, b) in unfolding epOwnerX(a, a) in unfolding epOwnerLeft(a, a) in b.left == a.x;
159 loop_invariant unfolding epOwnerX(c, c) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
156 unfolding epOwnerX(a, a) in unfolding epOwnerLeft(a, a) in b.x - c.x == c.x - a.x;
157 loop_invariant unfolding epOwnerX(b, b) in
[-----------------
158 unfolding epOwnerLeft(b, b) in unfolding epOwnerX(a, a) in unfolding epOwnerLeft(a, a) in b.left == a.x;
-----------------]
159 loop_invariant unfolding epOwnerX(c, c) in
160 unfolding epOwnerLeft(c, c) in unfolding epOwnerX(b, b) in unfolding epOwnerLeft(b, b) in c.left == b.x;
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
156 unfolding epOwnerX(a, a) in unfolding epOwnerLeft(a, a) in b.x - c.x == c.x - a.x;
157 loop_invariant unfolding epOwnerX(b, b) in
[--------------
158 unfolding epOwnerLeft(b, b) in unfolding epOwnerX(a, a) in unfolding epOwnerLeft(a, a) in b.left == a.x;
--------------]
159 loop_invariant unfolding epOwnerX(c, c) in
160 unfolding epOwnerLeft(c, c) in unfolding epOwnerX(b, b) in unfolding epOwnerLeft(b, b) in c.left == b.x;
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
156 unfolding epOwnerX(a, a) in unfolding epOwnerLeft(a, a) in b.x - c.x == c.x - a.x;
157 loop_invariant unfolding epOwnerX(b, b) in
[-----------------
158 unfolding epOwnerLeft(b, b) in unfolding epOwnerX(a, a) in unfolding epOwnerLeft(a, a) in b.left == a.x;
-----------------]
159 loop_invariant unfolding epOwnerX(c, c) in
160 unfolding epOwnerLeft(c, c) in unfolding epOwnerX(b, b) in unfolding epOwnerLeft(b, b) in c.left == b.x;
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
157 loop_invariant unfolding epOwnerX(b, b) in
158 unfolding epOwnerLeft(b, b) in unfolding epOwnerX(a, a) in unfolding epOwnerLeft(a, a) in b.left == a.x;
[--------------
159 loop_invariant unfolding epOwnerX(c, c) in
--------------]
160 unfolding epOwnerLeft(c, c) in unfolding epOwnerX(b, b) in unfolding epOwnerLeft(b, b) in c.left == b.x;
161 loop_invariant unfolding epOwnerX(a, a) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
158 unfolding epOwnerLeft(b, b) in unfolding epOwnerX(a, a) in unfolding epOwnerLeft(a, a) in b.left == a.x;
159 loop_invariant unfolding epOwnerX(c, c) in
[-----------------
160 unfolding epOwnerLeft(c, c) in unfolding epOwnerX(b, b) in unfolding epOwnerLeft(b, b) in c.left == b.x;
-----------------]
161 loop_invariant unfolding epOwnerX(a, a) in
162 unfolding epOwnerLeft(a, a) in unfolding epOwnerX(c, c) in unfolding epOwnerLeft(c, c) in a.left == c.x;
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
158 unfolding epOwnerLeft(b, b) in unfolding epOwnerX(a, a) in unfolding epOwnerLeft(a, a) in b.left == a.x;
159 loop_invariant unfolding epOwnerX(c, c) in
[--------------
160 unfolding epOwnerLeft(c, c) in unfolding epOwnerX(b, b) in unfolding epOwnerLeft(b, b) in c.left == b.x;
--------------]
161 loop_invariant unfolding epOwnerX(a, a) in
162 unfolding epOwnerLeft(a, a) in unfolding epOwnerX(c, c) in unfolding epOwnerLeft(c, c) in a.left == c.x;
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
158 unfolding epOwnerLeft(b, b) in unfolding epOwnerX(a, a) in unfolding epOwnerLeft(a, a) in b.left == a.x;
159 loop_invariant unfolding epOwnerX(c, c) in
[-----------------
160 unfolding epOwnerLeft(c, c) in unfolding epOwnerX(b, b) in unfolding epOwnerLeft(b, b) in c.left == b.x;
-----------------]
161 loop_invariant unfolding epOwnerX(a, a) in
162 unfolding epOwnerLeft(a, a) in unfolding epOwnerX(c, c) in unfolding epOwnerLeft(c, c) in a.left == c.x;
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
159 loop_invariant unfolding epOwnerX(c, c) in
160 unfolding epOwnerLeft(c, c) in unfolding epOwnerX(b, b) in unfolding epOwnerLeft(b, b) in c.left == b.x;
[--------------
161 loop_invariant unfolding epOwnerX(a, a) in
--------------]
162 unfolding epOwnerLeft(a, a) in unfolding epOwnerX(c, c) in unfolding epOwnerLeft(c, c) in a.left == c.x;
163 loop_invariant readLeft(a, a) != readX(a, a) == readLeft(b, b) != readX(b, b);
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
160 unfolding epOwnerLeft(c, c) in unfolding epOwnerX(b, b) in unfolding epOwnerLeft(b, b) in c.left == b.x;
161 loop_invariant unfolding epOwnerX(a, a) in
[-----------------
162 unfolding epOwnerLeft(a, a) in unfolding epOwnerX(c, c) in unfolding epOwnerLeft(c, c) in a.left == c.x;
-----------------]
163 loop_invariant readLeft(a, a) != readX(a, a) == readLeft(b, b) != readX(b, b);
164 loop_invariant readLeft(b, b) != readX(b, b) == readLeft(c, c) != readX(c, c);
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
160 unfolding epOwnerLeft(c, c) in unfolding epOwnerX(b, b) in unfolding epOwnerLeft(b, b) in c.left == b.x;
161 loop_invariant unfolding epOwnerX(a, a) in
[--------------
162 unfolding epOwnerLeft(a, a) in unfolding epOwnerX(c, c) in unfolding epOwnerLeft(c, c) in a.left == c.x;
--------------]
163 loop_invariant readLeft(a, a) != readX(a, a) == readLeft(b, b) != readX(b, b);
164 loop_invariant readLeft(b, b) != readX(b, b) == readLeft(c, c) != readX(c, c);
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
160 unfolding epOwnerLeft(c, c) in unfolding epOwnerX(b, b) in unfolding epOwnerLeft(b, b) in c.left == b.x;
161 loop_invariant unfolding epOwnerX(a, a) in
[-----------------
162 unfolding epOwnerLeft(a, a) in unfolding epOwnerX(c, c) in unfolding epOwnerLeft(c, c) in a.left == c.x;
-----------------]
163 loop_invariant readLeft(a, a) != readX(a, a) == readLeft(b, b) != readX(b, b);
164 loop_invariant readLeft(b, b) != readX(b, b) == readLeft(c, c) != readX(c, c);
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
74 requires Perm(c.left, write);
75 requires Perm(epOwnerLeft(c, c), write);
[--------------
76 requires unfolding epOwnerX(b, b) in
--------------]
77 unfolding epOwnerLeft(b, b) in
78 unfolding epOwnerX(c, c) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
75 requires Perm(epOwnerLeft(c, c), write);
76 requires unfolding epOwnerX(b, b) in
[-----------------
77 unfolding epOwnerLeft(b, b) in
-----------------]
78 unfolding epOwnerX(c, c) in
79 unfolding epOwnerLeft(c, c) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
76 requires unfolding epOwnerX(b, b) in
77 unfolding epOwnerLeft(b, b) in
[--------------
78 unfolding epOwnerX(c, c) in
--------------]
79 unfolding epOwnerLeft(c, c) in
80 unfolding epOwnerX(a, a) in unfolding epOwnerLeft(a, a) in b.x - c.x == c.x - a.x;
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
77 unfolding epOwnerLeft(b, b) in
78 unfolding epOwnerX(c, c) in
[-----------------
79 unfolding epOwnerLeft(c, c) in
-----------------]
80 unfolding epOwnerX(a, a) in unfolding epOwnerLeft(a, a) in b.x - c.x == c.x - a.x;
81 ensures a != b;
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
78 unfolding epOwnerX(c, c) in
79 unfolding epOwnerLeft(c, c) in
[--------------
80 unfolding epOwnerX(a, a) in unfolding epOwnerLeft(a, a) in b.x - c.x == c.x - a.x;
--------------]
81 ensures a != b;
82 ensures a != c;
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
78 unfolding epOwnerX(c, c) in
79 unfolding epOwnerLeft(c, c) in
[-----------------
80 unfolding epOwnerX(a, a) in unfolding epOwnerLeft(a, a) in b.x - c.x == c.x - a.x;
-----------------]
81 ensures a != b;
82 ensures a != c;
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
97 ensures Perm(c.left, write);
98 ensures Perm(epOwnerLeft(c, c), write);
[--------------
99 ensures unfolding epOwnerX(a, a) in
--------------]
100 unfolding epOwnerLeft(a, a) in unfolding epOwnerX(b, b) in unfolding epOwnerLeft(b, b) in a.x == b.x;
101 ensures unfolding epOwnerX(b, b) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
98 ensures Perm(epOwnerLeft(c, c), write);
99 ensures unfolding epOwnerX(a, a) in
[-----------------
100 unfolding epOwnerLeft(a, a) in unfolding epOwnerX(b, b) in unfolding epOwnerLeft(b, b) in a.x == b.x;
-----------------]
101 ensures unfolding epOwnerX(b, b) in
102 unfolding epOwnerLeft(b, b) in unfolding epOwnerX(c, c) in unfolding epOwnerLeft(c, c) in b.x == c.x;
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
98 ensures Perm(epOwnerLeft(c, c), write);
99 ensures unfolding epOwnerX(a, a) in
[--------------
100 unfolding epOwnerLeft(a, a) in unfolding epOwnerX(b, b) in unfolding epOwnerLeft(b, b) in a.x == b.x;
--------------]
101 ensures unfolding epOwnerX(b, b) in
102 unfolding epOwnerLeft(b, b) in unfolding epOwnerX(c, c) in unfolding epOwnerLeft(c, c) in b.x == c.x;
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
98 ensures Perm(epOwnerLeft(c, c), write);
99 ensures unfolding epOwnerX(a, a) in
[-----------------
100 unfolding epOwnerLeft(a, a) in unfolding epOwnerX(b, b) in unfolding epOwnerLeft(b, b) in a.x == b.x;
-----------------]
101 ensures unfolding epOwnerX(b, b) in
102 unfolding epOwnerLeft(b, b) in unfolding epOwnerX(c, c) in unfolding epOwnerLeft(c, c) in b.x == c.x;
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
99 ensures unfolding epOwnerX(a, a) in
100 unfolding epOwnerLeft(a, a) in unfolding epOwnerX(b, b) in unfolding epOwnerLeft(b, b) in a.x == b.x;
[--------------
101 ensures unfolding epOwnerX(b, b) in
--------------]
102 unfolding epOwnerLeft(b, b) in unfolding epOwnerX(c, c) in unfolding epOwnerLeft(c, c) in b.x == c.x;
103 run {
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
100 unfolding epOwnerLeft(a, a) in unfolding epOwnerX(b, b) in unfolding epOwnerLeft(b, b) in a.x == b.x;
101 ensures unfolding epOwnerX(b, b) in
[-----------------
102 unfolding epOwnerLeft(b, b) in unfolding epOwnerX(c, c) in unfolding epOwnerLeft(c, c) in b.x == c.x;
-----------------]
103 run {
104 assert b != a;
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
100 unfolding epOwnerLeft(a, a) in unfolding epOwnerX(b, b) in unfolding epOwnerLeft(b, b) in a.x == b.x;
101 ensures unfolding epOwnerX(b, b) in
[--------------
102 unfolding epOwnerLeft(b, b) in unfolding epOwnerX(c, c) in unfolding epOwnerLeft(c, c) in b.x == c.x;
--------------]
103 run {
104 assert b != a;
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
100 unfolding epOwnerLeft(a, a) in unfolding epOwnerX(b, b) in unfolding epOwnerLeft(b, b) in a.x == b.x;
101 ensures unfolding epOwnerX(b, b) in
[-----------------
102 unfolding epOwnerLeft(b, b) in unfolding epOwnerX(c, c) in unfolding epOwnerLeft(c, c) in b.x == c.x;
-----------------]
103 run {
104 assert b != a;
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
)
Expected test result: pass
Actual test result: crash with message:
The following error occurred during choreography verification:
The encodePermissionStratification rewrite caused the AST to no longer typecheck:
======================================
49 Perm(c.left, write) ** Perm(epOwnerLeft(c, c), write) **
50 true **
[--------------
51 (unfolding epOwnerX(b, b) in
--------------]
52 unfolding epOwnerLeft(b, b) in
53 unfolding epOwnerX(c, c) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
50 true **
51 (unfolding epOwnerX(b, b) in
[-----------------
52 unfolding epOwnerLeft(b, b) in
-----------------]
53 unfolding epOwnerX(c, c) in
54 unfolding epOwnerLeft(c, c) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
51 (unfolding epOwnerX(b, b) in
52 unfolding epOwnerLeft(b, b) in
[--------------
53 unfolding epOwnerX(c, c) in
--------------]
54 unfolding epOwnerLeft(c, c) in
55 unfolding epOwnerX(a, a) in unfolding epOwnerLeft(a, a) in b.x - c.x == c.x - a.x);
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
52 unfolding epOwnerLeft(b, b) in
53 unfolding epOwnerX(c, c) in
[-----------------
54 unfolding epOwnerLeft(c, c) in
-----------------]
55 unfolding epOwnerX(a, a) in unfolding epOwnerLeft(a, a) in b.x - c.x == c.x - a.x);
56 }
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
53 unfolding epOwnerX(c, c) in
54 unfolding epOwnerLeft(c, c) in
[--------------
55 unfolding epOwnerX(a, a) in unfolding epOwnerLeft(a, a) in b.x - c.x == c.x - a.x);
--------------]
56 }
57
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
53 unfolding epOwnerX(c, c) in
54 unfolding epOwnerLeft(c, c) in
[-----------------
55 unfolding epOwnerX(a, a) in unfolding epOwnerLeft(a, a) in b.x - c.x == c.x - a.x);
-----------------]
56 }
57
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
150 loop_invariant Perm(c.left, write);
151 loop_invariant Perm(epOwnerLeft(c, c), write);
[--------------
152 loop_invariant unfolding epOwnerX(b, b) in
--------------]
153 unfolding epOwnerLeft(b, b) in
154 unfolding epOwnerX(c, c) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
151 loop_invariant Perm(epOwnerLeft(c, c), write);
152 loop_invariant unfolding epOwnerX(b, b) in
[-----------------
153 unfolding epOwnerLeft(b, b) in
-----------------]
154 unfolding epOwnerX(c, c) in
155 unfolding epOwnerLeft(c, c) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
152 loop_invariant unfolding epOwnerX(b, b) in
153 unfolding epOwnerLeft(b, b) in
[--------------
154 unfolding epOwnerX(c, c) in
--------------]
155 unfolding epOwnerLeft(c, c) in
156 unfolding epOwnerX(a, a) in unfolding epOwnerLeft(a, a) in b.x - c.x == c.x - a.x;
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
153 unfolding epOwnerLeft(b, b) in
154 unfolding epOwnerX(c, c) in
[-----------------
155 unfolding epOwnerLeft(c, c) in
-----------------]
156 unfolding epOwnerX(a, a) in unfolding epOwnerLeft(a, a) in b.x - c.x == c.x - a.x;
157 loop_invariant unfolding epOwnerX(b, b) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
154 unfolding epOwnerX(c, c) in
155 unfolding epOwnerLeft(c, c) in
[--------------
156 unfolding epOwnerX(a, a) in unfolding epOwnerLeft(a, a) in b.x - c.x == c.x - a.x;
--------------]
157 loop_invariant unfolding epOwnerX(b, b) in
158 unfolding epOwnerLeft(b, b) in unfolding epOwnerX(a, a) in unfolding epOwnerLeft(a, a) in b.left == a.x;
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
154 unfolding epOwnerX(c, c) in
155 unfolding epOwnerLeft(c, c) in
[-----------------
156 unfolding epOwnerX(a, a) in unfolding epOwnerLeft(a, a) in b.x - c.x == c.x - a.x;
-----------------]
157 loop_invariant unfolding epOwnerX(b, b) in
158 unfolding epOwnerLeft(b, b) in unfolding epOwnerX(a, a) in unfolding epOwnerLeft(a, a) in b.left == a.x;
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
155 unfolding epOwnerLeft(c, c) in
156 unfolding epOwnerX(a, a) in unfolding epOwnerLeft(a, a) in b.x - c.x == c.x - a.x;
[--------------
157 loop_invariant unfolding epOwnerX(b, b) in
--------------]
158 unfolding epOwnerLeft(b, b) in unfolding epOwnerX(a, a) in unfolding epOwnerLeft(a, a) in b.left == a.x;
159 loop_invariant unfolding epOwnerX(c, c) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
156 unfolding epOwnerX(a, a) in unfolding epOwnerLeft(a, a) in b.x - c.x == c.x - a.x;
157 loop_invariant unfolding epOwnerX(b, b) in
[-----------------
158 unfolding epOwnerLeft(b, b) in unfolding epOwnerX(a, a) in unfolding epOwnerLeft(a, a) in b.left == a.x;
-----------------]
159 loop_invariant unfolding epOwnerX(c, c) in
160 unfolding epOwnerLeft(c, c) in unfolding epOwnerX(b, b) in unfolding epOwnerLeft(b, b) in c.left == b.x;
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
156 unfolding epOwnerX(a, a) in unfolding epOwnerLeft(a, a) in b.x - c.x == c.x - a.x;
157 loop_invariant unfolding epOwnerX(b, b) in
[--------------
158 unfolding epOwnerLeft(b, b) in unfolding epOwnerX(a, a) in unfolding epOwnerLeft(a, a) in b.left == a.x;
--------------]
159 loop_invariant unfolding epOwnerX(c, c) in
160 unfolding epOwnerLeft(c, c) in unfolding epOwnerX(b, b) in unfolding epOwnerLeft(b, b) in c.left == b.x;
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
156 unfolding epOwnerX(a, a) in unfolding epOwnerLeft(a, a) in b.x - c.x == c.x - a.x;
157 loop_invariant unfolding epOwnerX(b, b) in
[-----------------
158 unfolding epOwnerLeft(b, b) in unfolding epOwnerX(a, a) in unfolding epOwnerLeft(a, a) in b.left == a.x;
-----------------]
159 loop_invariant unfolding epOwnerX(c, c) in
160 unfolding epOwnerLeft(c, c) in unfolding epOwnerX(b, b) in unfolding epOwnerLeft(b, b) in c.left == b.x;
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
157 loop_invariant unfolding epOwnerX(b, b) in
158 unfolding epOwnerLeft(b, b) in unfolding epOwnerX(a, a) in unfolding epOwnerLeft(a, a) in b.left == a.x;
[--------------
159 loop_invariant unfolding epOwnerX(c, c) in
--------------]
160 unfolding epOwnerLeft(c, c) in unfolding epOwnerX(b, b) in unfolding epOwnerLeft(b, b) in c.left == b.x;
161 loop_invariant unfolding epOwnerX(a, a) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
158 unfolding epOwnerLeft(b, b) in unfolding epOwnerX(a, a) in unfolding epOwnerLeft(a, a) in b.left == a.x;
159 loop_invariant unfolding epOwnerX(c, c) in
[-----------------
160 unfolding epOwnerLeft(c, c) in unfolding epOwnerX(b, b) in unfolding epOwnerLeft(b, b) in c.left == b.x;
-----------------]
161 loop_invariant unfolding epOwnerX(a, a) in
162 unfolding epOwnerLeft(a, a) in unfolding epOwnerX(c, c) in unfolding epOwnerLeft(c, c) in a.left == c.x;
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
158 unfolding epOwnerLeft(b, b) in unfolding epOwnerX(a, a) in unfolding epOwnerLeft(a, a) in b.left == a.x;
159 loop_invariant unfolding epOwnerX(c, c) in
[--------------
160 unfolding epOwnerLeft(c, c) in unfolding epOwnerX(b, b) in unfolding epOwnerLeft(b, b) in c.left == b.x;
--------------]
161 loop_invariant unfolding epOwnerX(a, a) in
162 unfolding epOwnerLeft(a, a) in unfolding epOwnerX(c, c) in unfolding epOwnerLeft(c, c) in a.left == c.x;
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
158 unfolding epOwnerLeft(b, b) in unfolding epOwnerX(a, a) in unfolding epOwnerLeft(a, a) in b.left == a.x;
159 loop_invariant unfolding epOwnerX(c, c) in
[-----------------
160 unfolding epOwnerLeft(c, c) in unfolding epOwnerX(b, b) in unfolding epOwnerLeft(b, b) in c.left == b.x;
-----------------]
161 loop_invariant unfolding epOwnerX(a, a) in
162 unfolding epOwnerLeft(a, a) in unfolding epOwnerX(c, c) in unfolding epOwnerLeft(c, c) in a.left == c.x;
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
159 loop_invariant unfolding epOwnerX(c, c) in
160 unfolding epOwnerLeft(c, c) in unfolding epOwnerX(b, b) in unfolding epOwnerLeft(b, b) in c.left == b.x;
[--------------
161 loop_invariant unfolding epOwnerX(a, a) in
--------------]
162 unfolding epOwnerLeft(a, a) in unfolding epOwnerX(c, c) in unfolding epOwnerLeft(c, c) in a.left == c.x;
163 loop_invariant readLeft(a, a) != readX(a, a) == readLeft(b, b) != readX(b, b);
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
160 unfolding epOwnerLeft(c, c) in unfolding epOwnerX(b, b) in unfolding epOwnerLeft(b, b) in c.left == b.x;
161 loop_invariant unfolding epOwnerX(a, a) in
[-----------------
162 unfolding epOwnerLeft(a, a) in unfolding epOwnerX(c, c) in unfolding epOwnerLeft(c, c) in a.left == c.x;
-----------------]
163 loop_invariant readLeft(a, a) != readX(a, a) == readLeft(b, b) != readX(b, b);
164 loop_invariant readLeft(b, b) != readX(b, b) == readLeft(c, c) != readX(c, c);
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
160 unfolding epOwnerLeft(c, c) in unfolding epOwnerX(b, b) in unfolding epOwnerLeft(b, b) in c.left == b.x;
161 loop_invariant unfolding epOwnerX(a, a) in
[--------------
162 unfolding epOwnerLeft(a, a) in unfolding epOwnerX(c, c) in unfolding epOwnerLeft(c, c) in a.left == c.x;
--------------]
163 loop_invariant readLeft(a, a) != readX(a, a) == readLeft(b, b) != readX(b, b);
164 loop_invariant readLeft(b, b) != readX(b, b) == readLeft(c, c) != readX(c, c);
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
160 unfolding epOwnerLeft(c, c) in unfolding epOwnerX(b, b) in unfolding epOwnerLeft(b, b) in c.left == b.x;
161 loop_invariant unfolding epOwnerX(a, a) in
[-----------------
162 unfolding epOwnerLeft(a, a) in unfolding epOwnerX(c, c) in unfolding epOwnerLeft(c, c) in a.left == c.x;
-----------------]
163 loop_invariant readLeft(a, a) != readX(a, a) == readLeft(b, b) != readX(b, b);
164 loop_invariant readLeft(b, b) != readX(b, b) == readLeft(c, c) != readX(c, c);
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
74 requires Perm(c.left, write);
75 requires Perm(epOwnerLeft(c, c), write);
[--------------
76 requires unfolding epOwnerX(b, b) in
--------------]
77 unfolding epOwnerLeft(b, b) in
78 unfolding epOwnerX(c, c) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
75 requires Perm(epOwnerLeft(c, c), write);
76 requires unfolding epOwnerX(b, b) in
[-----------------
77 unfolding epOwnerLeft(b, b) in
-----------------]
78 unfolding epOwnerX(c, c) in
79 unfolding epOwnerLeft(c, c) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
76 requires unfolding epOwnerX(b, b) in
77 unfolding epOwnerLeft(b, b) in
[--------------
78 unfolding epOwnerX(c, c) in
--------------]
79 unfolding epOwnerLeft(c, c) in
80 unfolding epOwnerX(a, a) in unfolding epOwnerLeft(a, a) in b.x - c.x == c.x - a.x;
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
77 unfolding epOwnerLeft(b, b) in
78 unfolding epOwnerX(c, c) in
[-----------------
79 unfolding epOwnerLeft(c, c) in
-----------------]
80 unfolding epOwnerX(a, a) in unfolding epOwnerLeft(a, a) in b.x - c.x == c.x - a.x;
81 ensures a != b;
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
78 unfolding epOwnerX(c, c) in
79 unfolding epOwnerLeft(c, c) in
[--------------
80 unfolding epOwnerX(a, a) in unfolding epOwnerLeft(a, a) in b.x - c.x == c.x - a.x;
--------------]
81 ensures a != b;
82 ensures a != c;
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
78 unfolding epOwnerX(c, c) in
79 unfolding epOwnerLeft(c, c) in
[-----------------
80 unfolding epOwnerX(a, a) in unfolding epOwnerLeft(a, a) in b.x - c.x == c.x - a.x;
-----------------]
81 ensures a != b;
82 ensures a != c;
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
97 ensures Perm(c.left, write);
98 ensures Perm(epOwnerLeft(c, c), write);
[--------------
99 ensures unfolding epOwnerX(a, a) in
--------------]
100 unfolding epOwnerLeft(a, a) in unfolding epOwnerX(b, b) in unfolding epOwnerLeft(b, b) in a.x == b.x;
101 ensures unfolding epOwnerX(b, b) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
98 ensures Perm(epOwnerLeft(c, c), write);
99 ensures unfolding epOwnerX(a, a) in
[-----------------
100 unfolding epOwnerLeft(a, a) in unfolding epOwnerX(b, b) in unfolding epOwnerLeft(b, b) in a.x == b.x;
-----------------]
101 ensures unfolding epOwnerX(b, b) in
102 unfolding epOwnerLeft(b, b) in unfolding epOwnerX(c, c) in unfolding epOwnerLeft(c, c) in b.x == c.x;
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
98 ensures Perm(epOwnerLeft(c, c), write);
99 ensures unfolding epOwnerX(a, a) in
[--------------
100 unfolding epOwnerLeft(a, a) in unfolding epOwnerX(b, b) in unfolding epOwnerLeft(b, b) in a.x == b.x;
--------------]
101 ensures unfolding epOwnerX(b, b) in
102 unfolding epOwnerLeft(b, b) in unfolding epOwnerX(c, c) in unfolding epOwnerLeft(c, c) in b.x == c.x;
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
98 ensures Perm(epOwnerLeft(c, c), write);
99 ensures unfolding epOwnerX(a, a) in
[-----------------
100 unfolding epOwnerLeft(a, a) in unfolding epOwnerX(b, b) in unfolding epOwnerLeft(b, b) in a.x == b.x;
-----------------]
101 ensures unfolding epOwnerX(b, b) in
102 unfolding epOwnerLeft(b, b) in unfolding epOwnerX(c, c) in unfolding epOwnerLeft(c, c) in b.x == c.x;
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
99 ensures unfolding epOwnerX(a, a) in
100 unfolding epOwnerLeft(a, a) in unfolding epOwnerX(b, b) in unfolding epOwnerLeft(b, b) in a.x == b.x;
[--------------
101 ensures unfolding epOwnerX(b, b) in
--------------]
102 unfolding epOwnerLeft(b, b) in unfolding epOwnerX(c, c) in unfolding epOwnerLeft(c, c) in b.x == c.x;
103 run {
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
100 unfolding epOwnerLeft(a, a) in unfolding epOwnerX(b, b) in unfolding epOwnerLeft(b, b) in a.x == b.x;
101 ensures unfolding epOwnerX(b, b) in
[-----------------
102 unfolding epOwnerLeft(b, b) in unfolding epOwnerX(c, c) in unfolding epOwnerLeft(c, c) in b.x == c.x;
-----------------]
103 run {
104 assert b != a;
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
100 unfolding epOwnerLeft(a, a) in unfolding epOwnerX(b, b) in unfolding epOwnerLeft(b, b) in a.x == b.x;
101 ensures unfolding epOwnerX(b, b) in
[--------------
102 unfolding epOwnerLeft(b, b) in unfolding epOwnerX(c, c) in unfolding epOwnerLeft(c, c) in b.x == c.x;
--------------]
103 run {
104 assert b != a;
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
100 unfolding epOwnerLeft(a, a) in unfolding epOwnerX(b, b) in unfolding epOwnerLeft(b, b) in a.x == b.x;
101 ensures unfolding epOwnerX(b, b) in
[-----------------
102 unfolding epOwnerLeft(b, b) in unfolding epOwnerX(c, c) in unfolding epOwnerLeft(c, c) in b.x == c.x;
-----------------]
103 run {
104 assert b != a;
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
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
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:
The encodePermissionStratification rewrite caused the AST to no longer typecheck:
======================================
1377 Perm(p2.turn, write) ** Perm(epOwnerTurn(p2, p2), write) **
1378 true **
[------------------
1379 (unfolding epOwnerC00(p1, p1) in
------------------]
1380 unfolding epOwnerC01(p1, p1) in
1381 unfolding epOwnerC02(p1, p1) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1378 true **
1379 (unfolding epOwnerC00(p1, p1) in
[------------------
1380 unfolding epOwnerC01(p1, p1) in
------------------]
1381 unfolding epOwnerC02(p1, p1) in
1382 unfolding epOwnerC10(p1, p1) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1379 (unfolding epOwnerC00(p1, p1) in
1380 unfolding epOwnerC01(p1, p1) in
[------------------
1381 unfolding epOwnerC02(p1, p1) in
------------------]
1382 unfolding epOwnerC10(p1, p1) in
1383 unfolding epOwnerC11(p1, p1) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1380 unfolding epOwnerC01(p1, p1) in
1381 unfolding epOwnerC02(p1, p1) in
[------------------
1382 unfolding epOwnerC10(p1, p1) in
------------------]
1383 unfolding epOwnerC11(p1, p1) in
1384 unfolding epOwnerC12(p1, p1) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1381 unfolding epOwnerC02(p1, p1) in
1382 unfolding epOwnerC10(p1, p1) in
[------------------
1383 unfolding epOwnerC11(p1, p1) in
------------------]
1384 unfolding epOwnerC12(p1, p1) in
1385 unfolding epOwnerC20(p1, p1) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1382 unfolding epOwnerC10(p1, p1) in
1383 unfolding epOwnerC11(p1, p1) in
[------------------
1384 unfolding epOwnerC12(p1, p1) in
------------------]
1385 unfolding epOwnerC20(p1, p1) in
1386 unfolding epOwnerC21(p1, p1) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1383 unfolding epOwnerC11(p1, p1) in
1384 unfolding epOwnerC12(p1, p1) in
[------------------
1385 unfolding epOwnerC20(p1, p1) in
------------------]
1386 unfolding epOwnerC21(p1, p1) in
1387 unfolding epOwnerC22(p1, p1) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1384 unfolding epOwnerC12(p1, p1) in
1385 unfolding epOwnerC20(p1, p1) in
[------------------
1386 unfolding epOwnerC21(p1, p1) in
------------------]
1387 unfolding epOwnerC22(p1, p1) in
1388 unfolding epOwnerMyMark(p1, p1) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1385 unfolding epOwnerC20(p1, p1) in
1386 unfolding epOwnerC21(p1, p1) in
[------------------
1387 unfolding epOwnerC22(p1, p1) in
------------------]
1388 unfolding epOwnerMyMark(p1, p1) in
1389 unfolding epOwnerMove(p1, p1) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1386 unfolding epOwnerC21(p1, p1) in
1387 unfolding epOwnerC22(p1, p1) in
[---------------------
1388 unfolding epOwnerMyMark(p1, p1) in
---------------------]
1389 unfolding epOwnerMove(p1, p1) in
1390 unfolding epOwnerTurn(p1, p1) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1387 unfolding epOwnerC22(p1, p1) in
1388 unfolding epOwnerMyMark(p1, p1) in
[-------------------
1389 unfolding epOwnerMove(p1, p1) in
-------------------]
1390 unfolding epOwnerTurn(p1, p1) in
1391 unfolding epOwnerI(p1, p1.move) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1388 unfolding epOwnerMyMark(p1, p1) in
1389 unfolding epOwnerMove(p1, p1) in
[-------------------
1390 unfolding epOwnerTurn(p1, p1) in
-------------------]
1391 unfolding epOwnerI(p1, p1.move) in
1392 unfolding epOwnerJ(p1, p1.move) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1389 unfolding epOwnerMove(p1, p1) in
1390 unfolding epOwnerTurn(p1, p1) in
[---------------------
1391 unfolding epOwnerI(p1, p1.move) in
---------------------]
1392 unfolding epOwnerJ(p1, p1.move) in
1393 unfolding epOwnerMark(p1, p1.move) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1390 unfolding epOwnerTurn(p1, p1) in
1391 unfolding epOwnerI(p1, p1.move) in
[---------------------
1392 unfolding epOwnerJ(p1, p1.move) in
---------------------]
1393 unfolding epOwnerMark(p1, p1.move) in
1394 unfolding epOwnerC00(p2, p2) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1391 unfolding epOwnerI(p1, p1.move) in
1392 unfolding epOwnerJ(p1, p1.move) in
[------------------------
1393 unfolding epOwnerMark(p1, p1.move) in
------------------------]
1394 unfolding epOwnerC00(p2, p2) in
1395 unfolding epOwnerC01(p2, p2) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1392 unfolding epOwnerJ(p1, p1.move) in
1393 unfolding epOwnerMark(p1, p1.move) in
[------------------
1394 unfolding epOwnerC00(p2, p2) in
------------------]
1395 unfolding epOwnerC01(p2, p2) in
1396 unfolding epOwnerC02(p2, p2) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1393 unfolding epOwnerMark(p1, p1.move) in
1394 unfolding epOwnerC00(p2, p2) in
[------------------
1395 unfolding epOwnerC01(p2, p2) in
------------------]
1396 unfolding epOwnerC02(p2, p2) in
1397 unfolding epOwnerC10(p2, p2) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1394 unfolding epOwnerC00(p2, p2) in
1395 unfolding epOwnerC01(p2, p2) in
[------------------
1396 unfolding epOwnerC02(p2, p2) in
------------------]
1397 unfolding epOwnerC10(p2, p2) in
1398 unfolding epOwnerC11(p2, p2) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1395 unfolding epOwnerC01(p2, p2) in
1396 unfolding epOwnerC02(p2, p2) in
[------------------
1397 unfolding epOwnerC10(p2, p2) in
------------------]
1398 unfolding epOwnerC11(p2, p2) in
1399 unfolding epOwnerC12(
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1396 unfolding epOwnerC02(p2, p2) in
1397 unfolding epOwnerC10(p2, p2) in
[------------------
1398 unfolding epOwnerC11(p2, p2) in
------------------]
1399 unfolding epOwnerC12(
1400 p2,
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1397 unfolding epOwnerC10(p2, p2) in
1398 unfolding epOwnerC11(p2, p2) in
[-----------
1399 unfolding epOwnerC12(
1400 p2,
1401 p2
1402 ) in
---------------------------------------------------------------------------------------------]
1403 unfolding epOwnerC20(
1404 p2,
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1401 p2
1402 ) in
[-----------
1403 unfolding epOwnerC20(
1404 p2,
1405 p2
1406 ) in
-------------------------------------------------------------------------------------------------]
1407 unfolding epOwnerC21(
1408 p2,
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1405 p2
1406 ) in
[-----------
1407 unfolding epOwnerC21(
1408 p2,
1409 p2
1410 ) in
-----------------------------------------------------------------------------------------------------]
1411 unfolding epOwnerC22(
1412 p2,
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1409 p2
1410 ) in
[-----------
1411 unfolding epOwnerC22(
1412 p2,
1413 p2
1414 ) in
---------------------------------------------------------------------------------------------------------]
1415 unfolding epOwnerMyMark(
1416 p2,
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1413 p2
1414 ) in
[--------------
1415 unfolding epOwnerMyMark(
1416 p2,
1417 p2
1418 ) in
-------------------------------------------------------------------------------------------------------------]
1419 unfolding epOwnerMove(
1420 p2,
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1417 p2
1418 ) in
[------------
1419 unfolding epOwnerMove(
1420 p2,
1421 p2
1422 ) in
-----------------------------------------------------------------------------------------------------------------]
1423 unfolding epOwnerTurn(
1424 p2,
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1421 p2
1422 ) in
[------------
1423 unfolding epOwnerTurn(
1424 p2,
1425 p2
1426 ) in
---------------------------------------------------------------------------------------------------------------------]
1427 unfolding epOwnerI(
1428 p2,
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1425 p2
1426 ) in
[---------
1427 unfolding epOwnerI(
1428 p2,
1429 p2.move
1430 ) in
-------------------------------------------------------------------------------------------------------------------------]
1431 unfolding epOwnerJ(
1432 p2,
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1429 p2.move
1430 ) in
[---------
1431 unfolding epOwnerJ(
1432 p2,
1433 p2.move
1434 ) in
-----------------------------------------------------------------------------------------------------------------------------]
1435 unfolding epOwnerMark(
1436 p2,
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1433 p2.move
1434 ) in
[------------
1435 unfolding epOwnerMark(
1436 p2,
1437 p2.move
1438 ) in
---------------------------------------------------------------------------------------------------------------------------------]
1439 [write](p1.myMark ==
1440 0 **
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1794 loop_invariant Perm(p2.turn, write);
1795 loop_invariant Perm(epOwnerTurn(p2, p2), write);
[------------------
1796 loop_invariant unfolding epOwnerC00(p1, p1) in
------------------]
1797 unfolding epOwnerC01(p1, p1) in
1798 unfolding epOwnerC02(p1, p1) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1795 loop_invariant Perm(epOwnerTurn(p2, p2), write);
1796 loop_invariant unfolding epOwnerC00(p1, p1) in
[------------------
1797 unfolding epOwnerC01(p1, p1) in
------------------]
1798 unfolding epOwnerC02(p1, p1) in
1799 unfolding epOwnerC10(p1, p1) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1796 loop_invariant unfolding epOwnerC00(p1, p1) in
1797 unfolding epOwnerC01(p1, p1) in
[------------------
1798 unfolding epOwnerC02(p1, p1) in
------------------]
1799 unfolding epOwnerC10(p1, p1) in
1800 unfolding epOwnerC11(p1, p1) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1797 unfolding epOwnerC01(p1, p1) in
1798 unfolding epOwnerC02(p1, p1) in
[------------------
1799 unfolding epOwnerC10(p1, p1) in
------------------]
1800 unfolding epOwnerC11(p1, p1) in
1801 unfolding epOwnerC12(p1, p1) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1798 unfolding epOwnerC02(p1, p1) in
1799 unfolding epOwnerC10(p1, p1) in
[------------------
1800 unfolding epOwnerC11(p1, p1) in
------------------]
1801 unfolding epOwnerC12(p1, p1) in
1802 unfolding epOwnerC20(p1, p1) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1799 unfolding epOwnerC10(p1, p1) in
1800 unfolding epOwnerC11(p1, p1) in
[------------------
1801 unfolding epOwnerC12(p1, p1) in
------------------]
1802 unfolding epOwnerC20(p1, p1) in
1803 unfolding epOwnerC21(p1, p1) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1800 unfolding epOwnerC11(p1, p1) in
1801 unfolding epOwnerC12(p1, p1) in
[------------------
1802 unfolding epOwnerC20(p1, p1) in
------------------]
1803 unfolding epOwnerC21(p1, p1) in
1804 unfolding epOwnerC22(p1, p1) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1801 unfolding epOwnerC12(p1, p1) in
1802 unfolding epOwnerC20(p1, p1) in
[------------------
1803 unfolding epOwnerC21(p1, p1) in
------------------]
1804 unfolding epOwnerC22(p1, p1) in
1805 unfolding epOwnerMyMark(p1, p1) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1802 unfolding epOwnerC20(p1, p1) in
1803 unfolding epOwnerC21(p1, p1) in
[------------------
1804 unfolding epOwnerC22(p1, p1) in
------------------]
1805 unfolding epOwnerMyMark(p1, p1) in
1806 unfolding epOwnerMove(p1, p1) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1803 unfolding epOwnerC21(p1, p1) in
1804 unfolding epOwnerC22(p1, p1) in
[---------------------
1805 unfolding epOwnerMyMark(p1, p1) in
---------------------]
1806 unfolding epOwnerMove(p1, p1) in
1807 unfolding epOwnerTurn(p1, p1) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1804 unfolding epOwnerC22(p1, p1) in
1805 unfolding epOwnerMyMark(p1, p1) in
[-------------------
1806 unfolding epOwnerMove(p1, p1) in
-------------------]
1807 unfolding epOwnerTurn(p1, p1) in
1808 unfolding epOwnerI(p1, p1.move) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1805 unfolding epOwnerMyMark(p1, p1) in
1806 unfolding epOwnerMove(p1, p1) in
[-------------------
1807 unfolding epOwnerTurn(p1, p1) in
-------------------]
1808 unfolding epOwnerI(p1, p1.move) in
1809 unfolding epOwnerJ(p1, p1.move) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1806 unfolding epOwnerMove(p1, p1) in
1807 unfolding epOwnerTurn(p1, p1) in
[---------------------
1808 unfolding epOwnerI(p1, p1.move) in
---------------------]
1809 unfolding epOwnerJ(p1, p1.move) in
1810 unfolding epOwnerMark(p1, p1.move) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1807 unfolding epOwnerTurn(p1, p1) in
1808 unfolding epOwnerI(p1, p1.move) in
[---------------------
1809 unfolding epOwnerJ(p1, p1.move) in
---------------------]
1810 unfolding epOwnerMark(p1, p1.move) in
1811 unfolding epOwnerC00(p2, p2) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1808 unfolding epOwnerI(p1, p1.move) in
1809 unfolding epOwnerJ(p1, p1.move) in
[------------------------
1810 unfolding epOwnerMark(p1, p1.move) in
------------------------]
1811 unfolding epOwnerC00(p2, p2) in
1812 unfolding epOwnerC01(p2, p2) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1809 unfolding epOwnerJ(p1, p1.move) in
1810 unfolding epOwnerMark(p1, p1.move) in
[------------------
1811 unfolding epOwnerC00(p2, p2) in
------------------]
1812 unfolding epOwnerC01(p2, p2) in
1813 unfolding epOwnerC02(p2, p2) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1810 unfolding epOwnerMark(p1, p1.move) in
1811 unfolding epOwnerC00(p2, p2) in
[------------------
1812 unfolding epOwnerC01(p2, p2) in
------------------]
1813 unfolding epOwnerC02(p2, p2) in
1814 unfolding epOwnerC10(p2, p2) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1811 unfolding epOwnerC00(p2, p2) in
1812 unfolding epOwnerC01(p2, p2) in
[------------------
1813 unfolding epOwnerC02(p2, p2) in
------------------]
1814 unfolding epOwnerC10(p2, p2) in
1815 unfolding epOwnerC11(p2, p2) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1812 unfolding epOwnerC01(p2, p2) in
1813 unfolding epOwnerC02(p2, p2) in
[------------------
1814 unfolding epOwnerC10(p2, p2) in
------------------]
1815 unfolding epOwnerC11(p2, p2) in
1816 unfolding epOwnerC12(p2, p2) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1813 unfolding epOwnerC02(p2, p2) in
1814 unfolding epOwnerC10(p2, p2) in
[------------------
1815 unfolding epOwnerC11(p2, p2) in
------------------]
1816 unfolding epOwnerC12(p2, p2) in
1817 unfolding epOwnerC20(
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1814 unfolding epOwnerC10(p2, p2) in
1815 unfolding epOwnerC11(p2, p2) in
[------------------
1816 unfolding epOwnerC12(p2, p2) in
------------------]
1817 unfolding epOwnerC20(
1818 p2,
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1815 unfolding epOwnerC11(p2, p2) in
1816 unfolding epOwnerC12(p2, p2) in
[-----------
1817 unfolding epOwnerC20(
1818 p2,
1819 p2
1820 ) in
---------------------------------------------------------------------------------------------]
1821 unfolding epOwnerC21(
1822 p2,
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1819 p2
1820 ) in
[-----------
1821 unfolding epOwnerC21(
1822 p2,
1823 p2
1824 ) in
-------------------------------------------------------------------------------------------------]
1825 unfolding epOwnerC22(
1826 p2,
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1823 p2
1824 ) in
[-----------
1825 unfolding epOwnerC22(
1826 p2,
1827 p2
1828 ) in
-----------------------------------------------------------------------------------------------------]
1829 unfolding epOwnerMyMark(
1830 p2,
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1827 p2
1828 ) in
[--------------
1829 unfolding epOwnerMyMark(
1830 p2,
1831 p2
1832 ) in
---------------------------------------------------------------------------------------------------------]
1833 unfolding epOwnerMove(
1834 p2,
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1831 p2
1832 ) in
[------------
1833 unfolding epOwnerMove(
1834 p2,
1835 p2
1836 ) in
-------------------------------------------------------------------------------------------------------------]
1837 unfolding epOwnerTurn(
1838 p2,
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1835 p2
1836 ) in
[------------
1837 unfolding epOwnerTurn(
1838 p2,
1839 p2
1840 ) in
-----------------------------------------------------------------------------------------------------------------]
1841 unfolding epOwnerI(
1842 p2,
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1839 p2
1840 ) in
[---------
1841 unfolding epOwnerI(
1842 p2,
1843 p2.move
1844 ) in
---------------------------------------------------------------------------------------------------------------------]
1845 unfolding epOwnerJ(
1846 p2,
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1843 p2.move
1844 ) in
[---------
1845 unfolding epOwnerJ(
1846 p2,
1847 p2.move
1848 ) in
-------------------------------------------------------------------------------------------------------------------------]
1849 unfolding epOwnerMark(
1850 p2,
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1847 p2.move
1848 ) in
[------------
1849 unfolding epOwnerMark(
1850 p2,
1851 p2.move
1852 ) in
-----------------------------------------------------------------------------------------------------------------------------]
1853 [write](p1.myMark ==
1854 0 **
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1894 Perm(readMove(p2, p2).j, write) ** Perm(epOwnerJ(p2, readMove(p2, p2)), write) **
1895 Perm(readMove(p2, p2).mark, write) ** Perm(epOwnerMark(p2, readMove(p2, p2)), write) **
[------------------
1896 (unfolding epOwnerC00(p2, p2) in
------------------]
1897 unfolding epOwnerC01(p2, p2) in
1898 unfolding epOwnerC02(p2, p2) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1895 Perm(readMove(p2, p2).mark, write) ** Perm(epOwnerMark(p2, readMove(p2, p2)), write) **
1896 (unfolding epOwnerC00(p2, p2) in
[------------------
1897 unfolding epOwnerC01(p2, p2) in
------------------]
1898 unfolding epOwnerC02(p2, p2) in
1899 unfolding epOwnerC10(p2, p2) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1896 (unfolding epOwnerC00(p2, p2) in
1897 unfolding epOwnerC01(p2, p2) in
[------------------
1898 unfolding epOwnerC02(p2, p2) in
------------------]
1899 unfolding epOwnerC10(p2, p2) in
1900 unfolding epOwnerC11(p2, p2) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1897 unfolding epOwnerC01(p2, p2) in
1898 unfolding epOwnerC02(p2, p2) in
[------------------
1899 unfolding epOwnerC10(p2, p2) in
------------------]
1900 unfolding epOwnerC11(p2, p2) in
1901 unfolding epOwnerC12(p2, p2) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1898 unfolding epOwnerC02(p2, p2) in
1899 unfolding epOwnerC10(p2, p2) in
[------------------
1900 unfolding epOwnerC11(p2, p2) in
------------------]
1901 unfolding epOwnerC12(p2, p2) in
1902 unfolding epOwnerC20(p2, p2) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
1899 unfolding epOwnerC10(p2, p2) in
1900 unfolding epOwnerC11(p2, p2) in
[------------------
1901 unfolding epOwnerC12(p2, p2) in
------------------]
1902 unfolding epOwnerC20(p2, p2) in
1...
Check failure on line 222 in test/main/vct/test/integration/helper/VeyMontSpec.scala
github-actions / TestReport
vct.test.integration.examples.veymont.TechnicalVeyMontSpec ► Files examples/technical/veymont/checkLTS/simpleifelse.pvl verifies with silicon
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:Raw output
org.scalatest.exceptions.TestFailedException: Pass did not equal Crash(vct.main.modes.VeyMont$WrapSystemError: The following error occurred during choreography verification:
The encodePermissionStratification rewrite caused the AST to no longer typecheck:
======================================
97 ensures Perm(c.left, write);
98 ensures Perm(epOwnerLeft(c, c), write);
[--------------
99 ensures unfolding epOwnerX(a, a) in
--------------]
100 unfolding epOwnerLeft(a, a) in unfolding epOwnerX(b, b) in unfolding epOwnerLeft(b, b) in a.x == b.x;
101 ensures unfolding epOwnerX(b, b) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
98 ensures Perm(epOwnerLeft(c, c), write);
99 ensures unfolding epOwnerX(a, a) in
[-----------------
100 unfolding epOwnerLeft(a, a) in unfolding epOwnerX(b, b) in unfolding epOwnerLeft(b, b) in a.x == b.x;
-----------------]
101 ensures unfolding epOwnerX(b, b) in
102 unfolding epOwnerLeft(b, b) in unfolding epOwnerX(c, c) in unfolding epOwnerLeft(c, c) in b.x == c.x;
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
98 ensures Perm(epOwnerLeft(c, c), write);
99 ensures unfolding epOwnerX(a, a) in
[--------------
100 unfolding epOwnerLeft(a, a) in unfolding epOwnerX(b, b) in unfolding epOwnerLeft(b, b) in a.x == b.x;
--------------]
101 ensures unfolding epOwnerX(b, b) in
102 unfolding epOwnerLeft(b, b) in unfolding epOwnerX(c, c) in unfolding epOwnerLeft(c, c) in b.x == c.x;
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
98 ensures Perm(epOwnerLeft(c, c), write);
99 ensures unfolding epOwnerX(a, a) in
[-----------------
100 unfolding epOwnerLeft(a, a) in unfolding epOwnerX(b, b) in unfolding epOwnerLeft(b, b) in a.x == b.x;
-----------------]
101 ensures unfolding epOwnerX(b, b) in
102 unfolding epOwnerLeft(b, b) in unfolding epOwnerX(c, c) in unfolding epOwnerLeft(c, c) in b.x == c.x;
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
99 ensures unfolding epOwnerX(a, a) in
100 unfolding epOwnerLeft(a, a) in unfolding epOwnerX(b, b) in unfolding epOwnerLeft(b, b) in a.x == b.x;
[--------------
101 ensures unfolding epOwnerX(b, b) in
--------------]
102 unfolding epOwnerLeft(b, b) in unfolding epOwnerX(c, c) in unfolding epOwnerLeft(c, c) in b.x == c.x;
103 run {
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
100 unfolding epOwnerLeft(a, a) in unfolding epOwnerX(b, b) in unfolding epOwnerLeft(b, b) in a.x == b.x;
101 ensures unfolding epOwnerX(b, b) in
[-----------------
102 unfolding epOwnerLeft(b, b) in unfolding epOwnerX(c, c) in unfolding epOwnerLeft(c, c) in b.x == c.x;
-----------------]
103 run {
104 assert readLeft(a, a) != readX(a, a) == readLeft(b, b) != readX(b, b);
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
100 unfolding epOwnerLeft(a, a) in unfolding epOwnerX(b, b) in unfolding epOwnerLeft(b, b) in a.x == b.x;
101 ensures unfolding epOwnerX(b, b) in
[--------------
102 unfolding epOwnerLeft(b, b) in unfolding epOwnerX(c, c) in unfolding epOwnerLeft(c, c) in b.x == c.x;
--------------]
103 run {
104 assert readLeft(a, a) != readX(a, a) == readLeft(b, b) != readX(b, b);
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
100 unfolding epOwnerLeft(a, a) in unfolding epOwnerX(b, b) in unfolding epOwnerLeft(b, b) in a.x == b.x;
101 ensures unfolding epOwnerX(b, b) in
[-----------------
102 unfolding epOwnerLeft(b, b) in unfolding epOwnerX(c, c) in unfolding epOwnerLeft(c, c) in b.x == c.x;
-----------------]
103 run {
104 assert readLeft(a, a) != readX(a, a) == readLeft(b, b) != readX(b, b);
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
)
Expected test result: pass
Actual test result: crash with message:
The following error occurred during choreography verification:
The encodePermissionStratification rewrite caused the AST to no longer typecheck:
======================================
97 ensures Perm(c.left, write);
98 ensures Perm(epOwnerLeft(c, c), write);
[--------------
99 ensures unfolding epOwnerX(a, a) in
--------------]
100 unfolding epOwnerLeft(a, a) in unfolding epOwnerX(b, b) in unfolding epOwnerLeft(b, b) in a.x == b.x;
101 ensures unfolding epOwnerX(b, b) in
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
98 ensures Perm(epOwnerLeft(c, c), write);
99 ensures unfolding epOwnerX(a, a) in
[-----------------
100 unfolding epOwnerLeft(a, a) in unfolding epOwnerX(b, b) in unfolding epOwnerLeft(b, b) in a.x == b.x;
-----------------]
101 ensures unfolding epOwnerX(b, b) in
102 unfolding epOwnerLeft(b, b) in unfolding epOwnerX(c, c) in unfolding epOwnerLeft(c, c) in b.x == c.x;
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
98 ensures Perm(epOwnerLeft(c, c), write);
99 ensures unfolding epOwnerX(a, a) in
[--------------
100 unfolding epOwnerLeft(a, a) in unfolding epOwnerX(b, b) in unfolding epOwnerLeft(b, b) in a.x == b.x;
--------------]
101 ensures unfolding epOwnerX(b, b) in
102 unfolding epOwnerLeft(b, b) in unfolding epOwnerX(c, c) in unfolding epOwnerLeft(c, c) in b.x == c.x;
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
98 ensures Perm(epOwnerLeft(c, c), write);
99 ensures unfolding epOwnerX(a, a) in
[-----------------
100 unfolding epOwnerLeft(a, a) in unfolding epOwnerX(b, b) in unfolding epOwnerLeft(b, b) in a.x == b.x;
-----------------]
101 ensures unfolding epOwnerX(b, b) in
102 unfolding epOwnerLeft(b, b) in unfolding epOwnerX(c, c) in unfolding epOwnerLeft(c, c) in b.x == c.x;
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
99 ensures unfolding epOwnerX(a, a) in
100 unfolding epOwnerLeft(a, a) in unfolding epOwnerX(b, b) in unfolding epOwnerLeft(b, b) in a.x == b.x;
[--------------
101 ensures unfolding epOwnerX(b, b) in
--------------]
102 unfolding epOwnerLeft(b, b) in unfolding epOwnerX(c, c) in unfolding epOwnerLeft(c, c) in b.x == c.x;
103 run {
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
100 unfolding epOwnerLeft(a, a) in unfolding epOwnerX(b, b) in unfolding epOwnerLeft(b, b) in a.x == b.x;
101 ensures unfolding epOwnerX(b, b) in
[-----------------
102 unfolding epOwnerLeft(b, b) in unfolding epOwnerX(c, c) in unfolding epOwnerLeft(c, c) in b.x == c.x;
-----------------]
103 run {
104 assert readLeft(a, a) != readX(a, a) == readLeft(b, b) != readX(b, b);
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
100 unfolding epOwnerLeft(a, a) in unfolding epOwnerX(b, b) in unfolding epOwnerLeft(b, b) in a.x == b.x;
101 ensures unfolding epOwnerX(b, b) in
[--------------
102 unfolding epOwnerLeft(b, b) in unfolding epOwnerX(c, c) in unfolding epOwnerLeft(c, c) in b.x == c.x;
--------------]
103 run {
104 assert readLeft(a, a) != readX(a, a) == readLeft(b, b) != readX(b, b);
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
======================================
100 unfolding epOwnerLeft(a, a) in unfolding epOwnerX(b, b) in unfolding epOwnerLeft(b, b) in a.x == b.x;
101 ensures unfolding epOwnerX(b, b) in
[-----------------
102 unfolding epOwnerLeft(b, b) in unfolding epOwnerX(c, c) in unfolding epOwnerLeft(c, c) in b.x == c.x;
-----------------]
103 run {
104 assert readLeft(a, a) != readX(a, a) == readLeft(b, b) != readX(b, b);
--------------------------------------
[1/1] This predicate is abstract, and hence cannot be meaningfully folded or unfolded
======================================
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)
Loading