Describe the temporal behavior the property should capture.
Recent prompts
Should the intended property accept these traces?
→ ↵
Diff
Candidates hidden
Trace Classification History
Final Formula
Traces that satisfy
Traces that don't
Where do these candidates come from?
These LTL formula candidates are generated by the language model you’ve enabled in VS Code.
PICK sends your description to that model and asks it to suggest several possible LTL formulas.
PICK then helps you choose between them by having you vote on which example traces should or should not be accepted. As you classify examples, incompatible candidates are eliminated.
If none of the candidates seem correct, we recommend refining the description above and generating a new set of options.