失敗して学ぶAlloy

文章を見てわかるかとおもいますが、筆者はよくわかっていません。
失敗を繰り返したり、コードを読んだりすることで習得を頑張ります。

要素が複数の集合に重複して関係しないようようにする

例えば、あるノードが複数の要素を管理する場合、複数のノードが同一の要素を含まないようにする。 以下では、複数のDBが同一のデータを持たないように制限する。
互いに素であるDBの元i,j の持つ ID の集合積の個数が0になる
=集合積がない状態を指定する=どちらにも属す要素がない。

      // データ
      sig Data {}
      
      // データベース
      sig DB {
        oid: set Data
      }
      
      // 互いに素でなるDBの元i, jについて、i.oid と j.oid の集合積の個数が0以上にはならない
      fact {
        no disj i, j : DB | #(i.oid & j.oid) > 0
      }
      
      // 例の表示
      pred show { }
      run show for 2
      

要素が必ず含まれる

		sig Data {}

		sig DB {
			id: set Data
		}

		fact {
			// Data集合の全ての要素が DB.id に含まれる = Dataは全てDBの要素である
			all x : Data | x in DB.id
		}

		pred show { }
		run show