Skip to content

Navigation Menu

Sign in
Appearance settings
Sign in
Sign up
Appearance settings
Discussion options

nano-o
May 19, 2022

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
You must be logged in to vote

Replies: 2 comments · 1 reply

Comment options

ankushdesai
May 20, 2022
Maintainer

In the most recent version of P, we have disabled refinement checking.
We will be soon releasing an upgraded version of the refinement checker.
You must be logged in to vote
1 reply
@parryac
Comment options

parryac Jul 17, 2023

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.
Comment options

nano-o
May 20, 2022
Author

Okay, thanks. Looking forward to the new release!
You must be logged in to vote
0 replies
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Category
🙏
Q&A
Labels
Question Question! Information
3 participants
@nano-o @ankushdesai @parryac
Converted from issue

This discussion was converted from issue #429 on November 29, 2022 17:57.

Morty Proxy This is a proxified and sanitized view of the page, visit original site.