2 ms·

Perhaps best answered by: http://alloytools.org/faq/how_does_the_alloy_analyzer_differ_from_model_checkers.html http://alloytools.org/faq/how_does_the_alloy_ana

by hcs 7y ago

Perhaps best answered by: http://alloytools.org/faq/how_does_the_alloy_analyzer_differ_from_model_checkers.html http://alloytools.org/faq/how_does_the_alloy_analyzer_differ... It's more about data structures and testing every variation up to a fixed maximum size.

hwayne 7y ago
It's worth pointing out that Jackson wasn't specifically thinking of TLA+ when he wrote that. In _Software Abstractions_ he compares Alloy to B, OCL, VDM, and Z. TLA+ is very different from all of those, just as Alloy is. At some point in the future I'm supposed to write an in-depth comparison, though documentation work is higher priority right now.
- hcs 7y ago
  Thanks! I've only really been through the tutorials of each, I'm glad to read about your experience upthread.