debugging chained relation declaration in alloy

Question

I am using Alloy to model graph transformation. I specify my transformation as different transformations which are applied to different part of the graph. So I have a signature :

sig Transformation {
    nodes : some Node,
    added_node : one Special_Node
}

To apply this transformation I declare 3 relations in the fact part of the signature which apply to different part of the graph. The left part of a relation is related to the input graph and the right side to the output graph :

some mapping_rel0_nodes : rel0In one -> one rel0Out|{
    C1 && C2 && C3 
}
&&
some mapping_rel1_nodes : rel1In   ->  some (rel1Out+special_Node) | {
    C1' && C2' && C3'
}
&&
some mapping_rel2_nodes : rel2In   ->  some (rel2Out+special_Node) |{
    C1'' && C2'' && C3''
} && 
 out.nodes <: connections = ~mapping_rel2_nodes.inpCnx.mapping_rel2_nodes +
                            ~mapping_rel1_nodes.inpCnx.mapping_rel1_nodes +
                            ~mapping_rel0_nodes.inpCnx.mapping_rel0_nodes

Each relation applies to disjoint different part of the graph, but they are connected by connections between them. The CX, CX' and CX'' are constraints applied on the relations. A Node has the following signature :

sig Node{
    connections : set Node
}{
    this !in this.@connections
}

To obtain the new connection I take all the connections in the input graph inpCnx and use the mapping obtained for each point to get the associated connections in the new graph.

My questions are :

• Do mapping_relX_nodes are still known at his step of the fact?
• When I control them in the evaluator and i do the operation manually on the appropriate instance it works, but expressed as fact, it returns no instances. I read this post and I was wondering if there are other tools to control the expression and variable, like debug print or else?
• The relations have the same arity, but the rel0 is bijective and the others are just binary relation. Is there any constraint due to the bijectivity of rel0 that the union of these relations has to be bijective?
• In my experience in the evaluator, when there is a duplication of a tuple, one of it is deleted : {A$0->b$0, A$0->B$0} becomes {A$0->B$0}. But sometimes it could be needed to keep it both, is there any way to have it both?

Thanks in advance.

Answer 1

You ask:

Do mapping_relX_nodes are still known at his step of the fact?

Without a full working model to test, it's hard to give an absolutely firm answer. But Alloy is purely declarative, and the uses of mapping_rel1_nodes etc. do not appear to be local variables, so the references in the fourth conjunct of your fact will be bound in the same way as the references in the other conjuncts. (Or not bound, if they are not bound.)

When I control them in the evaluator and i do the operation manually on the appropriate instance it works, but expressed as fact, it returns no instances. I read this post and I was wondering if there are other tools to control the expression and variable, like debug print or else?

Not that I know of. In my experience, when something seems to work as expected in the evaluator but I can't get it to work in a fact or predicate, it's almost invariably a failure on my part to get the semantics of the fact or predicate correct.

The relations have the same arity, but the rel0 is bijective and the others are just binary relation. Is there any constraint due to the bijectivity of rel0 that the union of these relations has to be bijective?

No (not unless I am totally misunderstanding your question).

In my experience in the evaluator, when there is a duplication of a tuple, one of it is deleted : {A$0->b$0, A$0->B$0} becomes {A$0->B$0}. But sometimes it could be needed to keep it both, is there any way to have it both?

Yes; Alloy works with sets. (So the duplicate is not "deleted" -- it's just that sets don't have duplicates.) To distinguish two tuples which would otherwise be identical, you can either (a) add another value to the tuple (so pairs become triples, triples become 4-tuples, and n-tuples become tuples with arity n+1), or (b) define a signature for objects representing the tuples. Since members of signatures have object identity, rather than value identity, they can be used to distinguish different occurrences of pairs like A$0->B$0.