在 Alloy 中更改系统内对象的服务代码
Changing service code for object inside a system in Alloy
我想在有任何服务操作对象时更改对象的服务代码。假设,我有一个适用于对象的操作,该对象的服务代码将为 1,当另一个操作执行时,服务代码再次为 2。我想将最新的服务代码保存到每个对象。不幸的是,我无法很好地设计我的谓词,这就是为什么从 alloy.
得到谓词不一致消息的原因
我已经尝试了一些代码来为每个对象分配服务代码。完整代码如下-
open util/ordering[Environment]
abstract sig Object{
name: String,
serviceCode: Int,
}{
serviceCode >= 0 and serviceCode <= 3
}
// Events
enum Event {Event1, Event2, Event3}
abstract sig Condition{
name: Event,
object: Object
}
abstract sig BaseOperation{
name: Event,
object: Object
// it will have more attributes than Condition later
}
abstract sig Connector{
condition: Condition,
baseOperation: BaseOperation,
}
sig Environment{
ev : set Event
}
pred execute [u:Environment, u':Environment, r:Connector] {
some e: u.ev | {
e = r.condition.name =>
u'.ev = u.ev + r.baseOperation.name
else
u'.ev = u.ev
}
}
fact {
all u:Environment-last, u':u.next, r:Connector {
execute [u, u', r]
}
}
sig Object1 extends Object{
}{
name = "Object1 Object"
}
sig Object2 extends Object{
}{
name = "Object2 Object"
}
sig Condition1 extends Condition{
}{
name = Event1
object = Object2
object.serviceCode = 1
}
sig Operation1 extends BaseOperation{
}{
name = Event2
object = Object1
object.serviceCode = 1
}
sig Operation2 extends BaseOperation{
}{
name = Event3
object = Object1
object.serviceCode = 0
}
one sig Connector1 extends Connector{
}{
condition = Condition1
baseOperation = Operation1
}
one sig Connector2 extends Connector{
}{
condition = Condition1
baseOperation = Operation2
}
fact {
Event3 !in first.ev &&
Event2 !in first.ev
}
run {Event1 in last.ev} for 10
当我对一个对象只有一个操作 link 时,上面的代码工作正常。我附上了它的图表 here 。每当有多个操作时,alloy 将无法找到一个实例。在设计 alloy 代码以实现我的目标方面需要帮助。
另一种可能的方法可能是 - 我们可能有一个服务代码列表,而不是一个服务代码。考虑时间戳以及每个服务代码。然后什么时候需要查找最新的服务代码。我们可以取最大时间戳的服务代码。但我不确定如何在 alloy.
中设计它
我认为你应该看看丹尼尔杰克逊的书。 Alloy 不是具有 mutable 赋值的编程语言。它基本上是一个关系规则引擎,可以生成一个 实例 ,一组与这些规则匹配的关系。这意味着如果您需要 mutable 赋值,那么您需要一种方法来表示关系中 mutable 随时间变化的状态。有两种方式:
Time
– 使每个字段都有一个带有 Time
的列,其中 Time
是有序的。我觉得这很麻烦。 Electrum 项目通过提供 var
关键字来简化此操作,然后为您维护 Time
列。
Trace
– 除了将每个字段与 Time
相关联之外,您还可以将关联置于 state sig
中,即下令。然后该关系显示值如何随时间变化。
关键问题是你的问题描述几乎完全脱离规范。你说的Service和后面的Operation是一样的吗? Event
和 Connector
从哪里来?您的问题描述中从未提及它们?
让我们一一道来:
I want to change the service code of an object
open util/ordering[Environment]
sig Object {}
enum ServiceCode { _1, _2 }
sig Environment {
object : Object -> ServiceCode
}
通常,您不想将 Int 用于诸如服务代码之类的东西,因为它们往往会破坏状态 space。
Environment
就是我们的状态。我们想为每个环境原子执行一个 Service。
... whenever there has been any service operated upon it.
sig Service {
serviceCode : ServiceCode
}
pred execute[ e, e' : Environment, o : Object, s : Service ] {
e'.object = e.object ++ o -> s.serviceCode
}
Suppose, I have an Operation whenever that applies to an Object,
不清楚你说的Operation是什么意思,我猜这是之前的Service?
... the Service Code of that Object will be 1 and again when
another Operation executes then the ServiceCode will be 2.
I want to save the latest service code to each object. Unfortunately,
pred trace {
no first.object
all t : Environment-last, t':t.next {
some o: Object, s : Service {
execute[t,t', o, s]
}
}
}
run trace
在 table 视图中,这为您提供:
┌────────────────┐
│this/ServiceCode│
├────────────────┤
│_1⁰ │
├────────────────┤
│_2⁰ │
└────────────────┘
┌───────────┐
│this/Object│
├───────────┤
│Object⁰ │
├───────────┤
│Object¹ │
└───────────┘
┌────────────┬───────────┐
│this/Service│serviceCode│
├────────────┼───────────┤
│Service⁰ │_2⁰ │
├────────────┼───────────┤
│Service¹ │_2⁰ │
├────────────┼───────────┤
│Service² │_1⁰ │
└────────────┴───────────┘
┌────────────────┬───────────┐
│this/Environment│object │
├────────────────┼───────────┤
│Environment⁰ │ │
├────────────────┼───────┬───┤
│Environment¹ │Object¹│_2⁰│
├────────────────┼───────┼───┤
│Environment² │Object⁰│_1⁰│
│ ├───────┼───┤
│ │Object¹│_2⁰│
└────────────────┴───────┴───┘
当你使用Alloy时,你应该做的第一件事就是用简单的英语定义你想说明的问题。然后,您将本文中的概念转换为 Alloy 结构。 Alloy 规范的目标是让它读起来像散文。
我想在有任何服务操作对象时更改对象的服务代码。假设,我有一个适用于对象的操作,该对象的服务代码将为 1,当另一个操作执行时,服务代码再次为 2。我想将最新的服务代码保存到每个对象。不幸的是,我无法很好地设计我的谓词,这就是为什么从 alloy.
得到谓词不一致消息的原因我已经尝试了一些代码来为每个对象分配服务代码。完整代码如下-
open util/ordering[Environment]
abstract sig Object{
name: String,
serviceCode: Int,
}{
serviceCode >= 0 and serviceCode <= 3
}
// Events
enum Event {Event1, Event2, Event3}
abstract sig Condition{
name: Event,
object: Object
}
abstract sig BaseOperation{
name: Event,
object: Object
// it will have more attributes than Condition later
}
abstract sig Connector{
condition: Condition,
baseOperation: BaseOperation,
}
sig Environment{
ev : set Event
}
pred execute [u:Environment, u':Environment, r:Connector] {
some e: u.ev | {
e = r.condition.name =>
u'.ev = u.ev + r.baseOperation.name
else
u'.ev = u.ev
}
}
fact {
all u:Environment-last, u':u.next, r:Connector {
execute [u, u', r]
}
}
sig Object1 extends Object{
}{
name = "Object1 Object"
}
sig Object2 extends Object{
}{
name = "Object2 Object"
}
sig Condition1 extends Condition{
}{
name = Event1
object = Object2
object.serviceCode = 1
}
sig Operation1 extends BaseOperation{
}{
name = Event2
object = Object1
object.serviceCode = 1
}
sig Operation2 extends BaseOperation{
}{
name = Event3
object = Object1
object.serviceCode = 0
}
one sig Connector1 extends Connector{
}{
condition = Condition1
baseOperation = Operation1
}
one sig Connector2 extends Connector{
}{
condition = Condition1
baseOperation = Operation2
}
fact {
Event3 !in first.ev &&
Event2 !in first.ev
}
run {Event1 in last.ev} for 10
当我对一个对象只有一个操作 link 时,上面的代码工作正常。我附上了它的图表 here 。每当有多个操作时,alloy 将无法找到一个实例。在设计 alloy 代码以实现我的目标方面需要帮助。
另一种可能的方法可能是 - 我们可能有一个服务代码列表,而不是一个服务代码。考虑时间戳以及每个服务代码。然后什么时候需要查找最新的服务代码。我们可以取最大时间戳的服务代码。但我不确定如何在 alloy.
中设计它我认为你应该看看丹尼尔杰克逊的书。 Alloy 不是具有 mutable 赋值的编程语言。它基本上是一个关系规则引擎,可以生成一个 实例 ,一组与这些规则匹配的关系。这意味着如果您需要 mutable 赋值,那么您需要一种方法来表示关系中 mutable 随时间变化的状态。有两种方式:
Time
– 使每个字段都有一个带有Time
的列,其中Time
是有序的。我觉得这很麻烦。 Electrum 项目通过提供var
关键字来简化此操作,然后为您维护Time
列。Trace
– 除了将每个字段与Time
相关联之外,您还可以将关联置于 statesig
中,即下令。然后该关系显示值如何随时间变化。
关键问题是你的问题描述几乎完全脱离规范。你说的Service和后面的Operation是一样的吗? Event
和 Connector
从哪里来?您的问题描述中从未提及它们?
让我们一一道来:
I want to change the service code of an object
open util/ordering[Environment]
sig Object {}
enum ServiceCode { _1, _2 }
sig Environment {
object : Object -> ServiceCode
}
通常,您不想将 Int 用于诸如服务代码之类的东西,因为它们往往会破坏状态 space。
Environment
就是我们的状态。我们想为每个环境原子执行一个 Service。
... whenever there has been any service operated upon it.
sig Service {
serviceCode : ServiceCode
}
pred execute[ e, e' : Environment, o : Object, s : Service ] {
e'.object = e.object ++ o -> s.serviceCode
}
Suppose, I have an Operation whenever that applies to an Object,
不清楚你说的Operation是什么意思,我猜这是之前的Service?
... the Service Code of that Object will be 1 and again when another Operation executes then the ServiceCode will be 2. I want to save the latest service code to each object. Unfortunately,
pred trace {
no first.object
all t : Environment-last, t':t.next {
some o: Object, s : Service {
execute[t,t', o, s]
}
}
}
run trace
在 table 视图中,这为您提供:
┌────────────────┐
│this/ServiceCode│
├────────────────┤
│_1⁰ │
├────────────────┤
│_2⁰ │
└────────────────┘
┌───────────┐
│this/Object│
├───────────┤
│Object⁰ │
├───────────┤
│Object¹ │
└───────────┘
┌────────────┬───────────┐
│this/Service│serviceCode│
├────────────┼───────────┤
│Service⁰ │_2⁰ │
├────────────┼───────────┤
│Service¹ │_2⁰ │
├────────────┼───────────┤
│Service² │_1⁰ │
└────────────┴───────────┘
┌────────────────┬───────────┐
│this/Environment│object │
├────────────────┼───────────┤
│Environment⁰ │ │
├────────────────┼───────┬───┤
│Environment¹ │Object¹│_2⁰│
├────────────────┼───────┼───┤
│Environment² │Object⁰│_1⁰│
│ ├───────┼───┤
│ │Object¹│_2⁰│
└────────────────┴───────┴───┘
当你使用Alloy时,你应该做的第一件事就是用简单的英语定义你想说明的问题。然后,您将本文中的概念转换为 Alloy 结构。 Alloy 规范的目标是让它读起来像散文。