Hi,

Hi there.

Alloy is probably showing you a counter example, I guess. Here $e refers to the variable "e" in the security check predicate. Alloy is trying to show you that in this instance the marked node is referenced by "e" in that predicate. Does that answer your question? Eric -- Eric tgp Sonntagsinformatiker Beiträge: 268 Registriert: 15. Nov 2006 21:41 ### Re:$e - meaning?

I have the same elements, so my guess is:

This could be a result from skolemization. Since the arrow points from a company to an employee, i guess it belongs to the fact f1b2 (every company has some employee). If you specified this as something like "for all companies c there is some employee e...", "$e" is an example for that employee. Check the link above and also switch from the "Viz" solution drawing to the XML drawing. You should see something like "<skolem label="$e" ID="10">". Also: if you rename the "variable e" in the fact, the new name should be used in the generated solutions.

I think i specified the fact right, so my solution for this is: tell alloy not to draw these arrows – in the "Viz" solution drawing, click on "Theme", select the "\$e" relation, click "Show as arcs" and "Influence layout" until they are off.