Performance issue with a relatively small application domain

models
5

Hi,

AFAIK, this is due to the Kodkod/Pardinus representation of fields (= relations) as specific matrices. The CapacityExceeded exception occurs when there’s a relation with an arity a (notice that a var relation has a hidden “time” column counting +1) and a domain (= the set of all possible atoms, incl. integers taken from the Int sig) of cardinality d such that d^a > 2,147,483,647 (= MAX_INT) . You model has a domain of size 96 (!). So with a relation of arity 5, or a var relation of arity 4, you’re already above MAX_INT… Perhaps this is what you had in your model before refactoring?

This was exactly the case, thanks for the explanation.

Adding to Daniel’s answer: I fear this is to be expected due to the combination of a number of parameters: the number of atoms and relations, the number of var fields and sigs, the under-specification of goals (e.g. an eventually goal is less constrained than a more fixed scenario)… The main way to address this issue will, I guess, to decrease the size of the state space, by making your models as small and deterministic as possible: to do so, I suppose you should split the model in several smaller ones, depending on abstractions of other complex parts and try to reduce non-determinism.

I was afraid of this. I’m not working on a small tricky domain but on a simple and large one. Many aspects need to be added like access control and or other small modules, I was hoping to address them all at once.

Regarding univ , notice also that, in Alloy 6, it is the set of all atoms “existing in the current state”, not all atoms at all states. So I’m not sure all expressions you wrote using univ always mean what you think.

Thanks for mentioning this, I will double check.

Like Daniel, I’m a bit surprised by the idiom you’re using (with primes occurring sometimes at non-usual palces, as well as events referring to the past). This isn’t necessarily wrong but a bit hard to follow. We have some guidelines here and there that you may find useful.

Thanks for the links, I will definitely check them out.

Clément.

1 Like