私はAlloyモジュールを持っています
module WorkPlace
sig String{}
sig person{}
sig Employee extends person{
name :String, boss: Employee,worker: set Employee}
sig Employee1 extends person{
name :String, boss: Employee,worker: set Employee}
fact Employee{
all e1:Employee, e2:Employee| (e1.name = e2 && e2.name = e1) =>e1 = e2}
run{}
このモードをトライアドで実行すると、次のメッセージが表示されます。
私はそれが何を意味するのか分かりませんか?
2\ 2 つの Alloy モデルがある場合、各モデルには同じ要素 (mode1/name、model2/name) があります。mode1/name = model2/name と言うことができるファクトまたは pred を作成するにはどうすればよいですか?
よろしく