Codecov Report

Attention: Patch coverage is 90.64748% with 13 lines in your changes are missing coverage. Please review.

Project coverage is 78.91%. Comparing base (456a572) to head (22b8270).

@@            Coverage Diff             @@
##             main    #2864      +/-   ##
==========================================
+ Coverage   78.88%   78.91%   +0.03%     
==========================================
  Files         467      467              
  Lines       15959    15972      +13     
  Branches     2592     2556      -36     
==========================================
+ Hits        12589    12605      +16     
+ Misses       3370     3367       -3     

☔ View full report in Codecov by Sentry.
📢 Have feedback on the report? Share it here.

This isn't a full fix for #2863 yet: it only ensures primes are not added to assignments that occur within the body of the init predicate. For the general case, we need to ensure primes do not appear in any operator that is used by the init predicate.

We can solve that this way:

• A function referencedDeclarationNames : QuintOpDef => List[String] that gathers just the non-builtin operator names that are referenced within the body of the give operator definition.
• call referencedDeclarationNames on the init pred, then find all definitions with those names, and recurse on the results, until all results are exhausted (only empty lists returned)
• This should produce a list of all and only the operators that are used in the init pred, and it should be in topopological order.
• Set the isInit int the context (instead of doing it at

  apalache/tla-io/src/main/scala/at/forsyte/apalache/io/quint/Quint.scala

  Lines 790 to 792 in 22b8270

  	// If we are entering into the init predicate, mark that in the context
  	val ctx0 = ctx.copy(isInit = (op.name == quintInitName))
  	val (tlaInstruction, maybeName) = opDefConverter(op).run(ctx0)

  )
• Fold over those gathered operators with this context, using the same logic as

  apalache/tla-io/src/main/scala/at/forsyte/apalache/io/quint/Quint.scala

  Lines 815 to 817 in 22b8270

  	// Translate all definitions from the quint module
  	module.declarations
  	.foldLeft((Context.empty, accumulatedTlaDecls)) {

• Finally, set isInit to false, and the continue to process the rest of the declarations

Some additional care will need to be take about where the init-relevant operators are placed back into the sequence of converted operators, in case there other operators that refer to them, which must occur later. Placing the init-relevant operators after all variable declarations but before any others should be safe, since they are guaranteed not to refer to other operators.

Alternatively, a different strategy could be employed on the quint side to remove the need for this complexity, as suggested on #2863.

Unfortunately, I won't have time to complete this work, as I am losing my company access to github etc. now.

<3