RTLWS: Modeling systems with Alloy
Posted Nov 8, 2012 10:13 UTC (Thu) by epa
Parent article: RTLWS: Modeling systems with Alloy
The analyzer in Alloy is exhaustive
I understood that the analysis is not 'exhaustive' in the sense that it will find any counterexample that exists. Instead you specify a maximum structure size to check against - a counterexample might be found with 4 elements, or 5 elements, but the larger the number of elements you test the longer it takes to run. I suspect, but do not know for sure, that the Alloy language is Turing-complete and therefore an exhaustive analysis would be impossible.
to post comments)