Изменение сервисного кода для объекта внутри системы в Alloy - PullRequest
Новая
       44

Изменение сервисного кода для объекта внутри системы в Alloy

0 голосов
/ 12 мая 2019

Я хочу изменить сервисный код объекта всякий раз, когда какой-либо сервис работал с ним. Предположим, у меня есть операция, когда это применимо к объекту, служебный код этого объекта будет равен 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

Приведенный выше код прекрасно работает, когда у меня есть только одна ссылка на операцию для одного объекта. Я приложил диаграмму для этого здесь . Всякий раз, когда происходит более одной операции, сплав не может найти экземпляр. Нужна помощь в разработке кода сплава для достижения моей цели.

Другой возможный подход может заключаться в том, что вместо одного сервисного кода у нас может быть список сервисных кодов. Учитывая временную метку вместе с каждым сервисным кодом. Тогда когда нужно узнать последний сервисный код. Мы можем взять код обслуживания максимальной отметки времени. Но я не уверен, как спроектировать это из сплава.

1 Ответ

0 голосов
/ 14 мая 2019

Я думаю, вам стоит взглянуть на книгу Дэниела Джексона.Alloy не является языком программирования с изменяемыми назначениями.В основном это механизм правил над отношениями, который может генерировать экземпляр , набор отношений, соответствующих этим правилам.Это означает, что если вам нужны изменяемые назначения, вам нужен способ представления изменяемого состояния во времени в отношении.Есть два способа:

  • Time - сделать так, чтобы в каждом поле был столбец с Time, где упорядочено Time.Я нахожу это довольно громоздким.Проект Electrum упростил эту задачу, предоставив ключевое слово var, которое затем поддерживает столбец Time.
  • Trace - Вместо того, чтобы связывать каждое поле с TimeВы также можете поместить ассоциации в упорядоченное состояние sig.Затем это соотношение показывает, как значения меняются со временем.

Ключевая проблема заключается в том, что описание вашей проблемы почти полностью отсоединено от спецификации.Вы говорите о Службе , а затем о Операции , они одинаковы?Откуда 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       
   }

Предположим, у меня есть Операция всякий раз, когда это относится к Объекту ,

ItНепонятно, что вы имеете в виду под Операцией , я предполагаю, что это более ранняя Служба ?

... Сервисный код для этого Object будет 1, и снова, когда другая Operation будет выполнена, тогда ServiceCode будет 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, первое, что вам нужно сделать, это определить проблему, которую вы хотите указать впростой английский.Затем вы переводите понятия в этом тексте в конструкции Alloy.Цель спецификации Alloy - сделать ее читаемой как проза.

...