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

Fix DM

parent 32769270
......@@ -398,12 +398,12 @@ public class LTSminDMWalker {
int m = 0;
// the read action itself:
for (Expression e : cra.getExprs()) {
Expression read = cra.isRandom() ? channelIndex(id, STAR, m) :
channelBottom(id, m);
if (e instanceof Identifier) { // otherwise it is a guard!
walkExpression(params, e, MarkAction.EMAY_MUST_WRITE);
walkExpression(params, read, MarkAction.EREAD);
}
Expression read = cra.isRandom() ? channelIndex(id, STAR, m) :
channelBottom(id, m);
walkExpression(params, read, MarkAction.EREAD);
m++;
}
if (!cra.isPoll()) {
......
......@@ -1022,10 +1022,12 @@ guard_loop: for (int g2 : guardInfo.getTransMatrix().get(t2)) {
int neverCoEnabled = 0;
DepMatrix g2g = model.getGuardInfo().getMatrix(G2G);
for (int g1 = 0; g1 < nlabels; g1++) {
co.setDependent(g1, g1);
Expression ge1 = guardInfo.get(g1).getExpr();
for (int g2 = g1+1; g2 < nlabels; g2++) {
report.updateProgress ();
if (isTimeout(model, co, g1, g2) || isTimeout(model, co, g2, g1)) {
......
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