Is your feature request related to a problem? Please describe.
Considering the inputs
Signature:
p(x:int)
q(x:int)
Formula:
p(x) S[1,2] q(x)
Trace:
@1 q(1) q(2)
@1 p(1) p(3)
@2 p(1) p(2) p(3)
@5
The violation at time-point 0 does not point anywhere in the trace. Specifically, this happens because the corresponding proof (the PDT here is trivial) corresponds to VSinceOut 0. Such proofs (e.g., VPrevOutL, VPrevOutR, ...) do not contain subproofs and it is not yet clear how they should be presented.
Describe the solution you'd like
There should be an annotation somewhere pointing it out.
Describe alternatives you've considered
The annotation could potentially be included in the hovering table.
Additional context
No additional context.
Is your feature request related to a problem? Please describe.
Considering the inputs
The violation at time-point 0 does not point anywhere in the trace. Specifically, this happens because the corresponding proof (the PDT here is trivial) corresponds to
VSinceOut 0. Such proofs (e.g.,VPrevOutL,VPrevOutR, ...) do not contain subproofs and it is not yet clear how they should be presented.Describe the solution you'd like
There should be an annotation somewhere pointing it out.
Describe alternatives you've considered
The annotation could potentially be included in the hovering table.
Additional context
No additional context.