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

Question

我们需要创建 Alloy 个模型的元模型。我们对如何在我们的模型中模拟全局和局部状态有一些疑问。到目前为止我们有这个模型：

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 模型本身，模型签名对一个特定模型进行编码，与之关联的状态可以直接表示全局状态（即全局状态可以建模为状态与 Model 的实例相关联）。反过来，本地状态可以与 Signature signature 的实例相关联（这些实例又与 Model 的特定实例相关联）。实际上，这种方法可以被认为是查看模型 "one level" 更高，其中模型不是 top-level 实体而是签名的实例。（这个问题很笼统和模糊——我希望我对这个问题的理解是恰当的，并且这回答了这个问题。）

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

Alloy metamodel :: define local state and global state

models

meta

alloy