Atom number has no semantic meaning.

In first order logic, given a set of unknowns variables A, B, C,
and a set of uninterpreted values V1, V2, V3.
If none of your formula directly refer to V1, V2, or V3,
then given a satisfying solution to your model,
I can systematically rename V1 to V2, and V2 to V1,
and I will still end up with a satisfying solution.

Starting in Alloy 4.1.10, we implement a few heuristics for
picking an intuitive numbering. If you have "open util/ordering[X]",
then we will try to number X0, X1, X2... in the order that they
appear in the numbering. Also, if signature X contains a "next" field
and we verified that it is a linear total ordering, then
we will try to number the atoms X0, X1, X2... in the order that
they appear in that field.

(Obviously this is just a heuristic that won't work all the time...
in particular, what if the user decided to open util/ordering[X]
and yet deliberately define a "X.next" field
that defines a different ordering?)

Bottom line is: atom numbering is arbitrary; we are trying to choose
a numbering that may make more intuitive sense to the user, but that is
purely provided as a convenience, and has no semantic difference whatsoever.

Sincerely,
Felix Chang
Alloy4 Developer

Atom number has no semantic meaning.


I get that but I just wanted to be sure that my understanding of the problem was right, i.e the fact that trains go "backwards" when projecting over TrainState comes from that arbitrary numbering, not from something wrong in my model. Can you confirm that?

If so, here are a few remarks:
- It would be great to document *explicitly* the heuristics you use, maybe in the Alloy web page, such as recognizing the identifier "next".
- Considering my model, I have TrainState0 mapped to $move_ts2 and TrainState1 mapped to $move_ts1. Would it be possible, as another heuristic, to try first mappings which are the smallest possible along the product ordering? That is, as (TrainState0, $move_ts1) is lower than (TrainState0, $move_ts1), it should be tried first. Or is it absolutely impossible because it depends on SAT engines which don't give a damn about atom names?
- More generally, It looks to me like it illustrates the consequence of not adding into Alloy specific constructs for dynamic modelling, akin to the DynAlloy proposition, but rather pushing for the modeling of dynamic systems using *design patterns* reminiscent of the situation calculus (modelling of instants, or of states, as in the Alloy book). Admittedly, this choice simplifies the language and gives room for various modelling styles. OTOH, introducing explicit dynamic constructs would perhaps enable a nicer numbering of atoms (but this is not good reason for making such a modification of the language) and most importantly would greatly simplify many models and enable the verification of strong temporal properties which are currently out of reach. This is all the more important if you think that the small scope hypothesis is  convincing on static models but maybe less for dynamic models where bad things could happen within reach of a rather large scope. Of course, these questions shouldn't be seen as a dispproval of Alloy: quite the contrary, they just reflect my fascination for what I consider to be essentially extremely good design choices for this language, which of course, as every fan, I would like to see further improved  :-)

Cheers

dc

> i.e the fact that trains go "backwards" when projecting over TrainState

Projection merely shows you the sequence as numbered by the atom
(the box underneath each diagram shows you what atom the projection is on)

I (or others) would have to carefully read your Alloy model to determine
if it correctly models your expected behavior, so I cannot say at this point
whether it is correct.  But projecting over a signature, say X, will
merely show you the diagrams associated with X0 and X1 and X2...

There is no going "backward" or "forward" implied by projection.
It merely shows you a set of n diagrams associated with X[0] to X[n-1]

>
> It would be great to document *explicitly* the heuristics you use
>

I do not believe so, because it then encourages the reliance on atom numbering,
rather than encourages people to get more comfortable with uninterpreted atom values.

Furthermore, formally guaranteeing the heuristics would prevent us from
improving the heuristics in the future.  For example, "Magic Layout" is not
formally specified in the user documentation, and we can adjust how it decides
when to project based on further research.

>
> product ordering... SAT engines which didn't give a damn...
>

The atom numbering comes *after* SAT solving.

In general, the SAT solving is the most expensive, slowest, and most memory intensive step,
so we wouldn't implement this if it complicates the problem that the SAT solver
has to solve.  Indeed, the SAT solver simply deals with a set of atoms (whose labels
are completely ignored).

