Significado de la palabra clave 'privada' en Alloy? Significado de la declaración 'enum'?

Question

El Alloy 4 grammar permite declaraciones de firma (y algunas otras cosas) para llevar una palabra clave private. También permite Permitir a las especificaciones contienen declaraciones de enumeración de forma

enum nephews { hughie, louis, dewey } 
enum ducks { donald, daisy, scrooge, nephews } 

The language reference no (por lo que puedo decir) describir el significado de la palabra clave, ya sea private o la construcción enum.

¿Hay documentación disponible? ¿O están en la gramática como construcciones que están reservadas para futuras especificaciones?

Answer 1

Este es mi conocimiento no oficial de esas dos palabras clave.

enum nephews { hughie, louis, dewey } 

es semánticamente equivalente a

open util/ordering[nephews] as nephewsOrd 

abstract sig nephews {} 

one sig hughie extends nephews {} 
one sig louis extends nephews {} 
one sig dewey extends nephews {} 

fact { 
    nephewsOrd/first = hughie 
    nephewsOrd/next = hughie -> louis + louis -> dewey 
} 

La palabra clave private significa que si una firma tiene el atributo private, su etiqueta es privado dentro del mismo módulo. Lo mismo aplica para campos privados y funciones privadas.

Answer 2

Además de la respuesta aceptada anterior, me gustaría añadir algunas ideas útiles que vienen de una experiencia de una semana con la aleación en el enum s, en particular sobre las principales diferencias con sig estándar.

Si usa abstract sig + extend, obtendrá un modelo en el que hay muchos conjuntos que corresponden al mismo concepto. Tal vez un ejemplo podría aclararlo mejor. somthing supongo que como

sig Car { 
    dameges: set Damage 
} 

Usted tiene la opción de usar

abstract sig Damage {} 
sig MajorDamage, MinorDamage extends Damage {} 

vs

enum Damage { 
    MajorDamage, MinorDamage 
} 

En el primer caso podemos llegar wiht un modelo con diferentes átomos MinorDamage (MinorDamage0, MinorDamage1, ...) se asocian a Cars, mientras que en el segundo caso siempre tienes un MinorDamage al que pueden referirse diferentes Cars.

Podría tener sentido en este caso usar un formulario abstract sig + extend (porque puede decidir rastrear diferentes elementos de MinorDamage o MajorDamage).

Por otro lado, si usted quiere tener un currentState: set State, podría ser mejor usar un

enum State {Damaged, Parked, Driven} 

para mapear el concepto, con el fin de tener exactamente tres State en que cada Car puede referirse a . De esta forma, en el Visualizer, puede decidir proyectar su modelo en exactamente uno de los estados y resaltará todos los Car asociados a este estado. No se puede hacer eso con la construcción abstract + extend, por supuesto, porque al proyectar sobre MajorDamage0 se resaltará solo el Car asociado a ese Damage y nada más.

Por lo tanto, en conclusión, realmente depende de lo que tiene que hacer.

Además, tenga en cuenta que si usted tiene una enumeración compuesta por elementos X y ejecutar

run some_predicate for Y 

donde Y < X, aleación produce ningún caso en absoluto. Por lo tanto, en nuestro último ejemplo, no podemos tener un Y < 3.

Como última nota, las enumeraciones no siempre aparecen en el Visualizador si utiliza el botón Diseño Mágico, pero como dije anteriormente usted puede "proyectar" su modelo sobre la enumeración y cambiar entre los diferentes elementos de la enumeración.