您的主要问题是 Huth / Ryan 书的第二版似乎已于 2004 年出版，并且使用（不出所料）当时合金分析仪接受的语法，这（也不出所料）不完全是与当前版本的合金分析仪接受的语法相同。
因此，要在当前版本的分析器中运行它，您将必须了解 (a) 他们想要表达的内容 (b) 他们试图表达的当时当前的 Alloy 语法，以及(c) 当前的 Alloy 语法，足以将模型转换为当前语法。 （或者找到已经这样做的人。）幸运的是，Huth 和 Ryan 详细解释了他们使用的 Alloy 语法，因此对于熟悉 Alloy 4 的人来说，将模型转换为 Alloy 4 语法并不是一个困难的练习。
祝你好运！
[后记] 理论上，你的作业目标是让你熟悉合金分析仪，而不是因为要求翻译旧合金而让你陷入困境对于新的 Alloy 语法，我将 Huth / Ryan PDS 模型的粗略翻译附加到 Alloy 4 语法中，并穿插了一些 cmets。 （我说“粗略”是因为我没有花很多时间在上面，而且我可能错过了一些细微差别，尤其是在谓词 HighestVersionPolicy 中，作者有点棘手。）如果你的作业目标正是强迫你只用你天生的独创性作为砍刀在语法的丛林中奋战，那么我为搞砸了这种体验而道歉。
在模块的顶部，主要的变化是调用排序库模块的方式。
module PDS
open util/ordering[Number]
在 Component 中，关键字 'option' 被当前关键字 'lone' 替换，我抄录了一些 Huth 和 Ryan 的 cmets，以帮助自己更好地理解发生了什么。
sig Component {
name: Name, // name of the component
main: lone Service, // component may have a 'main' service
export: set Service, // services the component exports
import: set Service, // services the component imports
version: Number // version number of the component
}{
no import & export // imports and exports are disjoint
// sets of services
}
在 PDS 的 sig 中，主要变化还是基数语法的变化：->? 变为 -> lone。
// Package Dependency System
// components is the set of Component in this PDS
// schedule assigns to each component in the PDS
// and any of its import services
// a component in the PDS that provides that service
// (see SoundPDSs, below)
// requires expresses the component dependencies
// entailed by the schedule
sig PDS {
components: set Component,
schedule: components -> Service -> lone components,
// any component / Service pair maps to at most
// one component
requires: components -> components
}{
// for every component in the system,
// the services it imports are supplied (exported)
// by some (other) component in the system
components.import in components.export
}
事实上 SoundPDS，作者使用了 with P 构造，我不记得在我使用过的 Alloy 版本中见过这种构造。所以我把它拿出来，为了清楚起见，重新表述了一些表达式，因为作者解释说，清晰是他们使用with P 构造的主要动机。确保您了解 Alloy 的盒子符号以及为什么 P.schedule[c][s] 是 c.(P.schedule)[s] 或 s.(c.(P .schedule))。
fact SoundPDSs {
all P : PDS | {
all c : P.components, s : Service |
let c' = P.schedule[c][s] {
(some c' iff s in c.import)
// c and s require c' only iff c imports s
&&
(some c' => s in c'.export)
// c and s require c' only if c' exports s
}
all c : P.components | P.requires[c]= P.schedule[c][Service]
// c requires precisely those components
// that schedule says c depends on for some service
}
}
sig Name, Number, Service {}
从现在开始最大的变化是 Huth 和 Ryan 使用 fun 来定义各种属性，而 Alloy 4 使用 pred -- 关键字 fun 仍然是合法的，但它意味着一个函数 (一个表达式，在计算时返回一个值，而不是布尔值）而不是谓词。
pred AddComponent(P, P': PDS, c: Component) {
not c in P.components
P'.components = P.components + c
} run AddComponent for 3 but 2 PDS
pred RemoveComponent(P, P' : PDS, c: Component) {
c in P.components
P'.components = P.components - c
} run RemoveComponent for 3 but 2 PDS
在 HighestVersionPolicy 中，我再次引入了方框符号来尝试使表达式更清晰。请注意，prev 此处未定义 - 它是模块顶部的导入指令 (open ...) 导入的关系之一，从用于排序的库模块。
pred HighestVersionPolicy(P: PDS) {
all s : Service,
c : P.components,
c' : P.schedule[c][s],
c'' : P.components - c' {
s in c''.export && c''.name = c'.name
=>
c''.version in ^prev[c'.version]
}
} run HighestVersionPolicy for 3 but 1 PDS
pred AGuideSimulation(P, P', P'' : PDS, c1, c2 : Component) {
AddComponent[P, P', c1]
RemoveComponent[P, P'', c2]
HighestVersionPolicy[P]
HighestVersionPolicy[P']
HighestVersionPolicy[P'']
} run AGuideSimulation for 3
assert AddingIsFunctionalForPDSs {
all P, P', P'' : PDS, c : Component {
AddComponent[P, P', c] && AddComponent[P, P'', c]
=> P' = P''
}
}
check AddingIsFunctionalForPDSs for 3
version of their model given by Huth and Ryan on the web 不包括他们在文本中描述的 StructurallyEqual 谓词；我添加它是为了帮助确保我对模型的翻译有效。
pred StructurallyEqual(P, P' : PDS) {
P.components = P'.components
P.schedule = P'.schedule
P.requires = P'.requires
}
run StructurallyEqual for 2
同样，它们不包括对AddingIsStructurallyFunctional 的修复——其意图可能是让学生在Alloy 中动态地进行修复。
assert AddingIsStructurallyFunctionalForPDSs {
all P, P', P'' : PDS, c : Component {
AddComponent[P, P', c] && AddComponent[P, P'', c]
=>
StructurallyEqual[P',P'']
}
}
check AddingIsStructurallyFunctionalForPDSs for 3