0

私は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 を作成するにはどうすればよいですか?

よろしく

4

1 に答える 1

1

  1. user1513683 が既に回答したように:

    「文字列」は予約語です。代わりに「文字列」を使用してください（または、「名前」の方が適切です）

  2. 別のモジュールから既存のモジュールを開くことができ、そのモジュールで、2 つのモジュールのいずれかに存在するすべての sigs/関係を使用できます。例えば：

モジュール 1 (ファイル m1.als):

module m1

sig S1 {}

モジュール 2 (ファイル m2.als):

module m2

open m1

sig S2 {}

run { #S1 = #S2 }
于 2013-01-16T16:53:18.693 に答える