Commit 5f8d058c authored by Alfons Laarman's avatar Alfons Laarman
Browse files

Ignore never by default

parent ecb14071
......@@ -148,9 +148,6 @@ public class Compile {
final OptionParser parser =
new OptionParser("java spins.Compiler", shortd, longd, true);
final BooleanOption nonever = new BooleanOption('n', "No never");
parser.addOption(nonever);
final StringOption define = new StringOption('D',
"sets preprocessor macro define value", true);
parser.addOption(define);
......@@ -195,7 +192,11 @@ public class Compile {
final BooleanOption total = new BooleanOption('T',
"make next-state a total function\n");
parser.addOption(total);
final BooleanOption useNever = new BooleanOption('N',
"Force use of never claim (slow; it is preferable to supply the LTL formula to LTSmin).\n");
parser.addOption(useNever);
final BooleanOption preprocessor = new BooleanOption('I',
"prints output of preprocessor\n");
parser.addOption(preprocessor);
......@@ -272,13 +273,18 @@ public class Compile {
}
Options opts = new Options(verbose.isSet(), no_guards.isSet(),
must_write.isSet(), !no_cnf.isSet(),
nonever.isSet(), java.isSet(), no_atomic.isSet(), total.isSet());
must_write.isSet(), !no_cnf.isSet(),
java.isSet(), no_atomic.isSet(), total.isSet());
final Specification spec =
Compile.compile(file, !optimalizations.isSet("3"), opts);
if (nonever.isSet()) spec.setNever(null);
if (!useNever.isSet() && spec.getNever() != null) {
LTSminTreeWalker.NEVER = false;
System.out.println("\nWARNING: Ignoring NEVER claim. Supply LTL formula to LTSmin or override with -N.\n\n");
spec.setNever(null);
}
if (spec == null) {
System.exit(-4);
}
......@@ -347,9 +353,11 @@ public class Compile {
Expression progress) {
final File dotFile = new File(outputDir, name + ".spins.dot");
LTSminTreeWalker walker = new LTSminTreeWalker(spec, ltsmin_ltl);
LTSminModel model = walker.createLTSminModel(name, opts,
exports, progress);
String out = "digraph {\n";
for (LTSminTransition t : model.getTransitions()) {
String s[] = t.getName().split(" X ");
......
......@@ -101,7 +101,7 @@ public class LTSminDMWalker {
}
private static RWMatrix DUMMY_MATRIX = new RWMatrix(null, null, null);
private static Options DUMMY_OPTIONS = new Options(false, false, 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,
0, DUMMY_OPTIONS);
public static void walkOneGuard(LTSminModel model, DepMatrix dm,
......
......@@ -40,13 +40,11 @@ import java.io.IOException;
import java.io.InputStreamReader;
import java.util.ArrayList;
import java.util.HashMap;
import java.util.HashSet;
import java.util.Iterator;
import java.util.LinkedList;
import java.util.List;
import java.util.ListIterator;
import java.util.Map;
import java.util.Set;
import spins.promela.compiler.Preprocessor;
import spins.promela.compiler.Preprocessor.DefineMapping;
......@@ -158,7 +156,7 @@ public class LTSminTreeWalker {
}
private final Specification spec;
static boolean NEVER;
public static boolean NEVER;
static boolean LTSMIN_LTL = false;
private LTSminDebug debug;
......@@ -173,19 +171,17 @@ public class LTSminTreeWalker {
public static class Options {
public Options(boolean verbose, boolean no_gm, boolean must_write,
boolean cnf, boolean nonever,
boolean cnf,
boolean unless_java_semantics, boolean no_atomic,
boolean total) {
this.verbose = verbose;
this.no_gm = no_gm;
this.must_write = must_write;
this.cnf = cnf;
this.nonever = nonever;
this.unless_java_semantics = unless_java_semantics;
this.no_atomic = no_atomic;
this.total = total;
}
public boolean nonever = false;
public boolean verbose = false;
public boolean no_gm = false;
public boolean must_write = false;
......@@ -206,7 +202,7 @@ public class LTSminTreeWalker {
Expression progress) {
this.debug = new LTSminDebug(opts.verbose);
UNLESS_JAVA_SEMANTICS = opts.unless_java_semantics;
debug.say("Generating next-state function ...");
debug.say_indent++;
LTSminProgress report = new LTSminProgress(debug).startTimer();
......@@ -485,7 +481,7 @@ public class LTSminTreeWalker {
id++;
}
}
if (null != spec.getNever()) {
if (NEVER) {
Proctype never = spec.getNever();
ProcInstance n = instantiate(never, -1, -1);
spec.setNever(n);
......@@ -1249,7 +1245,7 @@ public class LTSminTreeWalker {
}
if (never_t.getTo().isInAtomic() || never_t.getFrom().isInAtomic())
throw new AssertionError("Atomic in never claim not implemented");
throw new AssertionError("Atomic in never claim not implemented");
lt.addGuard(pcGuard(never_t.getFrom(), spec.getNever()));
createEnabledGuard(never_t, lt);
lt.addAction(assign(spec.getNever().getPC(),
......
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