CODEWITHSUNDEEP
alloy
Loïc Gammaitoni
Loïc Gammaitoni

Reputation: 4171

express equivalence between several instances

Suppose I have a sig A in my module that is related to a sig B.

Imagine now that we have the several instances :

A$1 -> B$1   , A$2 -> B$2

and

A$1 -> B$2   , A$2 -> B$1

I would like to express that B$1 and B$2 are equivalent (under certain conditions) such that only this instance would be generated A$1 -> B , A$2 -> B.

One of the solution might be to use the keyword "one" while declaring the sig B, but it won't work in my case, because B have several fields, making B atoms not necessarily equivalent . In short 2 atoms are equivalent only if they have their fields of same values.

Ideally I would like to remove the numbering for B. but still be able to have several atoms B .

Upvotes: 3

Views: 134

Answers (2)

C. M. Sperberg-McQueen
C. M. Sperberg-McQueen

Reputation: 25054

First you say that the two instances you describe are equivalent, although at a superficial level they appear to have distinct values for A$1 and A$2. Then you say "2 atoms are equivalent only if ... their fields [have the] same values". If that's the definition of equivalence, then your two instances are not equivalent; if your two instances are equivalent, then your definition is not capturing what you want.

It sounds as if you mean (1) that B atoms are either (1a) always equivalent, or (1b) equivalent under certain circumstances, and (2) that A atoms are equivalent if their fields all have values which are either identical or equivalent. And as if you want to prohibit equivalent A atoms. If that's so, then your jobs are:

  • Define a predicate that is true for two B elements if and only if they are equivalent.
  • Define a predicate for two A elements that is true if and only if they are equivalent.
  • Define a predicate (or a fact) that specifies that no two A atoms in the instance are equivalent.

If your problem is just that the Analyzer is showing you instances of the model which are not interestingly distinct from each other, then see Aleksandar Milicevic's response.

Upvotes: 1

Aleksandar Milicevic
Aleksandar Milicevic

Reputation: 3867

The Alloy Analyzer doesn't give you much control over how the subsequent instances are generated (or how to break symmetries), so you typically have to work around those issues at the model level.

For your example, maybe this is the right model

sig B{}

one sig BA extends B {}

sig A {
  b: one BA
}

run { #A=2 }

Upvotes: 4

Related Questions