合金元模型::定义局部状态和全局状态

Question

我们需要创建合金模型的元模型。我们对如何在模型中对全局和本地状态进行建模存在一些疑问。到目前为止我们已经有了这个模型：

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
}

问题是如何在这样的模型中对局部和全局状态进行建模？我们知道有什么区别以及如何在特定模型中对每个状态进行建模，但这是不同的。

Answer 1

由于您对元建模感兴趣，即对 Alloy 模型本身进行建模，因此模型签名对一个特定模型进行编码，并且与其关联的状态可以直接表示全局状态（即全局状态可以建模为与模型实例关联的状态）。本地状态又可以与 Signature 签名的实例相关联（这些实例又与 Model 的特定实例相关联）。实际上，这种方法可以被认为是查看更高“一级”的模型，其中模型不是顶级实体，而是签名的实例。 （这个问题相当笼统和模糊——我希望我对这个问题的理解是适当的，这回答了问题。）