He estado usando la Aleación de la API que puede ser escrito en Java. Mi objetivo es recopilar la Aleación modelo, mostrar visualmente, y limitar la búsqueda de instancias.
En este momento, necesito comando de la fuente de la Aleación de lenguaje, que puede ejecutar correctamente o lanzar un NullPointerException, dependiendo de la fuente. He comprobado el contenido de la API de la clase en el depurador de eclipse, pero no puedo entender correctamente.
La cuestión es: El depurador muestra que TranslateAlloyToKodkod.execute_command se produce java.lang.NullPointerException.
De acuerdo a la Aleación de la documentación de la API,
TranslateAlloyToKodkod.execute_commanddevuelve null si el usuario selecciona "guardar ARCHIVO" como el SAT solver, y no null si el solucionador de acabados de la totalidad de problemas y es válido o unsatisfiable.
Pero nunca he cambiado ejecutar opciones de "guardar en ARCHIVO" como el SAT solver. Para su información, el solver, Alloy analyzer acabados de toda la solución de los siguientes dos fuentes.
Podría usted, hágamelo saber cómo solucionar el problema?
Aquí está el código Java que he creado, con algunas adiciones de la API de ejemplo:
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();
}
}
}
}
}
}
Esta es la muestra de Aleación de fuentes que serán ejecutados con éxito:
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
Esta es la Aleación de la fuente que no se ejecuta (se va a lanzar un puntero 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