我创建了一个将数据块写入固定大小的内存的Alloy模型 . 见下文 . 合金分析器生成的实例都包含大小为1的块（即，具有一个数据的块）或更少 . 我希望Alloy Analyzer使用大小为2的块生成实例 . 所以，我把它添加到 writeBlock 谓词： #block = 2 . 这是更新的谓词：

pred writeBlock (m, m': Memory, block: set Data) {
    some addrs: set m.data.Data {
        #addrs = #block
        #block = 2   // I added this
        m'.data = m.data ++ (addrs -> block)
    }
}

但随后分析师说“没有找到实例” .

为什么？

为什么没有实例？

module fixedSizeMemory [Addr, Data]

sig Memory {
    data: Addr -> one Data
}

// Write a block of data to memory.
pred writeBlock (m, m': Memory, block: set Data) {
    some addrs: set m.data.Data {
        #addrs = #block
        m'.data = m.data ++ (addrs -> block)
    }
}

pred Show {}
run writeBlock

更新：我想出了添加 #block = 2 时没有实例的原因 . 问题出在 (addrs -> block) 上 . 这就是说：取所有 addrs 值和 block 值的排列 . 因此，如果有2个 addrs 值和2个 block 值，那么将有4个排列 . data 关系表示每个 Addr 值映射到一个 Data 值 . 但这四种排列将违反这一限制 . 唯一不违反关系的 blocks 是大小为1或0的 blocks .

Update#2 ：我解决了这个问题 . 这是合金代码写一块内存：

// Write a block of data to memory. That is,
// overwrite the data at a set of addresses
// with values in block.
pred writeBlock (m, m': Memory, block: set Data) {
       // Non-deterministically select a subset 
       // of m's addresses to be overwritten.
       some addresses: set m.data.Data {
           // The chunk of memory overwritten
           // matches the size of the block.
           #addresses = #block
           // Create a temporary relation, mapping.
           // It defines a mapping from each address
           // selected above to a block value. The
           // relation is 1:1. That is, each address is
           // assigned a value from block, and each
           // value in block is associated to an address.
           some mapping: addresses one -> one block {
               // Overwrite the selected portion of memory
               // with mapping.
               m'.data = m.data ++ mapping
              // This is so cool!
         }
    }
}
alloy