| java.lang.Object
 gov.nasa.ltl.trans.LTL2Buchi
| LTL2Buchi | | public class LTL2Buchi (Code) | | DOCUMENT ME!
|
| reset_all_static | | public static void reset_all_static()(Code) | | |
| usage_warning | | public static void usage_warning()(Code) | | Commented out on 8/7/03 by Dimitra - apparently redundant now
since JPF not tied with Bandera any longer
public static Graph translate(String formula) throws ParseErrorException {
// To work with Bandera and JPF
boolean rewrite = true;
boolean superset = true;
boolean scc = true;
boolean bisim = true;
boolean fair_sim = true;
if (rewrite) {
try {
formula = Rewriter.rewrite(formula);
} catch (ParseErrorException e) {
throw new ParseErrorException(e.getMessage());
}
System.out.println("Rewritten as : " + formula);
System.out.println();
}
Graph gba = Translator.translate(formula);
//#ifdef BANDERA
try {
gba.save(System.getProperty("user.dir") + File.separator + "gba.sm");
} catch (IOException ex) {
}
//#else BANDERA
//#endif BANDERA
if (superset) {
gba = SuperSetReduction.reduce(gba);
//#ifdef BANDERA
try {
gba.save(
System.getProperty("user.dir") + File.separator + "ssr-gba.sm");
} catch (IOException ex) {
}
//#else BANDERA
//#endif BANDERA
}
Graph ba = Degeneralize.degeneralize(gba);
//#ifdef BANDERA
try {
ba.save(System.getProperty("user.dir") + File.separator + "ba.sm");
} catch (IOException ex) {
}
//#else BANDERA
//#endif BANDERA
if (scc) {
ba = SCCReduction.reduce(ba);
//#ifdef BANDERA
try {
ba.save(System.getProperty("user.dir") + File.separator + "scc-ba.sm");
} catch (IOException ex) {
}
//#else BANDERA
//#endif BANDERA
}
if (bisim) {
ba = Simplify.simplify(ba);
//#ifdef BANDERA
try {
ba.save(System.getProperty("user.dir") + File.separator + "bisim.sm");
} catch (IOException ex) {
}
//#else BANDERA
//#endif BANDERA
}
if (fair_sim) {
ba = SFSReduction.reduce(ba);
//#ifdef BANDERA
try {
ba.save(
System.getProperty("user.dir") + File.separator + "fairSim-ba.sm");
} catch (IOException ex) {
}
//#else BANDERA
//#endif BANDERA
}
System.out.println("***********************\n");
reset_all_static();
return ba;
}
|
|
|