Search code examples
predicatesignaturealloypredicates

Alloy - Count atoms used by other atoms

I'm trying to notice a change in atom relations to other atoms. Using the below signatures :

    sig Word, Definition{}

    sig Dictionary {
        def: Word -> lone Definition
    }

I then use a predicate to show what happens when you add a new relation to a Dictionary by having another Dictionarywhich is the same but with one more relation.

    pred addRelation [d,d':Dictionary,w:Word,f:Definition] { 
        d'.word = d.word + w -> f 
    }

To see if the number of Word atoms used by the first Dictionary increase I can show only the instances where this occurs using:

    #d'.def.Definition > #d.def.Definition

However, is there a way to see if the number of Definition atoms used by the second Dictionary atom has increased? I've been using trial and error in the Alloy Evaluator to try and find a value for this but have come up short.

Thanks!

Solution

  • Like this?

    sig Word, Definition{}

sig Dictionary {
    def: Word -> lone Definition
}

pred addRelation [d,d':Dictionary,w:Word,f:Definition] { 
    d'.def = d.def + w -> f 
    #d'.def[Word] > #d.def[Word]
}
run addRelation