組込みシグネチャ String

[hawaii]

田辺です。Stringについて使い方や用途がよく分かってませんが
とりあえずサンプルモデルを作成してみました。

one sig Language {
greeting: String
} {
"Hello World!" in greeting
}
run {}

このコードは Alloy 4.2rc で動作します。
ver. 4.1.10 では文字列のリテラルがサポートされていないようなので動作しません。
リテラルを使わず正確スコープで String の要素数を指定すれば ver. 4.1.10 でも
String シグネチャを使うことができます。
以下、その例です。

abstract sig Person {
firstName: String,
lastName: String,
character: Character,
partner: lone Person
}
sig Man extends Person {}
sig Woman extends Person {}

pred HappyMarriage [he, he': Man, she, she': Woman] {
no he.partner
no she.partner

she'.partner = he
he'.partner = she

she'.firstName = she.firstName
she'.lastName = (she.character = Independent implies she.lastName
else he.lastName)
she'.character = Influential

he'.firstName = he.firstName
he'.lastName = he.lastName
he'.character = Patient
}
enum Character {Normal, Independent, Influential, Patient}

run HappyMarriage for 4 Person, exactly 3 String

ところで、このコードをいじっているときに不思議な現象に遭遇しました。
述語の宣言は、HappyMarriage [he, he': Man, she, she': Woman] となっているのに
次のコマンドを実行すると、男と男が結婚したり、結婚後、性別が変わったりするのです。

run {
some m, m', w, w': Person | HappyMarriage [m, m', w, w']
} for 4 Person, exactly 3 String

本を見返してみると、この現象について次の説明がありました。
p.267 B.7.6 コマンド
述語や関数の宣言制約は述語や関数を直接 run するときにだけ用いられ、他の述語や関数から呼び出されるときには無視されることに注意が必要です。

[Takeo Imai]

今井です。

Stringは、4.2rcリリース前に「一時的に導入されたもので、削除する予定」と聞いていました。
もしかしたら向こうの気が変わったのかもしれませんが、現状公式サポートは期待しない方がいいと思います。

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

> 述語の宣言は、HappyMarriage [he, he': Man, she, she': Woman] となっているのに
> 次のコマンドを実行すると、男と男が結婚したり、結婚後、性別が変わったりするのです。
>
> run {
> some m, m', w, w': Person | HappyMarriage [m, m', w, w']
> } for 4 Person, exactly 3 String

中の制約を

some m, m': Man, w, w': Woman | HappyMarriage [m, m', w, w']

とすれば、この現象は起こらなくなります。

> 本を見返してみると、この現象について次の説明がありました。
> p.267 B.7.6 コマンド
> 述語や関数の宣言制約は述語や関数を直接 run するときにだけ用いられ、他の述語や関数から呼び出されるときには無視されることに注意が必要です。

はい。必要であれば、B.6.3, B.6.4なども参照してください。

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

[hawaii]

> Stringは、4.2rcリリース前に「一時的に導入されたもので、削除する予定」と聞いていました。

情報ありがとうございます。
用途もなさそうですし、結構なことだと思います。

> はい。必要であれば、B.6.3, B.6.4なども参照してください。

述語や関数の引数宣言は、型検査、直接起動では使用されるけども他から呼び出しでは無視される。
それで意味が変わるようなモデルは書いてはならない。
というようなことがしっかり書いてありました。