When the SAT solver gives us a solution containing 3 X atoms and 2 Y atoms and 5 Z atoms
arranged in a certain way, then our heuristics kicks in and try to find a nice numbering
for the 3 X atoms and the 2 Y atoms...

So we can certainly develop more complicated schemes, though there definitely comes a
point of diminished returns, when the post-processing starts to take longer and longer
(since multiple heuristics could apply, and when one heuristic is applied it may
enforce a particular numbering scheme on a particular signature which then
prohibits another heuristic from being applied to another signature), so the post processing
might become a nightmare worthy of a SAT solver itself!

Your particular suggestion of product ordering is problematic, because the association
of two signatures is not necessarily obvious from a compiler looking at an Alloy model,
and the number of potentially-eligible pairs of signatures can be large.

Also, so far the most user confusion has come from projection, and we generally only project
over a single signature, so that means the most benefit for the user comes from
finding a good linear ordering for each signature, rather than finding an ordering for pairs of sigs.

>
> dynamic modeling
>

That is a separate discussion for another topic. Though many dynamic models are based
on linear time, and there is a very standard Alloy idiom of defining a "Time" or "Step" sig,
putting util/ordering on it, then writing a predicate to specify legal transitions
between each t and t.next.  When people follow this idiom for dynamic behavior,
then the heuristic of numbering util/ordering according to its order ensures the time atoms
will go from Time0 to Time_n-1.

Simply put, we've kept the language and tool completely state-less (thus logically simpler,
keeping the Alloy toolchain itself simpler, and also making the logic easier to prove / reason about),
while providing additional conveniences and benefits for the most common use cases.
It's a simple matter of optimizing for the most common cases.

Sincerely,
Felix Chang
Alloy4 Developer

Thansk for your answers.


There is no going "backward" or "forward" implied by projection.
It merely shows you a set of n diagrams associated with X[0] to X[n-1]


Yes I get the inner working.


Though many dynamic models are based
on linear time, and there is a very standard Alloy idiom of defining a "Time" or "Step" sig,
putting util/ordering on it, then writing a predicate to specify legal transitions
between each t and t.next. When people follow this idiom for dynamic behavior,
then the heuristic of numbering util/ordering according to its order ensures the time atoms
will go from Time0 to Time_n-1.


Sure but it implies mixing Time within the static model. Another idiom is discussed in the Alloy book p.175 where one considers a global notion of State, thus avoiding to mix static and dynamic aspects: as D. Jackson puts it, it is less object-oriented but it supports further detailing of states seamlessly. This is what I've done in my model and an annoying consequence is a numbering of States not necessarily coherent with the "next" field which operates on Segments, not on States.

Furthermore, many dynamic models may also rely on a partial, rather than linear, ordering.

Both these situations are not so uncommon and their handling through projection is not as user-friendly as with the OO idiom and an associated linear ordering.

--
David Chemouil
Research Scientist
ONERA/DTIM, Toulouse, France
http://www.onera.fr/staff/david-chemouil/

>
> Furthermore, many dynamic models may also rely on a partial,
> rather than linear, ordering.
>

Indeed, and now we've come full circle, and this is one of the
main strength I think Alloy has: it doesn't impose a specific
temporal semantics or event modeling idiom.  We can start
with a static model of just the domain objects and relationships,
and gradually refactor it or specialize it into different
dynamic models.

Modeling and solving in Alloy4, I think, are usually straightforward.

Visualizing the solution though is one place where I think the Alloy Analyzer 4 is weak at.
In fact, while the Alloy 4 language has gone through massive improvements over the last 3 years,
and many things can be written far more succinctly compared to using Alloy 3,
unfortunately Alloy 4 visualizer is exactly identical to Alloy 3 (except the "magic layout" button)!

Partly this lack of major progress is because our research group is focused on logic and
program analysis, and none of us have a background in user interface design or graphical layout.
Also, both Emina (creator of the underlying Kodkod engine) and I prefer to look at an Alloy solution
by looking at its textual or tree output directly, without using the graphical visualizer.
So arguably this also resulted in lack of progress towards a better graphical visualizer.
Hopefully others can chime in to help us figure out, for example, how to best present
a solution involving branching time, partially ordered events, etc.

Sincerely,
Felix Chang
Alloy4 Developer