Commit c3dba26d authored by Sarah Grebing's avatar Sarah Grebing

Adding test cases

parent fc3786e4
Pipeline #13608 failed with stage
in 2 minutes and 18 seconds
......@@ -216,7 +216,9 @@ public class MatcherFacadeTest {
"fint2(1,2), fint2(2,3), !p ==> pred(a), p",
"fint2(1, ?X), fint2(?X, ?Y) ==> p",
"[{EMPTY_MATCH=null, ?X=Z(2(#)), ?Y=Z(3(#))}]");
shouldMatchSeq("2 >= 1, h2(1,2) = h2(2,3), h2(2,3) = 0 ==> p, !p", "?X=0 ==>", "[{?X= h2(2,3)}]");
shouldMatchSeq("2 >= 1, h2(1,2) = h2(2,3), h2(2,3) = 0 ==> p, !p", "?X=0 ==>", "[{?X=h2(Z(2(#)),Z(3(#)))}]");
shouldMatchSeq("pred(a) <-> pred(b), pred(a), pred(b) ==> p", "?X <-> ?Y ==> ", "[{?X=pred(a), ?Y=pred(b)}]");
}
private void shouldMatchSeq(String seq, String seqPattern, String exp) throws ParserException {
......
package edu.kit.iti.formal.psdbg.interpreter;
import de.uka.ilkd.key.logic.Term;
import de.uka.ilkd.key.logic.sort.Sort;
import de.uka.ilkd.key.parser.DefaultTermParser;
import de.uka.ilkd.key.parser.ParserException;
import static edu.kit.iti.formal.psdbg.TestHelper.getFile;
import edu.kit.iti.formal.psdbg.interpreter.data.KeyData;
import edu.kit.iti.formal.psdbg.interpreter.data.State;
import edu.kit.iti.formal.psdbg.parser.ast.Variable;
import edu.kit.iti.formal.psdbg.parser.data.Value;
import org.apache.commons.cli.ParseException;
import org.junit.Assert;
import org.junit.Test;
import java.io.IOException;
import java.io.StringReader;
/**
* @author Alexander Weigl
......@@ -48,15 +55,25 @@ public class ExecuteTest {
}
@Test
public void testContrapositionCut() throws IOException, ParseException {
public void testContrapositionCut() throws IOException, ParseException, ParserException {
Execute execute = create(
getFile(getClass(), "contraposition/contraposition.key"),
"-s", getFile(getClass(), "contraposition/cutTest.kps"));
Interpreter<KeyData> i = execute.run();
State<KeyData> currentState = i.getCurrentState();
System.out.println(currentState);
//This reveals a bug in the cases merge
//This revealed a bug in the interpreter for body of a case
Assert.assertEquals("Number of goals has to be two ", 2, i.getCurrentGoals().size());
KeyData goal0_data = currentState.getGoals().get(0).getData();
Value y = currentState.getGoals().get(0).getAssignments().getValue(new Variable("Y"));
Assert.assertTrue(goal0_data.getRuleLabel().contains("cut"));
KeyData goal1_data = currentState.getGoals().get(1).getData();
Assert.assertTrue(goal1_data.getRuleLabel().contains("cut"));
DefaultTermParser dp = new DefaultTermParser();
Term s = dp.parse(new StringReader(y.getData().toString()), Sort.FORMULA, goal0_data.getEnv().getServices(), goal0_data.getProof().getNamespaces(), null);
Assert.assertEquals("Antecedent should contain the cut formula", s, goal0_data.getNode().sequent().antecedent().get(0).formula());
}
}
\ No newline at end of file
script cutTest(){
cut `p <->q`;
//cases{
//cut `p <->q`;
cases{
//X:TERM :=`p`;
// case match `==>?X -> ?Y`:
// cut `?X`[?X \ Y];
case match `==>?X -> ?Y`:
cut `?X`[?X \ Y];
//}
}
}
\ No newline at end of file
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