Sigs

Sigs are the basic building block of any model in Forge. You can declare a sig in the following way:

sig <name> {
    <field>,
    <field> ...
}

Fields

Each field in a sig is declared using a name, the multiplicity (set, one, lone), and the type of the field, e.g. myField: set Atom. Each field is a relation where it is implicitly a cross-product between the sig and the type of the field. So,

sig Atom {
    myField: set Node -> Atom
}

makes a relation named myField that looks like Atom -> Node -> Atom.

The multiplicity of the field (set, one, or lone) lets you specify how many elements should be in each atom's field.

• set: a set of things - can have zero or more elements in it
• one: each atom will have only one element in it. This is the same as specifying all a: Atom | one a.myField
• lone: each atom will have zero or one elements in it. This is the same as specifying all a: Atom | lone a.myField

Extending

You can also extend sigs using the following syntax:

sig Cat {}
sig ActorCat extends Cat {}
sig ProgrammerCat extends Cat {}

This means that any atom that is a KittyBacon is also a Cat, so the Cat set includes all atoms of ActorCats, but the set ActorCat only contains ActorCats.

Extending also has an effect on bounds, in that atoms of ProgrammerCat will count as Cats as well in the bound. So, if we run the following:

run {} for 5 Cat, exactly 2 ActorCat, 2 ProgrammerCat

we expect to get instances with up to 5 Cats total, where 2 of them will always be ActorCats and 0-2 will be ProgrammerCats.

Note for Alloy users: Forge does not currently support in subset sigs; instead, you should create a helper sig with a field to emulate the subset. If you are unable to do this, please contact the Forge team.

Bounds on sigs

You can set some bounds on sigs immediately when defining them by doing the following:

one sig LonelyAtom {}
lone sig MaybeNotThereAtom {}

This enforces that there is the specified multiplicity of those atoms in the universe.