Commit b543e6c6 authored by Alfons Laarman's avatar Alfons Laarman
Browse files

Option ignore atomics

Better for LTSmin POR and symbolic
parent 86170828
...@@ -35,6 +35,7 @@ import spins.promela.compiler.Preprocessor; ...@@ -35,6 +35,7 @@ import spins.promela.compiler.Preprocessor;
import spins.promela.compiler.Preprocessor.DefineMapping; import spins.promela.compiler.Preprocessor.DefineMapping;
import spins.promela.compiler.Proctype; import spins.promela.compiler.Proctype;
import spins.promela.compiler.Specification; import spins.promela.compiler.Specification;
import spins.promela.compiler.automaton.State;
import spins.promela.compiler.expression.Expression; import spins.promela.compiler.expression.Expression;
import spins.promela.compiler.ltsmin.LTSminPrinter; import spins.promela.compiler.ltsmin.LTSminPrinter;
import spins.promela.compiler.ltsmin.LTSminTreeWalker; import spins.promela.compiler.ltsmin.LTSminTreeWalker;
...@@ -59,8 +60,8 @@ import spins.promela.compiler.parser.TokenMgrError; ...@@ -59,8 +60,8 @@ import spins.promela.compiler.parser.TokenMgrError;
public class Compile { public class Compile {
private static Specification compile(final File promFile, private static Specification compile(final File promFile,
final boolean useStateMerging, final boolean useStateMerging,
final boolean verbose) { final Options opts) {
LTSminDebug debug = new LTSminDebug(verbose); LTSminDebug debug = new LTSminDebug(opts.verbose);
try { try {
Preprocessor.setFilename(promFile.getName()); Preprocessor.setFilename(promFile.getName());
String path = promFile.getAbsoluteFile().getParent(); String path = promFile.getAbsoluteFile().getParent();
...@@ -74,6 +75,19 @@ public class Compile { ...@@ -74,6 +75,19 @@ public class Compile {
report.stopTimer().sec()); report.stopTimer().sec());
debug.say(""); debug.say("");
if (opts.no_atomic) {
for (Proctype p : spec.getProcs()) {
for (State s : p.getAutomaton()) {
s.setInAtomic(false);
}
}
if (spec.getNever() != null) {
for (State s : spec.getNever().getAutomaton()) {
s.setInAtomic(false);
}
}
}
report.resetTimer().startTimer(); report.resetTimer().startTimer();
debug.say("Optimizing graphs..."); debug.say("Optimizing graphs...");
final GraphOptimizer[] optimizers = new GraphOptimizer[] { final GraphOptimizer[] optimizers = new GraphOptimizer[] {
...@@ -193,6 +207,10 @@ public class Compile { ...@@ -193,6 +207,10 @@ public class Compile {
"compilation process."); "compilation process.");
parser.addOption(verbose); parser.addOption(verbose);
final BooleanOption no_atomic = new BooleanOption('i',
"Ignore atomic sections (better for LTSmin POR and symbolic tools).");
parser.addOption(no_atomic);
parser.parse(args); parser.parse(args);
final List<String> files = parser.getFiles(); final List<String> files = parser.getFiles();
...@@ -248,8 +266,12 @@ public class Compile { ...@@ -248,8 +266,12 @@ public class Compile {
System.exit(0); System.exit(0);
} }
Options opts = new Options(verbose.isSet(), no_guards.isSet(),
must_write.isSet(), !no_cnf.isSet(),
nonever.isSet(), java.isSet(), no_atomic.isSet());
final Specification spec = final Specification spec =
Compile.compile(file, !optimalizations.isSet("3"), verbose.isSet()); Compile.compile(file, !optimalizations.isSet("3"), opts);
if (nonever.isSet()) spec.setNever(null); if (nonever.isSet()) spec.setNever(null);
if (spec == null) { if (spec == null) {
...@@ -275,9 +297,6 @@ public class Compile { ...@@ -275,9 +297,6 @@ public class Compile {
System.out.println(""); System.out.println("");
} }
Options opts = new Options(verbose.isSet(), no_guards.isSet(),
must_write.isSet(), !no_cnf.isSet(),
nonever.isSet(), java.isSet());
File outputDir = new File(System.getProperty("user.dir")); File outputDir = new File(System.getProperty("user.dir"));
if (dot.isSet()) { if (dot.isSet()) {
...@@ -380,13 +399,12 @@ public class Compile { ...@@ -380,13 +399,12 @@ public class Compile {
boolean ltsmin_ltl, Options opts, boolean ltsmin_ltl, Options opts,
Map<String, Expression> exports, Map<String, Expression> exports,
Expression progress) { Expression progress) {
LTSminTreeWalker walker = new LTSminTreeWalker(spec, ltsmin_ltl);
LTSminModel model = walker.createLTSminModel(name, opts, exports, progress);
String code = LTSminPrinter.generateCode(model, opts);
final File javaFile = new File(outputDir, name + ".spins.c"); final File javaFile = new File(outputDir, name + ".spins.c");
try { try {
final FileOutputStream fos = new FileOutputStream(javaFile); final FileOutputStream fos = new FileOutputStream(javaFile);
LTSminTreeWalker walker = new LTSminTreeWalker(spec, ltsmin_ltl);
LTSminModel model = walker.createLTSminModel(name, opts,
exports, progress);
String code = LTSminPrinter.generateCode(model, opts);
fos.write(code.getBytes()); fos.write(code.getBytes());
fos.flush(); fos.flush();
fos.close(); fos.close();
......
...@@ -98,7 +98,7 @@ public class LTSminDMWalker { ...@@ -98,7 +98,7 @@ public class LTSminDMWalker {
} }
private static RWMatrix DUMMY_MATRIX = new RWMatrix(null, null, null); private static RWMatrix DUMMY_MATRIX = new RWMatrix(null, null, null);
private static Options DUMMY_OPTIONS = new Options(false, false, false, false, false, false); private static Options DUMMY_OPTIONS = new Options(false, false, false, false, false, false, false);
private static Params sParams = new Params(null, null, DUMMY_MATRIX, private static Params sParams = new Params(null, null, DUMMY_MATRIX,
0, DUMMY_OPTIONS); 0, DUMMY_OPTIONS);
public static void walkOneGuard(LTSminModel model, DepMatrix dm, public static void walkOneGuard(LTSminModel model, DepMatrix dm,
......
...@@ -171,13 +171,14 @@ public class LTSminTreeWalker { ...@@ -171,13 +171,14 @@ public class LTSminTreeWalker {
public static class Options { public static class Options {
public Options(boolean verbose, boolean no_gm, boolean must_write, public Options(boolean verbose, boolean no_gm, boolean must_write,
boolean cnf, boolean nonever, boolean cnf, boolean nonever,
boolean unless_java_semantics) { boolean unless_java_semantics, boolean no_atomic) {
this.verbose = verbose; this.verbose = verbose;
this.no_gm = no_gm; this.no_gm = no_gm;
this.must_write = must_write; this.must_write = must_write;
this.cnf = cnf; this.cnf = cnf;
this.nonever = nonever; this.nonever = nonever;
this.unless_java_semantics = unless_java_semantics; this.unless_java_semantics = unless_java_semantics;
this.no_atomic = no_atomic;
} }
public boolean nonever = false; public boolean nonever = false;
public boolean verbose = false; public boolean verbose = false;
...@@ -185,6 +186,7 @@ public class LTSminTreeWalker { ...@@ -185,6 +186,7 @@ public class LTSminTreeWalker {
public boolean must_write = false; public boolean must_write = false;
public boolean cnf = false; public boolean cnf = false;
public boolean unless_java_semantics = false; public boolean unless_java_semantics = false;
public boolean no_atomic = false;
} }
TimeoutExpression timeout = null; TimeoutExpression timeout = null;
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment