Alloy Community

User login

  • : Function ereg_replace() is deprecated in /afs/csail.mit.edu/proj/alloy/www/data/community/sites/all/themes/Aeon5/advforum/forum-thread.tpl.php on line 25.
  • : Function ereg_replace() is deprecated in /afs/csail.mit.edu/proj/alloy/www/data/community/sites/all/themes/Aeon5/advforum/forum-thread.tpl.php on line 26.
  • : Function ereg_replace() is deprecated in /afs/csail.mit.edu/proj/alloy/www/data/community/sites/all/themes/Aeon5/advforum/forum-thread.tpl.php on line 27.
  • : Function ereg_replace() is deprecated in /afs/csail.mit.edu/proj/alloy/www/data/community/sites/all/themes/Aeon5/advforum/forum-thread.tpl.php on line 28.
  • : Function ereg_replace() is deprecated in /afs/csail.mit.edu/proj/alloy/www/data/community/sites/all/themes/Aeon5/advforum/forum-thread.tpl.php on line 29.
  • : Function ereg_replace() is deprecated in /afs/csail.mit.edu/proj/alloy/www/data/community/sites/all/themes/Aeon5/advforum/forum-thread.tpl.php on line 30.
  • : Function ereg_replace() is deprecated in /afs/csail.mit.edu/proj/alloy/www/data/community/sites/all/themes/Aeon5/advforum/forum-thread.tpl.php on line 31.
  • : Function ereg_replace() is deprecated in /afs/csail.mit.edu/proj/alloy/www/data/community/sites/all/themes/Aeon5/advforum/forum-thread.tpl.php on line 32.
  • : Function ereg_replace() is deprecated in /afs/csail.mit.edu/proj/alloy/www/data/community/sites/all/themes/Aeon5/advforum/forum-thread.tpl.php on line 33.
  • : Function ereg_replace() is deprecated in /afs/csail.mit.edu/proj/alloy/www/data/community/sites/all/themes/Aeon5/advforum/forum-thread.tpl.php on line 34.

Suggestion: add forum on gotchas, simple but mystifying errors, etc

 
Posted on: Thu, 03/25/2010 - 08:48
cmsmcq's picture
Joined: 2008-07-25
Points: 77
User is offline
Suggestion: add forum on gotchas, simple but mystifying errors, etc
A forum for common / understandable mistakes?

Would it be helpful to have a forum (or perhaps a section in the FAQ) to which users of Alloy could contribute accounts of problems which proved eventually to have a simple solution, but which appeared mystifying at first because of some mismatch between the user's mental model and what was actually happening?  I'm thinking of suggesting a forum title like "Burn marks" (things that users have been burned by) or "D'oh!".

On the positive side, it would make it possible to derive some benefit for others from the kind of error that (when you finally understand it) makes the user cry "D'oh!" and hit themselves on the forehead.  (On the negative side, I suppose it risks suggesting to newcomers that Alloy is full of traps and tricky bits.)

Candidates from my own experience and from recent reading in the archives:

- The # operator usually gives the cardinality of a set, but will take other values (including negative values) in cases of arithmetic overflow.

- Statements of the form all x : X | 1 = 2 are not always held false:  if the instance has no atoms in signature X, it doesn't matter what follows the bar.  (This can prove baffling if you're careless about the scope of the quantification.)

- The reflexive transitive closure of any relation includes the full identity relation; this can lead to counter-intuitive failures to find any instances of what look like simple models, such as

sig Node {}
one sig globals { r, s : Node -> Node }{ s = *r }
run {}


This proves to have no instances because s is constrained to include iden as a subset, which would violate its type signature Node -> Node.  If r and s are declared univ > univ, the model does have instances.  

The fact that * includes "irrelevant" tuples is discussed in Software Abstractions, but this one still caught me by surprise today, and took a couple hours to figure out.  Mostly you can ignore the irrelevant tuples, and so mostly you can safely act as if it magically added only relevant tuples.

It might be nice if there were a place to report on such things, so that those of us who are at wits' end trying to diagnose some problem can read them and either find help or at least find comfort in thinking other people occasionally have trouble, too.

Syndicate content  

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