Alloy metamodel :: define local state and global state

Question

We need to create a metamodel of Alloy models. We have some doubts about how to model global and local state inside our model. We have this model so far:

open util/ordering[Estado] as E

sig Estado{

}

//an alloy model is composed by a set of signatures
sig Model {
    sigs : set Signature
}

// each signature has name 
sig Signature {
    nameSig : one Name
}

sig Name {

}

sig Atom {
    nameAtom : one Name
}

sig Instance {
    atom : set Atom -> Estado,
    instance : set Estado
}

pred solve [m : Model, i : Instance, e : Estado] {
    -- every signature name must be different and they all should be part of the signatures
    (i.atom.e).(nameAtom) in (m.sigs).(nameSig)
}

pred valid[m : Model] {
    all n : Name | lone nameSig.n & m.sigs
}

pred invs [e : Estado]{
    -- every sig make part of the model
    all s : Signature | s in Model.sigs 
    all m : Model | valid[m]
    all m : Model, i : Instance | solve[m, i, e]
    all a : Atom | a in (Instance.atom).e 
}
-- invariants
fact invs1 {
    all e : Estado | invs[e]
}

----------------------------------------------------------------------------------
-- Será que estes predicados são sobre os atomos ou sobre as instancias?
----------------------------------------------------------------------------------

--pred mantemAtoms[e,e' : Estado, i : Instance]{
--  i.atom.e' = i.atom.e
--}

-- run { some e,e' : Estado, i : Instance | mantemAtoms[e, e', i] } for 3 but exactly 1 Model, exactly 2 Estado

--check addAtoms {
    --all e,e' : Estado, a : Atom, i : Instance | invs[e] and  addAtoms[e, e', a, i] => invs[e']
--}

pred addAtoms[e,e':Estado, a : Atom, i : Instance]{
    --pre
    a not in i.(atom.e)
    --pos
    atom.e' = atom.e + i -> a
    instance.e' = instance.e + i
    --frame
}

run { some e,e' : Estado, i : Instance,  a : Atom | addAtoms[e, e', a, i] }
for 3 but exactly 1 Model, exactly 2 Estado

--check addAtoms {
    --all e,e' : Estado, a : Atom, i : Instance | invs[e] and  addAtoms[e, e', a, i] => invs[e']
--}


pred excludeAtoms[e,e' : Estado, i : Instance]{
    --pre
    i in instance.e
    --pos
    atom.e'= atom.e - i -> i.(atom.e)
    instance.e' = instance.e - i
    --frame
}

The question is how to model the local and global state inside such a model? We know what are the differences and how to model each state in a specific model but this is different.

Answer 1

Since you are interested in metamodelling, i.e. modelling Alloy models themselves, the Model signature encodes one particular model and the state associated with it can directly represent the global state (i.e. global state can be modelled as state associated with an instance of Model). Local state, in turn, can be associated with instances of Signature signature (which are in turn associated with a particular instance of Model). Effectively, this approach can be thought of as viewing models "one level" higher, where a model is not a top-level entity but an instance of a signature. (The question is quite general and vague -- I hope my understanding of the question was appropriate and this answers the question.)