Issue visualizing skolem funs with past operators

[nmacedo]

When considering past operators, the value of expressions may change depending on which loop unrolling it is being evaluated. Instances in the visualizer only have the value of the prefix (and the looping state), and skolem functions are statically calculated and registered in the prefix. If a function has past operators, and its value changes depending on the loop unrolling, it will always show in the visualizer its value in the first unrolling.

Minimal example:

some var sig A {}
run {always A = A'}

fun x : A {
    { a:A | not before a in A }
}

Function x is equal to A in the first unrolling, but empty in the remaining, but it always appear as A in the visualizer.

PS: the evaluator works fine since the values are calculated dynamically.

[alcinocunha]

I think the behaviour with skolem functions should be the same as if they were declared as signatures or fields. In this case we should have the same behaviour as if the model was

some var sig A {}
run {always A = A'}

var sig x in A {}
fact { always x = { a:A | not before a in A } }

which works fine.

To implement this correctly we need to compute the maximum depth of past operator nesting in all the skolems (in this case it is 1) and unroll the trace in the generated instance that many times, so that we make enough states distinct in the prefix for the past formulas to make sense. I'm not sure how easy it is to implement this?

[nmacedo]

I'm having a lot of trouble fixing this. I see two options:

• We assume the skolem functions are part of the trace, and unroll the trace accordingly when processing the Pardinus trace into XML for the visualizer. This option is easy to implement, but may perhaps give surprising solutions. For instance, in the example above the Pardinus trace has a single looping state, but after unrolling it will show as follows. A consequence is that solutions may no longer be provided with increasing length. Maybe I can try to use the original state identifiers in the visualizer, so that it at least just shows transitions between state 0?

• We assume that skolem functions are not part of the trace, do not unroll the trace for the visualizer, and dynamically calculate the value of those functions when navigating the trace in the visualizer. While this seems simple in principle, the instance visualization and the evaluator are completely disconnected, and neither has access to the definition of the skolem functions, so I can't find an elegant way to implement this.

[nmacedo]

Ok, new plan: I unroll the trace at the XML level, but register information about the original trace. So in the example above, even though the value of the skolem function changes, it would still show like this:

So the user still sees the instance as minimal, in the sense that the trace shows only a state 0. The only tradeoff is that the XML get a bit messy: the header says it's a trace with a single instance, but it actually contains two distinct states.

[nmacedo]

Richer example for illustration: original trace has two states looping to the first, value of the skolem changes at the third state.

var sig A { var r : A }

run {
    always A = A' 
    always r != r' }

fun x : A {
    { a:A | not before (before a in A) }
}

[alcinocunha]

The proposed solution looks great!