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.