Open bugarela opened 5 months ago
The CounterExample
TLA+ value that is given to a -dumpTrace exporter supports lassos.
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.
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
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.
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.
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:
This is done by
Since this command will wrap the init, step and inv definitions, the
.cfg
file should always be something likeWe 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 thecompile
command (which depends on Apalache).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:
While a similar trace state in quint is simply:
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. https://github.com/tlaplus/tlaplus/issues/853#issuecomment-1858848122. 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).