Skolemization results on Table View

[ferhaterata]

Hi Peter,

Thank you for introducing 'compact' tables to the Alloy community. I think they are extremely useful.

It would be great if the table view could also show tuples coming from skolemization. Have you considered this before?

In fact, while enumerating instances in the solution space using the table view, several models might look isomorphic to the user if the skolem values are different but the rest of the instances are the same.

In the following, I listed several observations:

• In some scenarios, skolem values greatly help to identify the reason of the state changes as being witnesses. For instance, in the following instance, we can infer that three consecutive 'add' operations are simulated. However, inferring types for skolem tuples might be cumbersome in order to compactly append them to the existing tables. In this example, first skolem function has this definition, $traces_n1: (Book-last) -> one Name ; and the second function, $traces_t1: (Book-last) -> one Target.

• In the following example, the formula which is subject to skolemization is: {some p: Process | p.elected != none}. There is no skolem function (no universal quantifier in the context), instead, skolomization produces a skolem constant, it is a unary relation wrt Alloy semantics, whose type is: $show_p: one Process, and the result is a singleton, skolem $show_p={Process$2}. Here my visualization suggestion:

• As an illustrative example, please find in the following a simple Stack Data Structure specification.

open util/ordering [Stack] as StackOrder

sig Stack{
    nodes: set Node,
    top: lone nodes,
    nextNode: Node -> lone Node,
    action: lone Action
}{
    all disj n1, n2: nodes | one n1.nextNode and one n2.nextNode => n1.nextNode != n2.nextNode

    all n: Node - nodes | no n.nextNode and no nextNode.n

    all n: nodes | n in top.*nextNode

    no n: nodes | n in n.^nextNode
}

sig Node{}

enum Action {push, pop}
------------------------------------------------------------

pred push[s, s': Stack, n: Node]{
    s'.nodes = s.nodes + n
    s'.nextNode = s.nextNode + (n -> s.top)
    s.action = push
}

pred pop[s, s': Stack]{
    s'.nodes = s.nodes - s.top
    s'.nextNode = s.nextNode - (s.top -> s.top.(s.nextNode))
    s.action = pop
}

fun getTop [s: Stack]: lone Node { s.top } 

------------------------------------------------------------

pred init[s:Stack]{
    no s.nodes
}

fact{ no StackOrder/last.action}

//deterministic
fact traces{
    init[StackOrder/first]
    all s: Stack - last | 
        some n: Node |
            push[s, s.StackOrder/next, n] or pop[s, s.StackOrder/next]
}

------------------------------------------------------------
run {} for 4 

------------------------------------------------------------
check pushAndPopOkay{
    all s, s', s'': Stack, n: Node - s.nodes | 
        push[s, s', n] and pop[s', s''] 
            => s.nodes = s''.nodes and s.top = s''.top
} for 7 but 3 Stack
------------------------------------------------------------
check popEmptyStackOkay{
    all s, s':Stack | pop[s, s'] and init[s] implies init[s']
} for 3 but 3 Stack
------------------------------------------------------------
check popReturnsAlwaysTop{
    all s, s' : Stack | pop[s, s'] and !init[s] implies no getTop[s].(s.nextNode)
} for 3 but 2 Stack
-----------------------------------------------------------

It can be visualized like this:

Does this make sense? Do you think that this approach can be generalized for all skolemization cases?

Cheers,

Ferhat

[nmacedo]

Added for 6.2. Note that skolem vars cannot be associated to a sig table since they may relate atoms from different sigs. So I've introduced a new table for each skolem var.

[pkriens]

so this is done?