Блокировка вызова в сплаве - PullRequest
Новая
       25

Блокировка вызова в сплаве

0 голосов
/ 31 марта 2020

Я хотел бы решить следующую проблему блокировки , используя Alloy .

Моя главная проблема заключается в том, как смоделировать целые числа, представляющие клавиши di git.

Я создал быстрый черновик: 

sig Digit, Position{}

sig Lock {
 d: Digit one -> lone Position
}

run {} for exactly 1 Lock, exactly 3 Position, 10 Digit

В этом контексте, не могли бы вы:

  • сказать мне, если Сплав кажется вам подходящим для решения такого рода проблемы?
  • подскажите, как я могу смоделировать цифры клавиш (без использования Int с)?

Спасибо.

enter image description here

Ответы [ 4 ]

0 голосов
/ 04 апреля 2020

Когда вы решите, что решение завершено, давайте рассмотрим, является ли решение обобщенным c.

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

  • Подсказка1: (1,2,3) - Ничего не правильно.
  • Подсказка 2: (4,5,6) - Ничего не правильно.
  • Подсказка3: (7,8,9) - Одно число верно, но неправильно помещено.
  • Подсказка4: (9,0,0) - Все числа верны, с одной лункой.
0 голосов
/ 31 марта 2020

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

pred lock[ a,b,c : Int ] {
    a=6 || b=8 || c= 2
    a in 1+4 || b in 6+4 || c in 6+1
    a in 0+6 || b in 2+6 || c in 2+0
    a != 7 && b != 3 && c != 8
    a = 7 || b=8 || c=0 
}

run lock for 6 int

Найдите ответ в текстовом представлении.

upate у нас была дискуссия в списке Alloy, и я хотел бы дополнить свое решение более читаемой версией: 

let sq[a,b,c]       = 0->a + 1->b + 2->c
let digit       = { n : Int | n>=0 and n <10 }

fun correct[ lck : seq digit, a, b, c : digit ] : Int    { # (Int.lck & (a+b+c)) }
fun wellPlaced[ lck : seq digit, a, b, c : digit ] : Int { # (lck & sq[a,b,c])   }

pred lock[ a, b, c : digit ] {
    let lck = sq[a,b,c] {
        1 = correct[ lck, 6,8,2] and 1 = wellPlaced[ lck, 6,8,2]        
        1 = correct[ lck, 6,1,4] and 0 = wellPlaced[ lck, 6,1,4]
        2 = correct[ lck, 2,0,6] and 0 = wellPlaced[ lck, 2,0,6]
        0 = correct[ lck, 7,3,8]
        1 = correct[ lck, 7,8,0] and 0 = wellPlaced[ lck, 7,8,0]
    }
}

run lock for 6 Int
0 голосов
/ 01 апреля 2020

Моя рамка этой головоломки: 

enum Digit { N0,N1,N2,N3,N4,N5,N6,N7,N8,N9 }
one sig Code {a,b,c:Digit}

pred hint(h1,h2,h3:Digit, matched,wellPlaced:Int) {
    matched = #(XXXX)        // fix XXXX
    wellPlaced = #(XXXX)     // fix XXXX
}

fact {
    hint[N6,N8,N2, 1,1]
    hint[N6,N1,N4, 1,0]
    hint[N2,N0,N6, 2,0]
    hint[N7,N3,N8, 0,0]
    hint[N7,N8,N0, 1,0]
}

run {}
0 голосов
/ 31 марта 2020

Да, я думаю, что Alloy подходит для такого рода проблем.

Что касается цифр, вам вообще не нужны целые числа: на самом деле, это немного неуместно для этой конкретной цели, если они являются цифрами или любой набор из 10 различных идентификаторов (с ними не выполняется арифметика c). Вы можете использовать одноэлементные подписи для объявления цифр, все расширяющие сигнатуру Digit, которые должны быть помечены как abstract. Примерно так: 

abstract sig Digit {}
one sig Zero, One, ..., Nine extends Digit {}

Аналогичная стратегия может быть использована для объявления трех разных положений замка. И, кстати, поскольку у вас ровно одна блокировка, вы также можете объявить Lock единственной подписью.

...