On Sat, 5 Jul 2008, ikarus1983de wrote:
> I'm looking for some information (e.g. technical report) on how an
> Alloy model is reduced / sliced before the analysis.
>
> I know about the work on the Kato-Tool by Ilya Shlyakhter et. al. but
> up to my knowledge this isn't integrated into Alloy (or Kodkod) yet.
> Furthermore, I'd like to know if Alloy does stuff like "signature x is
> not used for check y, thus remove x for the analysis of y".
Dear Christian:
There is currently no technical report on Alloy4's translation yet,
but I will write it soon as part of my thesis.
To answer your question, since Alloy translates the user problem into
a single CNF problem, that means "each predicate call" adds to
the final CNF, and unused predicates are completely omitted.
Several optimizations include: 1) calls to the same predicates
with the same actual arguments are merged, so that if you call
the same predicate from multiple places in your model with the
same arguments, then the cost is borne only once. 2) Even between
two calls with different arguments, identical subformulas and
subexpressions are merged ("shared") to further reduce the cost.
Sincerely,
Felix Chang
Alloy4 Developer
