Discussions

• 1 You must be logged in to vote

  🙏

  Is Theorem keyword a synonym for Lemma in PVerifier?

  dasblinkenlight asked Feb 7, 2026 in Q&A · Answered

  

  

  1
• 2 You must be logged in to vote

  🙏

  How to model transient network/service failures with eventual success (TLA+ fairness equivalent)?

  GilbertBckr asked Jan 14, 2026 in Q&A · Unanswered

  

  

  0
• 3 You must be logged in to vote

  🙏

  How was solved the "conformance problem" in the AWS s3 implementation?

  gabrielgiussi asked Apr 14, 2023 in Q&A · Unanswered

  

  

  

  

  3
• 1 You must be logged in to vote

  🙏

  Modeling a shared sense of time

  nigelkerr asked Jul 15, 2025 in Q&A · Unanswered

  

  

  0
• 1 You must be logged in to vote

  🙏

  Does the new statement introduce a scheduling point?

  dotnwat asked Aug 24, 2024 in Q&A · Answered

  

  

  

  

  2
• 1 You must be logged in to vote

  🙏

  Semantics of send to halted machines

  rajivr asked Jun 28, 2025 in Q&A · Answered

  

  

  1
• 1 You must be logged in to vote

  📣

  Please ask any questions related to P here!

  ankushdesai announced Sep 22, 2021 in Announcements

  

  

  1
• 1 You must be logged in to vote

  🙏

  Why P assumes send are reliable?

  gabrielgiussi asked Oct 20, 2023 in Q&A · Answered

  

  

  1
• 1 You must be logged in to vote

  💬

  Is the latest version of P still "interpreting its operational semantics in the explicit-state model checker Zing"?

  AnDongLi started Oct 23, 2024 in General

  

  

  0
• 1 You must be logged in to vote

  🙏

  A FIFO queue per machine, or per pair of machines?

  dotnwat asked Aug 31, 2024 in Q&A · Unanswered

  

  

  0
• 1 You must be logged in to vote

  🙏

  machine references vs identifiers

  dotnwat asked Aug 11, 2024 in Q&A · Answered

  

  

  2
• 2 You must be logged in to vote

  🙏

  Module not closed. test module is not closed with respect to created interfaces; interface ABC is created but not implemented inside the module

  dhruvin5 asked Jun 12, 2024 in Q&A · Unanswered

  

  

  0
• 2 You must be logged in to vote

  🙏

  GuaranteedWithDrawProgress in Tutorial 1 is inaccurate/misdocumented

  hwayne asked Jan 16, 2023 in Q&A · Unanswered

  

  

  

  

  6
• 2 You must be logged in to vote

  🙏

  Difference between hot, warm?, hot states in monitors

  nvartolomei asked May 22, 2024 in Q&A · Unanswered

  

  

  0
• 1 You must be logged in to vote

  💡

  Grammar railroad diagram

  Information

  mingodad started Jan 6, 2023 in Ideas

  

  

  2
• 1 You must be logged in to vote

  🚀

  Emacs support for editing P files

  rudi started Nov 21, 2022 in Feature Request!

  

  

  3
• 4 You must be logged in to vote

  🙏

  Modeling Message Reordering

  dasblinkenlight asked Dec 30, 2023 in Q&A · Unanswered

  

  

  0
• 1 You must be logged in to vote

  💬

  Some feedback after trying P

  gabrielgiussi started Oct 27, 2023 in General

  

  

  1
• 2 You must be logged in to vote

  🚀

  Feature request: machine-local types

  Feature Request Feature Request or Enhancement

  toddlipcon started Nov 13, 2023 in Feature Request!

  

  

  1
• 1 You must be logged in to vote

  🙏

  Fair and unfair schedules

  fintara asked Nov 8, 2023 in Q&A · Unanswered

  

  

  0
• 1 You must be logged in to vote

  🙏

  "no viable alternative at input ..." for simple struct creation

  pcholakov asked Oct 3, 2023 in Q&A · Answered

  

  

  2
• 2 You must be logged in to vote

  🙏

  Liveness specification - cold vs hot state

  fintara asked Aug 8, 2023 in Q&A · Answered

  

  

  1
• 1 You must be logged in to vote

  🙏

  What grammar is used for P?

  greggirwin asked Jul 31, 2023 in Q&A · Answered

  

  

  7
• 2 You must be logged in to vote

  🙏

  Is it possible to check refinement?

  Question Question! Information

  nano-o asked May 19, 2022 in Q&A · Unanswered

  

  

  

  

  3
• 1 You must be logged in to vote

  💬

  Internal error when generating Java code

  Pozas91 started Feb 9, 2023 in General

  

  

  0