From 9c8f234eb5f514aeb59dd19f4f13e31286938629 Mon Sep 17 00:00:00 2001 From: Jan Gruteser <jan.gruteser@hhu.de> Date: Sat, 27 Jul 2024 07:46:27 +0200 Subject: [PATCH] support description pragma for constants and variables --- .../de/tlc4b/analysis/MachineContext.java | 111 +++--------------- .../java/de/tlc4b/analysis/Typechecker.java | 26 +--- src/main/java/de/tlc4b/util/UtilMethods.java | 21 +++- .../java/de/tlc4b/analysis/ConstantsTest.java | 15 ++- 4 files changed, 54 insertions(+), 119 deletions(-) diff --git a/src/main/java/de/tlc4b/analysis/MachineContext.java b/src/main/java/de/tlc4b/analysis/MachineContext.java index 9b1012a..b80100d 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 7e6bf65..2a777c5 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 407f944..fedd597 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 ccd9b9c..fc42e4d 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); + } } -- GitLab