# Performance issue with a relatively small application domain **URL:** \ **Category:** models\ **Created:** [April 8, 2022, 11:35am UTC](https://alloytools.discourse.group/t/performance-issue-with-a-relatively-small-application-domain/253 "2022-04-08T11:35:26Z")\ **Posts on this page:** 1\ **Showing post:** 3
**Author:** ![grayswandyr](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/grayswandyr/32/17_2.png) [@grayswandyr](https://alloytools.discourse.group/u/grayswandyr)\ **Post date:** [April 11, 2022, 4:47pm UTC](https://alloytools.discourse.group/t/performance-issue-with-a-relatively-small-application-domain/253/3 "2022-04-11T16:47:06Z")
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 `int`s to `long`s 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](https://alloytools.discourse.group/t/modelling-a-state-machine-in-electrum-towards-alloy-6/88) and [there](https://haslab.github.io/formal-software-design/) that you may find useful. Hope this helps. --- _[View the full topic](https://alloytools.discourse.group/t/performance-issue-with-a-relatively-small-application-domain/253)._