|
|
|
SearchNavigationUser login |
How does the Analyzer slice Alloy models
|
||||
The development of this site is supported by the National Science Foundation under Computing Research Infrastructure Grant No. 0707612.
Theme originally designed by Chris Herberte
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
I am an academic and I am working on evaluating some SAT algorithms on Alloy instances. I am also interested in reading a such technical paper.
Would you please let me know when yours would be available?
Sincerely,
Adriana Alexandru