执行合金命令时会抛出一个空值。

Question

我一直在使用合金化API，它可以用Java编写。我的目标是编译合金模型，可视化地显示它，缩小对实例的搜索范围。

此时，我需要命令合金语言的源，它可以根据源正确执行或抛出NullPointerException。我已经在eclipse调试器中检查了API类的内容，但我无法正确理解它。

问题是:调试器显示java.lang.NullPointerException.发生TranslateAlloyToKodkod.execute_command

根据合金API文档的说法

如果用户选择“保存到文件”作为TranslateAlloyToKodkod.execute_command求解器，则返回null；如果求解器完成整个求解，则返回非空值，并且要么是可满足的，要么是不可满足的。

但我从未改变“保存到文件”作为SAT解决程序的执行选项。作为您的信息，解决器，合金分析器完成了以下两个来源的整个解决方案。

你能告诉我怎么解决这个问题吗？

下面是我创建的Java代码，并从API示例中添加了一些内容：

import java.io.File;
import edu.mit.csail.sdg.alloy4.A4Reporter;
import edu.mit.csail.sdg.alloy4.Err;
import edu.mit.csail.sdg.alloy4.ErrorWarning;
import edu.mit.csail.sdg.alloy4compiler.ast.Command;
import edu.mit.csail.sdg.alloy4compiler.ast.Module;
import edu.mit.csail.sdg.alloy4compiler.parser.CompUtil;
import edu.mit.csail.sdg.alloy4compiler.translator.A4Options;
import edu.mit.csail.sdg.alloy4compiler.translator.A4Solution;
import edu.mit.csail.sdg.alloy4compiler.translator.TranslateAlloyToKodkod;
import edu.mit.csail.sdg.alloy4viz.VizGUI;

public final class exportXML {
    
    private static String outputfilepath;

    public static void main(String[] args) throws Err {

        VizGUI viz = null;
        
        A4Reporter rep = new A4Reporter() {
            @Override public void warning(ErrorWarning msg) {
                System.out.print("Relevance Warning:\n"+(msg.toString().trim())+"\n\n");
                System.out.flush();
            }
        };

        String args_filename = args[0];

        String[] path_split = args_filename.split("/");
        int pos_fname = path_split.length -1;
        String[] filename_split = path_split[pos_fname].split("\\.");

        for ( int i=0; i<filename_split.length; i++ ) {
            System.out.println(filename_split[i]);
        }

        String dir = "";
        for ( int i = 0; i < path_split.length - 1; i++ ) {
            dir =  dir.concat(path_split[i]) + "/";
        }
        
        String out_fname = "Instance_of_" + filename_split[0];
        outputfilepath = dir + out_fname;

        File outdir = new File(outputfilepath);
        outdir.mkdir();

        for(String filename:args) {

            System.out.println("=========== parse + typechecking: "+filename+" =============");
            Module world = CompUtil.parseEverything_fromFile(rep, null, filename);

            A4Options options = new A4Options();

            options.solver = A4Options.SatSolver.SAT4J;

            for (Command command: world.getAllCommands()) {

                System.out.println("=========== command : "+command+" ============");
                A4Solution ans = TranslateAlloyToKodkod.execute_command(rep, world.getAllReachableSigs(), command, options);

                System.out.println(ans);

                if (ans.satisfiable()) {
                    int cnt = 1;
                    A4Solution tmp = ans.next();
                    while ( tmp.satisfiable() ) {
                        tmp = tmp.next();
                        cnt++;
                    }
                    System.out.println("=========== "+cnt+" satisfiable solution found ============");

                    tmp = ans;
                    String[] outXml = new String[cnt];
                    for ( int i = 0; i < cnt; i++ ) {
                        outXml[i] = outputfilepath + "/" + out_fname + String.valueOf(i+1) + ".xml";
                        tmp.writeXML(outXml[i]);
                        tmp = tmp.next();
                    }
                }
            }
        }
    }
}

这是将成功执行的合金源示例：

module adressBook
open ordering [Book]

abstract sig Target {}
sig Addr extends Target {}
abstract sig Name extends Target {}
sig Alias, Group extends Name {}

sig Book {
    names: set Name,
    addr: names -> some Target 
}
{
    no n: Name | n in n.^(addr)
    all a: Alias | lone a.addr
}

pred add (b, b': Book, n: Name, t: Target) {
    t in Addr or some lookup [b, t]
    b'.addr = b.addr + n -> t
}

pred del (b, b': Book, n: Name, t: Target) {
    no b.addr.n or some n.(b.addr) - t
    b'.addr = b.addr - n -> t
}

fun lookup (b: Book, n: Name): set Addr {
    n.^(b.addr) & Addr
}

pred init (b: Book) {no b.addr}
fact traces {
    init [first]
    all b: Book - last | let b' = next [b] |
       some n: Name, t: Target | add [b, b', n, t] or del [b, b', n, t]
}

pred show {}
run show for 10

assert lookupYields {
    all b: Book, n: b.names | some lookup [b, n]
}
check lookupYields for 3 but 4 Book
check lookupYields for 6

这是将无法执行的合金源(它将抛出一个空指针)：

sig Element {}

one sig Group {
    elements: set Element,
    unit: one elements,
    mult: elements -> elements -> one elements,
    inv: elements -> one elements
}

fact NoRedundantElements {
    all e: Element | e in Group.elements
}

fact UnitLaw1 {
    all a: Group.elements | Group.mult [a] [Group.unit] = a
}

fact UnitLaw2 {
    all a: Group.elements |
    Group.mult [Group.unit] [a] = a
}

fact AssociativeLaw {
    all a: Group.elements | all b: Group.elements | all c:Group.elements |
    Group.mult [Group.mult [a] [b]] [c] = Group.mult [a] [Group.mult [b] [c]]
}

fact InvLaw1{
    all a: Group.elements | Group.mult [Group.inv[a]] [a] = Group.unit
}

assert InvLaw2 {
    all a: Group.elements | Group.mult [a] [Group.inv[a]] = Group.unit
}

check InvLaw2

assert Commutativity {
    all a: Group.elements | all b: Group.elements | Group.mult [a] [b] = Group.mult [b] [a]
}

check Commutativity for 6
pred subgroup (g: set Element, h: set Element) {
    (all a: g | a in h) and
    (Group.unit in g) and
    (all a, b: g | Group.mult [a] [b] in g) and
    (all a: g | Group.inv[a] in g)
}

pred regularSubgroup(n: set Element, g: set Element) {
    subgroup [n, g] and
    (all n0: n, g0: g | Group.mult [Group.mult [g0] [n0]] [Group.inv[g0]] in n)
}

pred main(n1: set Element, n2: set Element) {
    let g = Group.elements |
    regularSubgroup [n1, g] and
    (some g0: g | (not g0 in n1)) and
    regularSubgroup [n2, n1] and
    (some n10: n1 | (not n10 in n2)) and
    (not regularSubgroup [n2, g])
}
run main for 8

Answer 1

我认为这应该作为一个问题在https://github.com/alloytools/org.alloytools.alloy网站上报道吗？最好是用公关来修复它。