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

Merge checking prop and explore state space operation

parent 8960c2d9
No related branches found
No related tags found
No related merge requests found
Pipeline #99154 passed
......@@ -109,18 +109,21 @@ public class VOTypeChecker extends DepthFirstAdapter {
case RESET:
newAnimatorState = newAnimatorState.cons(AnimatorState.TRACE);
break;
case STATIC:
newAnimatorState = newAnimatorState.disjoin(AnimatorState.TRACE);
newAnimatorState = newAnimatorState.disjoin(AnimatorState.STATE_SPACE);
break;
case TRACE:
valid = newAnimatorState.contains(AnimatorState.TRACE);
break;
case STATE_SPACE:
valid = newAnimatorState.contains(AnimatorState.STATE_SPACE);
break;
case CHECKING_PROP:
newAnimatorState = newAnimatorState.disjoin(AnimatorState.TRACE);
newAnimatorState = newAnimatorState.disjoin(AnimatorState.STATE_SPACE);
break;
case EXPLORING_STATE_SPACE:
case EXPLORE:
valid = newAnimatorState.contains(AnimatorState.TRACE);
newAnimatorState = newAnimatorState.disjoin(AnimatorState.TRACE);
newAnimatorState = newAnimatorState.cons(AnimatorState.STATE_SPACE);
break;
default:
break;
......
......@@ -3,5 +3,5 @@ package de.prob.voparser;
public enum VTType {
RELOAD, RESET, STATIC,
TRACE, STATE_SPACE,
CHECKING_PROP, EXPLORING_STATE_SPACE
EXPLORE
}
......@@ -13,7 +13,7 @@ public class VOScopingTest {
@Test
public void testAtomic() throws VOParseException {
VOParser voParser = new VOParser();
voParser.registerTask("MC1", VTType.CHECKING_PROP);
voParser.registerTask("MC1", VTType.EXPLORE);
voParser.scopeCheck("MC1");
}
......@@ -61,7 +61,7 @@ public class VOScopingTest {
@Test
public void testDot() throws VOParseException {
VOParser voParser = new VOParser();
voParser.registerTask("MC1.1", VTType.CHECKING_PROP);
voParser.registerTask("MC1.1", VTType.EXPLORE);
voParser.scopeCheck("MC1.1");
}
......
......@@ -13,7 +13,7 @@ public class VOTypeCheckingTest {
@Test
public void testAtomic() throws VOParseException {
VOParser voParser = new VOParser();
voParser.registerTask("MC1", VTType.CHECKING_PROP);
voParser.registerTask("MC1", VTType.EXPLORE);
voParser.typeCheck("MC1");
}
......@@ -21,7 +21,7 @@ public class VOTypeCheckingTest {
public void testSequential() throws VOParseException {
VOParser voParser = new VOParser();
voParser.registerTask("MC1", VTType.TRACE);
voParser.registerTask("MC2", VTType.CHECKING_PROP);
voParser.registerTask("MC2", VTType.EXPLORE);
voParser.typeCheck("MC1;MC2");
}
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment