1

Alloy Analyzer を使用して、特定のスコープ内の述語からすべてのソリューションを列挙したいと考えています。Alloy はこの機能をサポートしていますか? 可能であれば、コマンドラインから呼び出す方法は?

ありがとうございました

4

2 に答える 2

1

これを行うコードは次のとおりです。この例では、通常の Alloy モデル ファイル (スコープを指定する場所) を作成し、このコードを使用してそれを実行します。つまり、モデル ファイルに存在する各コマンドのすべてのソリューションを列挙します。

public void run(String filename) {
    A4Reporter rep = new A4Reporter();
    Module world = CompUtil.parseEverything_fromFile(rep, null, filename);
    A4Options options = new A4Options();
    options.solver = A4Options.SatSolver.SAT4J;
    // options.symmetry = 0; // optionally turn off symmetry breaking
    for (Command command: world.getAllCommands()) {
        // Execute the command
        A4Solution sol = TranslateAlloyToKodkod.execute_command(rep, world.getAllReachableSigs(), command, options);
        while (sol.satisfiable()) {
            System.out.println("[Solution]:");
            System.out.println(sol.toString());
            sol = sol.next();
        }
    }
}
于 2013-06-14T16:20:53.400 に答える
0

はい、Alloy を使用すると、有限の宇宙内ですべての「可能な」ソリューションを列挙できます。ただし、対称性破り (SB) アルゴリズムを使用して、すべての対称性 (ほとんどの対称性) を破ります。したがって、すべての可能なソリューションを列挙することはできません。一方、SB をオフにできたとしても、モデルに対してかなりの数のインスタンスが得られる場合があります。最終的には終了しますが、いつ終了するかはわかりません。実際にはスコープに依存します。jar ファイル (ExampleUsingTheCompiler.java および ExampleUsingTheAPI) 内に、API を使用して Alloy を呼び出す例があり、それを使用してソリューションを列挙できることを覚えています。

于 2013-06-14T14:49:39.480 に答える