宣言の disj 範囲式の文法

[hawaii]

田辺です。本書 F.4.7 互いに素な範囲式 で紹介されている disj ですが、

sig X {
f: disj some Y, g: Y
}
は仕様上、文法誤りでしょうか。

以下のようにしなければ、Alloy 4.2RC でも動作しません。

sig X {
f: disj (some Y), g: Y
}


実行例---------------------------------
sig Y {}
sig X {
f: disj some Y, g: Y
}
check {
all disj a, b: X | no (a.f & b.f)
} for 10

Syntax error at line 4 column 1:
There are 3 possible tokens that can appear here:
, { |

[Takeo Imai]

今井です。

2011/10/30 hawaii <happy.lov...@gmail.com>:

> sig X {
> f: disj some Y, g: Y
> }
> は仕様上、文法誤りでしょうか。

これはバグではないでしょうか。どうもsome が多重度制約でなく、限量子として解釈されてしまっているように思えます。someの代わりにset
など、限量子にない多重度制約キーワードを置くと、この問題が発生しません。

あるいは、g の前に private をつけるなど、g 以下が別の宣言であることが明らかなようにすると、やはり問題は発生しなくなります。

--
IMAI Takeo <takeo...@gmail.com>

[Takeo Imai]

今井です。

本家コミュニティの掲示板に、バグレポートとして報告しておきました。
http://alloy.mit.edu/community/node/2817

2011/11/6 Takeo Imai <takeo...@gmail.com>:

--
IMAI Takeo <takeo...@gmail.com>