如何创建 100% 声明式模型？

Question

我正在创建一个简单的网络模型。网络包含节点。节点发送和接收数据。

这是对网络建模的一种方法：每个节点都有一个 "data" 字段，表示该节点在时间 t 拥有的数据。每个节点还有一个"send"字段记录在时间t发送给其他节点的数据。

sig Node {
    data: Data -> Time,                   
    send: Data -> Node -> Time   
}

在 100% 声明性和 100% 强制性之间的范围内，我认为该签名不在 100% 声明性一侧。在我的第一段中，我没有提到节点具有数据存储，也没有提到保留发送数据的记录。

此外，"send" 不是动词吗？这不是表明该模型没有达到应有的声明性吗？声明式模型不应该只使用名词吗？

我希望我的模型处于范围的 100% 声明性端。为此，我必须简单说明 "is"。我们开始做吧！

什么是有节点：

sig Node {}

什么是在任意时刻t，一个节点有数据。

sig Node {
    data: Data -> Time
}

什么是网络在节点之间有电线。

sig Network {
    wire: Node -> Node
}

什么是数据 d 在时间 t 和 t' 之间在线路上...

让我到此为止。我勾勒出的第二种方法是否更具声明性？有没有一种更具声明性的方法？

如何以 100% 声明的方式对网络建模？

Answer 1

我认为您需要将模型的语义内容与其中使用的名称分开，这是一个问题。对我来说，声明性模型的本质是它记录了以逻辑表达的观察——可能是关于状态的，或者是关于像转换这样的动态事物的。另一种方法是操作模型，它通过建立原始动作序列来描述行为和状态。一个简单的例子：建模一个从集合中非确定性地挑选元素的动作。操作规范可能会按顺序处理集合，然后使用循环遍历集合，在每一步中抛硬币，并在抛硬币第一次出现正面时返回给定元素。这模拟了直观的操作描述："go through the elements of the set one at a time, and pick one to return"。声明性规范会简单地说返回值是集合的一个元素——没有其他需要说的。

关于您的特定模型中名称的使用，对我来说似乎更大的问题是名称是否直接传达了它们的含义。所以 send 对我来说不是一个很有帮助的名字；更好的是 sentAt.

如何创建 100% 声明式模型？

How to create a 100% declarative model?

alloy