Skip to content
Snippets Groups Projects

Compare revisions

Changes are shown as if the source revision was being merged into the target revision. Learn more about comparing revisions.

Source

Select target project
No results found
Select Git revision
  • develop
  • 0.1.0
  • 0.2.0
  • 0.2.1
  • 0.3.0
5 results

Target

Select target project
  • general/stups/vo_parser
1 result
Select Git revision
Loading items
Show changes

Commits on Source 2

  • dgelessus's avatar
    Bump version number to 0.3.0-SNAPSHOT in preparation of major changes · 99885c0e
    dgelessus authored
    99885c0e
  • dgelessus's avatar
    Remove sequential operator and meta-state · f74185e9
    dgelessus authored 
    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.
    f74185e9
Show whitespace changes
Inline Side-by-side
Showing
with 7 additions and 302 deletions
build.gradle
View file @ f74185e9
......@@ -7,7 +7,7 @@ plugins {
}
project.group = "de.hhu.stups"
project.version = "0.2.2-SNAPSHOT"
project.version = "0.3.0-SNAPSHOT"
final isSnapshot = project.version.endsWith("-SNAPSHOT")
......
src/main/java/de/prob/voparser/AnimatorState.java deleted 100644 → 0
View file @ 8b5050b7
package de.prob.voparser;
public enum AnimatorState {
TRACE, STATE_SPACE;
}
src/main/java/de/prob/voparser/VOParser.java
View file @ f74185e9
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;
}
}
src/main/java/de/prob/voparser/VOTypeCheckException.java deleted 100644 → 0
View file @ 8b5050b7
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);
}
}
src/main/java/de/prob/voparser/VOTypeChecker.java deleted 100644 → 0
View file @ 8b5050b7
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;
}
}
src/main/java/de/prob/voparser/VTType.java deleted 100644 → 0
View file @ 8b5050b7
package de.prob.voparser;
public enum VTType {
RELOAD, RESET, STATIC,
TRACE, STATE_SPACE,
EXPLORE
}
src/main/sablecc/VOParser.scc
View file @ f74185e9
......@@ -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;
src/test/java/de/prob/voparser/VOParserTest.java
View file @ f74185e9
......@@ -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&");
}
}
src/test/java/de/prob/voparser/VOTypeCheckingTest.java deleted 100644 → 0
View file @ 8b5050b7
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");
}
}