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.

[nano-o]

Okay, thanks. Looking forward to the new release!