Is it possible to check refinement?

[nano-o]

Hello, in the Client Server example of the P tutorial, AbstractBankServer is supposed to be an abstraction of the composition of BankServer and Database. Is it possible to test whether every behavior produced by the composition of BankServer and Database is also a behavior of AbstractBankServer?

In the ModP paper, there is a refines keyword. So, I tried the following:

test tcSingleClientRefinement [main=TestWithSingleClient]:
  (union Client, Bank, { TestWithSingleClient }) refines (union Client, AbstractBank, { TestWithSingleClient });

Which fails with:

Parsing ..
Type checking ...
<Internal Error>:
 The method or operation is not implemented.
<Please report to the P team (p-devs@amazon.com) or create an issue on GitHub, Thanks!>
   at Plang.Compiler.TypeChecker.ModuleSystemTypeChecker.CheckRefinementTest(RefinementTest test) in /home/runner/work/P/P/Src/PCompiler/CompilerCore/TypeChecker/ModuleSystemTypeChecker.cs:line 176
   at Plang.Compiler.TypeChecker.Analyzer.AnalyzeCompilationUnit(ITranslationErrorHandler handler, ProgramContext[] programUnits) in /home/runner/work/P/P/Src/PCompiler/CompilerCore/TypeChecker/Analyzer.cs:line 94
   at Plang.Compiler.Compiler.Compile(ICompilationJob job) in /home/runner/work/P/P/Src/PCompiler/CompilerCore/Compiler.cs:line 30
   at Plang.Compiler.CommandLine.Main(String[] args) in /home/runner/work/P/P/Src/PCompiler/CommandLine/CommandLine.cs:line 25

[ankushdesai]

In the most recent version of P, we have disabled refinement checking.
We will be soon releasing an upgraded version of the refinement checker.

[parryac]

Hello, when checking the example in the original post here I still get the same error. So it seems like the updated refinement checker has not been released yet or is not enabled. Is that correct? If so, is there a plan for releasing a new refinement checker in a future version of P? Thanks.

[nano-o]

Okay, thanks. Looking forward to the new release!