是否可以在合金中建模逻辑门

Question

我是一名新的合金学习者。我有几件事想知道。

是否可以创建元素？

您将如何建模 AND 逻辑门？

我的想法是无用的，就像

open util/ordering[Time]
sig Time {frame: set gate}


abstract sig gate{}
sig ABinCout extends gate{ 
getA    : A,
getB    : B,
outputsC    : C,
} 


abstract sig Signals {}
sig A extends Signals{}
sig B extends Signals{}
sig C extends Signals{}


fact{first.frame = gate && no gate.getA && no gate.getB && no gate.outputsC } 

pred GateAB [t,t' : set Time,Gate : ABinCout]{
one a : A  | one b : B | {
Gate.getA = Gate.getA + a 
Gate.getB = Gate.getB + b
}}

pred GateABparaC [Gate : set ABinCout]{
one a : Gate.getA | one b : Gate.getB | one c : C{
    Gate.getA = Gate.getA - a
    Gate.getB = Gate.getB - b
    Gate.outputsC = Gate.outputsC + c

}}

pred GateC [Gate : set ABinCout]{
one c : Gate.outputsC | {
    Gate.outputsC =Gate.outputsC - c
}}

fact{
all t : Time, t' : t.next | one cel: ABinCout{
 GateAB[t,t',cel]
}}


run{ }for exactly 2 Time, 1 ABinCout, 3 A, 3 B, 1 C 

我可以从字面上说我对合金一无所知，但我想单独代表门......然后我产生 2 个输入......然后在另一个帧中它产生一个不是任何输入的输出！

提前致谢

如果有什么我应该阅读或现在要执行此任务的内容，请说出来。

Answer 1

目前尚不清楚您究竟想通过门实现什么。希望我下面的示例将阐明有关 Alloy 的某些内容，并帮助您设计所需的任何门。

在这个简单的示例中，有一个代表信号的抽象 sig，以及两种不同的具体信号：One 和 Zero。接下来，一个抽象门被建模为在其输入（ins 字段）上有一组信号，在其输出（out 字段）上有一个信号。最后，我定义了 3 个具体的信号来模拟标准 AND、OR 和 NOT 门；对于这些信号中的每一个，我添加了一个 附加事实 以建立在输入和输出上找到的信号之间必须保持的关系（例如，AND 门的输出是 One 如果并且只有当它的所有输入都是Ones)。

然后我认为展示如何对由几个简单门组成的更复杂的门进行建模会很有用。我定义了xorgate 谓词，它断言给定的输入信号（a、b）和门（and1、and2、not1、not2、or1）一起形成一个异或门（下图“已连接”）

现在，Alloy 最好的部分是您可以使用run 命令通过查找满足此谓词的实例来模拟此 XOR 门。您还可以使用check 命令检查此异或门上所有可能的输入，当且仅当输入不同时，其输出为One（这就是异或门的工作方式）。在 Alloy 中执行此检查没有发现反例。

abstract sig Signal {}
one sig One extends Signal {}
one sig Zero extends Signal {}

abstract sig Gate {
  ins: set Signal,
  out: one Signal
} 

sig AND extends Gate {}{ out = One iff ins in One }
sig OR  extends Gate {}{ out = Zero iff ins in Zero }
sig NOT extends Gate {}{ #ins = 1 and out = Signal - ins }

pred xorgate[a, b: Signal, and1, and2: AND, not1, not2: NOT, o1: OR] {
  not1.ins = a
  and1.ins = b + not1.out
  not2.ins = b
  and2.ins = a + not2.out
  or1.ins = and1.out + and2.out
}

run xorgate for 5

check {
  all in1, in2: Signal |
    all a1, a2: AND, n1, n2: NOT, o1: OR {
      xorgate[in1, in2, a1, a2, n1, n2, o1] implies (o1.out = One iff in1 != in2)
    }
} for 5