Skip to content
Snippets Groups Projects
Commit 9dfbe644 authored by Fabian Vu's avatar Fabian Vu
Browse files

Fix a bug in IdentifierAnalyzer

parent 0cba584e
No related branches found
No related tags found
No related merge requests found
......@@ -194,7 +194,9 @@ public class IdentifierAnalyzer implements AbstractVisitor<Void, Void> {
@Override
public Void visitWhileSubstitutionNode(WhileSubstitutionNode node, Void expected) {
if(kind == Kind.READ) {
visitPredicateNode(node.getCondition(), expected);
}
visitSubstitutionNode(node.getBody(), expected);
return null;
}
......@@ -207,7 +209,9 @@ public class IdentifierAnalyzer implements AbstractVisitor<Void, Void> {
@Override
public Void visitIfOrSelectSubstitutionsNode(IfOrSelectSubstitutionsNode node, Void expected) {
if(kind == Kind.READ) {
node.getConditions().forEach(cond -> visitPredicateNode(cond, expected));
}
node.getSubstitutions().forEach(subs -> visitSubstitutionNode(subs, expected));
if(node.getElseSubstitution() != null) {
visitSubstitutionNode(node.getElseSubstitution(), expected);
......@@ -232,21 +236,27 @@ public class IdentifierAnalyzer implements AbstractVisitor<Void, Void> {
@Override
public Void visitConditionSubstitutionNode(ConditionSubstitutionNode node, Void expected) {
if(kind == Kind.READ) {
visitPredicateNode(node.getCondition(), expected);
}
visitSubstitutionNode(node.getSubstitution(), expected);
return null;
}
@Override
public Void visitAnySubstitution(AnySubstitutionNode node, Void expected) {
if(kind == Kind.READ) {
visitPredicateNode(node.getWherePredicate(), expected);
}
visitSubstitutionNode(node.getThenSubstitution(), expected);
return null;
}
@Override
public Void visitLetSubstitution(LetSubstitutionNode node, Void expected) {
if(kind == Kind.READ) {
visitPredicateNode(node.getPredicate(), expected);
}
visitSubstitutionNode(node.getBody(), expected);
return null;
}
......@@ -277,7 +287,9 @@ public class IdentifierAnalyzer implements AbstractVisitor<Void, Void> {
@Override
public Void visitSubstitutionIdentifierCallNode(OperationCallSubstitutionNode node, Void expected) {
if(kind == Kind.READ) {
node.getArguments().forEach(arg -> visitExprNode(arg, expected));
}
return null;
}
......
......@@ -141,7 +141,7 @@ public class ModelCheckingInfoGenerator {
List<String> variablesAsString = variables.stream().map(DeclarationNode::toString).collect(Collectors.toList());
Map<String, List<String>> writeInformation = new HashMap<>();
for (OperationNode operation : operations) {
IdentifierAnalyzer identifierAnalyzer = new IdentifierAnalyzer(IdentifierAnalyzer.Kind.WRITE);
IdentifierAnalyzer identifierAnalyzer = new IdentifierAnalyzer(IdentifierAnalyzer.Kind.READ);
PredicateNode guard = transitionGenerator.extractGuard(operation);
String opName = "_tr_" + nameHandler.handle(operation.getName());
List<String> identifiers = new ArrayList<>();
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment