Integration with TLC

[bugarela]

I've been thinking about and trying to use Quint with TLC for a while now, so here's an issue to track these thoughts/experiments.

First of all, we need to translate Quint to TLA+. We almost have that, with two pending issues:

• TLA+ pretty printer produces [] on empty tuples, which is invalid syntax apalache-mc/apalache#2875
• Assignments in quint init operators need to be unprimed apalache-mc/apalache#2863

This is done by

quint compile --target tlaplus file.qnt

Since this command will wrap the init, step and inv definitions, the .cfg file should always be something like

INVARIANTS
q_inv

INIT
q_init

NEXT
q_step

We can produce that automatically in Quint.

Then, we can invoke TLC pointing the lib path to Apalache libs, since the generated TLA+ module will depend on them. I found that the easiest way to do this is by using the TLC inside of apalache.jar, which is already automatically dowloaded by Quint in the compile command (which depends on Apalache).

java -Xmx4096m -cp ~/.quint/apalache-dist-0.44.10/apalache/lib/apalache.jar tlc2.TLC file.tla

However, the counterexample printed by TLC is hard to read, since it refers to things in the generated TLA+ spec, which don't map directly to the original Quint spec. For example, see this state from a tic tac toe spec:

State 6: <MoveX line 166, col 3 to line 176, col 23 of module tictactoe>
/\ board = << << [tag |-> "Occupied", value |-> [tag |-> "X", value |-> "U_OF_UNIT"]],
      [tag |-> "Occupied", value |-> [tag |-> "O", value |-> "U_OF_UNIT"]],
      [tag |-> "Occupied", value |-> [tag |-> "O", value |-> "U_OF_UNIT"]] >>,
   << [tag |-> "Empty", value |-> "U_OF_UNIT"],
      [tag |-> "Occupied", value |-> [tag |-> "X", value |-> "U_OF_UNIT"]],
      [tag |-> "Empty", value |-> "U_OF_UNIT"] >>,
   << [tag |-> "Empty", value |-> "U_OF_UNIT"],
      [tag |-> "Empty", value |-> "U_OF_UNIT"],
      [tag |-> "Occupied", value |-> [tag |-> "X", value |-> "U_OF_UNIT"]] >> >>
/\ nextTurn = [tag |-> "O", value |-> "U_OF_UNIT"]

While a similar trace state in quint is simply:

[State 5]
{
  board:
    Map(
      1 -> Map(1 -> Occupied(O), 2 -> Occupied(O), 3 -> Occupied(X)),
      2 -> Map(1 -> Empty, 2 -> Occupied(X), 3 -> Empty),
      3 -> Map(1 -> Occupied(X), 2 -> Empty, 3 -> Empty)
    ),
  nextTurn: O
}

So I'd like to parse something back from TLC in the quint tool, so we can show it back to the user as they expect. The first option that came to my mind was to generate ITF out of TLC, but I actually think that might be impossible with no type information, since ITF is typed. Now, I'm considering something like the example by Markus in this comment. tlaplus/tlaplus#853 (comment). We should be able to parse this into a Quint run, and then, from that run, produce a trace.

One important thing to consider is how to express lasso-shaped counterexamples for liveness properties, since this is probably the main use case for TLC (as Apalache's temporal property verification is not the most mature).

[lemmy]

The CounterExample TLA+ value that is given to a -dumpTrace exporter supports lassos.

[bugarela]

Yes! I mean, I don't know what to convert that to in the Quint counterexample formatting,as we don't have lassos there yet.

[konnov]

Yes! I mean, I don't know what to convert that to in the Quint counterexample formatting,as we don't have lassos there yet.

You could just print the index of the state that closes the loop

[bugarela]

Yes! I mean, I don't know what to convert that to in the Quint counterexample formatting,as we don't have lassos there yet.

You could just print the index of the state that closes the loop

I need to check how TLC provides this info, but I guess that's the ideal thing: print something similar to the TLC regular output "Look: State X". I don't expect this to be hard, I just haven't tried or thought about it enough.

[GonVas]

I've playing around with compiling quint into tla and then using tlc and I came across some issues (after un-primming the init operator):

Compiling tictactoe.qnt found in the examples yields the following error on these lines of code:

(*
  @type: ((<<Int, Int>>) => Bool);
*)
isEmpty(coordinate_184) ==
  CASE VariantTag((square(coordinate_184))) = "Empty"
      -> LET (*@type: ((UNIT) => Bool); *) __QUINT_LAMBDA2(id__179) == TRUE IN
      __QUINT_LAMBDA2(VariantGetUnsafe("Empty", (square(coordinate_184))))
    [] OTHER
      -> LET (*@type: ((a) => Bool); *) __QUINT_LAMBDA3(id__182) == FALSE IN
      __QUINT_LAMBDA3([])

On the last line:
"Unsupported expression type 'N_GenNonExpPrefixOp'"

Converting the prisioners.qnt also in the examples yields this error:

[
          (__quint_var0) EXCEPT
            ![p_103] =
              LET (*
                @type: ((Int) => Int);
              *)
              __QUINT_LAMBDA0(old_79) == old_79 + 1
              IN
              __QUINT_LAMBDA0((__quint_var0)[p_103])
        ]
      /\ switchBUp' := switchBUp

"Attempted to evaluate an expression of form P /\ Q when P was
a function of the form (d1 :> e1 @@ ... @@ dN :> eN)."

Also in quint if we have in an operator that defines the two vals with the same name it works fines in apalache but fails in TLA because of the same variable name.