Commit 559327a5 authored by Sarah Grebing's avatar Sarah Grebing

added first testcases for try and closes

parent 79786fc6
Pipeline #13279 failed with stage
in 10 seconds
......@@ -114,7 +114,10 @@ casesStmt
;
casesList
: (TRY | (CASE (expression | (CLOSES INDENT closesScript=stmtList DEDENT)))) COLON INDENT? body=stmtList DEDENT?
: (TRY |
(CASE (expression
| (CLOSES INDENT closesScript=stmtList DEDENT) ) ) )
COLON INDENT? body=stmtList DEDENT?
;
/*closesExpression
......
......@@ -36,7 +36,7 @@ public class KeYInterpreterTest {
@Test
public void testIsClosable() throws IOException, ProblemLoaderException {
public void testTryFail() throws IOException, ProblemLoaderException {
facade.loadKeyFileSync(new File("src/test/resources/edu/kit/iti/formal/psdbg/interpreter/contraposition/contraposition.key"));
Interpreter<KeyData> i = execute(getClass().getResourceAsStream("contraposition/testIsClosable.kps"));
List<GoalNode<KeyData>> goals = i.getCurrentState().getGoals();
......@@ -45,8 +45,33 @@ public class KeYInterpreterTest {
Assert.assertEquals("Label for node " + goal.getData().getNode(), "impLeft // impRight // $$", goal.getData().getRuleLabel());
}
}
@Test
public void testClosesFail() throws IOException, ProblemLoaderException {
facade.loadKeyFileSync(new File("src/test/resources/edu/kit/iti/formal/psdbg/interpreter/contraposition/contraposition.key"));
Interpreter<KeyData> i = execute(getClass().getResourceAsStream("contraposition/closes.kps"));
List<GoalNode<KeyData>> goals = i.getCurrentState().getGoals();
Assert.assertEquals(2, goals.size());
for (GoalNode<KeyData> goal : goals) {
Assert.assertEquals("Label for node " + goal.getData().getNode(), "impLeft // impRight // $$", goal.getData().getRuleLabel());
}
// Assert.assertEquals(10, i.getCurrentState().getGoals().size());
}
@Test
public void testClosesScriptSuccess() throws IOException, ProblemLoaderException {
facade.loadKeyFileSync(new File("src/test/resources/edu/kit/iti/formal/psdbg/interpreter/contraposition/contraposition.key"));
Interpreter<KeyData> i = execute(getClass().getResourceAsStream("contraposition/closesSuccess.kps"));
List<GoalNode<KeyData>> goals = i.getCurrentState().getGoals();
Assert.assertEquals(2, goals.size());
for (GoalNode<KeyData> goal : goals) {
Assert.assertEquals("Label for node " + goal.getData().getNode(), "impRight // impLeft // impRight // $$", goal.getData().getRuleLabel());
}
}
}
script t1(){
impRight;
impLeft;
cases{
case closes {impRight; } :
impRight; //should not close proof
}
}
\ No newline at end of file
script t1(){
impRight;
impLeft;
cases{
case closes {
auto; //should close
}:
impRight; //should not close proof
case match `==> imp(not(q),not(p))`:
auto;
}
}
\ No newline at end of file
......@@ -184,8 +184,6 @@ public class Interpreter<T> extends DefaultASTVisitor<Object>
//handle cases
List<CaseStatement> cases = casesStatement.getCases();
// Map<GoalNode, Pair<VariableAssignment, Statements>> goalToCaseMapping = matchGoalsToCases(allGoalsBeforeCases, casesStatement);
for (GoalNode<T> goal : allGoalsBeforeCases) {
newState(goal); //to allow the visit method for the case stmt to retrieve goal
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment