From 71c49a4cba212c3010572c77e81af34a176bfe6b Mon Sep 17 00:00:00 2001
From: Fabian Vu <Fabian.Vu@hhu.de>
Date: Thu, 29 Sep 2022 09:33:23 +0200
Subject: [PATCH] Merge checking prop and explore state space operation
---
src/main/java/de/prob/voparser/VOTypeChecker.java | 11 +++++++----
src/main/java/de/prob/voparser/VTType.java | 2 +-
src/test/java/de/prob/voparser/VOScopingTest.java | 4 ++--
.../java/de/prob/voparser/VOTypeCheckingTest.java | 4 ++--
4 files changed, 12 insertions(+), 9 deletions(-)
diff --git a/src/main/java/de/prob/voparser/VOTypeChecker.java b/src/main/java/de/prob/voparser/VOTypeChecker.java
index 9f95c36..0288979 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 0159357..b6dab03 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 66eaf0a..d033f72 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 815f610..16ed0c6 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");
}
--
GitLab