Sono stato con la Lega di API che possono essere scritti in Java. Il mio obiettivo è quello di compilare in Lega modello, visualizzazione punto di vista visivo, e restringere il campo di ricerca per le istanze.
In questo momento, ho bisogno di comandare la sorgente della Lega di lingua, che si può eseguire correttamente o lanciare una NullPointerException, a seconda della fonte. Ho controllato il contenuto della classe API nel debugger di eclipse, ma io non riesco a capire bene.
Il problema è: Il debugger mostra che TranslateAlloyToKodkod.execute_command si verifica java.lang.NullPointerException.
Secondo la Lega la documentazione delle API,
TranslateAlloyToKodkod.execute_commandrestituisce null se l'utente sceglie "salva su FILE", come la SAT solver, e non null se il risolutore finiture tutto e di risoluzione è soddisfacibile o inappagabile.
Ma non ho mai cambiato eseguire le opzioni "salva su FILE", come la SAT solver. Per vostra informazione, il risolutore, analizzatore di Lega finiture in tutta la soluzione dei seguenti due fonti.
Vuoi fammi sapere come risolvere il problema?
Qui è il codice Java che ho creato, con alcune aggiunte all'API esempio:
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();
}
}
}
}
}
}
Questo è il campione della Lega di fonti che sarà eseguito con successo:
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
Questa è la Lega di origine che non è in grado di eseguire (sarà lanciare un puntatore 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