Commit c344d3ed authored by Alfons Laarman's avatar Alfons Laarman

Total transition function with -T (see LTSmin --local

parent bfca30be
...@@ -191,7 +191,12 @@ public class Compile { ...@@ -191,7 +191,12 @@ public class Compile {
"sets output to textbook LTL semantics \n"); "sets output to textbook LTL semantics \n");
parser.addOption(textbook_ltl); parser.addOption(textbook_ltl);
final BooleanOption preprocessor = new BooleanOption('I',
final BooleanOption total = new BooleanOption('T',
"make next-state a total function\n");
parser.addOption(total);
final BooleanOption preprocessor = new BooleanOption('I',
"prints output of preprocessor\n"); "prints output of preprocessor\n");
parser.addOption(preprocessor); parser.addOption(preprocessor);
...@@ -268,7 +273,7 @@ public class Compile { ...@@ -268,7 +273,7 @@ public class Compile {
Options opts = new Options(verbose.isSet(), no_guards.isSet(), Options opts = new Options(verbose.isSet(), no_guards.isSet(),
must_write.isSet(), !no_cnf.isSet(), must_write.isSet(), !no_cnf.isSet(),
nonever.isSet(), java.isSet(), no_atomic.isSet()); nonever.isSet(), java.isSet(), no_atomic.isSet(), total.isSet());
final Specification spec = final Specification spec =
Compile.compile(file, !optimalizations.isSet("3"), opts); Compile.compile(file, !optimalizations.isSet("3"), opts);
......
...@@ -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, false); private static Options DUMMY_OPTIONS = new Options(false, 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,
......
...@@ -150,14 +150,13 @@ public class LTSminPrinter { ...@@ -150,14 +150,13 @@ public class LTSminPrinter {
static int n_active = 0; static int n_active = 0;
public static String generateCode(LTSminModel model, Options opts) { public static String generateCode(LTSminModel model, Options opts) {
StringWriter w = new StringWriter(); StringWriter w = new StringWriter(opts);
LTSminPrinter.generateModel(w, model, opts. no_gm); LTSminPrinter.generateModel(w, model);
return w.toString(); return w.toString();
} }
private static void generateModel(StringWriter w, LTSminModel model, private static void generateModel(StringWriter w, LTSminModel model) {
boolean no_gm) { if (w.options.no_gm) {
if (no_gm) {
w.appendLine("#define SPINS_TEST_CODE").appendLine(""); w.appendLine("#define SPINS_TEST_CODE").appendLine("");
} }
...@@ -176,9 +175,9 @@ public class LTSminPrinter { ...@@ -176,9 +175,9 @@ public class LTSminPrinter {
generateDepMatrix(w, model.getAtomicDepMatrix().read, DM_ACTIONS_NAME); generateDepMatrix(w, model.getAtomicDepMatrix().read, DM_ACTIONS_NAME);
generateDepMatrix(w, model.getDepMatrix(), DM_NAME); generateDepMatrix(w, model.getDepMatrix(), DM_NAME);
generateDMFunctions(w, model.getDepMatrix()); generateDMFunctions(w, model.getDepMatrix());
generateGuardMatrices(w, model, no_gm); generateGuardMatrices(w, model, w.options.no_gm);
generateOtherMatrices(w, model); generateOtherMatrices(w, model);
generateGuardFunctions(w, model, no_gm); generateGuardFunctions(w, model, w.options.no_gm);
generateStateDescriptors(w, model); generateStateDescriptors(w, model);
generateEdgeDescriptors(w, model); generateEdgeDescriptors(w, model);
...@@ -627,10 +626,13 @@ public class LTSminPrinter { ...@@ -627,10 +626,13 @@ public class LTSminPrinter {
List<Integer> list = model.getGuardInfo().getTransMatrix().get(t.getGroup()); List<Integer> list = model.getGuardInfo().getTransMatrix().get(t.getGroup());
for (int g : list) { for (int g : list) {
w.append("__guards["+ g +"]"); w.append("__guards["+ g +"]");
if (w.options.total)
w.append(" == 1");
if (list.size() != ++guards) { if (list.size() != ++guards) {
w.append(" &&").appendPostfix().appendPrefix(); w.append(" &&").appendPostfix().appendPrefix();
} }
} } else { }
} else {
LTSminGuardBase last = t.getGuards().get(t.getGuards().size() - 1); LTSminGuardBase last = t.getGuards().get(t.getGuards().size() - 1);
for (LTSminGuardBase g : t.getGuards()) { for (LTSminGuardBase g : t.getGuards()) {
guards += generateGuard(w, model, g, in(model)); guards += generateGuard(w, model, g, in(model));
...@@ -774,6 +776,15 @@ public class LTSminPrinter { ...@@ -774,6 +776,15 @@ public class LTSminPrinter {
LTSminGuardBase guard, LTSminPointer state) { LTSminGuardBase guard, LTSminPointer state) {
Expression expression = guard.getExpression(); Expression expression = guard.getExpression();
if (expression == null) return 0; if (expression == null) return 0;
if (w.options.total) {
StringWriter w2 = new StringWriter(w);
generateMaybe(w2, expression, state);
String maybe = w2.toString();
if (maybe.length() != 0) {
w.append("(false "+ maybe +") == 0 && ");
}
}
generateExpression(w, expression, state); generateExpression(w, expression, state);
return 1; return 1;
} }
...@@ -908,23 +919,32 @@ public class LTSminPrinter { ...@@ -908,23 +919,32 @@ public class LTSminPrinter {
activeExpr = calc(PromelaConstants.PLUS, e, activeExpr); activeExpr = calc(PromelaConstants.PLUS, e, activeExpr);
} }
} }
String activeStr = generateExpression(model, activeExpr); String activeStr = generateExpression(model, activeExpr);
++n_active; ++n_active;
w.appendLine("int __active_" + n_active + " = "+ activeStr +";"); w.appendLine("int __active_" + n_active + " = "+ activeStr +";");
w.appendLine("if (__active_" + n_active + " >= "+ re.getProctype().getInstances().size() +") {"); w.appendLine("if (__active_" + n_active + " >= "+ re.getProctype().getInstances().size() +") {");
w.appendLine(" printf (\"Error, too many instances for "+ instance.getTypeName() +": %d.\\n\", __active_" + n_active + ");"); if (!w.options.total) {
w.appendLine(" printf (\"Exiting on '"+ re +"'.\\n\");"); w.appendLine(" printf (\"Error, too many instances for "+ instance.getTypeName() +": %d.\\n\", __active_" + n_active + ");");
w.appendLine(" exit (1);"); w.appendLine(" printf (\"Exiting on '"+ re +"'.\\n\");");
w.appendLine(" exit (1);");
} else {
w.appendLine(" return 0;");
}
w.appendLine("}"); w.appendLine("}");
//} //}
StringWriter w2 = new StringWriter(w); StringWriter w2 = new StringWriter(w);
//only one dynamic process supported atm //only one dynamic process supported atm
w2.appendLine("if (-1 != "+ printPC(instance, out(model)) +") {"); w2.appendLine("if (-1 != "+ printPC(instance, out(model)) +") {");
w2.appendLine(" printf (\"Instance %d of process "+ instance.getTypeName() +" was already started.\\n\", __active_" + n_active + ");"); if (!w.options.total) {
w2.appendLine(" printf (\"Exiting on '"+ re +"'.\\n\");"); w2.appendLine(" printf (\"Instance %d of process "+ instance.getTypeName() +" was already started.\\n\", __active_" + n_active + ");");
w2.appendLine(" exit (1);"); w2.appendLine(" printf (\"Exiting on '"+ re +"'.\\n\");");
w2.appendLine(" exit (1);");
} else {
w2.appendLine(" return 0;");
}
w2.appendLine("}"); w2.appendLine("}");
//set pid //set pid
...@@ -983,8 +1003,11 @@ public class LTSminPrinter { ...@@ -983,8 +1003,11 @@ public class LTSminPrinter {
} catch (LTSminRendezVousException e) { } catch (LTSminRendezVousException e) {
throw new AssertionError(e); throw new AssertionError(e);
} }
int count = generateGuard(w, model, ag, out(model)); if (ag.getExpression() == null)
if (count == 0) w.append("true"); w.append("true");
else {
generateExpression(w, ag.getExpression(), out(model));
}
w.append(") {").appendPostfix(); w.append(") {").appendPostfix();
w.indent(); w.indent();
for (Action act : seq) { for (Action act : seq) {
...@@ -1714,7 +1737,7 @@ public class LTSminPrinter { ...@@ -1714,7 +1737,7 @@ public class LTSminPrinter {
w.appendLine(""); w.appendLine("");
} }
private static int generateBound(StringWriter w, LTSminModel model, Expression e, LTSminPointer state) { private static int generateBound(StringWriter w, Expression e, LTSminPointer state) {
if (e == null) return 0; if (e == null) return 0;
if (e instanceof LTSminIdentifier) { if (e instanceof LTSminIdentifier) {
} else if (e instanceof Identifier) { } else if (e instanceof Identifier) {
...@@ -1733,29 +1756,29 @@ public class LTSminPrinter { ...@@ -1733,29 +1756,29 @@ public class LTSminPrinter {
Expression ex1 = ae.getExpr1(); Expression ex1 = ae.getExpr1();
Expression ex2 = ae.getExpr2(); Expression ex2 = ae.getExpr2();
Expression ex3 = ae.getExpr3(); Expression ex3 = ae.getExpr3();
generateDiv(w, model, e, state); generateDiv(w,e, state);
generateMaybe(w, model, ex1, state); generateMaybe(w, ex1, state);
generateMaybe(w, model, ex2, state); generateMaybe(w, ex2, state);
generateMaybe(w, model, ex3, state); generateMaybe(w, ex3, state);
} else if (e instanceof BooleanExpression) { } else if (e instanceof BooleanExpression) {
BooleanExpression ae = (BooleanExpression) e; BooleanExpression ae = (BooleanExpression) e;
Expression ex1 = ae.getExpr1(); Expression ex1 = ae.getExpr1();
Expression ex2 = ae.getExpr2(); Expression ex2 = ae.getExpr2();
generateMaybe(w, model, ex1, state); generateMaybe(w, ex1, state);
generateMaybe(w, model, ex2, state); generateMaybe(w, ex2, state);
} else if (e instanceof CompareExpression) { } else if (e instanceof CompareExpression) {
CompareExpression ae = (CompareExpression) e; CompareExpression ae = (CompareExpression) e;
Expression ex1 = ae.getExpr1(); Expression ex1 = ae.getExpr1();
Expression ex2 = ae.getExpr2(); Expression ex2 = ae.getExpr2();
generateMaybe(w, model, ex1, state); generateMaybe(w, ex1, state);
generateMaybe(w, model, ex2, state); generateMaybe(w, ex2, state);
} else if (e instanceof TranslatableExpression) { } else if (e instanceof TranslatableExpression) {
TranslatableExpression te = (TranslatableExpression) e; TranslatableExpression te = (TranslatableExpression) e;
generateMaybe(w, model, te.translate(), state); generateMaybe(w, te.translate(), state);
} else if (e instanceof ChannelReadExpression) { } else if (e instanceof ChannelReadExpression) {
ChannelReadExpression cre = (ChannelReadExpression) e; ChannelReadExpression cre = (ChannelReadExpression) e;
for (Expression ex : cre.getExprs()) { for (Expression ex : cre.getExprs()) {
generateMaybe(w, model, ex, state); generateMaybe(w, ex, state);
} }
} else if (e instanceof MTypeReference) { } else if (e instanceof MTypeReference) {
} else if (e instanceof ConstantExpression) { } else if (e instanceof ConstantExpression) {
...@@ -1774,13 +1797,13 @@ public class LTSminPrinter { ...@@ -1774,13 +1797,13 @@ public class LTSminPrinter {
return 1; return 1;
} }
private static int generateDiv(StringWriter w, LTSminModel model, Expression e, LTSminPointer state) { private static int generateDiv(StringWriter w, Expression e, LTSminPointer state) {
if (e == null) return 0; if (e == null) return 0;
if (e instanceof LTSminIdentifier) { if (e instanceof LTSminIdentifier) {
} else if (e instanceof Identifier) { } else if (e instanceof Identifier) {
Identifier id = (Identifier) e; Identifier id = (Identifier) e;
generateMaybe(w, model, id.getArrayExpr(), state); generateMaybe(w, id.getArrayExpr(), state);
generateBound(w, model, id, state); generateBound(w, id, state);
} else if (e instanceof AritmicExpression) { } else if (e instanceof AritmicExpression) {
AritmicExpression ae = (AritmicExpression) e; AritmicExpression ae = (AritmicExpression) e;
Expression ex2 = ae.getExpr2(); Expression ex2 = ae.getExpr2();
...@@ -1793,21 +1816,21 @@ public class LTSminPrinter { ...@@ -1793,21 +1816,21 @@ public class LTSminPrinter {
BooleanExpression ae = (BooleanExpression) e; BooleanExpression ae = (BooleanExpression) e;
Expression ex1 = ae.getExpr1(); Expression ex1 = ae.getExpr1();
Expression ex2 = ae.getExpr2(); Expression ex2 = ae.getExpr2();
generateMaybe(w, model, ex1, state); generateMaybe(w, ex1, state);
generateMaybe(w, model, ex2, state); generateMaybe(w, ex2, state);
} else if (e instanceof CompareExpression) { } else if (e instanceof CompareExpression) {
CompareExpression ae = (CompareExpression) e; CompareExpression ae = (CompareExpression) e;
Expression ex1 = ae.getExpr1(); Expression ex1 = ae.getExpr1();
Expression ex2 = ae.getExpr2(); Expression ex2 = ae.getExpr2();
generateMaybe(w, model, ex1, state); generateMaybe(w, ex1, state);
generateMaybe(w, model, ex2, state); generateMaybe(w, ex2, state);
} else if (e instanceof TranslatableExpression) { } else if (e instanceof TranslatableExpression) {
TranslatableExpression te = (TranslatableExpression) e; TranslatableExpression te = (TranslatableExpression) e;
generateMaybe(w, model, te.translate(), state); generateMaybe(w,te.translate(), state);
} else if (e instanceof ChannelReadExpression) { } else if (e instanceof ChannelReadExpression) {
ChannelReadExpression cre = (ChannelReadExpression) e; ChannelReadExpression cre = (ChannelReadExpression) e;
for (Expression ex : cre.getExprs()) { for (Expression ex : cre.getExprs()) {
generateMaybe(w, model, ex, state); generateMaybe(w, ex, state);
} }
} else if (e instanceof MTypeReference) { } else if (e instanceof MTypeReference) {
} else if (e instanceof ConstantExpression) { } else if (e instanceof ConstantExpression) {
...@@ -1826,42 +1849,42 @@ public class LTSminPrinter { ...@@ -1826,42 +1849,42 @@ public class LTSminPrinter {
return 1; return 1;
} }
private static int generateMaybe(StringWriter w, LTSminModel model, Expression e, LTSminPointer state) { private static int generateMaybe(StringWriter w, Expression e, LTSminPointer state) {
if (e == null) return 0; if (e == null) return 0;
if (e instanceof LTSminIdentifier) { if (e instanceof LTSminIdentifier) {
} else if (e instanceof Identifier) { } else if (e instanceof Identifier) {
Identifier id = (Identifier) e; Identifier id = (Identifier) e;
generateMaybe(w, model, id.getArrayExpr(), state); generateMaybe(w, id.getArrayExpr(), state);
generateBound(w, model, id, state); generateBound(w, id, state);
} else if (e instanceof AritmicExpression) { } else if (e instanceof AritmicExpression) {
AritmicExpression ae = (AritmicExpression) e; AritmicExpression ae = (AritmicExpression) e;
Expression ex1 = ae.getExpr1(); Expression ex1 = ae.getExpr1();
Expression ex2 = ae.getExpr2(); Expression ex2 = ae.getExpr2();
Expression ex3 = ae.getExpr3(); Expression ex3 = ae.getExpr3();
generateDiv(w, model, e, state); generateDiv(w,e, state);
generateMaybe(w, model, ex1, state); generateMaybe(w, ex1, state);
generateMaybe(w, model, ex2, state); generateMaybe(w, ex2, state);
generateMaybe(w, model, ex3, state); generateMaybe(w, ex3, state);
} else if (e instanceof BooleanExpression) { } else if (e instanceof BooleanExpression) {
BooleanExpression ae = (BooleanExpression) e; BooleanExpression ae = (BooleanExpression) e;
Expression ex1 = ae.getExpr1(); Expression ex1 = ae.getExpr1();
Expression ex2 = ae.getExpr2(); Expression ex2 = ae.getExpr2();
generateMaybe(w, model, ex1, state); generateMaybe(w, ex1, state);
generateMaybe(w, model, ex2, state); generateMaybe(w, ex2, state);
} else if (e instanceof CompareExpression) { } else if (e instanceof CompareExpression) {
CompareExpression ae = (CompareExpression) e; CompareExpression ae = (CompareExpression) e;
Expression ex1 = ae.getExpr1(); Expression ex1 = ae.getExpr1();
Expression ex2 = ae.getExpr2(); Expression ex2 = ae.getExpr2();
generateMaybe(w, model, ex1, state); generateMaybe(w, ex1, state);
generateMaybe(w, model, ex2, state); generateMaybe(w, ex2, state);
} else if (e instanceof TranslatableExpression) { } else if (e instanceof TranslatableExpression) {
TranslatableExpression te = (TranslatableExpression) e; TranslatableExpression te = (TranslatableExpression) e;
generateMaybe(w, model, te.translate(), state); generateMaybe(w, te.translate(), state);
} else if (e instanceof ChannelReadExpression) { } else if (e instanceof ChannelReadExpression) {
ChannelReadExpression cre = (ChannelReadExpression) e; ChannelReadExpression cre = (ChannelReadExpression) e;
for (Expression ex : cre.getExprs()) { for (Expression ex : cre.getExprs()) {
generateMaybe(w, model, ex, state); generateMaybe(w, ex, state);
} }
} else if (e instanceof MTypeReference) { } else if (e instanceof MTypeReference) {
} else if (e instanceof ConstantExpression) { } else if (e instanceof ConstantExpression) {
...@@ -1929,7 +1952,7 @@ public class LTSminPrinter { ...@@ -1929,7 +1952,7 @@ public class LTSminPrinter {
for (int g = gm.getNumberOfGuards(); g < gm.getNumberOfLabels(); ++g) { for (int g = gm.getNumberOfGuards(); g < gm.getNumberOfLabels(); ++g) {
w.appendPrefix(); w.appendPrefix();
w.append("case ").append(g).append(": return "); w.append("case ").append(g).append(": return ");
generateGuard(w, model, gm.getLabel(g), in(model)); generateExpression(w, gm.getLabel(g).getExpr(), in(model));
w.append(";"); w.append(";");
w.appendPostfix(); w.appendPostfix();
} }
...@@ -1969,7 +1992,7 @@ public class LTSminPrinter { ...@@ -1969,7 +1992,7 @@ public class LTSminPrinter {
for (int g = gm.getNumberOfGuards(); g < gm.getNumberOfLabels(); ++g) { for (int g = gm.getNumberOfGuards(); g < gm.getNumberOfLabels(); ++g) {
w.appendPrefix(); w.appendPrefix();
w.append("label[").append(g).append("] = "); w.append("label[").append(g).append("] = ");
generateGuard(w, model, gm.getLabel(g), in(model)); generateExpression(w, gm.getLabel(g).getExpr(), in(model));
w.append(";"); w.append(";");
w.appendPostfix(); w.appendPostfix();
} }
...@@ -2079,7 +2102,7 @@ public class LTSminPrinter { ...@@ -2079,7 +2102,7 @@ public class LTSminPrinter {
GuardInfo gm = model.getGuardInfo(); GuardInfo gm = model.getGuardInfo();
StringWriter w2 = new StringWriter(w); StringWriter w2 = new StringWriter(w);
generateMaybe(w2, model, gm.getLabel(g).getExpr(), in(model)); generateMaybe(w2, gm.getLabel(g).getExpr(), in(model));
String maybe = w2.toString(); String maybe = w2.toString();
if (maybe.length() != 0) { if (maybe.length() != 0) {
...@@ -2088,7 +2111,7 @@ public class LTSminPrinter { ...@@ -2088,7 +2111,7 @@ public class LTSminPrinter {
w.append(") ? 2 :").appendLine(); w.append(") ? 2 :").appendLine();
w.appendPrefix().appendPrefix().appendPrefix(); w.appendPrefix().appendPrefix().appendPrefix();
} }
generateGuard(w, model, gm.getLabel(g), in(model)); generateExpression(w, gm.getLabel(g).getExpr(), in(model));
w.append(" != 0;"); w.append(" != 0;");
w.appendPostfix(); w.appendPostfix();
} }
......
...@@ -172,7 +172,8 @@ public class LTSminTreeWalker { ...@@ -172,7 +172,8 @@ 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 no_atomic) { boolean unless_java_semantics, boolean no_atomic,
boolean total) {
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;
...@@ -180,6 +181,7 @@ public class LTSminTreeWalker { ...@@ -180,6 +181,7 @@ public class LTSminTreeWalker {
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; this.no_atomic = no_atomic;
this.total = total;
} }
public boolean nonever = false; public boolean nonever = false;
public boolean verbose = false; public boolean verbose = false;
...@@ -188,6 +190,7 @@ public class LTSminTreeWalker { ...@@ -188,6 +190,7 @@ public class LTSminTreeWalker {
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; public boolean no_atomic = false;
public boolean total = false;
} }
TimeoutExpression timeout = null; TimeoutExpression timeout = null;
......
...@@ -14,6 +14,8 @@ ...@@ -14,6 +14,8 @@
package spins.util; package spins.util;
import spins.promela.compiler.ltsmin.LTSminTreeWalker.Options;
/** /**
* The StringWriter can be used as a replacement for the {@link StringBuilder}, * The StringWriter can be used as a replacement for the {@link StringBuilder},
* but with support for adding lines with prefixes (indentation) and * but with support for adding lines with prefixes (indentation) and
...@@ -50,6 +52,13 @@ public final class StringWriter { ...@@ -50,6 +52,13 @@ public final class StringWriter {
this("\t", System.getProperty("line.separator"), size); this("\t", System.getProperty("line.separator"), size);
} }
public Options options = null;
public StringWriter(Options opts) {
this();
options = opts;
}
/** /**
* Constructor of StringWriter. * Constructor of StringWriter.
* *
...@@ -92,9 +101,10 @@ public final class StringWriter { ...@@ -92,9 +101,10 @@ public final class StringWriter {
public StringWriter(StringWriter w) { public StringWriter(StringWriter w) {
this(w.preprefix, w.prefix, w.postfix, w.buffer.length); this(w.preprefix, w.prefix, w.postfix, w.buffer.length);
this.indented = w.indented; this.indented = w.indented;
this.options = w.options;
} }
/** /**
* Appends the object converted to a String to this StringWriter. * Appends the object converted to a String to this StringWriter.
* *
* @param obj * @param obj
......
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