0

每当有任何服务对其进行操作时，我都想更改对象的服务代码。假设我有一个操作适用于一个对象，该对象的服务代码将为 1，当另一个操作执行时，服务代码将再次为 2。我想将最新的服务代码保存到每个对象。不幸的是，我不能很好地设计我的谓词，这就是为什么从合金中得到谓词不一致的消息。

我尝试了一些代码来为每个对象分配服务代码。如下所示的完整代码 -

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

当我只有一个操作链接到一个对象时，上面的代码可以正常工作。我在这里附上了它的图表。每当有多个操作时，合金就无法找到一个实例。需要帮助设计合金代码以实现我的目标。

另一种可能的方法可能是——我们可能有一个服务代码列表，而不是一个服务代码。考虑时间戳以及每个服务代码。然后什么时候需要找出最新的服务代码。我们可以取最大时间戳的服务代码。但我不确定如何用合金设计这个。

4

1 回答 1

0

我认为你应该看看丹尼尔杰克逊的书。Alloy 不是具有可变分配的编程语言。它基本上是一个基于关系的规则引擎，可以生成一个实例，一组与这些规则匹配的关系。这意味着如果您需要可变分配，那么您需要一种方法来表示关系中随时间变化的可变状态。有两种方法：

  • Time– 使每个字段都有一列Time，其中Time排序。我觉得这很麻烦。Electrum项目通过提供一个关键字来为您维护该列，从而使这变得更容易。varTime
  • Trace– 除了将每个字段与 相关联Time，您还可以将关联置于有序状态 sig。然后，该关系显示值如何随时间变化。

关键问题是您的问题描述几乎与规范完全脱节。你说的是Service，然后是Operation，它们是一样的吗？在哪里做Event和Connector进来？您的问题描述中从未提及它们？

让我们一一来看：

我想更改对象的服务代码 

   open util/ordering[Environment]

   sig Object {}
   enum ServiceCode { _1, _2 }

   sig Environment {
      object    : Object -> ServiceCode
   }

通常，您不想将 Ints 用于服务代码之类的东西，因为它们往往会破坏状态空间。

Environment是我们的状态。我们希望每个环境原子执行一个服务。

...只要有任何服务对其进行操作。

   sig Service {
    serviceCode : ServiceCode
   }

   pred execute[ e, e' : Environment, o : Object, s : Service ] {
    e'.object = e.object ++ o -> s.serviceCode       
   }

假设，只要适用于Object ，我就有一个Operation，

目前尚不清楚您对Operation的含义是什么，我认为这是较早的Service？

...该对象的服务代码将为 1，当另一个操作执行时，服务代码将再次为 2。我想将最新的服务代码保存到每个对象。很遗憾，

  pred trace {
    no first.object
    all t : Environment-last, t':t.next {
           some o: Object, s : Service {
           execute[t,t', o, s]
        }
    }
  }

  run trace

在表格视图中，这为您提供：

┌────────────────┐
│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 时，您应该做的第一件事是用简单的英语定义您想要指定的问题。然后，您将本文中的概念翻译成合金结构。合金规范的目标是让它读起来像散文。

于 2019-05-14T07:20:20.430 回答