J'ai été en utilisant l'Alliage de l'API qui peut être écrit en Java. Mon objectif est de compiler en Alliage de modèle, de les afficher visuellement, et pour affiner la recherche pour les instances.
En ce moment, j'ai besoin de commande de la source de l'Alliage de la langue, qui peut exécuter correctement ou de jeter un NullPointerException, selon la source. J'ai vérifié le contenu de la classe de l'API dans le débogueur eclipse, mais je ne peut pas le comprendre correctement.
La question est: Le débogueur montre que TranslateAlloyToKodkod.execute_command se produit java.lang.NullPointerException.
Selon l' Alliage de la documentation de l'API,
TranslateAlloyToKodkod.execute_commandretourne null si l'utilisateur a choisi "enregistrer le FICHIER", comme le SAT solver, et non null si le solveur finitions de l'ensemble de problèmes et est soit satisfaisante ou unsatisfiable.
Mais je n'ai jamais changé d'exécuter les options "enregistrer le FICHIER", comme le solveur SAT. Pour votre information, le solveur, en Alliage d'analyseur de finitions de l'ensemble de la résolution de deux sources suivantes.
Vous laissez-moi savoir comment résoudre le problème?
Voici le code Java que j'ai créé, avec quelques ajouts à partir de l'API exemple:
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();
}
}
}
}
}
}
C'est l'échantillon de l'Alliage sources qui seront exécutées avec succès:
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
C'est l'Alliage de la source qui ne peut pas fonctionner (il va jeter un pointeur null):
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