diff --git a/src/main/java/de/prob/voparser/VOTypeChecker.java b/src/main/java/de/prob/voparser/VOTypeChecker.java index 9f95c36a800331b6d0d9550050f6283b89df8ca1..0288979b8a8574b73a036540e15b380a3af0e2ed 100644 --- a/src/main/java/de/prob/voparser/VOTypeChecker.java +++ b/src/main/java/de/prob/voparser/VOTypeChecker.java @@ -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; diff --git a/src/main/java/de/prob/voparser/VTType.java b/src/main/java/de/prob/voparser/VTType.java index 0159357dca849ccc8f60869d6d620f93cb4a856f..b6dab03f1b5757fe0236795d8ca31e292b901951 100644 --- a/src/main/java/de/prob/voparser/VTType.java +++ b/src/main/java/de/prob/voparser/VTType.java @@ -3,5 +3,5 @@ package de.prob.voparser; public enum VTType { RELOAD, RESET, STATIC, TRACE, STATE_SPACE, - CHECKING_PROP, EXPLORING_STATE_SPACE + EXPLORE } diff --git a/src/test/java/de/prob/voparser/VOScopingTest.java b/src/test/java/de/prob/voparser/VOScopingTest.java index 66eaf0a4eccf47e73b30aac118aa9cc335001fab..d033f722b6226135e9d5cc39b01b51beea9eafd2 100644 --- a/src/test/java/de/prob/voparser/VOScopingTest.java +++ b/src/test/java/de/prob/voparser/VOScopingTest.java @@ -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"); } diff --git a/src/test/java/de/prob/voparser/VOTypeCheckingTest.java b/src/test/java/de/prob/voparser/VOTypeCheckingTest.java index 815f610f9069c676147ceedf78dc5a636fde7964..16ed0c65a6caaa6a8a6412a7f3bb6cf8558a1c23 100644 --- a/src/test/java/de/prob/voparser/VOTypeCheckingTest.java +++ b/src/test/java/de/prob/voparser/VOTypeCheckingTest.java @@ -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"); }