ボンジュール・マドモアゼル

本サイトの情報は自己責任にてご利用下さい。

[Alloy] Alloy 4.1.10 シーケンス seq/Int MaxSeq

 
シーケンスの使用例
open util/sequniv  -- 省略可


sig E {}
one sig A {
s: seq E -- 予約語 seq でシーケンスを定義
} {
#s > 5 -- 要素数は 5 より多い
not s.hasDups -- 各要素は重複しない
}

run {} for 10 E, 7 seq -- シーケンスの要素数の上限を 7 と指定
実行例:
Executing "Run run$1 for 7 seq, 10 E"

Solver=sat4j Bitwidth=4 MaxSeq=7 SkolemDepth=2 Symmetry=20
1233 vars. 80 primary vars. 3589 clauses. 296ms.
. found. Predicate is consistent. 156ms.
Alloy Sequence
seq/Int について
seq/Int は シーケンスのインデックスの集合であり、Int の部分集合となっている。
0 以上 MaxSeq - 1 以下の正の整数(MaxSeq個)の要素を含む。
MaxSeq はスコープ指定 MaxSeq seq で指定する。
指定できる数値は

0 ≤ MaxSeq ≤ (2^(Bitwidth-1))-1

である。
one sig A {

Min: seq/Int,
Max: seq/Int
} {
all n: seq/Int | int Min =< int n
all n: seq/Int | int n =< int Max
}
run {} for 4 int, 7 seq
実行例:
Executing "Run run$1 for 4 int, 7 seq"

Solver=sat4j Bitwidth=4 MaxSeq=7 SkolemDepth=2 Symmetry=20
159 vars. 14 primary vars. 362 clauses. 212ms.
. found. Predicate is consistent. 60ms.

Alloy seq/Int
参考:
http://alloy.mit.edu/alloy4/xmlformat.html

[未分類] VDM Overture (Ver.1.1.0) コード生成できない

 
although features to generate executable code in high-level programming languages are not yet available in Overture.

Overture VDM-10 Tool Support: User Guide

[トラブルシューティング] Windows Update (KB2586448) 80070011 エラー

 
Program Files を別ドライブに移動し、
レジストリのプログラムフォルダへのパスを書き換えず、
C:\Program Files のジャンクションを作成している場合、
Windows Update に失敗することがある。

解決策については、以下(特に No.4)を参考に。
http://oshiete.goo.ne.jp/qa/6192528.html

[VBScript] Dictionary オブジェクトがコレクションではありません。(800A01C3)

 
Set dict = CreateObject("Scripting.Dictionary")

dict.Add 1, "a"
Msgbox dict.Items(0)
上記の VBSciprt ファイルを実行すると以下のエラーが発生します。(エラーメッセージが表示されない場合は、既定のホストが CScript になっている可能性があります。既定のホスト切り替えについては、『WSH エラーメッセージを表示する』を参照して下さい。)

エラーメッセージ
エラー: オブジェクトがコレクションではありません。: 'dict.Items'
コード: 800A01C3

解決策
もともと Dictionary オブジェクトの Items(), Keys()メソッドには引数はありません。戻り値は要素ではなく要素の配列になります。そこで以下のように Items メソッドの呼び出しで引数なしの括弧を補えば解決します。
Set dict = CreateObject("Scripting.Dictionary")

dict.Add 1, "a"
Msgbox dict.Items()(0)
Itemsメソッドの返す配列を何度も参照する場合には、Itemsメソッドの戻り値を一時変数に格納するのも良いでしょう。

参考
MSDN : Script Runtime → Dictionary Object → Items Method (日本語)

MSDN : Script Runtime → Dictionary Object → Items Method (英語)

[WSH] WSH エラーメッセージを表示する

 
VBS, WSHファイルをダブルクリックしても VBScript のコンパイルエラーなど、エラーメッセージがメッセージボックスで表示されないことがある。エラーメッセージをダイアログボックスで出すには、コマンドプロンプトで以下のコマンドを実行する。
C:\>wscript //h:wscript
参考

WscriptとCscriptの違い

MSDN — Windows からスクリプトを実行する