Metamodels and TLA+

[Samuel Miller]

Hello,

Thank you to all the active participants in this group as I have learned a lot by reading exchanges. I am relatively new to formal methods and I am trying to understand how some concepts apply to TLA+.

I understand that TLC checks a model. We can write that model in TLA+ syntax. This model can belong to many different domains. 

A metamodel is a model of models. It seems like in TLA+ the metamodel is TLA+ operators and records/structures, which can then be used to create domain specific models in TLA or Pluscal. Things like invariants would apply at this level, where we are modeling properties of the model itself. We can create multiple models that either conform or violate those invariants. When we set up operators before creating the model, we are, in a way, creating a domain specific modeling language for the model.

Going one step further in the abstraction, the metametamodel of TLA+ seems to be math.

Is that a fair assessment of how these ideas might relate to TLA+? Am I misunderstanding something about the underlying concepts or TLA+? I tried researching how these concepts relate, but found little, and I'd be curious if TLA+ uses this coneptual framework or thinks about these ideas in a different way. 

Thank you!

Sam

[Samuel Miller]

I tried to investigate this a little further and ended up writing a blog post. I'm sure I got some things inaccurately, but I think meta-modeling is an interesting perspective to apply to TLA+.

https://medium.com/@thesammiller/meta-models-for-web-apis-in-tla-and-formula-bcb224efe5bf