Performance issue with a relatively small application domain

[grayswandyr]

Hi,
that’s a big model indeed!

@cdelg

In the first instance we got a “Capacity exceeded” warning when generating CNF. Even if we solved it with a refactoring, it is still a red flag as all is not yet implemented. Do you think that it is surprising or expected given the size of our models?

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?

I don’t know if this threshold can be changed: is it a specific limitation that could be addressed by simply switching from ints to longs in Kodkod source code?

@cdelg

A second issue is the time required to solve a simulation that involves multiple modules/concepts. When working module by module everything is fine, the problem arises when we merge/reuse them in the application file. A workaround is to compose 2 or 3 modules/concepts at a time, but is not really maintainable especially with the themes that cannot be modularized. Same question here, do you think it is expected? Or the models are poorly implemented maybe?

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.

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.

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.

Hope this helps.