Commit 759a8c73 authored by Alfons Laarman's avatar Alfons Laarman

Fix guard containers and random channel read

parent 40b1da4b
......@@ -1272,25 +1272,25 @@ public class LTSminTreeWalker {
Identifier elem = id(elemVar(i));
Identifier buf = id(bufferVar(cv), constant(0), elem);
Identifier next = new Identifier(id, buf);
lt.addGuard(compare(PromelaConstants.EQ,next,expr));
lt.addGuard(eq(next,expr));
}
}
} else {
LTSminGuardOr or = new LTSminGuardOr();
// Compare constant arguments with channel content
Expression g = null;
for (int b = 0 ; b < cv.getType().getBufferSize(); b++) {
g = chanContentsGuard(id, b);
for (int b = 1 ; b <= cv.getType().getBufferSize(); b++) {
LTSminGuardAnd and = new LTSminGuardAnd();
and.addGuard(chanContentsGuard(id, PromelaConstants.EQ, b));
for (int i = 0; i < exprs.size(); i++) {
final Expression expr = exprs.get(i);
if (!(expr instanceof Identifier)) {
Identifier elem = id(elemVar(i));
Identifier buf = id(bufferVar(cv), constant(0), elem);
Identifier buf = id(bufferVar(cv), constant(b - 1), elem);
Identifier next = new Identifier(id, buf);
g = and(g, eq(next, expr));
and.addGuard(eq(next, expr));
}
}
or.addGuard(g);
or.addGuard(and);
}
lt.addGuard(or);
}
......
package spins.promela.compiler.ltsmin.matrix;
import static spins.promela.compiler.ltsmin.util.LTSminUtil.and;
import static spins.promela.compiler.ltsmin.util.LTSminUtil.bool;
import java.util.ArrayList;
import java.util.Iterator;
......@@ -43,7 +44,7 @@ public class LTSminGuardAnd extends LTSminGuardBase implements LTSminGuardContai
w.outdent();
w.appendLine(")");
} else {
w.appendLine("false _GAND_ ");
w.appendLine("true _GAND_ ");
}
}
......@@ -77,10 +78,10 @@ public class LTSminGuardAnd extends LTSminGuardBase implements LTSminGuardContai
Expression e = null;
for (LTSminGuardBase sub : this) {
Expression sube = sub.getExpression();
if (sube == null) continue;
if (sube == null) throw new AssertionError();
if (e == null) e = sube;
else e = and(sube, e);
}
return e;
return e == null ? bool(true) : e;
}
}
package spins.promela.compiler.ltsmin.matrix;
import static spins.promela.compiler.ltsmin.util.LTSminUtil.and;
import static spins.promela.compiler.ltsmin.util.LTSminUtil.not;
import static spins.promela.compiler.ltsmin.util.LTSminUtil.bool;
import static spins.promela.compiler.ltsmin.util.LTSminUtil.negate;
import java.util.ArrayList;
import java.util.Iterator;
......@@ -82,12 +83,10 @@ public class LTSminGuardNand extends LTSminGuardBase implements LTSminGuardConta
Expression e = null;
for (LTSminGuardBase sub : this) {
Expression sube = sub.getExpression();
if (sube == null) continue;
if (sube == null) throw new AssertionError();
if (e == null) e = sube;
else e = and(sube, e);
}
if (e != null)
e = not(e);
return e;
return e == null ? bool(false) : negate(e);
}
}
package spins.promela.compiler.ltsmin.matrix;
import static spins.promela.compiler.ltsmin.util.LTSminUtil.not;
import static spins.promela.compiler.ltsmin.util.LTSminUtil.bool;
import static spins.promela.compiler.ltsmin.util.LTSminUtil.negate;
import static spins.promela.compiler.ltsmin.util.LTSminUtil.or;
import java.util.ArrayList;
......@@ -44,7 +45,7 @@ public class LTSminGuardNor extends LTSminGuardBase implements LTSminGuardContai
w.outdent();
w.appendLine(")");
} else {
w.appendLine("false _GNOR_ ");
w.appendLine("true _GNOR_ ");
}
}
......@@ -78,12 +79,10 @@ public class LTSminGuardNor extends LTSminGuardBase implements LTSminGuardContai
Expression e = null;
for (LTSminGuardBase sub : this) {
Expression sube = sub.getExpression();
if (sube == null) continue;
if (sube == null) throw new AssertionError();
if (e == null) e = sube;
else e = or(sube, e);
}
if (e != null)
e = not(e);
return e;
return e == null ? bool(true) : negate(e);
}
}
package spins.promela.compiler.ltsmin.matrix;
import static spins.promela.compiler.ltsmin.util.LTSminUtil.bool;
import static spins.promela.compiler.ltsmin.util.LTSminUtil.or;
import java.util.ArrayList;
......@@ -77,10 +78,10 @@ public class LTSminGuardOr extends LTSminGuardBase implements LTSminGuardContain
Expression e = null;
for (LTSminGuardBase sub : this) {
Expression sube = sub.getExpression();
if (sube == null) continue;
if (sube == null) throw new AssertionError();
if (e == null) e = sube;
else e = or(sube, e);
}
return e;
return e == null ? bool(false) : e;
}
}
......@@ -122,14 +122,20 @@ public class LTSminTransition implements LTSminGuardContainer,
pcGuard.add((LTSminPCGuard) guard);
}
} else if (guard instanceof LTSminGuardAnd) {
for(LTSminGuardBase gb : (LTSminGuardContainer)guard)
addGuard(gb);
for (LTSminGuardBase gb : (LTSminGuardContainer)guard) {
Expression e = gb.getExpression();
if (e == null) continue;
addGuard(e);
}
} else if (guard instanceof LTSminGuardNand) {
LTSminGuardNand g = (LTSminGuardNand)guard;
addGuard(g.getExpression());
} else if (guard instanceof LTSminGuardNor) { // DeMorgan
for (LTSminGuardBase gb : (LTSminGuardContainer)guard)
addGuard(negate(gb.getExpression()));
for (LTSminGuardBase gb : (LTSminGuardContainer)guard) {
Expression e = gb.getExpression();
if (e == null) continue;
addGuard(negate(e));
}
} else if (guard instanceof LTSminGuardOr) {
LTSminGuardOr g = (LTSminGuardOr)guard;
addGuard(g.getExpression());
......@@ -207,7 +213,7 @@ public class LTSminTransition implements LTSminGuardContainer,
name += " X tau";
}
}
name += "]";
name += "] "+ original.getUnlessPriority();
return this.name = name;
}
......
......@@ -114,9 +114,21 @@ public class LTSminUtil {
}
public static Expression negate(Expression e) {
if (e instanceof BooleanExpression &&
e.getToken().kind == PromelaConstants.LNOT) {
return ((BooleanExpression) e).getExpr1();
try {
int c = e.getConstantValue();
return c != 0 ? bool(true) : bool(false);
} catch (ParseException e1) {}
if (e instanceof BooleanExpression) {
BooleanExpression be = (BooleanExpression) e;
switch (e.getToken().kind) {
case PromelaConstants.LNOT:
return be.getExpr1();
case PromelaConstants.LOR:
return and(negate(be.getExpr1()), negate(be.getExpr2()));
case PromelaConstants.LAND:
return or(negate(be.getExpr1()), negate(be.getExpr2()));
default: throw new AssertionError("Unknown arithmetic expression kind: "+ e.getToken());
}
} else if (e instanceof CompareExpression) {
CompareExpression ae = (CompareExpression)e;
switch(ae.getToken().kind) {
......@@ -126,7 +138,7 @@ public class LTSminUtil {
case NEQ: return new CompareExpression(ae, EQ);
case GT: return new CompareExpression(ae, LTE);
case GTE: return new CompareExpression(ae, LT);
default: throw new AssertionError("Unknown arithmetic expression kind: "+ ae.getToken());
default: throw new AssertionError("Unknown arithmetic expression kind: "+ e.getToken());
}
} else {
return not(e);
......@@ -161,7 +173,8 @@ public class LTSminUtil {
}
public static ConstantExpression bool(boolean b) {
return new ConstantExpression(new Token(PromelaConstants.BOOL, ""+b), b?1:0);
Token t = new Token(b?PromelaConstants.TRUE:PromelaConstants.FALSE, ""+b);
return new ConstantExpression(t, b?1:0);
}
public static ConstantExpression constant(int nr) {
......
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