Поиск экземпляров выполнения предикатов Alloy

Question

Можно ли искать экземпляры предикатных исполнений (последовательности предикатных приложений), которые ведут из заданного состояния в другое состояние с ограничениями?

Несколько связанных вопросов: есть ли способ передать предикат в качестве аргумента другому предикату?

Answer 1

Это не совсем понятно, что вы ищете, по крайней мере, для читателя, как я, который думает о предикатах, как вещи, чтобы оценить , а не вещи, чтобы выполнить.

Можно ли искать случаи предикатных казни ...?

Это звучит так, как будто здесь вы ищете такие вещи обсуждались в Джексон Software абстракций в разделе 2.4 «Execution следов» и в других местах (см «след» в индексе). Основная идея заключается в том, чтобы

• определить предикат, описывающий начальное состояние (например, Джексон называет его инициализации)
• определить набор предикатов, описывающих возможные переходы из состояния в состояние
• налагать общий порядок на состояний

• определить предикат для проверки выполнения трассировки, занимает примерно форма

  pred traces { 
      init [first] /* 'first' is defined by util/ordering[State] */ 
      all s : State - last 
      | let s' = next[s] 
      | Possible_Transition[s, s'] 
  } 
  

Многие варианты, конечно, возможны.

Есть ли способ передать предикат в качестве аргумента другому предикату?

Нет и да.

Нет, потому что сплав использует логику первого порядка; все аргументы предикатов являются множествами атомов, которые определены как расширение.

Да, потому что можно, конечно, подтвердить предикаты, сделав сигнатуру, которая отображает 1: 1 в набор предикатов и пропускает атомы этой подписи, когда кто-то хочет передать предикат. Это всегда возможно, учитывая конечное число предикатов, которые человек хочет восстановить таким образом. (Пожалуйста, извините меня, если этот момент и объяснение ниже кажутся вам очевидными: я помню время, когда они не были для меня неожиданно очевидны, и я ожидаю, что у Stack Overflow есть некоторые читатели, для которых они не очевидны.)

Предположим, что у нас есть два предиката P и Q, каждый из которых принимает атомный аргумент a типа Atom. И мы хотим определить мета-предикат M, который принимает атом x и предикат Y и возвращает значение Y[x].

// First some scaffolding 
sig Atom {} 
pred P [a : Atom] { ... // whatever you like } 
pred Q [a : Atom] { ... // whatever ... } 

// Now the heart of the matter 
abstract sig reification {} 
one sig p, q extends reification {} 

pred M [x : Atom, Y : reification] { 
    (Y = p) implies P[x] 
    else (Y = q) implies Q[x] 
    else x != x 
} 

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

Но, как и другие системы первого порядка, сплав может с некоторой осторожностью и усилием использоваться для поддержки аргументов более высокого порядка. Когда мы применяем Alloy, чтобы показать, что данный проект имеет свойство P, мы находимся в наиболее распространенном случае, утверждая, что все правильные реализации дизайна также будут иметь свойство P, утверждение, что в Alloy может принять форму all i : Implementation | correctly_implements_design[i] implies has_property_P[i]. Но реализация (слегка упрощение) представляет собой соотношение между входами и выходами. Таким образом, любое утверждение о реализации является претензией второго порядка. Поэтому, обобщая все реализации данного проекта, мы делаем аргумент первого порядка (выраженный в модели сплава) для поддержки заявки второго порядка.

Если у вас есть серьезная заинтересованность в использовании сплава для аргументов о предложениях второго порядка, вы захотите ознакомиться с разделами 3.2.3, 5.2.2 и 5.3 в книге Джексона.