$e - meaning?

Moderator: Automated Software Engineering

Toobee
Sonntagsinformatiker
Sonntagsinformatiker
Beiträge: 225
Registriert: 7. Apr 2011 12:58

$e - meaning?

Beitrag von Toobee »

Hi,

what is the meaning of this "$e" in alloy (see screen).
Dateianhänge
pic.jpg
pic.jpg (54.35 KiB) 258 mal betrachtet

Benutzeravatar
ericbodden
Sonntagsinformatiker
Sonntagsinformatiker
Beiträge: 243
Registriert: 5. Apr 2010 19:06

Re: $e - meaning?

Beitrag von ericbodden »

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
Sonntagsinformatiker
Beiträge: 268
Registriert: 15. Nov 2006 21:41

Re: $e - meaning?

Beitrag von tgp »

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.

Antworten

Zurück zu „Automated Software Engineering“