From f74185e9de4aae73d1a0c0bc4e6d7ec32f5189db Mon Sep 17 00:00:00 2001
From: dgelessus <dgelessus@users.noreply.github.com>
Date: Mon, 6 May 2024 22:54:15 +0200
Subject: [PATCH] Remove sequential operator and meta-state
In the latest formalization of VOs, sequential composition is done by
passing a validation task/expression as an argument to another task.
This makes the previous "animator meta-state" concept obsolete.
Because this parser doesn't handle validation task arguments yet (and we
still have work to do before we can implement that usefully), there is
nothing to be type-checked at this stage anymore, so I'm removing the
type checker completely for now.
The first implementation of the new type checker will probably be inside
ProB 2 UI. Once we have formalized the validation task types and their
parameters well enough, we can implement a standalone type checker in
this library again.
---
.../java/de/prob/voparser/AnimatorState.java | 5 -
src/main/java/de/prob/voparser/VOParser.java | 41 +-----
.../prob/voparser/VOTypeCheckException.java | 17 ---
.../java/de/prob/voparser/VOTypeChecker.java | 138 ------------------
src/main/java/de/prob/voparser/VTType.java | 7 -
src/main/sablecc/VOParser.scc | 8 -
.../java/de/prob/voparser/VOParserTest.java | 8 +-
.../de/prob/voparser/VOTypeCheckingTest.java | 83 -----------
8 files changed, 6 insertions(+), 301 deletions(-)
delete mode 100644 src/main/java/de/prob/voparser/AnimatorState.java
delete mode 100644 src/main/java/de/prob/voparser/VOTypeCheckException.java
delete mode 100644 src/main/java/de/prob/voparser/VOTypeChecker.java
delete mode 100644 src/main/java/de/prob/voparser/VTType.java
delete mode 100644 src/test/java/de/prob/voparser/VOTypeCheckingTest.java
diff --git a/src/main/java/de/prob/voparser/AnimatorState.java b/src/main/java/de/prob/voparser/AnimatorState.java
deleted file mode 100644
index e3d8d61..0000000
--- a/src/main/java/de/prob/voparser/AnimatorState.java
+++ /dev/null
@@ -1,5 +0,0 @@
-package de.prob.voparser;
-
-public enum AnimatorState {
- TRACE, STATE_SPACE;
-}
diff --git a/src/main/java/de/prob/voparser/VOParser.java b/src/main/java/de/prob/voparser/VOParser.java
index fe5c544..4dad9b9 100644
--- a/src/main/java/de/prob/voparser/VOParser.java
+++ b/src/main/java/de/prob/voparser/VOParser.java
@@ -1,27 +1,17 @@
package de.prob.voparser;
+import java.io.IOException;
+import java.io.PushbackReader;
+import java.io.StringReader;
+
import de.prob.voparser.lexer.Lexer;
import de.prob.voparser.lexer.LexerException;
import de.prob.voparser.node.Start;
import de.prob.voparser.parser.Parser;
import de.prob.voparser.parser.ParserException;
-import java.io.IOException;
-import java.io.PushbackReader;
-import java.io.StringReader;
-import java.util.HashMap;
-import java.util.Map;
-
public class VOParser {
-
- private final Map<String, VTType> tasks;
-
- private final VOTypeChecker typeChecker;
-
- public VOParser() {
- this.tasks = new HashMap<>();
- this.typeChecker = new VOTypeChecker(this);
- }
+ public VOParser() {}
public Start parseFormula(String formula) {
return parseAST(formula);
@@ -44,25 +34,4 @@ public class VOParser {
}
return ast;
}
-
- public void registerTask(String id, VTType type) {
- tasks.put(id, type);
- }
-
- public void deregisterTask(String id) {
- tasks.remove(id);
- }
-
- public void typeCheck(Start ast) {
- typeChecker.typeCheck(ast);
- }
-
- public void typeCheck(String formula) {
- Start start = parseFormula(formula);
- typeChecker.typeCheck(start);
- }
-
- public Map<String, VTType> getTasks() {
- return tasks;
- }
}
diff --git a/src/main/java/de/prob/voparser/VOTypeCheckException.java b/src/main/java/de/prob/voparser/VOTypeCheckException.java
deleted file mode 100644
index a0b0555..0000000
--- a/src/main/java/de/prob/voparser/VOTypeCheckException.java
+++ /dev/null
@@ -1,17 +0,0 @@
-package de.prob.voparser;
-
-public class VOTypeCheckException extends VOException {
- private static final long serialVersionUID = 1L;
-
- public VOTypeCheckException(final String message, final Throwable cause) {
- super(message, cause);
- }
-
- public VOTypeCheckException(final String message) {
- this(message, null);
- }
-
- public VOTypeCheckException(final Throwable cause) {
- this(cause == null ? null : cause.toString(), cause);
- }
-}
diff --git a/src/main/java/de/prob/voparser/VOTypeChecker.java b/src/main/java/de/prob/voparser/VOTypeChecker.java
deleted file mode 100644
index a73e6eb..0000000
--- a/src/main/java/de/prob/voparser/VOTypeChecker.java
+++ /dev/null
@@ -1,138 +0,0 @@
-package de.prob.voparser;
-
-
-import com.github.krukow.clj_lang.PersistentHashSet;
-import de.prob.voparser.analysis.DepthFirstAdapter;
-import de.prob.voparser.node.AAndVo;
-import de.prob.voparser.node.AIdentifierVo;
-import de.prob.voparser.node.AOrVo;
-import de.prob.voparser.node.ASequentialVo;
-import de.prob.voparser.node.Node;
-import de.prob.voparser.node.Start;
-
-public class VOTypeChecker extends DepthFirstAdapter {
-
- private final VOParser voParser;
-
- private PersistentHashSet<AnimatorState> modifiedAnimatorState;
-
- public VOTypeChecker(VOParser voParser) {
- this.voParser = voParser;
- this.modifiedAnimatorState = PersistentHashSet.create(AnimatorState.STATE_SPACE, AnimatorState.TRACE);
- }
-
- public void typeCheck(Start start) {
- start.apply(this);
- }
-
- private PersistentHashSet<AnimatorState> visitVOExpression(Node node, PersistentHashSet<AnimatorState> animatorState) {
- if (node instanceof AIdentifierVo) {
- return visitIdentifierNode((AIdentifierVo) node, animatorState);
- } else if (node instanceof AAndVo) {
- return visitAndExpression((AAndVo) node, animatorState);
- } else if(node instanceof AOrVo) {
- return visitOrExpression((AOrVo) node, animatorState);
- } else if(node instanceof ASequentialVo) {
- return visitSequentialExpression((ASequentialVo) node, animatorState);
- } else {
- throw new RuntimeException("Node type unknown: " + node.getClass());
- }
- }
-
- @Override
- public void caseAAndVo(AAndVo node) {
- modifiedAnimatorState = visitAndExpression(node, modifiedAnimatorState);
- }
-
- private PersistentHashSet<AnimatorState> visitAndExpression(AAndVo node, PersistentHashSet<AnimatorState> animatorState) {
- PersistentHashSet<AnimatorState> leftAnimatorState = visitVOExpression(node.getLeft(), animatorState);
- PersistentHashSet<AnimatorState> rightAnimatorState = visitVOExpression(node.getRight(), animatorState);
- PersistentHashSet<AnimatorState> resultAnimatorState = leftAnimatorState;
- for(AnimatorState state : leftAnimatorState) {
- if(!rightAnimatorState.contains(state)) {
- // Do not use remove as PersistentHashSet is immutable
- resultAnimatorState = resultAnimatorState.disjoin(state);
- }
- }
- resultAnimatorState = resultAnimatorState.disjoin(AnimatorState.TRACE);
- return resultAnimatorState;
- }
-
- @Override
- public void caseAOrVo(AOrVo node) {
- modifiedAnimatorState = visitOrExpression(node, modifiedAnimatorState);
- }
-
- private PersistentHashSet<AnimatorState> visitOrExpression(AOrVo node, PersistentHashSet<AnimatorState> animatorState) {
- PersistentHashSet<AnimatorState> leftAnimatorState = visitVOExpression(node.getLeft(), animatorState);
- PersistentHashSet<AnimatorState> rightAnimatorState = visitVOExpression(node.getRight(), animatorState);
- PersistentHashSet<AnimatorState> resultAnimatorState = leftAnimatorState;
- for(AnimatorState state : leftAnimatorState) {
- if(!rightAnimatorState.contains(state)) {
- // Do not use remove as PersistentHashSet is immutable
- resultAnimatorState = resultAnimatorState.disjoin(state);
- }
- }
- resultAnimatorState = resultAnimatorState.disjoin(AnimatorState.STATE_SPACE);
- return resultAnimatorState;
- }
-
- @Override
- public void caseASequentialVo(ASequentialVo node) {
- modifiedAnimatorState = visitSequentialExpression(node, modifiedAnimatorState);
- }
-
- private PersistentHashSet<AnimatorState> visitSequentialExpression(ASequentialVo node, PersistentHashSet<AnimatorState> animatorState) {
- PersistentHashSet<AnimatorState> leftAnimatorState = visitVOExpression(node.getLeft(), animatorState);
- return visitVOExpression(node.getRight(), leftAnimatorState);
- }
-
- @Override
- public void caseAIdentifierVo(AIdentifierVo node) {
- modifiedAnimatorState = visitIdentifierNode(node, modifiedAnimatorState);
- }
-
-
- private PersistentHashSet<AnimatorState> visitIdentifierNode(AIdentifierVo node, PersistentHashSet<AnimatorState> animatorState) {
- final String id = node.getIdentifierLiteral().getText();
- if (!voParser.getTasks().containsKey(id)) {
- throw new VOTypeCheckException("Unknown validation task identifier: " + id);
- }
- VTType type = voParser.getTasks().get(id);
- PersistentHashSet<AnimatorState> newAnimatorState = animatorState;
- switch (type) {
- case RELOAD:
- newAnimatorState = newAnimatorState.cons(AnimatorState.TRACE);
- newAnimatorState = newAnimatorState.cons(AnimatorState.STATE_SPACE);
- break;
- case RESET:
- newAnimatorState = newAnimatorState.cons(AnimatorState.TRACE);
- break;
- case STATIC:
- newAnimatorState = newAnimatorState.disjoin(AnimatorState.TRACE);
- newAnimatorState = newAnimatorState.disjoin(AnimatorState.STATE_SPACE);
- break;
- case TRACE:
- if (!newAnimatorState.contains(AnimatorState.TRACE)) {
- throw new VOTypeCheckException("Validation task " + id + " requires a trace");
- }
- break;
- case STATE_SPACE:
- if (!newAnimatorState.contains(AnimatorState.STATE_SPACE)) {
- throw new VOTypeCheckException("Validation task " + id + " requires a state space");
- }
- newAnimatorState = newAnimatorState.disjoin(AnimatorState.TRACE);
- newAnimatorState = newAnimatorState.disjoin(AnimatorState.STATE_SPACE);
- break;
- case EXPLORE:
- if (!newAnimatorState.contains(AnimatorState.TRACE)) {
- throw new VOTypeCheckException("Validation task " + id + " requires a trace");
- }
- newAnimatorState = newAnimatorState.disjoin(AnimatorState.TRACE);
- break;
- default:
- break;
- }
- return newAnimatorState;
- }
-}
diff --git a/src/main/java/de/prob/voparser/VTType.java b/src/main/java/de/prob/voparser/VTType.java
deleted file mode 100644
index b6dab03..0000000
--- a/src/main/java/de/prob/voparser/VTType.java
+++ /dev/null
@@ -1,7 +0,0 @@
-package de.prob.voparser;
-
-public enum VTType {
- RELOAD, RESET, STATIC,
- TRACE, STATE_SPACE,
- EXPLORE
-}
diff --git a/src/main/sablecc/VOParser.scc b/src/main/sablecc/VOParser.scc
index e719f31..fe3a649 100644
--- a/src/main/sablecc/VOParser.scc
+++ b/src/main/sablecc/VOParser.scc
@@ -23,9 +23,6 @@ Tokens
and = '&' | 0x2227 | 'and';
or = 'or' | 0x2228 | '||';
- /* Sequential Operator*/
- sequential = ';';
-
identifier_literal = (letter | '_') (letter | '_' | digit | '.' | ',')*;
white_space = line_break | layout_char+;
@@ -47,10 +44,6 @@ Productions
vo_formula1 {-> vo_formula1.vo};
vo_formula1 {-> vo} =
- {sequential} [left]:vo_formula1 sequential [right]:vo_formula2 {-> New vo.sequential(left.vo, right.vo)} |
- vo_formula2 {-> vo_formula2.vo};
-
- vo_formula2 {-> vo} =
{identifier} identifier_literal {-> New vo.identifier(identifier_literal)} |
{par} l_par vo_formula r_par {-> vo_formula.vo};
@@ -62,5 +55,4 @@ Abstract Syntax Tree
vo =
{and} [left]:vo [right]:vo |
{or} [left]:vo [right]:vo |
- {sequential} [left]:vo [right]:vo |
{identifier} identifier_literal;
diff --git a/src/test/java/de/prob/voparser/VOParserTest.java b/src/test/java/de/prob/voparser/VOParserTest.java
index 4e8956b..05b815c 100644
--- a/src/test/java/de/prob/voparser/VOParserTest.java
+++ b/src/test/java/de/prob/voparser/VOParserTest.java
@@ -16,12 +16,6 @@ public class VOParserTest {
voParser.parseFormula("MC1");
}
- @Test
- public void testSequential() {
- VOParser voParser = new VOParser();
- voParser.parseFormula("MC1;TR1");
- }
-
@Test
public void testAnd() {
VOParser voParser = new VOParser();
@@ -44,7 +38,7 @@ public class VOParserTest {
@Test(expected = VOParseException.class)
public void testParseError() {
VOParser voParser = new VOParser();
- voParser.parseFormula("MC.1;");
+ voParser.parseFormula("MC.1&");
}
}
diff --git a/src/test/java/de/prob/voparser/VOTypeCheckingTest.java b/src/test/java/de/prob/voparser/VOTypeCheckingTest.java
deleted file mode 100644
index 96e2baa..0000000
--- a/src/test/java/de/prob/voparser/VOTypeCheckingTest.java
+++ /dev/null
@@ -1,83 +0,0 @@
-package de.prob.voparser;
-
-/**
- * (c) 2022 Lehrstuhl fuer Softwaretechnik und Programmiersprachen,
- * Heinrich Heine Universitaet Duesseldorf
- * This software is licenced under EPL 1.0 (http://www.eclipse.org/org/documents/epl-v10.html)
- * */
-
-import org.junit.Test;
-
-public class VOTypeCheckingTest {
-
- @Test
- public void testAtomic() {
- VOParser voParser = new VOParser();
- voParser.registerTask("MC1", VTType.EXPLORE);
- voParser.typeCheck("MC1");
- }
-
- @Test
- public void testSequential() {
- VOParser voParser = new VOParser();
- voParser.registerTask("MC1", VTType.TRACE);
- voParser.registerTask("MC2", VTType.EXPLORE);
- voParser.typeCheck("MC1;MC2");
- }
-
- @Test(expected = VOTypeCheckException.class)
- public void testSequentialError() {
- VOParser voParser = new VOParser();
- voParser.registerTask("MC1", VTType.TRACE);
- voParser.typeCheck("MC1;TR1");
- }
-
- @Test(expected = VOTypeCheckException.class)
- public void testSequential2() {
- VOParser voParser = new VOParser();
- voParser.registerTask("MC1", VTType.TRACE);
- voParser.registerTask("MC2", VTType.TRACE);
- voParser.registerTask("TR1", VTType.TRACE);
- voParser.typeCheck("(MC1 & MC2);TR1");
- }
-
- @Test
- public void testAnd() {
- VOParser voParser = new VOParser();
- voParser.registerTask("MC1", VTType.TRACE);
- voParser.registerTask("TR1", VTType.TRACE);
- voParser.typeCheck("MC1 & TR1");
- }
-
- @Test
- public void testAnd2() {
- VOParser voParser = new VOParser();
- voParser.registerTask("MC1.1", VTType.TRACE);
- voParser.registerTask("TR1.1", VTType.TRACE);
- voParser.registerTask("MC2.1", VTType.TRACE);
- voParser.registerTask("TR2.1", VTType.TRACE);
- voParser.typeCheck("(MC1.1; TR1.1) & (MC2.1; TR2.1)");
- }
-
- @Test
- public void testOr() {
- VOParser voParser = new VOParser();
- voParser.registerTask("MC1", VTType.TRACE);
- voParser.registerTask("TR1", VTType.TRACE);
- voParser.typeCheck("MC1 or TR1");
- }
-
- @Test
- public void testDot() {
- VOParser voParser = new VOParser();
- voParser.registerTask("MC1.1", VTType.EXPLORE);
- voParser.typeCheck("MC1.1");
- }
-
- @Test(expected = VOTypeCheckException.class)
- public void testScopingError() {
- VOParser voParser = new VOParser();
- voParser.typeCheck("MC1");
- }
-
-}
--
GitLab