diff --git a/src/main/java/de/tlc4b/analysis/MachineContext.java b/src/main/java/de/tlc4b/analysis/MachineContext.java index 9b1012a065a654fd21ba6653b36546ee4c009207..b80100df54fb6b0e31bdbd3341485afe07eb0335 100644 --- a/src/main/java/de/tlc4b/analysis/MachineContext.java +++ b/src/main/java/de/tlc4b/analysis/MachineContext.java @@ -1,70 +1,10 @@ package de.tlc4b.analysis; -import java.util.ArrayList; -import java.util.Collection; -import java.util.HashSet; -import java.util.Hashtable; -import java.util.LinkedHashMap; -import java.util.LinkedList; -import java.util.List; +import java.util.*; import java.util.Map.Entry; import de.be4.classicalb.core.parser.analysis.DepthFirstAdapter; -import de.be4.classicalb.core.parser.node.AAbstractConstantsMachineClause; -import de.be4.classicalb.core.parser.node.AAbstractMachineParseUnit; -import de.be4.classicalb.core.parser.node.AAnySubstitution; -import de.be4.classicalb.core.parser.node.AAssertionsMachineClause; -import de.be4.classicalb.core.parser.node.AAssignSubstitution; -import de.be4.classicalb.core.parser.node.AComprehensionSetExpression; -import de.be4.classicalb.core.parser.node.AConcreteVariablesMachineClause; -import de.be4.classicalb.core.parser.node.AConstantsMachineClause; -import de.be4.classicalb.core.parser.node.AConstraintsMachineClause; -import de.be4.classicalb.core.parser.node.ADeferredSetSet; -import de.be4.classicalb.core.parser.node.ADefinitionExpression; -import de.be4.classicalb.core.parser.node.ADefinitionPredicate; -import de.be4.classicalb.core.parser.node.ADefinitionSubstitution; -import de.be4.classicalb.core.parser.node.ADefinitionsMachineClause; -import de.be4.classicalb.core.parser.node.AEnumeratedSetSet; -import de.be4.classicalb.core.parser.node.AEventBComprehensionSetExpression; -import de.be4.classicalb.core.parser.node.AExistsPredicate; -import de.be4.classicalb.core.parser.node.AExpressionDefinitionDefinition; -import de.be4.classicalb.core.parser.node.AForallPredicate; -import de.be4.classicalb.core.parser.node.AFunctionExpression; -import de.be4.classicalb.core.parser.node.AGeneralProductExpression; -import de.be4.classicalb.core.parser.node.AGeneralSumExpression; -import de.be4.classicalb.core.parser.node.AIdentifierExpression; -import de.be4.classicalb.core.parser.node.AInitialisationMachineClause; -import de.be4.classicalb.core.parser.node.AInvariantMachineClause; -import de.be4.classicalb.core.parser.node.ALambdaExpression; -import de.be4.classicalb.core.parser.node.ALetSubstitution; -import de.be4.classicalb.core.parser.node.AMachineHeader; -import de.be4.classicalb.core.parser.node.AMachineReferenceNoParams; -import de.be4.classicalb.core.parser.node.AOpSubstitution; -import de.be4.classicalb.core.parser.node.AOperation; -import de.be4.classicalb.core.parser.node.AOperationsMachineClause; -import de.be4.classicalb.core.parser.node.APredicateDefinitionDefinition; -import de.be4.classicalb.core.parser.node.APredicateParseUnit; -import de.be4.classicalb.core.parser.node.APrimedIdentifierExpression; -import de.be4.classicalb.core.parser.node.APropertiesMachineClause; -import de.be4.classicalb.core.parser.node.AQuantifiedIntersectionExpression; -import de.be4.classicalb.core.parser.node.AQuantifiedUnionExpression; -import de.be4.classicalb.core.parser.node.ARecEntry; -import de.be4.classicalb.core.parser.node.ARecordFieldExpression; -import de.be4.classicalb.core.parser.node.ASeesMachineClause; -import de.be4.classicalb.core.parser.node.ASetsContextClause; -import de.be4.classicalb.core.parser.node.ASubstitutionDefinitionDefinition; -import de.be4.classicalb.core.parser.node.AVariablesMachineClause; -import de.be4.classicalb.core.parser.node.Node; -import de.be4.classicalb.core.parser.node.PDefinition; -import de.be4.classicalb.core.parser.node.PExpression; -import de.be4.classicalb.core.parser.node.PMachineClause; -import de.be4.classicalb.core.parser.node.PMachineHeader; -import de.be4.classicalb.core.parser.node.PMachineReferenceNoParams; -import de.be4.classicalb.core.parser.node.POperation; -import de.be4.classicalb.core.parser.node.PPredicate; -import de.be4.classicalb.core.parser.node.PSet; -import de.be4.classicalb.core.parser.node.Start; -import de.be4.classicalb.core.parser.node.TIdentifierLiteral; +import de.be4.classicalb.core.parser.node.*; import de.be4.classicalb.core.parser.util.Utils; import de.tlc4b.MP; import de.tlc4b.TLC4BGlobals; @@ -74,6 +14,8 @@ import de.tlc4b.exceptions.ScopeException; import de.tlc4b.ltl.LTLBPredicate; import de.tlc4b.ltl.LTLFormulaVisitor; +import static de.tlc4b.util.UtilMethods.getIdentifierExpression; + public class MachineContext extends DepthFirstAdapter { private String machineName; @@ -419,58 +361,37 @@ public class MachineContext extends DepthFirstAdapter { exist(node.getIdentifier()); enumeratedSets.put(name, node); } - List<PExpression> copy = new ArrayList<>(node.getElements()); - for (PExpression e : copy) { - AIdentifierExpression v = (AIdentifierExpression) e; - String name = Utils.getTIdentifierListAsString(v.getIdentifier()); - exist(v.getIdentifier()); - enumValues.put(name, v); - } + extractIdentifierExpressions(new ArrayList<>(node.getElements()), enumValues); } @Override public void caseAConstantsMachineClause(AConstantsMachineClause node) { hasConstants = true; - List<PExpression> copy = new ArrayList<>(node.getIdentifiers()); - for (PExpression e : copy) { - AIdentifierExpression c = (AIdentifierExpression) e; - String name = Utils.getTIdentifierListAsString(c.getIdentifier()); - exist(c.getIdentifier()); - constants.put(name, c); - } + extractIdentifierExpressions(new ArrayList<>(node.getIdentifiers()), constants); } @Override public void caseAAbstractConstantsMachineClause(AAbstractConstantsMachineClause node) { hasConstants = true; - List<PExpression> copy = new ArrayList<>(node.getIdentifiers()); - for (PExpression e : copy) { - AIdentifierExpression c = (AIdentifierExpression) e; - String name = Utils.getTIdentifierListAsString(c.getIdentifier()); - exist(c.getIdentifier()); - constants.put(name, c); - } + extractIdentifierExpressions(new ArrayList<>(node.getIdentifiers()), constants); } @Override public void caseAVariablesMachineClause(AVariablesMachineClause node) { - List<PExpression> copy = new ArrayList<>(node.getIdentifiers()); - for (PExpression e : copy) { - AIdentifierExpression v = (AIdentifierExpression) e; - String name = Utils.getTIdentifierListAsString(v.getIdentifier()); - exist(v.getIdentifier()); - variables.put(name, v); - } + extractIdentifierExpressions(new ArrayList<>(node.getIdentifiers()), variables); } @Override public void caseAConcreteVariablesMachineClause(AConcreteVariablesMachineClause node) { - List<PExpression> copy = new ArrayList<>(node.getIdentifiers()); + extractIdentifierExpressions(new ArrayList<>(node.getIdentifiers()), variables); + } + + private void extractIdentifierExpressions(List<PExpression> copy, Map<String, Node> addToMap) { for (PExpression e : copy) { - AIdentifierExpression v = (AIdentifierExpression) e; - String name = Utils.getTIdentifierListAsString(v.getIdentifier()); - exist(v.getIdentifier()); - variables.put(name, v); + AIdentifierExpression identifier = getIdentifierExpression(e); + String name = Utils.getTIdentifierListAsString(identifier.getIdentifier()); + exist(identifier.getIdentifier()); + addToMap.put(name, identifier); } } diff --git a/src/main/java/de/tlc4b/analysis/Typechecker.java b/src/main/java/de/tlc4b/analysis/Typechecker.java index 7e6bf658ab12c14928b98f862c5c481c53606a25..2a777c5f067864be40aded1aecfca8001888b848 100644 --- a/src/main/java/de/tlc4b/analysis/Typechecker.java +++ b/src/main/java/de/tlc4b/analysis/Typechecker.java @@ -30,6 +30,8 @@ import de.tlc4b.exceptions.UnificationException; import de.tlc4b.ltl.LTLBPredicate; import de.tlc4b.ltl.LTLFormulaVisitor; +import static de.tlc4b.util.UtilMethods.getIdentifierExpression; + /** * TODO we need a second run over the AST to check if all local variables have a * type. This run should be performed after the normal model checking task. @@ -179,41 +181,25 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker { @Override public void caseAConstantsMachineClause(AConstantsMachineClause node) { List<PExpression> copy = new ArrayList<>(node.getIdentifiers()); - for (PExpression e : copy) { - AIdentifierExpression id = (AIdentifierExpression) e; - UntypedType u = new UntypedType(); - setType(id, u); - } + copy.forEach(e -> setType(getIdentifierExpression(e), new UntypedType())); } @Override public void caseAAbstractConstantsMachineClause(AAbstractConstantsMachineClause node) { List<PExpression> copy = new ArrayList<>(node.getIdentifiers()); - for (PExpression e : copy) { - AIdentifierExpression id = (AIdentifierExpression) e; - UntypedType u = new UntypedType(); - setType(id, u); - } + copy.forEach(e -> setType(getIdentifierExpression(e), new UntypedType())); } @Override public void caseAVariablesMachineClause(AVariablesMachineClause node) { List<PExpression> copy = new ArrayList<>(node.getIdentifiers()); - for (PExpression e : copy) { - AIdentifierExpression v = (AIdentifierExpression) e; - UntypedType u = new UntypedType(); - setType(v, u); - } + copy.forEach(e -> setType(getIdentifierExpression(e), new UntypedType())); } @Override public void caseAConcreteVariablesMachineClause(AConcreteVariablesMachineClause node) { List<PExpression> copy = new ArrayList<>(node.getIdentifiers()); - for (PExpression e : copy) { - AIdentifierExpression v = (AIdentifierExpression) e; - UntypedType u = new UntypedType(); - setType(v, u); - } + copy.forEach(e -> setType(getIdentifierExpression(e), new UntypedType())); } /** diff --git a/src/main/java/de/tlc4b/util/UtilMethods.java b/src/main/java/de/tlc4b/util/UtilMethods.java index 407f9447a97157e13c71e63daac51941ccce247e..fedd59716bea35c1dd8f89ac9db588a69b7bde71 100644 --- a/src/main/java/de/tlc4b/util/UtilMethods.java +++ b/src/main/java/de/tlc4b/util/UtilMethods.java @@ -2,9 +2,7 @@ package de.tlc4b.util; import java.util.ArrayList; -import de.be4.classicalb.core.parser.node.AIdentifierExpression; -import de.be4.classicalb.core.parser.node.Node; -import de.be4.classicalb.core.parser.node.TIdentifierLiteral; +import de.be4.classicalb.core.parser.node.*; import de.hhu.stups.sablecc.patch.SourcePosition; public class UtilMethods { @@ -16,6 +14,23 @@ public class UtilMethods { return new AIdentifierExpression(idList); } + public static AIdentifierExpression getIdentifierExpression(PExpression e) { + AIdentifierExpression identifier; + if (e instanceof ADescriptionExpression) { + PExpression desc = ((ADescriptionExpression) e).getExpression(); + if (desc instanceof AIdentifierExpression) { + identifier = (AIdentifierExpression) desc; + } else { + throw new IllegalStateException("Unexpected expression type: " + e); + } + } else if (e instanceof AIdentifierExpression) { + identifier = (AIdentifierExpression) e; + } else { + throw new IllegalStateException("Unexpected expression type: " + e); + } + return identifier; + } + public static String getPositionAsString(Node node) { StringBuilder sb = new StringBuilder(); SourcePosition startPos = node.getStartPos(); diff --git a/src/test/java/de/tlc4b/analysis/ConstantsTest.java b/src/test/java/de/tlc4b/analysis/ConstantsTest.java index ccd9b9cd60b9d3493400590188e2937e7714aeb2..fc42e4d2d88e8a69a8b32fe067820f67407884fd 100644 --- a/src/test/java/de/tlc4b/analysis/ConstantsTest.java +++ b/src/test/java/de/tlc4b/analysis/ConstantsTest.java @@ -38,7 +38,7 @@ public class ConstantsTest { } @Test - public void testConstantMultiplePossipleValues() throws Exception { + public void testConstantMultiplePossibleValues() throws Exception { String machine = "MACHINE test\n" + "CONSTANTS k \n" + "PROPERTIES k : {1} \n" + "END"; @@ -134,5 +134,18 @@ public class ConstantsTest { + "======"; compare(expected, machine); } + + @Test + public void testConstantsDescPragma() throws Exception { + String machine = "MACHINE test\n" + + "CONSTANTS n /*@desc description*/\n" + + "PROPERTIES n = 1\n" + + "END"; + + String expected = "---- MODULE test----\n" + + "n == 1\n" + + "======"; + compare(expected, machine); + } }