Internal Error Using PVerifier on the Tutorial Example

[daniel-larraz]

I get the following internal error when running p compile on the Two-Phase Commit example after setting the target to PVerifier, as described on this page:

Error: [Internal Error]:
 Not supported expr (Plang.Compiler.TypeChecker.AST.Expressions.ChooseExpr) at PTst/Client.p:59:31
<Please report to the P team or create an issue on GitHub, Thanks!>
Error: [PTool] unhandled exception: System.NotSupportedException: Not supported expr (Plang.Compiler.TypeChecker.AST.Expressions.ChooseExpr) at PTst/Client.p:59:31
 Stack Trace:    at Plang.Compiler.Backend.PVerifier.PVerifierCodeGenerator.ExprToString(IPExpr expr) in /home/runner/work/P/P/Src/PCompiler/CompilerCore/Backend/PVerifier/Uclid5CodeGenerator.cs:line 2053
   at System.Linq.Enumerable.SelectListIterator`2.MoveNext()
   at System.String.Join(String separator, IEnumerable`1 values)
   at Plang.Compiler.Backend.PVerifier.PVerifierCodeGenerator.ExprToString(IPExpr expr) in /home/runner/work/P/P/Src/PCompiler/CompilerCore/Backend/PVerifier/Uclid5CodeGenerator.cs:line 2025
   at System.Linq.Enumerable.SelectArrayIterator`2.MoveNext()
   at System.Linq.Enumerable.ZipIterator[TFirst,TSecond](IEnumerable`1 first, IEnumerable`1 second)+MoveNext()
   at System.Linq.Enumerable.SelectEnumerableIterator`2.MoveNext()
   at System.String.Join(String separator, IEnumerable`1 values)
   at Plang.Compiler.Backend.PVerifier.PVerifierCodeGenerator.NamedTupleExprHelper(NamedTupleExpr t) in /home/runner/work/P/P/Src/PCompiler/CompilerCore/Backend/PVerifier/Uclid5CodeGenerator.cs:line 2121
   at Plang.Compiler.Backend.PVerifier.PVerifierCodeGenerator.ExprToString(IPExpr expr) in /home/runner/work/P/P/Src/PCompiler/CompilerCore/Backend/PVerifier/Uclid5CodeGenerator.cs:line 2023
   at Plang.Compiler.Backend.PVerifier.PVerifierCodeGenerator.GenerateStmt(IPStmt stmt, Machine specMachine, List`1 goals, Boolean generateSanityChecks) in /home/runner/work/P/P/Src/PCompiler/CompilerCore/Backend/PVerifier/Uclid5CodeGenerator.cs:line 2001
   at Plang.Compiler.Backend.PVerifier.PVerifierCodeGenerator.GenerateStmt(IPStmt stmt, Machine specMachine, List`1 goals, Boolean generateSanityChecks) in /home/runner/work/P/P/Src/PCompiler/CompilerCore/Backend/PVerifier/Uclid5CodeGenerator.cs:line 1725
   at Plang.Compiler.Backend.PVerifier.PVerifierCodeGenerator.GenerateGlobalProcedures(IEnumerable`1 functions, List`1 goals, Boolean generateSanityChecks) in /home/runner/work/P/P/Src/PCompiler/CompilerCore/Backend/PVerifier/Uclid5CodeGenerator.cs:line 1373
   at Plang.Compiler.Backend.PVerifier.PVerifierCodeGenerator.GenerateMain(Machine machine, State state, Event event, ProofCommand cmd, Boolean generateSanityChecks) in /home/runner/work/P/P/Src/PCompiler/CompilerCore/Backend/PVerifier/Uclid5CodeGenerator.cs:line 1144
   at Plang.Compiler.Backend.PVerifier.PVerifierCodeGenerator.CompileToFile(String name, ProofCommand cmd) in /home/runner/work/P/P/Src/PCompiler/CompilerCore/Backend/PVerifier/Uclid5CodeGenerator.cs:line 473
   at Plang.Compiler.Backend.PVerifier.PVerifierCodeGenerator.GenerateCode(ICompilerConfiguration job, Scope globalScope) in /home/runner/work/P/P/Src/PCompiler/CompilerCore/Backend/PVerifier/Uclid5CodeGenerator.cs:line 362
   at Plang.Compiler.Compiler.Compile(ICompilerConfiguration job) in /home/runner/work/P/P/Src/PCompiler/CompilerCore/Compiler.cs:line 89
   at Plang.CommandLine.RunCompiler(String[] args) in /home/runner/work/P/P/Src/PCompiler/PCommandLine/CommandLine.cs:line 144
   at Plang.CommandLine.Main(String[] args) in /home/runner/work/P/P/Src/PCompiler/PCommandLine/CommandLine.cs:line 40

I am using Ubuntu 26.04 with the following software versions:

$ java --version
openjdk 11.0.31 2026-04-21
OpenJDK Runtime Environment (build 11.0.31+11-post-1ubuntu1-26.04.2-Ubuntu)
OpenJDK 64-Bit Server VM (build 11.0.31+11-post-1ubuntu1-26.04.2-Ubuntu, mixed mode, sharing)

$ dotnet --version
8.0.127

$ uclid --help
uclid 0.9.5

$ git branch 
* dev_p3.0/pverifier

$ p --version
P version 3.0.4.0

[daniel-larraz]

It seems that the version in Tutorial/2_TwoPhaseCommit is not compatible with PVerifier; only the versions in Tutorial/Advanced/2_TwoPhaseCommitVerification/ are. I suggest updating the "Get the Two-Phase Commit Example Locally" section of the "Using PVerifier" page to point to the correct version of the example.

I will leave this issue open in case you would like to address it.